6a6a048 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

No mucking about with de Bruijn indices in proof construction

commit6a6a048f06926745b505c28dd995ea2ded945543 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 26 Sep 2011, 12:11 (15 years ago) parent1921eac

8 files changed+132−36

compare with master

unifiedsplit

impl-paper/overview.tex+4 src/Core.hs+11−12 src/CoreParser.hs+7 src/Evaluate.hs+33−5 src/ProofShell.hs+4−2 src/ProofState.hs+29−14 src/Typecheck.hs+43−2 src/test.mi+1−1

impl-paper/overview.tex+4

@@ -8,6 +8,10 @@ High level view of steps we've taken to implement this new version:

88\item The important bit: a simple type checker. No unification or

99 inference.

1010\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}

1115\end{itemize}

1216

1317For 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 }

4747 | Pi { binderTy :: b }

4848 | Let { binderTy :: b,

4949 binderVal :: b }

50+ | NLet { binderTy :: b,

51+ binderVal :: b }

5052 | Hole { binderTy :: b}

5153 | Guess { binderTy :: b,

5254 binderVal :: b }

@@ -66,7 +68,7 @@ type RProgram = [(Name, RDef)]

6668

6769-- WELL TYPED TERMS ---------------------------------------------------------

6870

69−data NameType = Ref | DCon Int Int | TCon Int

71+data NameType = Bound | Ref | DCon Int Int | TCon Int

7072 deriving (Show, Eq)

7173

7274-- FIXME: Consider changing this to birectional, with type annotations.

@@ -80,12 +82,13 @@ data TT n = P NameType n (TT n) -- embed type

8082

8183type EnvTT n = [(n, Binder (TT n))]

8284

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

8486

85−noOccurrence :: TT n -> Bool

86−noOccurrence t = no' 0 t

87+noOccurrence :: Eq n => n -> TT n -> Bool

88+noOccurrence n t = no' 0 t

8789 where

8890 no' i (V x) = not (i == x)

91+ no' i (P Bound x _) = not (n == x)

8992 no' i (Bind n b sc) = noB' i b && no' (i+1) sc

9093 where noB' i (Let t v) = no' i t && no' i v

9194 noB' i (Guess t v) = no' i t && no' i v

@@ -93,10 +96,6 @@ noOccurrence t = no' 0 t

9396 no' i (App f a) = no' i f && no' i a

9497 no' i _ = True

9598

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−

10099type Term = TT Name

101100type Type = Term

102101

@@ -108,20 +107,20 @@ type Env = EnvTT Name

108107newtype WkEnvTT n = Wk (EnvTT n)

109108type WkEnv = WkEnvTT Name

110109

111−instance Show n => Show (TT n) where

110+instance (Eq n, Show n) => Show (TT n) where

112111 show t = showEnv [] t

113112

114113showEnv env t = showEnv' env t False

115114showEnvDbg env t = showEnv' env t True

116115

117116showEnv' env t dbg = se 10 env t where

118− se p env (P nt n t) = show n ++

119− if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

117+ se p env (P nt n t) = show n

118+-- ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

120119 se p env (V i) | i < length env = (show $ fst $ env!!i) ++

121120 if dbg then "{" ++ show i ++ "}" else ""

122121 | otherwise = "!!V " ++ show i ++ "!!"

123122 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

125124 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

126125 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

127126 se p env (Set i) = "Set" ++ show i

src/CoreParser.hs+7

@@ -99,6 +99,13 @@ pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

9999 reserved "in";

100100 sc <- pTerm

101101 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))

102109 <|> try (do lchar '_';

103110 x <- iName; lchar ':'; ty <- pTerm

104111 lchar '.';

src/Evaluate.hs+33−5

@@ -22,22 +22,50 @@ instance Show Value where

2222

2323-- THE EVALUATOR ------------------------------------------------------------

2424

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+

2530normalise :: 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)

2751

2852eval :: Context -> Env -> TT Name -> Value

2953eval ctxt genv tm = ev [] tm where

54+ ev env (P Bound n ty)

55+ | Just (Let t v) <- lookup n genv = ev env v

3056 ev env (P Ref n ty)

3157 | Just v <- lookupVal n ctxt = v

3258 ev env (P nt n ty) = VP nt n (ev env ty)

3359 ev env (V i) | i < length env = env !! i

34− | i < length env + length genv

