system F
This commit is contained in:
crumbtoo
@@ -38,7 +38,7 @@ module Core.Syntax
|
||||
, HasRHS(_rhs), HasLHS(_lhs)
|
||||
, _BindingF, _MkVar
|
||||
-- ** Classy optics
|
||||
, HasBinders(..), HasArrowStops(..)
|
||||
, HasBinders(..), HasArrowStops(..), HasApplicants1(..), HasApplicants(..)
|
||||
)
|
||||
where
|
||||
----------------------------------------------------------------------------------
|
||||
@@ -577,23 +577,34 @@ deriving instance Lift b => Lift (Program b)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- class HasApplicants s t a b | s -> a, t -> b, s b -> t, t a -> s where
|
||||
-- applicants :: Traversal s t a b
|
||||
class HasApplicants1 s t a b | s -> a, t -> b, s b -> t, t a -> s where
|
||||
applicants1 :: Traversal s t a b
|
||||
|
||||
-- instance HasApplicants (ExprF b (Fix (ExprF b))) (ExprF b (Fix (ExprF b)))
|
||||
class HasApplicants s t a b | s -> a, t -> b, s b -> t, t a -> s where
|
||||
applicants :: Traversal s t a b
|
||||
|
||||
instance HasApplicants1 Type Type Type Type where
|
||||
applicants1 k (TyApp f x) = TyApp <$> applicants1 k f <*> k x
|
||||
applicants1 k x = k x
|
||||
|
||||
instance HasApplicants Type Type Type Type where
|
||||
applicants k (TyApp f x) = TyApp <$> applicants k f <*> k x
|
||||
applicants k x = pure x
|
||||
|
||||
-- instance HasArguments (ExprF b (Fix (ExprF b))) (ExprF b (Fix (ExprF b)))
|
||||
-- (Fix (ExprF b)) (Fix (ExprF b)) where
|
||||
-- applicants k (AppF f x) = AppF <$> applicants k f <*> k x
|
||||
-- applicants k x = unwrapFix <$> k (wrapFix x)
|
||||
-- arguments k (AppF f x) = AppF <$> arguments k f <*> k x
|
||||
-- arguments k x = unwrapFix <$> k (wrapFix x)
|
||||
|
||||
-- instance HasApplicants (f (Fix f)) (f (Fix f)) (Fix f) (Fix f)
|
||||
-- => HasApplicants (Fix f) (Fix f) (Fix f) (Fix f) where
|
||||
-- applicants :: forall g. Applicative g
|
||||
-- instance HasArguments (f (Fix f)) (f (Fix f)) (Fix f) (Fix f)
|
||||
-- => HasArguments (Fix f) (Fix f) (Fix f) (Fix f) where
|
||||
-- arguments :: forall g. Applicative g
|
||||
-- => LensLike' g (Fix f) (Fix f)
|
||||
-- applicants k (Fix f) = Fix <$> applicants k f
|
||||
-- arguments k (Fix f) = Fix <$> arguments k f
|
||||
|
||||
-- applicants :: Traversal' (Expr b) (Expr b)
|
||||
-- applicants k (App f x) = App <$> applicants k f <*> k x
|
||||
-- applicants k x = k x
|
||||
-- arguments :: Traversal' (Expr b) (Expr b)
|
||||
-- arguments k (App f x) = App <$> arguments k f <*> k x
|
||||
-- arguments k x = k x
|
||||
|
||||
class HasBinders s t a b | s -> a, t -> b, s b -> t, t a -> s where
|
||||
binders :: Traversal s t a b
|
||||
|
||||
@@ -14,6 +14,9 @@ import Data.Foldable
|
||||
import Data.List.Extra
|
||||
import Control.Monad.Utils
|
||||
import Control.Monad
|
||||
import Data.Text qualified as T
|
||||
import Data.Pretty
|
||||
import Text.Printf
|
||||
|
||||
import Control.Comonad
|
||||
import Control.Comonad.Cofree
|
||||
@@ -24,6 +27,7 @@ import Control.Lens hiding ((:<))
|
||||
import Control.Lens.Unsound
|
||||
|
||||
import Compiler.RLPC
|
||||
import Compiler.RlpcError
|
||||
import Core
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@@ -46,12 +50,27 @@ lint = undefined
|
||||
|
||||
type ET = Cofree (ExprF Var) Type
|
||||
|
||||
type SysF = Either TypeError
|
||||
type SysF = Either SystemFError
|
||||
|
||||
data TypeError = TypeErrorUndefinedVariable Name
|
||||
| TypeErrorKindMismatch Kind Kind
|
||||
| TypeErrorCouldNotMatch Type Type
|
||||
deriving Show
|
||||
data SystemFError = SystemFErrorUndefinedVariable Name
|
||||
| SystemFErrorKindMismatch Kind Kind
|
||||
| SystemFErrorCouldNotMatch Type Type
|
||||
deriving Show
|
||||
|
||||
instance IsRlpcError SystemFError where
|
||||
liftRlpcError = \case
|
||||
SystemFErrorUndefinedVariable n ->
|
||||
undefinedVariableErr n
|
||||
SystemFErrorKindMismatch k k' ->
|
||||
Text [ T.pack $ printf "Could not match kind `%s' with `%s'"
|
||||
(pretty k) (pretty k')
|
||||
]
|
||||
SystemFErrorCouldNotMatch t t' ->
|
||||
Text [ T.pack $ printf "Could not match type `%s' with `%s'"
|
||||
(pretty t) (pretty t')
|
||||
]
|
||||
|
||||
justLintCoreExpr = fmap (fmap (prettyPrec appPrec1)) . lintE demoContext
|
||||
|
||||
lintE :: Gamma -> Expr Var -> SysF ET
|
||||
lintE g = \case
|
||||
@@ -97,7 +116,7 @@ lintE g = \case
|
||||
g' = supplementVars vs g
|
||||
checkBind v@(MkVar n t) e = case lintE g' e of
|
||||
Right (t' :< e') | t == t' -> Right (BindingF v e')
|
||||
| otherwise -> Left (TypeErrorCouldNotMatch t t')
|
||||
| otherwise -> Left (SystemFErrorCouldNotMatch t t')
|
||||
Left e -> Left e
|
||||
Let NonRec bs e -> do
|
||||
(g',bs') <- mapAccumLM checkBind g bs
|
||||
@@ -109,38 +128,50 @@ lintE g = \case
|
||||
checkBind g (BindingF v@(n :^ t) e) = case lintE g (wrapFix e) of
|
||||
Right (t' :< e')
|
||||
| t == t' -> Right (supplementVar n t g, BindingF v e')
|
||||
| otherwise -> Left (TypeErrorCouldNotMatch t t')
|
||||
| otherwise -> Left (SystemFErrorCouldNotMatch t t')
|
||||
Left e -> Left e
|
||||
|
||||
Case e as -> do
|
||||
(ts,as') <- unzip <$> checkAlt `traverse` as
|
||||
unless (allSame ts) $
|
||||
Left (error "unifica oh my god fix this later")
|
||||
e' <- lintE g e
|
||||
pure $ head ts :< CaseF e' as'
|
||||
e'@(et :< _) <- lintE g e
|
||||
(ts,as') <- unzip <$> checkAlt et `traverse` as
|
||||
case allUnify ts of
|
||||
Just err -> Left err
|
||||
Nothing -> pure $ head ts :< CaseF e' as'
|
||||
where
|
||||
checkAlt :: Alter Var -> SysF (Type, AlterF Var ET)
|
||||
checkAlt (AlterF (AltData con) bs e) = do
|
||||
checkAlt :: Type -> Alter Var -> SysF (Type, AlterF Var ET)
|
||||
checkAlt scrutineeType (AlterF (AltData con) bs e) = do
|
||||
ct <- lookupVar g con
|
||||
zipWithM_ fzip bs (ct ^.. arrowStops)
|
||||
ct' <- foldrMOf applicants (elimForall g) ct scrutineeType
|
||||
zipWithM_ fzip bs (ct' ^.. arrowStops)
|
||||
(t :< e') <- lintE (supplementVars (varsToPairs bs) g) (wrapFix e)
|
||||
pure (t, AlterF (AltData con) bs e')
|
||||
where
|
||||
fzip (MkVar _ t) t'
|
||||
| t == t' = Right ()
|
||||
| otherwise = Left (TypeErrorCouldNotMatch t t')
|
||||
| otherwise = Left (SystemFErrorCouldNotMatch t t')
|
||||
|
||||
unforall :: Type -> Type
|
||||
unforall (TyForall _ m) = m
|
||||
unforall m = m
|
||||
allUnify :: [Type] -> Maybe SystemFError
|
||||
allUnify [] = Nothing
|
||||
allUnify [t] = Nothing
|
||||
allUnify (t:t':ts)
|
||||
| t == t' = allUnify ts
|
||||
| otherwise = Just (SystemFErrorCouldNotMatch t t')
|
||||
|
||||
elimForall :: Gamma -> Type -> Type -> SysF Type
|
||||
elimForall g t (TyForall (n :^ k) m) = do
|
||||
k' <- kindOf g t
|
||||
case k == k' of
|
||||
True -> pure $ subst n t m
|
||||
False -> Left $ SystemFErrorKindMismatch k k'
|
||||
elimForall _ m _ = pure m
|
||||
|
||||
varsToPairs :: [Var] -> [(Name, Type)]
|
||||
varsToPairs = toListOf (each . _MkVar)
|
||||
|
||||
checkAgainst :: Gamma -> Var -> Expr Var -> SysF ET
|
||||
checkAgainst g v@(MkVar n t) e = case lintE g e of
|
||||
Right e'@(t' :< _) | t == t' -> Right e'
|
||||
| otherwise -> Left (TypeErrorCouldNotMatch t t')
|
||||
| otherwise -> Left (SystemFErrorCouldNotMatch t t')
|
||||
Left a -> Left a
|
||||
|
||||
supplementVars :: [(Name, Type)] -> Gamma -> Gamma
|
||||
@@ -174,17 +205,17 @@ kindOf _ e = error (show e)
|
||||
lookupCon :: Gamma -> Name -> SysF Kind
|
||||
lookupCon g n = case g ^. gammaTyCons . at n of
|
||||
Just k -> Right k
|
||||
Nothing -> Left (TypeErrorUndefinedVariable n)
|
||||
Nothing -> Left (SystemFErrorUndefinedVariable n)
|
||||
|
||||
lookupVar :: Gamma -> Name -> SysF Type
|
||||
lookupVar g n = case g ^. gammaVars . at n of
|
||||
Just t -> Right t
|
||||
Nothing -> Left (TypeErrorUndefinedVariable n)
|
||||
Nothing -> Left (SystemFErrorUndefinedVariable n)
|
||||
|
||||
lookupTyVar :: Gamma -> Name -> SysF Kind
|
||||
lookupTyVar g n = case g ^. gammaTyVars . at n of
|
||||
Just k -> Right k
|
||||
Nothing -> Left (TypeErrorUndefinedVariable n)
|
||||
Nothing -> Left (SystemFErrorUndefinedVariable n)
|
||||
|
||||
demoContext :: Gamma
|
||||
demoContext = Gamma
|
||||
|
||||
Reference in New Issue
Block a user