1 (* Title: Specify/input-calchead.sml |
|
2 Author: Walther Neuper |
|
3 (c) due to copyright terms |
|
4 |
|
5 This will be dropped at switch to Isabelle/PIDE. |
|
6 *) |
|
7 |
|
8 signature INPUT_SPECIFICATION = |
|
9 sig |
|
10 datatype iitem = |
|
11 Find of TermC.as_string list |
|
12 | Given of TermC.as_string list |
|
13 | Relate of TermC.as_string list |
|
14 type imodel = iitem list |
|
15 type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T |
|
16 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T |
|
17 val cas_input : term -> (Ctree.ctree * Specification.T) option |
|
18 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
|
19 (* NONE *) |
|
20 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
|
21 val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T -> |
|
22 string * TermC.as_string -> I_Model.single |
|
23 val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T -> |
|
24 (string * TermC.as_string) list -> I_Model.T |
|
25 val cas_input_: References.T -> (term * term list) list -> |
|
26 Problem.id * I_Model.T * Method.id * I_Model.T * Pre_Conds.T * Proof.context |
|
27 val dtss2itm_: Model_Pattern.single list -> term * term list -> |
|
28 int list * bool * string * I_Model.feedback (*I_Model.single'*) |
|
29 val e_icalhd: icalhd |
|
30 val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool |
|
31 val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list |
|
32 val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e |
|
33 val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string -> |
|
34 int list * bool * ''a * I_Model.feedback (*I_Model.single'*) |
|
35 val imodel2fstr: iitem list -> (string * TermC.as_string) list |
|
36 val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*) |
|
37 val is_casinput: TermC.as_string -> Formalise.T -> bool |
|
38 val is_e_ts: term list -> bool |
|
39 val itms2fstr: I_Model.single -> string * string |
|
40 val par2fstr: I_Model.single -> string * TermC.as_string |
|
41 val parsitm: theory -> I_Model.single -> I_Model.single |
|
42 val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*) |
|
43 (''a * string) list -> |
|
44 (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*) |
|
45 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
|
46 end |
|
47 |
|
48 (**) |
|
49 structure Input_Spec(**): INPUT_SPECIFICATION(**) = |
|
50 struct |
|
51 (**) |
|
52 |
|
53 (** handle input **) |
|
54 |
|
55 fun dtss2itm_ ppc (d, ts) = |
|
56 let |
|
57 val (f, (d, id)) = the (find_first ((curry op= d) o |
|
58 (#1: (term * term) -> term) o |
|
59 (#2: Model_Pattern.single -> (term * term))) ppc) |
|
60 in |
|
61 ([1], true, f, I_Model.Cor ((d, ts), (id, ts))) |
|
62 end |
|
63 |
|
64 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e) |
|
65 |
|
66 fun cas_input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*) |
|
67 let |
|
68 val thy = ThyC.get_theory dI |
|
69 val {ppc, ...} = Problem.from_store pI |
|
70 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*) |
|
71 val its = O_Model.add_id its_ |
|
72 val pits = map flattup2 its |
|
73 val (pI, mI) = |
|
74 if mI <> ["no_met"] |
|
75 then (pI, mI) |
|
76 else |
|
77 case Refine.problem thy pI pits of |
|
78 SOME (pI,_) => (pI, (hd o #met o Problem.from_store) pI) |
|
79 | NONE => (pI, (hd o #met o Problem.from_store) pI) |
|
80 val {ppc, pre, prls, ...} = Method.from_store mI |
|
81 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*) |
|
82 val its = O_Model.add_id its_ |
|
83 val mits = map flattup2 its |
|
84 val pre = Pre_Conds.check' thy prls pre mits |
|
85 val ctxt = Proof_Context.init_global thy |
|
86 in (pI, pits, mI, mits, pre, ctxt) end; |
|
87 |
|
88 |
|
89 (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *) |
|
90 fun cas_input hdt = |
|
91 let |
|
92 val (h, argl) = strip_comb hdt |
|
93 in |
|
94 case assoc_cas (ThyC.get_theory "Isac_Knowledge") h of |
|
95 NONE => NONE |
|
96 | SOME (spec as (dI,_,_), argl2dtss) => |
|
97 let |
|
98 val dtss = argl2dtss argl |
|
99 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss |
|
100 val spec = (dI, pI, mI) |
|
101 val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty) |
|
102 ([], References.empty) ([], References.empty, hdt, ctxt) |
|
103 val pt = Ctree.update_spec pt [] spec |
|
104 val pt = Ctree.update_pbl pt [] pits |
|
105 val pt = Ctree.update_met pt [] mits |
|
106 in |
|
107 SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Specification.T) |
|
108 end |
|
109 end |
|
110 |
|
111 |
|
112 (** handle an input calc-head **) |
|
113 |
|
114 datatype iitem = |
|
115 Given of TermC.as_string list |
|
116 (*Where is still not input*) |
|
117 | Find of TermC.as_string list |
|
118 | Relate of TermC.as_string list |
|
119 |
|
120 type imodel = iitem list |
|
121 |
|
122 type icalhd = |
|
123 Pos.pos' * (* the position in Ctree *) |
|
124 TermC.as_string * (* the headline shown on Calc.T *) |
|
125 imodel * (* the model *) |
|
126 Pos.pos_ * (* model belongs to Problem or Method *) |
|
127 References.T; (* into Know_Store *) |
|
128 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty) |
|
129 |
|
130 fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) = |
|
131 hdf <> "" andalso fmz_ = [] andalso spec = References.empty |
|
132 |
|
133 (* re-parse itms with a new thy and prepare for checking with ori list *) |
|
134 fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) = |
|
135 (let val t = Input_Descript.join (d, ts) |
|
136 val _ = (UnparseC.term_in_thy dI t) |
|
137 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *) |
|
138 in itm end |
|
139 handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) |
|
140 | parsitm dI (i, v, b, f, I_Model.Syn str) = |
|
141 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str |
|
142 in (i, v, b ,f, I_Model.Par str) end |
|
143 handle _ => (i, v, b, f, I_Model.Syn str)) |
|
144 | parsitm dI (i, v, b, f, I_Model.Typ str) = |
|
145 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str |
|
146 in (i, v, b, f, I_Model.Par str) end |
|
147 handle _ => (i, v, b, f, I_Model.Syn str)) |
|
148 | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) = |
|
149 (let val t = Input_Descript.join (d,ts); |
|
150 val _ = UnparseC.term_in_thy dI t; |
|
151 (*this ^ should raise the exn on unability of re-parsing dts*) |
|
152 in itm end |
|
153 handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) |
|
154 | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) = |
|
155 (let val t = Input_Descript.join (d,ts); |
|
156 val _ = UnparseC.term_in_thy dI t; |
|
157 (*this ^ should raise the exn on unability of re-parsing dts*) |
|
158 in itm end |
|
159 handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) |
|
160 | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) = |
|
161 (let val t = d $ t'; |
|
162 val _ = UnparseC.term_in_thy dI t; |
|
163 (*this ^ should raise the exn on unability of re-parsing dts*) |
|
164 in itm end |
|
165 handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) |
|
166 | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) = |
|
167 raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal"); |
|
168 |
|
169 (*separate a list to a pair of elements that do NOT satisfy the predicate, |
|
170 and of elements that satisfy the predicate, i.e. (false, true)*) |
|
171 fun filter_sep pred xs = |
|
172 let |
|
173 fun filt ab [] = ab |
|
174 | filt (a, b) (x :: xs) = |
|
175 if pred x |
|
176 then filt (a, b @ [x]) xs |
|
177 else filt (a @ [x], b) xs |
|
178 in filt ([], []) xs end; |
|
179 fun is_Par (_, _, _, _, I_Model.Par _) = true |
|
180 | is_Par _ = false; |
|
181 |
|
182 fun is_e_ts [] = true |
|
183 | is_e_ts [Const ("List.list.Nil", _)] = true |
|
184 | is_e_ts _ = false; |
|
185 |
|
186 (* WN.9.11.03 copied from fun appl_add *) |
|
187 fun appl_add' dI oris ppc pbt (sel, ct) = |
|
188 let |
|
189 val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt; |
|
190 in |
|
191 case TermC.parseNEW ctxt ct of |
|
192 NONE => (0, [], false, sel, I_Model.Syn ct) |
|
193 | SOME t => |
|
194 (case I_Model.is_known ctxt sel oris t of |
|
195 ("", ori', all) => |
|
196 (case I_Model.is_notyet_input ctxt ppc all ori' pbt of |
|
197 ("",itm) => itm |
|
198 | (msg,_) => raise ERROR ("appl_add': " ^ msg)) |
|
199 | (_, (i, v, _, d, ts), _) => |
|
200 if is_e_ts ts |
|
201 then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, []))) |
|
202 else (i, v, false, sel, I_Model.Sup (d, ts))) |
|
203 end |
|
204 |
|
205 (* generate preliminary itm_ from a strin (with field "#Given" etc.) *) |
|
206 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d'; |
|
207 fun fstr2itm_ thy pbt (f, str) = |
|
208 let |
|
209 val topt = TermC.parse thy str |
|
210 in |
|
211 case topt of |
|
212 NONE => ([], false, f, I_Model.Syn str) |
|
213 | SOME ct => |
|
214 let |
|
215 val (d, ts) = (Input_Descript.split o Thm.term_of) ct |
|
216 val popt = find_first (eq7 (f, d)) pbt |
|
217 in |
|
218 case popt of |
|
219 NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts)) |
|
220 | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts))) |
|
221 end |
|
222 end |
|
223 |
|
224 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*) |
|
225 fun unknown_expl dI pbt selcts = |
|
226 let |
|
227 val thy = ThyC.get_theory dI |
|
228 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*) |
|
229 val its = O_Model.add_id its_ |
|
230 in map flattup2 its end |
|
231 |
|
232 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation |
|
233 appl_add': generate 1 item |
|
234 appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..) |
|
235 appl_add' . is_notyet_input: compare with items in model already input |
|
236 insert_ppc': insert this 1 item*) |
|
237 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts |
|
238 (*already present itms in model are being overwritten*) |
|
239 | appl_adds _ _ ppc _ [] = ppc |
|
240 | appl_adds dI oris ppc pbt (selct :: ss) = |
|
241 let val itm = appl_add' dI oris ppc pbt selct; |
|
242 in appl_adds dI oris (Specification.insert_ppc' itm ppc) pbt ss end |
|
243 |
|
244 fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s) |
|
245 | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm) |
|
246 fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts)) |
|
247 | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str) |
|
248 | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str) |
|
249 | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts)) |
|
250 | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts)) |
|
251 | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t)) |
|
252 | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) = |
|
253 raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal"); |
|
254 |
|
255 fun imodel2fstr iitems = |
|
256 let |
|
257 fun xxx is [] = is |
|
258 | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis |
|
259 | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis |
|
260 | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis |
|
261 in xxx [] iitems end; |
|
262 |
|
263 (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *) |
|
264 fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) = |
|
265 let |
|
266 val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of |
|
267 Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), |
|
268 spec = sspec as (sdI, spI, smI), probl, meth, ...} |
|
269 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) |
|
270 | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p" |
|
271 in if is_casinput hdf fmz then the (cas_input (TermC.str2term hdf)) |
|
272 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*) |
|
273 let val (pos_, pits, mits) = |
|
274 if dI <> sdI |
|
275 then let val its = map (parsitm (ThyC.get_theory dI)) probl; |
|
276 val (its, trms) = filter_sep is_Par its; |
|
277 val pbt = (#ppc o Problem.from_store) (#2 (Specification.some_spec ospec sspec)) |
|
278 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end |
|
279 else |
|
280 if pI <> spI |
|
281 then if pI = snd3 ospec then (Pos.Pbl, probl, meth) |
|
282 else |
|
283 let val pbt = (#ppc o Problem.from_store) pI |
|
284 val dI' = #1 (Specification.some_spec ospec spec) |
|
285 val oris = if pI = #2 ospec then oris |
|
286 else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*); |
|
287 in (Pos.Pbl, appl_adds dI' oris probl pbt |
|
288 (map itms2fstr probl), meth) end |
|
289 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*) |
|
290 then let val met = (#ppc o Method.from_store) mI |
|
291 val mits = Specification.complete_metitms oris probl meth met |
|
292 in if foldl and_ (true, map #3 mits) |
|
293 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) |
|
294 end |
|
295 else (Pos.Pbl, appl_adds (#1 (Specification.some_spec ospec spec)) oris [(*!!!*)] |
|
296 ((#ppc o Problem.from_store) (#2 (Specification.some_spec ospec spec))) |
|
297 (imodel2fstr imodel), meth) |
|
298 val pt = Ctree.update_spec pt p spec; |
|
299 in if pos_ = Pos.Pbl |
|
300 then let val {prls,where_,...} = Problem.from_store (#2 (Specification.some_spec ospec spec)) |
|
301 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits |
|
302 in (Ctree.update_pbl pt p pits, |
|
303 (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T) |
|
304 end |
|
305 else let val {prls,pre,...} = Method.from_store (#3 (Specification.some_spec ospec spec)) |
|
306 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits |
|
307 in (Ctree.update_met pt p mits, |
|
308 (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T) |
|
309 end |
|
310 end |
|
311 end |
|
312 | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl." |
|
313 |
|
314 (**)end (**) |
|