c966457 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Just use proof state as TState

c966457Edwin Brady15 years ago

src/CoreParser.hs+1−7

compare with master

unifiedsplit

@@ -64,7 +64,6 @@ pTerm = try (do chainl1 pNoApp app)

64pNoApp :: Parser Raw

65pNoApp = try (chainr1 pExp arrow)

66 <|> pExp

67−

68pExp :: Parser Raw

67pExp :: Parser Raw

69pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

68pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

70 symbol "=>";

69 symbol "=>";

@@ -73,7 +72,7 @@ pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

73 <|> try (do lchar '?'; x <- iName; lchar ':'; ty <- pTerm

72 <|> try (do lchar '?'; x <- iName; lchar ':'; ty <- pTerm

74 lchar '.';

73 lchar '.';

75 sc <- pTerm

74 sc <- pTerm

76− return (RBind x (Lam ty) sc))

75+ return (RBind x (Hole ty) sc))

77 <|> try (do lchar '(';

76 <|> try (do lchar '(';

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

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

79 lchar ')';

78 lchar ')';

@@ -84,11 +83,6 @@ pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

84 t <- pTerm

83 t <- pTerm

85 lchar ')'

84 lchar ')'

86 return t)

85 return t)

87− <|> try (do lchar '?';

88− x <- iName; lchar ':'; ty <- pTerm

89− lchar '.';

90− sc <- pTerm

91− return (RBind x (Hole ty) sc))

92 <|> try (do symbol "??";

86 <|> try (do symbol "??";

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

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

94 lchar '=';

88 lchar '=';

src/Elaborate.hs+8

@@ -101,6 +101,12 @@ fill t = processTactic' (Fill t)

101solve :: Elab ()

102solve = processTactic' Solve

103

104+start_unify :: Name -> Elab ()

105+start_unify n = processTactic' (StartUnify n)

106+

107+end_unify :: Elab ()

108+end_unify = processTactic' EndUnify

109+

104regret :: Elab ()

110regret :: Elab ()

105regret = processTactic' Regret

111regret = processTactic' Regret

106

112

@@ -146,6 +152,7 @@ prepare_apply fn imps =

146 where

152 where

147 doClaims (Bind n' (Pi t) sc) (i : is) claims =

153 doClaims (Bind n' (Pi t) sc) (i : is) claims =

148 do n <- unique_hole n'

154 do n <- unique_hole n'

155+ when (null claims) (start_unify n)

149 let sc' = instantiate (P Bound n t) sc

156 let sc' = instantiate (P Bound n t) sc

150 claim n (forget t)

157 claim n (forget t)

151 when i (movelast n)

158 when i (movelast n)

@@ -157,6 +164,7 @@ apply :: Raw -> [Bool] -> Elab ()

157apply fn imps =

164apply fn imps =

158 do args <- prepare_apply fn imps

165 do args <- prepare_apply fn imps

159 fill (raw_apply fn (map Var args))

166 fill (raw_apply fn (map Var args))

167+ when (not (null args)) end_unify

160

168

161-- Abstract over an argument of unknown type, giving a name for the hole

169-- Abstract over an argument of unknown type, giving a name for the hole

162-- which we'll fill with the argument type too.

170-- which we'll fill with the argument type too.

src/ProofState.hs+85−76

@@ -22,9 +22,11 @@ data ProofState = PS { thname :: Name,

22 nextname :: Int, -- name supply

23 pterm :: Term, -- current proof term

24 ptype :: Type, -- original goal

25+ unified :: (Name, [(Name, Term)]),

25 defer :: [(Name, Type)], -- names we'll need to define

26 defer :: [(Name, Type)], -- names we'll need to define

26 previous :: Maybe ProofState, -- for undo

27 previous :: Maybe ProofState, -- for undo

27 context :: Context,

28 context :: Context,

29+ plog :: String,

28 done :: Bool

30 done :: Bool

29 }

31 }

@@ -38,6 +40,8 @@ data Tactic = Attack

38 | Fill Raw

40 | Fill Raw

39 | Regret

41 | Regret

40 | Solve

42 | Solve

43+ | StartUnify Name

44+ | EndUnify

41 | Compute

45 | Compute

42 | EvalIn Raw

46 | EvalIn Raw

43 | CheckIn Raw

47 | CheckIn Raw

@@ -55,14 +59,14 @@ data TacticAction = AddGoal Name -- add a new goal, solve immediately

55 | FocusGoal Name -- focus on this goal next

59 | FocusGoal Name -- focus on this goal next

56 | MoveGoal Name -- move this goal to the end of the hole queue

60 | MoveGoal Name -- move this goal to the end of the hole queue

57 | Solved Name

61 | Solved Name

58− | AlsoSolved Name Term -- goals solved by unification

62+ | AlsoSolved [(Name, Term)] -- variables solved by unification

59 | Log String

63 | Log String

61-- Some utilites on proof and tactic states

65-- Some utilites on proof and tactic states

63instance Show ProofState where

67instance Show ProofState where

64− show (PS nm [] _ tm _ _ _ _ _) = show nm ++ ": no more goals"

68+ show (PS nm [] _ tm _ _ _ _ _ _ _) = show nm ++ ": no more goals"

65− show (PS nm (h:hs) _ tm _ i _ ctxt _)

69+ show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)

66 = let OK g = goal (Just h) tm

70 = let OK g = goal (Just h) tm

67 wkenv = premises g in

71 wkenv = premises g in

68 showPs wkenv (reverse wkenv) ++ "\n" ++

72 showPs wkenv (reverse wkenv) ++ "\n" ++

@@ -93,21 +97,25 @@ hole _ = False

93holeName i = MN i "hole"

97holeName i = MN i "hole"

95getName :: Monad m => String -> StateT TState m Name

99getName :: Monad m => String -> StateT TState m Name

96−getName tag = do (n, ts) <- get

100+getName tag = do ps <- get

101+ let n = nextname ps

97− put (n+1, ts)

102+ put (ps { nextname = n+1 })

98 return $ MN n tag

103 return $ MN n tag

104

100−action :: Monad m => TacticAction -> StateT TState m ()

105+action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()

101−action a = do (n, ts) <- get

106+action a = do ps <- get

102− put (n, a:ts)

107+ put (a ps)

108+

109+addLog :: Monad m => String -> StateT TState m ()

110+addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

103

111

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

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

105newProof n ctxt ty = let h = holeName 0

113newProof n ctxt ty = let h = holeName 0

106 ty' = vToP ty in

114 ty' = vToP ty in

107− PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty []

115+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) []

108− Nothing ctxt False

116+ Nothing ctxt "" False

109

117

110−type TState = (Int, [TacticAction])

118+type TState = ProofState -- [TacticAction])

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

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

112type Hole = Maybe Name -- Nothing = default hole, first in list in proof state

120type Hole = Maybe Name -- Nothing = default hole, first in list in proof state

113

121

@@ -134,27 +142,28 @@ goal h tm = g [] tm where

134 gb env (Guess t v) = g env t `mplus` g env v

142 gb env (Guess t v) = g env t `mplus` g env v

135 gb env t = g env (binderTy t)

143 gb env t = g env (binderTy t)

136

144

137−tactic :: Hole -> ProofState -> Context -> RunTactic -> StateT TState TC ProofState

145+tactic :: Hole -> RunTactic -> StateT TState TC ()

138−tactic h ps ctxt f = do let tm = pterm ps

146+tactic h f = do ps <- get

139− tm' <- atH [] tm

147+ tm' <- atH (context ps) [] (pterm ps)

148+ ps <- get -- might have changed while processing

140− return (ps { pterm = tm' })

149+ put (ps { pterm = tm' })

141 where

150 where

142− atH env binder@(Bind n b sc)

151+ atH c env binder@(Bind n b sc)

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

152+ | hole b && same h n = f c env binder

144 | otherwise

153 | otherwise

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

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

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

155+ atH c env (App f a) = pure App <*> atH c env f <*> atH c env a

147− atH env t = return t

156+ atH c env t = return t

148

157

149− atHb env (Let t v) = pure Let <*> atH env t <*> atH env v

158+ atHb c env (Let t v) = pure Let <*> atH c env t <*> atH c env v

150− atHb env (Guess t v) = pure Guess <*> atH env t <*> atH env v

159+ atHb c env (Guess t v) = pure Guess <*> atH c env t <*> atH c env v

151− atHb env t = do ty' <- atH env (binderTy t)

160+ atHb c env t = do ty' <- atH c env (binderTy t)

152− return $ t { binderTy = ty' }

161+ return $ t { binderTy = ty' }

153

162

154attack :: RunTactic

163attack :: RunTactic

155attack ctxt env (Bind x (Hole t) sc)

164attack ctxt env (Bind x (Hole t) sc)

156 = do h <- getName "hole"

165 = do h <- getName "hole"

157− action (AddGoal h)

166+ action (\ps -> ps { holes = h : holes ps })

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

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

159 where

168 where

160 newtm h = Bind h (Hole t) (P Bound h t)

169 newtm h = Bind h (Hole t) (P Bound h t)

@@ -164,15 +173,22 @@ claim :: Name -> Raw -> RunTactic

164claim n ty ctxt env t =

173claim n ty ctxt env t =

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

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

166 lift $ isSet ctxt env tyt

175 lift $ isSet ctxt env tyt

167− action (NextGoal n)

176+ action (\ps -> let (g:gs) = holes ps in

177+ ps { holes = g : n : gs } )

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

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

169

179

170focus :: Name -> RunTactic

180focus :: Name -> RunTactic

171−focus n ctxt env t = do action (FocusGoal n)

181+focus n ctxt env t = do action (\ps -> let hs = holes ps in

182+ if n `elem` hs

183+ then ps { holes = n : (hs \\ [n]) }

184+ else ps)

172 return t

185 return t

173

186

174movelast :: Name -> RunTactic

187movelast :: Name -> RunTactic

175−movelast n ctxt env t = do action (MoveGoal n)

188+movelast n ctxt env t = do action (\ps -> let hs = holes ps in

189+ if n `elem` hs

190+ then ps { holes = (hs \\ [n]) ++ [n] }

191+ else ps)

176 return t

192 return t

177

193

178-- Hmmm. YAGNI?

194-- Hmmm. YAGNI?

@@ -192,17 +208,16 @@ fill :: Raw -> RunTactic

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

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

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

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

194 ns <- lift $ unify ctxt env valty ty

210 ns <- lift $ unify ctxt env valty ty

195− solve_all ns

211+ ps <- get

212+ let (uh, uns) = unified ps

213+ put (ps { unified = (uh, uns ++ ns) })

214+ addLog (show (uh, uns ++ ns))

196 return $ Bind x (Guess ty val) sc

215 return $ Bind x (Guess ty val) sc

197− where

198− solve_all [] = return ()

199− solve_all ((n, tm): ns) = do action (AlsoSolved n tm)

200− solve_all ns

201fill _ _ _ _ = fail "Can't fill here."

216fill _ _ _ _ = fail "Can't fill here."

202

217

203solve :: RunTactic

218solve :: RunTactic

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

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

205− | pureTerm val = do action (Solved x)

220+ | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })

206 return $ Bind x (Let ty val) sc -- instantiate val (pToV x sc)

221 return $ Bind x (Let ty val) sc -- instantiate val (pToV x sc)

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

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

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

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

@@ -236,7 +251,7 @@ compute ctxt env (Bind x (Hole ty) sc) =

236check_in :: Raw -> RunTactic

251check_in :: Raw -> RunTactic

237check_in t ctxt env tm =

252check_in t ctxt env tm =

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

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

239− action (Log (showEnv env val ++ " : " ++ showEnv env valty))

254+ addLog (showEnv env val ++ " : " ++ showEnv env valty)

240 return tm

255 return tm

241

256

242eval_in :: Raw -> RunTactic

257eval_in :: Raw -> RunTactic

@@ -244,14 +259,34 @@ eval_in t ctxt env tm =

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

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

245 let val' = normalise ctxt env val

260 let val' = normalise ctxt env val

246 let valty' = normalise ctxt env valty

261 let valty' = normalise ctxt env valty

247− action (Log (showEnv env val ++ " : " ++

262+ addLog (showEnv env val ++ " : " ++

248− showEnv env valty ++

263+ showEnv env valty ++

249-- " in " ++ show env ++

264-- " in " ++ show env ++

250− " ==>\n " ++

265+ " ==>\n " ++

251− showEnv env val' ++ " : " ++

266+ showEnv env val' ++ " : " ++

252− showEnv env valty'))

267+ showEnv env valty')

253 return tm

268 return tm

254

269

270+start_unify :: Name -> RunTactic

271+start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })

272+ return tm

273+

274+solve_unified :: RunTactic

275+solve_unified ctxt env tm =

276+ do ps <- get

277+ let (_, ns) = unified ps

278+ action (\ps -> ps { holes = holes ps \\ map fst ns })

279+ return (updateSolved ns tm)

280+ where

281+ updateSolved xs (Bind n b@(Hole _) t)

282+ | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

283+ updateSolved xs (Bind n b t)

284+ | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

285+ updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

286+ updateSolved xs (P _ n _)

287+ | Just v <- lookup n xs = v

288+ updateSolved xs t = t

289+

255-- shuffleHoles :: Term -> Term

290-- shuffleHoles :: Term -> Term

256-- shuffleHoles tm = shuffle [] tm

291-- shuffleHoles tm = shuffle [] tm

257-- where

292-- where

@@ -273,48 +308,22 @@ processTactic t ps

273 = case holes ps of

308 = case holes ps of

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

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

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

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

276− (ps', (n', actions)) <- runStateT (process t h ps) (n, [])

311+ ps' <- execStateT (process t h) ps

277− return (ps' { nextname = n',

278− pterm = updateSolved (getSolved actions) (pterm ps'),

279− holes = goals (holes ps') actions,

280− previous = Just ps },

312+ return (ps' { previous = Just ps, plog = "" }, plog ps')

281− logs actions)

313+

282− where logs [] = ""

283− logs (Log x : xs) = x ++ "\n" ++ logs xs

284− logs (_ : xs) = logs xs

285−

286− goals g [] = g

287− goals g (AddGoal n : xs) = goals (n : g) xs

288− goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs

289− goals g (FocusGoal n : xs)

290− | n `elem` g = goals (n : (g \\ [n])) xs

291− goals g (MoveGoal n : xs)

292− | n `elem` g = goals ((g \\ [n]) ++ [n]) xs

293− goals g (Solved n : xs) = goals (g \\ [n]) xs

294− goals g (AlsoSolved n tm : xs) = goals (g \\ [n]) xs

295− goals g (_ : xs) = goals g xs

296−

297− getSolved [] = []

298− getSolved (AlsoSolved n tm : xs) = (n, tm) : getSolved xs

299− getSolved (_ : xs) = getSolved xs

300−

301− updateSolved xs (Bind n b@(Hole _) t)

302− | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

303− updateSolved xs (Bind n b t)

304− | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

305− updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

306− updateSolved xs (P _ n _)

307− | Just v <- lookup n xs = v

308− updateSolved xs t = t

309−

310−process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState

314+process :: Tactic -> Name -> StateT TState TC ()

311−process t h ps = tactic (Just h) ps (context ps) (mktac t)

315+process EndUnify _

316+ = do ps <- get

317+ let (h, _) = unified ps

318+ tactic (Just h) solve_unified

319+process t h = tactic (Just h) (mktac t)

312 where mktac Attack = attack

320 where mktac Attack = attack

313 mktac (Claim n r) = claim n r

321 mktac (Claim n r) = claim n r

314 mktac (Exact r) = exact r

322 mktac (Exact r) = exact r

315 mktac (Fill r) = fill r

323 mktac (Fill r) = fill r

316 mktac Regret = regret

324 mktac Regret = regret

317 mktac Solve = solve

325 mktac Solve = solve

326+ mktac (StartUnify n) = start_unify n

318 mktac Compute = compute

327 mktac Compute = compute

319 mktac (Intro n) = intro n

328 mktac (Intro n) = intro n

320 mktac (Forall n t) = forall n t

329 mktac (Forall n t) = forall n t