20 |
20 |
21 type record |
21 type record |
22 |
22 |
23 val from_store: Tactic.input -> Error_Pattern_Def.id list |
23 val from_store: Tactic.input -> Error_Pattern_Def.id list |
24 val filled_exactly: Calc.T -> string -> string * Tactic.input |
24 val filled_exactly: Calc.T -> string -> string * Tactic.input |
25 val check_for: term * term -> term * Env.T -> T list * Rule_Set.T -> id option |
25 val check_for: Proof.context -> term * term -> term * Env.T -> T list * Rule_Set.T -> id option |
26 |
26 |
27 val find_fill_patterns: Calc.T -> id -> record list |
27 val find_fill_patterns: Calc.T -> id -> record list |
28 |
28 |
29 \<^isac_test>\<open> |
29 \<^isac_test>\<open> |
30 val check_for': term * term -> subst -> id * term -> Rule_Set.T -> id option |
30 val check_for': Proof.context -> term * term -> subst -> id * term -> Rule_Set.T -> id option |
31 val fill_from_store: Subst.input option * Subst.T -> term -> id -> thm -> |
31 val fill_from_store: Subst.input option * Subst.T -> term -> id -> thm -> |
32 record list |
32 record list |
33 val fill_form: Subst.input option * Subst.T -> thm * term -> id -> fill_in -> |
33 val fill_form: Subst.input option * Subst.T -> thm * term -> id -> fill_in -> |
34 record option |
34 record option |
35 \<close> |
35 \<close> |
52 type record = (fill_in_id * term * thm * Subst.input option); |
52 type record = (fill_in_id * term * thm * Subst.input option); |
53 |
53 |
54 (* |
54 (* |
55 check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls |
55 check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls |
56 *) |
56 *) |
57 fun check_for' (res, inf) subst (id, pat) rls = |
57 fun check_for' ctxt (res, inf) subst (id, pat) rls = |
58 let |
58 let |
59 val ctxt = Proof_Context.init_global ((ThyC.Isac())) |
|
60 val (res', _, _, rewritten) = |
59 val (res', _, _, rewritten) = |
61 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty |
60 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty |
62 Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
61 Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
63 in |
62 in |
64 if rewritten then |
63 if rewritten then |
77 |
76 |
78 (* |
77 (* |
79 check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls; |
78 check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls; |
80 (prog, env) for retrieval of casual substitution for bdv in the pattern. |
79 (prog, env) for retrieval of casual substitution for bdv in the pattern. |
81 *) |
80 *) |
82 fun check_for (res, inf) (prog, env) (errpats, rls) = |
81 fun check_for ctxt (res, inf) (prog, env) (errpats, rls) = |
83 let |
82 let |
84 val (_, subst) = Subst.for_bdv prog env |
83 val (_, subst) = Subst.for_bdv prog env |
85 fun scan (_, [], _) = NONE |
84 fun scan (_, [], _) = NONE |
86 | scan (id, T :: errpats, _) = |
85 | scan (id, T :: errpats, _) = |
87 case check_for' (res, inf) subst (id, T) rls of |
86 case check_for' ctxt (res, inf) subst (id, T) rls of |
88 NONE => scan (id, errpats, []) |
87 NONE => scan (id, errpats, []) |
89 | SOME id => SOME id |
88 | SOME id => SOME id |
90 fun scans [] = NONE |
89 fun scans [] = NONE |
91 | scans (group :: groups) = |
90 | scans (group :: groups) = |
92 case scan group of |
91 case scan group of |