Permalink
Browse files

Linearity experiment

  • Loading branch information...
Edwin Brady
Edwin Brady committed May 25, 2011
1 parent c91de60 commit 07e10a7844bb8b4f4ccfac4344b05d5560a5b95e
Showing with 49 additions and 6 deletions.
  1. +4 −0 Ivor/Nobby.lhs
  2. +29 −0 Ivor/TTCore.lhs
  3. +11 −6 Ivor/Typecheck.lhs
  4. +1 −0 Ivor/Values.lhs
  5. +4 −0 Ivor/ViewTerm.lhs
View
@@ -74,6 +74,7 @@ Do the actual evaluation
> where bty = eval stage gamma g ty
> eval stage gamma g (Const x) = (MR (RdConst x))
> eval stage gamma g Star = MR RdStar
+> eval stage gamma g LinStar = MR RdLinStar
> eval stage gamma g Erased = MR RdErased
> eval stage gamma (VG g) (Bind n (B Lambda ty) (Sc sc)) =
> (MR (RdBind n (B Lambda (eval stage gamma (VG g) ty))
@@ -239,6 +240,7 @@ Splice the escapes inside a term
> weakenp i (RdBind n bind sc) = RdBind n (weakenp i bind) (weakenp i sc)
> weakenp i (RdConst x) = RdConst x
> weakenp i RdStar = RdStar
+> weakenp i RdLinStar = RdLinStar
> weakenp i RdErased = RdErased
> weakenp i (RCon t n sp) = RCon t n (fmap (weakenp i) sp)
> weakenp i (RTyCon n sp) = RTyCon n (fmap (weakenp i) sp)
@@ -294,6 +296,7 @@ Splice the escapes inside a term
> instance Quote (Ready Kripke) (Ready Scope) where
> quote' ns (RdConst x) = RdConst x
> quote' ns RdStar = RdStar
+> quote' ns RdLinStar = RdLinStar
> quote' ns RdErased = RdErased
> quote' ns (RdBind n b@(B _ ty) sc)
> = let n' = mkUnique n ns in
@@ -390,6 +393,7 @@ Quotation to eta long normal form. DOESN'T WORK YET!
> forget (RdBind n b (Sc sc)) = Bind n (forget b) (Sc (forget sc))
> forget (RdConst x) = (Const x)
> forget RdStar = Star
+> forget RdLinStar = LinStar
> forget RdErased = Erased
> forget (RCon t c sp) = makeApp (Con t c (size sp)) (fmap forget sp)
> forget (RTyCon c sp) = makeApp (TyCon c (size sp)) (fmap forget sp)
View
@@ -22,6 +22,7 @@ Raw terms are those read in directly from the user, and may be badly typed.
> | RBind Name (Binder Raw) Raw
> | forall c.(Constant c) => RConst !c
> | RStar
+> | RLinStar
> | RInfer -- Term to be inferred by the typechecker
> | RMeta Name -- a metavariable, to be implemented separately
> | RLabel Raw RComputation
@@ -30,6 +31,8 @@ Raw terms are those read in directly from the user, and may be badly typed.
> | RAnnot String -- Debugging hack
> | RFileLoc FilePath Int Raw -- For more helpful type error messages
> | RStage RStage
+> | RLin Raw -- linear value
+> | RLinTy Raw -- linear type
> data RComputation = RComp Name [Raw]
> deriving Eq
@@ -59,6 +62,9 @@ representation of the names
> | Return (TT n)
> | forall c. Constant c => Const !c
> | Star
+> | LinStar
+> | Lin (TT n)
+> | LinTy (TT n)
> | Stage (Stage n)
> | Erased -- Forced, so deleted
@@ -86,6 +92,7 @@ Constants
> data Bind n
> = Lambda
> | Pi
+> | LinPi
> | Let n
> | Hole
> | Guess n
@@ -257,7 +264,10 @@ is dealt with later.
> fmap f (Call c t) = Call (fmap f c) (fmap f t)
> fmap f (Return t) = Return (fmap f t)
> fmap f (Stage t) = Stage (fmap f t)
+> fmap f (Lin t) = Lin (fmap f t)
+> fmap f (LinTy t) = LinTy (fmap f t)
> fmap f Star = Star
+> fmap f LinStar = LinStar
> instance Functor Stage where
> fmap f (Quote t) = Quote (fmap f t)
@@ -319,6 +329,8 @@ Each V is processed with a function taking the context and the index.
> = Call (Comp n (fmap (v' ctx) cs)) (v' ctx t)
> v' ctx (Return t) = Return (v' ctx t)
> v' ctx (Stage t) = Stage (sLift (v' ctx) t)
+> v' ctx (Lin t) = Lin (v' ctx t)
+> v' ctx (LinTy t) = LinTy (v' ctx t)
> v' ctx x = x
> indexise :: Levelled n -> Indexed n
@@ -345,6 +357,8 @@ Same, but for Ps
> = Call (Comp n (fmap (v') cs)) (v' t)
> v' (Return t) = Return (v' t)
> v' (Stage t) = Stage (sLift (v') t)
+> v' (Lin t) = Lin (v' t)
+> v' (LinTy t) = LinTy (v' t)
> v' x = x
FIXME: This needs to rename all duplicated binder names first, otherwise
@@ -397,6 +411,12 @@ we get a duff term when we go back to the indexed version.
> uniqifyAllState (Stage t) =
> do t' <- sLiftM uniqifyAllState t
> return (Stage t')
+> uniqifyAllState (Lin t) =
+> do t' <- uniqifyAllState t
+> return (Lin t')
+> uniqifyAllState (LinTy t) =
+> do t' <- uniqifyAllState t
+> return (LinTy t')
> uniqifyAllState x = return $ x
> uniqifyAllStateB (B Lambda ty) =
@@ -405,6 +425,9 @@ we get a duff term when we go back to the indexed version.
> uniqifyAllStateB (B Pi ty) =
> do ty' <- uniqifyAllState ty
> return (B Pi ty')
+> uniqifyAllStateB (B LinPi ty) =
+> do ty' <- uniqifyAllState ty
+> return (B LinPi ty')
> uniqifyAllStateB (B Hole ty) =
> do ty' <- uniqifyAllState ty
> return (B Hole ty')
@@ -714,6 +737,7 @@ Apply a function to a list of arguments
> Just x' -> x'==y
> Nothing -> False
> (==) RStar RStar = True
+> (==) RLinStar RLinStar = True
> (==) (RLabel t (RComp n cs)) (RLabel t' (RComp n' cs')) =
> t==t' && n==n' && cs == cs'
> (==) (RCall (RComp n cs) t) (RCall (RComp n' cs') t') =
@@ -747,6 +771,7 @@ Eta equality:
> Just x' -> x'==y
> Nothing -> False
> (==) Star Star = True
+> (==) LinStar LinStar = True
> (==) (Label t (Comp n cs)) (Label t' (Comp n' cs')) =
> t==t' -- && n==n' && cs == cs'
> (==) (Call (Comp n cs) t) (Call (Comp n' cs') t') =
@@ -808,6 +833,7 @@ Eta equality:
> fPrec _ (RStage (REscape t)) = "~" ++ fPrec 0 t
> fPrec _ (RConst x) = show x
> fPrec _ (RStar) = "*"
+> fPrec _ (RLinStar) = "!*"
> fPrec _ (RInfer) = "_"
> fPrec _ (RMeta n) = "[?"++forget n++"]"
> fPrec p (RFileLoc f l t) = fPrec p t
@@ -873,6 +899,7 @@ Eta equality:
> forgetTT (Stage t) = RStage (forget t)
> forgetTT (Const x) = RConst x
> forgetTT Star = RStar
+> forgetTT LinStar = RLinStar
> forgetTT Erased = RInfer
> instance (Show n) => Forget (TT n) Raw where
@@ -915,6 +942,7 @@ Eta equality:
> forgetTT (Stage t) = RStage (forget t)
> forgetTT (Const x) = RConst x
> forgetTT Star = RStar
+> forgetTT LinStar = RLinStar
> forgetTT Erased = RInfer
> instance Show n => Forget (Stage n) RStage where
@@ -1042,4 +1070,5 @@ Some handy gadgets for Raw terms
> pToV2 v p (Stage t) = Sc $ Stage (sLift (getSc.(pToV2 v p)) t)
> pToV2 v p (Const x) = Sc (Const x)
> pToV2 v p Star = Sc Star
+> pToV2 v p LinStar = Sc LinStar
> pToV2 v p Erased = Sc Erased
View
@@ -416,6 +416,7 @@ typechecker...
> return (rv,rt)
> tc env lvl (RConst x) _ = lift $ tcConst x
> tc env lvl RStar _ = return (Ind Star, Ind Star)
+> tc env lvl RLinStar _ = return (Ind LinStar, Ind Star)
> tc env lvl (RFileLoc f l t) exp =
> do (next, infer, bindings, errs, mvs, fc) <- get
> put (next, infer, bindings, errs, mvs, Just (FC f l))
@@ -567,13 +568,14 @@ Insert inferred values into the term
> let (Ind tvnf) = eval_nf_env env gamma (Ind tv)
> let ttnf = -- trace ("PI: " ++ show (tv, tvnf, debugTT tv)) $
> eval_nf_env env gamma (Ind tt)
-> checkConvSt env gamma ttnf (Ind Star)
+> -- checkConvSt env gamma ttnf (Ind AnyKind)
+> case ttnf of
+> (Ind Star) -> return (B Pi tv)
+> (Ind LinStar) -> return (B Pi tv)
+> (Ind (P (MN ("INFER",_)))) -> return (B Pi tv)
+> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
> return (B Pi tvnf)
- case ttnf of
- (Ind Star) -> return (B Pi tv)
- (Ind (P (MN ("INFER",_)))) -> return (B Pi tv)
- _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
> checkbinder gamma env lvl n (B (Let v) RInfer) = do
> (Ind vv,Ind vt) <- tcfixup env lvl v Nothing
@@ -710,7 +712,10 @@ extended environment.
> let lv = Bind n (B Lambda t) scv
> return (Ind lv,Ind lt)
> discharge gamma n (B Pi t) scv (Sc sct) = do
-> checkConvSt [] gamma (Ind Star) (Ind sct)
+> case sct of
+> Star -> return ()
+> LinStar -> return ()
+> _ -> checkConvSt [] gamma (Ind Star) (Ind sct)
> let lt = Star
> let lv = Bind n (B Pi t) scv
> return (Ind lv,Ind lt)
View
@@ -191,6 +191,7 @@ Model represents normal forms, including Ready (reducible) and Blocked
> | RTyCon Name (Spine (Model s))
> | forall c. Constant c => RdConst c
> | RdStar
+> | RdLinStar
> | RdErased
> | RdLabel (Model s) (MComp s)
> | RdCall (MComp s) (Model s)
View
@@ -77,6 +77,7 @@
> | Return { returnterm :: ViewTerm }
> | forall c. Constant c => Constant c
> | Star
+> | LinStar
> | Quote { quotedterm :: ViewTerm } -- ^ Staging annotation
> | Code { codetype :: ViewTerm } -- ^ Staging annotation
> | Eval { evalterm :: ViewTerm } -- ^ Staging annotation
@@ -114,6 +115,7 @@
> (==) (Ivor.ViewTerm.Call _ _ t) (Ivor.ViewTerm.Call _ _ t') = t == t'
> (==) (Ivor.ViewTerm.Return t) (Ivor.ViewTerm.Return t') = t==t'
> (==) Ivor.ViewTerm.Star Ivor.ViewTerm.Star = True
+> (==) Ivor.ViewTerm.LinStar Ivor.ViewTerm.LinStar = True
> (==) Placeholder Placeholder = True
> (==) (Metavar x) (Metavar y) = x == y
> (==) (Constant x) (Constant y) = case cast x of
@@ -163,6 +165,7 @@
> forget (Ivor.ViewTerm.Return ty) = RReturn (forget ty)
> forget (Constant c) = RConst c
> forget (Ivor.ViewTerm.Star) = TTCore.RStar
+> forget (Ivor.ViewTerm.LinStar) = TTCore.RLinStar
> forget Placeholder = RInfer
> forget (Metavar x) = RMeta x
> forget (Ivor.ViewTerm.Quote t) = RStage (RQuote (forget t))
@@ -215,6 +218,7 @@
> Ivor.ViewTerm.Let n (vtaux ctxt ty) (vtaux ctxt val) (vtaux (n:ctxt) sc)
> vtaux ctxt (Const c) = Constant c
> vtaux ctxt TTCore.Star = Ivor.ViewTerm.Star
+> vtaux ctxt TTCore.LinStar = Ivor.ViewTerm.LinStar
> vtaux ctxt (TTCore.Label ty (Comp n ts)) =
> Ivor.ViewTerm.Label n (fmap (vtaux ctxt) ts) (vtaux ctxt ty)
> vtaux ctxt (TTCore.Call (Comp n ts) ty) =

0 comments on commit 07e10a7

Please sign in to comment.