context
This commit is contained in:
crumbtoo
@@ -60,6 +60,7 @@ import Core.Syntax qualified as Core
|
||||
let { Located _ TokenLet }
|
||||
letrec { Located _ TokenLetrec }
|
||||
in { Located _ TokenIn }
|
||||
forall { Located _ TokenForall }
|
||||
|
||||
%nonassoc '='
|
||||
%right '->'
|
||||
|
||||
@@ -7,6 +7,7 @@ module Rlp.AltSyntax
|
||||
, DataCon(..), Type(..)
|
||||
, pattern IntT
|
||||
|
||||
, AnnotatedRlpExpr, TypedRlpExpr
|
||||
, TypeF(..)
|
||||
|
||||
, Core.Name, PsName
|
||||
@@ -49,6 +50,10 @@ import Compiler.Types
|
||||
import Core.Syntax qualified as Core
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
type AnnotatedRlpExpr b = Cofree (RlpExprF b)
|
||||
|
||||
type TypedRlpExpr b = Cofree (RlpExprF b) (Type b)
|
||||
|
||||
type PsName = T.Text
|
||||
|
||||
newtype Program b a = Program [Decl b a]
|
||||
@@ -58,15 +63,15 @@ programDecls :: Lens' (Program b a) [Decl b a]
|
||||
programDecls = lens (\ (Program ds) -> ds) (const Program)
|
||||
|
||||
data Decl b a = FunD b [Pat b] a
|
||||
| DataD b [b] [DataCon b]
|
||||
| TySigD b (Type b)
|
||||
| DataD Core.Name [Core.Name] [DataCon b]
|
||||
| TySigD Core.Name (Type b)
|
||||
deriving (Show, Functor, Foldable, Traversable)
|
||||
|
||||
data DataCon b = DataCon b [Type b]
|
||||
data DataCon b = DataCon Core.Name [Type b]
|
||||
deriving (Show, Generic)
|
||||
|
||||
data Type b = VarT b
|
||||
| ConT b
|
||||
data Type b = VarT Core.Name
|
||||
| ConT Core.Name
|
||||
| AppT (Type b) (Type b)
|
||||
| FunT
|
||||
| ForallT b (Type b)
|
||||
|
||||
@@ -1,7 +1,5 @@
|
||||
{-# LANGUAGE ParallelListComp #-}
|
||||
{-# LANGUAGE PartialTypeSignatures #-}
|
||||
{-# LANGUAGE OverloadedLists #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
module Rlp.HindleyMilner
|
||||
( typeCheckRlpProgR
|
||||
, annotate
|
||||
@@ -34,7 +32,7 @@ import Data.HashSet (HashSet)
|
||||
import Data.HashSet qualified as S
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Traversable
|
||||
import GHC.Generics (Generic(..), Generically(..))
|
||||
import GHC.Generics (Generic, Generically(..))
|
||||
import Debug.Trace
|
||||
|
||||
import Data.Functor
|
||||
@@ -89,16 +87,13 @@ gather' = \case
|
||||
Finl (LamF bs e) -> do
|
||||
tbs <- for bs (const freshTv)
|
||||
(te,je) <- gather e
|
||||
let cs = concatMap (uncurry . equals $ je ^. assumptions) $ bs `zip` tbs
|
||||
let cs = bs `zip` tbs
|
||||
& concatMap (uncurry $ elimAssumptions (je ^. assumptions))
|
||||
as = foldr H.delete (je ^. assumptions) bs
|
||||
j = mempty & constraints .~ (je ^. constraints <> cs)
|
||||
& assumptions .~ as
|
||||
t = foldr (:->) te tbs
|
||||
pure (t,j)
|
||||
where
|
||||
equals as b tb = maybe []
|
||||
(fmap $ Equality tb)
|
||||
(as ^. at b)
|
||||
|
||||
-- Finl (LamF [b] e) -> do
|
||||
-- tb <- freshTv
|
||||
@@ -109,7 +104,7 @@ gather' = \case
|
||||
-- t = tb :-> te
|
||||
-- pure (t,j)
|
||||
|
||||
unify :: [Constraint] -> HM Context
|
||||
unify :: [Constraint] -> HM [(PsName, Type PsName)]
|
||||
|
||||
unify [] = pure mempty
|
||||
|
||||
@@ -122,7 +117,7 @@ unify (Equality (VarT s) (VarT t) : cs) | s == t = unify cs
|
||||
|
||||
unify (Equality (VarT s) t : cs)
|
||||
| occurs s t = addFatal $ TyErrRecursiveType s t
|
||||
| otherwise = unify cs' <&> contextVars . at s ?~ t
|
||||
| otherwise = unify cs' <&> ((s,t):)
|
||||
where
|
||||
cs' = cs & each . constraintTypes %~ subst s t
|
||||
|
||||
@@ -131,46 +126,10 @@ unify (Equality s (VarT t) : cs) = unify (Equality (VarT t) s : cs)
|
||||
|
||||
unify (Equality s t : _) = addFatal $ TyErrCouldNotUnify s t
|
||||
|
||||
unify' :: [Constraint] -> HM [(PsName, Type PsName)]
|
||||
|
||||
unify' [] = pure mempty
|
||||
|
||||
unify' (Equality (sx :-> sy) (tx :-> ty) : cs) =
|
||||
unify' $ Equality sx tx : Equality sy ty : cs
|
||||
|
||||
-- elim
|
||||
unify' (Equality (ConT s) (ConT t) : cs) | s == t = unify' cs
|
||||
unify' (Equality (VarT s) (VarT t) : cs) | s == t = unify' cs
|
||||
|
||||
unify' (Equality (VarT s) t : cs)
|
||||
| occurs s t = addFatal $ TyErrRecursiveType s t
|
||||
| otherwise = unify' cs' <&> ((s,t):)
|
||||
where
|
||||
cs' = cs & each . constraintTypes %~ subst s t
|
||||
|
||||
-- swap
|
||||
unify' (Equality s (VarT t) : cs) = unify' (Equality (VarT t) s : cs)
|
||||
|
||||
unify' (Equality s t : _) = addFatal $ TyErrCouldNotUnify s t
|
||||
|
||||
annotate :: RlpExpr PsName
|
||||
-> HM (Cofree (RlpExprF PsName) (Type PsName, PartialJudgement))
|
||||
annotate = sequenceA . fixtend (gather . wrapFix)
|
||||
|
||||
-- infer1 :: RlpExpr PsName -> HM (Type PsName)
|
||||
-- infer1 = infer1' mempty
|
||||
|
||||
-- infer1' :: Context -> RlpExpr PsName -> HM (Type PsName)
|
||||
-- infer1' g1 e = do
|
||||
-- ((t,j) :< _) <- annotate e
|
||||
-- g2 <- unify (j ^. constraints)
|
||||
-- g <- unionContextWithKeyM unifyTypes g1 g2
|
||||
-- pure $ ifoldrOf (contextVars . itraversed) subst t g
|
||||
-- where
|
||||
-- -- intuitively, we'd return mgu(s,t) but the union is left-biased making `s`
|
||||
-- -- the user-specified type: prioritise her.
|
||||
-- unifyTypes _ s t = unify [Equality s t] $> s
|
||||
|
||||
assocs :: IndexedTraversal k [(k,v)] [(k,v')] v v'
|
||||
assocs f [] = pure []
|
||||
assocs f ((k,v):xs) = (\v' xs' -> (k,v') : xs')
|
||||
@@ -180,30 +139,32 @@ traceSubst k v t = trace ("subst " <> show' k <> " " <> show' v <> " " <> show'
|
||||
$ subst k v t
|
||||
where show' a = showsPrec 11 a mempty
|
||||
|
||||
elimAssumptions :: Assumptions -> PsName -> Type PsName -> [Constraint]
|
||||
-- elimAssumptions b tb as = maybe [] (fmap $ Equality tb) (as ^. at b)
|
||||
elimAssumptions as b tb =
|
||||
as ^. at b . non' _Empty & each %~ Equality tb
|
||||
|
||||
elimAssumptionsG :: Context -> Assumptions -> [Constraint]
|
||||
elimAssumptionsG g as =
|
||||
iconcatMapOf (contextVars . itraversed) (elimAssumptions as) g
|
||||
|
||||
infer :: Context -> RlpExpr PsName
|
||||
-> HM (Cofree (RlpExprF PsName) (Type PsName))
|
||||
infer g1 e = do
|
||||
infer g0 e = do
|
||||
e' <- annotate e
|
||||
g2 <- unify' $ concatOf (folded . _2 . constraints) e'
|
||||
traceM $ "e': " <> show (view _1 <$> e')
|
||||
traceM $ "g2: " <> show g2
|
||||
let sub t = ifoldrOf (reversed . assocs) traceSubst t g2
|
||||
let (as, concat -> cs) = unzip $ e' ^.. folded . _2
|
||||
. lensProduct assumptions constraints
|
||||
cs' = concatMap (elimAssumptionsG g0) as <> cs
|
||||
g <- unify cs'
|
||||
let sub t = ifoldrOf (reversed . assocs) subst t g
|
||||
pure $ sub . view _1 <$> e'
|
||||
where
|
||||
-- intuitively, we'd return mgu(s,t) but the union is left-biased making `s`
|
||||
-- the user-specified type: prioritise her.
|
||||
unifyTypes _ s t = unify [Equality s t] $> s
|
||||
|
||||
e :: Cofree (RlpExprF PsName) (Type PsName)
|
||||
e = AppT (AppT FunT (VarT "$a2")) (AppT (AppT FunT (VarT "$a3")) (VarT "$a4")) :< InL (LamF ["f","x"] (VarT "$a4" :< InL (AppF (VarT "$a5" :< InL (VarF "f")) (VarT "$a6" :< InL (AppF (VarT "$a5" :< InL (VarF "f")) (VarT "$a1" :< InL (VarF "x")))))))
|
||||
|
||||
g = Context
|
||||
{ _contextVars = H.fromList
|
||||
[("$a1",VarT "$a6")
|
||||
,("$a3",VarT "$a4")
|
||||
,("$a2",AppT (AppT FunT (VarT "$a4")) (VarT "$a4"))
|
||||
,("$a5",AppT (AppT FunT (VarT "$a1")) (VarT "$a6"))
|
||||
,("$a6",VarT "$a4")]}
|
||||
infer1 :: Context -> RlpExpr PsName -> HM (Type PsName)
|
||||
infer1 g = fmap extract . infer g
|
||||
|
||||
unionContextWithKeyM :: Monad m
|
||||
=> (PsName -> Type PsName -> Type PsName
|
||||
@@ -251,13 +212,6 @@ prettyHM = over (mapped . _1) rout
|
||||
fixtend :: Functor f => (f (Fix f) -> b) -> Fix f -> Cofree f b
|
||||
fixtend c (Fix f) = c f :< fmap (fixtend c) f
|
||||
|
||||
-- infer :: RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName))
|
||||
-- infer = infer' mempty
|
||||
|
||||
-- infer' :: Context -> RlpExpr PsName
|
||||
-- -> HM (Cofree (RlpExprF PsName) (Type PsName))
|
||||
-- infer' g = sequenceA . fixtend (infer1' g . wrapFix)
|
||||
|
||||
buildInitialContext :: Program PsName a -> Context
|
||||
buildInitialContext =
|
||||
Context . H.fromList . toListOf (programDecls . each . _TySigD)
|
||||
@@ -265,7 +219,7 @@ buildInitialContext =
|
||||
typeCheckRlpProgR :: (Monad m)
|
||||
=> Program PsName (RlpExpr PsName)
|
||||
-> RLPCT m (Program PsName
|
||||
(Cofree (RlpExprF PsName) (Type PsName)))
|
||||
(TypedRlpExpr PsName))
|
||||
typeCheckRlpProgR p = tc p
|
||||
where
|
||||
g = buildInitialContext p
|
||||
@@ -318,10 +272,3 @@ prettyVars root = appEndo (foldMap Endo subs)
|
||||
(freeVariablesLTR root)
|
||||
names
|
||||
|
||||
-- test :: Type PsName -> [(PsName, PsName)]
|
||||
-- test root = subs
|
||||
-- where
|
||||
-- alphabetNames = [ T.pack [c] | c <- ['a'..'z'] ]
|
||||
-- names = alphabetNames \\ S.toList (boundVariables root)
|
||||
-- subs = zip (freeVariablesLTR root) names
|
||||
|
||||
|
||||
@@ -36,9 +36,11 @@ newtype Context = Context
|
||||
data Constraint = Equality (Type PsName) (Type PsName)
|
||||
deriving (Eq, Generic, Show)
|
||||
|
||||
type Assumptions = HashMap PsName [Type PsName]
|
||||
|
||||
data PartialJudgement = PartialJudgement
|
||||
{ _constraints :: [Constraint]
|
||||
, _assumptions :: HashMap PsName [Type PsName]
|
||||
, _assumptions :: Assumptions
|
||||
}
|
||||
deriving (Generic, Show)
|
||||
deriving (Monoid)
|
||||
|
||||
@@ -59,7 +59,7 @@ $asciisym = [\!\#\$\%\&\*\+\.\/\<\=\>\?\@\\\^\|\-\~\:]
|
||||
|
||||
@reservedname =
|
||||
case|data|do|import|in|let|letrec|module|of|where
|
||||
|infixr|infixl|infix
|
||||
|infixr|infixl|infix|forall
|
||||
|
||||
@reservedop =
|
||||
"=" | \\ | "->" | "|" | ":"
|
||||
@@ -163,6 +163,7 @@ lexReservedName = \case
|
||||
"infix" -> TokenInfix
|
||||
"infixl" -> TokenInfixL
|
||||
"infixr" -> TokenInfixR
|
||||
"forall" -> TokenForall
|
||||
s -> error (show s)
|
||||
|
||||
lexReservedOp :: Text -> RlpToken
|
||||
|
||||
@@ -109,6 +109,7 @@ data RlpToken
|
||||
| TokenInfixL
|
||||
| TokenInfixR
|
||||
| TokenInfix
|
||||
| TokenForall
|
||||
-- reserved ops
|
||||
| TokenArrow
|
||||
| TokenPipe
|
||||
|
||||
Reference in New Issue
Block a user