Add lock and unlock operations similar to cubicaltt

examples/Lock.ctt

@@ -1,12 +1,19 @@
 module Lock where
 
-x : U = U
-w : U = U
+Pt : U = (X : U) * X
+
+lock Pt
+
+foo (A : Pt) : U = U
+
+bar (B : Pt) (_ : foo B) : U = U
 
-lock x w for
-  y : U = x
-  q : Path U y x = \_. x
-  -- q : Path U U x = \_. x -- does not type check
+unlock Pt
+
+
+
+x : U = U
 
+lock x
 
-p : Path U x U = \_. U
+-- p : Path U U x = \_. x

postt.cabal

@@ -76,6 +76,7 @@ executable postt
       , OverloadedStrings
       , UndecidableInstances
       , DerivingVia
+      , MultiWayIf
 
     build-depends:
         array

src/PosTT/Errors.hs

@@ -29,3 +29,14 @@ data TypeError where
   TypeErrorConArgCount :: SrcSpan -> Name -> Int -> Int -> TypeError
   TypeErrorInvalidSplit :: SrcSpan -> Tm -> [Name] -> [Name] -> TypeError
   TypeErrorHSplitCompat :: Tm -> SrcSpan -> Tm -> Tm -> ConvError -> TypeError
+  TypeErrorCollection :: [TypeError] -> TypeError
+
+instance Semigroup TypeError where
+  TypeErrorCollection es <> TypeErrorCollection es' = TypeErrorCollection (es ++ es')
+  TypeErrorCollection es <> e                       = TypeErrorCollection (es ++ [e])
+  e                      <> TypeErrorCollection es' = TypeErrorCollection (e  :  es')
+  e                      <> e'                      = TypeErrorCollection [e, e']
+
+instance Monoid TypeError where
+  mempty = TypeErrorCollection []
+

src/PosTT/Eval.hs

@@ -26,7 +26,6 @@ import PosTT.Poset
 lookupFib :: AtStage (Env -> Name -> Val)
 lookupFib (EnvFib _ y v)     x | y == x = v
 lookupFib ρ@(EnvDef _ y t _) x | y == x = eval ρ t -- recursive definition
-lookupFib (EnvLock _ y)      x | y == x = VVar x
 lookupFib (EnvCons ρ _ _)    x = lookupFib ρ x
 
 lookupInt :: Env -> Gen -> VI
@@ -47,7 +46,7 @@ closedEval = bindStage terminalStage $ eval EmptyEnv
 eval :: AtStage (Env -> Tm -> Val)
 eval rho = \case
   U            -> VU
-  Var x        -> rho `lookupFib` x
+  Var x        -> if locked x then VVar x else rho `lookupFib` x
   Let d t ty s -> eval (EnvDef rho d t ty) s
 
   Pi a b  -> VPi (eval rho a) (evalBinder rho b)
@@ -716,7 +715,6 @@ instance Restrictable EnvEntry where
     EntryFib v    -> EntryFib (v @ f)
     EntryDef t ty -> EntryDef t ty
     EntryInt r    -> EntryInt (r @ f)
-    EntryLock     -> EntryLock
 
 instance Restrictable a => Restrictable [a] where
   type Alt [a] = [Alt a]

src/PosTT/Frontend/Exp.cf

@@ -3,7 +3,7 @@ entrypoints Module, Exp ;
 comment "--" ;
 comment "{-" "-}" ;
 
-layout "where", "let", "split", "for";
+layout "where", "let", "split";
 layout stop "in" ;
 -- Do not use layout toplevel as it makes pExp fail!
 
@@ -12,10 +12,11 @@ Module.   Module ::= "module" MIdent "where" "{" [Imp] [Decl] "}" ;
 Import.   Imp ::= "import" MIdent ;
 separator Imp ";" ;
 
