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 patterns" 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 : 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
23 val from_store: Tactic.input -> Error_Pattern_Def.id list
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
27 val find_fill_patterns: Calc.T -> id -> record list
30 val check_for': term * term -> subst -> id * term -> Rule_Set.T -> id option
31 val fill_from_store: Subst.input option * Subst.T -> term -> id -> thm ->
33 val fill_form: Subst.input option * Subst.T -> thm * term -> id -> fill_in ->
39 structure Error_Pattern(**): ERROR_PATTERN(**) =
43 type id = Error_Pattern_Def.id;
44 type T = Error_Pattern_Def.T;
45 val s_to_string = Error_Pattern_Def.s_to_string;
46 val empty = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}])
48 type fill_in_id = Error_Pattern_Def.fill_in_id;
49 type fill_in = Error_Pattern_Def.fill_in;
50 val fill_in_empty = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
52 type record = (fill_in_id * term * thm * Subst.input option);
55 check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls
57 fun check_for' (res, inf) subst (id, pat) rls =
59 val ctxt = Proof_Context.init_global ((ThyC.Isac()))
60 val (res', _, _, rewritten) =
61 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord
62 Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
66 val norm_res = case Rewrite.rewrite_set_inst_ ctxt false subst rls res' of
68 | SOME (norm_res, _) => norm_res
69 val norm_inf = case Rewrite.rewrite_set_inst_ ctxt false subst rls inf of
71 | SOME (norm_inf, _) => norm_inf
73 if norm_res = norm_inf then SOME id else NONE
79 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.
82 fun check_for (res, inf) (prog, env) (errpats, rls) =
84 val (_, subst) = Subst.for_bdv prog env
85 fun scan (_, [], _) = NONE
86 | scan (id, T :: errpats, _) =
87 case check_for' (res, inf) subst (id, T) rls of
88 NONE => scan (id, errpats, [])
91 | scans (group :: groups) =
97 (* fill-in patterns an forms.
98 returns thm required by "fun in_fillform *)
99 fun fill_form (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) =
101 val ctxt = Proof_Context.init_global ((ThyC.Isac()))
102 val (form', _, _, rewritten) =
103 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
104 in (*the fillpat of the thm must be dedicated to id*)
105 if id = erpaID andalso rewritten then
106 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
110 fun fill_from_store subst form id thm =
112 val thmDeriv = Thm.get_name_hint thm
113 val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
114 val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
115 val fillpats = case Thy_Read.from_store theID of
116 Thy_Write.Hthm {fillpats, ...} => fillpats
117 | _ => raise ERROR "fill_from_store: uncovered case of get_the"
118 val some = map (fill_form subst (thm, form) id) fillpats
119 in some |> filter is_some |> map the end
121 fun find_fill_patterns (pt, pos as (p, _): Pos.pos') id =
123 val f_curr = Ctree.get_curr_formula (pt, pos);
124 val pp = Ctree.par_pblobj pt p
125 val (errpats, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
126 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
127 | _ => raise ERROR "find_fill_patterns: uncovered case of get_met"
128 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
129 val subst = Subst.for_bdv prog env
130 val errpatthms = errpats
131 |> filter ((curry op = id) o (#1: Error_Pattern_Def.T -> Error_Pattern_Def.id))
132 |> map (#3: Error_Pattern_Def.T -> thm list)
134 in map (fill_from_store subst f_curr id) errpatthms |> flat end
137 Check input on a fill-pattern:
138 check if input is exactly equal to the rewrite from a rule
139 which is stored at the pos where the input is stored of "ok".
141 fun filled_exactly (pt, pos as (p, _)) istr =
142 case TermC.parseNEW (ThyC.get_theory "Isac_Knowledge" |> Proof_Context.init_global) istr of
143 NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
146 val p' = Pos.lev_on p;
147 val tac = Ctree.get_obj Ctree.g_tac pt p';
149 case Solve_Step.check tac (pt, pos) of
150 Applicable.No msg => (msg, Tactic.Tac "")
151 | Applicable.Yes rew =>
153 val res = case rew of
154 Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
155 |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
156 | t => raise ERROR ("filled_exactly: uncovered case for " ^ Tactic.string_of t)
158 if not (ifo = res) then
159 ("input does not exactly fill the gaps", Tactic.Tac "")
164 (* fetch errpatIDs from an arbitrary tactic *)
169 Tactic.Rewrite_Set rlsID => rlsID
170 |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
172 val (part, thyID) = Thy_Read.thy_containing_rls "Isac_Knowledge" rlsID;
173 val rls = case Thy_Read.from_store [part, thyID, "Rulesets", rlsID] of
174 Thy_Write.Hrls {thy_rls = (_, rls), ...} => rls
175 | _ => raise ERROR "from_store: uncovered case of get_the"
177 Rule_Def.Repeat {errpatts, ...} => errpatts
178 | Rule_Set.Sequence {errpatts, ...} => errpatts
179 | Rule_Set.Rrls {errpatts, ...} => errpatts
180 | Rule_Set.Empty => []