|
1 (* tools for model-specify and ptyps |
|
2 use"ME/mstools.sml"; |
|
3 use"mstools.sml"; |
|
4 *) |
|
5 |
|
6 |
|
7 |
|
8 (*27.8.01: problem-environment*) |
|
9 type penv = (term (*err_*) |
|
10 * (term list) (*[#0, epsilon]*) |
|
11 ) list; |
|
12 fun pen2str thy (t, ts) = |
|
13 pair2str(Sign.string_of_term (sign_of thy) t, |
|
14 (strs2str' o map (Sign.string_of_term (sign_of thy))) ts); |
|
15 fun penv2str thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv; |
|
16 |
|
17 type envv = (int * penv) list; |
|
18 |
|
19 (*. 14.9.01: not used after putting penv-values into itm_ |
|
20 make the result of split_* a value of problem-environment .*) |
|
21 fun mkval dsc [] = raise error "mkval called with []" |
|
22 | mkval dsc [t] = t |
|
23 | mkval dsc ts = list2isalist ((type_of o hd) ts) ts; |
|
24 |
|
25 |
|
26 |
|
27 |
|
28 (*. get the constant value from a penv .*) |
|
29 fun getval (id, values) = |
|
30 case values of |
|
31 [] => raise error ("penv_value: no values in '"^ |
|
32 (Sign.string_of_term (sign_of Tools.thy) id)) |
|
33 | [v] => (id, v) |
|
34 | (v1::v2::_) => (case v1 of |
|
35 Const ("Script.Arbfix",_) => (id, v2) |
|
36 | _ => (id, v1)); |
|
37 (* |
|
38 val e_ = (term_of o the o (parse thy)) "e_::bool"; |
|
39 val ev = (term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0"; |
|
40 val v_ = (term_of o the o (parse thy)) "v_"; |
|
41 val vv = (term_of o the o (parse thy)) "x"; |
|
42 val r_ = (term_of o the o (parse thy)) "err_::bool"; |
|
43 val rv1 = (term_of o the o (parse thy)) "eps"; |
|
44 val rv2 = (term_of o the o (parse thy)) "#0"; |
|
45 |
|
46 val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv1])]:penv; |
|
47 map getval penv; |
|
48 [(Free ("e_","bool"), |
|
49 Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#0","RealDef.real")), |
|
50 (Free ("v_","RealDef.real"),Free ("x","RealDef.real")), |
|
51 (Free ("err_","bool"),Free ("#0","RealDef.real"))] : (term * term) list |
|
52 *) |
|
53 |
|
54 |
|
55 (*23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc |
|
56 (1) kinds of itms: |
|
57 (1.1) untouched: for modeling only dsc displayed(impossible after match_itms) |
|
58 =(presently) Mis (? should be Inc initially, and Mis after match_itms?) |
|
59 (1.2) Syn,Typ,Sup: not related to oris |
|
60 Syn, Typ (presently) should be accepted in appl_add (instead Error') |
|
61 Sup (presently) should be accepted in appl_add (instead Error') |
|
62 _could_ be w.r.t current vat (and then _is_ related to vat |
|
63 Mis should _not_ be made Inc ((presently, by appl_add & match_itms) |
|
64 - dsc in itm_ is timeconsuming -- keep id for respective queries ? |
|
65 - order of items in ppc should be stable w.r.t order of itms |
|
66 |
|
67 - stepwise input of itms --- match_itms (in one go) ..not koordinated |
|
68 - unify code |
|
69 - match_itms / match_itms_oris ..2 versions ?! |
|
70 (fast, for refine / slow, for modeling) |
|
71 |
|
72 - clarify: efficiency <--> simplicity !!! |
|
73 ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc |
|
74 | take int for perserving order of item ppc in itms |
|
75 | make all(!?) handling of itms stable against reordering(?) |
|
76 | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???) |
|
77 -"- "#undef" ?= not touched ?= (id,..) |
|
78 ----------------------------------------------------------------- |
|
79 27.3.02: |
|
80 def: type pbt = (field, (dsc, pid)) |
|
81 |
|
82 (1) fmz + pbt -> oris |
|
83 (2) input + oris -> itm |
|
84 (3) match_itms : schnell(?) f"ur refine |
|
85 match_itms_oris : r"uckmeldung f"ur item ppc |
|
86 |
|
87 (1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid) |
|
88 ---------- ^^^^^ --- dh. pbt meist als argument zu viel !!! |
|
89 |
|
90 (3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht; |
|
91 wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????: |
|
92 (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ???? |
|
93 (b) |
|
94 *) |
|
95 |
|
96 |
|
97 |
|
98 |
|
99 (*4.9.01: not consistent: |
|
100 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation |
|
101 (involves 'is_error'); |
|
102 bool in itm really necessary ???*) |
|
103 datatype itm_ = |
|
104 Cor of (term * (* description *) |
|
105 (term list)) * (* for list: elem-wise input *) |
|
106 (term * (term list)) (* elem of penv *) |
|
107 | Syn of cterm' |
|
108 | Typ of cterm' |
|
109 | Inc of (term * (term list)) * (term * (term list)) (*lists only !*) |
|
110 | Sup of (term * (term list)) (* user-input not found in pbt *) |
|
111 | Mis of (term * term) (* pbt-item not found in pbl: only dsc, pid_ *) |
|
112 (*| Inc of bool --- instead of istate in itm ?26.1.00?*); |
|
113 |
|
114 type vats = int list; (*variants in formalizations*) |
|
115 |
|
116 (*.data-type for working on pbl/met-ppc: |
|
117 in pbl initially holds descriptions (only) for user guidance.*) |
|
118 type itm = |
|
119 int * (* id =0 .. untouched - descript (only) from init |
|
120 23.3.02: seems to correspond to ori (fun insert_ppc) |
|
121 with the purpose to maintain order in item ppc?*) |
|
122 vats * (* variants - copy from ori *) |
|
123 bool * (* input on this item is not/complete *) |
|
124 string * (* #Given | #Find | #Relate *) |
|
125 itm_; (* *) |
|
126 (* use"ME/sequent.sml"; |
|
127 *) |
|
128 val e_itm = (0,[],false,"e_itm",Syn"e_itm"):itm; |
|
129 |
|
130 (* find most frequent variant v in itms *) |
|
131 |
|
132 fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list); |
|
133 |
|
134 fun cnt itms v = (v,(length o (filter (curry op= v)) o |
|
135 flat o (map #2)) (itms:itm list)); |
|
136 fun vts_cnt vts itms = map (cnt itms) vts; |
|
137 fun max2 [] = raise error "max2 of []" |
|
138 | max2 (y::ys) = |
|
139 let fun mx (a,x) [] = (a,x) |
|
140 | mx (a,x) ((b,y)::ys) = |
|
141 if x < y then mx (b,y) ys else mx (a,x) ys; |
|
142 in mx y ys end; |
|
143 |
|
144 (*. find the variant with most items already input .*) |
|
145 fun max_vt itms = |
|
146 let val vts = (vts_cnt (vts_in itms)) itms; |
|
147 in if vts = [] then 0 else (fst o max2) vts end; |
|
148 |
|
149 |
|
150 (* TODO ev. make more efficient by avoiding flat *) |
|
151 fun mk_e (Cor (_, iv)) = [getval iv] |
|
152 | mk_e (Syn _) = [] |
|
153 | mk_e (Typ _) = [] |
|
154 | mk_e (Inc (_, iv)) = [getval iv] |
|
155 | mk_e (Sup _) = [] |
|
156 | mk_e (Mis _) = []; |
|
157 fun mk_en vt ((i,vts,b,f,itm_):itm) = |
|
158 if vt mem vts then mk_e itm_ else []; |
|
159 (*. extract the environment from an item list; |
|
160 takes the variant with most items .*) |
|
161 fun mk_env itms = |
|
162 let val vt = max_vt itms |
|
163 in (flat o (map (mk_en vt))) itms end; |
|
164 |
|
165 |
|
166 |
|
167 (*. example as provided by an author, complete w.r.t. pbt specified |
|
168 not touched by any user action .*) |
|
169 type ori = (int * (* id: 10.3.00ff impl. only <>0 .. touched |
|
170 21.3.02: insert_ppc needs it ! ?:purpose maintain |
|
171 order in item ppc ???*) |
|
172 vats * (* variants 21.3.02: related to pbt..discard ?*) |
|
173 string * (* #Given | #Find | #Relate 21.3.02: discard ?*) |
|
174 term * (* description *) |
|
175 term list (* isalist2list t | [t] *) |
|
176 ); |
|
177 val e_ori_ = (0,[],"",e_term,[e_term]):ori; |
|
178 val e_ori = (0,[],"",e_term,[e_term]):ori; |
|
179 (* [e_ori_]:ori; |
|
180 val it = [(0,[],"",Const (#,#),[Const #])] : ori |
|
181 *) |
|
182 fun ori2str ((i,vs,fi,t,ts):ori) = |
|
183 "("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^ |
|
184 (term2str t)^", "^((strs2str o (map term2str)) ts)^")"; |
|
185 fun ori02str (vs,fi,t,ts) = |
|
186 "("^((strs2str o (map string_of_int)) vs)^", "^fi^", "^ |
|
187 (term2str t)^", "^((strs2str o (map term2str)) ts)^")"; |
|
188 |
|
189 |
|
190 |
|
191 |
|
192 (*. given the input value (from split_dts) |
|
193 make the value in a problem-env according to description-type .*) |
|
194 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*) |
|
195 fun pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v = |
|
196 if is_list v |
|
197 then [v] (*eg. [r=Arbfix]*) |
|
198 else (case v of (*eg. eps=#0*) |
|
199 (Const ("op =",_) $ l $ r) => [r,l] |
|
200 | _ => raise error ("pbl_ids Tools.nam: no equality " |
|
201 ^(Sign.string_of_term (sign_of thy) v))) |
|
202 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v] |
|
203 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v] |
|
204 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v] |
|
205 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v] |
|
206 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v] |
|
207 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v] |
|
208 | pbl_ids thy _ v = raise error ("pbl_ids: not implemented for " |
|
209 ^(Sign.string_of_term (sign_of thy) v)); |
|
210 (* |
|
211 val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; |
|
212 val (d,argl) = strip_comb t; |
|
213 is_dsc d; (*see split_dts*) |
|
214 dest_list (d,argl); |
|
215 val (_ $ v) = t; |
|
216 is_list v; |
|
217 pbl_ids thy d v; |
|
218 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $ |
|
219 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List.. |
|
220 |
|
221 val (dsc,vl,_) = (split_dts o term_of o the o (parse thy)) "solveFor x"; |
|
222 val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term |
|
223 val vl = Free ("x","RealDef.real") : term |
|
224 |
|
225 val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_"; |
|
226 pbl_ids thy dsc vl; |
|
227 val it = [Free ("x","RealDef.real")] : term list |
|
228 |
|
229 val (dsc,vl,_) = (split_dts o term_of o the o(parse thy)) |
|
230 "errorBound (eps=#0)"; |
|
231 val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_"; |
|
232 pbl_ids thy dsc vl; |
|
233 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *) |
|
234 |
|
235 (*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!)) |
|
236 make the value in a problem-env according to description-type .*) |
|
237 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*) |
|
238 fun pbl_ids' (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) vs = |
|
239 (case vs of |
|
240 [] => raise error ("pbl_ids' Tools.nam called with []") |
|
241 | [t] => (case t of (*eg. eps=#0*) |
|
242 (Const ("op =",_) $ l $ r) => [r,l] |
|
243 | _ => raise error ("pbl_ids' Tools.nam: no equality " |
|
244 ^(Sign.string_of_term (sign_of thy) t))) |
|
245 | vs' => vs (*14.9.01: ???TODO *)) |
|
246 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs |
|
247 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs |
|
248 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs |
|
249 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs |
|
250 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))vs = vs |
|
251 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))vs = vs |
|
252 | pbl_ids' _ vs = |
|
253 raise error ("pbl_ids': not implemented for " |
|
254 ^(terms2str vs)); |
|
255 |
|
256 (* |
|
257 @@@@@ v |
|
258 *) |
|
259 |
|
260 |
|
261 |
|
262 |
|
263 |
|
264 |
|
265 (*14.9.01: not used after putting values for penv into itm_*) |
|
266 fun upd_penv thy penv dsc (id, vl) = |
|
267 overwrite (penv, (id, pbl_ids thy dsc vl)); |
|
268 (* |
|
269 val penv = []; |
|
270 val (dsc,vl) = (split_did o term_of o the o (parse thy)) "solveFor x"; |
|
271 val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_"; |
|
272 val penv = upd_penv thy penv dsc (id, vl); |
|
273 [(Free ("v_","RealDef.real"), |
|
274 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")])] |
|
275 : (term * term list) list |
|
276 |
|
277 val (dsc,vl) = (split_did o term_of o the o(parse thy))"errorBound (eps=#0)"; |
|
278 val (dsc,id) = (split_did o term_of o the o(parse thy))"errorBound err_"; |
|
279 upd_penv thy penv dsc (id, vl); |
|
280 [(Free ("v_","RealDef.real"), |
|
281 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")]), |
|
282 (Free ("err_","bool"), |
|
283 [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")])] |
|
284 : (term * term list) list ^.........!!!! |
|
285 *) |
|
286 |
|
287 |
|
288 fun upd thy envv dsc (id, vl) i = |
|
289 let val penv = case assoc (envv, i) of |
|
290 Some e => e |
|
291 | None => []; |
|
292 val penv' = upd_penv thy penv dsc (id, vl); |
|
293 in (i, penv') end; |
|
294 (* |
|
295 val i = 2; |
|
296 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv; |
|
297 val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b"; |
|
298 val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_"; |
|
299 upd thy envv dsc (id, vl) i; |
|
300 val it = (2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])]) |
|
301 : int * (term * term list) list*) |
|
302 |
|
303 |
|
304 (*14.9.01: not used after putting pre-penv into itm_*) |
|
305 fun upd_envv thy (envv:envv) (vats:vats) dsc id vl = |
|
306 let val vats = if length vats = 0 |
|
307 then (*unknown id to _all_ variants*) |
|
308 if length envv = 0 then [1] |
|
309 else (intsto o length) envv |
|
310 else vats |
|
311 fun isin vats (i,_) = i mem vats; |
|
312 val envs_notin_vat = filter_out (isin vats) envv; |
|
313 in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end; |
|
314 (* |
|
315 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv; |
|
316 |
|
317 val vats = [2] |
|
318 val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b"; |
|
319 val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_"; |
|
320 val envv = upd_envv thy envv vats dsc id vl; |
|
321 val envv = [(2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])] |
|
322 : (int * (term * term list) list) list |
|
323 |
|
324 val vats = [1,2,3]; |
|
325 val (dsc,vl) = (split_did o term_of o the o(parse thy))"maximum A"; |
|
326 val (dsc,id) = (split_did o term_of o the o(parse thy))"maximum m_"; |
|
327 upd_envv thy envv vats dsc id vl; |
|
328 [(1,[(Free ("m_","bool"),[Free ("A","bool")])]), |
|
329 (2, |
|
330 [(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")]), |
|
331 (Free ("m_","bool"),[Free ("A","bool")])]), |
|
332 (3,[(Free ("m_","bool"),[Free ("A","bool")])])] |
|
333 : (int * (term * term list) list) list |
|
334 |
|
335 |
|
336 val env = []:envv; |
|
337 val (d,ts) = (split_dts o term_of o the o (parse thy)) |
|
338 "fixedValues [r=Arbfix]"; |
|
339 val (_,id) = (split_did o term_of o the o (parse thy))"fixedValues fix_"; |
|
340 val vats = [1,2,3]; |
|
341 val env = upd_envv thy env vats d id (mkval ts); |
|
342 *) |
|
343 |
|
344 (*. update envv by folding from a list of arguments .*) |
|
345 fun upds_envv thy envv [] = envv |
|
346 | upds_envv thy envv ((vs, dsc, id, vl)::ps) = |
|
347 upds_envv thy (upd_envv thy envv vs dsc id vl) ps; |
|
348 (* eval test-maximum.sml until Specify_Method ... |
|
349 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI)),...} = get_obj I pt []; |
|
350 val met = (#ppc o get_met) mI; |
|
351 |
|
352 val envv = []; |
|
353 val eargs = flat eargs; |
|
354 val (vs, dsc, id, vl) = hd eargs; |
|
355 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
356 |
|
357 val (vs, dsc, id, vl) = hd (tl eargs); |
|
358 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
359 |
|
360 val (vs, dsc, id, vl) = hd (tl (tl eargs)); |
|
361 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
362 |
|
363 val (vs, dsc, id, vl) = hd (tl (tl (tl eargs))); |
|
364 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
365 [(1, |
|
366 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
367 (Free ("m_","bool"),[Free (#,#)]), |
|
368 (Free ("vs_","bool List.list"),[# $ # $ Const #]), |
|
369 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]), |
|
370 (2, |
|
371 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
372 (Free ("m_","bool"),[Free (#,#)]), |
|
373 (Free ("vs_","bool List.list"),[# $ # $ Const #]), |
|
374 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]), |
|
375 (3, |
|
376 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
377 (Free ("m_","bool"),[Free (#,#)]), |
|
378 (Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *) |
|
379 |
|
380 |
|
381 datatype item = |
|
382 Correct of cterm' |
|
383 | SyntaxE of string |
|
384 | TypeE of string |
|
385 | False of cterm' |
|
386 | Incompl of cterm' |
|
387 | Superfl of string |
|
388 | Missing of cterm'; |
|
389 fun item2str (Correct s) ="Correct "^s |
|
390 | item2str (SyntaxE s) ="SyntaxE "^s |
|
391 | item2str (TypeE s) ="TypeE "^s |
|
392 | item2str (False s) ="False "^s |
|
393 | item2str (Incompl s) ="Incompl "^s |
|
394 | item2str (Superfl s) ="Superfl "^s |
|
395 | item2str (Missing s) ="Missing "^s; |
|
396 fun init_item str = SyntaxE str; |
|
397 |
|
398 |
|
399 |
|
400 |
|
401 type 'a ppc = |
|
402 {Given : 'a list, |
|
403 Where: 'a list, |
|
404 Find : 'a list, |
|
405 With : 'a list, |
|
406 Relate: 'a list}; |
|
407 fun ppc2str {Given=Given,Where=Where,Find=Find,With=With,Relate=Relate}= |
|
408 ("{Given =" ^ (strs2str Given ) ^ |
|
409 ",Where=" ^ (strs2str Where) ^ |
|
410 ",Find =" ^ (strs2str Find ) ^ |
|
411 ",With =" ^ (strs2str With ) ^ |
|
412 ",Relate=" ^ (strs2str Relate) ^ "}"); |
|
413 |
|
414 |
|
415 |
|
416 |
|
417 fun item_ppc ({Given = gi,Where= wh, |
|
418 Find = fi,With = wi,Relate= re}: string ppc) = |
|
419 {Given = map init_item gi,Where= map init_item wh, |
|
420 Find = map init_item fi,With = map init_item wi, |
|
421 Relate= map init_item re}:item ppc; |
|
422 fun itemppc2str ({Given=Given,Where=Where, |
|
423 Find=Find,With=With,Relate=Relate}:item ppc)= |
|
424 ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^ |
|
425 ",Where=" ^ ((strs2str' o (map item2str)) Where) ^ |
|
426 ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^ |
|
427 ",With =" ^ ((strs2str' o (map item2str)) With ) ^ |
|
428 ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}"); |
|
429 |
|
430 fun de_item (Correct x) = x |
|
431 | de_item (SyntaxE x) = x |
|
432 | de_item (TypeE x) = x |
|
433 | de_item (False x) = x |
|
434 | de_item (Incompl x) = x |
|
435 | de_item (Superfl x) = x |
|
436 | de_item (Missing x) = x; |
|
437 val empty_ppc ={Given = [], |
|
438 Where= [], |
|
439 Find = [], |
|
440 With = [], |
|
441 Relate= []}:item ppc; |
|
442 val empty_ppc_ct' ={Given = [], |
|
443 Where = [], |
|
444 Find = [], |
|
445 With = [], |
|
446 Relate= []}:cterm' ppc; |
|
447 |
|
448 |
|
449 datatype match = |
|
450 Matches of pblID * item ppc |
|
451 | NoMatch of pblID * item ppc; |
|
452 fun match2str (Matches (pI, ppc)) = |
|
453 "Matches ("^(strs2str pI)^", "^(itemppc2str ppc)^")" |
|
454 | match2str(NoMatch (pI, ppc)) = |
|
455 "NoMatch ("^(strs2str pI)^", "^(itemppc2str ppc)^")"; |
|
456 fun matchs2str ms = (strs2str o (map match2str)) ms; |
|
457 fun pblID_of_match (Matches (pI,_)) = pI |
|
458 | pblID_of_match (NoMatch (pI,_)) = pI; |
|
459 |
|
460 |
|
461 (*. the refined pbt is the last_element Matches in the list .*) |
|
462 fun is_matches (Matches _) = true |
|
463 | is_matches _ = false; |
|
464 fun matches_pblID (Matches (pI,_)) = pI; |
|
465 fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms) |
|
466 handle _ => []:pblID; |
|
467 |
|
468 fun ts_in (Cor ((_,ts),_)) = ts |
|
469 | ts_in (Syn (c)) = [] |
|
470 | ts_in (Typ (c)) = [] |
|
471 | ts_in (Inc ((_,ts),_)) = ts |
|
472 | ts_in (Sup (_,ts)) = ts |
|
473 | ts_in (Mis _) = []; |
|
474 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s; |
|
475 val unique = (term_of o the o (parse Real.thy)) "UnIqE_tErM"; |
|
476 fun d_in (Cor ((d,_),_)) = d |
|
477 | d_in (Syn (c)) = (writeln("*** d_in: Syn ("^c^")"); unique) |
|
478 | d_in (Typ (c)) = (writeln("*** d_in: Syn ("^c^")"); unique) |
|
479 | d_in (Inc ((d,_),_)) = d |
|
480 | d_in (Sup (d,_)) = d |
|
481 | d_in (Mis (d,_)) = d; |
|
482 |
|
483 |
|
484 |
|
485 (* val pre = t; |
|
486 (eval_true' "Isac.thy" "eval_rls" pre) handle e => print_exn e; |
|
487 *) |
|
488 |
|
489 (*. check a predicate and make it an item .*) |
|
490 (* val pre::_ = pres'; |
|
491 *) |
|
492 fun chkpre2item prls pre = |
|
493 if eval_true (assoc_thy "Isac.thy") (*for Pattern.match *) |
|
494 [pre] prls (*pre parsed, prls.thy*) |
|
495 then (true , Correct (term2str pre)) |
|
496 else (false , False (term2str pre)); |
|
497 |
|
498 (*. check preconditions, make them items, return true for all true .*) |
|
499 fun check_preconds' _ [] _ _ = ([], true) |
|
500 (* val pres = (#where_ o get_pbt) pI'; val mvat = max_vt pbl; |
|
501 |
|
502 val (pres,pbl)=(pre,itms); |
|
503 *) |
|
504 | check_preconds' prls pres pbl mvat = |
|
505 let val env = mk_env pbl; |
|
506 val pres' = map (subst_atomic env) pres; |
|
507 val pres'' = map (chkpre2item prls) pres'; |
|
508 in (map snd pres'', foldl and_ (true, map fst pres'')) end; |
|
509 (* |
|
510 val [t] = pres'; |
|
511 term2str t; |
|
512 chkpre2item t; |
|
513 *) |
|
514 |
|
515 |
|
516 fun check_preconds thy prls pres pbl = |
|
517 check_preconds' prls pres pbl (max_vt pbl); |
|
518 (* run test-root-equ-sml until nxt=Add_Find "solutions L")... |
|
519 |
|
520 val ppp = hd pres'; |
|
521 val ppp = (term_of o the o (parse thy)) "matches (a=b) (x=#0)"; |
|
522 |
|
523 eval_matches "" "" ppp thy; |
|
524 eval_true' "Isac.thy" "eval_rls" ppp; |
|
525 |
|
526 *) |
|
527 |
|
528 (*----------------------------24.3.02: done too much----- |
|
529 (**. copy the already input items from probl to meth (in PblObj): |
|
530 for each item in met search the related one in pbl, |
|
531 items not found in probl are (1) inserted as 'untouched' (0,...), |
|
532 and (2) completed from oris (via max_vt) |
|
533 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ "uberkomplett 21.2.02 ------------ .**) |
|
534 (* val (pbl, met) = (itms, ppc); |
|
535 *) |
|
536 fun copy_pbl thy oris pbl met = |
|
537 let val vt = max_vt pbl; |
|
538 fun vt_and_dsc d' ((i,v,f,d,ts):ori) = |
|
539 vt mem v andalso d'= d |
|
540 fun cpy its [] (f, (d, id)) = |
|
541 if length its = 0 (*no dsc found in pbl*) |
|
542 then case find_first (vt_and_dsc d) oris |
|
543 of Some (i,v,_,_,ts) => |
|
544 [(i,v,true,f, Cor ((d,ts), (id,pbl_ids' thy d ts)))] |
|
545 | None => [(0,[],false,f,Mis (d, id))] |
|
546 else its |
|
547 | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) = |
|
548 if d = d_in itm_ andalso i<>0 (*already touched by user*) |
|
549 then cpy (its @ [it]) itms pb else cpy its itms pb; |
|
550 in ((flat o (map (cpy [] pbl))) met):itm list end; |
|
551 |
|
552 |
|
553 (**. copy the already input items from probl to meth (in PblObj): |
|
554 for each item in met search the related one in pbl, |
|
555 items not found in probl are inserted as 'untouched' (0,...) |
|
556 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ "uberkomplett 21.2.02 ------------ .**) |
|
557 (* val (pbl, met) = (itms, ppc); |
|
558 *) |
|
559 fun copy_pbl (pbl:itm list) met = |
|
560 let fun cpy its [] (f, (d, id)) = |
|
561 if length its = 0 (*no dsc found in pbl*) |
|
562 then [(0,[],false,f,Mis (d, id))] |
|
563 else its |
|
564 | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) = |
|
565 if d = d_in itm_ andalso i<>0 (*already touched by user*) |
|
566 then cpy (its @ [it]) itms pb else cpy its itms pb; |
|
567 in ((flat o (map (cpy [] pbl))) met):itm list end; |
|
568 |
|
569 |
|
570 (**. copy the already input items from probl to meth (in PblObj): |
|
571 for each item in met search the related one in pbl |
|
572 (missing items are requested by nxt_spec) .**) |
|
573 (* val (pbl, met) = (itms, ppc); |
|
574 *) |
|
575 fun copy_pbl (pbl:itm list) met = |
|
576 let fun cpy its [] (f, (d, id)) = its |
|
577 | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) = |
|
578 if d = d_in itm_ andalso i<>0 (*already touched by user*) |
|
579 then cpy (its @ [it]) itms pb |
|
580 else cpy its itms pb; |
|
581 in ((flat o (map (cpy [] pbl))) met):itm list end; |
|
582 |
|
583 (*. copy pbt to met (in Specify_Method) |
|
584 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) => |
|
585 (2) filter (dsc(pbt) = dsc(oris)) oris; -> newitms; |
|
586 (3) pbt @ newitms .*) |
|
587 (* val (pbl, met) = (itms, pbt); |
|
588 *) |
|
589 fun copy_pbl (pbl:itm list) met oris = |
|
590 let fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_; |
|
591 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of |
|
592 Some _ => false | None => true; |
|
593 (*1*)val mis = ((map (cons2 (fst, fst o snd))) o (filter (notmem pbl))) met; |
|
594 |
|
595 fun eqdsc_ori d ((_,_,_,d',_):ori) = d = d'; |
|
596 fun ori2itmMis f ((i,v,_,d,ts):ori) = (i,v,false,f,Mis (d,ts)):itm; |
|
597 fun oris2itms oris mis1 = ((map (ori2itmMis (fst mis1))) |
|
598 o (filter ((eqdsc_ori o snd) mis1))) oris; |
|
599 val news = (flat o (map (oris2itms oris))) mis; |
|
600 in pbl @ news end; |
|
601 ----------------------------24.3.02: done too much-----*) |
|
602 |
|
603 |
|
604 |
|
605 |
|
606 |
|
607 |
|
608 (* ---------------------------------------------NOT UPTODATE !!! 4.9.01 |
|
609 eval test-maximum.sml until Specify_Method ... |
|
610 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI)),...} = get_obj I pt []; |
|
611 val met = (#ppc o get_met) mI; |
|
612 val (m::_) = met; |
|
613 cpy [] pbl m; |
|
614 [((1,[1,2,3],true,"#Given",Cor ((Const #,[#]),[])), |
|
615 [([1,2,3],Const ("Descript.fixedValues","bool List.list => Tools.nam"), |
|
616 Free ("fix_","bool List.list"),Const # $ Free # $ Const (#,#))])] |
|
617 : (itm * (vats * term * term * term) list) list |
|
618 |
|
619 upds_envv thy [] (flat eargs); |
|
620 [(1, |
|
621 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
622 (Free ("m_","bool"),[Free (#,#)]), |
|
623 (Free ("vs_","bool List.list"),[# $ # $ (# $ #)]), |
|
624 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]), |
|
625 (2, |
|
626 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
627 (Free ("m_","bool"),[Free (#,#)]), |
|
628 (Free ("vs_","bool List.list"),[# $ # $ (# $ #)]), |
|
629 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]), |
|
630 (3, |
|
631 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
632 (Free ("m_","bool"),[Free (#,#)]), |
|
633 (Free ("vs_","bool List.list"),[# $ # $ (# $ #)])])] : envv |
|
634 *) |
|
635 |
|
636 |
|
637 |