git.iko.soy/Idris-dev
on master help sign in
EvalIn and CheckIn tactics
4c68b68Edwin Brady
src/ProofState.hs+18−1
compare with master
unifiedsplit
@@ -33,9 +33,12 @@ data Tactic = Attack
33 | Fill Raw
33 | Fill Raw
34 | Regret
34 | Regret
35 | Solve
35 | Solve
36+ | EvalIn Raw
37+ | CheckIn Raw
36 | Intro Name
38 | Intro Name
37 | ProofState
39 | ProofState
38 | QED
40 | QED
41+-- Next: add 'EvalHere' and 'CheckHere' tactics
39
42
40data TacticAction = AddGoal Name
43data TacticAction = AddGoal Name
41 | Solved Name
44 | Solved Name
@@ -149,6 +152,19 @@ intro n ctxt env (Bind x (Hole t) (V 0)) =
149 _ -> fail "Nothing to introduce"
152 _ -> fail "Nothing to introduce"
150intro ctxt env _ _ = fail "Can't introduce here."
153intro ctxt env _ _ = fail "Can't introduce here."
151
154
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+
152processTactic :: Tactic -> ProofState -> TC (ProofState, String)
168processTactic :: Tactic -> ProofState -> TC (ProofState, String)
153processTactic QED ps = case holes ps of
169processTactic QED ps = case holes ps of
154 [] -> return (ps { done = True }, "Proof complete.")
170 [] -> return (ps { done = True }, "Proof complete.")
@@ -179,4 +195,5 @@ process t h ps = tactic (Just h) ps (context ps) (mktac t)
179 mktac Regret = regret
195 mktac Regret = regret
180 mktac Solve = solve
196 mktac Solve = solve
181 mktac (Intro n) = intro n
197 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
50 <|> do reserved "regret"; return Regret
50 <|> do reserved "regret"; return Regret
51 <|> do reserved "solve"; return Solve
51 <|> do reserved "solve"; return Solve
52 <|> do reserved "intro"; n <- iName; return (Intro n)
52 <|> 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)
53 <|> do reserved "state"; return ProofState
55 <|> do reserved "state"; return ProofState
54 <|> do reserved "qed"; return QED
56 <|> do reserved "qed"; return QED
55
57