1 (* title: Interpret/error-pattern.sml
4 (c) due to copyright terms
6 In case a term is input, which contains an "error pattern" (provided by a mathauthor),
7 several "fill_ins" can be presented as help for the next step.)
10 signature ERROR_PATTERN =
12 type id = Error_Pattern_Def.id
13 type T = Error_Pattern_Def.T
14 val s_to_string : Proof.context -> T list -> string
17 type fill_in_id = Error_Pattern_Def.fill_in_id
18 type fill_in = Error_Pattern_Def.fill_in
19 val fill_in_empty: fill_in
21 val from_store: Proof.context -> Tactic.input -> id list
22 val filled_exactly: Calc.T -> string -> string * Tactic.input
23 val check_for: Proof.context -> term * term -> term * Env.T -> T list * Rule_Set.T -> id option
25 val get_fill_ins: theory -> fill_in_id -> fill_in list
26 val store_fill_ins: (fill_in_id * fill_in list) list -> theory -> theory
28 (*val find_fill_ins: Calc.T -> id -> record list*)
29 val find_fill_patterns: Calc.T -> id -> record list
30 (*from isac_test for Minisubpbl*)
31 val fill_from_store: Proof.context -> Subst.input option * Subst.T -> term -> id -> thm ->
33 val fill_form: Proof.context -> Subst.input option * Subst.T -> thm * term -> id -> fill_in ->
37 val get_fill_inss: theory -> (fill_in_id * fill_in list) list
38 val check_for': Proof.context -> term * term -> subst -> id * term -> Rule_Set.T -> id option
43 structure Error_Pattern(**): ERROR_PATTERN(**) =
47 type id = Error_Pattern_Def.id;
48 type T = Error_Pattern_Def.T;
49 val s_to_string = Error_Pattern_Def.s_to_string;
50 val empty = ("e_errpatID", [ParseC.patt_opt @{theory} "?a = ?b" |> the], [@{thm refl}])
52 type fill_in_id = Error_Pattern_Def.fill_in_id;
53 type fill_in = Error_Pattern_Def.fill_in;
54 val fill_in_empty = ("e_fillpatID", ParseC.patt_opt @{theory} "?a = _" |> the, "e_errpatID")
56 type record = (fill_in_id * term * thm * Subst.input option);
58 structure Data = Theory_Data (
59 type T = (fill_in_id * fill_in list) list;
61 val merge = merge op=;
63 fun get_fill_inss thy = Data.get thy
64 fun store_fill_ins fill_in = Data.map (curry (Library.merge op=) fill_in)
65 fun get_fill_ins thy fill_in_id =
66 case AList.lookup (op =) (get_fill_inss thy) fill_in_id of
67 SOME fill_ins => fill_ins
68 | NONE => raise ERROR ("fill_ins for thm \"" ^ fill_in_id ^ "\" missing in theory \"" ^
69 (thy |> ThyC.id_of) ^ "\" (and ancestors)" ^
70 "\nTODO exception hierarchy needs to be established.")
73 check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls
75 fun check_for' ctxt (res, inf) subst (id, pat) rls =
77 val (res', _, _, rewritten) =
78 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty
79 Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
83 val norm_res = case Rewrite.rewrite_set_inst_ ctxt false subst rls res' of
85 | SOME (norm_res, _) => norm_res
86 val norm_inf = case Rewrite.rewrite_set_inst_ ctxt false subst rls inf of
88 | SOME (norm_inf, _) => norm_inf
90 if norm_res = norm_inf then SOME id else NONE
96 check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
97 (prog, env) for retrieval of casual substitution for bdv in the pattern.
99 fun check_for ctxt (res, inf) (prog, env) (errpats, rls) =
101 val (_, subst) = Subst.for_bdv ctxt prog env
102 fun scan (_, [], _) = NONE
103 | scan (id, T :: errpats, _) =
104 case check_for' ctxt (res, inf) subst (id, T) rls of
105 NONE => scan (id, errpats, [])
108 | scans (group :: groups) =
112 in scans errpats end;
114 (* fill-in patterns an forms.
115 returns thm required by "fun in_fillform *)
116 fun fill_form ctxt (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) =
118 val (form', _, _, rewritten) =
119 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
120 in (*the fillpat of the thm must be dedicated to id*)
121 if id = erpaID andalso rewritten then
122 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
126 fun fill_from_store ctxt subst form errpat_id thm =
128 val thm_id_long = Thm.get_name_hint thm
129 val thm_id = ThmC.cut_longid thm_id_long
130 val fill_ins = get_fill_ins (Proof_Context.theory_of ctxt) thm_id;
131 val some = map (fill_form ctxt subst (thm, form) errpat_id) fill_ins;
132 in some |> filter is_some |> map the end
134 fun find_fill_patterns (pt, pos as (p, _): Pos.pos') id =
136 val ctxt = Ctree.get_ctxt pt pos
137 val f_curr = Ctree.get_curr_formula (pt, pos)
138 val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)
139 val (errpats, prog) = (* after shift to Diff.thy -------vvvvvvvvvvvvvvv ctxt should be sufficient*)
140 case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of
141 {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
142 | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
143 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
144 val subst = Subst.for_bdv ctxt prog env
145 val errpat_thms = errpats
146 |> filter ((curry op = id) o (#1: Error_Pattern_Def.T -> Error_Pattern_Def.id))
147 |> map (#3: Error_Pattern_Def.T -> thm list)
149 in map (fill_from_store (Ctree.get_ctxt pt pos) subst f_curr id) errpat_thms |> flat end
152 Check input on a fill-pattern:
153 check if input is exactly equal to the rewrite from a rule
154 which is stored at the pos where the input is stored of "ok".
156 (*will come directly from PIDE --------vvvvvvvvvvv*)
157 fun filled_exactly (pt, pos as (p, _)) (istr(*, pp*)) =
159 val ctxt = (Ctree.get_ctxt pt pos)
160 val ifo = Syntax.read_term ctxt istr
161 handle ERROR msg => error (msg (*^ Position.here pp*))
162 val p' = Pos.lev_on p;
163 val tac = Ctree.get_obj Ctree.g_tac pt p';
165 case Solve_Step.check tac (pt, pos) of
166 Applicable.No msg => (msg, Tactic.Tac "")
167 | Applicable.Yes rew =>
169 val res = case rew of
170 Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
171 |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
172 | t => raise ERROR ("filled_exactly: uncovered case for " ^ Tactic.string_of ctxt t)
174 if not (ifo = res) then
175 ("input does not exactly fill the gaps", Tactic.Tac "")
180 (* fetch errpatIDs from an arbitrary tactic *)
181 fun from_store ctxt tac =
185 Tactic.Rewrite_Set rls_id => rls_id
186 |Tactic.Rewrite_Set_Inst (_, rls_id) => rls_id
188 in case get_rls ctxt rls_id of
189 Rule_Set.Repeat {errpatts, ...} => errpatts
190 | Rule_Set.Sequence {errpatts, ...} => errpatts
191 | Rule_Set.Rrls {errpatts, ...} => errpatts
192 | Rule_Set.Empty => []