-DeclDef.   Decl ::= AIdent [Tele] ":" Exp "=" Body ;
-DeclData.  Decl ::= "data" AIdent [Tele] ":" "U" "=" [Label] ;
-DeclLock.  Decl ::= "lock" [AIdent] "for" "{" [Decl] "}" ;
-separator  Decl ";" ;
+DeclDef.    Decl ::= AIdent [Tele] ":" Exp "=" Body ;
+DeclData.   Decl ::= "data" AIdent [Tele] ":" "U" "=" [Label] ;
+DeclLock.   Decl ::= "lock" [AIdent] ;
+DeclUnlock. Decl ::= "unlock" [AIdent] ;
+separator   Decl ";" ;
 
 NoSplit. Body ::= ExpWhere ;
 Split.   Body ::= "split" "{" [Branch] "}" ;

src/PosTT/Frontend/PreTerms.hs

@@ -88,7 +88,7 @@ data HLabel = HLabel SrcSpan Name Tel [Gen] (Sys PTm) deriving Show
 
 data Sys a = Sys SrcSpan [([(ITm, ITm)], a)] deriving Show
 
-data Decl = Decl SrcSpan Name PTm PTy | DeclLock SrcSpan [Name] [Decl]
+data Decl = Decl SrcSpan Name PTm PTy | DeclLock SrcSpan [Name] | DeclUnlock SrcSpan [Name]
 
 app :: SrcSpan -> PTm -> PTm -> PTm
 app _  (Con ss c as)  v = Con ss c (as ++ [v])

src/PosTT/Frontend/ScopeChecker.hs

