From 2be210bb9bee90160132161b3d3db3564694a253 Mon Sep 17 00:00:00 2001 From: crumbtoo Date: Tue, 5 Mar 2024 13:08:15 -0700 Subject: [PATCH] lift1 fix --- rlp.cabal | 1 + src/Core/Syntax.hs | 25 ++++++++++++------ src/Misc/Lift1.hs | 17 ++++++++++-- src/Rlp/AltParse.y | 8 +++++- src/Rlp/AltSyntax.hs | 23 +++++++++++++++++ src/Rlp/HindleyMilner.hs | 56 ++++++++++++++++++++++++++++++++++++++++ src/Rlp/TH.hs | 8 +++--- 7 files changed, 122 insertions(+), 16 deletions(-) create mode 100644 src/Rlp/HindleyMilner.hs diff --git a/rlp.cabal b/rlp.cabal index 4e90646..dcac32c 100644 --- a/rlp.cabal +++ b/rlp.cabal @@ -34,6 +34,7 @@ library , Rlp.Syntax , Rlp.AltSyntax , Rlp.AltParse + , Rlp.HindleyMilner , Rlp.Syntax.Backstage , Rlp.Syntax.Types -- , Rlp.Parse.Decls diff --git a/src/Core/Syntax.hs b/src/Core/Syntax.hs index a12933e..8165fc5 100644 --- a/src/Core/Syntax.hs +++ b/src/Core/Syntax.hs @@ -611,15 +611,24 @@ deriveBifunctor ''ExprF deriveBifoldable ''ExprF deriveBitraversable ''ExprF +instance Lift b => Lift1 (BindingF b) where + liftLift lf (BindingF k v) = liftCon2 'BindingF (lift k) (liftLift lf v) + +instance Lift b => Lift1 (AlterF b) where + liftLift lf (AlterF con bs e) = + liftCon3 'AlterF (lift con) (lift1 bs) (liftLift lf e) + instance Lift b => Lift1 (ExprF b) where - lift1 (VarF k) = liftCon 'VarF (lift k) - lift1 (AppF f x) = liftCon2 'AppF (lift f) (lift x) - lift1 (LamF b e) = liftCon2 'LamF (lift b) (lift e) - lift1 (LetF r bs e) = liftCon3 'LetF (lift r) (lift bs) (lift e) - lift1 (CaseF e as) = liftCon2 'CaseF (lift e) (lift as) - lift1 (TypeF t) = liftCon 'TypeF (lift t) - lift1 (LitF l) = liftCon 'LitF (lift l) - lift1 (ConF t a) = liftCon2 'ConF (lift t) (lift a) + liftLift lf (VarF k) = liftCon 'VarF (lift k) + liftLift lf (AppF f x) = liftCon2 'AppF (lf f) (lf x) + liftLift lf (LamF b e) = liftCon2 'LamF (lift b) (lf e) + liftLift lf (LetF r bs e) = liftCon3 'LetF (lift r) bs' (lf e) + where bs' = liftLift (liftLift lf) bs + liftLift lf (CaseF e as) = liftCon2 'CaseF (lf e) as' + where as' = liftLift (liftLift lf) as + liftLift lf (TypeF t) = liftCon 'TypeF (lift t) + liftLift lf (LitF l) = liftCon 'LitF (lift l) + liftLift lf (ConF t a) = liftCon2 'ConF (lift t) (lift a) deriving instance (Lift b, Lift a) => Lift (ExprF b a) deriving instance (Lift b, Lift a) => Lift (BindingF b a) diff --git a/src/Misc/Lift1.hs b/src/Misc/Lift1.hs index e2929bc..6aac50d 100644 --- a/src/Misc/Lift1.hs +++ b/src/Misc/Lift1.hs @@ -1,6 +1,6 @@ {-# LANGUAGE TemplateHaskell #-} module Misc.Lift1 - ( Lift1(..) + ( Lift1(..), lift1 , liftCon, liftCon2, liftCon3 , Lift(..) ) @@ -13,11 +13,17 @@ import Language.Haskell.TH.Quote import Data.Kind qualified import GHC.Generics +-- instances import Data.Fix +import Data.Functor.Sum -------------------------------------------------------------------------------- class Lift1 (f :: Data.Kind.Type -> Data.Kind.Type) where - lift1 :: (Quote m, Lift t) => f t -> m Exp + -- lift1 :: (Quote m, Lift t) => f t -> m Exp + liftLift :: (Quote m) => (a -> m Exp) -> f a -> m Exp + +lift1 :: (Lift1 f, Lift a, Quote m) => f a -> m Exp +lift1 = liftLift lift liftCon :: Quote m => TH.Name -> m Exp -> m Exp liftCon n = fmap (AppE (ConE n)) @@ -38,4 +44,11 @@ liftCon3 n a b c = do instance Lift1 f => Lift (Fix f) where lift (Fix f) = AppE (ConE 'Fix) <$> lift1 f +instance Lift1 [] where + liftLift lf [] = pure $ ConE '[] + liftLift lf (a:as) = liftCon2 '(:) (lf a) (liftLift lf as) + +instance (Lift1 f, Lift1 g) => Lift1 (Sum f g) where + liftLift lf (InL fa) = liftCon 'InL $ liftLift lf fa + liftLift lf (InR ga) = liftCon 'InR $ liftLift lf ga diff --git a/src/Rlp/AltParse.y b/src/Rlp/AltParse.y index da00607..6a3883c 100644 --- a/src/Rlp/AltParse.y +++ b/src/Rlp/AltParse.y @@ -2,6 +2,7 @@ module Rlp.AltParse ( parseRlpProg , parseRlpProgR + , parseRlpExprR , runP' ) where @@ -70,7 +71,7 @@ StandaloneProgram :: { Program Name (RlpExpr PsName) } StandaloneExpr :: { RlpExpr PsName } - : litint { undefined } + : VL Expr VR { $2 } VL :: { () } VL : vlbrace { () } @@ -207,6 +208,11 @@ parseRlpProgR s = liftErrorful $ errorful (ma,es) where (_,es,ma) = runP' parseRlpProg s +parseRlpExprR :: (Monad m) => Text -> RLPCT m (RlpExpr PsName) +parseRlpExprR s = liftErrorful $ errorful (ma,es) + where + (_,es,ma) = runP' parseRlpExpr s + parseError = error "explode" } diff --git a/src/Rlp/AltSyntax.hs b/src/Rlp/AltSyntax.hs index d318bdb..9eec275 100644 --- a/src/Rlp/AltSyntax.hs +++ b/src/Rlp/AltSyntax.hs @@ -27,6 +27,7 @@ import Control.Lens import Text.Show.Deriving import Data.Text qualified as T import Data.Pretty +import Misc.Lift1 import Compiler.Types import Core.Syntax qualified as Core @@ -162,3 +163,25 @@ instance (Pretty b) => Pretty1 (Program b) where makePrisms ''Pat makePrisms ''Binding +deriving instance (Lift b, Lift a) => Lift (Program b a) +deriving instance (Lift b, Lift a) => Lift (Decl b a) +deriving instance (Lift b) => Lift (Pat b) +deriving instance (Lift b) => Lift (DataCon b) +deriving instance (Lift b) => Lift (Type b) + +instance Lift b => Lift1 (Binding b) where + liftLift lf (VarB b a) = liftCon2 'VarB (lift b) (lf a) + +instance Lift b => Lift1 (Alter b) where + liftLift lf (Alter b a) = liftCon2 'Alter (lift b) (lf a) + +instance Lift b => Lift1 (ExprF b) where + liftLift lf (InfixEF o a b) = + liftCon3 'InfixEF (lift o) (lf a) (lf b) + liftLift lf (LetEF r bs e) = + liftCon3 'LetEF (lift r) bs' (lf e) + where bs' = liftLift (liftLift lf) bs + liftLift lf (CaseEF e as) = + liftCon2 'CaseEF (lf e) as' + where as' = liftLift (liftLift lf) as + diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs new file mode 100644 index 0000000..3675ddc --- /dev/null +++ b/src/Rlp/HindleyMilner.hs @@ -0,0 +1,56 @@ +module Rlp.HindleyMilner + ( infer + , check + , TypeError(..) + , HMError + ) + where +-------------------------------------------------------------------------------- +import Control.Lens hiding (Context', Context) +import Control.Monad.Errorful +import Data.Text qualified as T +import Data.Pretty +import Text.Printf + +import Data.Functor +import Control.Comonad.Cofree + +import Compiler.RlpcError +import Rlp.AltSyntax +-------------------------------------------------------------------------------- + +-- | Type error enum. +data TypeError + -- | Two types could not be unified + = TyErrCouldNotUnify (Type Name) (Type Name) + -- | @x@ could not be unified with @t@ because @x@ occurs in @t@ + | TyErrRecursiveType Name (Type Name) + -- | Untyped, potentially undefined variable + | TyErrUntypedVariable Name + | TyErrMissingTypeSig Name + deriving (Show) + +instance IsRlpcError TypeError where + liftRlpcError = \case + -- todo: use anti-parser instead of show + TyErrCouldNotUnify t u -> Text + [ T.pack $ printf "Could not match type `%s` with `%s`." + (rpretty @String t) (rpretty @String u) + , "Expected: " <> rpretty t + , "Got: " <> rpretty u + ] + TyErrUntypedVariable n -> Text + [ "Untyped (likely undefined) variable `" <> n <> "`" + ] + TyErrRecursiveType t x -> Text + [ T.pack $ printf "Recursive type: `%s' occurs in `%s'" + (rpretty @String t) (rpretty @String x) + ] + +-- | Synonym for @Errorful [TypeError]@. This means an @HMError@ action may +-- throw any number of fatal or nonfatal errors. Run with @runErrorful@. +type HMError = Errorful TypeError + +infer = undefined +check = undefined + diff --git a/src/Rlp/TH.hs b/src/Rlp/TH.hs index 47cd0d2..0ad18c7 100644 --- a/src/Rlp/TH.hs +++ b/src/Rlp/TH.hs @@ -13,16 +13,14 @@ import Control.Monad.IO.Class import Control.Monad import Compiler.RLPC -import Rlp.Parse +import Rlp.AltParse -------------------------------------------------------------------------------- rlpProg :: QuasiQuoter -rlpProg = undefined --- rlpProg = mkqq parseRlpProgR +rlpProg = mkqq parseRlpProgR rlpExpr :: QuasiQuoter -rlpExpr = undefined --- rlpExpr = mkqq parseRlpExprR +rlpExpr = mkqq parseRlpExprR mkq :: (Lift a) => (Text -> RLPCIO a) -> String -> Q Exp mkq parse = evalAndParse >=> lift where