git.iko.soy/Idris-dev
on master help sign in
Change tactic names: fill for unify_fill and exact for fill
commitee3dbaa79497317ac2c993d0ac8230822b21af7c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 28 Sep 2011, 22:55 (15 years ago) parent5dadd08
3 files changed+13−13
compare with master
unifiedsplit
src/Elaborate.hs+4−4 src/ProofState.hs+8−8 src/ShellParser.hs+1−1
src/Elaborate.hs+4−4
@@ -92,12 +92,12 @@ attack = processTactic' Attack
9292claim :: Name -> Raw -> Elab ()
9393claim n t = processTactic' (Claim n t)
9494
95+exact :: Raw -> Elab ()
96+exact t = processTactic' (Exact t)
97+
9598fill :: Raw -> Elab ()
9699fill t = processTactic' (Fill t)
97100
98−unify_fill :: Raw -> Elab ()
99−unify_fill t = processTactic' (UnifyFill t)
100−
101101solve :: Elab ()
102102solve = processTactic' Solve
103103
@@ -156,7 +156,7 @@ prepare_apply fn imps =
156156apply :: Raw -> [Bool] -> Elab ()
157157apply fn imps =
158158 do args <- prepare_apply fn imps
159− unify_fill (raw_apply fn (map Var args))
159+ fill (raw_apply fn (map Var args))
160160
161161-- Abstract over an argument of unknown type, giving a name for the hole
162162-- which we'll fill with the argument type too.
src/ProofState.hs+8−8
@@ -34,8 +34,8 @@ data Goal = GD { premises :: Env,
3434
3535data Tactic = Attack
3636 | Claim Name Raw
37+ | Exact Raw
3738 | Fill Raw
38− | UnifyFill Raw
3939 | Regret
4040 | Solve
4141 | Compute
@@ -179,17 +179,17 @@ movelast n ctxt env t = do action (MoveGoal n)
179179regret :: RunTactic
180180regret = undefined
181181
182−fill :: Raw -> RunTactic
183−fill guess ctxt env (Bind x (Hole ty) sc) =
182+exact :: Raw -> RunTactic
183+exact guess ctxt env (Bind x (Hole ty) sc) =
184184 do (val, valty) <- lift $ check ctxt env guess
185185 lift $ converts ctxt env valty ty
186186 return $ Bind x (Guess ty val) sc
187−fill _ _ _ _ = fail "Can't fill here."
187+exact _ _ _ _ = fail "Can't fill here."
188188
189189-- As fill, but attempts to solve other goals by unification
190190
191−unify_fill :: Raw -> RunTactic
192−unify_fill guess ctxt env (Bind x (Hole ty) sc) =
191+fill :: Raw -> RunTactic
192+fill guess ctxt env (Bind x (Hole ty) sc) =
193193 do (val, valty) <- lift $ check ctxt env guess
194194 ns <- lift $ unify ctxt env valty ty
195195 solve_all ns
@@ -198,7 +198,7 @@ unify_fill guess ctxt env (Bind x (Hole ty) sc) =
198198 solve_all [] = return ()
199199 solve_all ((n, tm): ns) = do action (AlsoSolved n tm)
200200 solve_all ns
201−unify_fill _ _ _ _ = fail "Can't fill here."
201+fill _ _ _ _ = fail "Can't fill here."
202202
203203solve :: RunTactic
204204solve ctxt env (Bind x (Guess ty val) sc)
@@ -303,8 +303,8 @@ process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
303303process t h ps = tactic (Just h) ps (context ps) (mktac t)
304304 where mktac Attack = attack
305305 mktac (Claim n r) = claim n r
306+ mktac (Exact r) = exact r
306307 mktac (Fill r) = fill r
307− mktac (UnifyFill r) = unify_fill r
308308 mktac Regret = regret
309309 mktac Solve = solve
310310 mktac Compute = compute
src/ShellParser.hs+1−1
@@ -48,8 +48,8 @@ pTactic = do reserved "attack"; return attack
4848 <|> do reserved "claim"; n <- iName; lchar ':'; ty <- pTerm
4949 return (claim n ty)
5050 <|> do reserved "regret"; return regret
51+ <|> do reserved "exact"; tm <- pTerm; return (exact tm)
5152 <|> do reserved "fill"; tm <- pTerm; return (fill tm)
52− <|> do reserved "unify"; tm <- pTerm; return (unify_fill tm)
5353 <|> do reserved "apply"; tm <- pTerm; args <- many pArgType;
5454 return (apply tm args)
5555 <|> do reserved "solve"; return solve