|
1 (* Types and tools for 'modeling' und 'specifying' to be used in |
|
2 modspec.sml. The types are separated from calchead.sml into this file, |
|
3 because some of them are stored in the calc-tree, and thus are required |
|
4 _before_ ctree.sml. |
|
5 author: Walther Neuper |
|
6 (c) due to copyright terms |
|
7 |
|
8 use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*); |
|
9 use"mstools.sml"; |
|
10 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
|
11 10 20 30 40 50 60 70 80 |
|
12 *) |
|
13 |
|
14 signature SPECIFY_TOOLS = |
|
15 sig |
|
16 type envv |
|
17 datatype |
|
18 item = |
|
19 Correct of cterm' |
|
20 | False of cterm' |
|
21 | Incompl of cterm' |
|
22 | Missing of cterm' |
|
23 | Superfl of string |
|
24 | SyntaxE of string |
|
25 | TypeE of string |
|
26 val item2str : item -> string |
|
27 type itm |
|
28 val itm2str_ : Proof.context -> itm -> string |
|
29 datatype |
|
30 itm_ = |
|
31 Cor of (term * term list) * (term * term list) |
|
32 | Inc of (term * term list) * (term * term list) |
|
33 | Mis of term * term |
|
34 | Par of cterm' |
|
35 | Sup of term * term list |
|
36 | Syn of cterm' |
|
37 | Typ of cterm' |
|
38 val itm_2str : itm_ -> string |
|
39 val itm_2str_ : Proof.context -> itm_ -> string |
|
40 val itms2str_ : Proof.context -> itm list -> string |
|
41 type 'a ppc |
|
42 val ppc2str : |
|
43 {Find: string list, With: string list, Given: string list, |
|
44 Where: string list, Relate: string list} -> string |
|
45 datatype |
|
46 match = |
|
47 Matches of pblID * item ppc |
|
48 | NoMatch of pblID * item ppc |
|
49 val match2str : match -> string |
|
50 datatype |
|
51 match_ = |
|
52 Match_ of pblID * (itm list * (bool * term) list) |
|
53 | NoMatch_ |
|
54 val matchs2str : match list -> string |
|
55 type ori |
|
56 val ori2str : ori -> string |
|
57 val oris2str : ori list -> string |
|
58 type preori |
|
59 val preori2str : preori -> string |
|
60 val preoris2str : preori list -> string |
|
61 type penv |
|
62 (* val penv2str_ : Proof.context -> penv -> string *) |
|
63 type vats |
|
64 (*----------------------------------------------------------------------*) |
|
65 val all_ts_in : itm_ list -> term list |
|
66 val check_preconds : |
|
67 'a -> |
|
68 rls -> |
|
69 term list -> itm list -> (bool * term) list |
|
70 val check_preconds' : |
|
71 rls -> |
|
72 term list -> |
|
73 itm list -> 'a -> (bool * term) list |
|
74 (* val chkpre2item : rls -> term -> bool * item *) |
|
75 val pres2str : (bool * term) list -> string |
|
76 (* val evalprecond : rls -> term -> bool * term *) |
|
77 (* val cnt : itm list -> int -> int * int *) |
|
78 val comp_dts : theory -> term * term list -> term |
|
79 val comp_dts' : term * term list -> term |
|
80 val comp_dts'' : term * term list -> string |
|
81 val comp_ts : term * term list -> term |
|
82 val d_in : itm_ -> term |
|
83 val de_item : item -> cterm' |
|
84 val dest_list : term * term list -> term list (* for testing *) |
|
85 val dest_list' : term -> term list |
|
86 val dts2str : term * term list -> string |
|
87 val e_itm : itm |
|
88 (* val e_listBool : term *) |
|
89 (* val e_listReal : term *) |
|
90 val e_ori : ori |
|
91 val e_ori_ : ori |
|
92 val empty_ppc : item ppc |
|
93 (* val empty_ppc_ct' : cterm' ppc *) |
|
94 (* val getval : term * term list -> term * term *) |
|
95 (*val head_precond : |
|
96 domID * pblID * 'a -> |
|
97 term option -> |
|
98 rls -> |
|
99 term list -> |
|
100 itm list -> 'b -> term * (bool * term) list*) |
|
101 (* val init_item : string -> item *) |
|
102 (* val is_matches : match -> bool *) |
|
103 (* val is_matches_ : match_ -> bool *) |
|
104 val is_var : term -> bool |
|
105 (* val item_ppc : |
|
106 string ppc -> item ppc *) |
|
107 val itemppc2str : item ppc -> string |
|
108 (* val matches_pblID : match -> pblID *) |
|
109 val max2 : ('a * int) list -> 'a * int |
|
110 val max_vt : itm list -> int |
|
111 val mk_e : itm_ -> (term * term) list |
|
112 val mk_en : int -> itm -> (term * term) list |
|
113 val mk_env : itm list -> (term * term) list |
|
114 val mkval : 'a -> term list -> term |
|
115 val mkval' : term list -> term |
|
116 (* val pblID_of_match : match -> pblID *) |
|
117 val pbl_ids : Proof.context -> term -> term -> term list |
|
118 val pbl_ids' : 'a -> term -> term list -> term list |
|
119 (* val pen2str : theory -> term * term list -> string *) |
|
120 val penvval_in : itm_ -> term list |
|
121 val refined : match list -> pblID |
|
122 val refined_ : |
|
123 match_ list -> match_ option |
|
124 (* val refined_IDitms : |
|
125 match list -> match option *) |
|
126 val split_dts : 'a -> term -> term * term list |
|
127 val split_dts' : term * term -> term list |
|
128 (* val take_apart : term -> term list *) |
|
129 (* val take_apart_inv : term list -> term *) |
|
130 val ts_in : itm_ -> term list |
|
131 (* val unique : term *) |
|
132 val untouched : itm list -> bool |
|
133 val upd : |
|
134 Proof.context -> |
|
135 (''a * (''b * term list) list) list -> |
|
136 term -> |
|
137 ''b * term -> ''a -> ''a * (''b * term list) list |
|
138 val upd_envv : |
|
139 Proof.context -> |
|
140 envv -> |
|
141 vats -> |
|
142 term -> term -> term -> envv |
|
143 val upd_penv : |
|
144 Proof.context -> |
|
145 (''a * term list) list -> |
|
146 term -> ''a * term -> (''a * term list) list |
|
147 (* val upds_envv : |
|
148 Proof.context -> |
|
149 envv -> |
|
150 (vats * term * term * term) list -> |
|
151 envv *) |
|
152 val vts_cnt : int list -> itm list -> (int * int) list |
|
153 val vts_in : itm list -> int list |
|
154 (* val w_itms2str_ : Proof.context -> itm list -> unit *) |
|
155 end |
|
156 |
|
157 (*----------------------------------------------------------*) |
|
158 structure SpecifyTools : SPECIFY_TOOLS = |
|
159 struct |
|
160 (*----------------------------------------------------------*) |
|
161 val e_listReal = (term_of o the o (parse (theory "Script"))) "[]::(real list)"; |
|
162 val e_listBool = (term_of o the o (parse (theory "Script"))) "[]::(bool list)"; |
|
163 |
|
164 (*.take list-term apart w.r.t. handling elementwise input.*) |
|
165 fun take_apart t = |
|
166 let val elems = isalist2list t |
|
167 in map ((list2isalist (type_of (hd elems))) o single) elems end; |
|
168 (*val t = str2term "[a, b]"; |
|
169 > val ts = take_apart t; writeln (terms2str ts); |
|
170 ["[a]","[b]"] |
|
171 |
|
172 > t = (take_apart_inv o take_apart) t; |
|
173 true*) |
|
174 fun take_apart_inv ts = |
|
175 let val elems = (flat o (map isalist2list)) ts; |
|
176 in list2isalist (type_of (hd elems)) elems end; |
|
177 (*val ts = [str2term "[a]", str2term "[b]"]; |
|
178 > val t = take_apart_inv ts; term2str t; |
|
179 "[a, b]" |
|
180 |
|
181 ts = (take_apart o take_apart_inv) ts; |
|
182 true*) |
|
183 |
|
184 |
|
185 |
|
186 |
|
187 (*.revert split_dts only for ts; compare comp_dts.*) |
|
188 fun comp_ts (d, ts) = |
|
189 if is_list_dsc d |
|
190 then if is_list (hd ts) |
|
191 then if is_unl d |
|
192 then (hd ts) (*e.g. someList [1,3,2]*) |
|
193 else (take_apart_inv ts) |
|
194 (* SML[ [a], [b] ]SML --> [a,b] *) |
|
195 else (hd ts) (*a variable or metavariable for a list*) |
|
196 else (hd ts); |
|
197 (*.revert split_. |
|
198 WN050903 we do NOT know which is from subtheory, description or term; |
|
199 typecheck thus may lead to TYPE-error 'unknown constant'; |
|
200 solution: typecheck with Isac.thy; i.e. arg 'thy' superfluous*) |
|
201 (*fun comp_dts thy (d,[]) = |
|
202 cterm_of (*(sign_of o assoc_thy) "Isac.thy"*) |
|
203 (theory "Isac") |
|
204 (*comp_dts:FIXXME stay with term for efficiency !!!*) |
|
205 (if is_reall_dsc d then (d $ e_listReal) |
|
206 else if is_booll_dsc d then (d $ e_listBool) |
|
207 else d) |
|
208 | comp_dts thy (d,ts) = |
|
209 (cterm_of (*(sign_of o assoc_thy) "Isac.thy"*) |
|
210 (theory "Isac") |
|
211 (*comp_dts:FIXXME stay with term for efficiency !!*) |
|
212 (d $ (comp_ts (d, ts))) |
|
213 handle _ => raise error ("comp_dts: "^(term2str d)^ |
|
214 " $ "^(term2str (hd ts))));*) |
|
215 fun comp_dts thy (d,[]) = |
|
216 (if is_reall_dsc d then (d $ e_listReal) |
|
217 else if is_booll_dsc d then (d $ e_listBool) |
|
218 else d) |
|
219 | comp_dts thy (d,ts) = |
|
220 (d $ (comp_ts (d, ts))) |
|
221 handle _ => raise error ("comp_dts: "^(term2str d)^ |
|
222 " $ "^(term2str (hd ts))); |
|
223 (*25.8.03*) |
|
224 fun comp_dts' (d,[]) = |
|
225 if is_reall_dsc d then (d $ e_listReal) |
|
226 else if is_booll_dsc d then (d $ e_listBool) |
|
227 else d |
|
228 | comp_dts' (d,ts) = (d $ (comp_ts (d, ts))) |
|
229 handle _ => raise error ("comp_dts': "^(term2str d)^ |
|
230 " $ "^(term2str (hd ts))); |
|
231 (*val t = str2term "maximum A"; |
|
232 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
233 val it = "maximum A" : cterm |
|
234 > val t = str2term "fixedValues [r=Arbfix]"; |
|
235 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
236 "fixedValues [r = Arbfix]" |
|
237 > val t = str2term "valuesFor [a]"; |
|
238 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
239 "valuesFor [a]" |
|
240 > val t = str2term "valuesFor [a,b]"; |
|
241 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
242 "valuesFor [a, b]" |
|
243 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"; |
|
244 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
245 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]" |
|
246 > val t = str2term "boundVariable a"; |
|
247 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
248 "boundVariable a" |
|
249 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}"; |
|
250 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
251 "interval {x. 0 <= x & x <= 2 * r}" |
|
252 |
|
253 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; |
|
254 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
255 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))" |
|
256 > val t = str2term "solveFor x"; |
|
257 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
258 "solveFor x" |
|
259 > val t = str2term "errorBound (eps=0)"; |
|
260 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
261 "errorBound (eps = 0)" |
|
262 > val t = str2term "solutions L"; |
|
263 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
264 "solutions L" |
|
265 |
|
266 before 6.5.03: |
|
267 > val t = (term_of o the o (parse thy)) "testdscforlist [#1]"; |
|
268 > val (d,ts) = split_dts t; |
|
269 > comp_dts thy (d,ts); |
|
270 val it = "testdscforlist [#1]" : cterm |
|
271 |
|
272 > val t = (term_of o the o (parse thy)) "(A::real)"; |
|
273 > val (d,ts) = split_dts t; |
|
274 val d = Const ("empty","empty") : term |
|
275 val ts = [Free ("A","RealDef.real")] : term list |
|
276 > val t = (term_of o the o (parse thy)) "[R=(R::real)]"; |
|
277 > val (d,ts) = split_dts t; |
|
278 val d = Const ("empty","empty") : term |
|
279 val ts = [Const # $ Free # $ Free (#,#)] : term list |
|
280 > val t = (term_of o the o (parse thy)) "[#1,#2]"; |
|
281 > val (d,ts) = split_dts t; |
|
282 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED |
|
283 *) |
|
284 |
|
285 (*for input_icalhd 11.03*) |
|
286 fun comp_dts'' (d,[]) = |
|
287 if is_reall_dsc d then term2str (d $ e_listReal) |
|
288 else if is_booll_dsc d then term2str (d $ e_listBool) |
|
289 else term2str d |
|
290 | comp_dts'' (d,ts) = term2str (d $ (comp_ts (d, ts))) |
|
291 handle _ => raise error ("comp_dts'': "^(term2str d)^ |
|
292 " $ "^(term2str (hd ts))); |
|
293 |
|
294 |
|
295 |
|
296 |
|
297 |
|
298 |
|
299 (* this may decompose an object-language isa-list; |
|
300 use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*) |
|
301 fun dest_list' t = if is_list t then isalist2list t else [t]; |
|
302 |
|
303 (*fun is_metavar (Free (str, _)) = |
|
304 if (last_elem o explode) str = "_" then true else false |
|
305 | is_metavar _ = false;*) |
|
306 fun is_var (Free _) = true |
|
307 | is_var _ = false; |
|
308 |
|
309 (*.special handling for lists. ?WN:14.5.03 ??!?*) |
|
310 fun dest_list (d,ts) = |
|
311 let fun dest t = |
|
312 if is_list_dsc d andalso not (is_unl d) |
|
313 andalso not (is_var t) (*..for pbt*) |
|
314 then isalist2list t else [t] |
|
315 in (flat o (map dest)) ts end; |
|
316 |
|
317 |
|
318 (*.decompose an input into description, terms (ev. elems of lists), |
|
319 and the value for the problem-environment; inv to comp_dts .*) |
|
320 (*WN.8.6.03: corrected with minimal effort, |
|
321 fn : theory -> term -> |
|
322 term * description |
|
323 term list * lists decomposed for elementwise input |
|
324 term list pbl_ids not _HERE_: dont know which list-elems input*) |
|
325 fun split_dts thy (t as d $ arg) = |
|
326 if is_dsc d |
|
327 then if is_list_dsc d |
|
328 then if is_list arg |
|
329 then if is_unl d |
|
330 then (d, [arg]) (*e.g. someList [1,3,2]*) |
|
331 else (d, take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*) |
|
332 else (d, [arg]) (*a variable or metavariable for a list*) |
|
333 else (d, [arg]) |
|
334 else (e_term, dest_list' t(*9.01 ???*)) |
|
335 | split_dts thy t = (*either dsc or term*) |
|
336 let val (h,argl) = strip_comb t |
|
337 in if (not o is_dsc) h then (e_term, dest_list' t) |
|
338 else (h, dest_list (h,argl)) |
|
339 end; |
|
340 (* tests see fun comp_dts |
|
341 |
|
342 > val t = str2term "someList []"; |
|
343 > val (_,ts) = split_dts thy t; writeln (terms2str ts); |
|
344 ["[]"] |
|
345 > val t = str2term "valuesFor []"; |
|
346 > val (_,ts) = split_dts thy t; writeln (terms2str ts); |
|
347 ["[]"]*) |
|
348 |
|
349 (*.version returning ts only.*) |
|
350 fun split_dts' (d, arg) = |
|
351 if is_dsc d |
|
352 then if is_list_dsc d |
|
353 then if is_list arg |
|
354 then if is_unl d |
|
355 then ([arg]) (*e.g. someList [1,3,2]*) |
|
356 else (take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*) |
|
357 else ([arg]) (*a variable or metavariable for a list*) |
|
358 else ([arg]) |
|
359 else (dest_list' arg(*9.01 ???*)) |
|
360 | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*) |
|
361 let val (h,argl) = strip_comb t |
|
362 in if (not o is_dsc) h then (dest_list' t) |
|
363 else (dest_list (h,argl)) |
|
364 end; |
|
365 |
|
366 |
|
367 |
|
368 |
|
369 |
|
370 (*27.8.01: problem-environment |
|
371 WN.6.5.03: FIXXME reconsider if penv is worth the effort -- |
|
372 -- just rerun a whole expl with num/var may show the same ?! |
|
373 WN.9.5.03: penv-concept stalled, immediately generate script env ! |
|
374 but [#0, epsilon] only outcommented for eventual reconsideration |
|
375 *) |
|
376 type penv = (term (*err_*) |
|
377 * (term list) (*[#0, epsilon] 9.5.03 outcommented*) |
|
378 ) list; |
|
379 fun pen2str ctxt (t, ts) = |
|
380 pair2str(Syntax.string_of_term ctxt t, |
|
381 (strs2str' o map (Syntax.string_of_term ctxt)) ts); |
|
382 fun penv2str_ thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv; |
|
383 |
|
384 (* |
|
385 9.5.03: still unused, but left for eventual future development*) |
|
386 type envv = (int * penv) list; (*over variants*) |
|
387 |
|
388 (*. 14.9.01: not used after putting penv-values into itm_ |
|
389 make the result of split_* a value of problem-environment .*) |
|
390 fun mkval dsc [] = raise error "mkval called with []" |
|
391 | mkval dsc [t] = t |
|
392 | mkval dsc ts = list2isalist ((type_of o hd) ts) ts; |
|
393 (*WN.12.12.03*) |
|
394 fun mkval' x = mkval e_term x; |
|
395 |
|
396 |
|
397 |
|
398 (*. get the constant value from a penv .*) |
|
399 fun getval (id, values) = |
|
400 case values of |
|
401 [] => raise error ("penv_value: no values in '"^ |
|
402 (Syntax.string_of_term (thy2ctxt' "Tools") id)) |
|
403 | [v] => (id, v) |
|
404 | (v1::v2::_) => (case v1 of |
|
405 Const ("Script.Arbfix",_) => (id, v2) |
|
406 | _ => (id, v1)); |
|
407 (* |
|
408 val e_ = (term_of o the o (parse thy)) "e_::bool"; |
|
409 val ev = (term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0"; |
|
410 val v_ = (term_of o the o (parse thy)) "v_"; |
|
411 val vv = (term_of o the o (parse thy)) "x"; |
|
412 val r_ = (term_of o the o (parse thy)) "err_::bool"; |
|
413 val rv1 = (term_of o the o (parse thy)) "#0"; |
|
414 val rv2 = (term_of o the o (parse thy)) "eps"; |
|
415 |
|
416 val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv; |
|
417 map getval penv; |
|
418 [(Free ("e_","bool"), |
|
419 Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#0","RealDef.real")), |
|
420 (Free ("v_","RealDef.real"),Free ("x","RealDef.real")), |
|
421 (Free ("err_","bool"),Free ("#0","RealDef.real"))] : (term * term) list |
|
422 *) |
|
423 |
|
424 |
|
425 (*23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc |
|
426 (1) kinds of itms: |
|
427 (1.1) untouched: for modeling only dsc displayed(impossible after match_itms) |
|
428 =(presently) Mis (? should be Inc initially, and Mis after match_itms?) |
|
429 (1.2) Syn,Typ,Sup: not related to oris |
|
430 Syn, Typ (presently) should be accepted in appl_add (instead Error') |
|
431 Sup (presently) should be accepted in appl_add (instead Error') |
|
432 _could_ be w.r.t current vat (and then _is_ related to vat |
|
433 Mis should _not_ be made Inc ((presently, by appl_add & match_itms) |
|
434 - dsc in itm_ is timeconsuming -- keep id for respective queries ? |
|
435 - order of items in ppc should be stable w.r.t order of itms |
|
436 |
|
437 - stepwise input of itms --- match_itms (in one go) ..not coordinated |
|
438 - unify code |
|
439 - match_itms / match_itms_oris ..2 versions ?! |
|
440 (fast, for refine / slow, for modeling) |
|
441 |
|
442 - clarify: efficiency <--> simplicity !!! |
|
443 ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc |
|
444 | take int for perserving order of item ppc in itms |
|
445 | make all(!?) handling of itms stable against reordering(?) |
|
446 | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???) |
|
447 -"- "#undef" ?= not touched ?= (id,..) |
|
448 ----------------------------------------------------------------- |
|
449 27.3.02: |
|
450 def: type pbt = (field, (dsc, pid)) |
|
451 |
|
452 (1) fmz + pbt -> oris |
|
453 (2) input + oris -> itm |
|
454 (3) match_itms : schnell(?) f"ur refine |
|
455 match_itms_oris : r"uckmeldung f"ur item ppc |
|
456 |
|
457 (1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid) |
|
458 ---------- ^^^^^ --- dh. pbt meist als argument zu viel !!! |
|
459 |
|
460 (3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht; |
|
461 wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????: |
|
462 (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ???? |
|
463 (b) |
|
464 *) |
|
465 |
|
466 |
|
467 |
|
468 |
|
469 (*the internal representation of a models' item |
|
470 |
|
471 4.9.01: not consistent: |
|
472 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation |
|
473 (involves 'is_error'); |
|
474 bool in itm really necessary ???*) |
|
475 datatype itm_ = |
|
476 Cor of (term * (* description *) |
|
477 (term list)) * (* for list: elem-wise input *) |
|
478 (*split_dts <-> comp_dts*) |
|
479 (term * (term list)) (* elem of penv *) |
|
480 (*9.5.03: ---- is already for script -- penv delayed to future*) |
|
481 | Syn of cterm' |
|
482 | Typ of cterm' |
|
483 | Inc of (term * (term list)) * (term * (term list)) (*lists, |
|
484 + init_pbl WN.11.03 FIXXME: empty penv .. bad |
|
485 init_pbl should return Mis !!!*) |
|
486 | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*) |
|
487 | Mis of (term * term) (* after re-specification pbt-item not found |
|
488 in pbl: only dsc, pid_*) |
|
489 | Par of cterm'; (*internal state from fun parsitm*) |
|
490 |
|
491 type vats = int list; (*variants in formalizations*) |
|
492 |
|
493 (*.data-type for working on pbl/met-ppc: |
|
494 in pbl initially holds descriptions (only) for user guidance.*) |
|
495 type itm = |
|
496 int * (* id =0 .. untouched - descript (only) from init |
|
497 23.3.02: seems to correspond to ori (fun insert_ppc) |
|
498 <> maintain order in item ppc?*) |
|
499 vats * (* variants - copy from ori *) |
|
500 bool * (* input on this item is not/complete *) |
|
501 string * (* #Given | #Find | #Relate *) |
|
502 itm_; (* *) |
|
503 (* use"ME/sequent.sml"; |
|
504 *) |
|
505 val e_itm = (0,[],false,"e_itm",Syn"e_itm"):itm; |
|
506 (*in CalcTree/Subproblem an 'untouched' model is created |
|
507 FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*) |
|
508 fun untouched (itms: itm list) = |
|
509 foldl and_ (true ,map ((curry op= 0) o #1) itms); |
|
510 (*> untouched []; |
|
511 val it = true : bool |
|
512 > untouched [e_itm]; |
|
513 val it = true : bool |
|
514 > untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")]; |
|
515 val it = false : bool*) |
|
516 |
|
517 |
|
518 |
|
519 |
|
520 |
|
521 (* find most frequent variant v in itms *) |
|
522 |
|
523 fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list); |
|
524 |
|
525 fun cnt itms v = (v,(length o (filter (curry op= v)) o |
|
526 flat o (map #2)) (itms:itm list)); |
|
527 fun vts_cnt vts itms = map (cnt itms) vts; |
|
528 fun max2 [] = raise error "max2 of []" |
|
529 | max2 (y::ys) = |
|
530 let fun mx (a,x) [] = (a,x) |
|
531 | mx (a,x) ((b,y)::ys) = |
|
532 if x < y then mx (b,y) ys else mx (a,x) ys; |
|
533 in mx y ys end; |
|
534 |
|
535 (*. find the variant with most items already input .*) |
|
536 fun max_vt itms = |
|
537 let val vts = (vts_cnt (vts_in itms)) itms; |
|
538 in if vts = [] then 0 else (fst o max2) vts end; |
|
539 |
|
540 |
|
541 (* TODO ev. make more efficient by avoiding flat *) |
|
542 fun mk_e (Cor (_, iv)) = [getval iv] |
|
543 | mk_e (Syn _) = [] |
|
544 | mk_e (Typ _) = [] |
|
545 | mk_e (Inc (_, iv)) = [getval iv] |
|
546 | mk_e (Sup _) = [] |
|
547 | mk_e (Mis _) = []; |
|
548 fun mk_en vt ((i,vts,b,f,itm_):itm) = |
|
549 if member op = vts vt then mk_e itm_ else []; |
|
550 (*. extract the environment from an item list; |
|
551 takes the variant with most items .*) |
|
552 fun mk_env itms = |
|
553 let val vt = max_vt itms |
|
554 in (flat o (map (mk_en vt))) itms end; |
|
555 |
|
556 |
|
557 |
|
558 (*. example as provided by an author, complete w.r.t. pbt specified |
|
559 not touched by any user action .*) |
|
560 type ori = (int * (* id: 10.3.00ff impl. only <>0 .. touched |
|
561 21.3.02: insert_ppc needs it ! ?:purpose maintain |
|
562 order in item ppc ???*) |
|
563 vats * (* variants 21.3.02: related to pbt..discard ?*) |
|
564 string * (* #Given | #Find | #Relate 21.3.02: discard ?*) |
|
565 term * (* description *) |
|
566 term list (* isalist2list t | [t] *) |
|
567 ); |
|
568 val e_ori_ = (0,[],"",e_term,[e_term]):ori; |
|
569 val e_ori = (0,[],"",e_term,[e_term]):ori; |
|
570 |
|
571 fun ori2str ((i,vs,fi,t,ts):ori) = |
|
572 "("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^ |
|
573 (term2str t)^", "^((strs2str o (map term2str)) ts)^")"; |
|
574 val oris2str = |
|
575 let val s = !show_types |
|
576 val _ = show_types:= true |
|
577 val str = (strs2str' o (map (linefeed o ori2str))) |
|
578 val _ = show_types:= s |
|
579 in str end; |
|
580 |
|
581 (*.an or without leading integer.*) |
|
582 type preori = (vats * |
|
583 string * |
|
584 term * |
|
585 term list); |
|
586 fun preori2str ((vs,fi,t,ts):preori) = |
|
587 "("^((strs2str o (map string_of_int)) vs)^", "^fi^", "^ |
|
588 (term2str t)^", "^((strs2str o (map term2str)) ts)^")"; |
|
589 val preoris2str = (strs2str' o (map (linefeed o preori2str))); |
|
590 |
|
591 (*. given the input value (from split_dts) |
|
592 make the value in a problem-env according to description-type .*) |
|
593 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*) |
|
594 fun pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v = |
|
595 if is_list v |
|
596 then [v] (*eg. [r=Arbfix]*) |
|
597 else (case v of (*eg. eps=#0*) |
|
598 (Const ("op =",_) $ l $ r) => [r,l] |
|
599 | _ => raise error ("pbl_ids Tools.nam: no equality " |
|
600 ^(Syntax.string_of_term ctxt v))) |
|
601 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v] |
|
602 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v] |
|
603 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v] |
|
604 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v] |
|
605 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v] |
|
606 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v] |
|
607 | pbl_ids ctxt _ v = raise error ("pbl_ids: not implemented for " |
|
608 ^(Syntax.string_of_term ctxt v)); |
|
609 (* |
|
610 val t as t1 $ t2 = str2term "antiDerivativeName M_b"; |
|
611 pbl_ids ctxt t1 t2; |
|
612 |
|
613 val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; |
|
614 val (d,argl) = strip_comb t; |
|
615 is_dsc d; (*see split_dts*) |
|
616 dest_list (d,argl); |
|
617 val (_ $ v) = t; |
|
618 is_list v; |
|
619 pbl_ids ctxt d v; |
|
620 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $ |
|
621 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List.. |
|
622 |
|
623 val (dsc,vl) = (split_dts o term_of o the o (parse thy)) "solveFor x"; |
|
624 val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term |
|
625 val vl = Free ("x","RealDef.real") : term |
|
626 |
|
627 val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_"; |
|
628 pbl_ids ctxt dsc vl; |
|
629 val it = [Free ("x","RealDef.real")] : term list |
|
630 |
|
631 val (dsc,vl) = (split_dts o term_of o the o(parse thy)) |
|
632 "errorBound (eps=#0)"; |
|
633 val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_"; |
|
634 pbl_ids ctxt dsc vl; |
|
635 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *) |
|
636 |
|
637 (*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!)) |
|
638 make the value in a problem-env according to description-type .*) |
|
639 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*) |
|
640 fun pbl_ids' (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) vs = |
|
641 (case vs of |
|
642 [] => raise error ("pbl_ids' Tools.nam called with []") |
|
643 | [t] => (case t of (*eg. eps=#0*) |
|
644 (Const ("op =",_) $ l $ r) => [r,l] |
|
645 | _ => raise error ("pbl_ids' Tools.nam: no equality " |
|
646 ^(Syntax.string_of_term (thy2ctxt' "Isac")t))) |
|
647 | vs' => vs (*14.9.01: ???TODO *)) |
|
648 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs |
|
649 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs |
|
650 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs |
|
651 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs |
|
652 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))vs = vs |
|
653 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))vs = vs |
|
654 | pbl_ids' _ vs = |
|
655 raise error ("pbl_ids': not implemented for " |
|
656 ^(terms2str vs)); |
|
657 (*9.5.03 penv postponed: pbl_ids'*) |
|
658 fun pbl_ids' thy d vs = [comp_ts (d, vs)]; |
|
659 |
|
660 |
|
661 (*14.9.01: not used after putting values for penv into itm_ |
|
662 WN.5.5.03: used in upd .. upd_envv*) |
|
663 fun upd_penv ctxt penv dsc (id, vl) = |
|
664 (writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; |
|
665 writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; |
|
666 writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; |
|
667 overwrite (penv, (id, pbl_ids ctxt dsc vl)) |
|
668 ); |
|
669 (* |
|
670 val penv = []; |
|
671 val (dsc,vl) = (split_did o term_of o the o (parse thy)) "solveFor x"; |
|
672 val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_"; |
|
673 val penv = upd_penv thy penv dsc (id, vl); |
|
674 [(Free ("v_","RealDef.real"), |
|
675 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")])] |
|
676 : (term * term list) list |
|
677 |
|
678 val (dsc,vl) = (split_did o term_of o the o(parse thy))"errorBound (eps=#0)"; |
|
679 val (dsc,id) = (split_did o term_of o the o(parse thy))"errorBound err_"; |
|
680 upd_penv thy penv dsc (id, vl); |
|
681 [(Free ("v_","RealDef.real"), |
|
682 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")]), |
|
683 (Free ("err_","bool"), |
|
684 [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")])] |
|
685 : (term * term list) list ^.........!!!! |
|
686 *) |
|
687 |
|
688 (*WN.9.5.03: not reconsidered; looks strange !!!*) |
|
689 fun upd thy envv dsc (id, vl) i = |
|
690 let val penv = case assoc (envv, i) of |
|
691 SOME e => e |
|
692 | NONE => []; |
|
693 val penv' = upd_penv thy penv dsc (id, vl); |
|
694 in (i, penv') end; |
|
695 (* |
|
696 val i = 2; |
|
697 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv; |
|
698 val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b"; |
|
699 val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_"; |
|
700 upd thy envv dsc (id, vl) i; |
|
701 val it = (2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])]) |
|
702 : int * (term * term list) list*) |
|
703 |
|
704 |
|
705 (*14.9.01: not used after putting pre-penv into itm_*) |
|
706 fun upd_envv thy (envv:envv) (vats:vats) dsc id vl = |
|
707 let val vats = if length vats = 0 |
|
708 then (*unknown id to _all_ variants*) |
|
709 if length envv = 0 then [1] |
|
710 else (intsto o length) envv |
|
711 else vats |
|
712 fun isin vats (i,_) = member op = vats i; |
|
713 val envs_notin_vat = filter_out (isin vats) envv; |
|
714 in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end; |
|
715 (* |
|
716 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv; |
|
717 |
|
718 val vats = [2] |
|
719 val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b"; |
|
720 val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_"; |
|
721 val envv = upd_envv thy envv vats dsc id vl; |
|
722 val envv = [(2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])] |
|
723 : (int * (term * term list) list) list |
|
724 |
|
725 val vats = [1,2,3]; |
|
726 val (dsc,vl) = (split_did o term_of o the o(parse thy))"maximum A"; |
|
727 val (dsc,id) = (split_did o term_of o the o(parse thy))"maximum m_"; |
|
728 upd_envv thy envv vats dsc id vl; |
|
729 [(1,[(Free ("m_","bool"),[Free ("A","bool")])]), |
|
730 (2, |
|
731 [(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")]), |
|
732 (Free ("m_","bool"),[Free ("A","bool")])]), |
|
733 (3,[(Free ("m_","bool"),[Free ("A","bool")])])] |
|
734 : (int * (term * term list) list) list |
|
735 |
|
736 |
|
737 val env = []:envv; |
|
738 val (d,ts) = (split_dts o term_of o the o (parse thy)) |
|
739 "fixedValues [r=Arbfix]"; |
|
740 val (_,id) = (split_did o term_of o the o (parse thy))"fixedValues fix_"; |
|
741 val vats = [1,2,3]; |
|
742 val env = upd_envv thy env vats d id (mkval ts); |
|
743 *) |
|
744 |
|
745 (*. update envv by folding from a list of arguments .*) |
|
746 fun upds_envv thy envv [] = envv |
|
747 | upds_envv thy envv ((vs, dsc, id, vl)::ps) = |
|
748 upds_envv thy (upd_envv thy envv vs dsc id vl) ps; |
|
749 (* eval test-maximum.sml until Specify_Method ... |
|
750 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt []; |
|
751 val met = (#ppc o get_met) mI; |
|
752 |
|
753 val envv = []; |
|
754 val eargs = flat eargs; |
|
755 val (vs, dsc, id, vl) = hd eargs; |
|
756 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
757 |
|
758 val (vs, dsc, id, vl) = hd (tl eargs); |
|
759 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
760 |
|
761 val (vs, dsc, id, vl) = hd (tl (tl eargs)); |
|
762 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
763 |
|
764 val (vs, dsc, id, vl) = hd (tl (tl (tl eargs))); |
|
765 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
766 [(1, |
|
767 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
768 (Free ("m_","bool"),[Free (#,#)]), |
|
769 (Free ("vs_","bool List.list"),[# $ # $ Const #]), |
|
770 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]), |
|
771 (2, |
|
772 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
773 (Free ("m_","bool"),[Free (#,#)]), |
|
774 (Free ("vs_","bool List.list"),[# $ # $ Const #]), |
|
775 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]), |
|
776 (3, |
|
777 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
778 (Free ("m_","bool"),[Free (#,#)]), |
|
779 (Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *) |
|
780 |
|
781 (*for _output_ of the items of a Model*) |
|
782 datatype item = |
|
783 Correct of cterm' (*labels a correct formula (type cterm')*) |
|
784 | SyntaxE of string (**) |
|
785 | TypeE of string (**) |
|
786 | False of cterm' (*WN050618 notexistent in itm_: only used in Where*) |
|
787 | Incompl of cterm' (**) |
|
788 | Superfl of string (**) |
|
789 | Missing of cterm'; |
|
790 fun item2str (Correct s) ="Correct " ^ s |
|
791 | item2str (SyntaxE s) ="SyntaxE " ^ s |
|
792 | item2str (TypeE s) ="TypeE " ^ s |
|
793 | item2str (False s) ="False " ^ s |
|
794 | item2str (Incompl s) ="Incompl " ^ s |
|
795 | item2str (Superfl s) ="Superfl " ^ s |
|
796 | item2str (Missing s) ="Missing " ^ s; |
|
797 (*make string for error-msgs*) |
|
798 fun itm_2str_ ctxt (Cor ((d,ts), penv)) = |
|
799 "Cor " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ," |
|
800 ^ pen2str ctxt penv |
|
801 | itm_2str_ ctxt (Syn c) = "Syn " ^ c |
|
802 | itm_2str_ ctxt (Typ c) = "Typ " ^ c |
|
803 | itm_2str_ ctxt (Inc ((d,ts), penv)) = |
|
804 "Inc " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ," |
|
805 ^ pen2str ctxt penv |
|
806 | itm_2str_ ctxt (Sup (d,ts)) = |
|
807 "Sup " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) |
|
808 | itm_2str_ ctxt (Mis (d,pid))= |
|
809 "Mis "^ Syntax.string_of_term ctxt d ^ |
|
810 " "^ Syntax.string_of_term ctxt pid |
|
811 | itm_2str_ ctxt (Par s) = "Trm "^s; |
|
812 fun itm_2str t = itm_2str_ (thy2ctxt' "Isac") t; |
|
813 fun itm2str_ ctxt ((i,is,b,s,itm_):itm) = |
|
814 "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^ |
|
815 s^" ,"^(itm_2str_ ctxt itm_)^")"; |
|
816 fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms); |
|
817 fun w_itms2str_ ctxt itms = writeln (itms2str_ ctxt itms); |
|
818 |
|
819 fun init_item str = SyntaxE str; |
|
820 |
|
821 |
|
822 |
|
823 |
|
824 type 'a ppc = |
|
825 {Given : 'a list, |
|
826 Where: 'a list, |
|
827 Find : 'a list, |
|
828 With : 'a list, |
|
829 Relate: 'a list}; |
|
830 fun ppc2str {Given=Given,Where=Where,Find=Find,With=With,Relate=Relate}= |
|
831 ("{Given =" ^ (strs2str Given ) ^ |
|
832 ",Where=" ^ (strs2str Where) ^ |
|
833 ",Find =" ^ (strs2str Find ) ^ |
|
834 ",With =" ^ (strs2str With ) ^ |
|
835 ",Relate=" ^ (strs2str Relate) ^ "}"); |
|
836 |
|
837 |
|
838 |
|
839 |
|
840 fun item_ppc ({Given = gi,Where= wh, |
|
841 Find = fi,With = wi,Relate= re}: string ppc) = |
|
842 {Given = map init_item gi,Where= map init_item wh, |
|
843 Find = map init_item fi,With = map init_item wi, |
|
844 Relate= map init_item re}:item ppc; |
|
845 fun itemppc2str ({Given=Given,Where=Where, |
|
846 Find=Find,With=With,Relate=Relate}:item ppc)= |
|
847 ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^ |
|
848 ",Where=" ^ ((strs2str' o (map item2str)) Where) ^ |
|
849 ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^ |
|
850 ",With =" ^ ((strs2str' o (map item2str)) With ) ^ |
|
851 ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}"); |
|
852 |
|
853 fun de_item (Correct x) = x |
|
854 | de_item (SyntaxE x) = x |
|
855 | de_item (TypeE x) = x |
|
856 | de_item (False x) = x |
|
857 | de_item (Incompl x) = x |
|
858 | de_item (Superfl x) = x |
|
859 | de_item (Missing x) = x; |
|
860 val empty_ppc ={Given = [], |
|
861 Where= [], |
|
862 Find = [], |
|
863 With = [], |
|
864 Relate= []}:item ppc; |
|
865 val empty_ppc_ct' ={Given = [], |
|
866 Where = [], |
|
867 Find = [], |
|
868 With = [], |
|
869 Relate= []}:cterm' ppc; |
|
870 |
|
871 |
|
872 datatype match = |
|
873 Matches of pblID * item ppc |
|
874 | NoMatch of pblID * item ppc; |
|
875 fun match2str (Matches (pI, ppc)) = |
|
876 "Matches ("^(strs2str pI)^", "^(itemppc2str ppc)^")" |
|
877 | match2str(NoMatch (pI, ppc)) = |
|
878 "NoMatch ("^(strs2str pI)^", "^(itemppc2str ppc)^")"; |
|
879 fun matchs2str ms = (strs2str o (map match2str)) ms; |
|
880 fun pblID_of_match (Matches (pI,_)) = pI |
|
881 | pblID_of_match (NoMatch (pI,_)) = pI; |
|
882 |
|
883 (*10.03 for Refine_Problem*) |
|
884 datatype match_ = |
|
885 Match_ of pblID * ((itm list) * ((bool * term) list)) |
|
886 | NoMatch_; |
|
887 |
|
888 (*. the refined pbt is the last_element Matches in the list .*) |
|
889 fun is_matches (Matches _) = true |
|
890 | is_matches _ = false; |
|
891 fun matches_pblID (Matches (pI,_)) = pI; |
|
892 fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms) |
|
893 handle _ => []:pblID; |
|
894 fun refined_IDitms ms = ((find_first is_matches) o rev) ms; |
|
895 |
|
896 (*. the refined pbt is the last_element Matches in the list, |
|
897 for Refine_Problem, tryrefine .*) |
|
898 fun is_matches_ (Match_ _) = true |
|
899 | is_matches_ _ = false; |
|
900 fun refined_ ms = ((find_first is_matches_) o rev) ms; |
|
901 |
|
902 |
|
903 fun ts_in (Cor ((_,ts),_)) = ts |
|
904 | ts_in (Syn (c)) = [] |
|
905 | ts_in (Typ (c)) = [] |
|
906 | ts_in (Inc ((_,ts),_)) = ts |
|
907 | ts_in (Sup (_,ts)) = ts |
|
908 | ts_in (Mis _) = []; |
|
909 (*WN050629 unused*) |
|
910 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s; |
|
911 val unique = (term_of o the o (parse (theory "Real"))) "UnIqE_tErM"; |
|
912 fun d_in (Cor ((d,_),_)) = d |
|
913 | d_in (Syn (c)) = (writeln("*** d_in: Syn ("^c^")"); unique) |
|
914 | d_in (Typ (c)) = (writeln("*** d_in: Typ ("^c^")"); unique) |
|
915 | d_in (Inc ((d,_),_)) = d |
|
916 | d_in (Sup (d,_)) = d |
|
917 | d_in (Mis (d,_)) = d; |
|
918 |
|
919 fun dts2str (d,ts) = pair2str (term2str d, terms2str ts); |
|
920 fun penvval_in (Cor ((d,_),(_,ts))) = [comp_ts (d,ts)] |
|
921 | penvval_in (Syn (c)) = (writeln("*** penvval_in: Syn ("^c^")"); []) |
|
922 | penvval_in (Typ (c)) = (writeln("*** penvval_in: Typ ("^c^")"); []) |
|
923 | penvval_in (Inc (_,(_,ts))) = ts |
|
924 | penvval_in (Sup dts) = (writeln("*** penvval_in: Sup "^(dts2str dts)); []) |
|
925 | penvval_in (Mis (d,t)) = (writeln("*** penvval_in: Mis "^ |
|
926 (pair2str(term2str d, term2str t))); []); |
|
927 |
|
928 |
|
929 (*. check a predicate labelled with indication of incomplete substitution; |
|
930 rls -> (*for eval_true*) |
|
931 bool * (*have _all_ variables(Free) from the model-pattern |
|
932 been substituted by a value from the pattern's environment ?*) |
|
933 term (*the precondition*) |
|
934 -> |
|
935 bool * (*has the precondition evaluated to true*) |
|
936 term (*the precondition (for map)*) |
|
937 .*) |
|
938 fun evalprecond prls (false, pre) = |
|
939 (*NOT ALL Free's have been substituted, eg. because of incomplete model*) |
|
940 (false, pre) |
|
941 | evalprecond prls (true, pre) = |
|
942 (* val (prls, pre) = (prls, hd pres'); |
|
943 val (prls, pre) = (prls, hd (tl pres')); |
|
944 *) |
|
945 if eval_true (assoc_thy "Isac.thy") (*for Pattern.match *) |
|
946 [pre] prls (*pre parsed, prls.thy*) |
|
947 then (true , pre) |
|
948 else (false , pre); |
|
949 |
|
950 fun pre2str (b, t) = pair2str(bool2str b, term2str t); |
|
951 fun pres2str pres = strs2str' (map (linefeed o pre2str) pres); |
|
952 |
|
953 (*. check preconditions, return true if all true .*) |
|
954 fun check_preconds' _ [] _ _ = [] (*empty preconditions are true*) |
|
955 | check_preconds' prls pres pbl _(*FIXME.WN0308 mvat re-introduce*) = |
|
956 (* val (prls, pres, pbl, _) = (prls, where_, probl, 0); |
|
957 val (prls, pres, pbl, _) = (prls, pre, itms, mvat); |
|
958 *) |
|
959 let val env = mk_env pbl; |
|
960 val pres' = map (subst_atomic_all env) pres; |
|
961 in map (evalprecond prls) pres' end; |
|
962 |
|
963 fun check_preconds thy prls pres pbl = |
|
964 check_preconds' prls pres pbl (max_vt pbl); |
|
965 |
|
966 (*----------------------------------------------------------*) |
|
967 end |
|
968 open SpecifyTools; |
|
969 (*----------------------------------------------------------*) |