lift1 fix

This commit is contained in:
crumbtoo
2024-03-05 13:08:15 -07:00
parent 156ef8d0a7
commit 2d15dbb7ee
7 changed files with 122 additions and 16 deletions

View File

@@ -34,6 +34,7 @@ library
, Rlp.Syntax
, Rlp.AltSyntax
, Rlp.AltParse
, Rlp.HindleyMilner
, Rlp.Syntax.Backstage
, Rlp.Syntax.Types
-- , Rlp.Parse.Decls

View File

@@ -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)

View File

@@ -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

View File

@@ -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"
}

View File

@@ -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

56
src/Rlp/HindleyMilner.hs Normal file
View File

@@ -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

View File

@@ -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