neuper@37906
|
1 |
(* Handle user-input during the specify- and the solve-phase.
|
neuper@37906
|
2 |
author: Walther Neuper
|
neuper@37906
|
3 |
0603
|
neuper@37906
|
4 |
(c) due to copyright terms
|
walther@59858
|
5 |
|
walther@59858
|
6 |
TODO: use "Error_Fill_Pattern" for renaming identifiers -- go back to Rule_Def.*
|
neuper@37906
|
7 |
*)
|
neuper@37906
|
8 |
|
walther@59858
|
9 |
signature ERROR_FILL_PATTERN =
|
wneuper@59262
|
10 |
sig
|
walther@59858
|
11 |
type errpatID = Rule_Def.errpatID
|
walther@59858
|
12 |
type errpat = errpatID * term list * thm list
|
walther@59858
|
13 |
val errpats2str : errpat list -> string
|
walther@59858
|
14 |
|
walther@59858
|
15 |
val find_fillpatterns : Calc.T -> Error_Fill_Def.errpatID -> (Error_Fill_Def.fillpatID * term * thm * Selem.subs option) list
|
walther@59775
|
16 |
val is_exactly_equal : Calc.T -> string -> string * Tactic.input
|
wneuper@59555
|
17 |
val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
|
walther@59851
|
18 |
Rule_Set.T -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
|
walther@59857
|
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))
|
walther@59858
|
20 |
val fetchErrorpatterns : Tactic.input -> Error_Fill_Def.errpatID list
|
walther@59844
|
21 |
val check_for :
|
wneuper@59556
|
22 |
term * term ->
|
walther@59858
|
23 |
term * (term * term) list -> (Error_Fill_Def.errpatID * term list * 'a list) list * Rule_Set.T -> Error_Fill_Def.errpatID option
|
walther@59874
|
24 |
val rule2thm'' : Rule.rule -> ThmC.T
|
walther@59822
|
25 |
val rule2rls' : Rule.rule -> string
|
wneuper@59310
|
26 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
wneuper@59310
|
27 |
(* NONE *)
|
walther@59785
|
28 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
wneuper@59262
|
29 |
val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
|
wneuper@59416
|
30 |
val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
|
walther@59863
|
31 |
val check_err_patt : term * term -> UnparseC.subst -> Error_Fill_Def.errpatID * term -> Rule_Set.T -> Error_Fill_Def.errpatID option
|
wneuper@59262
|
32 |
val get_fillform :
|
walther@59858
|
33 |
'a * (term * term) list -> 'b * term -> Error_Fill_Def.errpatID -> Error_Fill_Def.fillpat -> (Error_Fill_Def.fillpatID * term * 'b * 'a) option
|
wneuper@59262
|
34 |
val get_fillpats :
|
walther@59858
|
35 |
'a * (term * term) list -> term -> Error_Fill_Def.errpatID -> thm -> (Error_Fill_Def.fillpatID * term * thm * 'a) list
|
walther@59785
|
36 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59310
|
37 |
|
wneuper@59262
|
38 |
end
|
walther@59822
|
39 |
(**)
|
walther@59858
|
40 |
structure Error_Fill_Pattern(**): ERROR_FILL_PATTERN(**) =
|
walther@59822
|
41 |
struct
|
walther@59822
|
42 |
(**)
|
neuper@37906
|
43 |
|
walther@59858
|
44 |
type errpatID = Rule_Def.errpatID
|
walther@59858
|
45 |
|
walther@59822
|
46 |
fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
|
walther@59867
|
47 |
| rule2thm'' r = error ("rule2thm': not defined for " ^ Rule.to_string r);
|
walther@59867
|
48 |
fun rule2rls' (Rule.Rls_ rls) = Rule_Set.id rls
|
walther@59867
|
49 |
| rule2rls' r = error ("rule2rls': not defined for " ^ Rule.to_string r);
|
neuper@37906
|
50 |
|
neuper@37906
|
51 |
(*the lists contain eq-al elem-pairs at the beginning;
|
neuper@37906
|
52 |
return first list reverted (again) - ie. in order as required subsequently*)
|
neuper@37906
|
53 |
fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
|
walther@59848
|
54 |
if equal f1 i1 then
|
wneuper@59264
|
55 |
if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)
|
wneuper@59264
|
56 |
else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)
|
neuper@38031
|
57 |
else error "dropwhile': did not start with equal elements"
|
neuper@37906
|
58 |
| dropwhile' equal (f::fs) [i] =
|
walther@59848
|
59 |
if equal f i then
|
walther@59848
|
60 |
(rev (f::fs), [i])
|
neuper@38031
|
61 |
else error "dropwhile': did not start with equal elements"
|
neuper@37906
|
62 |
| dropwhile' equal [f] (i::is) =
|
walther@59848
|
63 |
if equal f i then
|
walther@59848
|
64 |
([f], i::is)
|
wneuper@59264
|
65 |
else error "dropwhile': did not start with equal elements"
|
wneuper@59264
|
66 |
| dropwhile' _ _ _ = error "dropwhile': uncovered case"
|
neuper@37906
|
67 |
|
wneuper@59264
|
68 |
(* 040214: version for concat_deriv *)
|
walther@59876
|
69 |
fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
|
neuper@37906
|
70 |
|
wneuper@59416
|
71 |
fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
|
wneuper@59571
|
72 |
(Tactic.Rewrite (id, thm),
|
walther@59822
|
73 |
Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, rule2thm'' r, t, (t', a)),
|
walther@59846
|
74 |
(Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
|
wneuper@59416
|
75 |
| mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) =
|
walther@59822
|
76 |
(Tactic.Rewrite_Set (rule2rls' r),
|
wneuper@59592
|
77 |
Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
|
walther@59846
|
78 |
(Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
|
walther@59868
|
79 |
| mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
|
neuper@37906
|
80 |
|
wneuper@59264
|
81 |
(* fo = ifo excluded already in inform *)
|
neuper@37906
|
82 |
fun concat_deriv rew_ord erls rules fo ifo =
|
neuper@55487
|
83 |
let
|
walther@59861
|
84 |
fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
|
neuper@55487
|
85 |
| derivat dt = (#1 o #3 o last_elem) dt
|
neuper@55487
|
86 |
fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
|
walther@59854
|
87 |
val fod = Rtools.make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE fo
|
walther@59854
|
88 |
val ifod = Rtools.make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
|
neuper@55487
|
89 |
in
|
neuper@55487
|
90 |
case (fod, ifod) of
|
neuper@55487
|
91 |
([], []) => if fo = ifo then (true, []) else (false, [])
|
neuper@55487
|
92 |
| (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
|
neuper@55487
|
93 |
| ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
|
neuper@55487
|
94 |
| (fod, ifod) =>
|
walther@59848
|
95 |
if derivat fod = derivat ifod (*common normal form found*) then
|
neuper@55487
|
96 |
let
|
neuper@55487
|
97 |
val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
|
neuper@55487
|
98 |
in (true, fod' @ (map rev_deriv' rifod')) end
|
neuper@55487
|
99 |
else (false, [])
|
wneuper@59264
|
100 |
end
|
neuper@37906
|
101 |
|
walther@59822
|
102 |
(*** handle an error pattern ***)
|
walther@59822
|
103 |
|
neuper@42428
|
104 |
(* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
|
wneuper@59405
|
105 |
fun check_err_patt (res, inf) subst (errpatID, pat) rls =
|
neuper@42423
|
106 |
let
|
neuper@42423
|
107 |
val (res', _, _, rewritten) =
|
walther@59857
|
108 |
Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
|
neuper@42423
|
109 |
in
|
walther@59848
|
110 |
if rewritten then
|
neuper@42423
|
111 |
let
|
walther@59854
|
112 |
val norm_res = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls res' of
|
neuper@42423
|
113 |
NONE => res'
|
neuper@42423
|
114 |
| SOME (norm_res, _) => norm_res
|
walther@59854
|
115 |
val norm_inf = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls inf of
|
neuper@42423
|
116 |
NONE => inf
|
neuper@42423
|
117 |
| SOME (norm_inf, _) => norm_inf
|
neuper@42423
|
118 |
in if norm_res = norm_inf then SOME errpatID else NONE
|
neuper@42423
|
119 |
end
|
neuper@42423
|
120 |
else NONE
|
neuper@42423
|
121 |
end;
|
neuper@42423
|
122 |
|
neuper@42428
|
123 |
(* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
|
neuper@42428
|
124 |
(prog, env) for retrieval of casual substitution for bdv in the pattern. *)
|
walther@59844
|
125 |
fun check_for (res, inf) (prog, env) (errpats, rls) =
|
neuper@42428
|
126 |
let
|
wneuper@59263
|
127 |
val (_, subst) = Rtools.get_bdv_subst prog env
|
neuper@42428
|
128 |
fun scan (_, [], _) = NONE
|
neuper@42428
|
129 |
| scan (errpatID, errpat :: errpats, _) =
|
wneuper@59405
|
130 |
case check_err_patt (res, inf) subst (errpatID, errpat) rls of
|
neuper@42428
|
131 |
NONE => scan (errpatID, errpats, [])
|
neuper@42428
|
132 |
| SOME errpatID => SOME errpatID
|
neuper@42428
|
133 |
fun scans [] = NONE
|
neuper@42428
|
134 |
| scans (group :: groups) =
|
neuper@42428
|
135 |
case scan group of
|
neuper@42428
|
136 |
NONE => scans groups
|
neuper@42428
|
137 |
| SOME errpatID => SOME errpatID
|
neuper@42428
|
138 |
in scans errpats end;
|
neuper@42428
|
139 |
|
neuper@42433
|
140 |
(* fill-in patterns an forms.
|
neuper@42433
|
141 |
returns thm required by "fun in_fillform *)
|
wneuper@59405
|
142 |
fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =
|
neuper@42430
|
143 |
let
|
neuper@42430
|
144 |
val (form', _, _, rewritten) =
|
walther@59857
|
145 |
Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
|
neuper@42430
|
146 |
in (*the fillpat of the thm must be dedicated to errpatID*)
|
walther@59848
|
147 |
if errpatID = erpaID andalso rewritten then
|
walther@59848
|
148 |
SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
|
wneuper@59264
|
149 |
else NONE
|
wneuper@59264
|
150 |
end
|
neuper@42430
|
151 |
|
neuper@42430
|
152 |
fun get_fillpats subst form errpatID thm =
|
wneuper@59264
|
153 |
let
|
wneuper@59264
|
154 |
val thmDeriv = Thm.get_name_hint thm
|
wneuper@59264
|
155 |
val (part, thyID) = Rtools.thy_containing_thm thmDeriv
|
walther@59876
|
156 |
val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
|
wneuper@59269
|
157 |
val fillpats = case Specify.get_the theID of
|
wneuper@59405
|
158 |
Celem.Hthm {fillpats, ...} => fillpats
|
wneuper@59264
|
159 |
| _ => error "get_fillpats: uncovered case of get_the"
|
wneuper@59264
|
160 |
val some = map (get_fillform subst (thm, form) errpatID) fillpats
|
wneuper@59264
|
161 |
in some |> filter is_some |> map the end
|
neuper@42430
|
162 |
|
walther@59846
|
163 |
fun find_fillpatterns (pt, pos as (p, _): Pos.pos') errpatID =
|
neuper@42430
|
164 |
let
|
wneuper@59276
|
165 |
val f_curr = Ctree.get_curr_formula (pt, pos);
|
wneuper@59276
|
166 |
val pp = Ctree.par_pblobj pt p
|
wneuper@59276
|
167 |
val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
|
wneuper@59416
|
168 |
{errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
|
wneuper@59264
|
169 |
| _ => error "find_fillpatterns: uncovered case of get_met"
|
walther@59807
|
170 |
val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
|
wneuper@59263
|
171 |
val subst = Rtools.get_bdv_subst prog env
|
neuper@42430
|
172 |
val errpatthms = errpats
|
walther@59858
|
173 |
|> filter ((curry op = errpatID) o (#1: Error_Fill_Def.errpat -> Error_Fill_Def.errpatID))
|
walther@59858
|
174 |
|> map (#3: Error_Fill_Def.errpat -> thm list)
|
neuper@42430
|
175 |
|> flat
|
wneuper@59264
|
176 |
in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
|
neuper@37906
|
177 |
|
neuper@42437
|
178 |
(* check if an input formula is exactly equal the rewrite from a rule
|
neuper@42437
|
179 |
which is stored at the pos where the input is stored of "ok". *)
|
neuper@42437
|
180 |
fun is_exactly_equal (pt, pos as (p, _)) istr =
|
walther@59854
|
181 |
case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> ThyC.thy2ctxt) istr of
|
wneuper@59571
|
182 |
NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
|
neuper@42437
|
183 |
| SOME ifo =>
|
neuper@42437
|
184 |
let
|
walther@59757
|
185 |
val p' = Pos.lev_on p;
|
wneuper@59276
|
186 |
val tac = Ctree.get_obj Ctree.g_tac pt p';
|
neuper@42437
|
187 |
in
|
wneuper@59272
|
188 |
case Applicable.applicable_in pos pt tac of
|
walther@59735
|
189 |
Applicable.Notappl msg => (msg, Tactic.Tac "")
|
walther@59735
|
190 |
| Applicable.Appl rew =>
|
neuper@42437
|
191 |
let
|
neuper@42437
|
192 |
val res = case rew of
|
wneuper@59571
|
193 |
Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
|
wneuper@59571
|
194 |
|Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
|
walther@59728
|
195 |
| t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t)
|
neuper@42437
|
196 |
in
|
walther@59848
|
197 |
if not (ifo = res) then
|
walther@59848
|
198 |
("input does not exactly fill the gaps", Tactic.Tac "")
|
neuper@42437
|
199 |
else ("ok", tac)
|
neuper@42437
|
200 |
end
|
neuper@42437
|
201 |
end
|
neuper@42437
|
202 |
|
neuper@42458
|
203 |
(* fetch errpatIDs from an arbitrary tactic *)
|
neuper@42458
|
204 |
fun fetchErrorpatterns tac =
|
neuper@42458
|
205 |
let
|
neuper@42458
|
206 |
val rlsID =
|
neuper@42458
|
207 |
case tac of
|
wneuper@59571
|
208 |
Tactic.Rewrite_Set rlsID => rlsID
|
wneuper@59571
|
209 |
|Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
|
walther@59852
|
210 |
| _ => "empty"
|
wneuper@59592
|
211 |
val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID;
|
wneuper@59269
|
212 |
val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
|
wneuper@59405
|
213 |
Celem.Hrls {thy_rls = (_, rls), ...} => rls
|
wneuper@59264
|
214 |
| _ => error "fetchErrorpatterns: uncovered case of get_the"
|
neuper@42458
|
215 |
in case rls of
|
walther@59851
|
216 |
Rule_Def.Repeat {errpatts, ...} => errpatts
|
walther@59878
|
217 |
| Rule_Set.Sequence {errpatts, ...} => errpatts
|
walther@59850
|
218 |
| Rule_Set.Rrls {errpatts, ...} => errpatts
|
walther@59851
|
219 |
| Rule_Set.Empty => []
|
neuper@42458
|
220 |
end
|
wneuper@59264
|
221 |
|
walther@59858
|
222 |
type errpatID = Rule_Def.errpatID
|
walther@59858
|
223 |
type errpat =
|
walther@59858
|
224 |
errpatID (* one identifier for a list of patterns
|
walther@59858
|
225 |
DESIGN ?TODO: errpatID list for hierarchy of errpats ? *)
|
walther@59858
|
226 |
* term list (* error patterns *)
|
walther@59858
|
227 |
* thm list (* thms related to error patterns; note that respective lhs
|
walther@59858
|
228 |
do not match (which reflects student's error).
|
walther@59858
|
229 |
fillpatterns are stored with these thms. *)
|
walther@59858
|
230 |
fun errpat2str (id, tms, thms) =
|
walther@59875
|
231 |
"(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC.string_of_thms thms
|
walther@59858
|
232 |
fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
|
walther@59858
|
233 |
|
walther@59858
|
234 |
(**)end(**) |