10b88ae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added refine, focus, undo

10b88aeEdwin Brady15 years ago

src/Core/Elaborate.hs+35−24

compare with master

unifiedsplit

@@ -27,11 +27,22 @@ data Command = Theorem Name Raw

27 | Print Name

28 | Tac (Elab ())

30−type ElabState = (ProofState, String)

30+data ElabState = ES ProofState String (Maybe ElabState)

31+ deriving Show

31type Elab a = StateT ElabState TC a

32type Elab a = StateT ElabState TC a

33proof :: ElabState -> ProofState

34proof :: ElabState -> ProofState

34−proof = fst

35+proof (ES p _ _) = p

36+

37+saveState :: Elab ()

38+saveState = do e@(ES p s _) <- get

39+ put (ES p s (Just e))

40+

41+loadState :: Elab ()

42+loadState = do (ES p s e) <- get

43+ case e of

44+ Just st -> put st

45+ _ -> fail "Nothing to undo"

36erun :: FC -> Elab a -> Elab a

47erun :: FC -> Elab a -> Elab a

37erun f elab = do s <- get

48erun f elab = do s <- get

@@ -41,49 +52,49 @@ erun f elab = do s <- get

41 Error (At f e) -> lift $ Error (At f e)

52 Error (At f e) -> lift $ Error (At f e)

42 Error e -> lift $ Error (At f e)

53 Error e -> lift $ Error (At f e)

44−runElab :: Elab a -> ProofState -> TC (a, (ProofState, String))

55+runElab :: Elab a -> ProofState -> TC (a, ElabState)

45−runElab e ps = runStateT e (ps, "")

56+runElab e ps = runStateT e (ES ps "" Nothing)

47−execElab :: Elab a -> ProofState -> TC (ProofState, String)

58+execElab :: Elab a -> ProofState -> TC ElabState

48−execElab e ps = execStateT e (ps, "")

59+execElab e ps = execStateT e (ES ps "" Nothing)

50initElaborator :: Name -> Context -> Type -> ProofState

61initElaborator :: Name -> Context -> Type -> ProofState

51initElaborator = newProof

62initElaborator = newProof

53elaborate :: Context -> Name -> Type -> Elab a -> TC (a, String)

64elaborate :: Context -> Name -> Type -> Elab a -> TC (a, String)

54elaborate ctxt n ty elab = do let ps = initElaborator n ctxt ty

65elaborate ctxt n ty elab = do let ps = initElaborator n ctxt ty

