ivor 0.1.14 → 0.1.14.1
raw patch · 7 files changed
+56/−9 lines, 7 files
Files
- Ivor/CtxtTT.lhs +4/−1
- Ivor/Nobby.lhs +4/−0
- Ivor/TTCore.lhs +29/−0
- Ivor/Typecheck.lhs +13/−7
- Ivor/Values.lhs +1/−0
- Ivor/ViewTerm.lhs +4/−0
- ivor.cabal +1/−1
Ivor/CtxtTT.lhs view
@@ -36,7 +36,10 @@ > tt (Right v) = Right v > getError :: IError -> TTError-> getError (ICantUnify l r) = CantUnify (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))+> getError (ICantUnify l r) -- = CantUnify (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))++> = Message $ "Can't unify " ++ show (view (Term (l, Ind TTCore.Star))) ++ " and " ++ show (view (Term (r, Ind TTCore.Star)))+ > getError (INotConvertible l r) = NotConvertible (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star))) > getError (IMessage s) = Message s > getError (IUnbound clause clty rhs rhsty names)
Ivor/Nobby.lhs view
@@ -74,6 +74,7 @@ > 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 @@ > 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 @@ > 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 @@ > 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)
Ivor/TTCore.lhs view
@@ -22,6 +22,7 @@ > | 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 @@ > | 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 @@ > | 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 @@ > data Bind n > = Lambda > | Pi+> | LinPi > | Let n > | Hole > | Guess n@@ -257,7 +264,10 @@ > 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 @@ > = 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 @@ > = 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 @@ > 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 @@ > 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 @@ > 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 @@ > 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 @@ > 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 @@ > 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 @@ > 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 @@ > 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
Ivor/Typecheck.lhs view
@@ -141,12 +141,13 @@ > let y' = papp s' y > let (Ind y'') = -- trace ("Unifying with " ++ show x' ++ " and " ++ show (papp s' y) ++ "[" ++ show (x,y) ++ "]") $ > eval_nf gam (Ind (papp s' y))+> let (Ind x'') = eval_nf gam (Ind (papp s' x)) > uns <- case unifyenvErr ok gam env (Ind y') (Ind x') of > Right uns -> return uns > Left err -> -- trace (showeqn all) $ > case unifyenvErr ok gam env (Ind y'') (Ind x') of > Right uns -> return uns-> Left err -> ifail (errCtxt fc (ICantUnify (Ind y') (Ind x')))+> Left err -> ifail (errCtxt fc (ICantUnify (Ind y'') (Ind x''))) Failure err -> fail $ err ++"\n" ++ show nms ++"\n" ++ show constraints -- $ -} ++ " Can't convert "++show x'++" and "++show y' ++ "\n" ++ show constraints ++ "\n" ++ show nms @@ -416,6 +417,7 @@ > 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 +569,14 @@ > 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 +713,10 @@ > 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)
Ivor/Values.lhs view
@@ -191,6 +191,7 @@ > | RTyCon Name (Spine (Model s)) > | forall c. Constant c => RdConst c > | RdStar+> | RdLinStar > | RdErased > | RdLabel (Model s) (MComp s) > | RdCall (MComp s) (Model s)
Ivor/ViewTerm.lhs 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) =
ivor.cabal view
@@ -1,5 +1,5 @@ Name: ivor-Version: 0.1.14+Version: 0.1.14.1 Author: Edwin Brady License: BSD3 License-file: LICENSE