diff --git a/src/Core/Syntax.hs b/src/Core/Syntax.hs index 3ab57e9..5efb560 100644 --- 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 diff --git a/src/Core/SystemF.hs b/src/Core/SystemF.hs index 9cc555f..a52d9d4 100644 --- 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 diff --git a/src/Rlp/Syntax/Types.hs b/src/Rlp/Syntax/Types.hs index 1f57f9e..64164f5 100644 --- 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 ---------------------------------------------------------------------------------- diff --git a/src/Rlp2Core.hs b/src/Rlp2Core.hs index 4f3bea4..2395d22 100644 --- 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