55− (a, (ps', str)) <- runElab elab ps

66+ (a, ES ps' str _) <- runElab elab ps

56 return (a, str)

67 return (a, str)

58−processTactic' t = do (p, logs) <- get

69+processTactic' t = do ES p logs prev <- get

59 (p', log) <- lift $ processTactic t p

70 (p', log) <- lift $ processTactic t p

60− put (p', logs ++ log)

71+ put (ES p' (logs ++ log) prev)

61 return ()

72 return ()

63-- Some handy gadgets for pulling out bits of state

74-- Some handy gadgets for pulling out bits of state

65-- get the global context

76-- get the global context

66get_context :: Elab Context

77get_context :: Elab Context

67−get_context = do (p, _) <- get

78+get_context = do ES p _ _ <- get

68 return (context p)

79 return (context p)

70-- get the proof term

81-- get the proof term

71get_term :: Elab Term

82get_term :: Elab Term

72−get_term = do (p, _) <- get

83+get_term = do ES p _ _ <- get

73 return (pterm p)

84 return (pterm p)

75-- get the local context at the currently in focus hole

86-- get the local context at the currently in focus hole

76get_env :: Elab Env

87get_env :: Elab Env

77−get_env = do (p, _) <- get

88+get_env = do ES p _ _ <- get

78 lift $ envAtFocus p

89 lift $ envAtFocus p

80get_holes :: Elab [Name]

91get_holes :: Elab [Name]

81−get_holes = do (p, _) <- get

92+get_holes = do ES p _ _ <- get

82 return (holes p)

93 return (holes p)

84-- get the current goal type

95-- get the current goal type

85goal :: Elab Type

96goal :: Elab Type

86−goal = do (p, _) <- get

97+goal = do ES p _ _ <- get

87 b <- lift $ goalAtFocus p

98 b <- lift $ goalAtFocus p

88 return (binderTy b)

99 return (binderTy b)

100

@@ -96,12 +107,12 @@ get_type tm = do ctxt <- get_context

107

97-- get holes we've deferred for later definition

108-- get holes we've deferred for later definition

98get_deferred :: Elab [Name]

109get_deferred :: Elab [Name]

99−get_deferred = do (p, _) <- get

110+get_deferred = do ES p _ _ <- get

100 return (deferred p)

111 return (deferred p)

101

112

102-- given a desired hole name, return a unique hole name

113-- given a desired hole name, return a unique hole name

103unique_hole :: Name -> Elab Name

114unique_hole :: Name -> Elab Name

104−unique_hole n = do (p, _) <- get

115+unique_hole n = do ES p _ _ <- get

105 env <- get_env

116 env <- get_env

106 return (uniq n (holes p ++ map fst env))

117 return (uniq n (holes p ++ map fst env))

107 where

118 where

@@ -118,8 +129,8 @@ next (UN (x:xs)) = let (num', nm') = span isDigit (reverse x)

118 readN x = read x

129 readN x = read x

119

130

120elog :: String -> Elab ()

131elog :: String -> Elab ()

121−elog str = do (p, logs) <- get

132+elog str = do ES p logs prev <- get

122− put (p, logs ++ str ++ "\n")

133+ put (ES p (logs ++ str ++ "\n") prev)

123

134

124-- The primitives, from ProofState

135-- The primitives, from ProofState

125

136

@@ -191,7 +202,7 @@ proofstate = processTactic' ProofState

191

202

192qed :: Elab Term

203qed :: Elab Term

193qed = do processTactic' QED

204qed = do processTactic' QED

194− (p, _) <- get

205+ ES p _ _ <- get

195 return (pterm p)

206 return (pterm p)

196

207

197undo :: Elab ()

208undo :: Elab ()

@@ -205,11 +216,11 @@ prepare_apply fn imps =

205 env <- get_env

216 env <- get_env

206 -- let claims = getArgs ty imps

217 -- let claims = getArgs ty imps

207 claims <- doClaims (normalise ctxt env ty) imps []

218 claims <- doClaims (normalise ctxt env ty) imps []

208− (p, s) <- get

219+ ES p s prev <- get

209 -- reverse the claims we made so that args go left to right

220 -- reverse the claims we made so that args go left to right

210 let n = length (filter not imps)

221 let n = length (filter not imps)

211 let (h : hs) = holes p

222 let (h : hs) = holes p

212− put (p { holes = h : (reverse (take n hs) ++ drop n hs) }, s)

223+ put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }) s prev)

213 return claims

224 return claims

214 where

225 where

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

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

@@ -232,10 +243,10 @@ apply fn imps =

232 -- *Don't* solve the arguments we're specifying by hand.

243 -- *Don't* solve the arguments we're specifying by hand.

233 -- (remove from unified list before calling end_unify)

244 -- (remove from unified list before calling end_unify)

234 let dontunify = map fst (filter (not.snd) (zip args imps))

245 let dontunify = map fst (filter (not.snd) (zip args imps))

235− (p, s) <- get

246+ ES p s prev <- get

236 let (n, hs) = unified p

247 let (n, hs) = unified p

237 let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)

248 let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)

238− put (p { unified = unify }, s)

249+ put (ES (p { unified = unify }) s prev)

239 end_unify

250 end_unify

240 return args

251 return args

241

252

@@ -262,7 +273,7 @@ apply_elab n args =

262 elabClaims [] = return ()

273 elabClaims [] = return ()

263 elabClaims ((n, Nothing) : xs) = elabClaims xs

274 elabClaims ((n, Nothing) : xs) = elabClaims xs

264 elabClaims ((n, Just elaboration) : xs) =

275 elabClaims ((n, Just elaboration) : xs) =

265− do (p, _) <- get

276+ do ES p _ _ <- get

266 focus n; elaboration; elabClaims xs

277 focus n; elaboration; elabClaims xs

267

278

268 mkMN n@(MN _ _) = n

279 mkMN n@(MN _ _) = n

src/Core/ProofShell.hs+1−1

@@ -42,7 +42,7 @@ processCommand (Print n) state =

42 Nothing -> (state, "No such name")

43processCommand (Tac e) state

44 | Just ps <- prf state = case execElab e ps of

45− OK (ps', resp) ->

45+ OK (ES ps' resp _) ->

46 if (not (done ps'))

47 then (state { prf = Just ps' }, resp)

48 else (state { prf = Nothing,

src/Idris/AbsSyntax.hs+3−3

@@ -218,12 +218,12 @@ data PTerm = PQuote Raw

218 | PElabError String -- error to report on elaboration

219 deriving Eq

220

221−data PTactic = Intro [Name]

221+data PTactic = Intro [Name] | Focus Name

222− | Refine Name

222+ | Refine Name [Bool]

223 | Exact PTerm

224 | Solve

225 | Attack

226− | ProofState | ProofTerm

226+ | ProofState | ProofTerm | Undo

227 | Qed

228 deriving (Show, Eq)

229

src/Idris/ElabDecls.hs+5−1

@@ -425,7 +425,11 @@ collectDeferred t = return t

425runTac :: PTactic -> Elab ()

426runTac (Intro xs) = mapM_ (\x -> do attack; intro x) xs

427runTac (Exact tm) = do elab toplevel False tm

428− try solve (return ())

428+ solveAll

429+runTac (Refine fn imps) = do ns <- apply (Var fn) imps

430+ solveAll

431+runTac (Focus n) = focus n

429runTac Solve = solve

432runTac Solve = solve

430runTac x = fail $ "Not implemented " ++ show x

433runTac x = fail $ "Not implemented " ++ show x

431

434

435+solveAll = try (do solve; solveAll) (return ())

src/Idris/Parser.hs+17−1

@@ -592,8 +592,17 @@ pWhereblock syn = do reserved "where"; lchar '{'

592pTactic :: SyntaxInfo -> IParser PTactic

593pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

594 return $ Intro ns

595+ <|> try (do reserved "refine"; n <- pName

596+ imps <- many1 imp

597+ return $ Refine n imps)

595 <|> do reserved "refine"; n <- pName

598 <|> do reserved "refine"; n <- pName

599+ i <- getState

600+ let imps = case lookupCtxt n (idris_implicits i) of

601+ Nothing -> []

602+ Just args -> map isImp args

596− return $ Refine n

603+ return $ Refine n imps

604+ <|> do reserved "focus"; n <- pName

605+ return $ Focus n

597 <|> do reserved "exact"; t <- pExpr syn;

606 <|> do reserved "exact"; t <- pExpr syn;

598 i <- getState

607 i <- getState

599 return $ Exact (desugar syn i t)

608 return $ Exact (desugar syn i t)

@@ -605,8 +614,15 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

605 return ProofState

614 return ProofState

606 <|> do reserved "term"

615 <|> do reserved "term"

607 return ProofTerm

616 return ProofTerm

617+ <|> do reserved "undo"

618+ return Undo

608 <|> do reserved "qed"

619 <|> do reserved "qed"

609 return Qed

620 return Qed

621+ where isImp (PImp _ _ _) = True

622+ isImp _ = False

623+ imp = do lchar '?'; return False

624+ <|> do lchar '_'; return True

625+

610

626

611-- Dealing with implicit arguments

627-- Dealing with implicit arguments

612

628

src/Idris/Prover.hs+6−2

@@ -32,7 +32,7 @@ dumpProof n ps = do putStrLn $ show n ++ " = proof {"

32prove :: Context -> Name -> Type -> Idris ()

33prove ctxt n ty

34 = do let ps = initElaborator n ctxt ty

35− (tm, prf) <- ploop True ("-" ++ show n) [] (ps, "")

35+ (tm, prf) <- ploop True ("-" ++ show n) [] (ES ps "" Nothing)

36 iLOG $ "Adding " ++ show tm

37 lift $ dumpProof n prf

38 let tree = simpleCase False [(P Ref n ty, tm)]

@@ -88,6 +88,9 @@ ploop d prompt prf e

88 (case cmd of

89 Left err -> do iputStrLn (show err)

90 return (False, e, False, prf)

91+ Right Undo ->

92+ do (_, st) <- elabStep e loadState

93+ return (True, st, False, init prf)

91 Right ProofState ->

94 Right ProofState ->

92 return (True, e, False, prf)

95 return (True, e, False, prf)

93 Right ProofTerm ->

96 Right ProofTerm ->

@@ -97,7 +100,8 @@ ploop d prompt prf e

97 Right Qed -> do hs <- lifte e get_holes

100 Right Qed -> do hs <- lifte e get_holes

98 when (not (null hs)) $ fail "Incomplete proof"

101 when (not (null hs)) $ fail "Incomplete proof"

99 return (False, e, True, prf)

102 return (False, e, True, prf)

103+ Right tac -> do (_, e) <- elabStep e saveState

100− Right tac -> do (_, st) <- elabStep e (runTac tac)

104+ (_, st) <- elabStep e (runTac tac)

101 return (True, st, False, prf ++ [step]))

105 return (True, st, False, prf ++ [step]))

102 (\err -> do iputStrLn (report err)

106 (\err -> do iputStrLn (report err)

103 return (False, e, False, prf))

107 return (False, e, False, prf))