@@ -263,10 +263,12 @@ checkDecl (DeclData ss id ts cs) = do
       let bd = foldr (\(ss', x, _) -> P.Lam ss' x Nothing) d ts'
 
       return ((id', (idss, Variable)):[ (c, (ssC, Constructor)) | (c, ssC) <- cs' ], P.Decl ss id' bd ty)
-checkDecl (DeclLock ss ids decls) = do
+checkDecl (DeclLock ss ids) = do
   ids' <- mapM checkDef ids
-  (env, decls') <- checkDecls decls
-  return (env, P.DeclLock ss ids' decls')
+  asks (, P.DeclLock ss ids')
+checkDecl (DeclUnlock ss ids) = do
+  ids' <- mapM checkDef ids
+  asks (, P.DeclUnlock ss ids')
 
 bindDecl :: Decl -> (P.Decl -> ScopeChecker a) -> ScopeChecker a
 bindDecl d k = checkDecl d >>= \(ids, d') -> local (ids ++) (k d')

src/PosTT/TypeChecker.hs

@@ -1,11 +1,13 @@
 module PosTT.TypeChecker where
 
+import           Control.Applicative
 import           Control.Monad.Reader
 import           Control.Monad.Writer (MonadWriter(..), Writer, runWriter)
 import           Control.Monad.Except
 
 import           Data.Bifunctor (first)
 import           Data.Either (fromRight)
+import           Data.Either.Extra (maybeToEither)
 import           Data.List (sortOn)
 import           Data.Tuple.Extra (uncurry3, first3, second3)
 
@@ -14,7 +16,7 @@ import           PosTT.Conversion
 import           PosTT.Errors
 import           PosTT.Eval
 import qualified PosTT.Frontend.PreTerms as P
-import           PosTT.Frontend.PreTerms (PTm)
+import           PosTT.Frontend.PreTerms (PTm, PTy)
 import           PosTT.Poset
 import           PosTT.Pretty
 import           PosTT.Quotation
@@ -32,7 +34,7 @@ emptyCxt :: Cxt
 emptyCxt = Cxt EmptyEnv [] [] Nothing
 
 newtype TypeChecker a = TypeChecker { unTypeChecker :: ReaderT Cxt (ExceptT TypeError (Writer [String])) a }
-  deriving (Functor, Applicative, Monad, MonadReader Cxt, MonadWriter [String], MonadError TypeError)
+  deriving (Functor, Applicative, Alternative, Monad, MonadReader Cxt, MonadWriter [String], MonadError TypeError)
 
 instance MonadFail TypeChecker where
   fail :: String -> TypeChecker a
@@ -46,11 +48,8 @@ runTC cxt ma = bindStage terminalStage $ runWriter $ runExceptT $ runReaderT (un
 ---- Utility Functions
 
 -- | Extends context Γ with a definition to a context Γ,(x=t:a)
-extDef :: (Name, Tm, Ty, VTy) -> Cxt -> Cxt
-extDef (x, t, a, va) (Cxt ρ ts is pos) = Cxt (EnvDef ρ x t a) ((x, va):ts) is pos
-
-extLock :: Name -> Cxt -> Cxt
-extLock x (Cxt ρ ts is pos) = Cxt (EnvLock ρ x) ts is pos
+extDef :: (Name, Tm, Ty) -> Cxt -> Cxt
+extDef (x, t, a) (Cxt ρ ts is pos) = Cxt (EnvDef ρ x t a) ts is pos
 
 -- | Extends context Γ with a (fibrant) value to a context Γ,(x=v:a)
 extFib :: Name -> Val -> VTy -> Cxt -> Cxt
@@ -97,10 +96,20 @@ checkIntVar i = asks (elem i . intVars) >>= \case
   True  -> return (IVar i)
   False -> fail $ show i ++ " is not an interval variable!"
 
-checkFibVar :: Name -> TypeChecker VTy
-checkFibVar x = asks (lookup x . types) >>= \case
+lookupFibVar :: AtStage (Name -> TypeChecker VTy)
+lookupFibVar x = asks (lookup x . types) >>= \case
   Just t  -> return t
-  Nothing -> fail $ show x ++ " is not a fibrant variable!"
+  Nothing -> fail $ show x ++ " is not a fibrant definition!"
+
+lookupDefType :: AtStage (Name -> TypeChecker VTy)
+lookupDefType x = asks env >>= (`go` x)
+  where
+    go (EnvDef ρ y _ t) x | y == x = return (eval ρ t)
+    go (EnvCons ρ _ _)  x = go ρ x
+    go EmptyEnv         x = fail $ show x ++ " is not a fibrant (non-definition) variable!"
+
+checkFibVar :: AtStage (Name -> TypeChecker VTy)
+checkFibVar x = lookupFibVar x <|> lookupDefType x
 
 
 ---- Evaluation and Quotation using context
@@ -175,7 +184,7 @@ check = flip $ \ty -> atArgPos $ \case
   P.Let _ x s a t -> do
     (a', va) <- checkAndEval a VU
     s' <- check s va
-    Let x s' a' <$> local (extDef (x, s', a', va)) (check t ty)
+    Let x s' a' <$> local (extDef (x, s', a')) (check t ty)
   P.U _ -> do
     () <- isU ty
     return U
@@ -440,8 +449,8 @@ checkAndEvalCof eqs = do
 --------------------------------------------------------------------------------
 ---- Checking lists of declarations
 
-checkDecl :: AtStage (P.Decl -> TypeChecker [(Name, Tm, Ty, VTy)])
-checkDecl (P.Decl _ x b t) = do
+checkDecl :: AtStage (Name -> PTm -> PTy -> TypeChecker (Name, Tm, Ty))
+checkDecl x b t = do
   tell ["\nChecking Definition: " ++ show x]
 
   (t', vt) <- checkAndEval t VU
@@ -450,15 +459,15 @@ checkDecl (P.Decl _ x b t) = do
   tell [prettyVal vt]
   tell [pretty b']
 
-  return [(x, b', t', vt)]
-checkDecl (P.DeclLock _ ids decls) =
-  local (\cxt -> foldr extLock cxt ids) (checkDecls decls)
+  return (x, b', t')
 
-checkDecls :: AtStage ([P.Decl] -> TypeChecker [(Name, Tm, Ty, VTy)])
-checkDecls []     = return []
-checkDecls (d:ds) = do
-  decls <- checkDecl d
-  (decls ++) <$> local (flip (foldr extDef) decls) (checkDecls ds)
+checkDecls :: AtStage ([P.Decl] -> TypeChecker [(Name, Tm, Ty)])
+checkDecls []                     = return []
+checkDecls (P.DeclLock   _ xs:ds) = lock xs (checkDecls ds)
+checkDecls (P.DeclUnlock _ xs:ds) = unlock xs (checkDecls ds)
+checkDecls (P.Decl _ x b t:ds)    = do
+  d <- checkDecl x b t
+  (d:) <$> local (extDef d) (checkDecls ds)
 
 checkDeclsCxt :: [P.Decl] -> (Either TypeError Cxt, [String])
 checkDeclsCxt decls = runTC emptyCxt $ asks (foldr extDef) <*> checkDecls decls

src/PosTT/Values.hs

@@ -1,15 +1,17 @@
 -- | Representations of Values
 module PosTT.Values where
 
-import Algebra.Lattice
+import           Algebra.Lattice
 
-import Data.Bifunctor
-import Data.List (uncons)
-import Data.Either (isRight)
+import           Data.Bifunctor
+import           Data.Either (isRight)
+import           Data.List (uncons)
+import           Data.Set (Set)
+import qualified Data.Set as S
 
-import PosTT.Common
-import PosTT.Terms
-import PosTT.Errors
+import           PosTT.Common
+import           PosTT.Terms
+import           PosTT.Errors
 import qualified PosTT.Common as M
 
 
@@ -225,10 +227,10 @@ instance InfSemilattice VCof where
 
 ---- Stages
 
-data Stage = Stage { gens :: !NameStore, cof :: !VCof, names :: !NameStore }
+data Stage = Stage { gens :: !NameStore, cof :: !VCof, names :: !NameStore, lockedNames :: !(Set Name) }
 
 terminalStage :: Stage
-terminalStage = Stage M.emptyStore top M.emptyStore
+terminalStage = Stage M.emptyStore top M.emptyStore S.empty
 
 type AtStage a = (?s :: Stage) => a
 
@@ -244,6 +246,12 @@ sExtGen n s = s { gens = addNameStore n (gens s) }
 sExtCof :: VCof -> Stage -> Stage
 sExtCof φ s = s { cof = φ /\ cof s}
 
+sLock :: Name -> Stage -> Stage
+sLock x s = s { lockedNames = S.insert x (lockedNames s) }
+
+sUnlock :: Name -> Stage -> Stage
+sUnlock x s = s { lockedNames = S.delete x (lockedNames s) }
+
 extName :: AtStage (Name -> AtStage a -> a)
 extName n = bindStage (sExtName n ?s)
 
@@ -253,6 +261,15 @@ extGen n = bindStage (sExtGen n ?s)
 extCof :: AtStage (VCof -> AtStage a -> a)
 extCof φ = bindStage (sExtCof φ ?s)
 
+lock :: AtStage ([Name] -> AtStage a -> a)
+lock xs = bindStage (foldr sLock ?s xs)
+
+unlock :: AtStage ([Name] -> AtStage a -> a)
+unlock xs = bindStage (foldr sUnlock ?s xs)
+
+locked :: AtStage (Name -> Bool)
+locked x = x `S.member` lockedNames ?s
+
 
 ---- Fresh Names/Generators
 
@@ -305,7 +322,7 @@ re = (@ IdRestr)
 
 type Env = [(Name, EnvEntry)]
 
-data EnvEntry = EntryDef !Tm !Ty | EntryFib !Val | EntryInt !VI | EntryLock
+data EnvEntry = EntryDef !Tm !Ty | EntryFib !Val | EntryInt !VI
 
 pattern EmptyEnv :: Env
 pattern EmptyEnv = []
@@ -316,9 +333,6 @@ pattern EnvCons rho x e <- (uncons -> Just ((x, e), rho))
 
 {-# COMPLETE EmptyEnv, EnvCons #-}
 
-pattern EnvLock :: Env -> Name -> Env
-pattern EnvLock rho x = (x, EntryLock):rho
-
 pattern EnvFib :: Env -> Name -> Val -> Env
 pattern EnvFib rho x v   = (x, EntryFib v):rho