begin gathering

begin gathering
This commit is contained in:
crumbtoo
2024-03-06 11:11:09 -07:00
parent 67c88df53a
commit 407a8f0a16
4 changed files with 114 additions and 12 deletions

View File

@@ -127,6 +127,7 @@ Expr :: { RlpExpr PsName }
: AppE { $1 }
| LetE { $1 }
| CaseE { $1 }
| Expr1 { $1 }
CaseE :: { RlpExpr PsName }
: case Expr of CaseAlts { Finr $ CaseEF $2 $4 }
@@ -144,9 +145,15 @@ LetE :: { RlpExpr PsName }
Binding :: { Binding PsName (RlpExpr PsName) }
: Pat '=' Expr { VarB $1 $3 }
Expr1 :: { RlpExpr PsName }
: VarE { $1 }
| litint { $1 ^. to extract
. singular _TokenLitInt
. to (Finl . Core.LitF . Core.IntL) }
AppE :: { RlpExpr PsName }
: AppE VarE { Finl $ Core.AppF $1 $2 }
| VarE { $1 }
: AppE Expr1 { Finl $ Core.AppF $1 $2 }
| Expr1 { $1 }
VarE :: { RlpExpr PsName }
: Var { Finl $ Core.VarF $1 }

View File

@@ -22,11 +22,13 @@ import Data.Functor.Sum
import Control.Comonad.Cofree
import Data.Fix
import Data.Function (fix)
import GHC.Generics (Generic(..))
import GHC.Generics (Generic, Generic1)
import Data.Hashable
import Data.Hashable.Lifted
import Control.Lens
import Text.Show.Deriving
import Data.Eq.Deriving
import Data.Text qualified as T
import Data.Pretty
import Misc.Lift1
@@ -49,7 +51,7 @@ data Decl b a = FunD b [Pat b] a
deriving Show
data DataCon b = DataCon b [Type b]
deriving Show
deriving (Show, Generic)
data Type b = VarT b
| ConT b
@@ -70,13 +72,16 @@ data ExprF b a = InfixEF b a a
| LetEF Core.Rec [Binding b a] a
| CaseEF a [Alter b a]
deriving (Functor, Foldable, Traversable)
deriving (Eq, Generic, Generic1)
data Alter b a = Alter (Pat b) a
deriving (Show, Functor, Foldable, Traversable)
deriving (Eq, Generic, Generic1)
data Binding b a = FunB b [Pat b] a
| VarB (Pat b) a
deriving (Show, Functor, Foldable, Traversable)
deriving (Eq, Generic, Generic1)
-- type Expr b = Cofree (ExprF b)
@@ -87,7 +92,7 @@ type RlpExpr b = Fix (RlpExprF b)
data Pat b = VarP b
| ConP b
| AppP (Pat b) (Pat b)
deriving Show
deriving (Eq, Show, Generic)
deriveShow1 ''Alter
deriveShow1 ''Binding
@@ -189,3 +194,15 @@ instance Lift b => Lift1 (ExprF b) where
liftCon2 'CaseEF (lf e) as'
where as' = liftLift (liftLift lf) as
deriveEq1 ''Binding
deriveEq1 ''Alter
deriveEq1 ''ExprF
instance (Hashable b) => Hashable (Pat b)
instance (Hashable b, Hashable a) => Hashable (Binding b a)
instance (Hashable b, Hashable a) => Hashable (Alter b a)
instance (Hashable b, Hashable a) => Hashable (ExprF b a)
instance (Hashable b) => Hashable1 (Alter b)
instance (Hashable b) => Hashable1 (Binding b)
instance (Hashable b) => Hashable1 (ExprF b)

View File

@@ -1,3 +1,6 @@
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE TemplateHaskell #-}
module Rlp.HindleyMilner
( infer
, check
@@ -8,6 +11,7 @@ module Rlp.HindleyMilner
--------------------------------------------------------------------------------
import Control.Lens hiding (Context', Context, (:<))
import Control.Monad.Errorful
import Control.Monad.State
import Data.Text qualified as T
import Data.Pretty
import Text.Printf
@@ -23,7 +27,9 @@ import Data.Fix
import Control.Comonad.Cofree
import Compiler.RlpcError
import Rlp.AltSyntax
import Rlp.AltSyntax as Rlp
import Core.Syntax qualified as Core
import Core.Syntax (ExprF(..))
--------------------------------------------------------------------------------
-- | Type error enum.
@@ -70,19 +76,67 @@ instance Hashable Constraint
type Constraints = HashSet Constraint
data PartialJudgement =
PartialJudgement Constraints Context'
data PartialJudgement = PartialJudgement Constraints Context'
deriving (Generic, Show)
deriving (Semigroup, Monoid)
via Generically PartialJudgement
constraints :: Lens' PartialJudgement Constraints
constraints = lens sa sbt where
sa (PartialJudgement cs _) = cs
sbt (PartialJudgement _ g) cs' = PartialJudgement cs' g
assumptions :: Lens' PartialJudgement Context'
assumptions = lens sa sbt where
sa (PartialJudgement _ g) = g
sbt (PartialJudgement cs _) g' = PartialJudgement cs g'
fixCofree :: (Functor f, Functor g)
=> Iso (Fix f) (Fix g) (Cofree f ()) (Cofree g b)
fixCofree = iso sa bt where
sa = foldFix (() :<)
bt (_ :< as) = Fix $ bt <$> as
gather :: Context' -> RlpExpr PsName -> HMError (Type PsName, Constraints)
gather = undefined
data TypeState t m = TypeState
{ _tsUnique :: Int
, _tsMemo :: HashMap t m
}
deriving Show
makeLenses ''TypeState
type TC t = State (TypeState t (Type PsName, PartialJudgement))
(Type PsName, PartialJudgement)
freshTv :: State (TypeState t m) (Type PsName)
freshTv = do
n <- use tsUnique
tsUnique %= succ
pure . VarT $ "$a" <> T.pack (show n)
memoisedTC :: (Hashable a) => (a -> TC a) -> a -> TC a
memoisedTC k a = do
m <- use tsMemo
r <- k a
tsMemo . at a %= \case
Just c -> Just c
Nothing -> Just r
pure r
gather :: Fix (RlpExprF PsName) -> TC (Fix (RlpExprF PsName))
gather (Fix (InL (Core.LitF (Core.IntL _)))) =
pure (ConT "Int#", mempty)
gather (Fix (InL (Core.VarF n))) = do
tv <- freshTv
let j = mempty & assumptions .~ H.singleton n tv
pure (tv, j)
gather (Fix (InL (Core.AppF f x))) = do
tv <- freshTv
(tf,j) <- memoisedTC gather f
(tx,j') <- memoisedTC gather x
let j'' = mempty & constraints .~ S.singleton (Equality tf $ tx :-> tv)
pure (tv, j <> j' <> j'')