diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs index 2f8055d2e..ff0306a7d 100644 --- a/primer-api/src/Primer/API.hs +++ b/primer-api/src/Primer/API.hs @@ -106,9 +106,9 @@ import Data.Tuple.Extra (curry3) import Optics (ifoldr, over, preview, to, traverseOf, view, (%), (^.), _Just) import Primer.API.NodeFlavor qualified as Flavor import Primer.API.RecordPair (RecordPair (RecordPair)) -import Primer.Action (ActionError, ProgAction, toProgActionInput, toProgActionNoInput) +import Primer.Action (ActionError (ParamNotFound), ProgAction, toProgActionInput, toProgActionNoInput) import Primer.Action.Available qualified as Available -import Primer.Action.ProgError (ProgError (NodeIDNotFound, ParamNotFound, TypeDefConFieldNotFound)) +import Primer.Action.ProgError (ProgError (ActionError, NodeIDNotFound, TypeDefConFieldNotFound)) import Primer.App ( App, DefSelection (..), @@ -178,11 +178,11 @@ import Primer.Core ( ValConName, getID, unLocalName, - unsafeMkLocalName, _bindMeta, _exprMetaLens, _kindMeta, _type, + _typeKindMeta, _typeMeta, _typeMetaLens, ) @@ -245,7 +245,13 @@ import Primer.Name qualified as Name import Primer.Primitives (primDefType) import Primer.TypeDef (ASTTypeDef (..), forgetTypeDefMetadata, typeDefKind, typeDefNameHints, typeDefParameters) import Primer.TypeDef qualified as TypeDef -import Primer.Zipper (SomeNode (..), findNodeWithParent, findType) +import Primer.Zipper ( + SomeNode (..), + findNodeWithParent, + findTypeOrKind, + focusOnKind, + target, + ) import StmContainers.Map qualified as StmMap -- | The API environment. @@ -409,8 +415,8 @@ data APILog | GetProgram' (ReqResp SessionId Prog) | GetProgram (ReqResp SessionId App.Prog) | Edit (ReqResp (SessionId, MutationRequest) (Either ProgError App.Prog)) - | VariablesInScope (ReqResp (SessionId, (GVarName, ID)) (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' ())]), [(GVarName, Type' ())]))) - | GenerateNames (ReqResp (SessionId, ((GVarName, ID), Either (Maybe (Type' ())) (Maybe (Kind' ())))) (Either ProgError [Name.Name])) + | VariablesInScope (ReqResp (SessionId, (GVarName, ID)) (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' () ())]), [(GVarName, Type' () ())]))) + | GenerateNames (ReqResp (SessionId, ((GVarName, ID), Either (Maybe (Type' () ())) (Maybe (Kind' ())))) (Either ProgError [Name.Name])) | EvalStep (ReqResp (SessionId, EvalReq) (Either ProgError EvalResp)) | EvalFull (ReqResp (SessionId, EvalFullReq) (Either ProgError App.EvalFullResp)) | EvalFull' (ReqResp (SessionId, Maybe TerminationBound, Maybe NormalOrderOptions, GVarName) EvalFullResp) @@ -751,7 +757,7 @@ viewProg p = astTypeDefConstructors t <&> \(TypeDef.ValCon nameCon argsCon) -> ValCon { name = nameCon - , fields = viewTreeType' . over _typeMeta (show . view _id) <$> argsCon + , fields = viewTreeType' . over _typeKindMeta (show . view _id) . over _typeMeta (show . view _id) <$> argsCon } } ) @@ -767,10 +773,11 @@ viewProg p = Def.DefPrim d' -> viewTreeType' $ labelNodes $ primDefType d' where labelNodes = - flip evalState (0 :: Int) . traverseOf _typeMeta \() -> do - n <- get - put $ n + 1 - pure $ "primtype_" <> Name.unName (Core.baseName name) <> "_" <> show n + let f () = do + n <- get + put $ n + 1 + pure $ "primtype_" <> Name.unName (Core.baseName name) <> "_" <> show n + in flip evalState (0 :: Int) . (traverseOf _typeKindMeta f <=< traverseOf _typeMeta f) } ) <$> Map.assocs (moduleDefsQualified m) @@ -955,11 +962,11 @@ viewTreeExpr e0 = case e0 of -- | Similar to 'viewTreeExpr', but for 'Type's viewTreeType :: Type -> Tree -viewTreeType = viewTreeType' . over _typeMeta (show . view _id) +viewTreeType = viewTreeType' . over _typeKindMeta (show . view _id) . over _typeMeta (show . view _id) -- | Like 'viewTreeType', but with the flexibility to accept arbitrary textual node identifiers, -- rather than using the type's numeric IDs. -viewTreeType' :: Type' Text -> Tree +viewTreeType' :: Type' Text Text -> Tree viewTreeType' t0 = case t0 of TEmptyHole _ -> Tree @@ -1006,17 +1013,10 @@ viewTreeType' t0 = case t0 of TForall _ n k t -> Tree { nodeId - , body = TextBody $ RecordPair Flavor.TForall $ localName $ unsafeMkLocalName $ withKindAnn $ Name.unName $ unLocalName n - , childTrees = [viewTreeType' t] + , body = TextBody $ RecordPair Flavor.TForall $ localName n + , childTrees = [viewTreeKind' k, viewTreeType' t] , rightChild = Nothing } - where - -- TODO this is a placeholder - -- for now we expect all kinds in student programs to be `KType` - -- but we show something for other kinds, in order to keep rendering injective - withKindAnn = case k of - KType _ -> identity - _ -> (<> (" :: " <> show k)) TLet _ n t b -> Tree { nodeId @@ -1073,14 +1073,14 @@ variablesInScope :: (MonadIO m, MonadThrow m, MonadAPILog l m) => SessionId -> (GVarName, ID) -> - PrimerM m (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' ())]), [(GVarName, Type' ())])) + PrimerM m (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' () ())]), [(GVarName, Type' () ())])) variablesInScope = curry $ logAPI (leftResultError VariablesInScope) $ \(sid, (defname, exprid)) -> liftQueryAppM (handleQuestion (App.VariablesInScope defname exprid)) sid generateNames :: (MonadIO m, MonadThrow m, MonadAPILog l m) => SessionId -> - ((GVarName, ID), Either (Maybe (Type' ())) (Maybe (Kind' ()))) -> + ((GVarName, ID), Either (Maybe (Type' () ())) (Maybe (Kind' ()))) -> PrimerM m (Either ProgError [Name.Name]) generateNames = curry $ logAPI (leftResultError GenerateNames) $ \(sid, ((defname, exprid), tk)) -> liftQueryAppM (handleQuestion $ GenerateName defname exprid tk) sid @@ -1342,28 +1342,27 @@ getSelectionTypeOrKind = curry $ logAPI (noError GetTypeOrKind) $ \(sid, sel0) - maybe (throw' $ NodeIDNotFound id) (pure . fst) (findNodeWithParent id $ astDefExpr def) <&> \case ExprNode e -> viewExprType $ e ^. _exprMetaLens TypeNode t -> viewTypeKind $ t ^. _typeMetaLens + KindNode k -> viewKindOfKind k CaseBindNode b -> viewExprType $ b ^. _bindMeta -- sig node selected - get kind from metadata SigNode -> - maybe (throw' $ NodeIDNotFound id) pure (findType id $ astDefType def) <&> \t -> - viewTypeKind $ t ^. _typeMetaLens + maybe (throw' $ NodeIDNotFound id) pure (findTypeOrKind id $ astDefType def) <&> \case + Left t -> viewTypeKind $ t ^. _typeMetaLens + Right k -> viewKindOfKind k SelectionTypeDef sel -> do def <- snd <$> findASTTypeDef allTypeDefs sel.def case sel.node of -- type def itself selected - return its kind Nothing -> pure $ Kind $ viewTreeKind' $ mkIdsK $ typeDefKind $ forgetTypeDefMetadata $ TypeDef.TypeDefAST def - -- param name node selected - return its kind - Just (TypeDefParamNodeSelection (TypeDefParamSelection p Nothing)) -> - maybe (throw' $ ParamNotFound p) (pure . Kind . viewTreeKind . snd) $ - find ((== p) . fst) (astTypeDefParameters def) - -- param kind node selected - just return `KType` - -- This is a slight lie, effectively reporting that kinds are types, - -- when this isn't true in Primer (as it is in Haskell with modern GHC's `TypeInType`). - -- But Primer also doesn't (explicitly) have an Agda-style infinite hierarchy of types - -- `True : Bool : Type0 : Type1 : Type2 : ...` (we don't go beyond `Type0` i.e. `KType`), - -- so this is the best that we can easily do. - Just (TypeDefParamNodeSelection (TypeDefParamSelection _ (Just _))) -> - pure $ Kind $ viewTreeKind' $ KType "kind" + Just (TypeDefParamNodeSelection (TypeDefParamSelection p s)) -> do + k <- maybe (throw' $ ActionError $ ParamNotFound p) (pure . snd) $ find ((== p) . fst) (astTypeDefParameters def) + case s of + Nothing -> + -- param name node selected - return its kind + pure . Kind . viewTreeKind $ k + Just i -> do + k' <- maybe (throw' $ NodeIDNotFound i) pure $ focusOnKind i k + pure $ viewKindOfKind $ target k' -- constructor node selected - return the type to which it belongs Just (TypeDefConsNodeSelection (TypeDefConsSelection _ Nothing)) -> pure . Type . viewTreeType' . mkIds $ @@ -1371,20 +1370,20 @@ getSelectionTypeOrKind = curry $ logAPI (noError GetTypeOrKind) $ \(sid, sel0) - -- field node selected - return its kind Just (TypeDefConsNodeSelection (TypeDefConsSelection c (Just s))) -> do t0 <- maybe (throw' $ TypeDefConFieldNotFound sel.def c s.index) pure $ getTypeDefConFieldType def c s.index - t <- maybe (throw' $ NodeIDNotFound s.meta) pure $ findType s.meta t0 - pure $ viewTypeKind $ t ^. _typeMetaLens + t <- maybe (throw' $ NodeIDNotFound s.meta) pure $ findTypeOrKind s.meta t0 + pure $ either (viewTypeKind . view _typeMetaLens) viewKindOfKind t where trivialTree = Tree{nodeId = "seltype-0", childTrees = [], rightChild = Nothing, body = NoBody Flavor.EmptyHole} viewExprType :: ExprMeta -> TypeOrKind viewExprType = Type . fromMaybe trivialTree . viewExprType' viewExprType' :: ExprMeta -> Maybe Tree viewExprType' = preview $ _type % _Just % to (viewTreeType' . mkIds . getAPIType) - isHole :: Type' a -> Bool + isHole :: Type' a b -> Bool isHole = \case THole{} -> True TEmptyHole{} -> True _ -> False - getAPIType :: TypeCache -> Type' () + getAPIType :: TypeCache -> Type' () () getAPIType = \case TCSynthed t -> t TCChkedAt t -> t @@ -1396,11 +1395,19 @@ getSelectionTypeOrKind = curry $ logAPI (noError GetTypeOrKind) $ \(sid, sel0) - -- if neither is a hole (in which case the two are consistent), we choose the synthed type | otherwise -> tcSynthed -- We prefix ids to keep them unique from other ids in the emitted program - mkIds :: Type' () -> Type' Text - mkIds = over _typeMeta (("seltype-" <>) . show . getID) . create' . generateTypeIDs + mkIds :: Type' () () -> Type' Text Text + mkIds = over _typeKindMeta (show . view _id) . over _typeMeta (("seltype-" <>) . show . getID) . create' . generateTypeIDs mkIdsK :: Kind' () -> Kind' Text mkIdsK = over _kindMeta (("selkind-" <>) . show . getID) . create' . generateKindIDs viewTypeKind :: TypeMeta -> TypeOrKind viewTypeKind = Kind . fromMaybe trivialTree . viewTypeKind' viewTypeKind' :: TypeMeta -> Maybe Tree viewTypeKind' = preview $ _type % _Just % to (viewTreeKind' . mkIdsK) + -- If a kind node is selected we just return `KType` + -- This is a slight lie, effectively reporting that kinds are types, + -- when this isn't true in Primer (as it is in Haskell with modern GHC's `TypeInType`). + -- But Primer also doesn't (explicitly) have an Agda-style infinite hierarchy of types + -- `True : Bool : Type0 : Type1 : Type2 : ...` (we don't go beyond `Type0` i.e. `KType`), + -- so this is the best that we can easily do. + viewKindOfKind :: Kind' a -> TypeOrKind + viewKindOfKind _ = Kind $ viewTreeKind' $ KType "kind" diff --git a/primer-api/test/Tests/API.hs b/primer-api/test/Tests/API.hs index 6d178081a..923340f68 100644 --- a/primer-api/test/Tests/API.hs +++ b/primer-api/test/Tests/API.hs @@ -158,11 +158,11 @@ unit_viewTreeType_injective_var = unit_viewTreeType_injective_forall_param :: Assertion unit_viewTreeType_injective_forall_param = - distinctTreeType (tforall "a" (KType ()) tEmptyHole) (tforall "b" (KType ()) tEmptyHole) + distinctTreeType (tforall "a" ktype tEmptyHole) (tforall "b" ktype tEmptyHole) unit_viewTreeType_injective_forall_kind :: Assertion unit_viewTreeType_injective_forall_kind = - distinctTreeType (tforall "a" (KType ()) tEmptyHole) (tforall "a" (KHole ()) tEmptyHole) + distinctTreeType (tforall "a" ktype tEmptyHole) (tforall "a" khole tEmptyHole) distinctTreeExpr :: S Expr -> S Expr -> Assertion distinctTreeExpr e1 e2 = diff --git a/primer-api/test/outputs/APITree/Expr b/primer-api/test/outputs/APITree/Expr index ff643cb5a..2af601a7f 100644 --- a/primer-api/test/outputs/APITree/Expr +++ b/primer-api/test/outputs/APITree/Expr @@ -1,5 +1,5 @@ Tree - { nodeId = "9" + { nodeId = "10" , body = TextBody ( RecordPair { fst = Let @@ -11,11 +11,11 @@ Tree ) , childTrees = [ Tree - { nodeId = "10" + { nodeId = "11" , body = NoBody Ann , childTrees = [ Tree - { nodeId = "11" + { nodeId = "12" , body = TextBody ( RecordPair { fst = Con @@ -32,7 +32,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "12" + { nodeId = "13" , body = TextBody ( RecordPair { fst = TCon @@ -52,7 +52,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "13" + { nodeId = "14" , body = TextBody ( RecordPair { fst = Letrec @@ -64,19 +64,19 @@ Tree ) , childTrees = [ Tree - { nodeId = "14" + { nodeId = "15" , body = NoBody App , childTrees = [ Tree - { nodeId = "15" + { nodeId = "16" , body = NoBody Hole , childTrees = [ Tree - { nodeId = "16" + { nodeId = "17" , body = NoBody Ann , childTrees = [ Tree - { nodeId = "17" + { nodeId = "18" , body = TextBody ( RecordPair { fst = Con @@ -91,7 +91,7 @@ Tree ) , childTrees = [ Tree - { nodeId = "18" + { nodeId = "19" , body = NoBody EmptyHole , childTrees = [] , rightChild = Nothing @@ -100,11 +100,11 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "19" + { nodeId = "20" , body = NoBody TApp , childTrees = [ Tree - { nodeId = "20" + { nodeId = "21" , body = TextBody ( RecordPair { fst = TCon @@ -121,7 +121,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "21" + { nodeId = "22" , body = NoBody TEmptyHole , childTrees = [] , rightChild = Nothing @@ -136,11 +136,11 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "22" + { nodeId = "23" , body = NoBody Hole , childTrees = [ Tree - { nodeId = "23" + { nodeId = "24" , body = TextBody ( RecordPair { fst = GlobalVar @@ -163,11 +163,11 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "24" + { nodeId = "25" , body = NoBody THole , childTrees = [ Tree - { nodeId = "25" + { nodeId = "26" , body = TextBody ( RecordPair { fst = TCon @@ -187,11 +187,11 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "26" + { nodeId = "27" , body = NoBody Ann , childTrees = [ Tree - { nodeId = "27" + { nodeId = "28" , body = TextBody ( RecordPair { fst = Lam @@ -203,7 +203,7 @@ Tree ) , childTrees = [ Tree - { nodeId = "28" + { nodeId = "29" , body = TextBody ( RecordPair { fst = LAM @@ -215,15 +215,15 @@ Tree ) , childTrees = [ Tree - { nodeId = "29" + { nodeId = "30" , body = NoBody App , childTrees = [ Tree - { nodeId = "30" + { nodeId = "31" , body = NoBody APP , childTrees = [ Tree - { nodeId = "31" + { nodeId = "32" , body = TextBody ( RecordPair { fst = LetType @@ -235,7 +235,7 @@ Tree ) , childTrees = [ Tree - { nodeId = "33" + { nodeId = "34" , body = TextBody ( RecordPair { fst = Con @@ -252,7 +252,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "32" + { nodeId = "33" , body = TextBody ( RecordPair { fst = TCon @@ -272,7 +272,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "34" + { nodeId = "35" , body = TextBody ( RecordPair { fst = TVar @@ -289,11 +289,11 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "35" + { nodeId = "36" , body = NoBody Case , childTrees = [ Tree - { nodeId = "36" + { nodeId = "37" , body = TextBody ( RecordPair { fst = LocalVar @@ -309,12 +309,12 @@ Tree ] , rightChild = Just ( Tree - { nodeId = "35P0" + { nodeId = "36P0" , body = BoxBody ( RecordPair { fst = Pattern , snd = Tree - { nodeId = "35P0B" + { nodeId = "36P0B" , body = TextBody ( RecordPair { fst = PatternCon @@ -334,7 +334,7 @@ Tree ) , childTrees = [ Tree - { nodeId = "37" + { nodeId = "38" , body = TextBody ( RecordPair { fst = Con @@ -353,12 +353,12 @@ Tree ] , rightChild = Just ( Tree - { nodeId = "35P1" + { nodeId = "36P1" , body = BoxBody ( RecordPair { fst = Pattern , snd = Tree - { nodeId = "35P1B" + { nodeId = "36P1B" , body = TextBody ( RecordPair { fst = PatternCon @@ -373,7 +373,7 @@ Tree ) , childTrees = [ Tree - { nodeId = "38" + { nodeId = "39" , body = TextBody ( RecordPair { fst = PatternBind @@ -393,11 +393,11 @@ Tree ) , childTrees = [ Tree - { nodeId = "39" + { nodeId = "40" , body = NoBody Case , childTrees = [ Tree - { nodeId = "40" + { nodeId = "41" , body = TextBody ( RecordPair { fst = LocalVar @@ -413,12 +413,12 @@ Tree ] , rightChild = Just ( Tree - { nodeId = "39P0" + { nodeId = "40P0" , body = BoxBody ( RecordPair { fst = Pattern , snd = Tree - { nodeId = "39P0B" + { nodeId = "40P0B" , body = TextBody ( RecordPair { fst = PatternCon @@ -438,21 +438,21 @@ Tree ) , childTrees = [ Tree - { nodeId = "41" + { nodeId = "42" , body = NoBody App , childTrees = [ Tree - { nodeId = "42" + { nodeId = "43" , body = NoBody App , childTrees = [ Tree - { nodeId = "43" + { nodeId = "44" , body = NoBody EmptyHole , childTrees = [] , rightChild = Nothing } , Tree - { nodeId = "44" + { nodeId = "45" , body = TextBody ( RecordPair { fst = LocalVar @@ -469,7 +469,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "45" + { nodeId = "46" , body = TextBody ( RecordPair { fst = LocalVar @@ -488,12 +488,12 @@ Tree ] , rightChild = Just ( Tree - { nodeId = "39Pwild" + { nodeId = "40Pwild" , body = BoxBody ( RecordPair { fst = Pattern , snd = Tree - { nodeId = "39PwildB" + { nodeId = "40PwildB" , body = NoBody PatternWildcard , childTrees = [] , rightChild = Nothing @@ -502,7 +502,7 @@ Tree ) , childTrees = [ Tree - { nodeId = "46" + { nodeId = "47" , body = NoBody EmptyHole , childTrees = [] , rightChild = Nothing @@ -531,11 +531,11 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "47" + { nodeId = "48" , body = NoBody TFun , childTrees = [ Tree - { nodeId = "48" + { nodeId = "49" , body = TextBody ( RecordPair { fst = TCon @@ -552,7 +552,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "49" + { nodeId = "50" , body = TextBody ( RecordPair { fst = TForall @@ -564,15 +564,21 @@ Tree ) , childTrees = [ Tree - { nodeId = "50" + { nodeId = "51" + , body = NoBody KType + , childTrees = [] + , rightChild = Nothing + } + , Tree + { nodeId = "52" , body = NoBody TApp , childTrees = [ Tree - { nodeId = "51" + { nodeId = "53" , body = NoBody TApp , childTrees = [ Tree - { nodeId = "52" + { nodeId = "54" , body = TextBody ( RecordPair { fst = TCon @@ -589,7 +595,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "53" + { nodeId = "55" , body = TextBody ( RecordPair { fst = TCon @@ -609,7 +615,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "54" + { nodeId = "56" , body = TextBody ( RecordPair { fst = TVar diff --git a/primer-api/test/outputs/APITree/Type b/primer-api/test/outputs/APITree/Type index c11fa6baa..14c6e78ff 100644 --- a/primer-api/test/outputs/APITree/Type +++ b/primer-api/test/outputs/APITree/Type @@ -33,18 +33,24 @@ Tree , childTrees = [ Tree { nodeId = "3" + , body = NoBody KType + , childTrees = [] + , rightChild = Nothing + } + , Tree + { nodeId = "4" , body = NoBody TApp , childTrees = [ Tree - { nodeId = "4" + { nodeId = "5" , body = NoBody THole , childTrees = [ Tree - { nodeId = "5" + { nodeId = "6" , body = NoBody TApp , childTrees = [ Tree - { nodeId = "6" + { nodeId = "7" , body = TextBody ( RecordPair { fst = TCon @@ -61,7 +67,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "7" + { nodeId = "8" , body = NoBody TEmptyHole , childTrees = [] , rightChild = Nothing @@ -73,7 +79,7 @@ Tree , rightChild = Nothing } , Tree - { nodeId = "8" + { nodeId = "9" , body = TextBody ( RecordPair { fst = TVar diff --git a/primer-service/src/Primer/Client.hs b/primer-service/src/Primer/Client.hs index a0d7eabed..13b2f6e5d 100644 --- a/primer-service/src/Primer/Client.hs +++ b/primer-service/src/Primer/Client.hs @@ -149,13 +149,13 @@ edit sid req = apiClient // API.sessionsAPI // API.sessionAPI /: sid // API.edit variablesInScope :: SessionId -> (GVarName, ID) -> - ClientM (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' ())]), [(GVarName, Type' ())])) + ClientM (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' () ())]), [(GVarName, Type' () ())])) variablesInScope sid ctx = apiClient // API.sessionsAPI // API.sessionAPI /: sid // API.questionAPI // API.variablesInScope /: ctx -- | As 'Primer.API.generateNames'. generateNames :: SessionId -> - ((GVarName, ID), Either (Maybe (Type' ())) (Maybe (Kind' ()))) -> + ((GVarName, ID), Either (Maybe (Type' () ())) (Maybe (Kind' ()))) -> ClientM (Either ProgError [Name]) generateNames sid ctx = apiClient // API.sessionsAPI // API.sessionAPI /: sid // API.questionAPI // API.generateNames /: ctx diff --git a/primer-service/src/Primer/Servant/API.hs b/primer-service/src/Primer/Servant/API.hs index 3104e400e..097312a8c 100644 --- a/primer-service/src/Primer/Servant/API.hs +++ b/primer-service/src/Primer/Servant/API.hs @@ -161,7 +161,7 @@ data QuestionAPI mode = QuestionAPI :- "variables-in-scope" :> Summary "Ask what variables are in scope for the given node ID" :> ReqBody '[JSON] (GVarName, ID) - :> Post '[JSON] (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' ())]), [(GVarName, Type' ())])) + :> Post '[JSON] (Either ProgError (([(TyVarName, Kind' ())], [(LVarName, Type' () ())]), [(GVarName, Type' () ())])) , generateNames :: mode :- "generate-names" @@ -172,7 +172,7 @@ data QuestionAPI mode = QuestionAPI \(since it doesn't modify any state) but we need \ \to provide a request body, which isn't well \ \supported for GET requests." - :> ReqBody '[JSON] ((GVarName, ID), Either (Maybe (Type' ())) (Maybe (Kind' ()))) + :> ReqBody '[JSON] ((GVarName, ID), Either (Maybe (Type' () ())) (Maybe (Kind' ()))) :> Post '[JSON] (Either ProgError [Name]) } deriving stock (Generic) diff --git a/primer/gen/Primer/Gen/Core/Raw.hs b/primer/gen/Primer/Gen/Core/Raw.hs index 4be07d264..3137cc075 100644 --- a/primer/gen/Primer/Gen/Core/Raw.hs +++ b/primer/gen/Primer/Gen/Core/Raw.hs @@ -51,7 +51,6 @@ import Primer.Core ( ValConName, qualifyName, ) -import Primer.Core.Utils (forgetKindMetadata) import Primer.Name (Name, unsafeMkName) type ExprGen a = StateT ID Gen a @@ -178,7 +177,7 @@ genType = [ THole <$> genMeta <*> genType , TFun <$> genMeta <*> genType <*> genType , TApp <$> genMeta <*> genType <*> genType - , TForall <$> genMeta <*> genTyVarName <*> (forgetKindMetadata <$> genKind) <*> genType + , TForall <$> genMeta <*> genTyVarName <*> genKind <*> genType , TLet <$> genMeta <*> genTyVarName <*> genType <*> genType ] diff --git a/primer/gen/Primer/Gen/Core/Typed.hs b/primer/gen/Primer/Gen/Core/Typed.hs index e80a1604d..1f7b7f4f9 100644 --- a/primer/gen/Primer/Gen/Core/Typed.hs +++ b/primer/gen/Primer/Gen/Core/Typed.hs @@ -125,9 +125,9 @@ types/expressions, but it is easy to have a post-processing step of adding IDs and empty TypeCaches to everything. -} -type TypeG = Type' () +type TypeG = Type' () () -type ExprG = Expr' () () +type ExprG = Expr' () () () newtype WT a = WT {unWT :: ReaderT Cxt TestM a} deriving newtype @@ -338,7 +338,7 @@ justT g = Gen.sized $ \s -> Gen.justT $ Gen.resize s g -- @sub ! a = t@ and @apps !! n = Left t@. -- - @sub@ is idempotent, and @apps@ do not refer to these names. I.e. the names -- in @InstUnconstrainedAPP@ do not appear free in @apps@ or the rhs of @sub@. -genInstApp :: [Inst] -> GenT WT (Map TyVarName (Type' ()), [Either TypeG ExprG]) +genInstApp :: [Inst] -> GenT WT (Map TyVarName TypeG, [Either TypeG ExprG]) genInstApp = reify mempty where reify sb = \case @@ -358,7 +358,7 @@ genSyn = genSyns (TEmptyHole ()) -- - the ADT it belongs to (if @c@ maps to @([(p1,k1),(p2,k2)],_,T)@ in the -- returned map, then @c [A,B] _ ∈ T A B@ for any @A@ of kind @k1@ and @B@ -- of kind @k2@) -allCons :: Cxt -> M.Map ValConName ([(TyVarName, Kind' ())], [Type' ()]) +allCons :: Cxt -> M.Map ValConName ([(TyVarName, Kind' ())], [TypeG]) allCons cxt = M.fromList $ concatMap consForTyDef $ typeDefs cxt where consForTyDef = \case diff --git a/primer/primer.cabal b/primer/primer.cabal index 21610db38..06dd2fddd 100644 --- a/primer/primer.cabal +++ b/primer/primer.cabal @@ -87,6 +87,7 @@ library Primer.Typecheck.SmartHoles Primer.Typecheck.TypeError Primer.Typecheck.Utils + Primer.Zipper.Nested Primer.Zipper.Type default-language: GHC2021 diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index 97552645a..57dd47161 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -20,6 +20,7 @@ module Primer.Action ( uniquifyDefName, toProgActionInput, toProgActionNoInput, + applyActionsToParam, applyActionsToField, insertSubseqBy, ) where @@ -32,6 +33,7 @@ import Data.Bifunctor.Swap qualified as Swap import Data.Bitraversable (bisequence) import Data.Functor.Compose (Compose (..)) import Data.Generics.Product (typed) +import Data.Generics.Uniplate.Zipper (fromZipper) import Data.List (delete, findIndex, insertBy) import Data.List.NonEmpty qualified as NE import Data.Map (insert) @@ -39,7 +41,22 @@ import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Text qualified as T import Data.Tuple.Extra ((&&&)) -import Optics (over, set, traverseOf, (%), (?~), (^.), (^?), _Just) +import Optics ( + findOf, + folded, + indices, + isnd, + over, + set, + traverseOf, + traversed, + (%), + (%&), + (?~), + (^.), + (^?), + _Just, + ) import Primer.Action.Actions (Action (..), BranchMove (Fallback, Pattern), Movement (..), QualifiedText) import Primer.Action.Available qualified as Available import Primer.Action.Errors (ActionError (..)) @@ -64,6 +81,8 @@ import Primer.Core ( HasID, HasMetadata (_metadata), ID, + Kind, + Kind' (KHole), KindMeta, LVarName, LocalName (LocalName, unLocalName), @@ -101,6 +120,9 @@ import Primer.Core.DSL ( con, emptyHole, hole, + kfun, + khole, + ktype, lAM, lam, let_, @@ -142,6 +164,7 @@ import Primer.Typecheck ( checkEverything, exprTtoExpr, getTypeDefInfo, + initialCxt, lookupConstructor, lookupVar, maybeTypeOf, @@ -153,6 +176,8 @@ import Primer.Zipper ( CaseBindZ, ExprZ, IsZipper, + KindTZ, + KindZ, Loc, Loc' (..), SomeNode (..), @@ -160,25 +185,28 @@ import Primer.Zipper ( TypeZip, down, findNodeWithParent, - findType, + findTypeOrKind, focus, + focusKind, focusLoc, focusOn, + focusOnlyKind, focusOnlyType, focusType, - locToEither, replace, right, target, top, unfocus, unfocusExpr, + unfocusKindT, unfocusLoc, unfocusType, up, updateCaseBind, _target, ) +import Primer.Zipper.Type (KindZip, focusOnlyKindT) import Primer.ZipperCxt (localVariablesInScopeExpr) -- | Given a definition name and a program, return a unique variant of @@ -218,17 +246,17 @@ applyActionsToTypeSig :: -- | This must be one of the definitions in the @Module@, with its correct name (Name, ASTDef) -> [Action] -> - m (Either ActionError ([Module], TypeZip)) + m (Either ActionError ([Module], Either TypeZip KindTZ)) applyActionsToTypeSig smartHoles imports (mod, mods) (defName, def) actions = runReaderT go (buildTypingContextFromModules (mod : mods <> imports) smartHoles) & runExceptT where - go :: ActionM m => m ([Module], TypeZip) + go :: ActionM m => m ([Module], Either TypeZip KindTZ) go = do zt <- withWrappedType (astDefType def) (\zt -> foldlM (flip applyActionAndSynth) (InType zt) actions) - let t = target (top zt) + let t = target (top $ either identity unfocusKindT zt) e <- check (forgetTypeMetadata t) (astDefExpr def) let def' = def{astDefExpr = exprTtoExpr e, astDefType = t} mod' = insertDef mod defName (DefAST def') @@ -243,7 +271,7 @@ applyActionsToTypeSig smartHoles imports (mod, mods) (defName, def) actions = -- Actions expect that all ASTs have a top-level expression of some sort. -- Signatures don't have this: they're just a type. -- We fake it by wrapping the type in a top-level annotation node, then unwrapping afterwards. - withWrappedType :: ActionM m => Type -> (TypeZ -> m Loc) -> m TypeZip + withWrappedType :: ActionM m => Type -> (TypeZ -> m Loc) -> m (Either TypeZip KindTZ) withWrappedType ty f = do wrappedType <- ann emptyHole (pure ty) let unwrapError = throwError $ InternalFailure "applyActionsToTypeSig: failed to unwrap type" @@ -254,11 +282,46 @@ applyActionsToTypeSig smartHoles imports (mod, mods) (defName, def) actions = Nothing -> wrapError Just wrappedTy -> f wrappedTy >>= \case - InType zt -> pure $ focusOnlyType zt + InType zt -> pure $ Left $ focusOnlyType zt + InKind zk -> pure $ Right (focusOnlyKind zk) -- This probably shouldn't happen, but it may be the case that an action accidentally -- exits the type and ends up in the outer expression that we have created as a wrapper. -- In this case we just refocus on the top of the type. - z -> maybe unwrapError (pure . focusOnlyType) (focusType (unfocusLoc z)) + z -> maybe unwrapError (pure . Left . focusOnlyType) (focusType (unfocusLoc z)) + +applyActionsToParam :: + (MonadFresh ID m, MonadFresh NameCounter m) => + SmartHoles -> + (TyVarName, ASTTypeDef TypeMeta KindMeta) -> + [Action] -> + m (Either ActionError (ASTTypeDef TypeMeta KindMeta, KindZip)) +applyActionsToParam sh (paramName, def) actions = runExceptT $ do + zk <- case findOf (#astTypeDefParameters % folded) ((== paramName) . fst) def of + Nothing -> throwError $ ParamNotFound paramName + Just (_, k) -> + -- no action in kinds should care about the context + flip runReaderT (initialCxt sh) $ + withWrappedKind k $ \zk' -> + foldlM (flip applyActionAndSynth) (InKind zk') actions + let def' = + set + (#astTypeDefParameters % traversed % isnd %& indices (== paramName)) + (fromZipper zk) + def + pure (def', zk) + where + withWrappedKind :: (MonadError ActionError m, MonadFresh ID m) => Kind -> (KindZ -> m Loc) -> m KindZip + withWrappedKind k f = do + wrappedKind <- ann emptyHole (tforall "a" (pure k) tEmptyHole) + let unwrapError = throwError $ InternalFailure "applyActionsToParam: failed to unwrap kind" + wrapError = throwError $ InternalFailure "applyActionsToParam: failed to wrap kind" + focusedKind = focusKind <=< focusType $ focus wrappedKind + case focusedKind of + Nothing -> wrapError + Just wrappedK -> + f wrappedK >>= \case + InKind zk -> pure $ focusOnlyKindT $ focusOnlyKind zk + z -> maybe unwrapError pure (fmap (focusOnlyKindT . focusOnlyKind) . focusKind <=< focusType $ unfocusLoc z) applyActionsToField :: (MonadFresh ID m, MonadFresh NameCounter m) => @@ -325,6 +388,7 @@ refocus Refocus{pre, post} = do TC.SmartHoles -> case pre of InExpr e -> candidateIDsExpr $ target e InType t -> candidateIDsType t + InKind k -> [getID k] InBind (BindCase ze) -> [getID ze] pure . getFirst . mconcat $ fmap (\i -> First $ focusOn i post) candidateIDs where @@ -381,10 +445,9 @@ applyActionAndCheck ty action z = do -- This is currently only used for tests. -- We may need it in the future for a REPL, where we want to build standalone expressions. -- We take a list of the modules that should be in scope for the test. -applyActionsToExpr :: (MonadFresh ID m, MonadFresh NameCounter m) => SmartHoles -> [Module] -> Expr -> [Action] -> m (Either ActionError (Either ExprZ TypeZ)) +applyActionsToExpr :: (MonadFresh ID m, MonadFresh NameCounter m) => SmartHoles -> [Module] -> Expr -> [Action] -> m (Either ActionError Loc) applyActionsToExpr sh modules expr actions = foldlM (flip applyActionAndSynth) (focusLoc expr) actions -- apply all actions - <&> locToEither & flip runReaderT (buildTypingContextFromModules modules sh) & runExceptT -- catch any errors @@ -420,6 +483,7 @@ applyAction' a = case a of Move m -> \case InExpr z -> InExpr <$> moveExpr m z InType z -> InType <$> moveType m z + InKind z -> InKind <$> moveKind m z z@(InBind _) -> case m of -- If we're moving up from a binding, then shift focus to the nearest parent expression. -- This is exactly what 'unfocusLoc' does if the 'Loc' is a binding. @@ -428,10 +492,12 @@ applyAction' a = case a of Delete -> \case InExpr ze -> InExpr . flip replace ze <$> emptyHole InType zt -> InType . flip replace zt <$> tEmptyHole + InKind zk -> InKind . flip replace zk <$> khole InBind _ -> throwError $ CustomFailure Delete "Cannot delete a binding" SetMetadata d -> \case InExpr ze -> pure $ InExpr $ setMetadata d ze InType zt -> pure $ InType $ setMetadata d zt + InKind zk -> pure $ InKind $ setMetadata d zk InBind (BindCase zb) -> pure $ InBind $ BindCase $ setMetadata d zb EnterHole -> termAction enterHole "non-empty type holes not supported" FinishHole -> termAction finishHole "there are no non-empty holes in types" @@ -473,8 +539,8 @@ applyAction' a = case a of RenameCaseBinding x -> \case InBind (BindCase z) -> InBind . BindCase <$> renameCaseBinding x z _ -> throwError $ CustomFailure a "cannot rename this node - not a case binding" - ConstructKType -> const $ throwError $ CustomFailure ConstructKType "kind edits currently only allowed in typedefs" - ConstructKFun -> const $ throwError $ CustomFailure ConstructKFun "kind edits currently only allowed in typedefs" + ConstructKType -> kindAction constructKType "cannot construct the kind 'Type' - not in kind" + ConstructKFun -> kindAction constructKFun "cannot construct the arrow kind - not in kind" where termAction f s = \case InExpr ze -> InExpr <$> f ze @@ -482,6 +548,9 @@ applyAction' a = case a of typeAction f s = \case InType zt -> InType <$> f zt _ -> throwError $ CustomFailure a s + kindAction f s = \case + InKind zt -> InKind <$> f zt + _ -> throwError $ CustomFailure a s setCursor :: MonadError ActionError m => ID -> ExprZ -> m Loc setCursor i e = case focusOn i (unfocusExpr e) of @@ -519,12 +588,18 @@ moveExpr Child2 z throwError $ CustomFailure (Move Child2) "cannot move to 'Child2' of a case: use Branch instead" moveExpr m z = move m z --- | Apply a movement to a zipper +-- | Apply a movement to a type zipper moveType :: MonadError ActionError m => Movement -> TypeZ -> m TypeZ moveType m@(Branch _) _ = throwError $ CustomFailure (Move m) "Move-to-branch unsupported in types (there are no cases in types!)" moveType m@(ConChild _) _ = throwError $ CustomFailure (Move m) "Move-to-constructor-argument unsupported in types (type constructors do not directly store their arguments)" moveType m z = move m z +-- | Apply a movement to a kind zipper +moveKind :: MonadError ActionError m => Movement -> KindZ -> m KindZ +moveKind m@(Branch _) _ = throwError $ CustomFailure (Move m) "Move-to-branch unsupported in kinds (there are no cases in kinds!)" +moveKind m@(ConChild _) _ = throwError $ CustomFailure (Move m) "Move-to-constructor-argument unsupported in kinds (there are no constructors in kinds)" +moveKind m z = move m z + -- | Apply a movement to a generic zipper - does not support movement to a case -- branch, or into an argument of a constructor move :: forall m za a. (MonadError ActionError m, IsZipper za a, HasID za) => Movement -> za -> m za @@ -794,6 +869,7 @@ getFocusType ze = case maybeTypeOf $ target ze of in synthZ (InExpr ze) `catchError` handler >>= \case Nothing -> throwError $ CustomFailure ConstructCase "internal error when synthesising the type of the scruntinee: focused expression went missing after typechecking" Just (InType _) -> throwError $ CustomFailure ConstructCase "internal error when synthesising the type of the scruntinee: focused expression changed into a type after typechecking" + Just (InKind _) -> throwError $ CustomFailure ConstructCase "internal error when synthesising the type of the scruntinee: focused expression changed into a kind after typechecking" Just (InBind _) -> throwError $ CustomFailure ConstructCase "internal error: scrutinee became a binding after synthesis" Just (InExpr ze') -> case maybeTypeOf $ target ze' of Nothing -> throwError $ CustomFailure ConstructCase "internal error: synthZ always returns 'Just', never 'Nothing'" @@ -1036,7 +1112,7 @@ constructTForall mx zt = do Nothing -> LocalName <$> mkFreshNameTy zt Just x -> pure (unsafeMkLocalName x) unless (isFreshTy x $ target zt) $ throwError NameCapture - flip replace zt <$> tforall x (C.KType ()) (pure (target zt)) + flip replace zt <$> tforall x ktype (pure (target zt)) constructTApp :: MonadFresh ID m => TypeZ -> m TypeZ constructTApp zt = flip replace zt <$> tapp (pure (target zt)) tEmptyHole @@ -1055,6 +1131,14 @@ renameForall b zt = case target zt of _ -> throwError $ CustomFailure (RenameForall b) "the focused expression is not a forall type" +constructKType :: (MonadFresh ID m, MonadError ActionError m) => KindZ -> m KindZ +constructKType zk = case target zk of + KHole _ -> flip replace zk <$> ktype + _ -> throwError $ CustomFailure ConstructKType "can only construct the kind 'Type' in hole" + +constructKFun :: MonadFresh ID m => KindZ -> m KindZ +constructKFun zk = flip replace zk <$> ktype `kfun` pure (target zk) + -- | Convert a high-level 'Available.NoInputAction' to a concrete sequence of 'ProgAction's. toProgActionNoInput :: DefMap -> @@ -1100,13 +1184,15 @@ toProgActionNoInput defs def0 sel0 = \case let id = field.meta vc <- maybeToEither (ValConNotFound tName vcName) $ find ((== vcName) . valConName) $ astTypeDefConstructors def t <- maybeToEither (FieldIndexOutOfBounds vcName field.index) $ flip atMay field.index $ valConArgs vc - case findType id t of - Just t' -> pure $ forgetTypeMetadata t' + case findTypeOrKind id t of + Just (Left t') -> pure $ forgetTypeMetadata t' + Just (Right k) -> Left $ NeedType $ KindNode k Nothing -> Left $ IDNotFound id Right def -> do id <- nodeID - forgetTypeMetadata <$> case findType id $ astDefType def of - Just t -> pure t + forgetTypeMetadata <$> case findTypeOrKind id $ astDefType def of + Just (Left t) -> pure t + Just (Right k) -> Left $ NeedType $ KindNode k Nothing -> case map fst $ findNodeWithParent id $ astDefExpr def of Just (TypeNode t) -> pure t Just sm -> Left $ NeedType sm @@ -1200,7 +1286,7 @@ toProgActionNoInput defs def0 sel0 = \case SelectionTypeDef sel -> case sel.node of Just (TypeDefParamNodeSelection _) -> do (t, p, id) <- typeParamKindSel - pure [ParamKindAction t p id actions] + pure [ParamKindAction t p $ SetCursor id : actions] Just (TypeDefConsNodeSelection _) -> do (t, c, f) <- conFieldSel pure [ConFieldAction t c f.index $ SetCursor f.meta : actions] diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index 7d4ad1e17..f59e39371 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -70,6 +70,7 @@ import Primer.Core ( GlobalName (baseName, qualifiedModule), HasID (_id), ID, + Kind, Kind' (..), KindMeta, ModuleName (unModuleName), @@ -126,11 +127,10 @@ import Primer.Typecheck ( import Primer.Zipper ( SomeNode (..), findNodeWithParent, - findType, + findTypeOrKind, focusOn, focusOnKind, focusOnTy, - locToEither, target, ) @@ -241,6 +241,7 @@ forBody tydefs l Editable expr id = sortByPriority l $ case findNodeWithParent i Just (ExprNode _) -> [] -- at the root of an annotation, so cannot raise _ -> [NoInput Raise] in forType l t <> raiseAction + Just (KindNode k, _) -> forKind l k Just (CaseBindNode _, _) -> [Input RenamePattern] @@ -251,11 +252,12 @@ forSig :: ID -> [Action] forSig _ NonEditable _ _ = mempty -forSig l Editable ty id = sortByPriority l $ case findType id ty of +forSig l Editable ty id = sortByPriority l $ case findTypeOrKind id ty of Nothing -> mempty - Just t -> + Just (Left t) -> forType l t <> mwhen (id /= getID ty) [NoInput RaiseType] + Just (Right k) -> forKind l k forExpr :: TypeDefMap -> Level -> Expr -> [Action] forExpr tydefs l expr = @@ -356,6 +358,12 @@ forType l type_ = ] delete = [NoInput DeleteType] +forKind :: Level -> Kind -> [Action] +forKind _ k = + [NoInput MakeKFun] <> case k of + KHole _ -> [NoInput MakeKType] + _ -> [NoInput DeleteKind] + forTypeDef :: Level -> Editable -> @@ -419,10 +427,9 @@ forTypeDefParamKindNode paramName id l Editable tydefs defs tdName td = sortByPriority l $ mwhen (not $ typeInUse tdName td tydefs defs) - $ [NoInput MakeKFun] <> case findKind id . snd =<< find ((== paramName) . fst) (astTypeDefParameters td) of + $ case findKind id . snd =<< find ((== paramName) . fst) (astTypeDefParameters td) of Nothing -> [] - Just (KHole _) -> [NoInput MakeKType] - Just _ -> [NoInput DeleteKind] + Just k -> forKind l k where findKind i k = target <$> focusOnKind i k @@ -456,8 +463,11 @@ forTypeDefConsFieldNode :: forTypeDefConsFieldNode _ _ _ _ NonEditable _ _ _ _ = mempty forTypeDefConsFieldNode con index id l Editable tydefs defs tdName td = sortByPriority l $ - maybe mempty (forType l) (findType id =<< fieldType) - <> mwhen ((view _id <$> fieldType) == Just id && not (typeInUse tdName td tydefs defs)) [NoInput DeleteConField] + mwhen ((view _id <$> fieldType) == Just id && not (typeInUse tdName td tydefs defs)) [NoInput DeleteConField] + <> case findTypeOrKind id =<< fieldType of + Nothing -> mempty + Just (Left t) -> forType l t + Just (Right k) -> forKind l k where fieldType = getTypeDefConFieldType td con index @@ -579,7 +589,7 @@ options typeDefs defs cxt level def0 sel0 = \case freeVar <$> genNames (Right Nothing) RenameForall -> do TypeNode (TForall _ _ k _) <- findNode - freeVar <$> genNames (Right $ Just k) + freeVar <$> genNames (Right $ Just $ forgetKindMetadata k) RenameDef -> pure $ freeVar [] RenameType -> @@ -645,10 +655,12 @@ options typeDefs defs cxt level def0 sel0 = \case def <- eitherToMaybe def0 case nodeSel.nodeType of BodyNode -> fst <$> findNodeWithParent nodeSel.meta (astDefExpr def) - SigNode -> TypeNode <$> findType nodeSel.meta (astDefType def) + SigNode -> either TypeNode KindNode <$> findTypeOrKind nodeSel.meta (astDefType def) SelectionTypeDef sel -> do - (_, zT) <- conField sel - pure $ TypeNode $ target zT + (_, z) <- conField sel + pure $ case z of + Left zT -> TypeNode $ target zT + Right zK -> KindNode (target zK) genNames typeOrKind = map localOpt . flip runReader cxt <$> case sel0 of SelectionDef sel -> do @@ -671,7 +683,7 @@ options typeDefs defs cxt level def0 sel0 = \case focusNode nodeSel = do def <- eitherToMaybe def0 case nodeSel.nodeType of - BodyNode -> Left . locToEither <$> focusOn nodeSel.meta (astDefExpr def) + BodyNode -> Left <$> focusOn nodeSel.meta (astDefExpr def) SigNode -> fmap Right $ focusOnTy nodeSel.meta $ astDefType def conField sel = do (con, field) <- case sel of diff --git a/primer/src/Primer/Action/Errors.hs b/primer/src/Primer/Action/Errors.hs index 51e7c94bd..5896e3795 100644 --- a/primer/src/Primer/Action/Errors.hs +++ b/primer/src/Primer/Action/Errors.hs @@ -13,7 +13,7 @@ import Data.Aeson (FromJSON (..), ToJSON (..)) import Primer.Action.Actions (Action) import Primer.Action.Available qualified as Available import Primer.Action.Movement (Movement) -import Primer.Core (Expr, GVarName, ID, LVarName, ModuleName, Pattern, TyConName, Type', ValConName) +import Primer.Core (Expr, GVarName, ID, LVarName, ModuleName, Pattern, TyConName, TyVarName, Type', ValConName) import Primer.JSON (CustomJSON (..), PrimerJSON) import Primer.Typecheck.TypeError (TypeError) import Primer.Zipper (SomeNode) @@ -45,7 +45,7 @@ data ActionError | CaseBranchAlreadyExists Pattern | CaseBranchNotExist Pattern | -- | Attempted to add a branch for an unexpected ctor - CaseBranchNotCon Pattern (Type' ()) + CaseBranchNotCon Pattern (Type' () ()) | -- TODO: semantic errors. -- https://github.com/hackworthltd/primer/issues/8 SaturatedApplicationError (Either Text TypeError) @@ -62,7 +62,7 @@ data ActionError -- The extra unit is to avoid having two constructors with a single -- TypeError field, breaking our MonadNestedError machinery... ImportFailed () TypeError - | NeedTFun (Type' ()) + | NeedTFun (Type' () ()) | NeedType SomeNode | NeedGlobal Available.Option | NeedLocal Available.Option @@ -79,6 +79,7 @@ data ActionError | NeedTypeDefParamKindSelection | NoNodeSelection | ValConNotFound TyConName ValConName + | ParamNotFound TyVarName | FieldIndexOutOfBounds ValConName Int deriving stock (Eq, Show, Read, Generic) deriving (FromJSON, ToJSON) via PrimerJSON ActionError diff --git a/primer/src/Primer/Action/ProgAction.hs b/primer/src/Primer/Action/ProgAction.hs index da611f1f6..af953c65c 100644 --- a/primer/src/Primer/Action/ProgAction.hs +++ b/primer/src/Primer/Action/ProgAction.hs @@ -44,7 +44,7 @@ data ProgAction | -- | Delete the value constructor with the given name, from the given type DeleteCon TyConName ValConName | -- | Add a new field, at the given index, to the given constructor - AddConField TyConName ValConName Int (Type' ()) + AddConField TyConName ValConName Int (Type' () ()) | -- | Delete the field at the given index of the given value constructor, in the given type DeleteConField TyConName ValConName Int | -- | Add a parameter at the given position, with the given name and kind, in the given type @@ -58,7 +58,7 @@ data ProgAction | -- | Execute a sequence of actions on the type of a field of a constructor in a typedef ConFieldAction TyConName ValConName Int [Action] | -- | Execute a sequence of actions on the kind of a parameter in a typedef - ParamKindAction TyConName TyVarName ID [Action] + ParamKindAction TyConName TyVarName [Action] | SetSmartHoles SmartHoles | -- | CopyPaste (d,i) as -- remembers the tree in def d, node i diff --git a/primer/src/Primer/Action/ProgError.hs b/primer/src/Primer/Action/ProgError.hs index cac4503a7..00025d4e3 100644 --- a/primer/src/Primer/Action/ProgError.hs +++ b/primer/src/Primer/Action/ProgError.hs @@ -33,7 +33,6 @@ data ProgError | -- | We expected to see more arguments to a constructor than actually existed -- (this should never happen in a well-typed program) ConNotSaturated ValConName - | ParamNotFound TyVarName | NodeIDNotFound ID | TypeDefConFieldNotFound TyConName ValConName Int | ValConParamClash Name diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 8715376bf..61cc55a74 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -72,6 +72,7 @@ import Control.Monad.Fresh (MonadFresh (..)) import Control.Monad.Log (MonadLog, WithSeverity) import Control.Monad.NestedError (MonadNestedError, throwError') import Control.Monad.Trans (MonadTrans) +import Data.Bitraversable (bitraverse) import Data.Data (Data) import Data.Generics.Uniplate.Operations (transform, transformM) import Data.Generics.Uniplate.Zipper ( @@ -106,6 +107,7 @@ import Optics ( (^.), (^?), _Just, + _Left, ) import Optics.State.Operators ((<<%=)) import Primer.Action ( @@ -115,6 +117,7 @@ import Primer.Action ( applyAction', applyActionsToBody, applyActionsToField, + applyActionsToParam, applyActionsToTypeSig, insertSubseqBy, ) @@ -144,6 +147,7 @@ import Primer.Core ( GVarName, GlobalName (baseName, qualifiedModule), ID (..), + Kind, Kind' (..), KindMeta, LocalName (LocalName, unLocalName), @@ -174,10 +178,20 @@ import Primer.Core ( _type, _typeMetaLens, ) -import Primer.Core.DSL (S, create, emptyHole, kfun, khole, ktype, tEmptyHole) +import Primer.Core.DSL (S, create, emptyHole, tEmptyHole) import Primer.Core.DSL qualified as DSL import Primer.Core.Transform (renameTyVar, renameVar, unfoldTApp) -import Primer.Core.Utils (freeVars, generateKindIDs, generateTypeIDs, regenerateExprIDs, regenerateTypeIDs, _freeTmVars, _freeTyVars, _freeVarsTy) +import Primer.Core.Utils ( + freeVars, + generateKindIDs, + generateTypeIDs, + regenerateExprIDs, + regenerateKindIDs, + regenerateTypeIDs, + _freeTmVars, + _freeTyVars, + _freeVarsTy, + ) import Primer.Def ( ASTDef (..), Def (..), @@ -233,10 +247,15 @@ import Primer.Typecheck ( ) import Primer.Typecheck qualified as TC import Primer.Zipper ( + BindLoc' (BindCase), ExprZ, - Loc' (InBind, InExpr, InType), + KindTZ, + KindZ, + Loc, + Loc' (InBind, InExpr, InKind, InType), TypeZ, TypeZip, + caseBindZMeta, current, focusLoc, focusOn, @@ -247,10 +266,11 @@ import Primer.Zipper ( getBoundHere, getBoundHereUp, getBoundHereUpTy, - locToEither, replace, target, unfocusExpr, + unfocusKind, + unfocusKindT, unfocusType, _target, ) @@ -527,19 +547,19 @@ handleQuestion = \case focusNode prog defname nodeid -- This only looks in the editable modules, not in any imports -focusNode :: MonadError ProgError m => Prog -> GVarName -> ID -> m (Either (Either ExprZ TypeZ) TypeZip) +focusNode :: MonadError ProgError m => Prog -> GVarName -> ID -> m (Either Loc (Either TypeZip KindTZ)) focusNode prog = focusNodeDefs $ foldMap' moduleDefsQualified $ progModules prog -- This looks in the editable modules and also in any imports -focusNodeImports :: MonadError ProgError m => Prog -> GVarName -> ID -> m (Either (Either ExprZ TypeZ) TypeZip) +focusNodeImports :: MonadError ProgError m => Prog -> GVarName -> ID -> m (Either Loc (Either TypeZip KindTZ)) focusNodeImports prog = focusNodeDefs $ allDefs prog -focusNodeDefs :: MonadError ProgError m => DefMap -> GVarName -> ID -> m (Either (Either ExprZ TypeZ) TypeZip) +focusNodeDefs :: MonadError ProgError m => DefMap -> GVarName -> ID -> m (Either Loc (Either TypeZip KindTZ)) focusNodeDefs defs defname nodeid = case lookupASTDef defname defs of Nothing -> throwError $ DefNotFound defname Just def -> - let mzE = locToEither <$> focusOn nodeid (astDefExpr def) + let mzE = focusOn nodeid (astDefExpr def) mzT = focusOnTy nodeid $ astDefType def in case fmap Left mzE <|> fmap Right mzT of Nothing -> throwError $ ActionError (IDNotFound nodeid) @@ -713,7 +733,7 @@ applyProgAction prog = \case TCEmb (TCBoth t1 t2) -> TCEmb (TCBoth (updateType t1) (updateType t2)) ) updateName n = if n == old then new else n - updateType :: Data a => Type' a -> Type' a + updateType :: (Data a, Data b) => Type' a b -> Type' a b updateType = transform $ over (#_TCon % _2) updateName RenameCon type_ old (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> new) -> editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do @@ -760,7 +780,7 @@ applyProgAction prog = \case def & traverseOf #astTypeDefParameters - ( maybe (throwError $ ParamNotFound old) pure + ( maybe (throwError $ ActionError $ ParamNotFound old) pure . findAndAdjust ((== old) . fst) (_1 .~ new) ) updateConstructors = @@ -928,7 +948,7 @@ applyProgAction prog = \case ( \ps -> do unless (paramName `elem` map fst ps) - (throwError $ ParamNotFound paramName) + (throwError $ ActionError $ ParamNotFound paramName) pure $ filter ((/= paramName) . fst) ps ) td @@ -943,7 +963,11 @@ applyProgAction prog = \case case res of Left err -> throwError $ ActionError err Right (def', z) -> do - let meta = bimap (view _exprMetaLens . target) (Left . view _typeMetaLens . target) $ locToEither z + let meta = case z of + InExpr ze -> Left $ ze ^. _target % _exprMetaLens + InType zt -> Right $ Left $ zt ^. _target % _typeMetaLens + InKind zk -> Right $ Right $ zk ^. _target % _kindMetaLens + InBind (BindCase zb) -> Left $ zb ^. caseBindZMeta pure ( insertDef m defName (DefAST def') , Just . SelectionDef $ @@ -960,8 +984,8 @@ applyProgAction prog = \case case res of Left err -> throwError $ ActionError err Right (mod', zt) -> do - let node = target zt - meta = view _typeMetaLens node + let node = bimap target target zt + meta = bimap (view _typeMetaLens) (view _kindMetaLens) node in pure ( mod' , Just . SelectionDef $ @@ -969,7 +993,7 @@ applyProgAction prog = \case Just NodeSelection { nodeType = SigNode - , meta = Right $ Left meta + , meta = Right meta } ) ConFieldAction tyName con index actions -> editModuleOfCrossType (Just tyName) prog $ \ms defName def -> do @@ -997,43 +1021,30 @@ applyProgAction prog = \case } } ) - ParamKindAction tyName paramName id actions -> editModuleOfCrossType (Just tyName) prog $ \(mod, mods) defName def -> do - def' <- - def - & traverseOf - #astTypeDefParameters - ( maybe (throwError $ ParamNotFound paramName) pure - <=< findAndAdjustA - ((== paramName) . fst) - ( traverseOf _2 $ - flip - ( foldlM $ flip \case - ConstructKType -> modifyKind $ replaceHole ConstructKType ktype - ConstructKFun -> modifyKind \k -> ktype `kfun` pure k - Delete -> modifyKind $ const khole - a -> const $ throwError $ ActionError $ CustomFailure a "unexpected non-kind action" - ) - actions - ) + ParamKindAction tyName paramName actions -> editModuleOfCrossType (Just tyName) prog $ \(mod, mods) defName def -> do + let smartHoles = progSmartHoles prog + res <- applyActionsToParam smartHoles (paramName, def) actions + case res of + Left err -> throwError $ ActionError err + Right (def', kz) -> do + let mod' = mod & over #moduleTypes (Map.insert defName $ TypeDefAST def') + imports = progImports prog + mods' <- + runExceptT + ( runReaderT + (checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mod' : mods})) + (buildTypingContextFromModules (mod : mods <> imports) smartHoles) + ) + >>= either (throwError . ActionError) pure + pure + ( mods' + , Just $ + SelectionTypeDef $ + TypeDefSelection tyName $ + Just $ + TypeDefParamNodeSelection $ + TypeDefParamSelection{param = paramName, kindMeta = Just $ Right $ Right $ kz ^. _target % _kindMetaLens} ) - let mod' = mod & over #moduleTypes (Map.insert defName $ TypeDefAST def') - imports = progImports prog - smartHoles = progSmartHoles prog - mods' <- - runExceptT - ( runReaderT - (checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mod' : mods})) - (buildTypingContextFromModules (mod : mods <> imports) smartHoles) - ) - >>= either (throwError . ActionError) pure - pure (mods', Nothing) - where - modifyKind f k = fromMaybe (throwError' $ IDNotFound id) $ do - k' <- focusOnKind id k - pure $ fromZipper . flip replace k' <$> f (target k') - replaceHole a r = \case - KHole{} -> r - _ -> throwError' $ CustomFailure a "can only construct this kind in a hole" SetSmartHoles smartHoles -> pure $ prog & #progSmartHoles .~ smartHoles CopyPasteSig fromIds setup -> case mdefName of @@ -1503,9 +1514,12 @@ copyPasteSig :: MonadEdit m ProgError => Prog -> (GVarName, ID) -> GVarName -> [ copyPasteSig p (fromDefName, fromTyId) toDefName setup = do c' <- focusNodeImports p fromDefName fromTyId c <- case c' of - Left (Left _) -> throwError $ CopyPasteError "tried to copy-paste an expression into a signature" - Left (Right zt) -> pure $ Left zt - Right zt -> pure $ Right zt + Left (InExpr _) -> throwError $ CopyPasteError "tried to copy-paste an expression into a signature" + Left (InType zt) -> pure $ Left $ Left zt + Left (InKind zk) -> pure $ Right $ Left zk + Left (InBind _) -> throwError $ CopyPasteError "tried to paste a binder into a signature" + Right (Left zt) -> pure $ Left $ Right zt + Right (Right zk) -> pure $ Right $ Right zk let smartHoles = progSmartHoles p finalProg <- editModuleOf (Just toDefName) p $ \mod toDefBaseName oldDef -> do let otherModules = filter ((/= moduleName mod) . moduleName) (progModules p) @@ -1521,21 +1535,36 @@ copyPasteSig p (fromDefName, fromTyId) toDefName setup = do Right (_, tgt) -> pure tgt let sharedScope = if fromDefName == toDefName - then getSharedScopeTy c $ Right tgt + then -- We rely here on the fact that there are no binders in kinds + + getSharedScopeTy (either identity (bimap unfocusKind unfocusKindT) c) $ + Right $ + either identity unfocusKindT tgt else mempty - -- Delete unbound vars - let cTgt = either target target c + -- Delete unbound vars (nb: no vars in kinds) + let cTgt = bimap (either target target) (either target target) c f (m, n) = if Set.member (unLocalName n) sharedScope then pure $ TVar m n else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing) - cScoped <- traverseOf _freeVarsTy f cTgt - freshCopy <- regenerateTypeIDs cScoped - pasted <- case target tgt of - TEmptyHole _ -> pure $ replace freshCopy tgt + cScoped <- traverseOf (_Left % _freeVarsTy) f cTgt + freshCopy <- bitraverse regenerateTypeIDs regenerateKindIDs cScoped + pasted <- case (tgt, freshCopy) of + (Left _, Right _) -> throwError $ CopyPasteError "tried to paste a kind into a type" + (Right _, Left _) -> throwError $ CopyPasteError "tried to paste a type into a kind" + (Left tgt'@(target -> TEmptyHole _), Left fc) -> pure $ Left $ replace fc tgt' + (Right tgt'@(target -> KHole _), Right fc) -> pure $ Right $ replace fc tgt' _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" - let newDef = oldDef{astDefType = fromZipper pasted} - let newSel = NodeSelection SigNode (Right $ Left $ pasted ^. _target % _typeMetaLens) + let newDef = oldDef{astDefType = either fromZipper (fromZipper . unfocusKindT) pasted} + let newSel = + NodeSelection + SigNode + ( Right $ + bimap + (view $ _target % _typeMetaLens) + (view $ _target % _kindMetaLens) + pasted + ) pure (insertDef mod toDefBaseName (DefAST newDef), Just (SelectionDef $ DefSelection toDefName $ Just newSel)) liftError ActionError $ tcWholeProg finalProg @@ -1611,8 +1640,13 @@ tcWholeProg p = do Just sel@NodeSelection{nodeType} -> do n <- runExceptT $ focusNode p' defName_ $ getID sel case (nodeType, n) of - (BodyNode, Right (Left x)) -> pure $ Just $ NodeSelection BodyNode $ bimap (view _exprMetaLens . target) (Left . view _typeMetaLens . target) x - (SigNode, Right (Right x)) -> pure $ Just $ NodeSelection SigNode $ Right $ Left $ x ^. _target % _typeMetaLens + (BodyNode, Right (Left x)) -> pure $ Just $ NodeSelection BodyNode $ case x of + InExpr ze -> Left $ view _exprMetaLens $ target ze + InType zt -> Right $ Left $ view _typeMetaLens $ target zt + InKind zk -> Right $ Right $ view _kindMetaLens $ target zk + InBind (BindCase zb) -> Left $ view caseBindZMeta zb + (SigNode, Right (Right (Left x))) -> pure $ Just $ NodeSelection SigNode $ Right $ Left $ x ^. _target % _typeMetaLens + (SigNode, Right (Right (Right zk))) -> pure $ Just $ NodeSelection SigNode $ Right $ Right $ zk ^. _target % _kindMetaLens _ -> pure Nothing -- something's gone wrong: expected a SigNode, but found it in the body, or vv, or just not found it pure $ Just . SelectionDef $ @@ -1647,12 +1681,12 @@ tcWholeProg p = do conSel & over #field \case Nothing -> Nothing Just fieldSel -> - flip (set #meta) fieldSel . (Right . Left . (^. _typeMetaLens)) <$> do + flip (set #meta) fieldSel . Right <$> do ty <- getTypeDefConFieldType tda conSel.con fieldSel.index id <- case fieldSel.meta of Left _ -> Nothing -- Any selection in a typedef should have TypeMeta or KindMeta, not ExprMeta Right m -> pure $ getID m - target <$> focusOnTy id ty + bimap (view $ _target % _typeMetaLens) (view $ _target % _kindMetaLens) <$> focusOnTy id ty pure $ Just $ SelectionTypeDef $ @@ -1674,14 +1708,40 @@ tcWholeProgWithImports p = do imports <- checkEverything (progSmartHoles p) CheckEverything{trusted = mempty, toCheck = progImports p} tcWholeProg $ p & #progImports .~ imports +data CPB + = ExprInBody ExprZ + | Type CPBT + | Kind CPBK +data CPBT + = TypeInBody TypeZ + | TypeInSig TypeZip +data CPBK + = KindInBody KindZ + | KindInSig KindTZ +cpbtToEither :: CPBT -> Either TypeZ TypeZip +cpbtToEither = \case + TypeInBody t -> Left t + TypeInSig t -> Right t +cpbtTarget :: CPBT -> Type +cpbtTarget = \case + TypeInBody t -> target t + TypeInSig t -> target t +cpbkTarget :: CPBK -> Kind +cpbkTarget = \case + KindInBody k -> target k + KindInSig k -> target k + copyPasteBody :: MonadEdit m ProgError => Prog -> (GVarName, ID) -> GVarName -> [Action] -> m Prog copyPasteBody p (fromDefName, fromId) toDefName setup = do src' <- focusNodeImports p fromDefName fromId - -- reassociate so get Expr+(Type+Type), rather than (Expr+Type)+Type - let src = case src' of - Left (Left e) -> Left e - Left (Right t) -> Right (Left t) - Right t -> Right (Right t) + -- unpack and reassociate + src <- case src' of + Left (InExpr e) -> pure $ ExprInBody e + Left (InType t) -> pure $ Type (TypeInBody t) + Left (InKind k) -> pure $ Kind (KindInBody k) + Left (InBind _) -> throwError $ CopyPasteError "tried to paste a binder into an expression" + Right (Left t) -> pure $ Type (TypeInSig t) + Right (Right k) -> pure $ Kind (KindInSig k) finalProg <- editModuleOf (Just toDefName) p $ \mod toDefBaseName oldDef -> do -- We manually use the low-level applyAction', as we do not want to -- typecheck intermediate states. There are two reasons for this, both @@ -1710,16 +1770,29 @@ copyPasteBody p (fromDefName, fromId) toDefName setup = do -- SH not important here, cxt only used to lookup global vars and ctors & flip runReaderT (buildTypingContextFromModules (progAllModules p) NoSmartHoles) case (src, tgt) of - (_, InBind _) -> throwError $ CopyPasteError "tried to paste an expression into a binder" - (Left _, InType _) -> throwError $ CopyPasteError "tried to paste an expression into a type" - (Right _, InExpr _) -> throwError $ CopyPasteError "tried to paste a type into an expression" - (Right srcT, InType tgtT) -> do + (_, InBind _) -> throwError $ CopyPasteError "tried to paste into a binder" + (ExprInBody _, InType _) -> throwError $ CopyPasteError "tried to paste an expression into a type" + (ExprInBody _, InKind _) -> throwError $ CopyPasteError "tried to paste an expression into a kind" + (Type _, InExpr _) -> throwError $ CopyPasteError "tried to paste a type into an expression" + (Type _, InKind _) -> throwError $ CopyPasteError "tried to paste a type into an kind" + (Kind _, InExpr _) -> throwError $ CopyPasteError "tried to paste a kind into an expression" + (Kind _, InType _) -> throwError $ CopyPasteError "tried to paste a kind into an type" + (Kind srcK, InKind tgtK) -> case target tgtK of + KHole _ -> do + -- Since there are no binders or variables in kinds, we can simply duplicate into the target + freshCopy <- regenerateKindIDs $ cpbkTarget srcK + let pasted = replace freshCopy tgtK + let newDef = oldDef{astDefExpr = unfocusExpr $ unfocusType $ unfocusKind pasted} + let newSel = NodeSelection BodyNode $ Right $ Right $ pasted ^. _target % _kindMetaLens + pure (insertDef mod toDefBaseName (DefAST newDef), Just (SelectionDef $ DefSelection toDefName $ Just newSel)) + _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" + (Type srcT, InType tgtT) -> do let sharedScope = if fromDefName == toDefName - then getSharedScopeTy srcT $ Left tgtT + then getSharedScopeTy (cpbtToEither srcT) $ Left tgtT else mempty -- Delete unbound vars. TODO: we may want to let-bind them? - let srcSubtree = either target target srcT + let srcSubtree = cpbtTarget srcT f (m, n) = if Set.member (unLocalName n) sharedScope then pure $ TVar m n @@ -1732,7 +1805,7 @@ copyPasteBody p (fromDefName, fromId) toDefName setup = do let newDef = oldDef{astDefExpr = unfocusExpr $ unfocusType pasted} let newSel = NodeSelection BodyNode $ Right $ Left $ pasted ^. _target % _typeMetaLens pure (insertDef mod toDefBaseName (DefAST newDef), Just (SelectionDef $ DefSelection toDefName $ Just newSel)) - (Left srcE, InExpr tgtE) -> do + (ExprInBody srcE, InExpr tgtE) -> do let sharedScope = if fromDefName == toDefName then getSharedScope srcE tgtE @@ -1822,7 +1895,7 @@ alterTypeDef f type_ m = do transformCaseBranches :: MonadEdit m ProgError => TyConName -> - (Maybe (Type' ()) -> ([CaseBranch], CaseFallback) -> m ([CaseBranch], CaseFallback)) -> + (Maybe (Type' () ()) -> ([CaseBranch], CaseFallback) -> m ([CaseBranch], CaseFallback)) -> Expr -> m Expr transformCaseBranches type_ f = transformM $ \case @@ -1843,7 +1916,7 @@ transformCaseBranches type_ f = transformM $ \case transformNamedCaseBranches :: MonadEdit m ProgError => TyConName -> - (Maybe (Type' ()) -> [CaseBranch] -> m [CaseBranch]) -> + (Maybe (Type' () ()) -> [CaseBranch] -> m [CaseBranch]) -> Expr -> m Expr transformNamedCaseBranches type_ f = transformCaseBranches type_ (\m (bs, fb) -> (,fb) <$> f m bs) @@ -1855,7 +1928,7 @@ transformNamedCaseBranch :: TyConName -> ValConName -> -- This only supports ADT case branches, since we cannot edit primitives - (Maybe (Type' ()) -> CaseBranch -> m CaseBranch) -> + (Maybe (Type' () ()) -> CaseBranch -> m CaseBranch) -> Expr -> m Expr transformNamedCaseBranch type_ con f = transformNamedCaseBranches type_ $ \m -> diff --git a/primer/src/Primer/App/Base.hs b/primer/src/Primer/App/Base.hs index 3032563ee..f5fd7fba0 100644 --- a/primer/src/Primer/App/Base.hs +++ b/primer/src/Primer/App/Base.hs @@ -147,7 +147,7 @@ data NodeSelection a = NodeSelection instance HasID a => HasID (NodeSelection a) where _id = lens (getID . (.meta)) (flip $ over #meta . set _id) -getTypeDefConFieldType :: ASTTypeDef a b -> ValConName -> Int -> Maybe (Type' a) +getTypeDefConFieldType :: ASTTypeDef a b -> ValConName -> Int -> Maybe (Type' a b) getTypeDefConFieldType def con index = flip atMay index . valConArgs =<< find ((== con) . valConName) (astTypeDefConstructors def) diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs index afdb87324..c41a055d3 100644 --- a/primer/src/Primer/Core.hs +++ b/primer/src/Primer/Core.hs @@ -25,6 +25,7 @@ module Primer.Core ( _exprMeta, _exprMetaLens, _exprTypeMeta, + _exprKindMeta, bindName, _bindMeta, typesInExpr, @@ -70,8 +71,8 @@ import Primer.Core.Meta ( mkSimpleModuleName, moduleNamePretty, qualifyName, - setID, trivialMeta, + trivialMetaUnit, unsafeMkGlobalName, unsafeMkLocalName, _type, @@ -85,6 +86,7 @@ import Primer.Core.Type ( TypeMeta, _kindMeta, _kindMetaLens, + _typeKindMeta, _typeMeta, _typeMetaLens, ) @@ -100,8 +102,8 @@ import Primer.JSON -- one is better for their needs, rather than having the choice forced upon -- them. data TypeCache - = TCSynthed (Type' ()) - | TCChkedAt (Type' ()) + = TCSynthed (Type' () ()) + | TCChkedAt (Type' () ()) | TCEmb TypeCacheBoth deriving stock (Eq, Ord, Show, Read, Generic, Data) deriving (FromJSON, ToJSON) via PrimerJSON TypeCache @@ -111,7 +113,7 @@ data TypeCache -- second We don't inline this into TypeCache because then we would get partial -- functions from tcChkedAt and tcSynthed. We really want to name these fields -- though, to make it clear what each one is! -data TypeCacheBoth = TCBoth {tcChkedAt :: Type' (), tcSynthed :: Type' ()} +data TypeCacheBoth = TCBoth {tcChkedAt :: Type' () (), tcSynthed :: Type' () ()} deriving stock (Eq, Ord, Show, Read, Generic, Data) deriving (FromJSON, ToJSON) via PrimerJSON TypeCacheBoth deriving anyclass (NFData) @@ -121,11 +123,11 @@ data TypeCacheBoth = TCBoth {tcChkedAt :: Type' (), tcSynthed :: Type' ()} -- See https://github.com/well-typed/optics/pull/393 -- | An affine fold getting TCChkedAt or TCEmb's chked-at field -_chkedAt :: AffineFold TypeCache (Type' ()) +_chkedAt :: AffineFold TypeCache (Type' () ()) _chkedAt = #_TCChkedAt `afailing` (#_TCEmb % #tcChkedAt) -- | An affine fold getting TCSynthed or TCEmb's synthed field -_synthed :: AffineFold TypeCache (Type' ()) +_synthed :: AffineFold TypeCache (Type' () ()) _synthed = #_TCSynthed `afailing` (#_TCEmb % #tcSynthed) -- Expression metadata. Each expression is annotated with a type (populated by @@ -142,31 +144,31 @@ type ExprMeta = Meta (Maybe TypeCache) -- tuple '(ID, Maybe Value)'. The first element is the ID of the node, and the -- second element is an optional JSON object of metadata owned by the frontend, -- which we treat as opaque. -type Expr = Expr' ExprMeta TypeMeta +type Expr = Expr' ExprMeta TypeMeta KindMeta -- | The generic expression type. -- a is the type of annotations that are placed on every expression node. -- b is the type of annotations that are placed on every type node. -- Most of the backend fixes a ~ b ~ ID. -- The typechecker produces a ~ (ID, Type' ()), b ~ ID. -data Expr' a b - = Hole a (Expr' a b) -- See Note [Holes and bidirectionality] +data Expr' a b c + = Hole a (Expr' a b c) -- See Note [Holes and bidirectionality] | EmptyHole a - | Ann a (Expr' a b) (Type' b) - | App a (Expr' a b) (Expr' a b) - | APP a (Expr' a b) (Type' b) - | Con a ValConName [Expr' a b] -- See Note [Checkable constructors] - | Lam a LVarName (Expr' a b) - | LAM a TyVarName (Expr' a b) + | Ann a (Expr' a b c) (Type' b c) + | App a (Expr' a b c) (Expr' a b c) + | APP a (Expr' a b c) (Type' b c) + | Con a ValConName [Expr' a b c] -- See Note [Checkable constructors] + | Lam a LVarName (Expr' a b c) + | LAM a TyVarName (Expr' a b c) | Var a TmVarRef | Let a -- | bound variable LVarName -- | value the variable is bound to - (Expr' a b) + (Expr' a b c) -- | expression the binding scopes over - (Expr' a b) + (Expr' a b c) | -- | LetType binds a type to a name in some expression. -- It is currently only constructed automatically during evaluation - -- the student can't directly make it. @@ -175,23 +177,23 @@ data Expr' a b -- | bound variable TyVarName -- | value the variable is bound to - (Type' b) + (Type' b c) -- | expression the binding scopes over - (Expr' a b) + (Expr' a b c) | Letrec a -- | bound variable LVarName -- | value the variable is bound to; the variable itself is in scope, as this is a recursive let - (Expr' a b) + (Expr' a b c) -- | type of the bound variable (variable is not in scope in this type) - (Type' b) + (Type' b c) -- | body of the let; binding scopes over this - (Expr' a b) - | Case a (Expr' a b) [CaseBranch' a b] (CaseFallback' a b) -- See Note [Case] + (Expr' a b c) + | Case a (Expr' a b c) [CaseBranch' a b c] (CaseFallback' a b c) -- See Note [Case] | PrimCon a PrimCon deriving stock (Eq, Show, Read, Data, Generic) - deriving (FromJSON, ToJSON) via PrimerJSON (Expr' a b) + deriving (FromJSON, ToJSON) via PrimerJSON (Expr' a b c) deriving anyclass (NFData) -- Note [Holes and bidirectionality] @@ -295,22 +297,27 @@ data Expr' a b -- branch if we don't mention all constructors). -- | A traversal over the metadata of an expression. -_exprMeta :: forall a b c. Traversal (Expr' a b) (Expr' c b) a c -_exprMeta = param @1 +_exprMeta :: forall a a' b c. Traversal (Expr' a b c) (Expr' a' b c) a a' +_exprMeta = param @2 -- | A lens on to the metadata of an expression. -- Note that unlike '_exprMeta', this is shallow i.e. it does not recurse in to sub-expressions. -- And for this reason, it cannot be type-changing. -_exprMetaLens :: Lens' (Expr' a b) a +_exprMetaLens :: Lens' (Expr' a b c) a _exprMetaLens = position @1 -- | A traversal over the type metadata of an expression -_exprTypeMeta :: forall a b c. Traversal (Expr' a b) (Expr' a c) b c -_exprTypeMeta = param @0 +_exprTypeMeta :: forall a b b' c. Traversal (Expr' a b c) (Expr' a b' c) b b' +_exprTypeMeta = param @1 -type CaseBranch = CaseBranch' ExprMeta TypeMeta +-- | A traversal over the kind metadata of an expression +-- (Note that kinds appear in foralls which appear in types) +_exprKindMeta :: forall a b c c'. Traversal (Expr' a b c) (Expr' a b c') c c' +_exprKindMeta = param @0 -data CaseBranch' a b +type CaseBranch = CaseBranch' ExprMeta TypeMeta KindMeta + +data CaseBranch' a b c = CaseBranch -- | constructor Pattern @@ -319,24 +326,24 @@ data CaseBranch' a b -- bindings. Unfortunately that breaks generic traversals like '_exprMeta'. [Bind' a] -- | right hand side - (Expr' a b) + (Expr' a b c) deriving stock (Eq, Show, Read, Data, Generic) - deriving (FromJSON, ToJSON) via PrimerJSON (CaseBranch' a b) + deriving (FromJSON, ToJSON) via PrimerJSON (CaseBranch' a b c) deriving anyclass (NFData) -caseBranchName :: CaseBranch' a b -> Pattern +caseBranchName :: CaseBranch' a b c -> Pattern caseBranchName (CaseBranch n _ _) = n -type CaseFallback = CaseFallback' ExprMeta TypeMeta +type CaseFallback = CaseFallback' ExprMeta TypeMeta KindMeta -data CaseFallback' a b +data CaseFallback' a b c = CaseExhaustive - | CaseFallback (Expr' a b) + | CaseFallback (Expr' a b c) deriving stock (Eq, Show, Read, Data, Generic) - deriving (FromJSON, ToJSON) via PrimerJSON (CaseFallback' a b) + deriving (FromJSON, ToJSON) via PrimerJSON (CaseFallback' a b c) deriving anyclass (NFData) -traverseFallback :: Applicative f => (Expr' a b -> f (Expr' a' b')) -> CaseFallback' a b -> f (CaseFallback' a' b') +traverseFallback :: Applicative f => (Expr' a b c -> f (Expr' a' b' c')) -> CaseFallback' a b c -> f (CaseFallback' a' b' c') traverseFallback f = \case CaseExhaustive -> pure CaseExhaustive CaseFallback e -> CaseFallback <$> f e @@ -359,7 +366,7 @@ _bindMeta :: forall a b. Lens (Bind' a) (Bind' b) a b _bindMeta = position @1 -- | Note that this does not recurse in to sub-expressions or sub-types. -typesInExpr :: AffineTraversal' (Expr' a b) (Type' b) +typesInExpr :: AffineTraversal' (Expr' a b c) (Type' b c) typesInExpr = atraversalVL $ \point f -> \case Ann m e ty -> Ann m e <$> f ty APP m e ty -> APP m e <$> f ty @@ -367,13 +374,13 @@ typesInExpr = atraversalVL $ \point f -> \case Letrec m x b ty e -> (\ty' -> Letrec m x b ty' e) <$> f ty e -> point e -instance HasID a => HasID (Expr' a b) where +instance HasID a => HasID (Expr' a b c) where _id = position @1 % _id instance HasID a => HasID (Bind' a) where _id = position @1 % _id -instance HasMetadata (Expr' ExprMeta b) where +instance HasMetadata (Expr' ExprMeta b c) where _metadata = position @1 % typed @(Maybe Value) instance HasMetadata (Bind' ExprMeta) where diff --git a/primer/src/Primer/Core/DSL/Type.hs b/primer/src/Primer/Core/DSL/Type.hs index 6f5d5d0e5..f24d6ffb8 100644 --- a/primer/src/Primer/Core/DSL/Type.hs +++ b/primer/src/Primer/Core/DSL/Type.hs @@ -43,8 +43,8 @@ thole t = THole <$> meta <*> t tcon :: MonadFresh ID m => TyConName -> m Type tcon t = TCon <$> meta <*> pure t -tforall :: MonadFresh ID m => TyVarName -> Kind' () -> m Type -> m Type -tforall v k t = TForall <$> meta <*> pure v <*> pure k <*> t +tforall :: MonadFresh ID m => TyVarName -> m Kind -> m Type -> m Type +tforall v k t = TForall <$> meta <*> pure v <*> k <*> t tlet :: MonadFresh ID m => TyVarName -> m Type -> m Type -> m Type tlet v t b = TLet <$> meta <*> pure v <*> t <*> b diff --git a/primer/src/Primer/Core/Meta.hs b/primer/src/Primer/Core/Meta.hs index 293676bdd..ced09b4e4 100644 --- a/primer/src/Primer/Core/Meta.hs +++ b/primer/src/Primer/Core/Meta.hs @@ -3,7 +3,6 @@ module Primer.Core.Meta ( HasID (..), getID, - setID, HasMetadata (_metadata), ID (ID), ModuleName (ModuleName, unModuleName), @@ -26,6 +25,7 @@ module Primer.Core.Meta ( Value, Meta (Meta), trivialMeta, + trivialMetaUnit, _type, PrimCon (..), Pattern (..), @@ -76,6 +76,9 @@ _type = position @2 trivialMeta :: ID -> Meta (Maybe a) trivialMeta id = Meta id Nothing Nothing +trivialMetaUnit :: ID -> Meta () +trivialMetaUnit id = Meta id () Nothing + newtype ModuleName = ModuleName {unModuleName :: NonEmpty Name} deriving stock (Eq, Ord, Show, Read, Data, Generic) deriving (FromJSON, ToJSON) via NonEmpty Name @@ -180,11 +183,6 @@ instance HasID a => HasID (Zipper a a) where getID :: HasID a => a -> ID getID = view _id --- | Set the ID of the given expression or type. --- | Don't use this function outside of tests, since you could cause ID clashes. -setID :: HasID a => ID -> a -> a -setID = set _id - -- | A class for types which have metadata. -- This exists for the same reasons that 'HasID' does class HasMetadata a where diff --git a/primer/src/Primer/Core/Transform.hs b/primer/src/Primer/Core/Transform.hs index 79e9514bb..de149df0d 100644 --- a/primer/src/Primer/Core/Transform.hs +++ b/primer/src/Primer/Core/Transform.hs @@ -39,7 +39,7 @@ import Primer.Core.Utils (_freeVars, _freeVarsTy) -- | Attempt to replace all free ocurrences of @x@ in @e@ with @y@ -- Returns 'Nothing' if replacement could result in variable capture. -- See the tests for explanation and examples. -renameVar :: (Data a, Data b) => TmVarRef -> TmVarRef -> Expr' a b -> Maybe (Expr' a b) +renameVar :: (Data a, Data b, Data c) => TmVarRef -> TmVarRef -> Expr' a b c -> Maybe (Expr' a b c) renameVar x y expr = case expr of Lam _ v _ | sameVarRef v x -> whenNotFreeIn y expr @@ -98,20 +98,20 @@ renameVar x y expr = case expr of guard $ noneOf (typesInExpr % getting _freeVarsTy % _2) (`sameVarRef` y) expr descendM (renameVar x y) expr -whenNotFreeIn :: TmVarRef -> Expr' a b -> Maybe (Expr' a b) +whenNotFreeIn :: TmVarRef -> Expr' a b c -> Maybe (Expr' a b c) whenNotFreeIn x e = do guard $ notFreeIn x e pure e -notFreeIn :: TmVarRef -> Expr' a b -> Bool +notFreeIn :: TmVarRef -> Expr' a b c -> Bool notFreeIn x = noneOf (_freeVars % to (bimap snd snd)) (either (`sameVarRef` x) (`sameVarRef` x)) -whenNotFreeInTy :: TyVarName -> Type' b -> Maybe (Type' b) +whenNotFreeInTy :: TyVarName -> Type' b c -> Maybe (Type' b c) whenNotFreeInTy x ty = do guard $ notFreeInTy x ty pure ty -notFreeInTy :: TyVarName -> Type' b -> Bool +notFreeInTy :: TyVarName -> Type' b c -> Bool notFreeInTy = notElemOf (getting _freeVarsTy % _2) sameVarRef :: LocalName k -> TmVarRef -> Bool @@ -122,13 +122,13 @@ sameVar :: LocalName k -> LocalName l -> Bool sameVar v v' = unLocalName v == unLocalName v' -- | As 'renameVar', but specialised to local variables -renameLocalVar :: (Data a, Data b) => LVarName -> LVarName -> Expr' a b -> Maybe (Expr' a b) +renameLocalVar :: (Data a, Data b, Data c) => LVarName -> LVarName -> Expr' a b c -> Maybe (Expr' a b c) renameLocalVar x y = renameVar (LocalVarRef x) (LocalVarRef y) -- | Attempt to replace all free ocurrences of @x@ in @t@ with @y@ -- Returns 'Nothing' if replacement could result in variable capture. -- See the tests for explanation and examples. -renameTyVar :: Data a => TyVarName -> TyVarName -> Type' a -> Maybe (Type' a) +renameTyVar :: (Data a, Data b) => TyVarName -> TyVarName -> Type' a b -> Maybe (Type' a b) -- We cannot use substTy to implement renaming, as that restricts to b~(), so as to not -- duplicate metadata. But for renaming, we know that will not happen. renameTyVar x y ty = case ty of @@ -155,7 +155,7 @@ renameTyVar x y ty = case ty of -- | Attempt to replace all free ocurrences of @x@ in some type inside @e@ with @y@ -- Returns 'Nothing' if replacement could result in variable capture. -- See the tests for explanation and examples. -renameTyVarExpr :: forall a b. (Data a, Data b) => TyVarName -> TyVarName -> Expr' a b -> Maybe (Expr' a b) +renameTyVarExpr :: forall a b c. (Data a, Data b, Data c) => TyVarName -> TyVarName -> Expr' a b c -> Maybe (Expr' a b c) renameTyVarExpr x y expr = case expr of Lam _ v _ | sameVar v x -> pure expr @@ -208,29 +208,29 @@ renameTyVarExpr x y expr = case expr of descendTypeM = traverseOf typesInExpr -- | Unfold a nested term application into the application head and a list of arguments. -unfoldApp :: Expr' a b -> (Expr' a b, [Expr' a b]) +unfoldApp :: Expr' a b c -> (Expr' a b c, [Expr' a b c]) unfoldApp = second reverse . go where go (App _ f x) = let (g, args) = go f in (g, x : args) go e = (e, []) -- | Unfold a nested type-level application into the application head and a list of arguments. -unfoldTApp :: Type' a -> (Type' a, [Type' a]) +unfoldTApp :: Type' a b -> (Type' a b, [Type' a b]) unfoldTApp = second reverse . go where go (TApp _ f x) = let (g, args) = go f in (g, x : args) go e = (e, []) -- | Fold an type-level application head and a list of arguments into a single expression. -foldTApp :: (Monad m, Foldable t) => m a -> Type' a -> t (Type' a) -> m (Type' a) +foldTApp :: (Monad m, Foldable t) => m a -> Type' a b -> t (Type' a b) -> m (Type' a b) foldTApp m = foldlM $ \a b -> (\m' -> TApp m' a b) <$> m -- | @mkTAppCon C [X,Y,Z] = C X Y Z@ -mkTAppCon :: TyConName -> [Type' ()] -> Type' () +mkTAppCon :: TyConName -> [Type' () ()] -> Type' () () mkTAppCon c = runIdentity . foldTApp (pure ()) (TCon () c) -- | Decompose @C X Y Z@ to @(C,[X,Y,Z])@ -decomposeTAppCon :: Type' a -> Maybe (TyConName, [Type' a]) +decomposeTAppCon :: Type' a b -> Maybe (TyConName, [Type' a b]) decomposeTAppCon = unfoldTApp <&> \case (TCon _ con, args) -> Just (con, args) @@ -238,7 +238,7 @@ decomposeTAppCon = -- | Split a function type into an array of argument types and the result type. -- Takes two arguments: the lhs and rhs of the topmost function node. -unfoldFun :: Type' a -> Type' a -> (NonEmpty (Type' a), Type' a) +unfoldFun :: Type' a b -> Type' a b -> (NonEmpty (Type' a b), Type' a b) unfoldFun a (TFun _ b c) = let (argTypes, resultType) = unfoldFun b c in (NE.cons a argTypes, resultType) diff --git a/primer/src/Primer/Core/Type.hs b/primer/src/Primer/Core/Type.hs index ddd62d06d..d6a5b1c19 100644 --- a/primer/src/Primer/Core/Type.hs +++ b/primer/src/Primer/Core/Type.hs @@ -6,6 +6,7 @@ module Primer.Core.Type ( TypeMeta, _typeMeta, _typeMetaLens, + _typeKindMeta, KindMeta, _kindMeta, _kindMetaLens, @@ -34,21 +35,21 @@ import Primer.JSON -- Type variables are currently represented as text, and we have no compile-time -- checks on scoping. We may want to introduce de Bruijn indices or use -- bound/unbound in the future. -type Type = Type' TypeMeta +type Type = Type' TypeMeta KindMeta -- | Type metadata. Each type is optionally annotated with a kind. -- Currently we don't fill these in during typechecking. type TypeMeta = Meta (Maybe (Kind' ())) -- | NB: Be careful with equality -- it is on-the-nose, rather than up-to-alpha: see Subst:alphaEqTy -data Type' a +data Type' a b = TEmptyHole a - | THole a (Type' a) + | THole a (Type' a b) | TCon a TyConName - | TFun a (Type' a) (Type' a) + | TFun a (Type' a b) (Type' a b) | TVar a TyVarName - | TApp a (Type' a) (Type' a) - | TForall a TyVarName (Kind' ()) (Type' a) + | TApp a (Type' a b) (Type' a b) + | TForall a TyVarName (Kind' b) (Type' a b) | -- | TLet is a let binding at the type level. -- It is currently only constructed automatically during evaluation - -- the student can't directly make it. @@ -57,23 +58,27 @@ data Type' a -- | bound variable TyVarName -- | type the variable is bound to; the variable itself is not in scope, this is a non-recursive let - (Type' a) + (Type' a b) -- | body of the let; binding scopes over this - (Type' a) + (Type' a b) deriving stock (Eq, Ord, Show, Read, Data, Generic) - deriving (FromJSON, ToJSON) via PrimerJSON (Type' a) + deriving (FromJSON, ToJSON) via PrimerJSON (Type' a b) deriving anyclass (NFData) -- | A traversal over the metadata of a type -_typeMeta :: Traversal (Type' a) (Type' b) a b -_typeMeta = param @0 +_typeMeta :: Traversal (Type' a c) (Type' b c) a b +_typeMeta = param @1 -- | A lens on to the metadata of a type. -- Note that unlike '_typeMeta', this is shallow i.e. it does not recurse in to sub-expressions. -- And for this reason, it cannot be type-changing. -_typeMetaLens :: Lens' (Type' a) a +_typeMetaLens :: Lens' (Type' a b) a _typeMetaLens = position @1 +-- | A traversal over the kind metadata of an type +_typeKindMeta :: forall a b c. Traversal (Type' a b) (Type' a c) b c +_typeKindMeta = param @0 + -- | Core kinds. type Kind = Kind' KindMeta @@ -98,10 +103,10 @@ _kindMeta = param @0 _kindMetaLens :: Lens' (Kind' a) a _kindMetaLens = position @1 -instance HasID a => HasID (Type' a) where +instance HasID a => HasID (Type' a b) where _id = position @1 % _id -instance HasMetadata (Type' TypeMeta) where +instance HasMetadata (Type' TypeMeta b) where _metadata = position @1 % typed @(Maybe Value) instance HasID a => HasID (Kind' a) where diff --git a/primer/src/Primer/Core/Type/Utils.hs b/primer/src/Primer/Core/Type/Utils.hs index 4798ab46e..782473f03 100644 --- a/primer/src/Primer/Core/Type/Utils.hs +++ b/primer/src/Primer/Core/Type/Utils.hs @@ -3,6 +3,7 @@ module Primer.Core.Type.Utils ( kindIDs, generateTypeIDs, regenerateTypeIDs, + regenerateKindIDs, generateKindIDs, forgetTypeMetadata, forgetKindMetadata, @@ -26,6 +27,7 @@ import Data.Set.Optics (setOf) import Optics ( Traversal, Traversal', + adjoin, getting, hasn't, set, @@ -41,6 +43,7 @@ import Primer.Core.Meta ( ID, TyVarName, trivialMeta, + trivialMetaUnit, ) import Primer.Core.Type ( Kind, @@ -48,28 +51,34 @@ import Primer.Core.Type ( Type, Type' (..), _kindMeta, + _typeKindMeta, _typeMeta, ) import Primer.Zipper.Type (getBoundHereDnTy) --- | Regenerate all IDs, not changing any other metadata -regenerateTypeIDs :: (HasID a, MonadFresh ID m) => Type' a -> m (Type' a) -regenerateTypeIDs = regenerateTypeIDs' (set _id) +-- | Regenerate all IDs (including in kinds), not changing any other metadata +regenerateTypeIDs :: (HasID a, HasID b, MonadFresh ID m) => Type' a b -> m (Type' a b) +regenerateTypeIDs = regenerateTypeIDs' (set _id) (set _id) -regenerateTypeIDs' :: MonadFresh ID m => (ID -> a -> b) -> Type' a -> m (Type' b) -regenerateTypeIDs' s = traverseOf _typeMeta (\a -> flip s a <$> fresh) +regenerateTypeIDs' :: MonadFresh ID m => (ID -> a -> a') -> (ID -> b -> b') -> Type' a b -> m (Type' a' b') +regenerateTypeIDs' st sk = + traverseOf _typeMeta (\a -> flip st a <$> fresh) + >=> traverseOf _typeKindMeta (\a -> flip sk a <$> fresh) + +regenerateKindIDs :: (HasID a, MonadFresh ID m) => Kind' a -> m (Kind' a) +regenerateKindIDs = traverseOf _kindMeta (\a -> flip (set _id) a <$> fresh) -- | Adds 'ID's and trivial metadata -generateTypeIDs :: MonadFresh ID m => Type' () -> m Type -generateTypeIDs = regenerateTypeIDs' $ const . trivialMeta +generateTypeIDs :: MonadFresh ID m => Type' () () -> m Type +generateTypeIDs = regenerateTypeIDs' (const . trivialMeta) (const . trivialMetaUnit) generateKindIDs :: MonadFresh ID m => Kind' () -> m Kind generateKindIDs = traverseOf _kindMeta $ \() -> kmeta --- | Replace all 'ID's in a Type with unit. +-- | Replace all 'ID's in a Type (including in embedded kinds) with unit. -- Technically this replaces all annotations, regardless of what they are. -forgetTypeMetadata :: Type' a -> Type' () -forgetTypeMetadata = set _typeMeta () +forgetTypeMetadata :: Type' a b -> Type' () () +forgetTypeMetadata = set _typeMeta () . set _typeKindMeta () -- | Replace all metadata in a Kind with unit. forgetKindMetadata :: Kind' a -> Kind' () @@ -77,7 +86,7 @@ forgetKindMetadata = set _kindMeta () -- | Test whether an type contains any holes -- (empty or non-empty, or inside a kind) -noHoles :: Data a => Type' a -> Bool +noHoles :: (Data a, Data b) => Type' a b -> Bool noHoles t = flip all (universe t) $ \case THole{} -> False TEmptyHole{} -> False @@ -86,15 +95,15 @@ noHoles t = flip all (universe t) $ \case _ -> True _ -> True -freeVarsTy :: Type' a -> Set TyVarName +freeVarsTy :: Type' a b -> Set TyVarName freeVarsTy = setOf (getting _freeVarsTy % _2) -_freeVarsTy :: Traversal (Type' a) (Type' a) (a, TyVarName) (Type' a) +_freeVarsTy :: Traversal (Type' a b) (Type' a b) (a, TyVarName) (Type' a b) _freeVarsTy = traversalVL $ traverseFreeVarsTy mempty -- Helper for _freeVarsTy and _freeTyVars -- Takes a set of considered-to-be-bound variables -traverseFreeVarsTy :: Applicative f => Set TyVarName -> ((a, TyVarName) -> f (Type' a)) -> Type' a -> f (Type' a) +traverseFreeVarsTy :: Applicative f => Set TyVarName -> ((a, TyVarName) -> f (Type' a b)) -> Type' a b -> f (Type' a b) traverseFreeVarsTy = go where go bound f = \case @@ -109,7 +118,7 @@ traverseFreeVarsTy = go TForall m a k s -> TForall m a k <$> go (S.insert a bound) f s TLet m a t b -> TLet m a <$> go bound f t <*> go (S.insert a bound) f b -boundVarsTy :: (Data a, Eq a) => Type' a -> Set TyVarName +boundVarsTy :: (Data a, Eq a, Data b, Eq b) => Type' a b -> Set TyVarName boundVarsTy = foldMap' getBoundHereDnTy . universe -- Check two types for alpha equality @@ -120,7 +129,7 @@ boundVarsTy = foldMap' getBoundHereDnTy . universe -- -- Note that we do not expand TLets, they must be structurally -- the same (perhaps with a different named binding) -alphaEqTy :: Type' () -> Type' () -> Bool +alphaEqTy :: Type' () () -> Type' () () -> Bool alphaEqTy = go (0, mempty, mempty) where go _ (TEmptyHole _) (TEmptyHole _) = True @@ -141,12 +150,12 @@ alphaEqTy = go (0, mempty, mempty) -- in the map. new (c, p, q) n m = (c + 1 :: Int, M.insert n c p, M.insert m c q) -concreteTy :: Data b => Type' b -> Bool +concreteTy :: (Data b, Data c) => Type' b c -> Bool concreteTy ty = hasn't (getting _freeVarsTy) ty && noHoles ty --- | Traverse the 'ID's in a 'Type''. -typeIDs :: HasID a => Traversal' (Type' a) ID -typeIDs = _typeMeta % _id +-- | Traverse the 'ID's in a 'Type'' (including in any 'Kind's). +typeIDs :: (HasID a, HasID b) => Traversal' (Type' a b) ID +typeIDs = (_typeMeta % _id) `adjoin` (_typeKindMeta % _id) -- | Traverse the 'ID's in a 'Type''. kindIDs :: HasID a => Traversal' (Kind' a) ID diff --git a/primer/src/Primer/Core/Utils.hs b/primer/src/Primer/Core/Utils.hs index 213393ef0..49ef8b70b 100644 --- a/primer/src/Primer/Core/Utils.hs +++ b/primer/src/Primer/Core/Utils.hs @@ -5,6 +5,7 @@ module Primer.Core.Utils ( typeIDs, generateTypeIDs, regenerateTypeIDs, + regenerateKindIDs, generateKindIDs, forgetTypeMetadata, forgetKindMetadata, @@ -63,6 +64,8 @@ import Primer.Core ( bindName, traverseFallback, trivialMeta, + trivialMetaUnit, + _exprKindMeta, _exprMeta, _exprTypeMeta, ) @@ -77,6 +80,7 @@ import Primer.Core.Type.Utils ( generateKindIDs, generateTypeIDs, noHoles, + regenerateKindIDs, regenerateTypeIDs, traverseFreeVarsTy, typeIDs, @@ -84,40 +88,47 @@ import Primer.Core.Type.Utils ( ) import Primer.Name (Name) --- | Regenerate all IDs, not changing any other metadata -regenerateExprIDs :: (HasID a, HasID b, MonadFresh ID m) => Expr' a b -> m (Expr' a b) -regenerateExprIDs = regenerateExprIDs' (set _id) (set _id) +-- | Regenerate all IDs (including in types and kinds), not changing any other metadata +regenerateExprIDs :: (HasID a, HasID b, HasID c, MonadFresh ID m) => Expr' a b c -> m (Expr' a b c) +regenerateExprIDs = regenerateExprIDs' (set _id) (set _id) (set _id) -regenerateExprIDs' :: MonadFresh ID m => (ID -> a -> a') -> (ID -> b -> b') -> Expr' a b -> m (Expr' a' b') -regenerateExprIDs' se st = +regenerateExprIDs' :: + MonadFresh ID m => + (ID -> a -> a') -> + (ID -> b -> b') -> + (ID -> c -> c') -> + Expr' a b c -> + m (Expr' a' b' c') +regenerateExprIDs' se st sk = traverseOf _exprMeta (\a -> flip se a <$> fresh) >=> traverseOf _exprTypeMeta (\a -> flip st a <$> fresh) + >=> traverseOf _exprKindMeta (\a -> flip sk a <$> fresh) -- | Like 'generateTypeIDs', but for expressions -generateIDs :: MonadFresh ID m => Expr' () () -> m Expr -generateIDs = regenerateExprIDs' (const . trivialMeta) (const . trivialMeta) +generateIDs :: MonadFresh ID m => Expr' () () () -> m Expr +generateIDs = regenerateExprIDs' (const . trivialMeta) (const . trivialMeta) (const . trivialMetaUnit) -- | Like 'forgetTypeMetadata', but for expressions -forgetMetadata :: Expr' a b -> Expr' () () -forgetMetadata = set _exprTypeMeta () . set _exprMeta () +forgetMetadata :: Expr' a b c -> Expr' () () () +forgetMetadata = set _exprKindMeta () . set _exprTypeMeta () . set _exprMeta () -- Both term and type vars, but not constructors or global variables. -- This is because constructor names and global variables are never -- captured by lambda bindings etc (since they are looked up in a different -- namespace) -freeVars :: Expr' a b -> Set Name +freeVars :: Expr' a b c -> Set Name freeVars = setOf $ _freeVars % (_Left % _2 % to unLocalName `summing` _Right % _2 % to unLocalName) -- We can't offer a traversal, as we can't enforce replacing term vars with -- terms and type vars with types. Use _freeTmVars and _freeTyVars for -- traversals. -_freeVars :: Fold (Expr' a b) (Either (a, LVarName) (b, TyVarName)) +_freeVars :: Fold (Expr' a b c) (Either (a, LVarName) (b, TyVarName)) _freeVars = getting _freeTmVars % to Left `summing` getting _freeTyVars % to Right -_freeTmVars :: Traversal (Expr' a b) (Expr' a b) (a, LVarName) (Expr' a b) +_freeTmVars :: Traversal (Expr' a b c) (Expr' a b c) (a, LVarName) (Expr' a b c) _freeTmVars = traversalVL $ go mempty where - go :: Applicative f => Set LVarName -> ((a, LVarName) -> f (Expr' a b)) -> Expr' a b -> f (Expr' a b) + go :: Applicative f => Set LVarName -> ((a, LVarName) -> f (Expr' a b c)) -> Expr' a b c -> f (Expr' a b c) go bound f = \case Hole m e -> Hole m <$> go bound f e t@EmptyHole{} -> pure t @@ -146,10 +157,10 @@ _freeTmVars = traversalVL $ go mempty where freeVarsBr (CaseBranch c binds e) = CaseBranch c binds <$> go (S.union bound $ S.fromList $ map bindName binds) f e -_freeTyVars :: Traversal (Expr' a b) (Expr' a b) (b, TyVarName) (Type' b) +_freeTyVars :: Traversal (Expr' a b c) (Expr' a b c) (b, TyVarName) (Type' b c) _freeTyVars = traversalVL $ go mempty where - go :: Applicative f => Set TyVarName -> ((b, TyVarName) -> f (Type' b)) -> Expr' a b -> f (Expr' a b) + go :: Applicative f => Set TyVarName -> ((b, TyVarName) -> f (Type' b c)) -> Expr' a b c -> f (Expr' a b c) go bound f = \case Hole m e -> Hole m <$> go bound f e t@EmptyHole{} -> pure t @@ -177,9 +188,9 @@ _freeTyVars = traversalVL $ go mempty where freeVarsBr (CaseBranch c binds e) = CaseBranch c binds <$> go bound f e -- case branches only bind term variables -freeGlobalVars :: (Data a, Data b) => Expr' a b -> Set GVarName +freeGlobalVars :: (Data a, Data b, Data c) => Expr' a b c -> Set GVarName freeGlobalVars e = S.fromList [v | Var _ (GlobalVarRef v) <- universe e] -- | Traverse the 'ID's in an 'Expr''. -exprIDs :: (HasID a, HasID b) => Traversal' (Expr' a b) ID -exprIDs = (_exprMeta % _id) `adjoin` (_exprTypeMeta % _id) +exprIDs :: (HasID a, HasID b, HasID c) => Traversal' (Expr' a b c) ID +exprIDs = (_exprMeta % _id) `adjoin` (_exprTypeMeta % _id) `adjoin` (_exprKindMeta % _id) diff --git a/primer/src/Primer/Def.hs b/primer/src/Primer/Def.hs index ca6b31fe0..c127bcabb 100644 --- a/primer/src/Primer/Def.hs +++ b/primer/src/Primer/Def.hs @@ -32,7 +32,7 @@ data Def deriving (FromJSON, ToJSON) via PrimerJSON Def deriving anyclass (NFData) -defType :: Def -> Type' () +defType :: Def -> Type' () () defType = \case DefPrim d -> primDefType d DefAST d -> forgetTypeMetadata $ astDefType d diff --git a/primer/src/Primer/Def/Utils.hs b/primer/src/Primer/Def/Utils.hs index 8ef3b027d..3f5f8858c 100644 --- a/primer/src/Primer/Def/Utils.hs +++ b/primer/src/Primer/Def/Utils.hs @@ -47,7 +47,7 @@ globalInUse v = (Set.member v) -- | Is this type (including any of its constructors) in use in the given definitions? -typeInUse :: (Foldable f, Foldable g, Data a', Ord a') => TyConName -> ASTTypeDef a b -> f (TypeDef a' b') -> g Def -> Bool +typeInUse :: (Foldable f, Foldable g, Data a', Ord a', Data b') => TyConName -> ASTTypeDef a b -> f (TypeDef a' b') -> g Def -> Bool typeInUse defName def ts ds = anyOf (folded % #_TypeDefAST % to tyConsInTypeDef) diff --git a/primer/src/Primer/Eval/Detail.hs b/primer/src/Primer/Eval/Detail.hs index f10533257..339a7f548 100644 --- a/primer/src/Primer/Eval/Detail.hs +++ b/primer/src/Primer/Eval/Detail.hs @@ -16,7 +16,7 @@ import Foreword import Primer.Core (Expr) import Primer.Core.Meta (LocalNameKind (..)) -import Primer.Core.Type (Kind', Type) +import Primer.Core.Type (Kind, Type) import Primer.Eval.Ann as Ann import Primer.Eval.Beta as Beta import Primer.Eval.Bind as Bind @@ -32,7 +32,7 @@ data EvalDetail = -- | Reduction of (λx. a : S -> T) b BetaReduction (BetaReductionDetail 'ATmVar Type Type) | -- | Reduction of (Λx. a : ∀y:k. T) S - BETAReduction (BetaReductionDetail 'ATyVar (Kind' ()) Type) + BETAReduction (BetaReductionDetail 'ATyVar Kind Type) | -- | Inlining of a local (let-bound) variable LocalVarInline (LocalVarInlineDetail 'ATmVar) | -- | Inlining of a local (let-bound) type variable diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs index bb07e910d..b6a41ad35 100644 --- a/primer/src/Primer/Eval/Redex.hs +++ b/primer/src/Primer/Eval/Redex.hs @@ -100,7 +100,7 @@ import Primer.Core ( ) import Primer.Core.DSL (ann, letType, let_, letrec, lvar, tlet, tvar) import Primer.Core.Transform (decomposeTAppCon) -import Primer.Core.Type (Kind') +import Primer.Core.Type (Kind) import Primer.Core.Utils ( concreteTy, forgetTypeMetadata, @@ -215,7 +215,7 @@ data EvalLog | -- | Found something that may have been a case redex, -- but the scrutinee's type is either under or over saturated. -- This should not happen if the expression is type correct. - CaseRedexNotSaturated (Type' ()) + CaseRedexNotSaturated (Type' () ()) | -- | Found something that may have been a case redex, -- but the scrutinee's head (value) constructor does not construct a member of the scrutinee's type. -- This should not happen if the expression is type correct. @@ -224,7 +224,7 @@ data EvalLog -- but the number of arguments in the scrutinee differs from the number of bindings in the corresponding branch. -- (Or the number of arguments expected from the scrutinee's type differs from either of these.) -- This should not happen if the expression is type correct. - CaseRedexWrongArgNum Pattern [Expr] [Type' ()] [LVarName] + CaseRedexWrongArgNum Pattern [Expr] [Type' () ()] [LVarName] | InvariantFailure Text deriving stock (Show, Eq, Data, Generic) deriving anyclass (NFData) @@ -321,7 +321,7 @@ data Redex -- ^ The body of the Λ , forallVar :: TyVarName -- ^ The annotation on the Λ must be a ∀, which binds this variable - , forallKind :: Kind' () + , forallKind :: Kind -- ^ The kind of the ∀ bound variable (used for details) , tgtTy :: Type -- ^ The body of the ∀ in the annotation @@ -350,10 +350,10 @@ data Redex -- ^ The head of the scrutinee , args :: [Expr] -- ^ The arguments of the scrutinee - , argTys :: [Type' ()] + , argTys :: [Type' () ()] -- ^ The type of each scrutinee's argument, directly from the constructor's definition -- (thus is not well formed in the current scope) - , params :: [(TyVarName, Type' ())] + , params :: [(TyVarName, Type' () ())] -- ^ The parameters of the constructor's datatype, and their -- instantiations from inspecting the type annotation on the scrutinee. , binders :: Maybe [Bind] @@ -472,7 +472,7 @@ data RedexType -- ^ metadata on forall (used for reduction) , origBinder :: TyVarName -- ^ original name, which we want to freshen (used for reduction, and finding normal-order redex) - , kind :: Kind' () + , kind :: Kind -- ^ kind of bound var (used for reduction) , body :: Type -- ^ body of forall (used for reduction) @@ -494,10 +494,10 @@ _LetTyBind = afolding $ \case LetTyBind b -> pure b; _ -> Nothing _LetTypeBind :: AffineFold LetTypeBinding (TyVarName, Type) _LetTypeBind = afolding $ \case LetTypeBind n t -> pure (n, t) -_freeVars' :: Fold (Expr' a b) Name +_freeVars' :: Fold (Expr' a b c) Name _freeVars' = _freeVars % to (either (unLocalName . snd) (unLocalName . snd)) -_freeVarsTy' :: Fold (Type' b) Name +_freeVarsTy' :: Fold (Type' b c) Name _freeVarsTy' = getting _freeVarsTy % _2 % to unLocalName -- | Fold over the free variables in the unfolding of this definition. @@ -625,8 +625,8 @@ viewCaseRedex tydefs = \case else Just $ RenameBindingsCase{meta, scrutinee, branches, fallbackBranch, avoid, orig} formCaseRedex :: Pattern -> - [Type' ()] -> - [(TyVarName, Type' ())] -> + [Type' () ()] -> + [(TyVarName, Type' () ())] -> [Expr] -> Maybe [Bind] -> Expr -> diff --git a/primer/src/Primer/Examples.hs b/primer/src/Primer/Examples.hs index c6c938df6..75316b049 100644 --- a/primer/src/Primer/Examples.hs +++ b/primer/src/Primer/Examples.hs @@ -65,7 +65,6 @@ import Primer.Builtins.DSL ( import Primer.Core ( GVarName, ID, - Kind' (KType), ModuleName (unModuleName), mkSimpleModuleName, qualifyName, @@ -86,6 +85,7 @@ import Primer.Core.DSL ( gvar', hole, int, + ktype, lAM, lam, letType, @@ -138,7 +138,7 @@ map :: MonadFresh ID m => ModuleName -> m (GVarName, Def) map modName = let this = qualifyName modName "map" in do - type_ <- tforall "a" (KType ()) $ tforall "b" (KType ()) $ (tvar "a" `tfun` tvar "b") `tfun` ((tcon B.tList `tapp` tvar "a") `tfun` (tcon B.tList `tapp` tvar "b")) + type_ <- tforall "a" ktype $ tforall "b" ktype $ (tvar "a" `tfun` tvar "b") `tfun` ((tcon B.tList `tapp` tvar "a") `tfun` (tcon B.tList `tapp` tvar "b")) term <- lAM "a" $ lAM "b" $ @@ -157,7 +157,7 @@ map modName = -- 'listDef'), implemented using a worker. map' :: MonadFresh ID m => ModuleName -> m (GVarName, Def) map' modName = do - type_ <- tforall "a" (KType ()) $ tforall "b" (KType ()) $ (tvar "a" `tfun` tvar "b") `tfun` ((tcon B.tList `tapp` tvar "a") `tfun` (tcon B.tList `tapp` tvar "b")) + type_ <- tforall "a" ktype $ tforall "b" ktype $ (tvar "a" `tfun` tvar "b") `tfun` ((tcon B.tList `tapp` tvar "a") `tfun` (tcon B.tList `tapp` tvar "b")) let worker = lam "xs" $ case_ @@ -235,7 +235,7 @@ comprehensive' typeable modName = do (tcon B.tNat) ( tforall "a" - (KType ()) + ktype ( tapp ( thole ( tapp @@ -274,7 +274,7 @@ comprehensive' typeable modName = do lAM "b" (lam "x" $ con B.cLeft [lvar "x"]) `ann` tforall "b" - (KType ()) + ktype ( tcon B.tBool `tfun` (tcon B.tEither `tapp` tcon B.tBool `tapp` tvar "b") ) @@ -319,7 +319,7 @@ comprehensive' typeable modName = do (tcon B.tNat) ( tforall "α" - (KType ()) + ktype ( tapp ( tapp (tcon B.tEither) diff --git a/primer/src/Primer/Module.hs b/primer/src/Primer/Module.hs index 050e7527d..419d2d886 100644 --- a/primer/src/Primer/Module.hs +++ b/primer/src/Primer/Module.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE OverloadedLabels #-} - module Primer.Module ( Module (..), qualifyTyConName, @@ -26,7 +24,6 @@ import Data.List.Extra (enumerate) import Data.Map (delete, insert, mapKeys, member) import Data.Map qualified as M import Data.Semigroup (Max (Max, getMax)) -import Optics (Field2 (_2), traverseOf, traversed, (%)) import Primer.Builtins ( boolDef, builtinModuleName, @@ -53,7 +50,6 @@ import Primer.Core ( qualifyName, ) import Primer.Core.DSL -import Primer.Core.Utils (generateKindIDs, generateTypeIDs) import Primer.Def ( Def (..), DefMap, @@ -67,7 +63,7 @@ import Primer.JSON ( ) import Primer.Name (Name) import Primer.Primitives (allPrimTypeDefs, primDefName, primitiveModuleName) -import Primer.TypeDef (ASTTypeDef (..), PrimTypeDef (..), TypeDef (..), TypeDefMap, forgetTypeDefMetadata, _typedefFields) +import Primer.TypeDef (TypeDef (..), TypeDefMap, forgetTypeDefMetadata, generateTypeDefIDs) data Module = Module { moduleName :: ModuleName @@ -136,22 +132,22 @@ nextModuleID m = -- It contains all primitive types and terms. primitiveModule :: MonadFresh ID m => m Module primitiveModule = do - allPrimTypeDefs' <- traverse (traverseOf (#primTypeDefParameters % traversed % _2) generateKindIDs) allPrimTypeDefs + allPrimTypeDefs' <- traverse (generateTypeDefIDs . TypeDefPrim) allPrimTypeDefs pure Module { moduleName = primitiveModuleName - , moduleTypes = TypeDefPrim <$> M.mapKeys baseName allPrimTypeDefs' + , moduleTypes = M.mapKeys baseName allPrimTypeDefs' , moduleDefs = M.fromList $ [(primDefName def, DefPrim def) | def <- enumerate] } builtinModule :: MonadFresh ID m => m Module builtinModule = do - boolDef' <- traverseOf _typedefFields generateTypeIDs $ TypeDefAST boolDef - natDef' <- traverseOf _typedefFields generateTypeIDs $ TypeDefAST natDef - listDef' <- traverseOf _typedefFields generateTypeIDs . TypeDefAST =<< traverseOf (#astTypeDefParameters % traversed % _2) generateKindIDs listDef - maybeDef' <- traverseOf _typedefFields generateTypeIDs . TypeDefAST =<< traverseOf (#astTypeDefParameters % traversed % _2) generateKindIDs maybeDef - pairDef' <- traverseOf _typedefFields generateTypeIDs . TypeDefAST =<< traverseOf (#astTypeDefParameters % traversed % _2) generateKindIDs pairDef - eitherDef' <- traverseOf _typedefFields generateTypeIDs . TypeDefAST =<< traverseOf (#astTypeDefParameters % traversed % _2) generateKindIDs eitherDef + boolDef' <- generateTypeDefIDs $ TypeDefAST boolDef + natDef' <- generateTypeDefIDs $ TypeDefAST natDef + listDef' <- generateTypeDefIDs $ TypeDefAST listDef + maybeDef' <- generateTypeDefIDs $ TypeDefAST maybeDef + pairDef' <- generateTypeDefIDs $ TypeDefAST pairDef + eitherDef' <- generateTypeDefIDs $ TypeDefAST eitherDef pure $ Module { moduleName = builtinModuleName diff --git a/primer/src/Primer/Prelude/Polymorphism.hs b/primer/src/Primer/Prelude/Polymorphism.hs index 68e99d212..164411a54 100644 --- a/primer/src/Primer/Prelude/Polymorphism.hs +++ b/primer/src/Primer/Prelude/Polymorphism.hs @@ -20,7 +20,7 @@ import Primer.Builtins (cCons, cNil) import Primer.Builtins.DSL ( listOf, ) -import Primer.Core (GVarName, ID, Kind' (KType), qualifyName) +import Primer.Core (GVarName, ID, qualifyName) import Primer.Core.DSL ( app, apps, @@ -29,6 +29,7 @@ import Primer.Core.DSL ( case_, con, gvar, + ktype, lAM, lam, lvar, @@ -44,7 +45,7 @@ id = qualifyName modName "id" idDef :: MonadFresh ID m => m Def idDef = do - type_ <- tforall "a" (KType ()) $ tvar "a" `tfun` tvar "a" + type_ <- tforall "a" ktype $ tvar "a" `tfun` tvar "a" term <- lAM "a" $ lam "x" (lvar "x") pure $ DefAST $ ASTDef term type_ @@ -53,7 +54,7 @@ const = qualifyName modName "const" constDef :: MonadFresh ID m => m Def constDef = do - type_ <- tforall "a" (KType ()) $ tvar "a" `tfun` tforall "b" (KType ()) (tvar "b" `tfun` tvar "a") + type_ <- tforall "a" ktype $ tvar "a" `tfun` tforall "b" ktype (tvar "b" `tfun` tvar "a") term <- lAM "a" $ lam "x" $ lAM "b" $ lam "y" (lvar "x") pure $ DefAST $ ASTDef term type_ @@ -63,8 +64,8 @@ map = qualifyName modName "map" mapDef :: MonadFresh ID m => m Def mapDef = do type_ <- - tforall "a" (KType ()) $ - tforall "b" (KType ()) $ + tforall "a" ktype $ + tforall "b" ktype $ (tvar "a" `tfun` tvar "b") `tfun` (listOf (tvar "a") `tfun` listOf (tvar "b")) term <- @@ -88,8 +89,8 @@ foldr = qualifyName modName "foldr" foldrDef :: MonadFresh ID m => m Def foldrDef = do type_ <- - tforall "a" (KType ()) $ - tforall "b" (KType ()) $ + tforall "a" ktype $ + tforall "b" ktype $ (tvar "a" `tfun` (tvar "b" `tfun` tvar "b")) `tfun` (tvar "b" `tfun` (listOf (tvar "a") `tfun` tvar "b")) term <- diff --git a/primer/src/Primer/Pretty.hs b/primer/src/Primer/Pretty.hs index bc70c1293..7ffdd2e32 100644 --- a/primer/src/Primer/Pretty.hs +++ b/primer/src/Primer/Pretty.hs @@ -85,7 +85,7 @@ compact = } -- | Pretty prints @Expr'@ using Prettyprinter library -prettyExpr :: PrettyOptions -> Expr' a b -> Doc AnsiStyle +prettyExpr :: PrettyOptions -> Expr' a b c -> Doc AnsiStyle prettyExpr opts = \case Hole _ e -> (if inlineHoles opts then group else identity) (brac Curly Red (pE e)) EmptyHole _ -> col Red "?" @@ -232,7 +232,7 @@ col :: Color -> Doc AnsiStyle -> Doc AnsiStyle col = annotate . color -- | Pretty prints @Type'@ using Prettyprinter library -prettyType :: PrettyOptions -> Type' b -> Doc AnsiStyle +prettyType :: PrettyOptions -> Type' b c -> Doc AnsiStyle prettyType opts typ = case typ of TEmptyHole _ -> col Red "?" THole _ t -> (if inlineHoles opts then group else identity) (brac Curly Red (pT t)) diff --git a/primer/src/Primer/Primitives.hs b/primer/src/Primer/Primitives.hs index 94320d4d9..3c4d3cd63 100644 --- a/primer/src/Primer/Primitives.hs +++ b/primer/src/Primer/Primitives.hs @@ -59,7 +59,7 @@ data PrimFunError PrimFunError PrimDef -- | Arguments - [Expr' () ()] + [Expr' () () ()] deriving stock (Eq, Show, Data, Generic) deriving (FromJSON, ToJSON) via PrimerJSON PrimFunError @@ -136,10 +136,10 @@ primDefName = \case IntToNat -> "Int.toNat" IntFromNat -> "Int.fromNat" -primDefType :: PrimDef -> Type' () +primDefType :: PrimDef -> Type' () () primDefType = uncurry (flip $ foldr $ TFun ()) . primFunTypes -primFunTypes :: PrimDef -> ([Type' ()], Type' ()) +primFunTypes :: PrimDef -> ([Type' () ()], Type' () ()) primFunTypes = \case ToUpper -> ([c tChar], c tChar) IsSpace -> ([c tChar], c tBool) @@ -165,7 +165,7 @@ primFunTypes = \case c = TCon () a = TApp () -primFunDef :: PrimDef -> [Expr' () ()] -> Either PrimFunError (forall m. MonadFresh ID m => m Expr) +primFunDef :: PrimDef -> [Expr' () () ()] -> Either PrimFunError (forall m. MonadFresh ID m => m Expr) primFunDef def args = case def of ToUpper -> case args of [PrimCon _ (PrimChar c)] -> diff --git a/primer/src/Primer/Questions.hs b/primer/src/Primer/Questions.hs index 61dcd84bf..c9dbe78a8 100644 --- a/primer/src/Primer/Questions.hs +++ b/primer/src/Primer/Questions.hs @@ -35,9 +35,14 @@ import Primer.Name.Fresh (mkAvoidForFreshName, mkAvoidForFreshNameTy, mkAvoidFor import Primer.TypeDef (typeDefNameHints) import Primer.Typecheck.Cxt (Cxt, typeDefs) import Primer.Zipper ( - ExprZ, - TypeZ, + BindLoc' (BindCase), + KindTZ, + Loc, + Loc' (InBind, InExpr, InKind, InType), TypeZip, + unfocusCaseBind, + unfocusKind, + unfocusKindT, ) import Primer.ZipperCxt ( ShadowedVarsExpr (M), @@ -58,14 +63,14 @@ data Question a where ID -> Question ( ( [(TyVarName, Kind' ())] - , [(LVarName, Type' ())] + , [(LVarName, Type' () ())] ) - , [(GVarName, Type' ())] + , [(GVarName, Type' () ())] ) GenerateName :: GVarName -> ID -> - Either (Maybe (Type' ())) (Maybe (Kind' ())) -> + Either (Maybe (Type' () ())) (Maybe (Kind' ())) -> Question [Name] -- | Collect the typing context for the focused node. @@ -76,46 +81,50 @@ data Question a where -- the third is globals. variablesInScopeExpr :: DefMap -> - Either ExprZ TypeZ -> - ([(TyVarName, Kind' ())], [(LVarName, Type' ())], [(GVarName, Type' ())]) -variablesInScopeExpr defs exprOrTy = - let locals = either extractLocalsExprZ extractLocalsTypeZ exprOrTy + Loc -> + ([(TyVarName, Kind' ())], [(LVarName, Type' () ())], [(GVarName, Type' () ())]) +variablesInScopeExpr defs loc = + let locals = case loc of + InExpr ze -> extractLocalsExprZ ze + InType zt -> extractLocalsTypeZ zt + InKind zk -> extractLocalsTypeZ $ unfocusKind zk + InBind (BindCase zb) -> extractLocalsExprZ $ unfocusCaseBind zb globals = Map.assocs $ fmap defType defs M tyvars tmvars globs = locals <> M [] [] globals in (reverse tyvars, reverse tmvars, globs) -- keep most-global first generateNameExpr :: MonadReader Cxt m => - Either (Maybe (Type' ())) (Maybe (Kind' ())) -> - Either ExprZ TypeZ -> + Either (Maybe (Type' () ())) (Maybe (Kind' ())) -> + Loc -> m [Name] --- NB: it makes perfect sense to ask for a type variable (first Either is Right) --- in a term context (second Either is Left): we could be inserting a LAM. +-- NB: it makes perfect sense to ask for a type variable (Either is Right) +-- in a term context (Loc is InExpr): we could be inserting a LAM. -- It doesn't make sense to ask for a term variable in a type context, -- but it also doesn't harm to support it. generateNameExpr tk z = uniquifyMany <$> getAvoidSet z <*> baseNames tk generateNameTy :: MonadReader Cxt m => - Either (Maybe (Type' ())) (Maybe (Kind' ())) -> - TypeZip -> + Either (Maybe (Type' () ())) (Maybe (Kind' ())) -> + Either TypeZip KindTZ -> m [Name] generateNameTy = generateNameTyAvoiding [] generateNameTyAvoiding :: MonadReader Cxt m => [Name] -> - Either (Maybe (Type' ())) (Maybe (Kind' ())) -> - TypeZip -> + Either (Maybe (Type' () ())) (Maybe (Kind' ())) -> + Either TypeZip KindTZ -> m [Name] -- It doesn't really make sense to ask for a term variable (Left) here, but -- it doesn't harm to support it generateNameTyAvoiding avoiding tk z = - uniquifyMany <$> ((Set.fromList avoiding <>) <$> mkAvoidForFreshNameTy z) <*> baseNames tk + uniquifyMany <$> ((Set.fromList avoiding <>) <$> getAvoidSetTy z) <*> baseNames tk baseNames :: MonadReader Cxt m => - Either (Maybe (Type' ())) (Maybe (Kind' ())) -> + Either (Maybe (Type' () ())) (Maybe (Kind' ())) -> m [Name] baseNames tk = do tys <- asks typeDefs @@ -132,10 +141,17 @@ baseNames tk = do where headCon = fmap fst . decomposeTAppCon -getAvoidSet :: MonadReader Cxt m => Either ExprZ TypeZ -> m (Set.Set Name) +getAvoidSet :: MonadReader Cxt m => Loc -> m (Set.Set Name) getAvoidSet = \case - Left ze -> mkAvoidForFreshName ze - Right zt -> mkAvoidForFreshNameTypeZ zt + InExpr ze -> mkAvoidForFreshName ze + InType zt -> mkAvoidForFreshNameTypeZ zt + InKind zk -> mkAvoidForFreshNameTypeZ $ unfocusKind zk + InBind (BindCase zb) -> mkAvoidForFreshName $ unfocusCaseBind zb + +getAvoidSetTy :: MonadReader Cxt m => Either TypeZip KindTZ -> m (Set.Set Name) +getAvoidSetTy = \case + Left zt -> mkAvoidForFreshNameTy zt + Right zk -> mkAvoidForFreshNameTy $ unfocusKindT zk -- | Adds a numeric suffix to a name to be distinct from a given set. -- (If the name is already distinct then return it unmodified.) diff --git a/primer/src/Primer/Refine.hs b/primer/src/Primer/Refine.hs index 95ae69672..21de24bda 100644 --- a/primer/src/Primer/Refine.hs +++ b/primer/src/Primer/Refine.hs @@ -13,7 +13,8 @@ import Primer.Subst (substTy, substTySimul) import Primer.Typecheck.Cxt (Cxt) import Primer.Typecheck.Kindcheck qualified as TC import Primer.Unification (InternalUnifyError, unify) -import Primer.Zipper.Type (bindersBelowTy, focus) +import Primer.Zipper.Nested (focus) +import Primer.Zipper.Type (bindersBelowTy) data Inst = InstApp TC.Type diff --git a/primer/src/Primer/Subst.hs b/primer/src/Primer/Subst.hs index ebc30216f..ba5ea08ef 100644 --- a/primer/src/Primer/Subst.hs +++ b/primer/src/Primer/Subst.hs @@ -17,7 +17,7 @@ import Primer.Name (NameCounter) -- @substTySimul [(a,A),(b,B)] t@ is @t[A,B/a,b]@, where any references to @a,b@ -- in their replacements @A,B@ are not substituted. -- We restrict to '()', i.e. no metadata as we don't want to duplicate IDs etc -substTySimul :: MonadFresh NameCounter m => Map TyVarName (Type' ()) -> Type' () -> m (Type' ()) +substTySimul :: MonadFresh NameCounter m => Map TyVarName (Type' () ()) -> Type' () () -> m (Type' () ()) substTySimul sub | M.null sub = pure | otherwise = go @@ -61,5 +61,5 @@ substTySimul sub -- | Simple and inefficient capture-avoiding substitution. -- @substTy n a t@ is @t[a/n]@ -- We restrict to '()', i.e. no metadata as we don't want to duplicate IDs etc -substTy :: MonadFresh NameCounter m => TyVarName -> Type' () -> Type' () -> m (Type' ()) +substTy :: MonadFresh NameCounter m => TyVarName -> Type' () () -> Type' () () -> m (Type' () ()) substTy n a = substTySimul $ M.singleton n a diff --git a/primer/src/Primer/TypeDef.hs b/primer/src/Primer/TypeDef.hs index 9a078e877..ecdcf6950 100644 --- a/primer/src/Primer/TypeDef.hs +++ b/primer/src/Primer/TypeDef.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE OverloadedLabels #-} - module Primer.TypeDef ( TypeDef (..), ValCon (..), @@ -11,7 +9,6 @@ module Primer.TypeDef ( ASTTypeDef (..), PrimTypeDef (..), valConType, - _typedefFields, forgetTypeDefMetadata, generateTypeDefIDs, ) where @@ -20,7 +17,9 @@ import Foreword import Control.Monad.Fresh (MonadFresh) import Data.Data (Data) -import Optics (Field2 (_2), Traversal, over, traversalVL, traverseOf, traversed, (%)) +import Data.Generics.Product (HasParam (param), Param (StarParam)) +import Optics (set, traverseOf) +import Primer.Core.DSL.Meta (kmeta, meta) import Primer.Core.Meta ( ID, TyConName, @@ -34,7 +33,7 @@ import Primer.Core.Type ( Type' (TForall, TFun, TVar), TypeMeta, ) -import Primer.Core.Utils (forgetKindMetadata, forgetTypeMetadata, generateKindIDs, generateTypeIDs) +import Primer.Core.Utils (forgetTypeMetadata) import Primer.JSON ( CustomJSON (CustomJSON), FromJSON, @@ -69,22 +68,22 @@ data PrimTypeDef c = PrimTypeDef -- The type of the constructor is C :: forall a:TYPE. forall b:(TYPE->TYPE). b a -> Nat -> T a b data ASTTypeDef b c = ASTTypeDef { astTypeDefParameters :: [(TyVarName, Kind' c)] -- These names scope over the constructors - , astTypeDefConstructors :: [ValCon b] + , astTypeDefConstructors :: [ValCon b c] , astTypeDefNameHints :: [Name] } deriving stock (Eq, Show, Read, Data, Generic) deriving (FromJSON, ToJSON) via PrimerJSON (ASTTypeDef b c) deriving anyclass (NFData) -data ValCon b = ValCon +data ValCon b c = ValCon { valConName :: ValConName - , valConArgs :: [Type' b] + , valConArgs :: [Type' b c] } deriving stock (Eq, Show, Read, Data, Generic) - deriving (FromJSON, ToJSON) via PrimerJSON (ValCon b) + deriving (FromJSON, ToJSON) via PrimerJSON (ValCon b c) deriving anyclass (NFData) -valConType :: TyConName -> ASTTypeDef () () -> ValCon () -> Type' () +valConType :: TyConName -> ASTTypeDef () () -> ValCon () () -> Type' () () valConType tc td vc = let ret = mkTAppCon tc (TVar () . fst <$> astTypeDefParameters td) args = foldr (TFun () . forgetTypeMetadata) ret (valConArgs vc) @@ -106,26 +105,12 @@ typeDefAST = \case typeDefKind :: TypeDef b () -> Kind' () typeDefKind = foldr (KFun () . snd) (KType ()) . typeDefParameters --- | A traversal over the contstructor fields in an typedef. -_typedefFields :: Traversal (TypeDef b c) (TypeDef b' c) (Type' b) (Type' b') -_typedefFields = - #_TypeDefAST - % #astTypeDefConstructors - % traversed - % #valConArgs - % traversed - -_typedefParamKinds :: Traversal (TypeDef b c) (TypeDef b c') (Kind' c) (Kind' c') -_typedefParamKinds = traversalVL $ \f -> \case - TypeDefPrim td -> TypeDefPrim <$> traverseOf (#primTypeDefParameters % traversed % _2) f td - TypeDefAST td -> TypeDefAST <$> traverseOf (#astTypeDefParameters % traversed % _2) f td - forgetTypeDefMetadata :: TypeDef b c -> TypeDef () () forgetTypeDefMetadata = - over _typedefFields forgetTypeMetadata - . over _typedefParamKinds forgetKindMetadata + set (param @1) () + . set (param @0) () generateTypeDefIDs :: MonadFresh ID m => TypeDef () () -> m (TypeDef TypeMeta KindMeta) generateTypeDefIDs = - traverseOf _typedefFields generateTypeIDs - <=< traverseOf _typedefParamKinds generateKindIDs + traverseOf (param @1) (\() -> meta) + <=< traverseOf (param @0) (\() -> kmeta) diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index d9a5afaaa..2f49f564e 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -218,7 +218,7 @@ import Primer.Typecheck.Utils ( -- synthesised type, not the checked one. For example, when checking that -- @Int -> ?@ accepts @\x . x@, we record that the variable node has type -- @Int@, rather than @?@. -type ExprT = Expr' (Meta TypeCache) (Meta (Kind' ())) +type ExprT = Expr' (Meta TypeCache) (Meta (Kind' ())) (Meta ()) assert :: MonadNestedError TypeError e m => Bool -> Text -> m () assert b s = unless b $ throwError' (InternalError s) @@ -381,7 +381,7 @@ checkTypeDefs tds = do local (extendLocalCxtTys params) $ traverseOf astTypeDefConArgs (checkKind' (KType ())) td -astTypeDefConArgs :: Traversal (ASTTypeDef a c) (ASTTypeDef b c) (Type' a) (Type' b) +astTypeDefConArgs :: Traversal (ASTTypeDef a c) (ASTTypeDef b c) (Type' a c) (Type' b c) astTypeDefConArgs = #astTypeDefConstructors % traversed % #valConArgs % traversed distinct :: Ord a => [a] -> Bool @@ -848,7 +848,7 @@ isSorted :: Ord a => [a] -> Bool isSorted [] = True isSorted xxs@(_ : xs) = and $ zipWith (<=) xxs xs -addChkMetaT :: Type' () -> ExprT -> ExprT +addChkMetaT :: Type' () () -> ExprT -> ExprT addChkMetaT = addChkMeta' equality -- NB: recurse over Let{,rec,Type}, as these have different typing @@ -856,7 +856,7 @@ addChkMetaT = addChkMeta' equality -- currently have a typing rule, but only because it is awkward to -- nicely handle the type equality it introduces -- it will be roughly -- the same as Let when it is implemented) -addChkMeta' :: Is k A_Setter => Optic' k NoIx a TypeCache -> Type' () -> Expr' (Meta a) b -> Expr' (Meta a) b +addChkMeta' :: Is k A_Setter => Optic' k NoIx a TypeCache -> Type' () () -> Expr' (Meta a) b c -> Expr' (Meta a) b c addChkMeta' set t e = let e' = case e of Let m v s b -> Let m v s $ addChkMeta' set t b @@ -880,11 +880,11 @@ addChkMeta' set t e = -- initially had typecaches @TCChkedAt (Bool -> Int)@ on @e@ and @TCChkedAt Int@ -- on @e'@, then we would return @{? λx.e' ?}@ where the @e'@ still has its -- typecache, but that is wrong for its anticipated new context. -enholeT :: MonadFresh ID m => Type' () -> ExprT -> m ExprT +enholeT :: MonadFresh ID m => Type' () () -> ExprT -> m ExprT enholeT = enhole' equality -- | A generic helper for 'enholeT' and (a hypothetical) @enhole = enhole' _Just@ -enhole' :: (Is k A_Prism, MonadFresh ID m) => Optic' k NoIx a TypeCache -> Type' () -> Expr' (Meta a) b -> m (Expr' (Meta a) b) +enhole' :: (Is k A_Prism, MonadFresh ID m) => Optic' k NoIx a TypeCache -> Type' () () -> Expr' (Meta a) b c -> m (Expr' (Meta a) b c) enhole' p' t e = let p = castOptic @A_Prism p' in Hole @@ -898,9 +898,9 @@ checkBranch :: forall e m. TypeM e m => Type -> - (ValConName, [Type' ()]) -> -- The constructor and its instantiated parameter types - CaseBranch' ExprMeta TypeMeta -> - m (CaseBranch' (Meta TypeCache) (Meta (Kind' ()))) + (ValConName, [Type' () ()]) -> -- The constructor and its instantiated parameter types + CaseBranch' ExprMeta TypeMeta KindMeta -> + m (CaseBranch' (Meta TypeCache) (Meta (Kind' ())) (Meta ())) checkBranch t (vc, args) (CaseBranch nb patterns rhs) = do -- We check an invariant due to paranoia @@ -922,7 +922,7 @@ checkBranch t (vc, args) (CaseBranch nb patterns rhs) = rhs' <- local (extendLocalCxts (map (first bindName) fixedPats)) $ check t fixedRHS pure $ CaseBranch nb (map fst fixedPats) rhs' where - createBinding :: S.Set Name -> Type' () -> m (Bind' (Meta TypeCache), Type' ()) + createBinding :: S.Set Name -> Type' () () -> m (Bind' (Meta TypeCache), Type' () ()) createBinding namesInScope ty = do -- Avoid automatically generated names shadowing anything name <- freshLocalName' namesInScope @@ -980,7 +980,7 @@ consistentTypes x y = uncurry eqType $ holepunch x y holepunch s t = (s, t) -- | Compare two types for alpha equality, ignoring their IDs -eqType :: Type' a -> Type' b -> Bool +eqType :: Type' a c -> Type' b d -> Bool eqType t1 t2 = forgetTypeMetadata t1 `alphaEqTy` forgetTypeMetadata t2 -- | Convert @Expr (Meta Type) (Meta Kind)@ to @Expr (Meta (Maybe Type)) (Meta (Maybe Kind))@ @@ -988,8 +988,8 @@ exprTtoExpr :: ExprT -> Expr exprTtoExpr = over _exprTypeMeta (fmap Just) . over _exprMeta (fmap Just) -- | Convert @Type (Meta Kind)@ to @Type (Meta (Maybe Kind))@ -typeTtoType :: TypeT -> Type' TypeMeta +typeTtoType :: TypeT -> Type' TypeMeta KindMeta typeTtoType = over _typeMeta (fmap Just) -checkKind' :: TypeM e m => Kind' () -> Type' (Meta a) -> m TypeT +checkKind' :: TypeM e m => Kind' () -> Type' (Meta a) (Meta b) -> m TypeT checkKind' k t = modifyError' KindError (checkKind k t) diff --git a/primer/src/Primer/Typecheck/Cxt.hs b/primer/src/Primer/Typecheck/Cxt.hs index 9c9de9af8..41587903a 100644 --- a/primer/src/Primer/Typecheck/Cxt.hs +++ b/primer/src/Primer/Typecheck/Cxt.hs @@ -13,7 +13,7 @@ import Primer.Name (Name) import Primer.TypeDef (TypeDefMap) import Primer.Typecheck.SmartHoles (SmartHoles) -type Type = Type' () +type Type = Type' () () type Kind = Kind' () diff --git a/primer/src/Primer/Typecheck/Kindcheck.hs b/primer/src/Primer/Typecheck/Kindcheck.hs index b628e83e0..f3a1832fb 100644 --- a/primer/src/Primer/Typecheck/Kindcheck.hs +++ b/primer/src/Primer/Typecheck/Kindcheck.hs @@ -19,12 +19,15 @@ import Foreword import Control.Monad.Fresh (MonadFresh) import Control.Monad.NestedError (MonadNestedError, throwError') import Data.Map qualified as Map +import Optics ((%), (.~)) import Primer.Core.DSL.Meta (meta') -import Primer.Core.Meta (ID, LocalName (LocalName), Meta (Meta), TyVarName, unLocalName) +import Primer.Core.Meta (ID, LocalName (LocalName), Meta (Meta), TyVarName, unLocalName, _type) import Primer.Core.Type ( Kind' (KFun, KHole, KType), Type' (TApp, TCon, TEmptyHole, TForall, TFun, THole, TLet, TVar), + _kindMeta, ) +import Primer.Core.Type.Utils (forgetKindMetadata) import Primer.Name (NameCounter) import Primer.TypeDef (typeDefKind) import Primer.Typecheck.Cxt (Cxt (localCxt, smartHoles, typeDefs), Kind, KindOrType (K, T), Type) @@ -50,7 +53,7 @@ type KindM e m = , MonadNestedError KindError e m -- can throw kind errors ) -type TypeT = Type' (Meta Kind) +type TypeT = Type' (Meta (Kind' ())) (Meta ()) lookupLocalTy :: TyVarName -> Cxt -> Either KindError Kind lookupLocalTy v cxt = case Map.lookup (unLocalName v) $ localCxt cxt of @@ -83,7 +86,7 @@ extendLocalCxtTys x cxt = cxt{localCxt = Map.fromList (bimap unLocalName K <$> x -- A similar thing would happen with -- synthKind $ TApp 0 (TCon 1 List) (THole 2 (TCon 3 List)) -- because we do not have checkKind KType List -synthKind :: KindM e m => Type' (Meta a) -> m (Kind, TypeT) +synthKind :: KindM e m => Type' (Meta a) (Meta b) -> m (Kind, TypeT) synthKind = \case TEmptyHole m -> pure (KHole (), TEmptyHole (annotate (KHole ()) m)) THole m t -> do @@ -126,11 +129,11 @@ synthKind = \case pure (KHole (), TApp (annotate (KHole ()) m) sWrap t') (Just (k1, k2), _) -> checkKind k1 t >>= \t' -> pure (k2, TApp (annotate k2 m) s' t') TForall m n k t -> do - t' <- local (extendLocalCxtTy (n, k)) $ checkKind (KType ()) t - pure (KType (), TForall (annotate (KType ()) m) n k t') + t' <- local (extendLocalCxtTy (n, forgetKindMetadata k)) $ checkKind (KType ()) t + pure (KType (), TForall (annotate (KType ()) m) n (k & _kindMeta % _type .~ ()) t') TLet{} -> throwError' TLetUnsupported -checkKind :: KindM e m => Kind -> Type' (Meta a) -> m TypeT +checkKind :: KindM e m => Kind -> Type' (Meta a) (Meta b) -> m TypeT checkKind k (THole m t) = do -- If we didn't have this special case, we might remove this hole (in a -- recursive call), only to reintroduce it again with a different ID diff --git a/primer/src/Primer/Typecheck/TypeError.hs b/primer/src/Primer/Typecheck/TypeError.hs index f4cfe3040..70e313ae1 100644 --- a/primer/src/Primer/Typecheck/TypeError.hs +++ b/primer/src/Primer/Typecheck/TypeError.hs @@ -15,7 +15,7 @@ data TypeError | TmVarWrongSort Name -- type var instead of term var | -- | Constructors (term-level) only inhabit fully-applied ADTs -- i.e. @Maybe a@, but not @Maybe@, @Maybe a b@, @Nat -> Bool@ or holes - ConstructorNotFullAppADT (Type' ()) ValConName + ConstructorNotFullAppADT (Type' () ()) ValConName | -- | This ADT does not have a constructor of that name ConstructorWrongADT TyConName ValConName | UnknownConstructor ValConName @@ -26,12 +26,12 @@ data TypeError -- in scope, or it is a student-defined type PrimitiveTypeNotInScope TyConName | CannotSynthesiseType Expr - | InconsistentTypes (Type' ()) (Type' ()) - | TypeDoesNotMatchArrow (Type' ()) - | TypeDoesNotMatchForall (Type' ()) + | InconsistentTypes (Type' () ()) (Type' () ()) + | TypeDoesNotMatchArrow (Type' () ()) + | TypeDoesNotMatchForall (Type' () ()) | CaseOfHoleNeedsEmptyBranches - | CannotCaseNonADT (Type' ()) - | CannotCaseNonSaturatedADT (Type' ()) + | CannotCaseNonADT (Type' () ()) + | CannotCaseNonSaturatedADT (Type' () ()) | -- | Either wrong number, wrong constructors or wrong order. The fields are @name of the ADT@, @branches given@, @wildcard/fallback branch given@ WrongCaseBranches TyConName [Pattern] Bool | CaseBranchWrongNumberPatterns diff --git a/primer/src/Primer/Typecheck/Utils.hs b/primer/src/Primer/Typecheck/Utils.hs index 212f49b13..6508465e6 100644 --- a/primer/src/Primer/Typecheck/Utils.hs +++ b/primer/src/Primer/Typecheck/Utils.hs @@ -46,14 +46,14 @@ import Primer.Typecheck.Cxt (Cxt, Kind, globalCxt, typeDefs) -- | Given a 'TypeDefMap', for each value constructor of a -- non-primitive typedef in the map, tuple the value constructor up -- with its type constructor name and its corresponding AST. -allNonPrimValCons :: TypeDefMap -> [(ValCon (), TyConName, ASTTypeDef () ())] +allNonPrimValCons :: TypeDefMap -> [(ValCon () (), TyConName, ASTTypeDef () ())] allNonPrimValCons tydefs = do (tc, TypeDefAST td) <- M.assocs tydefs vc <- astTypeDefConstructors td pure (vc, tc, td) -- We assume that constructor names are unique, returning the first one we find -lookupConstructor :: TypeDefMap -> ValConName -> Maybe (ValCon (), TyConName, ASTTypeDef () ()) +lookupConstructor :: TypeDefMap -> ValConName -> Maybe (ValCon () (), TyConName, ASTTypeDef () ()) lookupConstructor tyDefs c = find ((== c) . valConName . fst3) $ allNonPrimValCons tyDefs data TypeDefError @@ -63,12 +63,12 @@ data TypeDefError | TDIUnknown TyConName -- not in scope | TDINotSaturated -- e.g. @List@ or @List a b@ rather than @List a@ -data TypeDefInfo a = TypeDefInfo [Type' a] TyConName (TypeDef () ()) -- instantiated parameters, and the typedef (with its name), i.e. [Int] are the parameters for @List Int@ +data TypeDefInfo a b = TypeDefInfo [Type' a b] TyConName (TypeDef () ()) -- instantiated parameters, and the typedef (with its name), i.e. [Int] are the parameters for @List Int@ -getTypeDefInfo :: MonadReader Cxt m => Type' a -> m (Either TypeDefError (TypeDefInfo a)) +getTypeDefInfo :: MonadReader Cxt m => Type' a b -> m (Either TypeDefError (TypeDefInfo a b)) getTypeDefInfo t = reader $ flip getTypeDefInfo' t . typeDefs -getTypeDefInfo' :: TypeDefMap -> Type' a -> Either TypeDefError (TypeDefInfo a) +getTypeDefInfo' :: TypeDefMap -> Type' a b -> Either TypeDefError (TypeDefInfo a b) getTypeDefInfo' _ (TEmptyHole _) = Left TDIHoleType getTypeDefInfo' _ (THole _ _) = Left TDIHoleType getTypeDefInfo' tydefs ty = @@ -89,8 +89,8 @@ getTypeDefInfo' tydefs ty = -- (e.g. @Nil : List Nat ; Cons : Nat -> List Nat -> List Nat@) instantiateValCons :: (MonadFresh NameCounter m, MonadReader Cxt m) => - Type' () -> - m (Either TypeDefError (TyConName, ASTTypeDef () (), [(ValConName, [Type' ()])])) + Type' () () -> + m (Either TypeDefError (TyConName, ASTTypeDef () (), [(ValConName, [Type' () ()])])) instantiateValCons t = do tds <- asks typeDefs let instCons = instantiateValCons' tds t @@ -113,15 +113,15 @@ instantiateValCons t = do -- context into an argument instantiateValCons' :: TypeDefMap -> - Type' () -> - Either TypeDefError (TyConName, ASTTypeDef () (), [(ValConName, forall m. MonadFresh NameCounter m => [m (Type' ())])]) + Type' () () -> + Either TypeDefError (TyConName, ASTTypeDef () (), [(ValConName, forall m. MonadFresh NameCounter m => [m (Type' () ())])]) instantiateValCons' tyDefs t = getTypeDefInfo' tyDefs t >>= \(TypeDefInfo params tc def) -> case def of TypeDefPrim _ -> Left $ TDIPrim tc TypeDefAST tda -> do let defparams = map fst $ astTypeDefParameters tda - f :: ValCon () -> (ValConName, forall m. MonadFresh NameCounter m => [m (Type' ())]) + f :: ValCon () () -> (ValConName, forall m. MonadFresh NameCounter m => [m (Type' () ())]) -- eta expand to deal with shallow subsumption {- HLINT ignore instantiateValCons' "Avoid lambda" -} f c = (valConName c, map (\a -> substTySimul (M.fromList $ zip defparams params) (forgetTypeMetadata a)) $ valConArgs c) @@ -132,11 +132,11 @@ maybeTypeOf :: Expr -> Maybe TypeCache maybeTypeOf = view _typecache -- | A lens for the type annotation of an 'Expr' or 'ExprT' -_typecache :: Lens' (Expr' (Meta a) b) a +_typecache :: Lens' (Expr' (Meta a) b c) a _typecache = _exprMetaLens % _type -- | Get the type of an 'ExprT' -typeOf :: Expr' (Meta TypeCache) (Meta Kind) -> TypeCache +typeOf :: Expr' (Meta TypeCache) (Meta Kind) (Meta ()) -> TypeCache typeOf = view _typecache -- Helper to create fresh names diff --git a/primer/src/Primer/Unification.hs b/primer/src/Primer/Unification.hs index c4b90d202..f3ab5856f 100644 --- a/primer/src/Primer/Unification.hs +++ b/primer/src/Primer/Unification.hs @@ -13,6 +13,7 @@ import Primer.Core.Meta ( ) import Primer.Core.Type ( Type' (TApp, TCon, TEmptyHole, TForall, TFun, THole, TVar), + _typeKindMeta, _typeMeta, ) import Primer.Core.Type.Utils (_freeVarsTy) @@ -77,7 +78,7 @@ unify cxt unificationVars s t = do -- checkKind succeeded, and not the result. Thus we just add some dummy -- ones. -- TODO: this is a bit of a code smell! - let addPointlessMeta = set _typeMeta $ trivialMeta 0 + let addPointlessMeta = set _typeKindMeta (trivialMeta 0) . set _typeMeta (trivialMeta 0) let f v vt = case lookupLocalTy v cxt of Right k -> All . isRight <$> runExceptT @KindError (runReaderT (checkKind k $ addPointlessMeta vt) (cxt{smartHoles = NoSmartHoles})) -- this catchall should never happen: sb should only contain diff --git a/primer/src/Primer/Zipper.hs b/primer/src/Primer/Zipper.hs index 085059881..ce3874fcb 100644 --- a/primer/src/Primer/Zipper.hs +++ b/primer/src/Primer/Zipper.hs @@ -6,18 +6,25 @@ module Primer.Zipper ( ExprZ, TypeZip, TypeZ, + KindZ, + KindTZ, CaseBindZ, updateCaseBind, unfocusCaseBind, caseBindZFocus, + caseBindZMeta, IsZipper (asZipper), Loc, Loc' (..), BindLoc, BindLoc' (..), focusType, + focusKind, focusLoc, unfocusType, + unfocusKind, + unfocusKindT, + focusOnlyKind, focusOnlyType, focus, unfocus, @@ -41,7 +48,6 @@ module Primer.Zipper ( foldBelow, unfocusExpr, unfocusLoc, - locToEither, bindersAbove, bindersBelow, LetBinding' (..), @@ -60,7 +66,7 @@ module Primer.Zipper ( bindersBelowTy, SomeNode (..), findNodeWithParent, - findType, + findTypeOrKind, ) where import Foreword @@ -103,63 +109,78 @@ import Primer.Core ( ExprMeta, HasID (..), ID, + Kind, + Kind', + KindMeta, LVarName, LocalName (unLocalName), Type, - Type' (), + Type' (TForall), TypeMeta, bindName, getID, typesInExpr, + _bindMeta, ) import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON) import Primer.Name (Name) +import Primer.Zipper.Nested ( + IsZipper (..), + ZipNest (ZipNest), + down, + focus, + innerZipNest, + left, + mergeNest, + replace, + right, + target, + top, + unfocusNest, + up, + _target, + ) import Primer.Zipper.Type ( FoldAbove, FoldAbove' (..), - IsZipper (..), + KindTZ, + KindTZ', LetTypeBinding' (LetTypeBind), TypeZip, TypeZip', bindersAboveTy, bindersBelowTy, - down, farthest, - focus, focusOnKind, focusOnTy, + focusOnTy', foldAbove, foldBelow, getBoundHereDnTy, getBoundHereTy, getBoundHereUpTy, - left, - replace, - right, search, - target, - top, - up, - _target, + unfocusKindT, ) -type ExprZ' a b = Zipper (Expr' a b) (Expr' a b) +type ExprZ' a b c = Zipper (Expr' a b c) (Expr' a b c) -- | An ordinary zipper for 'Expr's -type ExprZ = ExprZ' ExprMeta TypeMeta +type ExprZ = ExprZ' ExprMeta TypeMeta KindMeta -- | A zipper for 'Type's embedded in expressions. -- For such types, we need a way -- to navigate around them without losing our place in the wider expression. -- This type contains a Zipper for a 'Type' and a function that will place the -- unzippered type back into the wider expression zipper, keeping its place. -data TypeZ' a b = TypeZ (TypeZip' b) (Type' b -> ExprZ' a b) - deriving stock (Generic) +type TypeZ' a b c = ZipNest (ExprZ' a b c) (TypeZip' b c) (Type' b c) -type TypeZ = TypeZ' ExprMeta TypeMeta +type TypeZ = TypeZ' ExprMeta TypeMeta KindMeta -instance HasID b => HasID (TypeZ' a b) where - _id = position @1 % _id +-- | A zipper for 'Kind's embedded in expressions (which will always be inside a 'Type'). +type KindZ' a b c = ZipNest (ExprZ' a b c) (KindTZ' b c) (Type' b c) + +type KindZ = KindZ' ExprMeta TypeMeta KindMeta -- | A zipper for variable bindings in case branches. -- This type focuses on a particular binding in a particular branch. @@ -169,21 +190,21 @@ instance HasID b => HasID (TypeZ' a b) where -- simultaneously, yielding a new expression. -- These fields are chosen to be convenient for renaming, and they may not be that useful for future -- actions we want to perform. -data CaseBindZ' a b = CaseBindZ - { caseBindZExpr :: ExprZ' a b +data CaseBindZ' a b c = CaseBindZ + { caseBindZExpr :: ExprZ' a b c -- ^ a zipper focused on the case expression , caseBindZFocus :: Bind' a -- ^ the focused binding - , caseBindZRhs :: Expr' a b + , caseBindZRhs :: Expr' a b c -- ^ the rhs of the branch , caseBindAllBindings :: [Bind' a] -- ^ all other bindings in the case branch, i.e. all except the focused one - , caseBindZUpdate :: Bind' a -> Expr' a b -> ExprZ' a b -> ExprZ' a b + , caseBindZUpdate :: Bind' a -> Expr' a b c -> ExprZ' a b c -> ExprZ' a b c -- ^ a function to update the focused binding and rhs simultaneously } deriving stock (Generic) -type CaseBindZ = CaseBindZ' ExprMeta TypeMeta +type CaseBindZ = CaseBindZ' ExprMeta TypeMeta KindMeta -- Apply an update function to the focus of a case binding, optionally modifying the rhs of the branch too. -- The update function is given three arguments: @@ -204,64 +225,87 @@ updateCaseBind (CaseBindZ z bind rhs bindings update) f = let z' = update bind' rhs' z in CaseBindZ z' bind' rhs' bindings update -instance HasID a => HasID (CaseBindZ' a b) where +instance HasID a => HasID (CaseBindZ' a b c) where _id = #caseBindZFocus % _id +caseBindZMeta :: Lens' (CaseBindZ' a b c) a +caseBindZMeta = #caseBindZFocus % _bindMeta + -- | A specific location in our AST. -- This can either be in an expression, type, or binding. -data Loc' a b +data Loc' a b c = -- | An expression - InExpr (ExprZ' a b) + InExpr (ExprZ' a b c) | -- | A type - InType (TypeZ' a b) + InType (TypeZ' a b c) + | -- | A kind + InKind (KindZ' a b c) | -- | A binding (currently just case bindings) - InBind (BindLoc' a b) + InBind (BindLoc' a b c) deriving stock (Generic) -type Loc = Loc' ExprMeta TypeMeta +type Loc = Loc' ExprMeta TypeMeta KindMeta -instance (HasID a, HasID b) => HasID (Loc' a b) where +instance (HasID a, HasID b, HasID c) => HasID (Loc' a b c) where _id = lens getter setter where getter = \case InExpr e -> view _id e InType l -> view _id l + InKind k -> view _id k InBind l -> view _id l setter l i = case l of InExpr e -> InExpr $ set _id i e InType t -> InType $ set _id i t + InKind k -> InKind $ set _id i k InBind t -> InBind $ set _id i t -- | A location of a binding. -- This only covers bindings in case branches for now. {- HLINT ignore BindLoc' "Use newtype instead of data" -} -data BindLoc' a b - = BindCase (CaseBindZ' a b) +data BindLoc' a b c + = BindCase (CaseBindZ' a b c) deriving stock (Generic) type BindLoc = BindLoc' ExprMeta TypeMeta -instance HasID a => HasID (BindLoc' a b) where +instance HasID a => HasID (BindLoc' a b c) where _id = position @1 % _id -- | Switch from an 'Expr' zipper to a 'Type' zipper, focusing on the type in -- the current target. This expects that the target is an @Ann@, @App@, -- @Letrec@ or @LetType@ node (as those are the only ones that contain a -- @Type@). -focusType :: (Data a, Data b) => ExprZ' a b -> Maybe (TypeZ' a b) +focusType :: (Data a, Data b, Data c) => ExprZ' a b c -> Maybe (TypeZ' a b c) focusType z = case target z of Con{} -> Nothing _ -> do t <- z ^? singular l - pure $ TypeZ (zipper t) $ \t' -> z & l .~ t' + pure $ ZipNest (zipper t) $ \t' -> z & l .~ t' where l = _target % typesInExpr +-- | Switch from an 'Type' zipper to a 'Kind' zipper, focusing on the kind in +-- the current target. This expects that the target is an @TForall@ node +-- (as this is the only one that contain a @Kind@). +focusKind :: (Data b, Data c) => TypeZ' a b c -> Maybe (KindZ' a b c) +focusKind (ZipNest z f) = case target z of + TForall m n k t -> + pure $ + ZipNest + ( ZipNest + (focus k) + $ \k' -> replace (TForall m n k' t) z + ) + f + -- pure $ ZipNest (zipper t) $ \t' -> z & l .~ t' + _ -> Nothing + -- | If the currently focused expression is a case expression, search the bindings of its branches -- to find one matching the given ID, and return the 'Loc' for that binding. -- If no match is found, return @Nothing@. -findInCaseBinds :: forall a b. (Data a, Data b, Eq a, HasID a) => ID -> ExprZ' a b -> Maybe (Loc' a b) +findInCaseBinds :: forall a b c. (Data a, Data b, Data c, Eq a, HasID a) => ID -> ExprZ' a b c -> Maybe (Loc' a b c) findInCaseBinds i z = do branches <- preview branchesLens z ((branchIx, bindIx), bind) <- branches & iheadOf (ifolded % binds <%> ifolded <% filteredBy (_id % only i)) @@ -273,23 +317,28 @@ findInCaseBinds i z = do let update bind' rhs' = set rhsLens rhs' . set bindLens bind' pure $ InBind $ BindCase $ CaseBindZ z bind rhs (delete bind allBinds) update where - branchesLens :: AffineTraversal' (ExprZ' a b) [CaseBranch' a b] + branchesLens :: AffineTraversal' (ExprZ' a b c) [CaseBranch' a b c] branchesLens = _target % #_Case % _3 - binds :: Lens' (CaseBranch' a b) [Bind' a] + binds :: Lens' (CaseBranch' a b c) [Bind' a] binds = position @2 - branchRHS :: Lens' (CaseBranch' a b) (Expr' a b) + branchRHS :: Lens' (CaseBranch' a b c) (Expr' a b c) branchRHS = position @3 -- | Switch from a 'Type' zipper back to an 'Expr' zipper. -unfocusType :: TypeZ' a b -> ExprZ' a b -unfocusType (TypeZ zt f) = f (fromZipper zt) +unfocusType :: (Data b, Data c) => TypeZ' a b c -> ExprZ' a b c +unfocusType = unfocusNest + +-- | Switch from a 'Kind'-in-'Type'-in-'Expr' zipper back to an 'Type'-in-'Expr' zipper. +unfocusKind :: Data c => KindZ' a b c -> TypeZ' a b c +unfocusKind = mergeNest -- | Forget the surrounding expression context -focusOnlyType :: TypeZ' a b -> TypeZip' b -focusOnlyType (TypeZ zt _) = zt +focusOnlyType :: TypeZ' a b c -> TypeZip' b c +focusOnlyType = innerZipNest -instance Data b => IsZipper (TypeZ' a b) (Type' b) where - asZipper = position @1 +-- | Forget the surrounding expression context +focusOnlyKind :: KindZ' a b c -> KindTZ' b c +focusOnlyKind = innerZipNest -- 'CaseBindZ' is sort of a fake zipper which can only focus on one thing: the case binding. -- It's a bit fiddly to make it appear as a zipper like this, but it's convenient to have a @@ -302,28 +351,20 @@ focusLoc :: Expr -> Loc focusLoc = InExpr . focus -- Convert a 'CaseBindZ' to an 'ExprZ' by shifting focus to the parent case expression. -unfocusCaseBind :: CaseBindZ' a b -> ExprZ' a b +unfocusCaseBind :: CaseBindZ' a b c -> ExprZ' a b c unfocusCaseBind = caseBindZExpr -- | Convert an 'Expr' zipper to an 'Expr' -unfocusExpr :: ExprZ' a b -> Expr' a b +unfocusExpr :: ExprZ' a b c -> Expr' a b c unfocusExpr = fromZipper -- | Convert a 'Loc' to an 'ExprZ'. --- If we're in a type or case binding, we'll shift focus up to the nearest enclosing expression. +-- If we're in a type or kind or case binding, we'll shift focus up to the nearest enclosing expression. unfocusLoc :: Loc -> ExprZ unfocusLoc (InExpr z) = z unfocusLoc (InType z) = unfocusType z unfocusLoc (InBind (BindCase z)) = unfocusCaseBind z - --- | Convert a 'Loc' to 'Either ExprZ TypeZ'. --- If the 'Loc' is in a case bind, we shift focus to the parent case expression. --- This function is mainly to keep compatibility with code which still expects 'Either ExprZ TypeZ' --- as a representation of an AST location. -locToEither :: Loc' a b -> Either (ExprZ' a b) (TypeZ' a b) -locToEither (InBind (BindCase z)) = Left $ unfocusCaseBind z -locToEither (InExpr z) = Left z -locToEither (InType z) = Right z +unfocusLoc (InKind k) = unfocusType $ unfocusKind k -- | Convert a 'Loc' to an 'Expr'. -- This shifts focus right up to the top, so the result is the whole expression. @@ -331,11 +372,11 @@ unfocus :: Loc -> Expr unfocus = unfocusExpr . unfocusLoc -- | Focus on the node with the given 'ID', if it exists in the expression -focusOn :: (Data a, Data b, Eq a, HasID a, HasID b) => ID -> Expr' a b -> Maybe (Loc' a b) +focusOn :: (Data a, Data b, Data c, Eq a, HasID a, HasID b, HasID c) => ID -> Expr' a b c -> Maybe (Loc' a b c) focusOn i = focusOn' i . focus -- | Focus on the node with the given 'ID', if it exists in the focussed expression -focusOn' :: (Data a, Data b, Eq a, HasID a, HasID b) => ID -> ExprZ' a b -> Maybe (Loc' a b) +focusOn' :: (Data a, Data b, Data c, Eq a, HasID a, HasID b, HasID c) => ID -> ExprZ' a b c -> Maybe (Loc' a b c) focusOn' i = fmap snd . search matchesID where matchesID z @@ -344,7 +385,11 @@ focusOn' i = fmap snd . search matchesID -- If the target has an embedded type, search the type for a match. -- If the target is a case expression with bindings, search each binding for a match. | otherwise = - let inType = focusType z >>= search (guarded (== i) . getID . target) <&> InType . fst + let inType = do + ZipNest tz f <- focusType z + focusOnTy' i tz <&> \case + Left tz' -> InType $ ZipNest tz' f + Right kz -> InKind (ZipNest kz f) inCaseBinds = findInCaseBinds i z in inType <|> inCaseBinds @@ -353,11 +398,11 @@ bindersAbove :: ExprZ -> S.Set Name bindersAbove = foldAbove getBoundHereUp foldAboveTypeZ :: - (Data a, Data b, Monoid m) => - (FoldAbove (Type' b) -> m) -> - (FoldAbove' (Type' b) (Expr' a b) -> m) -> - (FoldAbove (Expr' a b) -> m) -> - TypeZ' a b -> + (Data a, Data b, Data c, Monoid m) => + (FoldAbove (Type' b c) -> m) -> + (FoldAbove' (Type' b c) (Expr' a b c) -> m) -> + (FoldAbove (Expr' a b c) -> m) -> + TypeZ' a b c -> m foldAboveTypeZ inTy border inExpr tz = let tyz = focusOnlyType tz @@ -378,7 +423,7 @@ bindersAboveTypeZ = getBoundHereUp -- Get the names bound by this layer of an expression for a given child. -getBoundHereUp :: (Eq a, Eq b) => FoldAbove (Expr' a b) -> S.Set Name +getBoundHereUp :: (Eq a, Eq b, Eq c) => FoldAbove (Expr' a b c) -> S.Set Name getBoundHereUp e = getBoundHere (current e) (Just $ prior e) -- Get the names bound within the focussed subtree @@ -387,30 +432,30 @@ bindersBelow = foldBelow getBoundHereDn -- Get all names bound by this layer of an expression, for any child. -- E.g. for a "match" we get all vars bound by each branch. -getBoundHereDn :: (Eq a, Eq b) => Expr' a b -> S.Set Name +getBoundHereDn :: (Eq a, Eq b, Eq c) => Expr' a b c -> S.Set Name getBoundHereDn e = getBoundHere e Nothing -- Get the names bound by this layer of an expression (both term and type names) -- The second arg is the child we just came out of, if traversing up (and thus -- need to extract binders based on which case branch etc), and Nothing if -- traversing down (and want to get all binders regardless of branch). -getBoundHere :: (Eq a, Eq b) => Expr' a b -> Maybe (Expr' a b) -> S.Set Name +getBoundHere :: (Eq a, Eq b, Eq c) => Expr' a b c -> Maybe (Expr' a b c) -> S.Set Name getBoundHere e prev = S.fromList $ either identity letBindingName <$> getBoundHere' e prev -data LetBinding' a b - = LetBind LVarName (Expr' a b) - | LetrecBind LVarName (Expr' a b) (Type' b) - | LetTyBind (LetTypeBinding' b) +data LetBinding' a b c + = LetBind LVarName (Expr' a b c) + | LetrecBind LVarName (Expr' a b c) (Type' b c) + | LetTyBind (LetTypeBinding' b c) deriving stock (Eq, Show) -type LetBinding = LetBinding' ExprMeta TypeMeta +type LetBinding = LetBinding' ExprMeta TypeMeta KindMeta -letBindingName :: LetBinding' a b -> Name +letBindingName :: LetBinding' a b c -> Name letBindingName = \case LetBind n _ -> unLocalName n LetrecBind n _ _ -> unLocalName n LetTyBind (LetTypeBind n _) -> unLocalName n -getBoundHere' :: (Eq a, Eq b) => Expr' a b -> Maybe (Expr' a b) -> [Either Name (LetBinding' a b)] +getBoundHere' :: (Eq a, Eq b, Eq c) => Expr' a b c -> Maybe (Expr' a b c) -> [Either Name (LetBinding' a b c)] getBoundHere' e prev = case e of Lam _ v _ -> anon v LAM _ tv _ -> anon tv @@ -447,16 +492,21 @@ findNodeWithParent id x = do (TypeNode . target) (up tz) ) + InKind kz -> + ( KindNode (target kz) + , Just $ maybe (TypeNode $ target $ unfocusKind kz) (KindNode . target) $ up kz + ) InBind (BindCase bz) -> (CaseBindNode $ caseBindZFocus bz, Just . ExprNode . target . unfocusCaseBind $ bz) --- | Find a sub-type in a larger type by its ID. -findType :: (Data a, HasID a) => ID -> Type' a -> Maybe (Type' a) -findType id ty = target <$> focusOnTy id ty +-- | Find a sub-type or kind in a larger type by its ID. +findTypeOrKind :: (Data a, HasID a, Data b, HasID b) => ID -> Type' a b -> Maybe (Either (Type' a b) (Kind' b)) +findTypeOrKind id ty = bimap target target <$> focusOnTy id ty -- | An AST node tagged with its "sort" - i.e. if it's a type or expression or binding etc. data SomeNode = ExprNode Expr | TypeNode Type + | KindNode Kind | -- | If/when we model all bindings with 'Bind'', we will want to generalise this. CaseBindNode Bind deriving stock (Eq, Show, Read, Generic) diff --git a/primer/src/Primer/Zipper/Nested.hs b/primer/src/Primer/Zipper/Nested.hs new file mode 100644 index 000000000..74b5fe592 --- /dev/null +++ b/primer/src/Primer/Zipper/Nested.hs @@ -0,0 +1,115 @@ +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Primer.Zipper.Nested ( + ZipNest (ZipNest), + unfocusNest, + mergeNest, + innerZipNest, + HasID (..), + IsZipper (..), + target, + _target, + up, + down, + left, + right, + top, + farthest, + focus, + unfocus, + replace, +) where + +import Foreword + +import Data.Data (Data) +import Data.Generics.Product (position) +import Data.Generics.Uniplate.Zipper ( + Zipper, + replaceHole, + zipper, + ) +import Data.Generics.Uniplate.Zipper qualified as Z +import Optics (Lens', equality', lens, over, traverseOf, view, (%)) +import Primer.Core.Meta ( + HasID (..), + ) + +-- | A zipper for @small@s embedded in @large@s. +-- We often have a type @large@, where some constructors contain a field +-- of type @small@, where both @large@ and @small@ have interesting +-- tree structure that we would like to navigate with a zipper. When +-- navigating around the nested @small@ we do not want to lose our place +-- in the wider expression. This type contains a Zipper for a @small@ +-- and a function that will place the unzippered @small@ back into the +-- wider @large@ zipper, keeping its place. +data ZipNest largeZip smallZip small = ZipNest smallZip (small -> largeZip) + deriving stock (Generic) + +instance HasID smallZip => HasID (ZipNest largeZip smallZip small) where + _id = position @1 % _id + +unfocusNest :: IsZipper smallZip small => ZipNest largeZip smallZip small -> largeZip +unfocusNest (ZipNest zs f) = f (unfocus zs) + +mergeNest :: + IsZipper smallZip small => + ZipNest largeZip (ZipNest mediumZip smallZip small) medium -> + ZipNest largeZip mediumZip medium +mergeNest (ZipNest (ZipNest z f) g) = ZipNest (f $ unfocus z) g + +innerZipNest :: ZipNest largeZip smallZip small -> smallZip +innerZipNest (ZipNest zs _) = zs + +-- | We want to use zipper-style up, down, left, right, etc. on various +-- 'Zipper's and 'ZipNest's, despite them being very different types. +-- This class enables that, by proxying each method through to the +-- underlying Zipper. @za@ is the user-facing type and @a@ is the +-- type of targets of the internal zipper. +class Data a => IsZipper za a | za -> a where + asZipper :: Lens' za (Z.Zipper a a) + +instance Data a => IsZipper (Z.Zipper a a) a where + asZipper = equality' + +target :: IsZipper za a => za -> a +target = Z.hole . view asZipper + +-- | A 'Lens' for the target of a zipper +_target :: IsZipper za a => Lens' za a +_target = lens target (flip replace) + +up :: IsZipper za a => za -> Maybe za +up = traverseOf asZipper Z.up + +down :: (IsZipper za a) => za -> Maybe za +down = traverseOf asZipper Z.down + +left :: IsZipper za a => za -> Maybe za +left = traverseOf asZipper Z.left + +right :: IsZipper za a => za -> Maybe za +right = traverseOf asZipper Z.right + +top :: IsZipper za a => za -> za +top = farthest up + +-- | Move the zipper focus as far in one direction as possible +farthest :: (a -> Maybe a) -> a -> a +farthest f = go where go a = maybe a go (f a) + +-- | Convert a normal 'Expr' or 'Type' to a cursored one, focusing on the root +focus :: (Data a) => a -> Zipper a a +focus = zipper + +-- | Forget the focus of a zipper, obtaining the "whole value" +unfocus :: IsZipper za a => za -> a +unfocus = Z.fromZipper . view asZipper + +-- | Replace the node at the cursor with the given value. +replace :: (IsZipper za a) => a -> za -> za +replace = over asZipper . replaceHole + +instance IsZipper smallZip elt => IsZipper (ZipNest largeZip smallZip small) elt where + asZipper = position @1 % asZipper diff --git a/primer/src/Primer/Zipper/Type.hs b/primer/src/Primer/Zipper/Type.hs index 32d9037fa..0d933e892 100644 --- a/primer/src/Primer/Zipper/Type.hs +++ b/primer/src/Primer/Zipper/Type.hs @@ -1,22 +1,17 @@ -{-# LANGUAGE FunctionalDependencies #-} - -- | This module contains the zipper type @TypeZ@, and functions for -- operating on them. module Primer.Zipper.Type ( TypeZip, TypeZip', - IsZipper (asZipper), - focus, - target, - _target, - replace, focusOnKind, + KindZip', + KindZip, + KindTZ', + KindTZ, + unfocusKindT, + focusOnlyKindT, focusOnTy, - top, - up, - down, - left, - right, + focusOnTy', farthest, search, FoldAbove, @@ -40,17 +35,8 @@ import Data.Data (Data) import Data.Generics.Uniplate.Data () import Data.Generics.Uniplate.Zipper ( Zipper, - replaceHole, - zipper, ) -import Data.Generics.Uniplate.Zipper qualified as Z import Data.Set qualified as S -import Optics ( - over, - view, - ) -import Optics.Lens (Lens', equality', lens) -import Optics.Traversal (traverseOf) import Primer.Core.Meta ( HasID (..), ID, @@ -60,58 +46,47 @@ import Primer.Core.Meta ( ) import Primer.Core.Type ( Kind', + KindMeta, Type' (TForall, TLet), TypeMeta, ) import Primer.Name (Name) +import Primer.Zipper.Nested ( + IsZipper, + ZipNest (ZipNest), + down, + focus, + innerZipNest, + left, + replace, + right, + target, + unfocusNest, + up, + ) type KindZip' c = Zipper (Kind' c) (Kind' c) -type TypeZip' b = Zipper (Type' b) (Type' b) - --- | An ordinary zipper for 'Type's -type TypeZip = TypeZip' TypeMeta - --- | We want to use up, down, left, right, etc. on 'ExprZ' and 'TypeZ', --- despite them being very different types. This class enables that, by proxying --- each method through to the underlying Zipper. --- @za@ is the user-facing type, i.e. 'ExprZ' or 'TypeZ'. --- @a@ is the type of targets of the internal zipper, i.e. 'Expr' or 'Type'. -class Data a => IsZipper za a | za -> a where - asZipper :: Lens' za (Z.Zipper a a) +-- | An ordinary zipper for 'Kind's +type KindZip = KindZip' KindMeta -instance Data a => IsZipper (Z.Zipper a a) a where - asZipper = equality' +type TypeZip' b c = Zipper (Type' b c) (Type' b c) -target :: IsZipper za a => za -> a -target = Z.hole . view asZipper - --- | A 'Lens' for the target of a zipper -_target :: IsZipper za a => Lens' za a -_target = lens target (flip replace) - -up :: IsZipper za a => za -> Maybe za -up = traverseOf asZipper Z.up - -down :: (IsZipper za a) => za -> Maybe za -down = traverseOf asZipper Z.down - -left :: IsZipper za a => za -> Maybe za -left = traverseOf asZipper Z.left +-- | An ordinary zipper for 'Type's +type TypeZip = TypeZip' TypeMeta KindMeta -right :: IsZipper za a => za -> Maybe za -right = traverseOf asZipper Z.right +-- | A zipper for kinds inside types +type KindTZ' b c = ZipNest (TypeZip' b c) (KindZip' c) (Kind' c) -top :: IsZipper za a => za -> za -top = farthest up +type KindTZ = KindTZ' TypeMeta KindMeta --- | Convert a normal 'Expr' or 'Type' to a cursored one, focusing on the root -focus :: (Data a) => a -> Zipper a a -focus = zipper +-- | Switch from a 'Kind'-in-'Type' zipper back to an 'Type' zipper. +unfocusKindT :: Data c => KindTZ' b c -> TypeZip' b c +unfocusKindT = unfocusNest --- | Replace the node at the cursor with the given value. -replace :: (IsZipper za a) => a -> za -> za -replace = over asZipper . replaceHole +-- | Forget the surrounding type context +focusOnlyKindT :: KindTZ' b c -> KindZip' c +focusOnlyKindT = innerZipNest -- | Focus on the node with the given 'ID', if it exists in the kind focusOnKind :: @@ -136,23 +111,28 @@ focusOnKind' i = fmap snd . search matchesID -- | Focus on the node with the given 'ID', if it exists in the type focusOnTy :: - (Data b, HasID b) => + (Data b, HasID b, Data c, HasID c) => ID -> - Type' b -> - Maybe (Zipper (Type' b) (Type' b)) + Type' b c -> + Maybe (Either (TypeZip' b c) (KindTZ' b c)) focusOnTy i = focusOnTy' i . focus -- | Focus on the node with the given 'ID', if it exists in the focussed type +-- Note that this may be (@Left@) a type or (@Right@) a kind (inside a 'TForall') focusOnTy' :: - (Data b, HasID b) => + (Data b, HasID b, Data c, HasID c) => ID -> - Zipper (Type' b) (Type' b) -> - Maybe (Zipper (Type' b) (Type' b)) + TypeZip' b c -> + Maybe (Either (TypeZip' b c) (KindTZ' b c)) focusOnTy' i = fmap snd . search matchesID where matchesID z -- If the current target has the correct ID, return that - | getID (target z) == i = Just z + | getID (target z) == i = Just $ Left z + -- If the current target has a nested kind, search that + | TForall m a k t <- target z = do + (zk, _) <- search (guarded (== i) . getID) (focus k) + pure $ Right $ ZipNest zk $ \k' -> replace (TForall m a k' t) z | otherwise = Nothing -- | Search for a node for which @f@ returns @Just@ something. @@ -203,28 +183,28 @@ bindersAboveTy = foldAbove getBoundHereUpTy -- Note that we have two specialisations we care about: -- bindersBelowTy :: TypeZip -> S.Set Name -- bindersBelowTy :: Zipper (Type' One) (Type' One) -> S.Set Name -bindersBelowTy :: (Data a, Eq a) => Zipper (Type' a) (Type' a) -> S.Set TyVarName +bindersBelowTy :: (Data a, Eq a, Data b, Eq b) => TypeZip' a b -> S.Set TyVarName bindersBelowTy = foldBelow getBoundHereDnTy -- Get the names bound by this layer of an type for a given child. -getBoundHereUpTy :: Eq a => FoldAbove (Type' a) -> S.Set TyVarName +getBoundHereUpTy :: (Eq a, Eq b) => FoldAbove (Type' a b) -> S.Set TyVarName getBoundHereUpTy e = getBoundHereTy (current e) (Just $ prior e) -- Get all names bound by this layer of an type, for any child. -getBoundHereDnTy :: Eq a => Type' a -> S.Set TyVarName +getBoundHereDnTy :: (Eq a, Eq b) => Type' a b -> S.Set TyVarName getBoundHereDnTy e = getBoundHereTy e Nothing -getBoundHereTy :: Eq a => Type' a -> Maybe (Type' a) -> S.Set TyVarName +getBoundHereTy :: (Eq a, Eq b) => Type' a b -> Maybe (Type' a b) -> S.Set TyVarName getBoundHereTy t prev = S.fromList $ either identity (\(LetTypeBind n _) -> n) <$> getBoundHereTy' t prev -data LetTypeBinding' a = LetTypeBind TyVarName (Type' a) +data LetTypeBinding' a b = LetTypeBind TyVarName (Type' a b) deriving stock (Eq, Show) -type LetTypeBinding = LetTypeBinding' TypeMeta +type LetTypeBinding = LetTypeBinding' TypeMeta KindMeta -letTypeBindingName :: LetTypeBinding' a -> Name +letTypeBindingName :: LetTypeBinding' a b -> Name letTypeBindingName (LetTypeBind n _) = unLocalName n -getBoundHereTy' :: Eq a => Type' a -> Maybe (Type' a) -> [Either TyVarName (LetTypeBinding' a)] +getBoundHereTy' :: (Eq a, Eq b) => Type' a b -> Maybe (Type' a b) -> [Either TyVarName (LetTypeBinding' a b)] getBoundHereTy' t prev = case t of TForall _ v _ _ -> [Left v] TLet _ v rhs b -> diff --git a/primer/src/Primer/ZipperCxt.hs b/primer/src/Primer/ZipperCxt.hs index 9da655bdd..a29fcf6f9 100644 --- a/primer/src/Primer/ZipperCxt.hs +++ b/primer/src/Primer/ZipperCxt.hs @@ -30,11 +30,12 @@ import Primer.Core ( _type, _typeMetaLens, ) -import Primer.Core.Utils (forgetTypeMetadata) +import Primer.Core.Utils (forgetKindMetadata, forgetTypeMetadata) import Primer.Typecheck.Utils (maybeTypeOf) import Primer.Zipper ( ExprZ, FoldAbove, + KindTZ, TypeZ, TypeZip, asZipper, @@ -43,6 +44,7 @@ import Primer.Zipper ( prior, unfocusType, ) +import Primer.Zipper.Nested (unfocusNest) -- Helper for variablesInScopeExpr: collect variables, most local first, -- eliding shadowed variables @@ -54,9 +56,9 @@ data ShadowedVarsExpr -- | Local type variables [(TyVarName, Kind' ())] -- | Local term variables - [(LVarName, Type' ())] + [(LVarName, Type' () ())] -- | Global variables - [(GVarName, Type' ())] + [(GVarName, Type' () ())] deriving stock (Eq, Show) instance Semigroup ShadowedVarsExpr where @@ -81,14 +83,14 @@ instance Monoid ShadowedVarsExpr where -- Note that type/kind information is extracted from the TypeCache. localVariablesInScopeExpr :: Either ExprZ TypeZ -> - ([(TyVarName, Kind' ())], [(LVarName, Type' ())]) + ([(TyVarName, Kind' ())], [(LVarName, Type' () ())]) localVariablesInScopeExpr exprOrTy = let M tyvars tmvars _globs = either extractLocalsExprZ extractLocalsTypeZ exprOrTy in (reverse tyvars, reverse tmvars) -- keep most-global first extractLocalsTypeZ :: TypeZ -> ShadowedVarsExpr extractLocalsTypeZ z = - let x = variablesInScopeTy $ z ^. asZipper + let x = variablesInScopeTy $ Left $ z ^. asZipper y = unfocusType z in -- walkUpExpr will extract binders strictly containing y -- (i.e. if y=λs.t, then 's' won't be reported). Since no @@ -123,14 +125,14 @@ extractLocalsExprZ = foldAbove getBoundHere _ -> mempty -- If a node has no type annotation we assign it type TEmptyHole - typeOrHole :: Meta (Maybe TypeCache) -> Type' () + typeOrHole :: Meta (Maybe TypeCache) -> Type' () () typeOrHole (Meta _ t _) = typeOrHole' t - typeOrHole' :: Maybe TypeCache -> Type' () + typeOrHole' :: Maybe TypeCache -> Type' () () typeOrHole' = maybe (TEmptyHole ()) uncache -- Extract a Type from a TypeCache - uncache :: TypeCache -> Type' () + uncache :: TypeCache -> Type' () () uncache (TCSynthed t) = t uncache (TCChkedAt t) = t uncache (TCEmb TCBoth{tcSynthed = t}) = t @@ -156,14 +158,14 @@ instance Monoid ShadowedVarsTy where -- | As for 'variablesInScopeExpr', but when you are focussed somewhere inside -- a type, rather than somewhere inside an expr -- Note that kind information is extracted from the cached kind (for 'TLet') -variablesInScopeTy :: TypeZip -> [(TyVarName, Kind' ())] -variablesInScopeTy e = - let N vs = foldAbove getBoundHere e +variablesInScopeTy :: Either TypeZip KindTZ -> [(TyVarName, Kind' ())] +variablesInScopeTy z = + let N vs = foldAbove getBoundHere $ either identity unfocusNest z -- no bindings in kinds in reverse vs -- keep most-global first where getBoundHere :: FoldAbove Type -> ShadowedVarsTy getBoundHere t = case current t of - TForall _ v k _ -> N [(v, k)] + TForall _ v k _ -> N [(v, forgetKindMetadata k)] TLet _ v t' b | prior t == b -> N [(v, kindOrHoleOf t')] | otherwise -> mempty diff --git a/primer/test/Tests/Action.hs b/primer/test/Tests/Action.hs index 0bd7aadcd..2dacd8faf 100644 --- a/primer/test/Tests/Action.hs +++ b/primer/test/Tests/Action.hs @@ -54,7 +54,7 @@ import Primer.Zipper ( focus, target, unfocusExpr, - unfocusType, + unfocusLoc, ) import Tasty (Property, property) import Test.Tasty.HUnit (Assertion, assertFailure, (@?=)) @@ -69,10 +69,11 @@ unit_maxID :: Assertion unit_maxID = let m :: ID -> Meta (Maybe a) m i = Meta i Nothing Nothing + m' i = Meta i () Nothing h = EmptyHole . m - expr a b c d e f = App (m a) (h b) (APP (m c) (h d) $ TForall (m e) "a" (KType ()) (TEmptyHole $ m f)) - in for_ (permutations [0 .. 5]) $ \case - [a, b, c, d, e, f] -> maxID (expr a b c d e f) @?= 5 + expr a b c d e f g = App (m a) (h b) (APP (m c) (h d) $ TForall (m e) "a" (KType (m' f)) (TEmptyHole $ m g)) + in for_ (permutations [0 .. 6]) $ \case + [a, b, c, d, e, f, g] -> maxID (expr a b c d e f g) @?= 6 _ -> error "impossible" tasty_ConstructVar_succeeds_on_hole_when_in_scope :: Property @@ -366,9 +367,9 @@ unit_rename_LAM :: Assertion unit_rename_LAM = actionTest NoSmartHoles - (ann (lAM "a" (emptyHole `aPP` tvar "a")) (tforall "b" (KType ()) $ listOf (tvar "b"))) + (ann (lAM "a" (emptyHole `aPP` tvar "a")) (tforall "b" ktype $ listOf (tvar "b"))) [Move Child1, RenameLAM "b"] - (ann (lAM "b" (emptyHole `aPP` tvar "b")) (tforall "b" (KType ()) $ listOf (tvar "b"))) + (ann (lAM "b" (emptyHole `aPP` tvar "b")) (tforall "b" ktype $ listOf (tvar "b"))) unit_rename_LAM_2 :: Assertion unit_rename_LAM_2 = @@ -1072,22 +1073,22 @@ unit_construct_TForall = NoSmartHoles (emptyHole `ann` tEmptyHole) [EnterType, ConstructTForall (Just "a")] - (ann emptyHole $ tforall "a" (KType ()) tEmptyHole) + (ann emptyHole $ tforall "a" ktype tEmptyHole) unit_rename_TForall :: Assertion unit_rename_TForall = actionTest NoSmartHoles - (emptyHole `ann` tforall "a" (KType ()) (listOf (tvar "a"))) + (emptyHole `ann` tforall "a" ktype (listOf (tvar "a"))) [EnterType, RenameForall "b"] - (emptyHole `ann` tforall "b" (KType ()) (listOf (tvar "b"))) + (emptyHole `ann` tforall "b" ktype (listOf (tvar "b"))) unit_rename_TForall_2 :: Assertion unit_rename_TForall_2 = actionTestExpectFail (const True) NoSmartHoles - (emptyHole `ann` tforall "b" (KType ()) (tforall "a" (KType ()) $ listOf (tvar "b"))) + (emptyHole `ann` tforall "b" ktype (tforall "a" ktype $ listOf (tvar "b"))) [EnterType, Move Child1, RenameLAM "b"] unit_construct_TForall_TVar :: Assertion @@ -1096,7 +1097,7 @@ unit_construct_TForall_TVar = NoSmartHoles (emptyHole `ann` tEmptyHole) [EnterType, ConstructTForall (Just "a"), Move Child1, ConstructTVar "a"] - (ann emptyHole $ tforall "a" (KType ()) $ tvar "a") + (ann emptyHole $ tforall "a" ktype $ tvar "a") unit_poly_1 :: Assertion unit_poly_1 = @@ -1145,8 +1146,8 @@ unit_poly_1 = , Move Child2 , ConstructVar $ LocalVarRef "id" ] - ( let_ "id" (ann (lAM "a" $ lam "x" $ lvar "x") (tforall "a" (KType ()) $ tfun (tvar "a") (tvar "a"))) $ - app (aPP (lvar "id") (tforall "b" (KType ()) $ tfun (tvar "b") (tvar "b"))) (lvar "id") + ( let_ "id" (ann (lAM "a" $ lam "x" $ lvar "x") (tforall "a" ktype $ tfun (tvar "a") (tvar "a"))) $ + app (aPP (lvar "id") (tforall "b" ktype $ tfun (tvar "b") (tvar "b"))) (lvar "id") ) unit_constructTApp :: Assertion @@ -1193,17 +1194,17 @@ unit_refine_4 :: Assertion unit_refine_4 = actionTest NoSmartHoles - (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" (KType ()) (tcon tList `tapp` tvar "a")) $ emptyHole `ann` (tcon tList `tapp` tcon tNat)) + (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" ktype (tcon tList `tapp` tvar "a")) $ emptyHole `ann` (tcon tList `tapp` tcon tNat)) [Move Child2, Move Child1, InsertRefinedVar $ LocalVarRef "nil"] - (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" (KType ()) (tcon tList `tapp` tvar "a")) $ (lvar "nil" `aPP` tcon tNat) `ann` (tcon tList `tapp` tcon tNat)) + (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" ktype (tcon tList `tapp` tvar "a")) $ (lvar "nil" `aPP` tcon tNat) `ann` (tcon tList `tapp` tcon tNat)) unit_refine_5 :: Assertion unit_refine_5 = actionTest NoSmartHoles - (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" (KType ()) (tcon tList `tapp` tvar "a")) $ emptyHole `ann` (tcon tList `tapp` tEmptyHole)) + (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" ktype (tcon tList `tapp` tvar "a")) $ emptyHole `ann` (tcon tList `tapp` tEmptyHole)) [Move Child2, Move Child1, InsertRefinedVar $ LocalVarRef "nil"] - (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" (KType ()) (tcon tList `tapp` tvar "a")) $ (lvar "nil" `aPP` tEmptyHole) `ann` (tcon tList `tapp` tEmptyHole)) + (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" ktype (tcon tList `tapp` tvar "a")) $ (lvar "nil" `aPP` tEmptyHole) `ann` (tcon tList `tapp` tEmptyHole)) -- If there is no valid refinement, insert saturated variable into a non-empty hole unit_refine_mismatch_var :: Assertion @@ -1215,7 +1216,7 @@ unit_refine_mismatch_var = ( emptyHole `ann` tforall "a" - (KType ()) + ktype ( tvar "a" `tfun` ( (tcon tList `tapp` tvar "a") `tfun` (tcon tList `tapp` tvar "a") @@ -1230,7 +1231,7 @@ unit_refine_mismatch_var = ( emptyHole `ann` tforall "a" - (KType ()) + ktype ( tvar "a" `tfun` ( (tcon tList `tapp` tvar "a") `tfun` (tcon tList `tapp` tvar "a") @@ -1328,7 +1329,7 @@ actionTestExpectFail f sh expr actions = -- given value. Fails if the actions fail. runTestActions :: SmartHoles -> ID -> Expr -> [Action] -> Either ActionError Expr runTestActions sh i expr actions = - either unfocusExpr (unfocusExpr . unfocusType) + unfocusExpr . unfocusLoc <$> evalTestM (i + 1) ( do diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 8f328f98b..3664aa9be 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -113,6 +113,8 @@ import Primer.Core.DSL ( emptyHole, gvar, hole, + kfun, + ktype, lAM, lam, let_, @@ -799,32 +801,32 @@ unit_rename_lam_names = unit_make_LAM_names :: Assertion unit_make_LAM_names = do offeredNamesTest - (emptyHole `ann` tforall "a" (KType ()) (tcon tBool)) + (emptyHole `ann` tforall "a" ktype (tcon tBool)) (InExpr [Child1]) MakeLAM "α" - (lAM "α" emptyHole `ann` tforall "a" (KType ()) (tcon tBool)) + (lAM "α" emptyHole `ann` tforall "a" ktype (tcon tBool)) offeredNamesTest - (emptyHole `ann` tforall "a" (KFun () (KType ()) (KType ())) (tcon tBool)) + (emptyHole `ann` tforall "a" (kfun ktype ktype) (tcon tBool)) (InExpr [Child1]) MakeLAM "f" - (lAM "f" emptyHole `ann` tforall "a" (KFun () (KType ()) (KType ())) (tcon tBool)) + (lAM "f" emptyHole `ann` tforall "a" (kfun ktype ktype) (tcon tBool)) unit_rename_LAM_names :: Assertion unit_rename_LAM_names = do offeredNamesTest - (lAM "x" emptyHole `ann` tforall "a" (KType ()) (tcon tBool)) + (lAM "x" emptyHole `ann` tforall "a" ktype (tcon tBool)) (InExpr [Child1]) RenameLAM "α" - (lAM "α" emptyHole `ann` tforall "a" (KType ()) (tcon tBool)) + (lAM "α" emptyHole `ann` tforall "a" ktype (tcon tBool)) offeredNamesTest - (lAM "x" emptyHole `ann` tforall "a" (KFun () (KType ()) (KType ())) (tcon tBool)) + (lAM "x" emptyHole `ann` tforall "a" (kfun ktype ktype) (tcon tBool)) (InExpr [Child1]) RenameLAM "f" - (lAM "f" emptyHole `ann` tforall "a" (KFun () (KType ()) (KType ())) (tcon tBool)) + (lAM "f" emptyHole `ann` tforall "a" (kfun ktype ktype) (tcon tBool)) -- nb: renaming let cares about the type of the bound var, not of the let unit_rename_let_names :: Assertion @@ -869,17 +871,17 @@ unit_rename_letrec_names = unit_rename_forall_names :: Assertion unit_rename_forall_names = do offeredNamesTest - (emptyHole `ann` tforall "a" (KType ()) (tcon tBool)) + (emptyHole `ann` tforall "a" ktype (tcon tBool)) ([] `InType` []) RenameForall "α" - (emptyHole `ann` tforall "α" (KType ()) (tcon tBool)) + (emptyHole `ann` tforall "α" ktype (tcon tBool)) offeredNamesTest - (emptyHole `ann` tforall "a" (KFun () (KType ()) (KType ())) (tcon tBool)) + (emptyHole `ann` tforall "a" (kfun ktype ktype) (tcon tBool)) ([] `InType` []) RenameForall "f" - (emptyHole `ann` tforall "f" (KFun () (KType ()) (KType ())) (tcon tBool)) + (emptyHole `ann` tforall "f" (kfun ktype ktype) (tcon tBool)) {- -- TODO: reinstate once the TC handles let type! diff --git a/primer/test/Tests/Action/Capture.hs b/primer/test/Tests/Action/Capture.hs index a8c6ae750..bd0375716 100644 --- a/primer/test/Tests/Action/Capture.hs +++ b/primer/test/Tests/Action/Capture.hs @@ -8,9 +8,6 @@ import Primer.Action ( ActionError (NameCapture, NeedEmptyHole), Movement (..), ) -import Primer.Core ( - Kind' (KType), - ) import Primer.Core.DSL import Primer.Typecheck (SmartHoles (NoSmartHoles)) import Test.Tasty.HUnit (Assertion) @@ -135,23 +132,23 @@ unit_ConstructTForall_no_capture = actionTestExpectFail isNameCapture NoSmartHoles - (ann emptyHole $ tforall "x" (KType ()) $ tvar "x") + (ann emptyHole $ tforall "x" ktype $ tvar "x") [EnterType, Move Child1, ConstructTForall (Just "x")] unit_RenameForall_noop :: Assertion unit_RenameForall_noop = actionTest NoSmartHoles - (ann emptyHole $ tforall "x" (KType ()) $ tforall "y" (KType ()) $ tvar "x") + (ann emptyHole $ tforall "x" ktype $ tforall "y" ktype $ tvar "x") [EnterType, Move Child1, RenameForall "y"] - (ann emptyHole $ tforall "x" (KType ()) $ tforall "y" (KType ()) $ tvar "x") + (ann emptyHole $ tforall "x" ktype $ tforall "y" ktype $ tvar "x") unit_RenameForall_no_capture :: Assertion unit_RenameForall_no_capture = actionTestExpectFail isNameCapture NoSmartHoles - (ann emptyHole $ tforall "x" (KType ()) $ tforall "y" (KType ()) $ tvar "x") + (ann emptyHole $ tforall "x" ktype $ tforall "y" ktype $ tvar "x") [EnterType, Move Child1, RenameForall "x"] unit_ty_tm_same_namespace :: Assertion diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index cc8aaba5f..b8e32bdcb 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -24,7 +24,8 @@ import Primer.Action ( Delete, EnterType, Move, - RemoveAnn + RemoveAnn, + SetCursor ), ActionError (CustomFailure, IDNotFound, ImportNameClash), BranchMove (Pattern), @@ -546,7 +547,7 @@ unit_copy_paste_duplicate = do let fromDef = gvn "main" toDef = gvn "blank" (p, fromType, fromExpr, _toType, _toExpr) = create' $ do - mainType <- tforall "a" (KType ()) (tvar "a" `tfun` (tcon tMaybe `tapp` tEmptyHole)) + mainType <- tforall "a" ktype (tvar "a" `tfun` (tcon tMaybe `tapp` tEmptyHole)) mainExpr <- lAM "b" $ lam "x" $ con cJust [lvar "x"] let mainDef = ASTDef mainExpr mainType blankDef <- ASTDef <$> emptyHole <*> tEmptyHole @@ -593,16 +594,16 @@ unit_copy_paste_type_scoping :: Assertion unit_copy_paste_type_scoping = do let mainName = gvn "main" (pInitial, srcID, pExpected) = create' $ do - toCopy <- tvar "a" `tfun` tvar "b" `tfun` tforall "e" (KType ()) (tvar "c" `tfun` tvar "d" `tfun` tvar "e" `tfun` tvar "f") + toCopy <- tvar "a" `tfun` tvar "b" `tfun` tforall "e" ktype (tvar "c" `tfun` tvar "d" `tfun` tvar "e" `tfun` tvar "f") let skel r = - tforall "a" (KType ()) $ - tforall "d" (KType ()) $ - tforall "f" (KType ()) $ - tfun (tforall "b" (KType ()) $ tforall "c" (KType ()) $ tforall "d" (KType ()) $ pure toCopy) $ - tforall "c" (KType ()) $ - tforall "f" (KType ()) r + tforall "a" ktype $ + tforall "d" ktype $ + tforall "f" ktype $ + tfun (tforall "b" ktype $ tforall "c" ktype $ tforall "d" ktype $ pure toCopy) $ + tforall "c" ktype $ + tforall "f" ktype r defInitial <- ASTDef <$> emptyHole <*> skel tEmptyHole - expected <- ASTDef <$> emptyHole <*> skel (tvar "a" `tfun` tEmptyHole `tfun` tforall "e" (KType ()) (tEmptyHole `tfun` tEmptyHole `tfun` tvar "e" `tfun` tEmptyHole)) + expected <- ASTDef <$> emptyHole <*> skel (tvar "a" `tfun` tEmptyHole `tfun` tforall "e" ktype (tEmptyHole `tfun` tEmptyHole `tfun` tvar "e" `tfun` tEmptyHole)) pure ( newEmptyProg' & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)] , getID toCopy @@ -626,8 +627,8 @@ unit_raise = do mainName = gvn mainName' (pInitial, srcID, pExpected) = create' $ do toCopy <- tvar "a" - defInitial <- ASTDef <$> emptyHole <*> tforall "a" (KType ()) (tforall "b" (KType ()) $ pure toCopy) - expected <- ASTDef <$> emptyHole <*> tforall "a" (KType ()) (tvar "a") + defInitial <- ASTDef <$> emptyHole <*> tforall "a" ktype (tforall "b" ktype $ pure toCopy) + expected <- ASTDef <$> emptyHole <*> tforall "a" ktype (tvar "a") pure ( newEmptyProg' & #progModules % _head % #moduleDefs .~ Map.fromList [(mainName', DefAST defInitial)] , getID toCopy @@ -653,7 +654,7 @@ unit_copy_paste_expr_1 = do let mainName' = "main" mainName = gvn mainName' (pInitial, srcID, pExpected) = create' $ do - ty <- tforall "a" (KType ()) $ (tcon tList `tapp` tvar "a") `tfun` tforall "b" (KType ()) (tvar "b" `tfun` (tcon tPair `tapp` tvar "a" `tapp` tvar "b")) + ty <- tforall "a" ktype $ (tcon tList `tapp` tvar "a") `tfun` tforall "b" ktype (tvar "b" `tfun` (tcon tPair `tapp` tvar "a" `tapp` tvar "b")) let toCopy' = con cMakePair [lvar "y" `ann` tvar "a", lvar "z" `ann` tvar "b"] -- want different IDs for the two occurences in expected toCopy <- toCopy' let skel r = @@ -1183,7 +1184,7 @@ unit_ParamKindAction_1 = progActionTest ( defaultProgEditableTypeDefs (pure []) ) - [ParamKindAction tT pB 30 [ConstructKFun]] + [ParamKindAction tT pB [SetCursor 30, ConstructKFun]] $ expectSuccess $ \_ prog' -> do td <- findTypeDef tT prog' @@ -1197,18 +1198,18 @@ unit_ParamKindAction_2 = progActionTest ( defaultProgEditableTypeDefs (pure []) ) - [ ParamKindAction tT pB 30 [ConstructKFun] - , ParamKindAction tT pB 32 [ConstructKType] + [ ParamKindAction tT pB [SetCursor 30, ConstructKFun] + , ParamKindAction tT pB [SetCursor 36, ConstructKType] ] - $ expectError (@?= ActionError (CustomFailure ConstructKType "can only construct this kind in a hole")) + $ expectError (@?= ActionError (CustomFailure ConstructKType "can only construct the kind 'Type' in hole")) unit_ParamKindAction_2b :: Assertion unit_ParamKindAction_2b = progActionTest ( defaultProgEditableTypeDefs (pure []) ) - [ ParamKindAction tT pB 30 [ConstructKFun] - , ParamKindAction tT pB 32 [Delete] + [ ParamKindAction tT pB [SetCursor 30, ConstructKFun] + , ParamKindAction tT pB [SetCursor 36, Delete] ] $ expectSuccess $ \_ prog' -> do @@ -1223,7 +1224,7 @@ unit_ParamKindAction_3 = progActionTest ( defaultProgEditableTypeDefs (pure []) ) - [ ParamKindAction tT pA 29 [Delete] + [ ParamKindAction tT pA [SetCursor 29, Delete] ] $ expectSuccess $ \_ prog' -> do @@ -1238,8 +1239,8 @@ unit_ParamKindAction_bad_id = progActionTest ( defaultProgEditableTypeDefs (pure []) ) - [ ParamKindAction tT pB 30 [ConstructKFun] - , ParamKindAction tT pB 0 [ConstructKType] + [ ParamKindAction tT pB [SetCursor 30, ConstructKFun] + , ParamKindAction tT pB [SetCursor 0, ConstructKType] ] $ expectError (@?= ActionError (IDNotFound 0)) diff --git a/primer/test/Tests/AlphaEquality.hs b/primer/test/Tests/AlphaEquality.hs index 2e8f7b645..d89a267f5 100644 --- a/primer/test/Tests/AlphaEquality.hs +++ b/primer/test/Tests/AlphaEquality.hs @@ -5,7 +5,6 @@ import Foreword import Hedgehog hiding (Property, check, property) import Primer.Builtins import Primer.Core ( - Kind' (KFun, KType), Type', ) import Primer.Core.DSL @@ -45,49 +44,49 @@ unit_4 = unit_5 :: Assertion unit_5 = assertNotEqual - (create_ (tforall "a" (KType ()) $ tcon tList `tapp` tvar "a")) + (create_ (tforall "a" ktype $ tcon tList `tapp` tvar "a")) (create_ (tcon tNat)) unit_6 :: Assertion unit_6 = (@?=) - (create_ (tforall "a" (KType ()) $ tcon tList `tapp` tvar "a")) - (create_ (tforall "b" (KType ()) $ tcon tList `tapp` tvar "b")) + (create_ (tforall "a" ktype $ tcon tList `tapp` tvar "a")) + (create_ (tforall "b" ktype $ tcon tList `tapp` tvar "b")) unit_7 :: Assertion unit_7 = assertNotEqual - (create_ (tforall "a" (KType ()) $ tcon tList `tapp` tvar "a")) - (create_ (tforall "b" (KType ()) $ tcon tList `tapp` tcon tBool)) + (create_ (tforall "a" ktype $ tcon tList `tapp` tvar "a")) + (create_ (tforall "b" ktype $ tcon tList `tapp` tcon tBool)) unit_8 :: Assertion unit_8 = assertNotEqual - (create_ (tforall "a" (KType ()) $ tcon tBool)) - (create_ (tforall "b" (KFun () (KType ()) (KType ())) $ tcon tBool)) + (create_ (tforall "a" ktype $ tcon tBool)) + (create_ (tforall "b" (kfun ktype ktype) $ tcon tBool)) unit_9 :: Assertion unit_9 = assertNotEqual - (create_ (tforall "a" (KType ()) $ tforall "b" (KType ()) $ tcon tList `tapp` tvar "a")) - (create_ (tforall "a" (KType ()) $ tforall "b" (KType ()) $ tcon tList `tapp` tvar "b")) + (create_ (tforall "a" ktype $ tforall "b" ktype $ tcon tList `tapp` tvar "a")) + (create_ (tforall "a" ktype $ tforall "b" ktype $ tcon tList `tapp` tvar "b")) unit_10 :: Assertion unit_10 = assertNotEqual - (create_ (tforall "a" (KType ()) $ tcon tList `tapp` tvar "a")) - (create_ (tcon tList `tapp` tforall "a" (KType ()) (tvar "b"))) + (create_ (tforall "a" ktype $ tcon tList `tapp` tvar "a")) + (create_ (tcon tList `tapp` tforall "a" ktype (tvar "b"))) unit_11 :: Assertion unit_11 = assertNotEqual - (create_ (tforall "a" (KType ()) $ tcon tBool `tfun` (tcon tList `tapp` tvar "a"))) - (create_ (tcon tBool `tfun` tforall "a" (KType ()) (tcon tList `tapp` tvar "a"))) + (create_ (tforall "a" ktype $ tcon tBool `tfun` (tcon tList `tapp` tvar "a"))) + (create_ (tcon tBool `tfun` tforall "a" ktype (tcon tList `tapp` tvar "a"))) unit_repeated_names :: Assertion unit_repeated_names = - create_ (tforall "b" (KType ()) (tforall "foo" (KType ()) (tforall "x" (KType ()) $ tvar "x"))) - @?= create_ (tforall "foo" (KType ()) (tforall "foo" (KType ()) (tforall "x" (KType ()) $ tvar "x"))) + create_ (tforall "b" ktype (tforall "foo" ktype (tforall "x" ktype $ tvar "x"))) + @?= create_ (tforall "foo" ktype (tforall "foo" ktype (tforall "x" ktype $ tvar "x"))) tasty_refl :: Property tasty_refl = property $ do @@ -100,13 +99,13 @@ tasty_alpha = property $ do t <- f <$> forAll (evalExprGen 0 genTyVarName) s === t where - f v = create_ $ tforall v (KType ()) $ tvar v + f v = create_ $ tforall v ktype $ tvar v -create_ :: S (Type' a) -> Alpha +create_ :: S (Type' a b) -> Alpha create_ = Alpha . forgetTypeMetadata . create' -- | Like @Type' ()@, but 'Eq' only compares up to alpha-equality. -newtype Alpha = Alpha (Type' ()) +newtype Alpha = Alpha (Type' () ()) deriving stock (Show) instance Eq Alpha where diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs index b2788dc25..dc5e5688d 100644 --- a/primer/test/Tests/Eval.hs +++ b/primer/test/Tests/Eval.hs @@ -31,7 +31,7 @@ import Primer.Core ( Expr, GlobalName (baseName, qualifiedModule), ID, - Kind' (KFun, KType), + Kind' (KType), Pattern (PatCon, PatPrim), PrimCon (PrimChar), Type, @@ -182,9 +182,9 @@ unit_tryReduce_BETA = do b <- con cNil [] l <- lAM "x" (pure b) a <- tcon tBool - let k_ = KFun () (KType ()) (KType ()) + k_ <- kfun ktype ktype ty_ <- tEmptyHole - i <- aPP (pure l `ann` tforall "a" k_ (pure ty_)) (pure a) + i <- aPP (pure l `ann` tforall "a" (pure k_) (pure ty_)) (pure a) r <- letType "x" (pure a) (pure b) `ann` tlet "a" (pure a) (pure ty_) pure (b, l, a, i, r, k_, ty_) result <- runTryReduce tydefs mempty mempty (input, maxid) @@ -912,7 +912,7 @@ unit_findNodeByID_capture_type :: Assertion unit_findNodeByID_capture_type = let ((expr, varOcc), maxID) = create $ do v <- tvar "x" - e <- letType "x" (tvar "y") (emptyHole `ann` tlet "z" (tvar "y") (tforall "y" (KType ()) (pure v))) + e <- letType "x" (tvar "y") (emptyHole `ann` tlet "z" (tvar "y") (tforall "y" ktype (pure v))) pure (e, getID v) in do case findNodeByID varOcc Syn expr of @@ -1057,7 +1057,7 @@ unit_redexes_LAM_2 :: Assertion unit_redexes_LAM_2 = let e mkAnn = aPP - (lAM "a" (con0' ["M"] "C") `mkAnn` tforall "a" (KType ()) (tcon' ["M"] "C")) + (lAM "a" (con0' ["M"] "C") `mkAnn` tforall "a" ktype (tcon' ["M"] "C")) (tcon' ["M"] "A") in do redexesOf (e noAnn) <@?=> mempty @@ -1069,7 +1069,7 @@ unit_redexes_LAM_3 = lAM "a" ( aPP - (lAM "b" (con0' ["M"] "X") `mkAnn` tforall "a" (KType ()) (tcon' ["M"] "C")) + (lAM "b" (con0' ["M"] "X") `mkAnn` tforall "a" ktype (tcon' ["M"] "C")) (tcon' ["M"] "T") ) in do @@ -1086,7 +1086,7 @@ unit_redexes_LAM_4 = "a" ( aPP ( lAM "b" (lvar "x") - `mkAnn` tforall "a" (KType ()) (tcon' ["M"] "C") + `mkAnn` tforall "a" ktype (tcon' ["M"] "C") ) (tcon' ["M"] "T") ) @@ -1119,9 +1119,9 @@ unit_redexes_let_capture = unit_redexes_lettype_capture :: Assertion unit_redexes_lettype_capture = do -- We can push the letType down once - redexesOf (letType "x" (tvar "y") (emptyHole `ann` tforall "y" (KType ()) (tvar "x"))) <@?=> Set.singleton 0 + redexesOf (letType "x" (tvar "y") (emptyHole `ann` tforall "y" ktype (tvar "x"))) <@?=> Set.singleton 0 -- But now we should rename the forall and not push the tlet further - redexesOf (emptyHole `ann` tlet "x" (tvar "y") (tforall "y" (KType ()) (tvar "x"))) <@?=> Set.singleton 4 + redexesOf (emptyHole `ann` tlet "x" (tvar "y") (tforall "y" ktype (tvar "x"))) <@?=> Set.singleton 4 unit_redexes_letrec_1 :: Assertion unit_redexes_letrec_1 = @@ -1164,7 +1164,7 @@ unit_redexes_letrec_APP_1 = "e" (con0' ["M"] "C") (tcon' ["M"] "T") - (lAM "x" (lvar "e") `mkAnn` tforall "a" (KType ()) (tcon' ["M"] "T")) + (lAM "x" (lvar "e") `mkAnn` tforall "a" ktype (tcon' ["M"] "T")) ) (tcon' ["M"] "D") in do @@ -1303,20 +1303,20 @@ unit_redexes_case_prim = do -- The body of a let has the same directionality as the let itself unit_redexes_let_upsilon :: Assertion unit_redexes_let_upsilon = do - let t = tforall "a" (KType ()) (tvar "a") + let t = tforall "a" ktype (tvar "a") redexesOf (let_ "x" (lam "x" emptyHole `ann` t) $ lam "x" emptyHole `ann` t) <@?=> Set.fromList [0] - redexesOf (lam "x" $ let_ "x" (lam "x" emptyHole `ann` t) $ emptyHole `ann` t) <@?=> Set.fromList [1, 7] + redexesOf (lam "x" $ let_ "x" (lam "x" emptyHole `ann` t) $ emptyHole `ann` t) <@?=> Set.fromList [1, 8] redexesOf (letType "x" t $ lam "x" emptyHole `ann` t) <@?=> Set.fromList [0] - redexesOf (lam "x" $ letType "x" t $ emptyHole `ann` t) <@?=> Set.fromList [1, 4] + redexesOf (lam "x" $ letType "x" t $ emptyHole `ann` t) <@?=> Set.fromList [1, 5] redexesOf (letrec "x" (lam "x" emptyHole `ann` t) t $ lam "x" emptyHole `ann` t) <@?=> Set.fromList [0, 1] - redexesOf (lam "x" $ letrec "x" (lam "x" emptyHole `ann` t) t $ emptyHole `ann` t) <@?=> Set.fromList [1, 2, 9] + redexesOf (lam "x" $ letrec "x" (lam "x" emptyHole `ann` t) t $ emptyHole `ann` t) <@?=> Set.fromList [1, 2, 11] unit_redexes_push_let :: Assertion unit_redexes_push_let = do redexesOf (letrec "x" (lam "x" emptyHole) tEmptyHole $ lam "x" emptyHole) <@?=> Set.fromList [0, 4] redexesOf (letType "x" tEmptyHole $ let_ "y" (lam "x" emptyHole) $ lam "x" emptyHole) <@?=> Set.fromList [0, 2, 5] redexesOf (letType "x" tEmptyHole $ letrec "y" (lam "x" emptyHole) tEmptyHole $ lam "x" emptyHole) <@?=> Set.fromList [0, 2, 6] - redexesOf (letType "x" tEmptyHole $ letType "y" (tforall "x" (KType ()) tEmptyHole) $ lam "x" emptyHole) <@?=> Set.fromList [0, 2, 5] + redexesOf (letType "x" tEmptyHole $ letType "y" (tforall "x" ktype tEmptyHole) $ lam "x" emptyHole) <@?=> Set.fromList [0, 2, 6] unit_redexes_prim_1 :: Assertion unit_redexes_prim_1 = diff --git a/primer/test/Tests/Eval/Utils.hs b/primer/test/Tests/Eval/Utils.hs index faacda104..576bf245f 100644 --- a/primer/test/Tests/Eval/Utils.hs +++ b/primer/test/Tests/Eval/Utils.hs @@ -47,7 +47,7 @@ import Test.Tasty.HUnit (Assertion, (@?=)) -- * whether the term is synthesisable or checkable -- -- * the type of the term -genDirTm :: PropertyT WT (Dir, Expr, Type' ()) +genDirTm :: PropertyT WT (Dir, Expr, Type' () ()) genDirTm = do dir <- forAllT $ Gen.element @[] [Chk, Syn] (t', ty) <- case dir of diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs index 37f55d620..8c8023298 100644 --- a/primer/test/Tests/EvalFull.hs +++ b/primer/test/Tests/EvalFull.hs @@ -144,9 +144,9 @@ unit_2 = unit_3 :: Assertion unit_3 = let ((expr, expected), maxID) = create $ do - e <- letType "a" (tvar "b") $ emptyHole `ann` (tcon' ["M"] "T" `tapp` tvar "a" `tapp` tforall "a" (KType ()) (tvar "a") `tapp` tforall "b" (KType ()) (tcon' ["M"] "S" `tapp` tvar "a" `tapp` tvar "b")) - let b' = "a42" -- NB: fragile name - expect <- emptyHole `ann` (tcon' ["M"] "T" `tapp` tvar "b" `tapp` tforall "a" (KType ()) (tvar "a") `tapp` tforall b' (KType ()) (tcon' ["M"] "S" `tapp` tvar "b" `tapp` tvar b')) + e <- letType "a" (tvar "b") $ emptyHole `ann` (tcon' ["M"] "T" `tapp` tvar "a" `tapp` tforall "a" ktype (tvar "a") `tapp` tforall "b" ktype (tcon' ["M"] "S" `tapp` tvar "a" `tapp` tvar "b")) + let b' = "a46" -- NB: fragile name + expect <- emptyHole `ann` (tcon' ["M"] "T" `tapp` tvar "b" `tapp` tforall "a" ktype (tvar "a") `tapp` tforall b' ktype (tcon' ["M"] "S" `tapp` tvar "b" `tapp` tvar b')) pure (e, expect) in do s <- evalFullTestExactSteps maxID mempty mempty 12 Syn expr @@ -972,7 +972,7 @@ unit_type_preservation_BETA_regression = lAM "b" $ lam "x" $ ( lAM "a" (lam "c" $ emptyHole `ann` tvar "a") - `ann` tforall "b" (KType ()) (tcon tNat `tfun` tvar "b") + `ann` tforall "b" ktype (tcon tNat `tfun` tvar "b") ) `aPP` (tvar "b" `tapp` tcon tBool) `app` lvar "x" @@ -1049,7 +1049,7 @@ unit_type_preservation_BETA_regression = eB <- lAM "b" $ ( lAM "a" (gvar foo `aPP` (tvar "b" `tapp` tcon tBool)) - `ann` tforall "b" (KType ()) (tcon tNat) + `ann` tforall "b" ktype (tcon tNat) ) `aPP` tcon tChar -- BETA step diff --git a/primer/test/Tests/FreeVars.hs b/primer/test/Tests/FreeVars.hs index 87f872b51..bf0a810d4 100644 --- a/primer/test/Tests/FreeVars.hs +++ b/primer/test/Tests/FreeVars.hs @@ -4,7 +4,6 @@ import Foreword import Data.Set qualified as Set import Primer.Builtins -import Primer.Core (Kind' (KType)) import Primer.Core.DSL import Primer.Core.Utils import Test.Tasty.HUnit @@ -29,4 +28,4 @@ unit_2 = ) (lvar "y") ) - (tforall "a" (KType ()) $ tcon' ["M"] "T" `tapp` tvar "a" `tapp` tvar "b") + (tforall "a" ktype $ tcon' ["M"] "T" `tapp` tvar "a" `tapp` tvar "b") diff --git a/primer/test/Tests/Gen/Core/Typed.hs b/primer/test/Tests/Gen/Core/Typed.hs index 5522eb959..2b3574ff2 100644 --- a/primer/test/Tests/Gen/Core/Typed.hs +++ b/primer/test/Tests/Gen/Core/Typed.hs @@ -85,7 +85,7 @@ tasty_genTy = withTests 1000 $ ty === forgetTypeMetadata ty' -- check no smart holes stuff happened -- | Lift 'checkKind' into a property -checkKindTest :: HasCallStack => Kind' () -> Type -> PropertyT WT (Type' (Meta (Kind' ()))) +checkKindTest :: HasCallStack => Kind' () -> Type -> PropertyT WT (Type' (Meta (Kind' ())) (Meta ())) checkKindTest k t = do x <- lift $ runExceptT @TypeError $ checkKind k t case x of @@ -93,7 +93,7 @@ checkKindTest k t = do Right s -> pure s -- | Lift 'synthKind' into a property -synthKindTest :: HasCallStack => Type -> PropertyT WT (Kind' (), Type' (Meta (Kind' ()))) +synthKindTest :: HasCallStack => Type -> PropertyT WT (Kind' (), Type' (Meta (Kind' ())) (Meta ())) synthKindTest t = do x <- lift $ runExceptT @TypeError $ synthKind t case x of @@ -168,7 +168,7 @@ tasty_genSyns = withTests 1000 $ withDiscards 2000 $ propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] $ do tgtTy <- forAllT $ genWTType (KType ()) - _ :: Type' (Meta (Kind' ())) <- checkKindTest (KType ()) =<< generateTypeIDs tgtTy + _ :: Type' (Meta (Kind' ())) (Meta ()) <- checkKindTest (KType ()) =<< generateTypeIDs tgtTy (e, ty) <- forAllT $ genSyns tgtTy (ty', e') <- synthTest =<< generateIDs e annotateShow e' @@ -182,13 +182,13 @@ tasty_genChk = withTests 1000 $ withDiscards 2000 $ propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModule] $ do ty <- forAllT $ genWTType (KType ()) - _ :: Type' (Meta (Kind' ())) <- checkKindTest (KType ()) =<< generateTypeIDs ty + _ :: Type' (Meta (Kind' ())) (Meta ()) <- checkKindTest (KType ()) =<< generateTypeIDs ty t <- forAllT $ genChk ty t' <- checkTest ty =<< generateIDs t t === forgetMetadata t' -- check no smart holes stuff happened -- Lift 'synth' into a property -synthTest :: HasCallStack => Expr -> PropertyT WT (Type' (), ExprT) +synthTest :: HasCallStack => Expr -> PropertyT WT (Type' () (), ExprT) synthTest e = do x <- lift $ runExceptT @TypeError $ synth e case x of @@ -196,7 +196,7 @@ synthTest e = do Right y -> pure y -- Lift 'check' into a property -checkTest :: HasCallStack => Type' () -> Expr -> PropertyT WT ExprT +checkTest :: HasCallStack => Type' () () -> Expr -> PropertyT WT ExprT checkTest ty t = do x <- lift $ runExceptT @TypeError $ check ty t case x of diff --git a/primer/test/Tests/Questions.hs b/primer/test/Tests/Questions.hs index 55fb8f4b9..7cc890d9a 100644 --- a/primer/test/Tests/Questions.hs +++ b/primer/test/Tests/Questions.hs @@ -42,7 +42,7 @@ import Primer.Typecheck ( exprTtoExpr, synth, ) -import Primer.Zipper (ExprZ, TypeZip, down, focus, right) +import Primer.Zipper (ExprZ, Loc' (InExpr), TypeZip, down, focus, right) import Tasty (Property, property) import Test.Tasty import Test.Tasty.HUnit (Assertion, assertFailure, (@?=)) @@ -128,8 +128,8 @@ tasty_shadow_monoid_expr = property $ do data STE' = TyVar (TyVarName, Kind' ()) - | TmVar (LVarName, Type' ()) - | Global (GVarName, Type' ()) + | TmVar (LVarName, Type' () ()) + | Global (GVarName, Type' () ()) deriving stock (Show) nameSTE' :: STE' -> Name @@ -218,7 +218,7 @@ unit_variablesInScope_case = do unit_variablesInScope_type :: Assertion unit_variablesInScope_type = do - let ty = tforall "a" (KType ()) $ tfun (tvar "a") (tapp tEmptyHole tEmptyHole) + let ty = tforall "a" ktype $ tfun (tvar "a") (tapp tEmptyHole tEmptyHole) hasVariablesType ty pure [] hasVariablesType ty down [("a", KType ())] hasVariablesType ty (down >=> down) [("a", KType ())] @@ -227,7 +227,7 @@ unit_variablesInScope_type = do unit_variablesInScope_shadowed :: Assertion unit_variablesInScope_shadowed = do - let ty = tforall "a" (KFun () (KType ()) (KType ())) $ tforall "b" (KType ()) $ tcon tNat `tfun` tforall "a" (KType ()) (tcon tBool `tfun` (tcon tList `tapp` tvar "b")) + let ty = tforall "a" (kfun ktype ktype) $ tforall "b" ktype $ tcon tNat `tfun` tforall "a" ktype (tcon tBool `tfun` (tcon tList `tapp` tvar "b")) expr' = lAM "c" $ lAM "d" $ lam "c" $ lAM "c" $ lam "c" $ emptyHole `ann` (tcon tList `tapp` tvar "d") expr = ann expr' ty hasVariablesType ty pure [] @@ -245,24 +245,24 @@ unit_variablesInScope_shadowed = do -- | Test that if we walk 'path' to some node in 'expr', that node will have -- 'expected' in-scope variables. -- We start by typechecking the expression, so it is annotated with types. -hasVariables :: S Expr -> (ExprZ -> Maybe ExprZ) -> [(LVarName, Type' ())] -> Assertion +hasVariables :: S Expr -> (ExprZ -> Maybe ExprZ) -> [(LVarName, Type' () ())] -> Assertion hasVariables expr path expected = do let e = create' expr case runTypecheckTestM NoSmartHoles (synth e) of Left err -> assertFailure $ show err Right (_, exprT) -> case path $ focus $ exprTtoExpr exprT of - Just z' -> let (_, locals, _) = variablesInScopeExpr mempty (Left z') in locals @?= expected + Just z' -> let (_, locals, _) = variablesInScopeExpr mempty (InExpr z') in locals @?= expected Nothing -> assertFailure "" -- | Like 'hasVariables' but for type variables inside terms also -hasVariablesTyTm :: S Expr -> (ExprZ -> Maybe ExprZ) -> [(TyVarName, Kind' ())] -> [(LVarName, Type' ())] -> Assertion +hasVariablesTyTm :: S Expr -> (ExprZ -> Maybe ExprZ) -> [(TyVarName, Kind' ())] -> [(LVarName, Type' () ())] -> Assertion hasVariablesTyTm expr path expectedTy expectedTm = do let e = create' expr case runTypecheckTestM NoSmartHoles (synth e) of Left err -> assertFailure $ show err Right (_, exprT) -> case path $ focus $ exprTtoExpr exprT of Just z' -> do - let (tyvars, tmvars, _) = variablesInScopeExpr mempty (Left z') + let (tyvars, tmvars, _) = variablesInScopeExpr mempty (InExpr z') tyvars @?= expectedTy tmvars @?= expectedTm Nothing -> assertFailure "" @@ -272,7 +272,7 @@ hasVariablesType :: S Type -> (TypeZip -> Maybe TypeZip) -> [(TyVarName, Kind' ( hasVariablesType ty path expected = do let t = create' ty case path $ focus t of - Just z -> variablesInScopeTy z @?= expected + Just z -> variablesInScopeTy (Left z) @?= expected Nothing -> assertFailure "" -- Test type-directed names @@ -293,7 +293,7 @@ unit_hasGeneratedNames_2 = do hasGeneratedNamesTy tEmptyHole Nothing pure ["α", "β", "γ"] hasGeneratedNamesTy tEmptyHole (Just (KType ())) pure ["α", "β", "γ"] hasGeneratedNamesTy tEmptyHole (Just $ KFun () (KType ()) (KType ())) pure ["f", "m", "t"] - let ty = tforall "α" (KType ()) tEmptyHole + let ty = tforall "α" ktype tEmptyHole hasGeneratedNamesTy ty Nothing pure ["β", "γ", "α1"] hasGeneratedNamesTy ty (Just (KType ())) pure ["β", "γ", "α1"] hasGeneratedNamesTy ty (Just $ KFun () (KType ()) (KType ())) pure ["f", "m", "t"] @@ -314,12 +314,12 @@ hasGeneratedNamesExpr :: S Expr -> Maybe (S Type) -> (ExprZ -> Maybe ExprZ) -> [ hasGeneratedNamesExpr expr ty path expected = do let (e, t) = create' $ (,) <$> expr <*> sequence ty case path $ focus e of - Just z -> runReader (generateNameExpr (Left $ fmap forgetTypeMetadata t) (Left z)) defCxt @?= expected + Just z -> runReader (generateNameExpr (Left $ fmap forgetTypeMetadata t) (InExpr z)) defCxt @?= expected Nothing -> assertFailure "" hasGeneratedNamesTy :: S Type -> Maybe (Kind' ()) -> (TypeZip -> Maybe TypeZip) -> [Name] -> Assertion hasGeneratedNamesTy ty k path expected = do let t = create' ty case path $ focus t of - Just z -> runReader (generateNameTy (Right k) z) defCxt @?= expected + Just z -> runReader (generateNameTy (Right k) (Left z)) defCxt @?= expected Nothing -> assertFailure "" diff --git a/primer/test/Tests/Refine.hs b/primer/test/Tests/Refine.hs index 2c78ea068..5c82eea91 100644 --- a/primer/test/Tests/Refine.hs +++ b/primer/test/Tests/Refine.hs @@ -328,7 +328,7 @@ tasty_scoping = propertyWTInExtendedLocalGlobalCxt [builtinModule, primitiveModu InstAPP t -> Just t _ -> Nothing -isHole :: Type' a -> Bool +isHole :: Type' a b -> Bool isHole (TEmptyHole _) = True isHole (THole _ _) = True isHole _ = False diff --git a/primer/test/Tests/Serialization.hs b/primer/test/Tests/Serialization.hs index be79b3c11..65926451e 100644 --- a/primer/test/Tests/Serialization.hs +++ b/primer/test/Tests/Serialization.hs @@ -181,7 +181,7 @@ fixtures = , mkFixture "movement" Child1 , mkFixture "action" (SetCursor id0) , mkFixture "actionerror" actionError - , mkFixture "type" (TEmptyHole typeMeta) + , mkFixture "type" (TEmptyHole @TypeMeta @() typeMeta) , mkFixture "typecache" (TCSynthed $ TEmptyHole ()) , mkFixture "typecacheboth" (TCBoth (TEmptyHole ()) (TEmptyHole ())) , mkFixture "expr" expr @@ -205,6 +205,6 @@ fixtures = , evalRespDetail = reductionDetail } ) - , mkFixture "prim_char" $ PrimCon @() @() () $ PrimChar 'a' - , mkFixture "prim_int" $ PrimCon @() @() () $ PrimInt 42 + , mkFixture "prim_char" $ PrimCon @() @() @() () $ PrimChar 'a' + , mkFixture "prim_int" $ PrimCon @() @() @() () $ PrimInt 42 ] diff --git a/primer/test/Tests/Subst.hs b/primer/test/Tests/Subst.hs index 04487fc67..caf594834 100644 --- a/primer/test/Tests/Subst.hs +++ b/primer/test/Tests/Subst.hs @@ -9,7 +9,6 @@ import Hedgehog.Range qualified as Range import Primer.Builtins (tBool, tList) import Primer.Core ( ID (ID), - Kind' (KType), TyVarName, Type' (..), ) @@ -34,19 +33,19 @@ unit_1 = unit_2 :: Assertion unit_2 = - create_ (tforall "a" (KType ()) $ tvar "a") + create_ (tforall "a" ktype $ tvar "a") @=? substTy' "a" (create_ $ tcon tBool) - (create_ $ tforall "a" (KType ()) $ tvar "a") + (create_ $ tforall "a" ktype $ tvar "a") unit_3 :: Assertion unit_3 = - create_ (tforall "b" (KType ()) $ tcon tList `tapp` tcon tBool) + create_ (tforall "b" ktype $ tcon tList `tapp` tcon tBool) @=? substTy' "a" (create_ $ tcon tBool) - (create_ $ tforall "b" (KType ()) $ tcon tList `tapp` tvar "a") + (create_ $ tforall "b" ktype $ tcon tList `tapp` tvar "a") -- Substituting a variable that does not occur free is the identity tasty_subst_non_free_id :: Property @@ -116,10 +115,10 @@ tasty_subst_counter_indep = withDiscards 300 $ propertyWT [] $ inExtendedLocalCx j <- forAllT $ ID <$> Gen.int (Range.linear 0 100) Alpha (subst i) === Alpha (subst j) -create_ :: S (Type' a) -> Type' () +create_ :: S (Type' a b) -> Type' () () create_ = forgetTypeMetadata . create' -substTy' :: TyVarName -> Type' () -> Type' () -> Type' () +substTy' :: TyVarName -> Type' () () -> Type' () () -> Type' () () substTy' n s t = evalTestM 0 $ substTy n s t -- Pick an element from this set, without throwing an error if it is empty diff --git a/primer/test/Tests/Transform.hs b/primer/test/Tests/Transform.hs index 97ea567dc..65832517b 100644 --- a/primer/test/Tests/Transform.hs +++ b/primer/test/Tests/Transform.hs @@ -163,7 +163,7 @@ unit_var_6 = do unit_var_7 :: Assertion unit_var_7 = do let tst c = afterRenameTy "foo" "bar" (c $ tvar "bar") Nothing - tst $ tforall "foo" $ KType () + tst $ tforall "foo" ktype tst $ tlet "foo" tEmptyHole -- All other expressions are renamed as expected @@ -199,11 +199,11 @@ unit_case = -- conflicting name unit_forall_1 :: Assertion unit_forall_1 = - afterRenameTy "x" "y" (tforall "z" (KType ()) (tvar "x")) (Just (tforall "z" (KType ()) (tvar "y"))) + afterRenameTy "x" "y" (tforall "z" ktype (tvar "x")) (Just (tforall "z" ktype (tvar "y"))) -- We can't rename inside a type if it has a forall binding the new name already unit_forall_2 :: Assertion -unit_forall_2 = afterRenameTy "x" "y" (tapp (tforall "y" (KType ()) (tvar "x")) (tvar "x")) Nothing +unit_forall_2 = afterRenameTy "x" "y" (tapp (tforall "y" ktype (tvar "x")) (tvar "x")) Nothing -- We can rename a type with a forall that binds the same variable name, -- but we won't do any renaming underneath the forall. @@ -212,8 +212,8 @@ unit_forall_3 = afterRenameTy "x" "y" - (tapp (tforall "x" (KType ()) (tvar "x")) (tvar "x")) - (Just (tapp (tforall "x" (KType ()) (tvar "x")) (tvar "y"))) + (tapp (tforall "x" ktype (tvar "x")) (tvar "x")) + (Just (tapp (tforall "x" ktype (tvar "x")) (tvar "y"))) -- All other types are renamed as we expect unit_tEmptyHole :: Assertion @@ -293,14 +293,14 @@ afterRename' rename normalise fromVar toVar input output = do unit_unfoldApp_1 :: Assertion unit_unfoldApp_1 = - let expr :: Expr' () () + let expr :: Expr' () () () expr = App () (App () (App () (EmptyHole ()) (Lam () "x" (v "x"))) (App () (v "w") (v "y"))) (v "z") v = Var () . LocalVarRef in unfoldApp expr @?= (EmptyHole (), [Lam () "x" (v "x"), App () (v "w") (v "y"), v "z"]) unit_unfoldApp_2 :: Assertion unit_unfoldApp_2 = - let expr :: Expr' () () + let expr :: Expr' () () () expr = Con () (vcn ["M"] "C") [v "x", v "y"] v = Var () . LocalVarRef in unfoldApp expr @?= (expr, []) diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index 1792e8e8a..cd43faab1 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -417,7 +417,7 @@ unit_case_badType = -- than a simultaneous one, resulting in believing @x:b@ and @y:b@! unit_case_subst :: Assertion unit_case_subst = do - let ty x = tforall "a" (KType ()) $ tforall "b" (KType ()) $ (tvar x `tfun` (tvar "b" `tfun` tcon tNat)) `tfun` tcon tNat + let ty x = tforall "a" ktype $ tforall "b" ktype $ (tvar x `tfun` (tvar "b" `tfun` tcon tNat)) `tfun` tcon tNat let expr a b = lAM a $ lAM b $ @@ -564,7 +564,7 @@ unit_poly = expectTyped $ ann (lam "id" $ lAM "a" $ aPP (lvar "id") (tvar "a")) - (tforall "c" (KType ()) (tvar "c" `tfun` tvar "c") `tfun` tforall "b" (KType ()) (tvar "b" `tfun` tvar "b")) + (tforall "c" ktype (tvar "c" `tfun` tvar "c") `tfun` tforall "b" ktype (tvar "b" `tfun` tvar "b")) unit_poly_head_Nat :: Assertion unit_poly_head_Nat = @@ -599,7 +599,7 @@ unit_type_hole_4 :: Assertion unit_type_hole_4 = tapp (tcon tMaybeT) tEmptyHole `expectKinded` KFun () (KType ()) (KType ()) unit_type_hole_5 :: Assertion -unit_type_hole_5 = tforall "a" (KType ()) tEmptyHole `expectKinded` KType () +unit_type_hole_5 = tforall "a" ktype tEmptyHole `expectKinded` KType () unit_type_hole_6 :: Assertion unit_type_hole_6 = thole (tcon tBool) `expectKinded` KHole () @@ -611,8 +611,8 @@ unit_smart_type_not_arrow = unit_smart_type_forall :: Assertion unit_smart_type_forall = - tforall "a" (KType ()) (tcon tList) - `smartSynthKindGives` tforall "a" (KType ()) (thole $ tcon tList) + tforall "a" ktype (tcon tList) + `smartSynthKindGives` tforall "a" ktype (thole $ tcon tList) unit_smart_type_not_type :: Assertion unit_smart_type_not_type = @@ -646,8 +646,8 @@ unit_smart_type_remove_1 = unit_smart_type_remove_2 :: Assertion unit_smart_type_remove_2 = - tforall "a" (KType ()) (thole $ tcon tBool) - `smartSynthKindGives` tforall "a" (KType ()) (tcon tBool) + tforall "a" ktype (thole $ tcon tBool) + `smartSynthKindGives` tforall "a" ktype (tcon tBool) unit_smart_type_remove_3 :: Assertion unit_smart_type_remove_3 = @@ -723,11 +723,11 @@ unit_smartholes_idempotent_created_hole_typecache = ty'' @?= ty' e'' @?= e' -forgetKindCache :: Type' (Meta b) -> Type +forgetKindCache :: Type' (Meta b) (Meta ()) -> Type forgetKindCache = set (_typeMeta % _type) Nothing -- Also clears the kind cache in any embedded types -forgetTypeCache :: Expr' (Meta a) (Meta b) -> Expr +forgetTypeCache :: Expr' (Meta a) (Meta b) (Meta ()) -> Expr forgetTypeCache = set (_exprMeta % _type) Nothing . set (_exprTypeMeta % _type) Nothing -- Regression test: in the past, the inside of non-empty holes needed to be synthesisable. @@ -781,7 +781,7 @@ unit_smartholes_idempotent_holey_ann = unit_smartholes_idempotent_alpha_typecache :: Assertion unit_smartholes_idempotent_alpha_typecache = let x = runTypecheckTestM SmartHoles $ do - ty <- tforall "a" (KType ()) $ tforall "foo" (KType ()) $ tvar "a" `tfun` tvar "foo" + ty <- tforall "a" ktype $ tforall "foo" ktype $ tvar "a" `tfun` tvar "foo" e <- lAM "foo" emptyHole -- Important that this is the "inner" name: i.e. must be exactly "foo" given ty ty' <- checkKind (KType ()) ty e' <- check (forgetTypeMetadata ty') e @@ -819,7 +819,7 @@ instance (Eq (TypeCacheAlpha a), Eq (TypeCacheAlpha b)) => Eq (TypeCacheAlpha (E TypeCacheAlpha (Left a1) == TypeCacheAlpha (Left a2) = TypeCacheAlpha a1 == TypeCacheAlpha a2 TypeCacheAlpha (Right b1) == TypeCacheAlpha (Right b2) = TypeCacheAlpha b1 == TypeCacheAlpha b2 _ == _ = False -instance (Eq (TypeCacheAlpha a), Eq b) => Eq (TypeCacheAlpha (Expr' (Meta a) b)) where +instance (Eq (TypeCacheAlpha a), Eq b, Eq c) => Eq (TypeCacheAlpha (Expr' (Meta a) b c)) where (==) = (==) `on` ((_exprMeta % _type) %~ TypeCacheAlpha) . unTypeCacheAlpha instance Eq (TypeCacheAlpha Def) where TypeCacheAlpha (DefAST (ASTDef e1 t1)) == TypeCacheAlpha (DefAST (ASTDef e2 t2)) = @@ -921,8 +921,8 @@ unit_tcWholeProg_notice_type_updates = <*> t' <*> e' <*> tcon tBool - d0 = mkDefs (gvar' ["M"] "foo") (thole $ tforall "a" (KType ()) $ tvar "a") - d1 = mkDefs (hole $ gvar' ["M"] "foo") (tforall "a" (KType ()) $ tvar "a") + d0 = mkDefs (gvar' ["M"] "foo") (thole $ tforall "a" ktype $ tvar "a") + d1 = mkDefs (hole $ gvar' ["M"] "foo") (tforall "a" ktype $ tvar "a") mkProg ds = do builtinModule' <- builtinModule ds' <- ds @@ -1024,10 +1024,10 @@ smartSynthGives eIn eExpect = where -- We want eGot and eExpect' to have the same type annotations, but they -- may differ on whether they were synthed or checked, and this is OK - normaliseAnnotations :: ExprT -> Expr' (Meta (Type' ())) (Meta (Kind' ())) + normaliseAnnotations :: ExprT -> Expr' (Meta (Type' () ())) (Meta (Kind' ())) (Meta ()) normaliseAnnotations = over (_exprMeta % _type) f where - f :: TypeCache -> Type' () + f :: TypeCache -> Type' () () f = \case TCSynthed t -> t TCChkedAt t -> t diff --git a/primer/test/Tests/Utils.hs b/primer/test/Tests/Utils.hs index 1112c5555..776607f32 100644 --- a/primer/test/Tests/Utils.hs +++ b/primer/test/Tests/Utils.hs @@ -29,7 +29,7 @@ genAST example = fst $ create $ example <&> snd -- particular next 'ID', only that 'nextID' returns whatever -- 'Examples.map''s next 'ID' happens to be. unit_nextID_exampleMap :: Assertion -unit_nextID_exampleMap = nextID (genAST $ Examples.map modName) @?= ID 35 +unit_nextID_exampleMap = nextID (genAST $ Examples.map modName) @?= ID 37 -- See note for 'unit_nextID_exampleMap'. unit_nextID_exampleEven :: Assertion @@ -41,4 +41,4 @@ unit_nextID_exampleOdd = nextID (genAST $ Examples.odd modName) @?= ID 11 -- See note for 'unit_nextID_exampleMap'. unit_nextID_exampleComprehensive :: Assertion -unit_nextID_exampleComprehensive = nextID (genAST $ Examples.comprehensive modName) @?= ID 55 +unit_nextID_exampleComprehensive = nextID (genAST $ Examples.comprehensive modName) @?= ID 57 diff --git a/primer/test/Tests/Zipper.hs b/primer/test/Tests/Zipper.hs index fcc64742c..b13e9e020 100644 --- a/primer/test/Tests/Zipper.hs +++ b/primer/test/Tests/Zipper.hs @@ -3,10 +3,11 @@ module Tests.Zipper where import Foreword -import Data.Generics.Uniplate.Data (para) import Hedgehog hiding (Property, property) import Hedgehog.Gen qualified as Gen +import Optics ((^..)) import Primer.Core +import Primer.Core.Utils (exprIDs) import Primer.Gen.Core.Raw ( evalExprGen, genExpr, @@ -25,7 +26,7 @@ tasty_focus_unfocus_roundtrip = property $ do tasty_focusOn_unfocus_roundtrip :: Property tasty_focusOn_unfocus_roundtrip = property $ do e <- forAll $ evalExprGen 0 genExpr - i <- forAll $ Gen.element $ idsIn e + i <- forAll $ Gen.element $ e ^.. exprIDs case focusOn i e of Just e' -> unfocus e' === e _ -> annotateShow i >> failure @@ -35,13 +36,10 @@ tasty_focusOn_unfocus_roundtrip = property $ do tasty_focusOn_succeeds_on_valid_ids :: Property tasty_focusOn_succeeds_on_valid_ids = property $ do e <- forAll $ evalExprGen 0 genExpr - forM_ (idsIn e) $ \i -> do + forM_ (e ^.. exprIDs) $ \i -> do case focusOn i e of Just (InExpr e') -> getID (target e') === i Just (InType t) -> getID (target t) === i Just (InBind (BindCase b)) -> getID (target b) === i + Just (InKind k) -> getID (target k) === i _ -> annotateShow i >> failure - --- | The IDs of all nodes in an expression -idsIn :: Expr -> [ID] -idsIn = para (\e ids -> getID e : concat ids) diff --git a/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment index 374441dc7..b03355fcd 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment @@ -11,7 +11,7 @@ Output ] , bodyActions = [ - ( 9 + ( 10 , [ Input MakeLam ( Options @@ -62,7 +62,7 @@ Output ] ) , - ( 10 + ( 11 , [ Input MakeLam ( Options @@ -92,7 +92,7 @@ Output ] ) , - ( 11 + ( 12 , [ Input MakeLam ( Options @@ -121,7 +121,7 @@ Output ] ) , - ( 13 + ( 14 , [ Input MakeLam ( Options @@ -177,7 +177,7 @@ Output ] ) , - ( 14 + ( 15 , [ Input MakeLam ( Options @@ -207,7 +207,7 @@ Output ] ) , - ( 15 + ( 16 , [ Input MakeLam ( Options @@ -238,7 +238,7 @@ Output ] ) , - ( 16 + ( 17 , [ Input MakeLam ( Options @@ -267,7 +267,7 @@ Output ] ) , - ( 17 + ( 18 , [ Input MakeLam ( Options @@ -296,7 +296,7 @@ Output ] ) , - ( 18 + ( 19 , [ Input MakeLam ( Options @@ -379,7 +379,7 @@ Output ] ) , - ( 22 + ( 23 , [ Input MakeLam ( Options @@ -462,7 +462,7 @@ Output ] ) , - ( 25 + ( 26 , [ Input MakeLam ( Options @@ -496,7 +496,7 @@ Output ] ) , - ( 26 + ( 27 , [ Input MakeLam ( Options @@ -557,7 +557,7 @@ Output ] ) , - ( 27 + ( 28 , [ Input MakeLam ( Options @@ -586,7 +586,7 @@ Output ] ) , - ( 28 + ( 29 , [ Input MakeLam ( Options @@ -616,7 +616,7 @@ Output ] ) , - ( 29 + ( 30 , [ Input MakeLam ( Options @@ -645,7 +645,7 @@ Output ] ) , - ( 30 + ( 31 , [ Input MakeLam ( Options @@ -674,7 +674,7 @@ Output ] ) , - ( 31 + ( 32 , [ Input MakeLam ( Options @@ -703,7 +703,7 @@ Output ] ) , - ( 32 + ( 33 , [ Input MakeLam ( Options @@ -744,7 +744,7 @@ Output ] ) , - ( 33 + ( 34 , [ Input MakeLam ( Options @@ -773,7 +773,7 @@ Output ] ) , - ( 34 + ( 35 , [ Input MakeLam ( Options @@ -803,7 +803,7 @@ Output ] ) , - ( 44 + ( 46 , [ Input MakeLam ( Options @@ -851,7 +851,7 @@ Output ] ) , - ( 45 + ( 47 , [ Input MakeLam ( Options @@ -881,7 +881,7 @@ Output ] ) , - ( 46 + ( 48 , [ Input MakeLam ( Options @@ -910,7 +910,7 @@ Output ] ) , - ( 47 + ( 49 , [ Input RenamePattern ( Options @@ -942,7 +942,7 @@ Output ] ) , - ( 48 + ( 50 , [ Input MakeLam ( Options @@ -997,7 +997,7 @@ Output ] ) , - ( 49 + ( 51 , [ Input MakeLam ( Options @@ -1027,7 +1027,7 @@ Output ] ) , - ( 50 + ( 52 , [ Input MakeLam ( Options @@ -1057,7 +1057,7 @@ Output ] ) , - ( 51 + ( 53 , [ Input MakeLam ( Options @@ -1087,7 +1087,7 @@ Output ] ) , - ( 52 + ( 54 , [ Input MakeLam ( Options @@ -1180,7 +1180,7 @@ Output ] ) , - ( 53 + ( 55 , [ Input MakeLam ( Options @@ -1210,7 +1210,7 @@ Output ] ) , - ( 54 + ( 56 , [ Input MakeLam ( Options @@ -1240,7 +1240,7 @@ Output ] ) , - ( 55 + ( 57 , [ Input MakeLam ( Options @@ -1333,21 +1333,21 @@ Output ] ) , - ( 12 + ( 13 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 19 + ( 20 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 20 + ( 21 , [ NoInput MakeFun , NoInput Raise @@ -1355,7 +1355,7 @@ Output ] ) , - ( 21 + ( 22 , [ NoInput MakeFun , Input MakeTCon @@ -1417,14 +1417,14 @@ Output ] ) , - ( 23 + ( 24 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 24 + ( 25 , [ NoInput MakeFun , NoInput Raise @@ -1432,14 +1432,14 @@ Output ] ) , - ( 35 + ( 36 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 36 + ( 38 , [ NoInput MakeFun , NoInput AddInput @@ -1448,7 +1448,7 @@ Output ] ) , - ( 37 + ( 39 , [ NoInput MakeFun , NoInput Raise @@ -1456,7 +1456,7 @@ Output ] ) , - ( 38 + ( 40 , [ NoInput MakeFun , NoInput Raise @@ -1464,7 +1464,7 @@ Output ] ) , - ( 39 + ( 41 , [ NoInput MakeFun , NoInput Raise @@ -1472,7 +1472,7 @@ Output ] ) , - ( 40 + ( 42 , [ NoInput MakeFun , NoInput Raise @@ -1480,7 +1480,7 @@ Output ] ) , - ( 41 + ( 43 , [ NoInput MakeFun , NoInput Raise @@ -1488,7 +1488,7 @@ Output ] ) , - ( 42 + ( 44 , [ NoInput MakeFun , NoInput Raise @@ -1496,14 +1496,14 @@ Output ] ) , - ( 43 + ( 45 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 56 + ( 58 , [ NoInput MakeFun , NoInput AddInput @@ -1511,7 +1511,7 @@ Output ] ) , - ( 57 + ( 59 , [ NoInput MakeFun , NoInput Raise @@ -1519,7 +1519,7 @@ Output ] ) , - ( 58 + ( 60 , [ NoInput MakeFun , NoInput Raise @@ -1527,7 +1527,7 @@ Output ] ) , - ( 59 + ( 62 , [ NoInput MakeFun , NoInput Raise @@ -1535,7 +1535,7 @@ Output ] ) , - ( 60 + ( 63 , [ NoInput MakeFun , NoInput Raise @@ -1543,7 +1543,7 @@ Output ] ) , - ( 61 + ( 64 , [ NoInput MakeFun , NoInput Raise @@ -1551,7 +1551,7 @@ Output ] ) , - ( 62 + ( 65 , [ NoInput MakeFun , NoInput Raise @@ -1559,13 +1559,27 @@ Output ] ) , - ( 63 + ( 66 , [ NoInput MakeFun , NoInput Raise , NoInput DeleteType ] ) + , + ( 37 + , + [ NoInput MakeKFun + , NoInput DeleteKind + ] + ) + , + ( 61 + , + [ NoInput MakeKFun + , NoInput DeleteKind + ] + ) ] , sigActions = [ @@ -1593,7 +1607,7 @@ Output ] ) , - ( 3 + ( 4 , [ NoInput MakeFun , NoInput RaiseType @@ -1601,7 +1615,7 @@ Output ] ) , - ( 4 + ( 5 , [ NoInput MakeFun , NoInput RaiseType @@ -1609,7 +1623,7 @@ Output ] ) , - ( 5 + ( 6 , [ NoInput MakeFun , NoInput RaiseType @@ -1617,7 +1631,7 @@ Output ] ) , - ( 6 + ( 7 , [ NoInput MakeFun , NoInput RaiseType @@ -1625,7 +1639,7 @@ Output ] ) , - ( 7 + ( 8 , [ NoInput MakeFun , Input MakeTCon @@ -1687,7 +1701,7 @@ Output ] ) , - ( 8 + ( 9 , [ NoInput MakeFun , NoInput RaiseType diff --git a/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment index d408d6f06..c51a2fb5a 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment @@ -2,10 +2,6 @@ Output { defActions = [] , bodyActions = [ - ( 9 - , [] - ) - , ( 10 , [] ) @@ -14,7 +10,7 @@ Output , [] ) , - ( 13 + ( 12 , [] ) , @@ -38,11 +34,11 @@ Output , [] ) , - ( 22 + ( 19 , [] ) , - ( 25 + ( 23 , [] ) , @@ -82,11 +78,7 @@ Output , [] ) , - ( 44 - , [] - ) - , - ( 45 + ( 35 , [] ) , @@ -130,11 +122,15 @@ Output , [] ) , - ( 12 + ( 56 , [] ) , - ( 19 + ( 57 + , [] + ) + , + ( 13 , [] ) , @@ -146,7 +142,7 @@ Output , [] ) , - ( 23 + ( 22 , [] ) , @@ -154,17 +150,13 @@ Output , [] ) , - ( 35 + ( 25 , [] ) , ( 36 , [] ) - , - ( 37 - , [] - ) , ( 38 , [] @@ -190,11 +182,11 @@ Output , [] ) , - ( 56 + ( 44 , [] ) , - ( 57 + ( 45 , [] ) , @@ -210,15 +202,31 @@ Output , [] ) , - ( 61 + ( 62 , [] ) , - ( 62 + ( 63 , [] ) , - ( 63 + ( 64 + , [] + ) + , + ( 65 + , [] + ) + , + ( 66 + , [] + ) + , + ( 37 + , [] + ) + , + ( 61 , [] ) ] @@ -235,10 +243,6 @@ Output ( 2 , [] ) - , - ( 3 - , [] - ) , ( 4 , [] @@ -259,5 +263,9 @@ Output ( 8 , [] ) + , + ( 9 + , [] + ) ] } \ No newline at end of file diff --git a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment index a6fd44ec0..81ac37f9c 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment @@ -11,7 +11,7 @@ Output ] , bodyActions = [ - ( 9 + ( 10 , [ Input MakeLam ( Options @@ -87,7 +87,7 @@ Output ] ) , - ( 10 + ( 11 , [ Input MakeLam ( Options @@ -142,7 +142,7 @@ Output ] ) , - ( 11 + ( 12 , [ Input MakeLam ( Options @@ -196,7 +196,7 @@ Output ] ) , - ( 13 + ( 14 , [ Input MakeLam ( Options @@ -277,7 +277,7 @@ Output ] ) , - ( 14 + ( 15 , [ Input MakeLam ( Options @@ -332,7 +332,7 @@ Output ] ) , - ( 15 + ( 16 , [ Input MakeLam ( Options @@ -388,7 +388,7 @@ Output ] ) , - ( 16 + ( 17 , [ Input MakeLam ( Options @@ -442,7 +442,7 @@ Output ] ) , - ( 17 + ( 18 , [ Input MakeLam ( Options @@ -496,7 +496,7 @@ Output ] ) , - ( 18 + ( 19 , [ Input MakeLam ( Options @@ -716,7 +716,7 @@ Output ] ) , - ( 22 + ( 23 , [ Input MakeLam ( Options @@ -936,7 +936,7 @@ Output ] ) , - ( 25 + ( 26 , [ Input MakeLam ( Options @@ -995,7 +995,7 @@ Output ] ) , - ( 26 + ( 27 , [ Input MakeLam ( Options @@ -1081,7 +1081,7 @@ Output ] ) , - ( 27 + ( 28 , [ Input MakeLam ( Options @@ -1157,7 +1157,7 @@ Output ] ) , - ( 28 + ( 29 , [ Input MakeLam ( Options @@ -1212,7 +1212,7 @@ Output ] ) , - ( 29 + ( 30 , [ Input MakeLam ( Options @@ -1266,7 +1266,7 @@ Output ] ) , - ( 30 + ( 31 , [ Input MakeLam ( Options @@ -1320,7 +1320,7 @@ Output ] ) , - ( 31 + ( 32 , [ Input MakeLam ( Options @@ -1396,7 +1396,7 @@ Output ] ) , - ( 32 + ( 33 , [ Input MakeLam ( Options @@ -1462,7 +1462,7 @@ Output ] ) , - ( 33 + ( 34 , [ Input MakeLam ( Options @@ -1516,7 +1516,7 @@ Output ] ) , - ( 34 + ( 35 , [ Input MakeLam ( Options @@ -1571,7 +1571,7 @@ Output ] ) , - ( 44 + ( 46 , [ Input MakeLam ( Options @@ -1644,7 +1644,7 @@ Output ] ) , - ( 45 + ( 47 , [ Input MakeLam ( Options @@ -1699,7 +1699,7 @@ Output ] ) , - ( 46 + ( 48 , [ Input MakeLam ( Options @@ -1753,7 +1753,7 @@ Output ] ) , - ( 47 + ( 49 , [ Input RenamePattern ( Options @@ -1785,7 +1785,7 @@ Output ] ) , - ( 48 + ( 50 , [ Input MakeLam ( Options @@ -1865,7 +1865,7 @@ Output ] ) , - ( 49 + ( 51 , [ Input MakeLam ( Options @@ -1920,7 +1920,7 @@ Output ] ) , - ( 50 + ( 52 , [ Input MakeLam ( Options @@ -1975,7 +1975,7 @@ Output ] ) , - ( 51 + ( 53 , [ Input MakeLam ( Options @@ -2030,7 +2030,7 @@ Output ] ) , - ( 52 + ( 54 , [ Input MakeLam ( Options @@ -2260,7 +2260,7 @@ Output ] ) , - ( 53 + ( 55 , [ Input MakeLam ( Options @@ -2315,7 +2315,7 @@ Output ] ) , - ( 54 + ( 56 , [ Input MakeLam ( Options @@ -2370,7 +2370,7 @@ Output ] ) , - ( 55 + ( 57 , [ Input MakeLam ( Options @@ -2600,7 +2600,7 @@ Output ] ) , - ( 12 + ( 13 , [ NoInput MakeFun , NoInput MakeTApp @@ -2630,7 +2630,7 @@ Output ] ) , - ( 19 + ( 20 , [ NoInput MakeFun , NoInput MakeTApp @@ -2660,7 +2660,7 @@ Output ] ) , - ( 20 + ( 21 , [ NoInput MakeFun , NoInput MakeTApp @@ -2691,7 +2691,7 @@ Output ] ) , - ( 21 + ( 22 , [ NoInput MakeFun , Input MakeTVar @@ -2782,7 +2782,7 @@ Output ] ) , - ( 23 + ( 24 , [ NoInput MakeFun , NoInput MakeTApp @@ -2812,7 +2812,7 @@ Output ] ) , - ( 24 + ( 25 , [ NoInput MakeFun , NoInput MakeTApp @@ -2843,7 +2843,7 @@ Output ] ) , - ( 35 + ( 36 , [ NoInput MakeFun , NoInput MakeTApp @@ -2895,7 +2895,7 @@ Output ] ) , - ( 36 + ( 38 , [ NoInput MakeFun , NoInput AddInput @@ -2927,7 +2927,7 @@ Output ] ) , - ( 37 + ( 39 , [ NoInput MakeFun , NoInput MakeTApp @@ -2958,7 +2958,7 @@ Output ] ) , - ( 38 + ( 40 , [ NoInput MakeFun , NoInput MakeTApp @@ -2989,7 +2989,7 @@ Output ] ) , - ( 39 + ( 41 , [ NoInput MakeFun , NoInput MakeTApp @@ -3020,7 +3020,7 @@ Output ] ) , - ( 40 + ( 42 , [ NoInput MakeFun , NoInput MakeTApp @@ -3051,7 +3051,7 @@ Output ] ) , - ( 41 + ( 43 , [ NoInput MakeFun , NoInput MakeTApp @@ -3082,7 +3082,7 @@ Output ] ) , - ( 42 + ( 44 , [ NoInput MakeFun , NoInput MakeTApp @@ -3113,7 +3113,7 @@ Output ] ) , - ( 43 + ( 45 , [ NoInput MakeFun , NoInput MakeTApp @@ -3143,7 +3143,7 @@ Output ] ) , - ( 56 + ( 58 , [ NoInput MakeFun , NoInput AddInput @@ -3174,7 +3174,7 @@ Output ] ) , - ( 57 + ( 59 , [ NoInput MakeFun , NoInput MakeTApp @@ -3205,7 +3205,7 @@ Output ] ) , - ( 58 + ( 60 , [ NoInput MakeFun , NoInput MakeTApp @@ -3258,7 +3258,7 @@ Output ] ) , - ( 59 + ( 62 , [ NoInput MakeFun , NoInput MakeTApp @@ -3289,7 +3289,7 @@ Output ] ) , - ( 60 + ( 63 , [ NoInput MakeFun , NoInput MakeTApp @@ -3320,7 +3320,7 @@ Output ] ) , - ( 61 + ( 64 , [ NoInput MakeFun , NoInput MakeTApp @@ -3351,7 +3351,7 @@ Output ] ) , - ( 62 + ( 65 , [ NoInput MakeFun , NoInput MakeTApp @@ -3382,7 +3382,7 @@ Output ] ) , - ( 63 + ( 66 , [ NoInput MakeFun , NoInput MakeTApp @@ -3412,6 +3412,20 @@ Output , NoInput DeleteType ] ) + , + ( 37 + , + [ NoInput MakeKFun + , NoInput DeleteKind + ] + ) + , + ( 61 + , + [ NoInput MakeKFun + , NoInput DeleteKind + ] + ) ] , sigActions = [ @@ -3530,7 +3544,7 @@ Output ] ) , - ( 3 + ( 4 , [ NoInput MakeFun , NoInput MakeTApp @@ -3561,7 +3575,7 @@ Output ] ) , - ( 4 + ( 5 , [ NoInput MakeFun , NoInput MakeTApp @@ -3592,7 +3606,7 @@ Output ] ) , - ( 5 + ( 6 , [ NoInput MakeFun , NoInput MakeTApp @@ -3623,7 +3637,7 @@ Output ] ) , - ( 6 + ( 7 , [ NoInput MakeFun , NoInput MakeTApp @@ -3654,7 +3668,7 @@ Output ] ) , - ( 7 + ( 8 , [ NoInput MakeFun , Input MakeTVar @@ -3751,7 +3765,7 @@ Output ] ) , - ( 8 + ( 9 , [ NoInput MakeFun , NoInput MakeTApp diff --git a/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment index d408d6f06..c51a2fb5a 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment @@ -2,10 +2,6 @@ Output { defActions = [] , bodyActions = [ - ( 9 - , [] - ) - , ( 10 , [] ) @@ -14,7 +10,7 @@ Output , [] ) , - ( 13 + ( 12 , [] ) , @@ -38,11 +34,11 @@ Output , [] ) , - ( 22 + ( 19 , [] ) , - ( 25 + ( 23 , [] ) , @@ -82,11 +78,7 @@ Output , [] ) , - ( 44 - , [] - ) - , - ( 45 + ( 35 , [] ) , @@ -130,11 +122,15 @@ Output , [] ) , - ( 12 + ( 56 , [] ) , - ( 19 + ( 57 + , [] + ) + , + ( 13 , [] ) , @@ -146,7 +142,7 @@ Output , [] ) , - ( 23 + ( 22 , [] ) , @@ -154,17 +150,13 @@ Output , [] ) , - ( 35 + ( 25 , [] ) , ( 36 , [] ) - , - ( 37 - , [] - ) , ( 38 , [] @@ -190,11 +182,11 @@ Output , [] ) , - ( 56 + ( 44 , [] ) , - ( 57 + ( 45 , [] ) , @@ -210,15 +202,31 @@ Output , [] ) , - ( 61 + ( 62 , [] ) , - ( 62 + ( 63 , [] ) , - ( 63 + ( 64 + , [] + ) + , + ( 65 + , [] + ) + , + ( 66 + , [] + ) + , + ( 37 + , [] + ) + , + ( 61 , [] ) ] @@ -235,10 +243,6 @@ Output ( 2 , [] ) - , - ( 3 - , [] - ) , ( 4 , [] @@ -259,5 +263,9 @@ Output ( 8 , [] ) + , + ( 9 + , [] + ) ] } \ No newline at end of file diff --git a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment index 994b00cea..bd4bf0e0b 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment @@ -11,7 +11,7 @@ Output ] , bodyActions = [ - ( 9 + ( 10 , [ Input MakeLam ( Options @@ -63,7 +63,7 @@ Output ] ) , - ( 10 + ( 11 , [ Input MakeLam ( Options @@ -94,7 +94,7 @@ Output ] ) , - ( 11 + ( 12 , [ Input MakeLam ( Options @@ -124,7 +124,7 @@ Output ] ) , - ( 13 + ( 14 , [ Input MakeLam ( Options @@ -181,7 +181,7 @@ Output ] ) , - ( 14 + ( 15 , [ Input MakeLam ( Options @@ -212,7 +212,7 @@ Output ] ) , - ( 15 + ( 16 , [ Input MakeLam ( Options @@ -244,7 +244,7 @@ Output ] ) , - ( 16 + ( 17 , [ Input MakeLam ( Options @@ -274,7 +274,7 @@ Output ] ) , - ( 17 + ( 18 , [ Input MakeLam ( Options @@ -304,7 +304,7 @@ Output ] ) , - ( 18 + ( 19 , [ Input MakeLam ( Options @@ -500,7 +500,7 @@ Output ] ) , - ( 22 + ( 23 , [ Input MakeLam ( Options @@ -696,7 +696,7 @@ Output ] ) , - ( 25 + ( 26 , [ Input MakeLam ( Options @@ -731,7 +731,7 @@ Output ] ) , - ( 26 + ( 27 , [ Input MakeLam ( Options @@ -793,7 +793,7 @@ Output ] ) , - ( 27 + ( 28 , [ Input MakeLam ( Options @@ -823,7 +823,7 @@ Output ] ) , - ( 28 + ( 29 , [ Input MakeLam ( Options @@ -854,7 +854,7 @@ Output ] ) , - ( 29 + ( 30 , [ Input MakeLam ( Options @@ -884,7 +884,7 @@ Output ] ) , - ( 30 + ( 31 , [ Input MakeLam ( Options @@ -914,7 +914,7 @@ Output ] ) , - ( 31 + ( 32 , [ Input MakeLam ( Options @@ -944,7 +944,7 @@ Output ] ) , - ( 32 + ( 33 , [ Input MakeLam ( Options @@ -986,7 +986,7 @@ Output ] ) , - ( 33 + ( 34 , [ Input MakeLam ( Options @@ -1016,7 +1016,7 @@ Output ] ) , - ( 34 + ( 35 , [ Input MakeLam ( Options @@ -1047,7 +1047,7 @@ Output ] ) , - ( 44 + ( 46 , [ Input MakeLam ( Options @@ -1096,7 +1096,7 @@ Output ] ) , - ( 45 + ( 47 , [ Input MakeLam ( Options @@ -1127,7 +1127,7 @@ Output ] ) , - ( 46 + ( 48 , [ Input MakeLam ( Options @@ -1157,7 +1157,7 @@ Output ] ) , - ( 47 + ( 49 , [ Input RenamePattern ( Options @@ -1189,7 +1189,7 @@ Output ] ) , - ( 48 + ( 50 , [ Input MakeLam ( Options @@ -1245,7 +1245,7 @@ Output ] ) , - ( 49 + ( 51 , [ Input MakeLam ( Options @@ -1276,7 +1276,7 @@ Output ] ) , - ( 50 + ( 52 , [ Input MakeLam ( Options @@ -1307,7 +1307,7 @@ Output ] ) , - ( 51 + ( 53 , [ Input MakeLam ( Options @@ -1338,7 +1338,7 @@ Output ] ) , - ( 52 + ( 54 , [ Input MakeLam ( Options @@ -1544,7 +1544,7 @@ Output ] ) , - ( 53 + ( 55 , [ Input MakeLam ( Options @@ -1575,7 +1575,7 @@ Output ] ) , - ( 54 + ( 56 , [ Input MakeLam ( Options @@ -1606,7 +1606,7 @@ Output ] ) , - ( 55 + ( 57 , [ Input MakeLam ( Options @@ -1812,21 +1812,21 @@ Output ] ) , - ( 12 + ( 13 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 19 + ( 20 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 20 + ( 21 , [ NoInput MakeFun , NoInput Raise @@ -1834,7 +1834,7 @@ Output ] ) , - ( 21 + ( 22 , [ NoInput MakeFun , Input MakeTCon @@ -1896,14 +1896,14 @@ Output ] ) , - ( 23 + ( 24 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 24 + ( 25 , [ NoInput MakeFun , NoInput Raise @@ -1911,14 +1911,14 @@ Output ] ) , - ( 35 + ( 36 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 36 + ( 38 , [ NoInput MakeFun , NoInput AddInput @@ -1927,7 +1927,7 @@ Output ] ) , - ( 37 + ( 39 , [ NoInput MakeFun , NoInput Raise @@ -1935,7 +1935,7 @@ Output ] ) , - ( 38 + ( 40 , [ NoInput MakeFun , NoInput Raise @@ -1943,7 +1943,7 @@ Output ] ) , - ( 39 + ( 41 , [ NoInput MakeFun , NoInput Raise @@ -1951,7 +1951,7 @@ Output ] ) , - ( 40 + ( 42 , [ NoInput MakeFun , NoInput Raise @@ -1959,7 +1959,7 @@ Output ] ) , - ( 41 + ( 43 , [ NoInput MakeFun , NoInput Raise @@ -1967,7 +1967,7 @@ Output ] ) , - ( 42 + ( 44 , [ NoInput MakeFun , NoInput Raise @@ -1975,14 +1975,14 @@ Output ] ) , - ( 43 + ( 45 , [ NoInput MakeFun , NoInput DeleteType ] ) , - ( 56 + ( 58 , [ NoInput MakeFun , NoInput AddInput @@ -1990,7 +1990,7 @@ Output ] ) , - ( 57 + ( 59 , [ NoInput MakeFun , NoInput Raise @@ -1998,7 +1998,7 @@ Output ] ) , - ( 58 + ( 60 , [ NoInput MakeFun , NoInput Raise @@ -2006,7 +2006,7 @@ Output ] ) , - ( 59 + ( 62 , [ NoInput MakeFun , NoInput Raise @@ -2014,7 +2014,7 @@ Output ] ) , - ( 60 + ( 63 , [ NoInput MakeFun , NoInput Raise @@ -2022,7 +2022,7 @@ Output ] ) , - ( 61 + ( 64 , [ NoInput MakeFun , NoInput Raise @@ -2030,7 +2030,7 @@ Output ] ) , - ( 62 + ( 65 , [ NoInput MakeFun , NoInput Raise @@ -2038,13 +2038,27 @@ Output ] ) , - ( 63 + ( 66 , [ NoInput MakeFun , NoInput Raise , NoInput DeleteType ] ) + , + ( 37 + , + [ NoInput MakeKFun + , NoInput DeleteKind + ] + ) + , + ( 61 + , + [ NoInput MakeKFun + , NoInput DeleteKind + ] + ) ] , sigActions = [ @@ -2072,7 +2086,7 @@ Output ] ) , - ( 3 + ( 4 , [ NoInput MakeFun , NoInput RaiseType @@ -2080,7 +2094,7 @@ Output ] ) , - ( 4 + ( 5 , [ NoInput MakeFun , NoInput RaiseType @@ -2088,7 +2102,7 @@ Output ] ) , - ( 5 + ( 6 , [ NoInput MakeFun , NoInput RaiseType @@ -2096,7 +2110,7 @@ Output ] ) , - ( 6 + ( 7 , [ NoInput MakeFun , NoInput RaiseType @@ -2104,7 +2118,7 @@ Output ] ) , - ( 7 + ( 8 , [ NoInput MakeFun , Input MakeTCon @@ -2166,7 +2180,7 @@ Output ] ) , - ( 8 + ( 9 , [ NoInput MakeFun , NoInput RaiseType diff --git a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment index d408d6f06..c51a2fb5a 100644 --- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment +++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment @@ -2,10 +2,6 @@ Output { defActions = [] , bodyActions = [ - ( 9 - , [] - ) - , ( 10 , [] ) @@ -14,7 +10,7 @@ Output , [] ) , - ( 13 + ( 12 , [] ) , @@ -38,11 +34,11 @@ Output , [] ) , - ( 22 + ( 19 , [] ) , - ( 25 + ( 23 , [] ) , @@ -82,11 +78,7 @@ Output , [] ) , - ( 44 - , [] - ) - , - ( 45 + ( 35 , [] ) , @@ -130,11 +122,15 @@ Output , [] ) , - ( 12 + ( 56 , [] ) , - ( 19 + ( 57 + , [] + ) + , + ( 13 , [] ) , @@ -146,7 +142,7 @@ Output , [] ) , - ( 23 + ( 22 , [] ) , @@ -154,17 +150,13 @@ Output , [] ) , - ( 35 + ( 25 , [] ) , ( 36 , [] ) - , - ( 37 - , [] - ) , ( 38 , [] @@ -190,11 +182,11 @@ Output , [] ) , - ( 56 + ( 44 , [] ) , - ( 57 + ( 45 , [] ) , @@ -210,15 +202,31 @@ Output , [] ) , - ( 61 + ( 62 , [] ) , - ( 62 + ( 63 , [] ) , - ( 63 + ( 64 + , [] + ) + , + ( 65 + , [] + ) + , + ( 66 + , [] + ) + , + ( 37 + , [] + ) + , + ( 61 , [] ) ] @@ -235,10 +243,6 @@ Output ( 2 , [] ) - , - ( 3 - , [] - ) , ( 4 , [] @@ -259,5 +263,9 @@ Output ( 8 , [] ) + , + ( 9 + , [] + ) ] } \ No newline at end of file diff --git a/primer/testlib/Primer/Test/Util.hs b/primer/testlib/Primer/Test/Util.hs index cd5f3bb8e..58210200a 100644 --- a/primer/testlib/Primer/Test/Util.hs +++ b/primer/testlib/Primer/Test/Util.hs @@ -44,6 +44,7 @@ import Primer.Core ( HasID, HasMetadata (_metadata), ID, + KindMeta, ModuleName (ModuleName, unModuleName), TyConName, Type', @@ -51,12 +52,13 @@ import Primer.Core ( ValConName, Value, qualifyName, - setID, + _exprKindMeta, _exprMeta, _exprTypeMeta, + _typeKindMeta, _typeMeta, ) -import Primer.Core.Utils (exprIDs) +import Primer.Core.Utils (exprIDs, typeIDs) import Primer.Def (DefMap) import Primer.Log (ConvertLogMessage (convert), PureLogT, runPureLogT) import Primer.Module (Module (moduleDefs), primitiveModule) @@ -92,20 +94,20 @@ gvn :: NonEmpty Name -> Name -> GVarName gvn = qualifyName . ModuleName -- | Replace all 'ID's in an Expr with 0. -zeroIDs :: (HasID a, HasID b) => Expr' a b -> Expr' a b +zeroIDs :: (HasID a, HasID b, HasID c) => Expr' a b c -> Expr' a b c zeroIDs = set exprIDs 0 -- | Replace all 'ID's in a Type with 0. -zeroTypeIDs :: HasID a => Type' a -> Type' a -zeroTypeIDs = over _typeMeta (setID 0) +zeroTypeIDs :: (HasID a, HasID b) => Type' a b -> Type' a b +zeroTypeIDs = set typeIDs 0 -- | Clear the backend-created metadata (IDs and cached types) in the given expression -clearMeta :: Expr' ExprMeta TypeMeta -> Expr' (Maybe Value) (Maybe Value) -clearMeta = over _exprMeta (view _metadata) . over _exprTypeMeta (view _metadata) +clearMeta :: Expr' ExprMeta TypeMeta KindMeta -> Expr' (Maybe Value) (Maybe Value) () +clearMeta = over _exprMeta (view _metadata) . over _exprTypeMeta (view _metadata) . over _exprKindMeta (const ()) -- | Clear the backend-created metadata (IDs and cached types) in the given expression -clearTypeMeta :: Type' TypeMeta -> Type' (Maybe Value) -clearTypeMeta = over _typeMeta (view _metadata) +clearTypeMeta :: Type' TypeMeta KindMeta -> Type' (Maybe Value) () +clearTypeMeta = over _typeMeta (view _metadata) . over _typeKindMeta (const ()) (@?=) :: (MonadIO m, Eq a, Show a) => a -> a -> m () x @?= y = liftIO $ x HUnit.@?= y