35− = case genv !! (i - length env) of

36− (_, Let t v) -> ev env v

37− _ -> VV i

60+-- | i < length env + length genv

61+-- = case genv !! (i - length env) of

62+-- (_, Let t v) -> ev env v

63+-- _ -> VV i

3864 | otherwise = error $ "Internal error: V" ++ show i

3965 ev env (Bind n (Let t v) sc)

4066 = 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)

4169 ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)

4270 where vbind env t = fmap (ev env) t

4371 ev env (App f a) = evApply env [a] f

src/ProofShell.hs+4−2

@@ -21,8 +21,10 @@ initState c = State c Nothing False

2121processCommand :: Command -> ShellState -> (ShellState, String)

2222processCommand (Theorem n ty) state

2323 = case check (ctxt state) [] ty of

24− OK (gl, Set _) -> (state { prf = Just (newProof n (ctxt state) gl) }, "")

25− OK _ -> (state, "Goal is not a type")

24+ OK (gl, t) ->

25+ case isSet (ctxt state) [] t of

26+ OK _ -> (state { prf = Just (newProof n (ctxt state) gl) }, "")

27+ _ -> (state, "Goal is not a type")

2628 err -> (state, show err)

2729processCommand Quit state = (state { exitNow = True }, "Bye bye")

2830processCommand (Eval t) state =

src/ProofState.hs+29−14

@@ -62,6 +62,11 @@ instance Show ProofState where

6262 ") -------\n" ++

6363 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"

6464 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

6570 showPs env ((n, b):bs)

6671 = " " ++ show n ++ " : " ++

6772 showEnv env (normalise ctxt env (binderTy b)) ++

@@ -89,8 +94,9 @@ action a = do (n, ts) <- get

8994 put (n, a:ts)

9095

9196newProof :: Name -> Context -> Type -> ProofState

92−newProof n ctxt ty = let h = holeName 0 in

93− PS n [h] 1 (Bind h (Hole ty) (V 0)) ty ctxt False

97+newProof n ctxt ty = let h = holeName 0

98+ ty' = vToP ty in

99+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty ctxt False

94100

95101type TState = (Int, [TacticAction])

96102type RunTactic = Context -> Env -> Term -> StateT TState TC Term

@@ -100,7 +106,7 @@ goal :: Hole -> Term -> Context -> TC Goal

100106goal h tm ctxt = g [] tm where

101107 g env (Bind n b sc) | hole b && same h n = return $ GD env b

102108 | 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

104110 g env (App f a) = g env f `mplus` g env a

105111 g env t = Error "Can't find hole"

106112

@@ -116,8 +122,7 @@ tactic h ps ctxt f = do let tm = pterm ps

116122 atH env binder@(Bind n b sc)

117123 | hole b && same h n = f ctxt env binder

118124 | otherwise

119− = pure Bind <*> pure n <*> atHb env b <*>

120− atH ((n,fmap (weakenTm 1) b):weakenTmEnv 1 env) sc

125+ = pure Bind <*> pure n <*> atHb env b <*> atH ((n,b) : env) sc

121126 atH env (App f a) = pure App <*> atH env f <*> atH env a

122127 atH env t = return t

123128

@@ -132,7 +137,7 @@ attack ctxt env (Bind x (Hole t) sc)

132137 action (AddGoal h)

133138 return $ Bind x (Guess t (newtm h)) sc

134139 where

135− newtm h = Bind h (Hole t) (V 0)

140+ newtm h = Bind h (Hole t) (P Bound h t)

136141attack ctxt env _ = fail "Not an attackable hole"

137142

138143claim :: Name -> Raw -> RunTactic

@@ -140,7 +145,7 @@ claim n ty ctxt env t =

140145 do (tyv, tyt) <- lift $ check ctxt env ty

141146 lift $ isSet ctxt env tyt

142147 action (NextGoal n)

143− return $ Bind n (Hole tyv) t

148+ return $ Bind n (Hole tyv) t -- (weakenTm 1 t)

144149

145150focus :: Name -> RunTactic

146151focus n ctxt env t = do action (FocusGoal n)

@@ -149,7 +154,7 @@ focus n ctxt env t = do action (FocusGoal n)

149154regret :: RunTactic

150155regret = undefined

151156

152−fill :: Raw -> RunTactic -- Try

157+fill :: Raw -> RunTactic

