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
|
neuper@37906
|
5 |
*)
|
neuper@37906
|
6 |
|
wneuper@59262
|
7 |
signature INPUT_FORMULAS =
|
wneuper@59262
|
8 |
sig
|
wneuper@59416
|
9 |
datatype iitem = Find of Rule.cterm' list | Given of Rule.cterm' list | Relate of Rule.cterm' list
|
wneuper@59262
|
10 |
type imodel = iitem list
|
wneuper@59416
|
11 |
type icalhd = Ctree.pos' * Rule.cterm' * imodel * Ctree.pos_ * Celem.spec
|
wneuper@59571
|
12 |
val fetchErrorpatterns : Tactic.input -> Rule.errpatID list
|
wneuper@59279
|
13 |
val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
|
walther@59775
|
14 |
val find_fillpatterns : Calc.T -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list
|
walther@59775
|
15 |
val is_exactly_equal : Calc.T -> string -> string * Tactic.input
|
walther@59791
|
16 |
(*cp here from "! aktivate for Test_Isac" below due to LI*)
|
wneuper@59555
|
17 |
val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
|
wneuper@59555
|
18 |
Rule.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
|
wneuper@59572
|
19 |
val mk_tacis: Rule.rew_ord' * 'a -> Rule.rls -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))
|
wneuper@59556
|
20 |
val check_error_patterns :
|
wneuper@59556
|
21 |
term * term ->
|
wneuper@59556
|
22 |
term * (term * term) list -> (Rule.errpatID * term list * 'a list) list * Rule.rls -> Rule.errpatID option
|
wneuper@59556
|
23 |
val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
|
wneuper@59555
|
24 |
|
wneuper@59310
|
25 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
wneuper@59310
|
26 |
(* NONE *)
|
walther@59785
|
27 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
wneuper@59262
|
28 |
val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
|
wneuper@59416
|
29 |
val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
|
wneuper@59416
|
30 |
val check_err_patt : term * term -> Rule.subst -> Rule.errpatID * term -> Rule.rls -> Rule.errpatID option
|
wneuper@59262
|
31 |
val get_fillform :
|
wneuper@59416
|
32 |
'a * (term * term) list -> 'b * term -> Rule.errpatID -> Celem.fillpat -> (Celem.fillpatID * term * 'b * 'a) option
|
wneuper@59262
|
33 |
val get_fillpats :
|
wneuper@59416
|
34 |
'a * (term * term) list -> term -> Rule.errpatID -> thm -> (Celem.fillpatID * term * thm * 'a) list
|
walther@59785
|
35 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59310
|
36 |
|
wneuper@59310
|
37 |
(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
|
wneuper@59313
|
38 |
val e_icalhd : icalhd
|
wneuper@59313
|
39 |
val oris2itms : 'a -> ''b list -> ('c * ''b * 'd * term * term list) list ->
|
wneuper@59316
|
40 |
('c * ''b * bool * 'd * Model.itm_) list
|
wneuper@59262
|
41 |
end
|
neuper@37906
|
42 |
|
wneuper@59557
|
43 |
structure Inform(**): INPUT_FORMULAS(**) =
|
wneuper@59262
|
44 |
struct
|
neuper@37906
|
45 |
|
wneuper@59262
|
46 |
(*** handle an input calc-head ***)
|
neuper@37906
|
47 |
|
neuper@37906
|
48 |
datatype iitem =
|
wneuper@59416
|
49 |
Given of Rule.cterm' list
|
neuper@37906
|
50 |
(*Where is never input*)
|
wneuper@59416
|
51 |
| Find of Rule.cterm' list
|
wneuper@59416
|
52 |
| Relate of Rule.cterm' list
|
neuper@37906
|
53 |
|
wneuper@59262
|
54 |
type imodel = iitem list
|
neuper@37906
|
55 |
|
neuper@37906
|
56 |
(*calc-head as input*)
|
neuper@37906
|
57 |
type icalhd =
|
wneuper@59276
|
58 |
Ctree.pos' * (*the position of the calc-head in the calc-tree*)
|
wneuper@59416
|
59 |
Rule.cterm' * (*the headline*)
|
wneuper@59405
|
60 |
imodel * (*the model (without Find) of the calc-head*)
|
wneuper@59276
|
61 |
Ctree.pos_ * (*model belongs to Pbl or Met*)
|
wneuper@59405
|
62 |
Celem.spec; (*specification: domID, pblID, metID*)
|
walther@59694
|
63 |
val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Celem.e_spec)
|
neuper@37906
|
64 |
|
wneuper@59416
|
65 |
fun is_casinput (hdf : Rule.cterm') ((fmz_, spec) : Selem.fmz) =
|
wneuper@59405
|
66 |
hdf <> "" andalso fmz_ = [] andalso spec = Celem.e_spec
|
neuper@37906
|
67 |
|
neuper@37906
|
68 |
(*.handle an input as into an algebra system.*)
|
neuper@37906
|
69 |
fun dtss2itm_ ppc (d, ts) =
|
wneuper@59264
|
70 |
let
|
wneuper@59264
|
71 |
val (f, (d, id)) = the (find_first ((curry op= d) o
|
wneuper@59264
|
72 |
(#1: (term * term) -> term) o
|
wneuper@59405
|
73 |
(#2: Celem.pbt_ -> (term * term))) ppc)
|
wneuper@59264
|
74 |
in
|
wneuper@59316
|
75 |
([1], true, f, Model.Cor ((d, ts), (id, ts)))
|
wneuper@59264
|
76 |
end
|
neuper@37906
|
77 |
|
wneuper@59262
|
78 |
fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
|
neuper@37906
|
79 |
|
wneuper@59405
|
80 |
fun cas_input_ ((dI, pI, mI): Celem.spec) dtss = (*WN110515 reconsider thy..ctxt*)
|
neuper@41995
|
81 |
let
|
wneuper@59405
|
82 |
val thy = Celem.assoc_thy dI
|
wneuper@59269
|
83 |
val {ppc, ...} = Specify.get_pbt pI
|
neuper@41995
|
84 |
val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
|
wneuper@59269
|
85 |
val its = Specify.add_id its_
|
neuper@41995
|
86 |
val pits = map flattup2 its
|
neuper@41995
|
87 |
val (pI, mI) =
|
neuper@41995
|
88 |
if mI <> ["no_met"]
|
neuper@41995
|
89 |
then (pI, mI)
|
neuper@41995
|
90 |
else
|
wneuper@59269
|
91 |
case Specify.refine_pbl thy pI pits of
|
wneuper@59269
|
92 |
SOME (pI,_) => (pI, (hd o #met o Specify.get_pbt) pI)
|
wneuper@59269
|
93 |
| NONE => (pI, (hd o #met o Specify.get_pbt) pI)
|
wneuper@59269
|
94 |
val {ppc, pre, prls, ...} = Specify.get_met mI
|
neuper@41995
|
95 |
val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
|
wneuper@59269
|
96 |
val its = Specify.add_id its_
|
neuper@41995
|
97 |
val mits = map flattup2 its
|
wneuper@59308
|
98 |
val pre = Stool.check_preconds thy prls pre mits
|
walther@59722
|
99 |
val ctxt = Proof_Context.init_global thy
|
wneuper@59308
|
100 |
in (pI, pits, mI, mits, pre, ctxt) end;
|
neuper@37906
|
101 |
|
neuper@37906
|
102 |
|
wneuper@59279
|
103 |
(* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
|
neuper@37906
|
104 |
fun cas_input hdt =
|
wneuper@59262
|
105 |
let
|
wneuper@59262
|
106 |
val (h, argl) = strip_comb hdt
|
neuper@41995
|
107 |
in
|
wneuper@59592
|
108 |
case assoc_cas (Celem.assoc_thy "Isac_Knowledge") h of
|
wneuper@59262
|
109 |
NONE => NONE
|
wneuper@59262
|
110 |
| SOME (spec as (dI,_,_), argl2dtss) =>
|
neuper@41995
|
111 |
let
|
neuper@41995
|
112 |
val dtss = argl2dtss argl
|
neuper@41995
|
113 |
val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
|
neuper@41995
|
114 |
val spec = (dI, pI, mI)
|
neuper@41995
|
115 |
val (pt,_) =
|
wneuper@59581
|
116 |
Ctree.cappend_problem Ctree.e_ctree [] (Istate.e_istate, ContextC.e_ctxt) ([], Celem.e_spec) ([], Celem.e_spec, hdt)
|
wneuper@59276
|
117 |
val pt = Ctree.update_spec pt [] spec
|
wneuper@59276
|
118 |
val pt = Ctree.update_pbl pt [] pits
|
wneuper@59276
|
119 |
val pt = Ctree.update_met pt [] mits
|
wneuper@59276
|
120 |
val pt = Ctree.update_ctxt pt [] ctxt
|
wneuper@59262
|
121 |
in
|
walther@59694
|
122 |
SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Ctree.ocalhd)
|
wneuper@59262
|
123 |
end
|
wneuper@59262
|
124 |
end
|
neuper@37906
|
125 |
|
wneuper@59592
|
126 |
(*lazy evaluation for (Thy_Info_get_theory "Isac_Knowledge")*)
|
wneuper@59592
|
127 |
fun Isac _ = Celem.assoc_thy "Isac_Knowledge";
|
neuper@37906
|
128 |
|
wneuper@59262
|
129 |
(* re-parse itms with a new thy and prepare for checking with ori list *)
|
wneuper@59316
|
130 |
fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) =
|
wneuper@59316
|
131 |
(let val t = Model.comp_dts (d, ts)
|
wneuper@59416
|
132 |
val _ = (Rule.term_to_string''' dI t)
|
wneuper@59262
|
133 |
(*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
|
neuper@52070
|
134 |
in itm end
|
wneuper@59416
|
135 |
handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*))))
|
wneuper@59316
|
136 |
| parsitm dI (i, v, b, f, Model.Syn str) =
|
wneuper@59389
|
137 |
(let val _ = (Thm.term_of o the o (TermC.parse dI)) str
|
wneuper@59316
|
138 |
in (i, v, b ,f, Model.Par str) end
|
wneuper@59316
|
139 |
handle _ => (i, v, b, f, Model.Syn str))
|
wneuper@59316
|
140 |
| parsitm dI (i, v, b, f, Model.Typ str) =
|
wneuper@59389
|
141 |
(let val _ = (Thm.term_of o the o (TermC.parse dI)) str
|
wneuper@59316
|
142 |
in (i, v, b, f, Model.Par str) end
|
wneuper@59316
|
143 |
handle _ => (i, v, b, f, Model.Syn str))
|
wneuper@59316
|
144 |
| parsitm dI (itm as (i, v, _, f, Model.Inc ((d, ts), _))) =
|
wneuper@59316
|
145 |
(let val t = Model.comp_dts (d,ts);
|
wneuper@59416
|
146 |
val _ = Rule.term_to_string''' dI t;
|
neuper@37906
|
147 |
(*this ^ should raise the exn on unability of re-parsing dts*)
|
neuper@52070
|
148 |
in itm end
|
wneuper@59416
|
149 |
handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*))))
|
wneuper@59316
|
150 |
| parsitm dI (itm as (i, v, _, f, Model.Sup (d, ts))) =
|
wneuper@59316
|
151 |
(let val t = Model.comp_dts (d,ts);
|
wneuper@59416
|
152 |
val _ = Rule.term_to_string''' dI t;
|
neuper@37906
|
153 |
(*this ^ should raise the exn on unability of re-parsing dts*)
|
neuper@52070
|
154 |
in itm end
|
wneuper@59416
|
155 |
handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*))))
|
wneuper@59316
|
156 |
| parsitm dI (itm as (i, v, _, f, Model.Mis (d, t'))) =
|
neuper@37906
|
157 |
(let val t = d $ t';
|
wneuper@59416
|
158 |
val _ = Rule.term_to_string''' dI t;
|
neuper@37906
|
159 |
(*this ^ should raise the exn on unability of re-parsing dts*)
|
neuper@52070
|
160 |
in itm end
|
wneuper@59416
|
161 |
handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*))))
|
wneuper@59316
|
162 |
| parsitm dI (itm as (_, _, _, _, Model.Par _)) =
|
wneuper@59416
|
163 |
error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt dI) itm ^ "): Par should be internal");
|
neuper@37906
|
164 |
|
neuper@37906
|
165 |
(*separate a list to a pair of elements that do NOT satisfy the predicate,
|
neuper@37906
|
166 |
and of elements that satisfy the predicate, i.e. (false, true)*)
|
neuper@37906
|
167 |
fun filter_sep pred xs =
|
wneuper@59262
|
168 |
let
|
wneuper@59262
|
169 |
fun filt ab [] = ab
|
wneuper@59262
|
170 |
| filt (a, b) (x :: xs) =
|
wneuper@59262
|
171 |
if pred x
|
wneuper@59262
|
172 |
then filt (a, b @ [x]) xs
|
wneuper@59262
|
173 |
else filt (a @ [x], b) xs
|
wneuper@59262
|
174 |
in filt ([], []) xs end;
|
wneuper@59316
|
175 |
fun is_Par (_, _, _, _, Model.Par _) = true
|
neuper@37906
|
176 |
| is_Par _ = false;
|
neuper@37906
|
177 |
|
neuper@37906
|
178 |
fun is_e_ts [] = true
|
neuper@37906
|
179 |
| is_e_ts [Const ("List.list.Nil", _)] = true
|
neuper@37906
|
180 |
| is_e_ts _ = false;
|
neuper@37906
|
181 |
|
wneuper@59262
|
182 |
(* WN.9.11.03 copied from fun appl_add *)
|
neuper@37906
|
183 |
fun appl_add' dI oris ppc pbt (sel, ct) =
|
wneuper@59262
|
184 |
let
|
wneuper@59416
|
185 |
val ctxt = Celem.assoc_thy dI |> Rule.thy2ctxt;
|
wneuper@59262
|
186 |
in
|
wneuper@59389
|
187 |
case TermC.parseNEW ctxt ct of
|
wneuper@59316
|
188 |
NONE => (0, [], false, sel, Model.Syn ct)
|
wneuper@59262
|
189 |
| SOME t =>
|
wneuper@59265
|
190 |
(case Chead.is_known ctxt sel oris t of
|
wneuper@59262
|
191 |
("", ori', all) =>
|
wneuper@59265
|
192 |
(case Chead.is_notyet_input ctxt ppc all ori' pbt of
|
wneuper@59262
|
193 |
("",itm) => itm
|
wneuper@59262
|
194 |
| (msg,_) => error ("appl_add': " ^ msg))
|
wneuper@59262
|
195 |
| (_, (i, v, _, d, ts), _) =>
|
wneuper@59262
|
196 |
if is_e_ts ts
|
wneuper@59416
|
197 |
then (i, v, false, sel, Model.Inc ((d, ts), (Rule.e_term, [])))
|
wneuper@59316
|
198 |
else (i, v, false, sel, Model.Sup (d, ts)))
|
wneuper@59262
|
199 |
end
|
neuper@37906
|
200 |
|
wneuper@59262
|
201 |
(* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
|
wneuper@59262
|
202 |
fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
|
neuper@37906
|
203 |
fun fstr2itm_ thy pbt (f, str) =
|
wneuper@59262
|
204 |
let
|
wneuper@59389
|
205 |
val topt = TermC.parse thy str
|
wneuper@59262
|
206 |
in
|
wneuper@59262
|
207 |
case topt of
|
wneuper@59316
|
208 |
NONE => ([], false, f, Model.Syn str)
|
wneuper@59262
|
209 |
| SOME ct =>
|
wneuper@59262
|
210 |
let
|
wneuper@59316
|
211 |
val (d, ts) = (Model.split_dts o Thm.term_of) ct
|
wneuper@59262
|
212 |
val popt = find_first (eq7 (f, d)) pbt
|
wneuper@59262
|
213 |
in
|
wneuper@59262
|
214 |
case popt of
|
wneuper@59316
|
215 |
NONE => ([1](*??*), true(*??*), f, Model.Sup (d, ts))
|
wneuper@59316
|
216 |
| SOME (f, (d, id)) => ([1], true, f, Model.Cor ((d, ts), (id, ts)))
|
wneuper@59262
|
217 |
end
|
wneuper@59262
|
218 |
end
|
neuper@37906
|
219 |
|
neuper@37906
|
220 |
(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
|
neuper@37906
|
221 |
fun unknown_expl dI pbt selcts =
|
neuper@37906
|
222 |
let
|
wneuper@59405
|
223 |
val thy = Celem.assoc_thy dI
|
neuper@37906
|
224 |
val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
|
wneuper@59269
|
225 |
val its = Specify.add_id its_
|
wneuper@59308
|
226 |
in map flattup2 its end
|
neuper@37906
|
227 |
|
wneuper@59262
|
228 |
(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
|
wneuper@59262
|
229 |
appl_add': generate 1 item
|
wneuper@59262
|
230 |
appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
|
wneuper@59262
|
231 |
appl_add' . is_notyet_input: compare with items in model already input
|
wneuper@59262
|
232 |
insert_ppc': insert this 1 item*)
|
wneuper@59262
|
233 |
fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
|
wneuper@59262
|
234 |
(*already present itms in model are being overwritten*)
|
wneuper@59262
|
235 |
| appl_adds _ _ ppc _ [] = ppc
|
wneuper@59262
|
236 |
| appl_adds dI oris ppc pbt (selct :: ss) =
|
wneuper@59262
|
237 |
let val itm = appl_add' dI oris ppc pbt selct;
|
wneuper@59265
|
238 |
in appl_adds dI oris (Chead.insert_ppc' itm ppc) pbt ss end
|
neuper@37906
|
239 |
|
wneuper@59308
|
240 |
fun oris2itms _ _ [] = [] (* WN161130: similar in ptyps ?!? *)
|
wneuper@59308
|
241 |
| oris2itms pbt vat ((i, v, f, d, ts) :: os) =
|
neuper@37930
|
242 |
if member op = vat v
|
wneuper@59416
|
243 |
then (i, v, true, f, Model.Cor ((d, ts), (Rule.e_term, []))) :: (oris2itms pbt vat os)
|
wneuper@59262
|
244 |
else oris2itms pbt vat os
|
neuper@37906
|
245 |
|
wneuper@59316
|
246 |
fun par2fstr (_, _, _, f, Model.Par s) = (f, s)
|
wneuper@59592
|
247 |
| par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (Rule.thy2ctxt' "Isac_Knowledge") itm)
|
wneuper@59316
|
248 |
fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts))
|
wneuper@59316
|
249 |
| itms2fstr (_, _, _, f, Model.Syn str) = (f, str)
|
wneuper@59316
|
250 |
| itms2fstr (_, _, _, f, Model.Typ str) = (f, str)
|
wneuper@59316
|
251 |
| itms2fstr (_, _, _, f, Model.Inc ((d, ts), _)) = (f, Model.comp_dts'' (d,ts))
|
wneuper@59316
|
252 |
| itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts))
|
wneuper@59416
|
253 |
| itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, Rule.term2str (d $ t))
|
wneuper@59316
|
254 |
| itms2fstr (itm as (_, _, _, _, Model.Par _)) =
|
wneuper@59592
|
255 |
error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt' "Isac_Knowledge") itm ^ "): Par should be internal");
|
neuper@37906
|
256 |
|
neuper@37906
|
257 |
fun imodel2fstr iitems =
|
neuper@41976
|
258 |
let
|
neuper@41976
|
259 |
fun xxx is [] = is
|
neuper@41976
|
260 |
| xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
|
neuper@41976
|
261 |
| xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
|
neuper@41976
|
262 |
| xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
|
neuper@41976
|
263 |
in xxx [] iitems end;
|
neuper@37906
|
264 |
|
neuper@41976
|
265 |
(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
|
walther@59694
|
266 |
fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =
|
wneuper@59264
|
267 |
let
|
wneuper@59276
|
268 |
val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
|
wneuper@59276
|
269 |
Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
|
wneuper@59264
|
270 |
spec = sspec as (sdI, spI, smI), probl, meth, ...}
|
wneuper@59264
|
271 |
=> (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
|
wneuper@59264
|
272 |
| _ => error "input_icalhd: uncovered case of get_obj I pt p"
|
wneuper@59389
|
273 |
in if is_casinput hdf fmz then the (cas_input (TermC.str2term hdf))
|
neuper@37906
|
274 |
else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
|
neuper@41976
|
275 |
let val (pos_, pits, mits) =
|
neuper@41976
|
276 |
if dI <> sdI
|
wneuper@59405
|
277 |
then let val its = map (parsitm (Celem.assoc_thy dI)) probl;
|
neuper@41976
|
278 |
val (its, trms) = filter_sep is_Par its;
|
wneuper@59269
|
279 |
val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec))
|
walther@59694
|
280 |
in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
|
wneuper@59264
|
281 |
else
|
wneuper@59264
|
282 |
if pI <> spI
|
walther@59694
|
283 |
then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
|
wneuper@59264
|
284 |
else
|
wneuper@59269
|
285 |
let val pbt = (#ppc o Specify.get_pbt) pI
|
wneuper@59265
|
286 |
val dI' = #1 (Chead.some_spec ospec spec)
|
wneuper@59264
|
287 |
val oris = if pI = #2 ospec then oris
|
wneuper@59592
|
288 |
else Specify.prep_ori fmz_(Celem.assoc_thy"Isac_Knowledge") pbt |> #1;
|
walther@59694
|
289 |
in (Pos.Pbl, appl_adds dI' oris probl pbt
|
wneuper@59264
|
290 |
(map itms2fstr probl), meth) end
|
wneuper@59264
|
291 |
else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
|
wneuper@59269
|
292 |
then let val met = (#ppc o Specify.get_met) mI
|
wneuper@59265
|
293 |
val mits = Chead.complete_metitms oris probl meth met
|
wneuper@59264
|
294 |
in if foldl and_ (true, map #3 mits)
|
walther@59694
|
295 |
then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
|
wneuper@59264
|
296 |
end
|
walther@59694
|
297 |
else (Pos.Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
|
wneuper@59269
|
298 |
((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec)))
|
wneuper@59264
|
299 |
(imodel2fstr imodel), meth)
|
wneuper@59276
|
300 |
val pt = Ctree.update_spec pt p spec;
|
walther@59694
|
301 |
in if pos_ = Pos.Pbl
|
wneuper@59269
|
302 |
then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
|
wneuper@59592
|
303 |
val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls where_ pits
|
wneuper@59276
|
304 |
in (Ctree.update_pbl pt p pits,
|
walther@59694
|
305 |
(Chead.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
|
neuper@41976
|
306 |
end
|
wneuper@59269
|
307 |
else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
|
wneuper@59592
|
308 |
val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls pre mits
|
wneuper@59276
|
309 |
in (Ctree.update_met pt p mits,
|
walther@59694
|
310 |
(Chead.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
|
neuper@41976
|
311 |
end
|
neuper@41976
|
312 |
end
|
neuper@41976
|
313 |
end
|
wneuper@59264
|
314 |
| input_icalhd _ (_, _, _, _(*Met*), _) = error "input_icalhd Met not impl."
|
neuper@37906
|
315 |
|
neuper@37906
|
316 |
|
neuper@37906
|
317 |
(***. handle an input formula .***)
|
neuper@37906
|
318 |
|
neuper@37906
|
319 |
(*the lists contain eq-al elem-pairs at the beginning;
|
neuper@37906
|
320 |
return first list reverted (again) - ie. in order as required subsequently*)
|
neuper@37906
|
321 |
fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
|
wneuper@59264
|
322 |
if equal f1 i1
|
wneuper@59264
|
323 |
then
|
wneuper@59264
|
324 |
if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)
|
wneuper@59264
|
325 |
else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)
|
neuper@38031
|
326 |
else error "dropwhile': did not start with equal elements"
|
neuper@37906
|
327 |
| dropwhile' equal (f::fs) [i] =
|
wneuper@59264
|
328 |
if equal f i
|
wneuper@59264
|
329 |
then (rev (f::fs), [i])
|
neuper@38031
|
330 |
else error "dropwhile': did not start with equal elements"
|
neuper@37906
|
331 |
| dropwhile' equal [f] (i::is) =
|
wneuper@59264
|
332 |
if equal f i
|
wneuper@59264
|
333 |
then ([f], i::is)
|
wneuper@59264
|
334 |
else error "dropwhile': did not start with equal elements"
|
wneuper@59264
|
335 |
| dropwhile' _ _ _ = error "dropwhile': uncovered case"
|
neuper@37906
|
336 |
|
wneuper@59264
|
337 |
(* 040214: version for concat_deriv *)
|
wneuper@59263
|
338 |
fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));
|
neuper@37906
|
339 |
|
wneuper@59416
|
340 |
fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
|
wneuper@59571
|
341 |
(Tactic.Rewrite (id, thm),
|
walther@59790
|
342 |
Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, LItool.rule2thm'' r, t, (t', a)),
|
walther@59694
|
343 |
(Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt)))
|
wneuper@59416
|
344 |
| mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) =
|
walther@59790
|
345 |
(Tactic.Rewrite_Set (LItool.rule2rls' r),
|
wneuper@59592
|
346 |
Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
|
walther@59694
|
347 |
(Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt)))
|
wneuper@59416
|
348 |
| mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.rule2str r ^ " at " ^ Rule.term2str t)
|
neuper@37906
|
349 |
|
wneuper@59264
|
350 |
(* fo = ifo excluded already in inform *)
|
neuper@37906
|
351 |
fun concat_deriv rew_ord erls rules fo ifo =
|
neuper@55487
|
352 |
let
|
wneuper@59416
|
353 |
fun derivat ([]:(term * Rule.rule * (term * term list)) list) = Rule.e_term
|
neuper@55487
|
354 |
| derivat dt = (#1 o #3 o last_elem) dt
|
neuper@55487
|
355 |
fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
|
wneuper@59263
|
356 |
val fod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE fo
|
wneuper@59263
|
357 |
val ifod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
|
neuper@55487
|
358 |
in
|
neuper@55487
|
359 |
case (fod, ifod) of
|
neuper@55487
|
360 |
([], []) => if fo = ifo then (true, []) else (false, [])
|
neuper@55487
|
361 |
| (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
|
neuper@55487
|
362 |
| ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
|
neuper@55487
|
363 |
| (fod, ifod) =>
|
neuper@55487
|
364 |
if derivat fod = derivat ifod (*common normal form found*)
|
neuper@55487
|
365 |
then
|
neuper@55487
|
366 |
let
|
neuper@55487
|
367 |
val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
|
neuper@55487
|
368 |
in (true, fod' @ (map rev_deriv' rifod')) end
|
neuper@55487
|
369 |
else (false, [])
|
wneuper@59264
|
370 |
end
|
neuper@37906
|
371 |
|
neuper@42428
|
372 |
(* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
|
wneuper@59405
|
373 |
fun check_err_patt (res, inf) subst (errpatID, pat) rls =
|
neuper@42423
|
374 |
let
|
neuper@42423
|
375 |
val (res', _, _, rewritten) =
|
wneuper@59416
|
376 |
Rewrite.rew_sub (Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) res;
|
neuper@42423
|
377 |
in
|
neuper@42423
|
378 |
if rewritten
|
neuper@42423
|
379 |
then
|
neuper@42423
|
380 |
let
|
wneuper@59380
|
381 |
val norm_res = case Rewrite.rewrite_set_inst_ (Isac()) false subst rls res' of
|
neuper@42423
|
382 |
NONE => res'
|
neuper@42423
|
383 |
| SOME (norm_res, _) => norm_res
|
wneuper@59380
|
384 |
val norm_inf = case Rewrite.rewrite_set_inst_ (Isac()) false subst rls inf of
|
neuper@42423
|
385 |
NONE => inf
|
neuper@42423
|
386 |
| SOME (norm_inf, _) => norm_inf
|
neuper@42423
|
387 |
in if norm_res = norm_inf then SOME errpatID else NONE
|
neuper@42423
|
388 |
end
|
neuper@42423
|
389 |
else NONE
|
neuper@42423
|
390 |
end;
|
neuper@42423
|
391 |
|
neuper@42428
|
392 |
(* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
|
neuper@42428
|
393 |
(prog, env) for retrieval of casual substitution for bdv in the pattern. *)
|
neuper@42428
|
394 |
fun check_error_patterns (res, inf) (prog, env) (errpats, rls) =
|
neuper@42428
|
395 |
let
|
wneuper@59263
|
396 |
val (_, subst) = Rtools.get_bdv_subst prog env
|
neuper@42428
|
397 |
fun scan (_, [], _) = NONE
|
neuper@42428
|
398 |
| scan (errpatID, errpat :: errpats, _) =
|
wneuper@59405
|
399 |
case check_err_patt (res, inf) subst (errpatID, errpat) rls of
|
neuper@42428
|
400 |
NONE => scan (errpatID, errpats, [])
|
neuper@42428
|
401 |
| SOME errpatID => SOME errpatID
|
neuper@42428
|
402 |
fun scans [] = NONE
|
neuper@42428
|
403 |
| scans (group :: groups) =
|
neuper@42428
|
404 |
case scan group of
|
neuper@42428
|
405 |
NONE => scans groups
|
neuper@42428
|
406 |
| SOME errpatID => SOME errpatID
|
neuper@42428
|
407 |
in scans errpats end;
|
neuper@42428
|
408 |
|
neuper@42433
|
409 |
(* fill-in patterns an forms.
|
neuper@42433
|
410 |
returns thm required by "fun in_fillform *)
|
wneuper@59405
|
411 |
fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =
|
neuper@42430
|
412 |
let
|
neuper@42430
|
413 |
val (form', _, _, rewritten) =
|
wneuper@59416
|
414 |
Rewrite.rew_sub (Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) form;
|
neuper@42430
|
415 |
in (*the fillpat of the thm must be dedicated to errpatID*)
|
neuper@42430
|
416 |
if errpatID = erpaID andalso rewritten
|
wneuper@59264
|
417 |
then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
|
wneuper@59264
|
418 |
else NONE
|
wneuper@59264
|
419 |
end
|
neuper@42430
|
420 |
|
neuper@42430
|
421 |
fun get_fillpats subst form errpatID thm =
|
wneuper@59264
|
422 |
let
|
wneuper@59264
|
423 |
val thmDeriv = Thm.get_name_hint thm
|
wneuper@59264
|
424 |
val (part, thyID) = Rtools.thy_containing_thm thmDeriv
|
wneuper@59405
|
425 |
val theID = [part, thyID, "Theorems", Celem.thmID_of_derivation_name thmDeriv]
|
wneuper@59269
|
426 |
val fillpats = case Specify.get_the theID of
|
wneuper@59405
|
427 |
Celem.Hthm {fillpats, ...} => fillpats
|
wneuper@59264
|
428 |
| _ => error "get_fillpats: uncovered case of get_the"
|
wneuper@59264
|
429 |
val some = map (get_fillform subst (thm, form) errpatID) fillpats
|
wneuper@59264
|
430 |
in some |> filter is_some |> map the end
|
neuper@42430
|
431 |
|
wneuper@59276
|
432 |
fun find_fillpatterns (pt, pos as (p, _): Ctree.pos') errpatID =
|
neuper@42430
|
433 |
let
|
wneuper@59276
|
434 |
val f_curr = Ctree.get_curr_formula (pt, pos);
|
wneuper@59276
|
435 |
val pp = Ctree.par_pblobj pt p
|
wneuper@59276
|
436 |
val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
|
wneuper@59416
|
437 |
{errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
|
wneuper@59264
|
438 |
| _ => error "find_fillpatterns: uncovered case of get_met"
|
walther@59807
|
439 |
val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
|
wneuper@59263
|
440 |
val subst = Rtools.get_bdv_subst prog env
|
neuper@42430
|
441 |
val errpatthms = errpats
|
wneuper@59416
|
442 |
|> filter ((curry op = errpatID) o (#1: Rule.errpat -> Rule.errpatID))
|
wneuper@59416
|
443 |
|> map (#3: Rule.errpat -> thm list)
|
neuper@42430
|
444 |
|> flat
|
wneuper@59264
|
445 |
in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
|
neuper@37906
|
446 |
|
neuper@42437
|
447 |
(* check if an input formula is exactly equal the rewrite from a rule
|
neuper@42437
|
448 |
which is stored at the pos where the input is stored of "ok". *)
|
neuper@42437
|
449 |
fun is_exactly_equal (pt, pos as (p, _)) istr =
|
wneuper@59592
|
450 |
case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> Rule.thy2ctxt) istr of
|
wneuper@59571
|
451 |
NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
|
neuper@42437
|
452 |
| SOME ifo =>
|
neuper@42437
|
453 |
let
|
walther@59757
|
454 |
val p' = Pos.lev_on p;
|
wneuper@59276
|
455 |
val tac = Ctree.get_obj Ctree.g_tac pt p';
|
neuper@42437
|
456 |
in
|
wneuper@59272
|
457 |
case Applicable.applicable_in pos pt tac of
|
walther@59735
|
458 |
Applicable.Notappl msg => (msg, Tactic.Tac "")
|
walther@59735
|
459 |
| Applicable.Appl rew =>
|
neuper@42437
|
460 |
let
|
neuper@42437
|
461 |
val res = case rew of
|
wneuper@59571
|
462 |
Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
|
wneuper@59571
|
463 |
|Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
|
walther@59728
|
464 |
| t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t)
|
neuper@42437
|
465 |
in
|
neuper@42437
|
466 |
if not (ifo = res)
|
wneuper@59571
|
467 |
then ("input does not exactly fill the gaps", Tactic.Tac "")
|
neuper@42437
|
468 |
else ("ok", tac)
|
neuper@42437
|
469 |
end
|
neuper@42437
|
470 |
end
|
neuper@42437
|
471 |
|
neuper@42458
|
472 |
(* fetch errpatIDs from an arbitrary tactic *)
|
neuper@42458
|
473 |
fun fetchErrorpatterns tac =
|
neuper@42458
|
474 |
let
|
neuper@42458
|
475 |
val rlsID =
|
neuper@42458
|
476 |
case tac of
|
wneuper@59571
|
477 |
Tactic.Rewrite_Set rlsID => rlsID
|
wneuper@59571
|
478 |
|Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
|
neuper@55415
|
479 |
| _ => "e_rls"
|
wneuper@59592
|
480 |
val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID;
|
wneuper@59269
|
481 |
val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
|
wneuper@59405
|
482 |
Celem.Hrls {thy_rls = (_, rls), ...} => rls
|
wneuper@59264
|
483 |
| _ => error "fetchErrorpatterns: uncovered case of get_the"
|
neuper@42458
|
484 |
in case rls of
|
wneuper@59416
|
485 |
Rule.Rls {errpatts, ...} => errpatts
|
wneuper@59416
|
486 |
| Rule.Seq {errpatts, ...} => errpatts
|
wneuper@59416
|
487 |
| Rule.Rrls {errpatts, ...} => errpatts
|
wneuper@59416
|
488 |
| Rule.Erls => []
|
neuper@42458
|
489 |
end
|
wneuper@59264
|
490 |
|
wneuper@59262
|
491 |
(**)
|
neuper@37906
|
492 |
end
|
wneuper@59262
|
493 |
(**) |