msyds/rlp
1
0
Fork 0
Code Issues 4 Pull Requests Actions Packages Projects Releases 2 Wiki Activity

context

Browse Source
This commit is contained in:
crumbtoo
2024-03-20 15:46:23 -06:00
parent 4f55b5387d
commit e75c9ac283
10 changed files with 89 additions and 107 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
.ghci
View File

@@ -1,5 +1,6 @@
-- repl extensions
:set -XOverloadedStrings
:set -XQuasiQuotes
--------------------------------------------------------------------------------

1
rlp.cabal
View File

@@ -75,6 +75,7 @@ library
, text >= 2.0.2 && < 2.3
, unordered-containers >= 0.2.20 && < 0.3
, recursion-schemes >= 5.2.2 && < 5.3
, monadic-recursion-schemes
, data-fix >= 0.3.2 && < 0.4
, utf8-string >= 1.0.2 && < 1.1
, extra >= 1.7.0 && <2

1
src/Core/SystemF.hs
View File

@@ -2,6 +2,7 @@
{-# LANGUAGE OverloadedLists #-}
module Core.SystemF
( lintCoreProgR
, kindOf
)
where
--------------------------------------------------------------------------------

1
src/Rlp/AltParse.y
View File

@@ -60,6 +60,7 @@ import Core.Syntax qualified as Core
let { Located _ TokenLet }
letrec { Located _ TokenLetrec }
in { Located _ TokenIn }
forall { Located _ TokenForall }
%nonassoc '='
%right '->'

15
src/Rlp/AltSyntax.hs
View File

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

99
src/Rlp/HindleyMilner.hs
View File

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

4
src/Rlp/HindleyMilner/Types.hs
View File

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

3
src/Rlp/Lex.x
View File

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

1
src/Rlp/Parse/Types.hs
View File

@@ -109,6 +109,7 @@ data RlpToken
| TokenInfixL
| TokenInfixR
| TokenInfix
| TokenForall
-- reserved ops
| TokenArrow
| TokenPipe

70
src/Rlp2Core.hs
View File

@@ -12,8 +12,7 @@ import Control.Monad.Writer.CPS
import Control.Monad.Utils
import Control.Arrow
import Control.Applicative
import Control.Comonad
import Control.Lens
import Control.Lens hiding ((:<))
import Compiler.RLPC
import Data.List (mapAccumL, partition)
import Data.Text (Text)
@@ -22,14 +21,18 @@ import Data.HashMap.Strict qualified as H
import Data.Monoid (Endo(..))
import Data.Either (partitionEithers)
import Data.Foldable
import Data.Fix
import Data.Maybe (fromJust, fromMaybe)
import Data.Functor.Bind
import Data.Function (on)
import GHC.Stack
import Debug.Trace
import Numeric
import Data.Fix hiding (cata, para, cataM)
import Data.Functor.Bind
import Data.Functor.Foldable
import Data.Functor.Foldable.Monadic
import Control.Comonad
import Effectful.State.Static.Local
import Effectful.Labeled
import Effectful
@@ -59,45 +62,64 @@ deriveShow1 ''Branch
--------------------------------------------------------------------------------
desugarRlpProgR :: forall m a. (Monad m)
=> Rlp.Program PsName a
-> RLPCT m Core.Program'
desugarRlpProgR p = do
let p' = desugarRlpProg p
addDebugMsg "dump-desugared" $ show (out p')
pure p'
-- desugarRlpProgR :: forall m a. (Monad m)
-- => Rlp.Program PsName (TypedRlpExpr PsName)
-- -> RLPCT m (Core.Program Var)
-- desugarRlpProgR p = do
-- let p' = desugarRlpProg p
-- addDebugMsg "dump-desugared" $ show (out p')
-- pure p'
desugarRlpProg = undefined
desugarRlpProgR = undefined
desugarRlpProg :: Rlp.Program PsName (TypedRlpExpr PsName) -> Core.Program Var
desugarRlpProg = rlpProgToCore
desugarRlpExpr = undefined
type NameSupply = Labeled "NameSupply" (State [Name])
runNameSupply :: Text -> Eff (NameSupply ': es) a -> Eff es a
runNameSupply pre = undefined -- evalState [ pre <> "_" <> tshow name | name <- [0..] ]
runNameSupply pre = runLabeled $ evalState [ pre <> "_" <> tshow name | name <- [0..] ]
where tshow = T.pack . show
-- the rl' program is desugared by desugaring each declaration as a separate
-- program, and taking the monoidal product of the lot :3
rlpProgToCore :: Rlp.Program PsName (RlpExpr PsName) -> Program'
rlpProgToCore :: Rlp.Program PsName (TypedRlpExpr PsName) -> Core.Program Var
rlpProgToCore = foldMapOf (programDecls . each) declToCore
declToCore :: Rlp.Decl PsName (RlpExpr PsName) -> Program'
declToCore :: Rlp.Decl PsName (TypedRlpExpr PsName) -> Core.Program Var
-- assume all arguments are VarP's for now
declToCore (FunD b as e) = mempty & programScDefs .~ [ScDef b as' e']
-- assume full eta-expansion for now
declToCore (FunD b [] e) = mempty & programScDefs .~ [ScDef b' [] undefined]
where
as' = as ^.. each . singular _VarP
b' = MkVar b (typeToCore $ extract e)
e' = runPureEff . runNameSupply b . exprToCore $ e
type NameSupply = State [Name]
typeToCore :: Rlp.Type PsName -> Core.Type
typeToCore (VarT n) = TyVar n
exprToCore :: (NameSupply :> es)
=> RlpExpr PsName -> Eff es Core.Expr'
exprToCore = foldFixM \case
InL e -> pure $ Fix e
InR e -> rlpExprToCore e
=> TypedRlpExpr PsName
-> Eff es (Cofree (Core.ExprF Var) Core.Type)
exprToCore = cataM \case
t :<$ InL e -> pure $ t' :< annotateVar t' e
where t' = typeToCore t
-- InL e -> pure . annotateVars . Fix $ e
-- InR e -> rlpExprToCore e
annotateVar :: Core.Type -> Core.ExprF PsName a -> Core.ExprF Var a
-- fixed points:
annotateVar _ (VarF n) = VarF n
annotateVar _ (ConF t a) = ConF t a
annotateVar _ (AppF f x) = AppF f x
annotateVar _ (LitF l) = LitF l
annotateVar _ (TypeF t) = TypeF t
rlpExprToCore :: (NameSupply :> es)
=> Rlp.ExprF PsName Core.Expr' -> Eff es Core.Expr'
=> Rlp.ExprF PsName Core.Expr' -> Eff es Core.Expr'
-- assume all binders are simple variable patterns for now
rlpExprToCore (LetEF r bs e) = pure $ Let r bs' e