1 (* Handle user-input during the specify- and the solve-phase.
4 (c) due to copyright terms
6 TODO: use "Error_Fill_Pattern" for renaming identifiers -- go back to Rule_Def.*
9 signature ERROR_FILL_PATTERN =
11 type errpatID = Rule_Def.errpatID
12 type errpat = errpatID * term list * thm list
13 val errpats2str : errpat list -> string
15 val find_fillpatterns : Calc.T -> Error_Fill_Def.errpatID -> (Error_Fill_Def.fillpatID * term * thm * Selem.subs option) list
16 val is_exactly_equal : Calc.T -> string -> string * Tactic.input
17 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
18 Rule_Set.T -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
19 val mk_tacis: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))
20 val fetchErrorpatterns : Tactic.input -> Error_Fill_Def.errpatID list
23 term * (term * term) list -> (Error_Fill_Def.errpatID * term list * 'a list) list * Rule_Set.T -> Error_Fill_Def.errpatID option
24 val rule2thm'' : Rule.rule -> ThmC_Def.thm''
25 val rule2rls' : Rule.rule -> string
26 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
28 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
29 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
30 val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
31 val check_err_patt : term * term -> UnparseC.subst -> Error_Fill_Def.errpatID * term -> Rule_Set.T -> Error_Fill_Def.errpatID option
33 'a * (term * term) list -> 'b * term -> Error_Fill_Def.errpatID -> Error_Fill_Def.fillpat -> (Error_Fill_Def.fillpatID * term * 'b * 'a) option
35 'a * (term * term) list -> term -> Error_Fill_Def.errpatID -> thm -> (Error_Fill_Def.fillpatID * term * thm * 'a) list
36 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
40 structure Error_Fill_Pattern(**): ERROR_FILL_PATTERN(**) =
44 type errpatID = Rule_Def.errpatID
46 fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
47 | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule.rule2str r);
48 fun rule2rls' (Rule.Rls_ rls) = Rule_Set.rls2str rls
49 | rule2rls' r = error ("rule2rls': not defined for " ^ Rule.rule2str r);
51 (*the lists contain eq-al elem-pairs at the beginning;
52 return first list reverted (again) - ie. in order as required subsequently*)
53 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
55 if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)
56 else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)
57 else error "dropwhile': did not start with equal elements"
58 | dropwhile' equal (f::fs) [i] =
61 else error "dropwhile': did not start with equal elements"
62 | dropwhile' equal [f] (i::is) =
65 else error "dropwhile': did not start with equal elements"
66 | dropwhile' _ _ _ = error "dropwhile': uncovered case"
68 (* 040214: version for concat_deriv *)
69 fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));
71 fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
72 (Tactic.Rewrite (id, thm),
73 Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, rule2thm'' r, t, (t', a)),
74 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
75 | mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) =
76 (Tactic.Rewrite_Set (rule2rls' r),
77 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
78 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
79 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.rule2str r ^ " at " ^ UnparseC.term2str t)
81 (* fo = ifo excluded already in inform *)
82 fun concat_deriv rew_ord erls rules fo ifo =
84 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
85 | derivat dt = (#1 o #3 o last_elem) dt
86 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
87 val fod = Rtools.make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE fo
88 val ifod = Rtools.make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
91 ([], []) => if fo = ifo then (true, []) else (false, [])
92 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
93 | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
95 if derivat fod = derivat ifod (*common normal form found*) then
97 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
98 in (true, fod' @ (map rev_deriv' rifod')) end
102 (*** handle an error pattern ***)
104 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
105 fun check_err_patt (res, inf) subst (errpatID, pat) rls =
107 val (res', _, _, rewritten) =
108 Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
112 val norm_res = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls res' of
114 | SOME (norm_res, _) => norm_res
115 val norm_inf = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls inf of
117 | SOME (norm_inf, _) => norm_inf
118 in if norm_res = norm_inf then SOME errpatID else NONE
123 (* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
124 (prog, env) for retrieval of casual substitution for bdv in the pattern. *)
125 fun check_for (res, inf) (prog, env) (errpats, rls) =
127 val (_, subst) = Rtools.get_bdv_subst prog env
128 fun scan (_, [], _) = NONE
129 | scan (errpatID, errpat :: errpats, _) =
130 case check_err_patt (res, inf) subst (errpatID, errpat) rls of
131 NONE => scan (errpatID, errpats, [])
132 | SOME errpatID => SOME errpatID
134 | scans (group :: groups) =
137 | SOME errpatID => SOME errpatID
138 in scans errpats end;
140 (* fill-in patterns an forms.
141 returns thm required by "fun in_fillform *)
142 fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =
144 val (form', _, _, rewritten) =
145 Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
146 in (*the fillpat of the thm must be dedicated to errpatID*)
147 if errpatID = erpaID andalso rewritten then
148 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
152 fun get_fillpats subst form errpatID thm =
154 val thmDeriv = Thm.get_name_hint thm
155 val (part, thyID) = Rtools.thy_containing_thm thmDeriv
156 val theID = [part, thyID, "Theorems", ThmC_Def.thmID_of_derivation_name thmDeriv]
157 val fillpats = case Specify.get_the theID of
158 Celem.Hthm {fillpats, ...} => fillpats
159 | _ => error "get_fillpats: uncovered case of get_the"
160 val some = map (get_fillform subst (thm, form) errpatID) fillpats
161 in some |> filter is_some |> map the end
163 fun find_fillpatterns (pt, pos as (p, _): Pos.pos') errpatID =
165 val f_curr = Ctree.get_curr_formula (pt, pos);
166 val pp = Ctree.par_pblobj pt p
167 val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
168 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
169 | _ => error "find_fillpatterns: uncovered case of get_met"
170 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
171 val subst = Rtools.get_bdv_subst prog env
172 val errpatthms = errpats
173 |> filter ((curry op = errpatID) o (#1: Error_Fill_Def.errpat -> Error_Fill_Def.errpatID))
174 |> map (#3: Error_Fill_Def.errpat -> thm list)
176 in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
178 (* check if an input formula is exactly equal the rewrite from a rule
179 which is stored at the pos where the input is stored of "ok". *)
180 fun is_exactly_equal (pt, pos as (p, _)) istr =
181 case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> ThyC.thy2ctxt) istr of
182 NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
185 val p' = Pos.lev_on p;
186 val tac = Ctree.get_obj Ctree.g_tac pt p';
188 case Applicable.applicable_in pos pt tac of
189 Applicable.Notappl msg => (msg, Tactic.Tac "")
190 | Applicable.Appl rew =>
192 val res = case rew of
193 Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
194 |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
195 | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t)
197 if not (ifo = res) then
198 ("input does not exactly fill the gaps", Tactic.Tac "")
203 (* fetch errpatIDs from an arbitrary tactic *)
204 fun fetchErrorpatterns tac =
208 Tactic.Rewrite_Set rlsID => rlsID
209 |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
211 val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID;
212 val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
213 Celem.Hrls {thy_rls = (_, rls), ...} => rls
214 | _ => error "fetchErrorpatterns: uncovered case of get_the"
216 Rule_Def.Repeat {errpatts, ...} => errpatts
217 | Rule_Set.Seqence {errpatts, ...} => errpatts
218 | Rule_Set.Rrls {errpatts, ...} => errpatts
219 | Rule_Set.Empty => []
222 type errpatID = Rule_Def.errpatID
224 errpatID (* one identifier for a list of patterns
225 DESIGN ?TODO: errpatID list for hierarchy of errpats ? *)
226 * term list (* error patterns *)
227 * thm list (* thms related to error patterns; note that respective lhs
228 do not match (which reflects student's error).
229 fillpatterns are stored with these thms. *)
230 fun errpat2str (id, tms, thms) =
231 "(\"" ^ id ^ "\",\n" ^ UnparseC.terms2str tms ^ ",\n" ^ ThmC_Def.thms2str thms
232 fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats