4c68b68 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

EvalIn and CheckIn tactics

commit4c68b68f8c756359fbed66ee396d142241511ec2 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 24 Sep 2011, 17:28 (15 years ago) parentd615021

2 files changed+20−1

compare with master

unifiedsplit

src/ProofState.hs+18−1 src/ShellParser.hs+2

src/ProofState.hs+18−1

@@ -33,9 +33,12 @@ data Tactic = Attack

3333 | Fill Raw

3434 | Regret

3535 | Solve

36+ | EvalIn Raw

37+ | CheckIn Raw

3638 | Intro Name

3739 | ProofState

3840 | QED

41+-- Next: add 'EvalHere' and 'CheckHere' tactics

3942

4043data TacticAction = AddGoal Name

4144 | Solved Name

@@ -149,6 +152,19 @@ intro n ctxt env (Bind x (Hole t) (V 0)) =

149152 _ -> fail "Nothing to introduce"

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

151154

155+check_in :: Raw -> RunTactic

156+check_in t ctxt env tm =

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

158+ action (Log (showEnv env val ++ " : " ++ showEnv env valty))

159+ return tm

160+

161+eval_in :: Raw -> RunTactic

162+eval_in t ctxt env tm =

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

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

165+ return tm

166+

167+

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

153169processTactic QED ps = case holes ps of

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

@@ -179,4 +195,5 @@ process t h ps = tactic (Just h) ps (context ps) (mktac t)

179195 mktac Regret = regret

180196 mktac Solve = solve

181197 mktac (Intro n) = intro n

182−

198+ mktac (CheckIn r) = check_in r

199+ mktac (EvalIn r) = eval_in r

src/ShellParser.hs+2

@@ -50,6 +50,8 @@ pTactic = do reserved "attack"; return Attack

5050 <|> do reserved "regret"; return Regret

5151 <|> do reserved "solve"; return Solve

5252 <|> do reserved "intro"; n <- iName; return (Intro n)

53+ <|> do reserved "eval"; t <- pTerm; return (EvalIn t)

54+ <|> do reserved "check"; t <- pTerm; return (CheckIn t)

5355 <|> do reserved "state"; return ProofState

5456 <|> do reserved "qed"; return QED

5557