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

git.iko.soy/Idris-dev

Added refine, focus, undo

commit10b88ae2eb5b90a6dc88134d133b59f3b21c5f58 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 30 Oct 2011, 18:47 (15 years ago) parentebcb29b

6 files changed+67−32

compare with master

unifiedsplit

src/Core/Elaborate.hs+35−24 src/Core/ProofShell.hs+1−1 src/Idris/AbsSyntax.hs+3−3 src/Idris/ElabDecls.hs+5−1 src/Idris/Parser.hs+17−1 src/Idris/Prover.hs+6−2

src/Core/Elaborate.hs+35−24

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

2727 | Print Name

2828 | Tac (Elab ())

2929

30−type ElabState = (ProofState, String)

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

31+ deriving Show

3132type Elab a = StateT ElabState TC a

3233

3334proof :: 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"

3546

3647erun :: FC -> Elab a -> Elab a

3748erun f elab = do s <- get

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

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

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

4354

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

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

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

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

4657

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

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

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

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

4960

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

5162initElaborator = newProof

5263

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

5465elaborate 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

5667 return (a, str)

5768

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

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

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

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

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

6172 return ()

6273

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

6475

6576-- get the global context

6677get_context :: Elab Context

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

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

6879 return (context p)

6980

7081-- get the proof term

7182get_term :: Elab Term

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

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

7384 return (pterm p)

7485

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

7687get_env :: Elab Env

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

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

7889 lift $ envAtFocus p

7990

8091get_holes :: Elab [Name]

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

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

8293 return (holes p)

8394

8495-- get the current goal type

8596goal :: Elab Type

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

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

8798 b <- lift $ goalAtFocus p

8899 return (binderTy b)

89100

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

96107

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

98109get_deferred :: Elab [Name]

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

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

100111 return (deferred p)

101112

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

103114unique_hole :: Name -> Elab Name

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

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

105116 env <- get_env

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

107118 where

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

118129 readN x = read x

119130

120131elog :: String -> Elab ()

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

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

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

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

123134

124135-- The primitives, from ProofState

125136

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

191202

192203qed :: Elab Term

193204qed = do processTactic' QED

194− (p, _) <- get

205+ ES p _ _ <- get

195206 return (pterm p)

196207

197208undo :: Elab ()

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

205216 env <- get_env

206217 -- let claims = getArgs ty imps

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

208− (p, s) <- get

219+ ES p s prev <- get

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

210221 let n = length (filter not imps)

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

213224 return claims

214225 where

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

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

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

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

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

235− (p, s) <- get

246+ ES p s prev <- get

236247 let (n, hs) = unified p

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

239250 end_unify

240251 return args

241252

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

262273 elabClaims [] = return ()

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

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

265− do (p, _) <- get

276+ do ES p _ _ <- get

266277 focus n; elaboration; elabClaims xs

267278

268279 mkMN n@(MN _ _) = n

src/Core/ProofShell.hs+1−1

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

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

4343processCommand (Tac e) state

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

45− OK (ps', resp) ->

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

4646 if (not (done ps'))

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

4848 else (state { prf = Nothing,

src/Idris/AbsSyntax.hs+3−3

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

218218 | PElabError String -- error to report on elaboration

219219 deriving Eq

220220

221−data PTactic = Intro [Name]

222− | Refine Name

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

222+ | Refine Name [Bool]

223223 | Exact PTerm

224224 | Solve

225225 | Attack

226− | ProofState | ProofTerm

226+ | ProofState | ProofTerm | Undo

227227 | Qed

228228 deriving (Show, Eq)

229229

src/Idris/ElabDecls.hs+5−1

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

425425runTac :: PTactic -> Elab ()

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

427427runTac (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

429432runTac Solve = solve

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

431434

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

src/Idris/Parser.hs+17−1

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

592592pTactic :: SyntaxInfo -> IParser PTactic

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

594594 return $ Intro ns

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

596+ imps <- many1 imp

597+ return $ Refine n imps)

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

596− return $ Refine n

599+ i <- getState

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

601+ Nothing -> []

602+ Just args -> map isImp args

603+ return $ Refine n imps

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

605+ return $ Focus n

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

598607 i <- getState

599608 return $ Exact (desugar syn i t)

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

605614 return ProofState

606615 <|> do reserved "term"

607616 return ProofTerm

617+ <|> do reserved "undo"

618+ return Undo

608619 <|> do reserved "qed"

609620 return Qed

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

622+ isImp _ = False

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

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

625+

610626

611627-- Dealing with implicit arguments

612628

src/Idris/Prover.hs+6−2

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

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

3333prove ctxt n ty

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

3636 iLOG $ "Adding " ++ show tm

3737 lift $ dumpProof n prf

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

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

8888 (case cmd of

8989 Left err -> do iputStrLn (show err)

9090 return (False, e, False, prf)

91+ Right Undo ->

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

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

9194 Right ProofState ->

9295 return (True, e, False, prf)

9396 Right ProofTerm ->

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

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

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

99102 return (False, e, True, prf)

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

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

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

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

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

103107 return (False, e, False, prf))