1 (* Handle user-input during the specify- and the solve-phase.
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_FILL_PATTERN =
12 type errpatID = Rule_Def.errpatID
13 type errpat = errpatID * term list * thm list
14 val errpats2str : errpat list -> string
16 val find_fillpatterns : Calc.T -> Error_Fill_Def.errpatID ->
17 (Error_Fill_Def.fillpatID * term * thm * Selem.subs option) list
18 val fetchErrorpatterns : Tactic.input -> Error_Fill_Def.errpatID list
19 val is_exactly_equal : Calc.T -> string -> string * Tactic.input
20 val check_for : term * term -> term * (term * term) list ->
21 (Error_Fill_Def.errpatID * term list * 'a list) list * Rule_Set.T ->
22 Error_Fill_Def.errpatID option
24 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
27 val check_err_patt : term * term -> UnparseC.subst -> Error_Fill_Def.errpatID * term -> Rule_Set.T -> Error_Fill_Def.errpatID option
29 'a * (term * term) list -> 'b * term -> Error_Fill_Def.errpatID -> Error_Fill_Def.fillpat -> (Error_Fill_Def.fillpatID * term * 'b * 'a) option
31 'a * (term * term) list -> term -> Error_Fill_Def.errpatID -> thm -> (Error_Fill_Def.fillpatID * term * thm * 'a) list
32 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
36 structure Error_Fill_Pattern(**): ERROR_FILL_PATTERN(**) =
40 type errpatID = Rule_Def.errpatID
43 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
44 fun check_err_patt (res, inf) subst (errpatID, pat) rls =
46 val (res', _, _, rewritten) =
47 Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
51 val norm_res = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls res' of
53 | SOME (norm_res, _) => norm_res
54 val norm_inf = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls inf of
56 | SOME (norm_inf, _) => norm_inf
57 in if norm_res = norm_inf then SOME errpatID else NONE
63 check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
64 (prog, env) for retrieval of casual substitution for bdv in the pattern.
66 fun check_for (res, inf) (prog, env) (errpats, rls) =
68 val (_, subst) = Rtools.get_bdv_subst prog env
69 fun scan (_, [], _) = NONE
70 | scan (errpatID, errpat :: errpats, _) =
71 case check_err_patt (res, inf) subst (errpatID, errpat) rls of
72 NONE => scan (errpatID, errpats, [])
73 | SOME errpatID => SOME errpatID
75 | scans (group :: groups) =
78 | SOME errpatID => SOME errpatID
81 (* fill-in patterns an forms.
82 returns thm required by "fun in_fillform *)
83 fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =
85 val (form', _, _, rewritten) =
86 Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
87 in (*the fillpat of the thm must be dedicated to errpatID*)
88 if errpatID = erpaID andalso rewritten then
89 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
93 fun get_fillpats subst form errpatID thm =
95 val thmDeriv = Thm.get_name_hint thm
96 val (part, thyID) = Rtools.thy_containing_thm thmDeriv
97 val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
98 val fillpats = case Specify.get_the theID of
99 Thy_Html.Hthm {fillpats, ...} => fillpats
100 | _ => error "get_fillpats: uncovered case of get_the"
101 val some = map (get_fillform subst (thm, form) errpatID) fillpats
102 in some |> filter is_some |> map the end
104 fun find_fillpatterns (pt, pos as (p, _): Pos.pos') errpatID =
106 val f_curr = Ctree.get_curr_formula (pt, pos);
107 val pp = Ctree.par_pblobj pt p
108 val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
109 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
110 | _ => error "find_fillpatterns: uncovered case of get_met"
111 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
112 val subst = Rtools.get_bdv_subst prog env
113 val errpatthms = errpats
114 |> filter ((curry op = errpatID) o (#1: Error_Fill_Def.errpat -> Error_Fill_Def.errpatID))
115 |> map (#3: Error_Fill_Def.errpat -> thm list)
117 in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
119 (* check if an input formula is exactly equal to the rewrite from a rule
120 which is stored at the pos where the input is stored of "ok". *)
121 fun is_exactly_equal (pt, pos as (p, _)) istr =
122 case TermC.parseNEW (ThyC.get_theory "Isac_Knowledge" |> ThyC.to_ctxt) istr of
123 NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
126 val p' = Pos.lev_on p;
127 val tac = Ctree.get_obj Ctree.g_tac pt p';
129 case Applicable.applicable_in pos pt tac of
130 Applicable.Notappl msg => (msg, Tactic.Tac "")
131 | Applicable.Appl rew =>
133 val res = case rew of
134 Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
135 |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
136 | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t)
138 if not (ifo = res) then
139 ("input does not exactly fill the gaps", Tactic.Tac "")
144 (* fetch errpatIDs from an arbitrary tactic *)
145 fun fetchErrorpatterns tac =
149 Tactic.Rewrite_Set rlsID => rlsID
150 |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
152 val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID;
153 val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
154 Thy_Html.Hrls {thy_rls = (_, rls), ...} => rls
155 | _ => error "fetchErrorpatterns: uncovered case of get_the"
157 Rule_Def.Repeat {errpatts, ...} => errpatts
158 | Rule_Set.Sequence {errpatts, ...} => errpatts
159 | Rule_Set.Rrls {errpatts, ...} => errpatts
160 | Rule_Set.Empty => []
163 type errpatID = Rule_Def.errpatID
165 errpatID (* one identifier for a list of patterns
166 DESIGN ?TODO: errpatID list for hierarchy of errpats ? *)
167 * term list (* error patterns *)
168 * thm list (* thms related to error patterns; note that respective lhs
169 do not match (which reflects student's error).
170 fillpatterns are stored with these thms. *)
171 fun errpat2str (id, tms, thms) =
172 "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC.string_of_thms thms
173 fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats