lintCoreProg

2024-03-01 11:18:19 -07:00
parent c026f6f8f9
commit 451b003e08
4 changed files with 66 additions and 175 deletions
--- a/src/Core/Syntax.hs
+++ b/src/Core/Syntax.hs
@@ -33,10 +33,10 @@ module Core.Syntax
    , Pretty(pretty), WithTerseBinds(..)

    -- * Optics
-    , programScDefs, programTypeSigs, programDataTags
-    , formalising
+    , programScDefs, programTypeSigs, programDataTags, programTyCons
+    , formalising, lambdaLifting
    , HasRHS(_rhs), HasLHS(_lhs)
-    , _BindingF, _MkVar
+    , _BindingF, _MkVar, _ScDef
    -- ** Classy optics
    , HasBinders(..), HasArrowStops(..), HasApplicants1(..), HasApplicants(..)
    )
@@ -216,6 +216,8 @@ data Program b = Program
    , _programTypeSigs :: HashMap b Type
    , _programDataTags :: HashMap Name (Tag, Int)
    -- ^ map constructors to their tag and arity
+    , _programTyCons   :: HashMap Name Kind
+    -- ^ map type constructors to their kind
    }
    deriving (Generic)
    deriving (Semigroup, Monoid)
@@ -242,6 +244,14 @@ type ScDef' = ScDef Name
 -- instance IsString (Expr b) where
 --     fromString = Var . fromString

+lambdaLifting :: Iso (ScDef b) (ScDef b') (b, Expr b) (b', Expr b')
+lambdaLifting = iso sa bt where
+    sa (ScDef n as e) = (n, e') where
+        e' = Lam as e
+
+    bt (n, Lam as e) = ScDef n as e
+    bt (n, e)        = ScDef n [] e
+
 ----------------------------------------------------------------------------------

 class HasRHS s t a b | s -> a, t -> b, s b -> t, t a -> s where
@@ -621,6 +631,7 @@ instance (Hashable b, Hashable b')
        <$> traverse (binders k) (_programScDefs p)
        <*> (getAp . ifoldMap toSingleton $ _programTypeSigs p)
        <*> pure (_programDataTags p)
+        <*> pure (_programTyCons p)
      where
        toSingleton :: b -> Type -> Ap f (HashMap b' Type)
        toSingleton b t = Ap $ (`H.singleton` t) <$> k b
@@ -692,4 +703,5 @@ deriving instance (Eq b, Eq a) => Eq (ExprF b a)

 makePrisms ''BindingF
 makePrisms ''Var
+makePrisms ''ScDef

--- a/src/Core/SystemF.hs
+++ b/src/Core/SystemF.hs
@@ -45,8 +45,36 @@ makeLenses ''Gamma
 lintCoreProgR :: (Monad m) => Program Var -> RLPCT m (Program Name)
 lintCoreProgR = undefined

-lint :: Program Var -> Program Name
-lint = undefined
+lintDontCheck :: Program Var -> Program Name
+lintDontCheck = binders %~ view (_MkVar . _1)
+
+lint :: Program Var -> SysF (Program Name)
+lint p = do
+    scs <- traverse (lintScDef g0) $ p ^. programScDefs
+    pure $ lintDontCheck p & programScDefs .~ scs
+  where
+    g0 = mempty & gammaVars .~ typeSigs
+                & gammaTyCons .~ p ^. programTyCons
+    -- 'p' stores the type signatures as 'HashMap Var Type',
+    -- while our typechecking context demands a 'HashMap Name Type'.
+    -- This conversion is perfectly safe, as the 'Hashable' instance for
+    -- 'Var' hashes exactly the internal 'Name'. i.e.
+    -- `hash (MkVar n t) = hash n`.
+    typeSigs = p ^. programTypeSigs
+             & H.mapKeys (view $ _MkVar . _1)
+
+lintScDef :: Gamma -> ScDef Var -> SysF (ScDef Name)
+lintScDef g = traverseOf lambdaLifting $ \ (MkVar n t, e) -> do
+    e'@(t' :< _) <- lintE g e
+    assertUnify t t'
+    let e'' = stripVars . stripTypes $ e'
+    pure (n, e'')
+
+stripTypes :: ET -> Expr Var
+stripTypes (_ :< as) = Fix (stripTypes <$> as)
+
+stripVars :: Expr Var -> Expr Name
+stripVars = binders %~ view (_MkVar . _1)

 type ET = Cofree (ExprF Var) Type

@@ -150,6 +178,11 @@ lintE g = \case
                | t == t'   = Right ()
                | otherwise = Left (SystemFErrorCouldNotMatch t t')

+assertUnify :: Type -> Type -> SysF ()
+assertUnify t t'
+    | t == t'   = pure ()
+    | otherwise = Left (SystemFErrorCouldNotMatch t t')
+
 allUnify :: [Type] -> Maybe SystemFError
 allUnify [] = Nothing
 allUnify [t] = Nothing
--- a/src/Rlp/Syntax/Types.hs
+++ b/src/Rlp/Syntax/Types.hs
@@ -15,7 +15,7 @@ module Rlp.Syntax.Types
    , Rec(..)
    , Lit(..)
    , Pat(..)
-    , Decl(..)
+    , Decl(..), Decl'
    , Program(..)
    , Where

@@ -23,6 +23,8 @@ module Rlp.Syntax.Types
    , Cofree(..)
    , Trans.Cofree.CofreeF
    , SrcSpan(..)
+
+    , programDecls
    )
    where
 ----------------------------------------------------------------------------------
--- a/src/Rlp2Core.hs
+++ b/src/Rlp2Core.hs
@@ -35,18 +35,12 @@ import Effectful
 import Text.Show.Deriving

 import Core.Syntax                      as Core
+import Rlp.Syntax                       as Rlp
 import Compiler.Types
 import Data.Pretty                      (render, pretty)
-import Rlp.Syntax                       as Rlp
 import Rlp.Parse.Types                  (RlpcPs, PsName)
 --------------------------------------------------------------------------------

-desugarRlpProgR = undefined
-desugarRlpProg = undefined
-desugarRlpExpr = undefined
-
-{--
-
 type Tree a = Either Name (Name, Branch a)

 -- | Rose tree branch representing "nested" "patterns" in the Core language. That
@@ -65,180 +59,30 @@ deriveShow1 ''Branch

 --------------------------------------------------------------------------------

-desugarRlpProgR :: forall m. (Monad m) => RlpProgram RlpcPs -> RLPCT m Program'
+desugarRlpProgR :: forall m. (Monad m)
+                => Rlp.Program RlpcPs SrcSpan
+                -> RLPCT m Core.Program'
 desugarRlpProgR p = do
    let p' = desugarRlpProg p
    addDebugMsg "dump-desugared" $ render (pretty p')
    pure p'

-desugarRlpProg :: RlpProgram RlpcPs -> Program'
+desugarRlpProg :: Rlp.Program RlpcPs SrcSpan -> Core.Program'
 desugarRlpProg = rlpProgToCore

-desugarRlpExpr :: RlpExpr RlpcPs -> Expr'
+desugarRlpExpr :: Rlp.Expr' RlpcPs SrcSpan -> Core.Expr'
 desugarRlpExpr = runPureEff . runNameSupply "anon" . exprToCore

+runNameSupply = undefined
+
 -- the rl' program is desugared by desugaring each declaration as a separate
 -- program, and taking the monoidal product of the lot :3

-rlpProgToCore :: RlpProgram RlpcPs -> Program'
-rlpProgToCore = foldMapOf (progDecls . each) declToCore
+rlpProgToCore :: Rlp.Program RlpcPs SrcSpan -> Program'
+rlpProgToCore = foldMapOf (programDecls . each) declToCore

-declToCore :: Decl' RlpcPs -> Program'
+declToCore :: Rlp.Decl RlpcPs SrcSpan -> Program'
+declToCore = undefined

-declToCore (TySigD'' ns t) = mempty &
-    programTypeSigs .~ H.fromList [ (n, typeToCore t) | n <- ns ]
-
-declToCore (DataD'' n as ds) = fold . getZipList $
-    constructorToCore t' <$> ZipList [0..] <*> ZipList ds
-    where
-        -- create the appropriate type from the declared constructor and its
-        -- arguments
-        t' = foldl TyApp (TyCon n) (TyVar . dsNameToName <$> as)
-
-- TODO: where-binds
-declToCore fd@(FunD'' n as e _) = mempty & programScDefs .~ [ScDef n' as' e']
-    where
-        n' = dsNameToName n
-        e' = runPureEff . runNameSupply n . exprToCore . unXRec $ e
-        as' = as <&> \case
-            (unXRec -> VarP k) -> dsNameToName k
-            _                  -> error "no patargs yet"
-
-type NameSupply = Labeled NameSupplyLabel (State [IdP RlpcPs])
-type NameSupplyLabel = "expr-name-supply"
-
-exprToCore :: forall es. (NameSupply :> es) => RlpExpr RlpcPs -> Eff es Expr'
-
-exprToCore (VarE n) = pure $ Var (dsNameToName n)
-
-exprToCore (AppE a b) = (liftA2 App `on` exprToCore . unXRec) a b
-
-exprToCore (OAppE f a b) = (liftA2 mkApp `on` exprToCore . unXRec) a b
-    where
-        mkApp s t = (Var f `App` s) `App` t
-
-exprToCore (CaseE (unXRec -> e) as) = do
-    e' <- exprToCore e
-    Case e' <$> caseAltToCore `traverse` as
-
-exprToCore (LetE bs e) = letToCore NonRec bs e
-exprToCore (LetrecE bs e) = letToCore Rec bs e
-
-exprToCore (LitE l) = litToCore l
-
-letToCore :: forall es. (NameSupply :> es)
-          => Rec -> [Rlp.Binding' RlpcPs] -> RlpExpr' RlpcPs -> Eff es Expr'
-letToCore r bs e = do
-    -- TODO: preserve binder order.
-    (bs',as) <- getParts
-    let insbs | null bs'  = pure
-              | otherwise = pure . Let r bs'
-    appKendo (foldMap Kendo (as `snoc` insbs)) <=< exprToCore $ unXRec e
-  where
-    -- partition & map the list of binders into:
-    --  bs'   : the let-binds that may be directly translated to Core
-    --          let-binds (we do exactly that). this is all the binders that
-    --          are a simple variable rather than a pattern match.
-    -- and as : the let-binds that may **not** be directly translated to
-    --          Core let-exprs. they get turned into case alternates.
-    getParts = traverse f bs <&> partitionEithers
-
-    f :: Rlp.Binding' RlpcPs
-      -> Eff es (Either Core.Binding' (Expr' -> Eff es Expr'))
-    f (PatB'' (VarP'' n) e) = Left . (n :=) <$> exprToCore (unXRec e)
-    f (PatB'' p          e) = pure $ Right (caseify p e)
-
-litToCore :: (NameSupply :> es) => Rlp.Lit RlpcPs -> Eff es Expr'
-litToCore (Rlp.IntL n) = pure . Lit $ Core.IntL n
-
-{-
-let C x = y
-in e
-
-case y of
-    C x -> e
- -}
-
-caseify :: (NameSupply :> es)
-        => Pat' RlpcPs -> RlpExpr' RlpcPs -> Expr' -> Eff es Expr'
-caseify p (unXRec -> e) i =
-    Case <$> exprToCore e <*> ((:[]) <$> alt)
-  where
-    alt = conToRose (unXRec p) <&> foldFix (branchToCore i)
-
-- TODO: where-binds
-caseAltToCore :: (HasCallStack, NameSupply :> es)
-              => (Alt RlpcPs, Where RlpcPs) -> Eff es Alter'
-caseAltToCore (AltA (unXRec -> p) e, wh) = do
-    e' <- exprToCore . unXRec $ e
-    conToRose p <&> foldFix (branchToCore e')
-
-altToCore :: (NameSupply :> es)
-          => Alt RlpcPs -> Eff es Alter'
-altToCore (AltA p e) = altToCore' p e
-
-altToCore' :: (NameSupply :> es)
-           => Pat' RlpcPs -> RlpExpr' RlpcPs -> Eff es Alter'
-altToCore' (unXRec -> p) (unXRec -> e) = do
-    e' <- exprToCore e
-    conToRose p <&> foldFix (branchToCore e')
-
-conToRose :: forall es. (HasCallStack, NameSupply :> es) => Pat RlpcPs -> Eff es Rose
-conToRose (ConP cn as) = Fix . Branch cn <$> patToForrest `traverse` as
-    where
-        patToForrest :: Pat' RlpcPs -> Eff es (Tree Rose)
-        patToForrest (VarP'' x) = pure $ Left (dsNameToName x)
-        patToForrest p@(ConP'' _ _) =
-            Right <$> liftA2 (,) uniqueName br
-          where
-            br = unwrapFix <$> conToRose (unXRec p)
-conToRose s = error $ "conToRose: not a ConP!: " <> show s
-
-branchToCore :: Expr' -> Branch Alter' -> Alter'
-branchToCore e (Branch cn as) = Alter (AltData cn) myBinds e'
-    where
-        -- gather binders for the /current/ pattern, and build an expression
-        -- matching subpatterns
-        (e', myBinds) = mapAccumL f e as
-
-        f :: Expr' -> Tree Alter' -> (Expr', Name)
-        f e (Left n)       = (e, dsNameToName n)
-        f e (Right (n,cs)) = (e', dsNameToName n) where
-            e' = Case (Var $ dsNameToName n) [branchToCore e cs]
-
-runNameSupply :: IdP RlpcPs -> Eff (NameSupply ': es) a -> Eff es a
-runNameSupply n = runLabeled @NameSupplyLabel (evalState ns) where
-    ns = [ "$" <> n <> "_" <> T.pack (show k) | k <- [0..] ]
-
-- | debug helper
-
-nameSupply :: [IdP RlpcPs]
-nameSupply = [ T.pack $ "$x_" <> show n | n <- [0..] ]
-
-uniqueName :: (NameSupply :> es) => Eff es (IdP RlpcPs)
-uniqueName = labeled @NameSupplyLabel @(State [IdP RlpcPs]) $
-    state @[IdP RlpcPs] (fromMaybe err . uncons)
-  where
-    err = error "NameSupply ran out of names! This shound never happen.\
-                \ The caller of runNameSupply is responsible."
-
-constructorToCore :: Type -> Tag -> ConAlt RlpcPs -> Program'
-constructorToCore t tag (ConAlt cn as) =
-    mempty & programTypeSigs . at cn ?~ foldr (:->) t as'
-           & programDataTags . at cn ?~ (tag, length as)
-    where
-        as' = typeToCore <$> as
-
-typeToCore :: RlpType' RlpcPs -> Type
-typeToCore FunConT''    = TyFun
-typeToCore (FunT'' s t) = typeToCore s :-> typeToCore t
-typeToCore (AppT'' s t) = TyApp (typeToCore s) (typeToCore t)
-typeToCore (ConT'' n)   = TyCon (dsNameToName n)
-typeToCore (VarT'' x)   = TyVar (dsNameToName x)
-
-- | Forwards-compatiblity if IdP RlpDs is changed
-dsNameToName :: IdP RlpcPs -> Name
-dsNameToName = id
-
-}
+exprToCore = undefined