From 9e7d4b9590ab7131f693870cb279c37883687854 Mon Sep 17 00:00:00 2001 From: Daniel Gustafsson Date: Sun, 8 May 2016 21:26:04 +0200 Subject: [PATCH 1/3] start to type propagation --- Ling/Check/Core.hs | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/Ling/Check/Core.hs b/Ling/Check/Core.hs index abece3e..7f2ffa9 100644 --- a/Ling/Check/Core.hs +++ b/Ling/Check/Core.hs @@ -351,10 +351,33 @@ inferProcTyp cds proc = do checkTyp :: Typ -> TC () checkTyp = checkTerm TTyp +checkPiLam :: (VarDec, Typ) -> (VarDec, Term) -> TC () +checkPiLam (at, bt) (arg, t) = do + debug . unlines $ + ["Checking function" + ] + -- somehow check that at and arg agree on the same type + let bt' = bt -- should be updated to use arg name + checkVarDec arg (checkTerm bt' t) + +checkProtoProc :: [RSession] -> ([ChanDec], Proc) -> TC () +checkProtoProc ss (cs, proc) = do + let cs' = cs --should update RSession in cs with ss + ss' <- inferProcTyp cs' proc + debug . unlines $ + ["Checking process term" + ,"exp: " ++ pretty (Proc cs proc) + ,"expected: " ++ pretty (TProto ss) + ,"inferred: " ++ pretty ss' + ] + checkTypeEquivalence (TProto ss) ss' + checkMaybeTyp :: Maybe Typ -> TC () checkMaybeTyp = checkMaybeTerm TTyp checkTerm :: Typ -> Term -> TC () +checkTerm (TFun arg s) (Lam arg' t) = checkPiLam (arg,s) (arg',t) +checkTerm (TProto ss) (Proc cs proc) = checkProtoProc ss (cs,proc) checkTerm expectedTyp e = do inferredTyp <- inferTerm e debug . unlines $ From 63d718eeefa72b8c1c9d49d22fef655bf51cba11 Mon Sep 17 00:00:00 2001 From: Daniel Gustafsson Date: Mon, 9 May 2016 21:54:47 +0200 Subject: [PATCH 2/3] Change TCEnv to store information for type propagation --- Ling/Check/Base.hs | 3 ++- Ling/Check/Core.hs | 25 ++++++++++++++++++++----- 2 files changed, 22 insertions(+), 6 deletions(-) diff --git a/Ling/Check/Base.hs b/Ling/Check/Base.hs index 28be827..54b7e2d 100644 --- a/Ling/Check/Base.hs +++ b/Ling/Check/Base.hs @@ -61,12 +61,13 @@ data TCEnv = TCEnv -- ^ Datatypes definitions , _ctyps :: Map ConName DataTypeName -- ^ Data constructor ↦ type name + , _cses :: Map Channel RSession } makeLenses ''TCEnv emptyTCEnv :: TCEnv -emptyTCEnv = TCEnv defaultTCOpts ø ø ø ø +emptyTCEnv = TCEnv defaultTCOpts ø ø ø ø ø tcEqEnv :: MonadReader TCEnv m => m EqEnv tcEqEnv = eqEnv edefs diff --git a/Ling/Check/Core.hs b/Ling/Check/Core.hs index 7f2ffa9..457c6dd 100644 --- a/Ling/Check/Core.hs +++ b/Ling/Check/Core.hs @@ -12,6 +12,7 @@ import Ling.Print import Ling.Proc import Ling.Proto import Ling.Reduce +import qualified Ling.Rename as R import Ling.Scoped import Ling.Session import Ling.Prelude hiding (subst1) @@ -356,14 +357,28 @@ checkPiLam (at, bt) (arg, t) = do debug . unlines $ ["Checking function" ] - -- somehow check that at and arg agree on the same type - let bt' = bt -- should be updated to use arg name - checkVarDec arg (checkTerm bt' t) + -- lot's of code for the Maybe type, I don't know enough about lens to + -- reduce the LOC here + at' <- case at ^. argBody of + Nothing -> error "Pi type should have a domain" + Just t -> return t + case arg ^. argBody of + Nothing -> return () + Just ty -> checkTypeEquivalence at' ty + let bt' = R.rename1 (at ^. argName, arg ^. argName) bt + arg' = arg & argBody .~ (at ^. argBody) + checkVarDec arg' (checkTerm bt' t) checkProtoProc :: [RSession] -> ([ChanDec], Proc) -> TC () checkProtoProc ss (cs, proc) = do - let cs' = cs --should update RSession in cs with ss - ss' <- inferProcTyp cs' proc + assert (length ss == length cs) + [ "Checking process term" + , "exp: " ++ pretty (Proc cs proc) + , "expected: " ++ pretty (TProto ss) + , "The amount of sessions don't match the amount of channels" + ] + let chanSessions = l2m $ zip (map (^. cdChan) cs) ss + ss' <- local (cses .~ chanSessions) $ inferProcTyp cs proc debug . unlines $ ["Checking process term" ,"exp: " ++ pretty (Proc cs proc) From 1ae20096df9734ec9351f0ca8836f906bbdbdebd Mon Sep 17 00:00:00 2001 From: Daniel Gustafsson Date: Wed, 18 May 2016 14:09:25 +0200 Subject: [PATCH 3/3] Change checkPref to take a TC Proto continuation rather than a Proto --- Ling/Check/Base.hs | 12 +++++++++++- Ling/Check/Core.hs | 23 ++++++++++++++--------- 2 files changed, 25 insertions(+), 10 deletions(-) diff --git a/Ling/Check/Base.hs b/Ling/Check/Base.hs index 54b7e2d..7867d67 100644 --- a/Ling/Check/Base.hs +++ b/Ling/Check/Base.hs @@ -228,12 +228,22 @@ conTypeName c = maybe (tcError $ "No such constructor " ++ pretty c) return =<< view (ctyps . at c) debugCheck :: MonadTC m => (Err a -> String) -> Endom (m a) -debugCheck fmt k = +{-debugCheck fmt k = (do x <- k debug (fmt (Ok x)) return x ) `catchError` \err -> do debug (fmt (Bad err)) + throwError err-} +debugCheck fmt = debugCheckM (pure . fmt) + +debugCheckM :: MonadTC m => (Err a -> m String) -> Endom (m a) +debugCheckM fmt k = + (do x <- k + debug =<< fmt (Ok x) + return x + ) `catchError` \err -> + do debug =<< fmt (Bad err) throwError err errorScope :: (Print name, MonadError TCErr m) => name -> Endom (m a) diff --git a/Ling/Check/Core.hs b/Ling/Check/Core.hs index 457c6dd..42ae1d1 100644 --- a/Ling/Check/Core.hs +++ b/Ling/Check/Core.hs @@ -53,7 +53,7 @@ checkProc proc0 = do checkPrefWellFormness pref let defs = acts ^. each . actDefs pushDefs . Scoped ø defs <$> - (checkPref pref =<< + (checkPref pref $ checkDefs defs (checkVarDecs (acts >>= actVarDecs) (checkProc proc1))) @@ -88,12 +88,13 @@ sendRecvSession = \case checkMaybeTyp typ $> (c, (pure .) $ depRecv arg) _ -> tcError "typeSendRecv: Not Send/Recv" -checkPref :: Pref -> Proto -> TC Proto -checkPref (Prll pref) proto +checkPref :: Pref -> Endom (TC Proto) +checkPref (Prll pref) kont | null pref = - return proto + kont | all isSendRecv pref = do css <- mapM sendRecvSession pref + proto <- kont proto' <- protoSendRecv css proto when (length pref >= 1) $ debug . unlines $ @@ -104,7 +105,7 @@ checkPref (Prll pref) proto ] ++ prettyProto proto' return proto' | [act] <- pref = - checkAct act proto + checkAct act kont | otherwise = tcError $ "Unsupported parallel prefix " ++ pretty pref @@ -235,9 +236,9 @@ or classically: Γ(c{c0,...,cN} P)(d) = (Γ(P)/(c0,...,cN))(d) -} -checkAct :: Act -> Proto -> TC Proto -checkAct act proto = - debugCheck (\proto' -> unlines $ +checkAct :: Act -> Endom (TC Proto) +checkAct act kont = + debugCheckM (\proto' -> kont >>= \proto -> pure . unlines $ [ "Checking act `" ++ pretty act ++ "`" , "Inferred protocol for the sub-process:" ] ++ prettyProto proto ++ @@ -246,10 +247,12 @@ checkAct act proto = case act of Nu anns newpatt -> do for_ anns $ checkTerm allocationTyp + proto <- kont checkNewPatt proto newpatt Split c pat -> case pat ^? _ArrayCs of Just (k, dOSs) -> do + proto <- kont assertAbsent proto c for_ dOSs $ checkChanDec proto let ds = dOSs ^.. each . cdChan @@ -267,12 +270,14 @@ checkAct act proto = Recv{} -> error "IMPOSSIBLE: use checkPref instead" Ax s cs -> do proto' <- checkAx s cs + proto <- kont return $ proto' `dotProto` proto LetA{} -> - return proto + kont At e p -> do ss <- unTProto =<< inferTerm e proto' <- checkCPatt (wrapSessions ss) p + proto <- kont return $ proto' `dotProto` proto unTProto :: Term -> TC Sessions