From eca712d0d7204e063158becee02cb0cef7598dd4 Mon Sep 17 00:00:00 2001 From: crumbtoo Date: Wed, 20 Mar 2024 18:58:44 -0600 Subject: [PATCH] something --- app/Server.hs | 32 +++++++++++------- src/Rlp/AltSyntax.hs | 3 ++ src/Rlp/HindleyMilner.hs | 60 +++++++++++++++++++++------------- src/Rlp/HindleyMilner/Types.hs | 3 +- 4 files changed, 63 insertions(+), 35 deletions(-) diff --git a/app/Server.hs b/app/Server.hs index 339f57f..7d7a9d7 100644 --- a/app/Server.hs +++ b/app/Server.hs @@ -11,7 +11,7 @@ import Data.Text.Encoding qualified as T import Data.Text (Text) import Data.Text qualified as T import Data.Text.IO qualified as T -import Data.Pretty +import Data.Pretty hiding (annotate) import Data.Aeson import Data.Function import Control.Arrow @@ -43,14 +43,16 @@ application :: WS.ServerApp application pending = do WS.acceptRequest pending >>= talk -newtype Command = Annotate Text +data Command = Annotate Text + | PartiallyAnnotate Text deriving Show instance FromJSON Command where parseJSON = withObject "command object" $ \v -> do cmd :: Text <- v .: "command" case cmd of - "annotate" -> Annotate <$> v .: "source" + "annotate" -> Annotate <$> v .: "source" + "partially-annotate" -> PartiallyAnnotate <$> v .: "source" _ -> empty data Response = Annotated Value @@ -75,16 +77,24 @@ doCommand conn c = do respond :: Command -> Response respond (Annotate s) = s & (parseRlpProgR >=> typeCheckRlpProgR) - & fmap (\p -> p ^.. programDecls . each . _FunD - <&> serialiseSc) + & fmap (\p -> p ^.. funDs + <&> \sc -> serialiseSc (sc & _3 . mapped %~ rout @String)) & runRLPCJsonDef & Annotated - where - serialiseSc (n,as,e) = object - [ "name" .= n - , "args" .= as - , "body" .= let rootType = extract e - in serialiseAnnotated (e <&> prettyVars rootType) ] + +showPartialAnn = undefined + +funDs :: Traversal' (Program b a) (b, [Pat b], a) +funDs = programDecls . each . _FunD + +serialiseSc :: ToJSON a + => (PsName, [Pat PsName], Cofree (RlpExprF PsName) a) + -> Value +serialiseSc (n,as,e) = object + [ "name" .= n + , "args" .= as + , "body" .= let rootType = extract e + in serialiseAnnotated (e <&> prettyVars rootType) ] serialiseAnnotated :: Cofree (RlpExprF PsName) (Type PsName) -> Value diff --git a/src/Rlp/AltSyntax.hs b/src/Rlp/AltSyntax.hs index 7207613..2f474a2 100644 --- a/src/Rlp/AltSyntax.hs +++ b/src/Rlp/AltSyntax.hs @@ -6,6 +6,7 @@ module Rlp.AltSyntax , RlpExprF, RlpExpr, Binding(..), Alter(..) , DataCon(..), Type(..) , pattern IntT + , Core.Rec(..) , AnnotatedRlpExpr, TypedRlpExpr , TypeF(..) @@ -179,6 +180,8 @@ instance (Out b) => Out (Type b) where outPrec p (AppT f x) = maybeParens (p>appPrec) $ outPrec appPrec f <+> outPrec appPrec1 x outPrec p FunT = maybeParens (p>0) "->" + outPrec p (ForallT x m) = maybeParens (p>0) $ + hsep [ "∀", ttext x, outPrec 0 m ] instance (Out b) => Out (Pat b) where outPrec p (VarP b) = outPrec p b diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs index aa1d568..0be2e93 100644 --- a/src/Rlp/HindleyMilner.hs +++ b/src/Rlp/HindleyMilner.hs @@ -5,6 +5,7 @@ module Rlp.HindleyMilner , annotate , TypeError(..) , runHM' + , liftHM , HM , prettyVars , prettyVars' @@ -29,6 +30,7 @@ import Data.Hashable import Data.HashMap.Strict (HashMap) import Data.HashMap.Strict qualified as H import Data.HashSet (HashSet) +import Data.HashSet.Lens import Data.HashSet qualified as S import Data.Maybe (fromMaybe) import Data.Traversable @@ -95,6 +97,15 @@ gather' = \case t = foldr (:->) te tbs pure (t,j) + Finr (LetEF NonRec [VarB (VarP x) y] e) -> do + (ty,jy) <- gather y + (te,je) <- gather e + traceM $ "ty: " <> show ty + traceM $ "jy: " <> show jy + traceM $ "te: " <> show te + traceM $ "je: " <> show je + undefined + -- Finl (LamF [b] e) -> do -- tb <- freshTv -- (te,je) <- gather e @@ -104,6 +115,12 @@ gather' = \case -- t = tb :-> te -- pure (t,j) +generalise :: Context -> Type PsName -> Type PsName +generalise g t = ifoldr (\n _ s -> ForallT n s) t vs + where + vs = H.difference (freeVariables t ^. hashMap) + (g ^. contextTyVars) + unify :: [Constraint] -> HM [(PsName, Type PsName)] unify [] = pure mempty @@ -124,6 +141,7 @@ unify (Equality (VarT s) t : cs) -- swap unify (Equality s (VarT t) : cs) = unify (Equality (VarT t) s : cs) +-- failure! unify (Equality s t : _) = addFatal $ TyErrCouldNotUnify s t annotate :: RlpExpr PsName @@ -135,10 +153,6 @@ assocs f [] = pure [] assocs f ((k,v):xs) = (\v' xs' -> (k,v') : xs') <$> indexed f k v <*> assocs f xs -traceSubst k v t = trace ("subst " <> show' k <> " " <> show' v <> " " <> show' t) - $ 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 = @@ -166,23 +180,23 @@ infer g0 e = do infer1 :: Context -> RlpExpr PsName -> HM (Type PsName) infer1 g = fmap extract . infer g -unionContextWithKeyM :: Monad m - => (PsName -> Type PsName -> Type PsName - -> m (Type PsName)) - -> Context -> Context -> m Context -unionContextWithKeyM f a b = Context <$> unionWithKeyM f a' b' - where - a' = a ^. contextVars - b' = b ^. contextVars +-- unionContextWithKeyM :: Monad m +-- => (PsName -> Type PsName -> Type PsName +-- -> m (Type PsName)) +-- -> Context -> Context -> m Context +-- unionContextWithKeyM f a b = Context <$> unionWithKeyM f a' b' +-- where +-- a' = a ^. contextVars +-- b' = b ^. contextVars -unionWithKeyM :: forall m k v. (Eq k, Hashable k, Monad m) - => (k -> v -> v -> m v) -> HashMap k v -> HashMap k v - -> m (HashMap k v) -unionWithKeyM f a b = sequenceA $ H.unionWithKey f' ma mb - where - f' k x y = join $ liftA2 (f k) x y - ma = fmap (pure @m) a - mb = fmap (pure @m) b +-- unionWithKeyM :: forall m k v. (Eq k, Hashable k, Monad m) +-- => (k -> v -> v -> m v) -> HashMap k v -> HashMap k v +-- -> m (HashMap k v) +-- unionWithKeyM f a b = sequenceA $ H.unionWithKey f' ma mb +-- where +-- f' k x y = join $ liftA2 (f k) x y +-- ma = fmap (pure @m) a +-- mb = fmap (pure @m) b -- solve :: RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName)) -- solve = solve' mempty @@ -213,8 +227,8 @@ fixtend :: Functor f => (f (Fix f) -> b) -> Fix f -> Cofree f b fixtend c (Fix f) = c f :< fmap (fixtend c) f buildInitialContext :: Program PsName a -> Context -buildInitialContext = - Context . H.fromList . toListOf (programDecls . each . _TySigD) +buildInitialContext = const mempty + -- Context . H.fromList . toListOf (programDecls . each . _TySigD) typeCheckRlpProgR :: (Monad m) => Program PsName (RlpExpr PsName) @@ -241,7 +255,7 @@ liftHM = liftEither . runHM' freeVariables :: Type PsName -> HashSet PsName freeVariables = cata \case VarTF x -> S.singleton x - ForallTF x m -> m `S.difference` S.singleton x + ForallTF x m -> S.delete x m vs -> fold vs boundVariables :: Type PsName -> HashSet PsName diff --git a/src/Rlp/HindleyMilner/Types.hs b/src/Rlp/HindleyMilner/Types.hs index db08d19..c221f3d 100644 --- a/src/Rlp/HindleyMilner/Types.hs +++ b/src/Rlp/HindleyMilner/Types.hs @@ -26,8 +26,9 @@ import Compiler.RlpcError import Rlp.AltSyntax -------------------------------------------------------------------------------- -newtype Context = Context +data Context = Context { _contextVars :: HashMap PsName (Type PsName) + , _contextTyVars :: HashMap PsName (Type PsName) } deriving (Show, Generic) deriving (Semigroup, Monoid)