git.iko.soy/Idris-dev
on master help sign in
No mucking about with de Bruijn indices in proof construction
6a6a048Edwin Brady
impl-paper/overview.tex+4
compare with master
unifiedsplit
@@ -8,6 +8,10 @@ High level view of steps we've taken to implement this new version:
8\item The important bit: a simple type checker. No unification or
8\item The important bit: a simple type checker. No unification or
9 inference.
9 inference.
10\item The proof state and a tactic engine (Oleg style~\cite{mcbride-thesis}).
10\item The proof state and a tactic engine (Oleg style~\cite{mcbride-thesis}).
11+\begin{itemize}
12+ \item Dealing with names: typechecking and evaluation in a context, managing de Bruijn
13+ indices becomes tricky.
14+\end{itemize}
11\end{itemize}
15\end{itemize}
12
16
13For the high level language: we need nothing more than the core type theory,
17For the high level language: we need nothing more than the core type theory,
src/Core.hs+11−12
@@ -47,6 +47,8 @@ data Binder b = Lam { binderTy :: b }
47 | Pi { binderTy :: b }
47 | Pi { binderTy :: b }
48 | Let { binderTy :: b,
48 | Let { binderTy :: b,
49 binderVal :: b }
49 binderVal :: b }
50+ | NLet { binderTy :: b,
51+ binderVal :: b }
50 | Hole { binderTy :: b}
52 | Hole { binderTy :: b}
51 | Guess { binderTy :: b,
53 | Guess { binderTy :: b,
52 binderVal :: b }
54 binderVal :: b }
@@ -66,7 +68,7 @@ type RProgram = [(Name, RDef)]
66
68
67-- WELL TYPED TERMS ---------------------------------------------------------
69-- WELL TYPED TERMS ---------------------------------------------------------
68
70
69−data NameType = Ref | DCon Int Int | TCon Int
71+data NameType = Bound | Ref | DCon Int Int | TCon Int
70 deriving (Show, Eq)
72 deriving (Show, Eq)
71
73
72-- FIXME: Consider changing this to birectional, with type annotations.
74-- FIXME: Consider changing this to birectional, with type annotations.
@@ -80,12 +82,13 @@ data TT n = P NameType n (TT n) -- embed type
80
82
81type EnvTT n = [(n, Binder (TT n))]
83type EnvTT n = [(n, Binder (TT n))]
82
84
83−-- Returns true if V 0 does not occur in the term
85+-- Returns true if V 0 and bound name n do not occur in the term
84
86
85−noOccurrence :: TT n -> Bool
87+noOccurrence :: Eq n => n -> TT n -> Bool
86−noOccurrence t = no' 0 t
88+noOccurrence n t = no' 0 t
87 where
89 where
88 no' i (V x) = not (i == x)
90 no' i (V x) = not (i == x)
91+ no' i (P Bound x _) = not (n == x)
89 no' i (Bind n b sc) = noB' i b && no' (i+1) sc
92 no' i (Bind n b sc) = noB' i b && no' (i+1) sc
90 where noB' i (Let t v) = no' i t && no' i v
93 where noB' i (Let t v) = no' i t && no' i v
91 noB' i (Guess t v) = no' i t && no' i v
94 noB' i (Guess t v) = no' i t && no' i v
@@ -93,10 +96,6 @@ noOccurrence t = no' 0 t
93 no' i (App f a) = no' i f && no' i a
96 no' i (App f a) = no' i f && no' i a
94 no' i _ = True
97 no' i _ = True
95
98
96−bindEnv :: EnvTT n -> TT n -> TT n
97−bindEnv [] tm = tm
98−bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
99−
100type Term = TT Name
99type Term = TT Name
101type Type = Term
100type Type = Term
102
101
@@ -108,20 +107,20 @@ type Env = EnvTT Name
108newtype WkEnvTT n = Wk (EnvTT n)
107newtype WkEnvTT n = Wk (EnvTT n)
109type WkEnv = WkEnvTT Name
108type WkEnv = WkEnvTT Name
110
109
111−instance Show n => Show (TT n) where
110+instance (Eq n, Show n) => Show (TT n) where
112 show t = showEnv [] t
111 show t = showEnv [] t
113
112
114showEnv env t = showEnv' env t False
113showEnv env t = showEnv' env t False
115showEnvDbg env t = showEnv' env t True
114showEnvDbg env t = showEnv' env t True
116
115
117showEnv' env t dbg = se 10 env t where
116showEnv' env t dbg = se 10 env t where
118− se p env (P nt n t) = show n ++
117+ se p env (P nt n t) = show n
119− if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
118+-- ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
120 se p env (V i) | i < length env = (show $ fst $ env!!i) ++
119 se p env (V i) | i < length env = (show $ fst $ env!!i) ++
121 if dbg then "{" ++ show i ++ "}" else ""
120 if dbg then "{" ++ show i ++ "}" else ""
122 | otherwise = "!!V " ++ show i ++ "!!"
121 | otherwise = "!!V " ++ show i ++ "!!"
123 se p env (Bind n b@(Pi t) sc)
122 se p env (Bind n b@(Pi t) sc)
124− | noOccurrence sc = bracket p 2 $ se 10 env t ++ " -> " ++ se 10 ((n,b):env) sc
123+ | noOccurrence n sc = bracket p 2 $ se 10 env t ++ " -> " ++ se 10 ((n,b):env) sc
125 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc
124 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc
126 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
125 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
127 se p env (Set i) = "Set" ++ show i
126 se p env (Set i) = "Set" ++ show i
src/CoreParser.hs+7
@@ -99,6 +99,13 @@ pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm
99 reserved "in";
99 reserved "in";
100 sc <- pTerm
100 sc <- pTerm
101 return (RBind x (Let ty val) sc))
101 return (RBind x (Let ty val) sc))
102+-- <|> try (do reserved "nlet";
103+-- x <- iName; lchar ':'; ty <- pTerm
104+-- lchar '=';
105+-- val <- pTerm
106+-- reserved "in";
107+-- sc <- pTerm
108+-- return (RBind x (NLet ty val) sc))
102 <|> try (do lchar '_';
109 <|> try (do lchar '_';
103 x <- iName; lchar ':'; ty <- pTerm
110 x <- iName; lchar ':'; ty <- pTerm
104 lchar '.';
111 lchar '.';
src/Evaluate.hs+33−5
@@ -22,22 +22,50 @@ instance Show Value where
22
22
23-- THE EVALUATOR ------------------------------------------------------------
23-- THE EVALUATOR ------------------------------------------------------------
24
24
25+-- The environment is assumed to be "locally named" - i.e., not de Bruijn
26+-- indexed.
27+-- i.e. it's an intermediate environment that we have while type checking or
28+-- while building a proof.
29+
25normalise :: Context -> Env -> TT Name -> TT Name
30normalise :: Context -> Env -> TT Name -> TT Name
26−normalise ctxt env t = quote 0 (eval ctxt (weakenEnv env) t)
31+normalise ctxt env t = quote 0 (eval ctxt env t)
32+
33+-- let evtm = bindEnv (reverse env) t
34+-- evtm' = quote 0 (evalCtxt ctxt evtm) in
35+-- trace (show (evtm, evtm')) $
36+-- unbindEnv env evtm'
37+
38+-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
39+
40+bindEnv :: EnvTT n -> TT n -> TT n
41+bindEnv [] tm = tm
42+bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
43+bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
44+
45+unbindEnv :: EnvTT n -> TT n -> TT n
46+unbindEnv [] tm = tm
47+unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
48+
49+-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
50+-- such as we might have during construction of a proof)
27
51
28eval :: Context -> Env -> TT Name -> Value
52eval :: Context -> Env -> TT Name -> Value
29eval ctxt genv tm = ev [] tm where
53eval ctxt genv tm = ev [] tm where
54+ ev env (P Bound n ty)
55+ | Just (Let t v) <- lookup n genv = ev env v
30 ev env (P Ref n ty)
56 ev env (P Ref n ty)
31 | Just v <- lookupVal n ctxt = v
57 | Just v <- lookupVal n ctxt = v
32 ev env (P nt n ty) = VP nt n (ev env ty)
58 ev env (P nt n ty) = VP nt n (ev env ty)
33 ev env (V i) | i < length env = env !! i
59 ev env (V i) | i < length env = env !! i
34− | i < length env + length genv
60+-- | i < length env + length genv
35− = case genv !! (i - length env) of
61+-- = case genv !! (i - length env) of
36− (_, Let t v) -> ev env v
62+-- (_, Let t v) -> ev env v
37− _ -> VV i
63+-- _ -> VV i
38 | otherwise = error $ "Internal error: V" ++ show i
64 | otherwise = error $ "Internal error: V" ++ show i
39 ev env (Bind n (Let t v) sc)
65 ev env (Bind n (Let t v) sc)
40 = wknV (-1) $ ev (ev env v : env) sc
66 = wknV (-1) $ ev (ev env v : env) sc
67+ ev env (Bind n (NLet t v) sc)
68+ = VBind n (Let (ev env t) (ev env v)) $ (\x -> ev (ev env v : env) sc)
41 ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)
69 ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)
42 where vbind env t = fmap (ev env) t
70 where vbind env t = fmap (ev env) t
43 ev env (App f a) = evApply env [a] f
71 ev env (App f a) = evApply env [a] f
src/ProofShell.hs+4−2
@@ -21,8 +21,10 @@ initState c = State c Nothing False
21processCommand :: Command -> ShellState -> (ShellState, String)
21processCommand :: Command -> ShellState -> (ShellState, String)
22processCommand (Theorem n ty) state
22processCommand (Theorem n ty) state
23 = case check (ctxt state) [] ty of
23 = case check (ctxt state) [] ty of
24+ OK (gl, t) ->
25+ case isSet (ctxt state) [] t of
24− OK (gl, Set _) -> (state { prf = Just (newProof n (ctxt state) gl) }, "")
26+ OK _ -> (state { prf = Just (newProof n (ctxt state) gl) }, "")
25− OK _ -> (state, "Goal is not a type")
27+ _ -> (state, "Goal is not a type")
26 err -> (state, show err)
28 err -> (state, show err)
27processCommand Quit state = (state { exitNow = True }, "Bye bye")
29processCommand Quit state = (state { exitNow = True }, "Bye bye")
28processCommand (Eval t) state =
30processCommand (Eval t) state =
src/ProofState.hs+29−14
@@ -62,6 +62,11 @@ instance Show ProofState where
62 ") -------\n" ++
62 ") -------\n" ++
63 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
63 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
64 where showPs env [] = ""
64 where showPs env [] = ""
65+ showPs env ((n, Let t v):bs)
66+ = " " ++ show n ++ " : " ++
67+ showEnv env (normalise ctxt env t) ++ " = " ++
68+ showEnv env (normalise ctxt env v) ++
69+ "\n" ++ showPs env bs
65 showPs env ((n, b):bs)
70 showPs env ((n, b):bs)
66 = " " ++ show n ++ " : " ++
71 = " " ++ show n ++ " : " ++
67 showEnv env (normalise ctxt env (binderTy b)) ++
72 showEnv env (normalise ctxt env (binderTy b)) ++
@@ -89,8 +94,9 @@ action a = do (n, ts) <- get
89 put (n, a:ts)
94 put (n, a:ts)
90
95
91newProof :: Name -> Context -> Type -> ProofState
96newProof :: Name -> Context -> Type -> ProofState
92−newProof n ctxt ty = let h = holeName 0 in
97+newProof n ctxt ty = let h = holeName 0
98+ ty' = vToP ty in
93− PS n [h] 1 (Bind h (Hole ty) (V 0)) ty ctxt False
99+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty ctxt False
94
100
95type TState = (Int, [TacticAction])
101type TState = (Int, [TacticAction])
96type RunTactic = Context -> Env -> Term -> StateT TState TC Term
102type RunTactic = Context -> Env -> Term -> StateT TState TC Term
@@ -100,7 +106,7 @@ goal :: Hole -> Term -> Context -> TC Goal
100goal h tm ctxt = g [] tm where
106goal h tm ctxt = g [] tm where
101 g env (Bind n b sc) | hole b && same h n = return $ GD env b
107 g env (Bind n b sc) | hole b && same h n = return $ GD env b
102 | otherwise
108 | otherwise
103− = gb env b `mplus` g ((n,fmap (weakenTm 1) b):weakenTmEnv 1 env) sc
109+ = gb env b `mplus` g ((n, b):env) sc
104 g env (App f a) = g env f `mplus` g env a
110 g env (App f a) = g env f `mplus` g env a
105 g env t = Error "Can't find hole"
111 g env t = Error "Can't find hole"
106
112
@@ -116,8 +122,7 @@ tactic h ps ctxt f = do let tm = pterm ps
116 atH env binder@(Bind n b sc)
122 atH env binder@(Bind n b sc)
117 | hole b && same h n = f ctxt env binder
123 | hole b && same h n = f ctxt env binder
118 | otherwise
124 | otherwise
119− = pure Bind <*> pure n <*> atHb env b <*>
125+ = pure Bind <*> pure n <*> atHb env b <*> atH ((n,b) : env) sc
120− atH ((n,fmap (weakenTm 1) b):weakenTmEnv 1 env) sc
121 atH env (App f a) = pure App <*> atH env f <*> atH env a
126 atH env (App f a) = pure App <*> atH env f <*> atH env a
122 atH env t = return t
127 atH env t = return t
123
128
@@ -132,7 +137,7 @@ attack ctxt env (Bind x (Hole t) sc)
132 action (AddGoal h)
137 action (AddGoal h)
133 return $ Bind x (Guess t (newtm h)) sc
138 return $ Bind x (Guess t (newtm h)) sc
134 where
139 where
135− newtm h = Bind h (Hole t) (V 0)
140+ newtm h = Bind h (Hole t) (P Bound h t)
136attack ctxt env _ = fail "Not an attackable hole"
141attack ctxt env _ = fail "Not an attackable hole"
137
142
138claim :: Name -> Raw -> RunTactic
143claim :: Name -> Raw -> RunTactic
@@ -140,7 +145,7 @@ claim n ty ctxt env t =
140 do (tyv, tyt) <- lift $ check ctxt env ty
145 do (tyv, tyt) <- lift $ check ctxt env ty
141 lift $ isSet ctxt env tyt
146 lift $ isSet ctxt env tyt
142 action (NextGoal n)
147 action (NextGoal n)
143− return $ Bind n (Hole tyv) t
148+ return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
144
149
145focus :: Name -> RunTactic
150focus :: Name -> RunTactic
146focus n ctxt env t = do action (FocusGoal n)
151focus n ctxt env t = do action (FocusGoal n)
@@ -149,7 +154,7 @@ focus n ctxt env t = do action (FocusGoal n)
149regret :: RunTactic
154regret :: RunTactic
150regret = undefined
155regret = undefined
151
156
152−fill :: Raw -> RunTactic -- Try
157+fill :: Raw -> RunTactic
153fill guess ctxt env (Bind x (Hole ty) sc) =
158fill guess ctxt env (Bind x (Hole ty) sc) =
154 do (val, valty) <- lift $ check ctxt env guess
159 do (val, valty) <- lift $ check ctxt env guess
155 lift $ converts ctxt env valty ty
160 lift $ converts ctxt env valty ty
@@ -159,15 +164,16 @@ fill _ _ _ _ = fail "Can't fill here."
159solve :: RunTactic
164solve :: RunTactic
160solve ctxt env (Bind x (Guess ty val) sc)
165solve ctxt env (Bind x (Guess ty val) sc)
161 | pureTerm val = do action (Solved x)
166 | pureTerm val = do action (Solved x)
162− return $ Bind x (Let ty val) sc
167+ return $ Bind x (Let ty val) sc -- instantiate val (pToV x sc)
163 | otherwise = fail "I see a hole in your solution."
168 | otherwise = fail "I see a hole in your solution."
164solve _ _ _ = fail "Not a guess."
169solve _ _ _ = fail "Not a guess."
165
170
166intro :: Name -> RunTactic
171intro :: Name -> RunTactic
167−intro n ctxt env (Bind x (Hole t) (V 0)) =
172+intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
168 do let t' = normalise ctxt env t
173 do let t' = normalise ctxt env t
169 case t' of
174 case t' of
175+ Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
170− Bind y (Pi s) t -> return $ Bind n (Lam s) (Bind x (Hole t) (V 0))
176+ return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
171 _ -> fail "Nothing to introduce"
177 _ -> fail "Nothing to introduce"
172intro ctxt env _ _ = fail "Can't introduce here."
178intro ctxt env _ _ = fail "Can't introduce here."
173
179
@@ -184,15 +190,24 @@ check_in t ctxt env tm =
184eval_in :: Raw -> RunTactic
190eval_in :: Raw -> RunTactic
185eval_in t ctxt env tm =
191eval_in t ctxt env tm =
186 do (val, valty) <- lift $ check ctxt env t
192 do (val, valty) <- lift $ check ctxt env t
193+ let val' = normalise ctxt env val
194+ let valty' = normalise ctxt env valty
187− action (Log (showEnv env (normalise ctxt env val) ++ " : " ++ showEnv env valty))
195+ action (Log (showEnv env val ++ " : " ++
196+ showEnv env valty ++
197+-- " in " ++ show env ++
198+ " ==>\n " ++
199+ showEnv env val' ++ " : " ++
200+ showEnv env valty'))
188 return tm
201 return tm
189
202
190
203
191processTactic :: Tactic -> ProofState -> TC (ProofState, String)
204processTactic :: Tactic -> ProofState -> TC (ProofState, String)
192processTactic QED ps = case holes ps of
205processTactic QED ps = case holes ps of
206+ [] -> let tm = finalise (pterm ps) in
193− [] -> return (ps { done = True }, "Proof complete.")
207+ return (ps { done = True, pterm = tm },
208+ "Proof complete: " ++ showEnv [] tm)
194 _ -> Error "Still holes to fill."
209 _ -> Error "Still holes to fill."
195−processTactic ProofState ps = return (ps, show (pterm ps))
210+processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
196processTactic t ps = case holes ps of
211processTactic t ps = case holes ps of
197 [] -> Error "Nothing to fill in."
212 [] -> Error "Nothing to fill in."
198 (h:_) -> do let n = nextname ps
213 (h:_) -> do let n = nextname ps
src/Typecheck.hs+43−2
@@ -47,13 +47,14 @@ isSet ctxt env tm = isSet' (normalise ctxt env tm)
47
47
48check :: Context -> Env -> Raw -> TC (Term, Type)
48check :: Context -> Env -> Raw -> TC (Term, Type)
49check ctxt env (Var n)
49check ctxt env (Var n)
50− | Just (i, ty) <- lookupTyEnv n env = return (V i, ty)
50+ | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
51 | Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)
51 | Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)
52 | otherwise = do fail $ "No such variable " ++ show n
52 | otherwise = do fail $ "No such variable " ++ show n
53check ctxt env (RApp f a)
53check ctxt env (RApp f a)
54 = do (fv, fty) <- check ctxt env f
54 = do (fv, fty) <- check ctxt env f
55 (av, aty) <- check ctxt env a
55 (av, aty) <- check ctxt env a
56 let fty' = normalise ctxt env fty
56 let fty' = normalise ctxt env fty
57+-- trace (showEnv env fty ++ " ===> " ++ showEnv env fty') $
57 case fty' of
58 case fty' of
58 Bind x (Pi s) t ->
59 Bind x (Pi s) t ->
59 do converts ctxt env s aty
60 do converts ctxt env s aty
@@ -64,7 +65,7 @@ check ctxt env (RSet i) = return (Set i, Set (i+1))
64check ctxt env (RBind n b sc)
65check ctxt env (RBind n b sc)
65 = do b' <- checkBinder b
66 = do b' <- checkBinder b
66 (scv, sct) <- check ctxt ((n, b'):env) sc
67 (scv, sct) <- check ctxt ((n, b'):env) sc
67− discharge n b' scv sct
68+ discharge n b' (pToV n scv) (pToV n sct)
68 where checkBinder (Lam t)
69 where checkBinder (Lam t)
69 = do (tv, tt) <- check ctxt env t
70 = do (tv, tt) <- check ctxt env t
70 let tv' = normalise ctxt env tv
71 let tv' = normalise ctxt env tv
@@ -85,6 +86,14 @@ check ctxt env (RBind n b sc)
85 converts ctxt env tv vt
86 converts ctxt env tv vt
86 isSet ctxt env tt'
87 isSet ctxt env tt'
87 return (Let tv' vv)
88 return (Let tv' vv)
89+ checkBinder (NLet t v)
90+ = do (tv, tt) <- check ctxt env t
91+ (vv, vt) <- check ctxt env v
92+ let tv' = normalise ctxt env tv
93+ let tt' = normalise ctxt env tt
94+ converts ctxt env tv vt
95+ isSet ctxt env tt'
96+ return (NLet tv' vv)
88 checkBinder (Hole t)
97 checkBinder (Hole t)
89 = do (tv, tt) <- check ctxt env t
98 = do (tv, tt) <- check ctxt env t
90 let tv' = normalise ctxt env tv
99 let tv' = normalise ctxt env tv
@@ -112,6 +121,8 @@ check ctxt env (RBind n b sc)
112 = return (Bind n (Pi t) scv, sct)
121 = return (Bind n (Pi t) scv, sct)
113 discharge n (Let t v) scv sct
122 discharge n (Let t v) scv sct
114 = return (Bind n (Let t v) scv, Bind n (Let t v) sct)
123 = return (Bind n (Let t v) scv, Bind n (Let t v) sct)
124+ discharge n (NLet t v) scv sct
125+ = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
115 discharge n (Hole t) scv sct
126 discharge n (Hole t) scv sct
116 = do -- A hole can't appear in the type of its scope
127 = do -- A hole can't appear in the type of its scope
117 checkNotHoley 0 sct
128 checkNotHoley 0 sct
@@ -130,6 +141,36 @@ check ctxt env (RBind n b sc)
130 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
141 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
131 checkNotHoley _ _ = return ()
142 checkNotHoley _ _ = return ()
132
143
144+pToV :: Eq n => n -> TT n -> TT n
145+pToV n = pToV' 0 where
146+ pToV' i (P _ x _) | n == x = V i
147+ pToV' i (Bind x b sc)
148+ | n == x = Bind x (fmap (pToV' i) b) sc
149+ | otherwise = Bind x (fmap (pToV' i) b) (pToV' (i+1) sc)
150+ pToV' i (App f a) = App (pToV' i f) (pToV' i a)
151+ pToV' i t = t
152+
153+vToP :: TT n -> TT n
154+vToP = vToP' [] where
155+ vToP' env (V i) = let (n, b) = (env !! i) in
156+ P Bound n (binderTy b)
157+ vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in
158+ Bind n b' (vToP' ((n, b'):env) sc)
159+ vToP' env (App f a) = App (vToP' env f) (vToP' env a)
160+ vToP' env t = t
161+
162+instantiate :: TT n -> TT n -> TT n
163+instantiate e = subst 0 where
164+ subst i (V x) | i == x = e
165+ subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
166+ subst i (App f a) = App (subst i f) (subst i a)
167+ subst i t = t
168+
169+finalise :: Eq n => TT n -> TT n
170+finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
171+finalise (App f a) = App (finalise f) (finalise a)
172+finalise t = t
173+
133checkProgram :: Context -> RProgram -> TC Context
174checkProgram :: Context -> RProgram -> TC Context
134checkProgram ctxt [] = return ctxt
175checkProgram ctxt [] = return ctxt
135checkProgram ctxt ((n, RConst t):xs)
176checkProgram ctxt ((n, RConst t):xs)
src/test.mi+1−1
@@ -8,6 +8,6 @@ three : N = S two;
8
8
9Vect : (A:Set 0) -> (n:N) -> Set 0;
9Vect : (A:Set 0) -> (n:N) -> Set 0;
10Nil : (A:Set 0) -> (Vect A O);
10Nil : (A:Set 0) -> (Vect A O);
11−Cons : (A:Set 0) -> (k:N) -> (Vect A k) -> (Vect A (S k));
11+Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));
12
12
13vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);
13vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);