git.iko.soy/Idris-dev
on master help sign in
Change tactic names: fill for unify_fill and exact for fill
ee3dbaaEdwin Brady
src/Elaborate.hs+4−4
compare with master
unifiedsplit
@@ -92,12 +92,12 @@ attack = processTactic' Attack
92claim :: Name -> Raw -> Elab ()
92claim :: Name -> Raw -> Elab ()
93claim n t = processTactic' (Claim n t)
93claim n t = processTactic' (Claim n t)
94
94
95+exact :: Raw -> Elab ()
96+exact t = processTactic' (Exact t)
97+
95fill :: Raw -> Elab ()
98fill :: Raw -> Elab ()
96fill t = processTactic' (Fill t)
99fill t = processTactic' (Fill t)
97
100
98−unify_fill :: Raw -> Elab ()
99−unify_fill t = processTactic' (UnifyFill t)
100−
101solve :: Elab ()
101solve :: Elab ()
102solve = processTactic' Solve
102solve = processTactic' Solve
103
103
@@ -156,7 +156,7 @@ prepare_apply fn imps =
156apply :: Raw -> [Bool] -> Elab ()
156apply :: Raw -> [Bool] -> Elab ()
157apply fn imps =
157apply fn imps =
158 do args <- prepare_apply fn imps
158 do args <- prepare_apply fn imps
159− unify_fill (raw_apply fn (map Var args))
159+ fill (raw_apply fn (map Var args))
160
160
161-- Abstract over an argument of unknown type, giving a name for the hole
161-- Abstract over an argument of unknown type, giving a name for the hole
162-- which we'll fill with the argument type too.
162-- which we'll fill with the argument type too.
src/ProofState.hs+8−8
@@ -34,8 +34,8 @@ data Goal = GD { premises :: Env,
34
34
35data Tactic = Attack
35data Tactic = Attack
36 | Claim Name Raw
36 | Claim Name Raw
37+ | Exact Raw
37 | Fill Raw
38 | Fill Raw
38− | UnifyFill Raw
39 | Regret
39 | Regret
40 | Solve
40 | Solve
41 | Compute
41 | Compute
@@ -179,17 +179,17 @@ movelast n ctxt env t = do action (MoveGoal n)
179regret :: RunTactic
179regret :: RunTactic
180regret = undefined
180regret = undefined
181
181
182−fill :: Raw -> RunTactic
182+exact :: Raw -> RunTactic
183−fill guess ctxt env (Bind x (Hole ty) sc) =
183+exact guess ctxt env (Bind x (Hole ty) sc) =
184 do (val, valty) <- lift $ check ctxt env guess
184 do (val, valty) <- lift $ check ctxt env guess
185 lift $ converts ctxt env valty ty
185 lift $ converts ctxt env valty ty
186 return $ Bind x (Guess ty val) sc
186 return $ Bind x (Guess ty val) sc
187−fill _ _ _ _ = fail "Can't fill here."
187+exact _ _ _ _ = fail "Can't fill here."
188
188
189-- As fill, but attempts to solve other goals by unification
189-- As fill, but attempts to solve other goals by unification
190
190
191−unify_fill :: Raw -> RunTactic
191+fill :: Raw -> RunTactic
192−unify_fill guess ctxt env (Bind x (Hole ty) sc) =
192+fill guess ctxt env (Bind x (Hole ty) sc) =
193 do (val, valty) <- lift $ check ctxt env guess
193 do (val, valty) <- lift $ check ctxt env guess
194 ns <- lift $ unify ctxt env valty ty
194 ns <- lift $ unify ctxt env valty ty
195 solve_all ns
195 solve_all ns
@@ -198,7 +198,7 @@ unify_fill guess ctxt env (Bind x (Hole ty) sc) =
198 solve_all [] = return ()
198 solve_all [] = return ()
199 solve_all ((n, tm): ns) = do action (AlsoSolved n tm)
199 solve_all ((n, tm): ns) = do action (AlsoSolved n tm)
200 solve_all ns
200 solve_all ns
201−unify_fill _ _ _ _ = fail "Can't fill here."
201+fill _ _ _ _ = fail "Can't fill here."
202
202
203solve :: RunTactic
203solve :: RunTactic
204solve ctxt env (Bind x (Guess ty val) sc)
204solve ctxt env (Bind x (Guess ty val) sc)
@@ -303,8 +303,8 @@ process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
303process t h ps = tactic (Just h) ps (context ps) (mktac t)
303process t h ps = tactic (Just h) ps (context ps) (mktac t)
304 where mktac Attack = attack
304 where mktac Attack = attack
305 mktac (Claim n r) = claim n r
305 mktac (Claim n r) = claim n r
306+ mktac (Exact r) = exact r
306 mktac (Fill r) = fill r
307 mktac (Fill r) = fill r
307− mktac (UnifyFill r) = unify_fill r
308 mktac Regret = regret
308 mktac Regret = regret
309 mktac Solve = solve
309 mktac Solve = solve
310 mktac Compute = compute
310 mktac Compute = compute
src/ShellParser.hs+1−1
@@ -48,8 +48,8 @@ pTactic = do reserved "attack"; return attack
48 <|> do reserved "claim"; n <- iName; lchar ':'; ty <- pTerm
48 <|> do reserved "claim"; n <- iName; lchar ':'; ty <- pTerm
49 return (claim n ty)
49 return (claim n ty)
50 <|> do reserved "regret"; return regret
50 <|> do reserved "regret"; return regret
51+ <|> do reserved "exact"; tm <- pTerm; return (exact tm)
51 <|> do reserved "fill"; tm <- pTerm; return (fill tm)
52 <|> do reserved "fill"; tm <- pTerm; return (fill tm)
52− <|> do reserved "unify"; tm <- pTerm; return (unify_fill tm)
53 <|> do reserved "apply"; tm <- pTerm; args <- many pArgType;
53 <|> do reserved "apply"; tm <- pTerm; args <- many pArgType;
54 return (apply tm args)
54 return (apply tm args)
55 <|> do reserved "solve"; return solve
55 <|> do reserved "solve"; return solve