153158fill guess ctxt env (Bind x (Hole ty) sc) =

154159 do (val, valty) <- lift $ check ctxt env guess

155160 lift $ converts ctxt env valty ty

@@ -159,15 +164,16 @@ fill _ _ _ _ = fail "Can't fill here."

159164solve :: RunTactic

160165solve ctxt env (Bind x (Guess ty val) sc)

161166 | 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)

163168 | otherwise = fail "I see a hole in your solution."

164169solve _ _ _ = fail "Not a guess."

165170

166171intro :: 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' =

168173 do let t' = normalise ctxt env t

169174 case t' of

170− Bind y (Pi s) t -> return $ Bind n (Lam s) (Bind x (Hole t) (V 0))

175+ Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

176+ return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

171177 _ -> fail "Nothing to introduce"

172178intro ctxt env _ _ = fail "Can't introduce here."

173179

@@ -184,15 +190,24 @@ check_in t ctxt env tm =

184190eval_in :: Raw -> RunTactic

185191eval_in t ctxt env tm =

186192 do (val, valty) <- lift $ check ctxt env t

187− action (Log (showEnv env (normalise ctxt env val) ++ " : " ++ showEnv env valty))

193+ let val' = normalise ctxt env val

194+ let valty' = normalise ctxt 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'))

188201 return tm

189202

190203

191204processTactic :: Tactic -> ProofState -> TC (ProofState, String)

192205processTactic QED ps = case holes ps of

193− [] -> return (ps { done = True }, "Proof complete.")

206+ [] -> let tm = finalise (pterm ps) in

207+ return (ps { done = True, pterm = tm },

208+ "Proof complete: " ++ showEnv [] tm)

194209 _ -> Error "Still holes to fill."

195−processTactic ProofState ps = return (ps, show (pterm ps))

210+processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

196211processTactic t ps = case holes ps of

197212 [] -> Error "Nothing to fill in."

198213 (h:_) -> do let n = nextname ps

src/Typecheck.hs+43−2

@@ -47,13 +47,14 @@ isSet ctxt env tm = isSet' (normalise ctxt env tm)

4747

4848check :: Context -> Env -> Raw -> TC (Term, Type)

4949check 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)

5151 | Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)

5252 | otherwise = do fail $ "No such variable " ++ show n

5353check ctxt env (RApp f a)

5454 = do (fv, fty) <- check ctxt env f

5555 (av, aty) <- check ctxt env a

5656 let fty' = normalise ctxt env fty

57+-- trace (showEnv env fty ++ " ===> " ++ showEnv env fty') $

5758 case fty' of

5859 Bind x (Pi s) t ->

5960 do converts ctxt env s aty

@@ -64,7 +65,7 @@ check ctxt env (RSet i) = return (Set i, Set (i+1))

6465check ctxt env (RBind n b sc)

6566 = do b' <- checkBinder b

6667 (scv, sct) <- check ctxt ((n, b'):env) sc

67− discharge n b' scv sct

68+ discharge n b' (pToV n scv) (pToV n sct)

6869 where checkBinder (Lam t)

6970 = do (tv, tt) <- check ctxt env t

7071 let tv' = normalise ctxt env tv

@@ -85,6 +86,14 @@ check ctxt env (RBind n b sc)

8586 converts ctxt env tv vt

8687 isSet ctxt env tt'

8788 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)

8897 checkBinder (Hole t)

8998 = do (tv, tt) <- check ctxt env t

9099 let tv' = normalise ctxt env tv

@@ -112,6 +121,8 @@ check ctxt env (RBind n b sc)

112121 = return (Bind n (Pi t) scv, sct)

113122 discharge n (Let t v) scv sct

114123 = 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)

115126 discharge n (Hole t) scv sct

116127 = do -- A hole can't appear in the type of its scope

117128 checkNotHoley 0 sct

@@ -130,6 +141,36 @@ check ctxt env (RBind n b sc)

130141 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc

131142 checkNotHoley _ _ = return ()

132143

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+

133174checkProgram :: Context -> RProgram -> TC Context

134175checkProgram ctxt [] = return ctxt

135176checkProgram ctxt ((n, RConst t):xs)

src/test.mi+1−1

@@ -8,6 +8,6 @@ three : N = S two;

99Vect : (A:Set 0) -> (n:N) -> Set 0;

1010Nil : (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));

1212

1313vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);