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
6 (c) due to copyright terms
8 use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*);
12 signature SPECIFY_TOOLS =
24 val item2str : item -> string
26 val itm2str : Theory.theory -> itm -> string
29 Cor of (Term.term * Term.term list) * (Term.term * Term.term list)
30 | Inc of (Term.term * Term.term list) * (Term.term * Term.term list)
31 | Mis of Term.term * Term.term
33 | Sup of Term.term * Term.term list
36 val itm_2str : itm_ -> string
37 val itm__2str : Theory.theory -> itm_ -> string
38 val itms2str : Theory.theory -> itm list -> string
41 {Find: string list, With: string list, Given: string list,
42 Where: string list, Relate: string list} -> string
45 Matches of pblID * item ppc
46 | NoMatch of pblID * item ppc
47 val match2str : match -> string
50 Match_ of pblID * (itm list * (bool * Term.term) list)
52 val matchs2str : match list -> string
54 val ori2str : ori -> string
55 val oris2str : ori list -> string
57 val preori2str : preori -> string
58 val preoris2str : preori list -> string
60 (* val penv2str : Theory.theory -> penv -> string *)
62 (*----------------------------------------------------------------------*)
63 val all_ts_in : itm_ list -> Term.term list
67 Term.term list -> itm list -> (bool * Term.term) list
71 itm list -> 'a -> (bool * Term.term) list
72 (* val chkpre2item : rls -> Term.term -> bool * item *)
73 val pres2str : (bool * Term.term) list -> string
74 (* val evalprecond : rls -> Term.term -> bool * Term.term *)
75 (* val cnt : itm list -> int -> int * int *)
76 val comp_dts : Theory.theory -> Term.term * Term.term list -> Thm.cterm
77 val comp_dts' : Term.term * Term.term list -> Term.term
78 val comp_dts'' : Term.term * Term.term list -> string
79 val comp_ts : Term.term * Term.term list -> Term.term
80 val d_in : itm_ -> Term.term
81 val de_item : item -> cterm'
82 val dest_list : Term.term * Term.term list -> Term.term list (* for testing *)
83 val dest_list' : Term.term -> Term.term list
84 val dts2str : Term.term * Term.term list -> string
86 (* val e_listBool : Term.term *)
87 (* val e_listReal : Term.term *)
90 val empty_ppc : item ppc
91 (* val empty_ppc_ct' : cterm' ppc *)
92 (* val getval : Term.term * Term.term list -> Term.term * Term.term *)
95 Term.term Library.option ->
98 itm list -> 'b -> Term.term * (bool * Term.term) list*)
99 (* val init_item : string -> item *)
100 (* val is_matches : match -> bool *)
101 (* val is_matches_ : match_ -> bool *)
102 val is_var : Term.term -> bool
104 string ppc -> item ppc *)
105 val itemppc2str : item ppc -> string
106 val linefeed : string -> string
107 (* val matches_pblID : match -> pblID *)
108 val max2 : ('a * int) list -> 'a * int
109 val max_vt : itm list -> int
110 val mk_e : itm_ -> (Term.term * Term.term) list
111 val mk_en : int -> itm -> (Term.term * Term.term) list
112 val mk_env : itm list -> (Term.term * Term.term) list
113 val mkval : 'a -> Term.term list -> Term.term
114 val mkval' : Term.term list -> Term.term
115 (* val pblID_of_match : match -> pblID *)
116 val pbl_ids : Theory.theory -> Term.term -> Term.term -> Term.term list
117 val pbl_ids' : 'a -> Term.term -> Term.term list -> Term.term list
118 (* val pen2str : Theory.theory -> Term.term * Term.term list -> string *)
119 val penvval_in : itm_ -> Term.term list
120 val refined : match list -> pblID
122 match_ list -> match_ Library.option
123 (* val refined_IDitms :
124 match list -> match Library.option *)
125 val split_dts : 'a -> Term.term -> Term.term * Term.term list
126 val split_dts' : Term.term * Term.term -> Term.term list
127 (* val take_apart : Term.term -> Term.term list *)
128 (* val take_apart_inv : Term.term list -> Term.term *)
129 val ts_in : itm_ -> Term.term list
130 (* val unique : Term.term *)
131 val untouched : itm list -> bool
134 (''a * (''b * Term.term list) list) list ->
136 ''b * Term.term -> ''a -> ''a * (''b * Term.term list) list
141 Term.term -> Term.term -> Term.term -> envv
144 (''a * Term.term list) list ->
145 Term.term -> ''a * Term.term -> (''a * Term.term list) list
149 (vats * Term.term * Term.term * Term.term) list ->
151 val vts_cnt : int list -> itm list -> (int * int) list
152 val vts_in : itm list -> int list
153 (* val w_itms2str : Theory.theory -> itm list -> unit *)
156 (*----------------------------------------------------------*)
157 structure SpecifyTools : SPECIFY_TOOLS =
159 (*----------------------------------------------------------*)
160 val e_listReal = (term_of o the o (parse Script.thy)) "[]::(real list)";
161 val e_listBool = (term_of o the o (parse Script.thy)) "[]::(bool list)";
163 (*.take list-term apart w.r.t. handling elementwise input.*)
165 let val elems = isalist2list t
166 in map ((list2isalist (type_of (hd elems))) o single) elems end;
167 (*val t = str2term "[a, b]";
168 > val ts = take_apart t; writeln (terms2str ts);
171 > t = (take_apart_inv o take_apart) t;
173 fun take_apart_inv ts =
174 let val elems = (flat o (map isalist2list)) ts;
175 in list2isalist (type_of (hd elems)) elems end;
176 (*val ts = [str2term "[a]", str2term "[b]"];
177 > val t = take_apart_inv ts; term2str t;
180 ts = (take_apart o take_apart_inv) ts;
186 (*.revert split_dts only for ts; compare comp_dts.*)
187 fun comp_ts (d, ts) =
189 then if is_list (hd ts)
191 then (hd ts) (*e.g. someList [1,3,2]*)
192 else (take_apart_inv ts)
193 (* SML[ [a], [b] ]SML --> [a,b] *)
194 else (hd ts) (*a variable or metavariable for a list*)
197 WN050903 we do NOT know which is from subtheory, description or term;
198 typecheck thus may lead to TYPE-error 'unknown constant';
199 solution: typecheck with Isac.thy; i.e. arg 'thy' superfluous*)
200 fun comp_dts thy (d,[]) =
201 cterm_of ((sign_of o assoc_thy) "Isac.thy")
202 (*comp_dts:FIXXME stay with term for efficiency !!!*)
203 (if is_reall_dsc d then (d $ e_listReal)
204 else if is_booll_dsc d then (d $ e_listBool)
206 | comp_dts thy (d,ts) =
207 (cterm_of ((sign_of o assoc_thy) "Isac.thy")
208 (*comp_dts:FIXXME stay with term for efficiency !!*)
209 (d $ (comp_ts (d, ts)))
210 handle _ => raise error ("comp_dts: "^(term2str d)^
211 " $ "^(term2str (hd ts))));
213 fun comp_dts' (d,[]) =
214 if is_reall_dsc d then (d $ e_listReal)
215 else if is_booll_dsc d then (d $ e_listBool)
217 | comp_dts' (d,ts) = (d $ (comp_ts (d, ts)))
218 handle _ => raise error ("comp_dts': "^(term2str d)^
219 " $ "^(term2str (hd ts)));
220 (*val t = str2term "maximum A";
221 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
222 val it = "maximum A" : cterm
223 > val t = str2term "fixedValues [r=Arbfix]";
224 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
225 "fixedValues [r = Arbfix]"
226 > val t = str2term "valuesFor [a]";
227 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
229 > val t = str2term "valuesFor [a,b]";
230 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
232 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]";
233 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
234 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"
235 > val t = str2term "boundVariable a";
236 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
238 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}";
239 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
240 "interval {x. 0 <= x & x <= 2 * r}"
242 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))";
243 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
244 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
245 > val t = str2term "solveFor x";
246 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
248 > val t = str2term "errorBound (eps=0)";
249 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
250 "errorBound (eps = 0)"
251 > val t = str2term "solutions L";
252 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
256 > val t = (term_of o the o (parse thy)) "testdscforlist [#1]";
257 > val (d,ts) = split_dts t;
258 > comp_dts thy (d,ts);
259 val it = "testdscforlist [#1]" : cterm
261 > val t = (term_of o the o (parse thy)) "(A::real)";
262 > val (d,ts) = split_dts t;
263 val d = Const ("empty","empty") : term
264 val ts = [Free ("A","RealDef.real")] : term list
265 > val t = (term_of o the o (parse thy)) "[R=(R::real)]";
266 > val (d,ts) = split_dts t;
267 val d = Const ("empty","empty") : term
268 val ts = [Const # $ Free # $ Free (#,#)] : term list
269 > val t = (term_of o the o (parse thy)) "[#1,#2]";
270 > val (d,ts) = split_dts t;
271 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
274 (*for input_icalhd 11.03*)
275 fun comp_dts'' (d,[]) =
276 if is_reall_dsc d then term2str (d $ e_listReal)
277 else if is_booll_dsc d then term2str (d $ e_listBool)
279 | comp_dts'' (d,ts) = term2str (d $ (comp_ts (d, ts)))
280 handle _ => raise error ("comp_dts'': "^(term2str d)^
281 " $ "^(term2str (hd ts)));
288 (* this may decompose an object-language isa-list;
289 use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)
290 fun dest_list' t = if is_list t then isalist2list t else [t];
292 (*fun is_metavar (Free (str, _)) =
293 if (last_elem o explode) str = "_" then true else false
294 | is_metavar _ = false;*)
295 fun is_var (Free _) = true
298 (*.special handling for lists. ?WN:14.5.03 ??!?*)
299 fun dest_list (d,ts) =
301 if is_list_dsc d andalso not (is_unl d)
302 andalso not (is_var t) (*..for pbt*)
303 then isalist2list t else [t]
304 in (flat o (map dest)) ts end;
307 (*.decompose an input into description, terms (ev. elems of lists),
308 and the value for the problem-environment; inv to comp_dts .*)
309 (*WN.8.6.03: corrected with minimal effort,
310 fn : theory -> term ->
312 term list * lists decomposed for elementwise input
313 term list pbl_ids not _HERE_: dont know which list-elems input*)
314 fun split_dts thy (t as d $ arg) =
316 then if is_list_dsc d
319 then (d, [arg]) (*e.g. someList [1,3,2]*)
320 else (d, take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*)
321 else (d, [arg]) (*a variable or metavariable for a list*)
323 else (e_term, dest_list' t(*9.01 ???*))
324 | split_dts thy t = (*either dsc or term*)
325 let val (h,argl) = strip_comb t
326 in if (not o is_dsc) h then (e_term, dest_list' t)
327 else (h, dest_list (h,argl))
329 (* tests see fun comp_dts
331 > val t = str2term "someList []";
332 > val (_,ts) = split_dts thy t; writeln (terms2str ts);
334 > val t = str2term "valuesFor []";
335 > val (_,ts) = split_dts thy t; writeln (terms2str ts);
338 (*.version returning ts only.*)
339 fun split_dts' (d, arg) =
341 then if is_list_dsc d
344 then ([arg]) (*e.g. someList [1,3,2]*)
345 else (take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*)
346 else ([arg]) (*a variable or metavariable for a list*)
348 else (dest_list' arg(*9.01 ???*))
349 | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
350 let val (h,argl) = strip_comb t
351 in if (not o is_dsc) h then (dest_list' t)
352 else (dest_list (h,argl))
359 (*27.8.01: problem-environment
360 WN.6.5.03: FIXXME reconsider if penv is worth the effort --
361 -- just rerun a whole expl with num/var may show the same ?!
362 WN.9.5.03: penv-concept stalled, immediately generate script env !
363 but [#0, epsilon] only outcommented for eventual reconsideration
365 type penv = (term (*err_*)
366 * (term list) (*[#0, epsilon] 9.5.03 outcommented*)
368 fun pen2str thy (t, ts) =
369 pair2str(Sign.string_of_term (sign_of thy) t,
370 (strs2str' o map (Sign.string_of_term (sign_of thy))) ts);
371 fun penv2str thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv;
374 9.5.03: still unused, but left for eventual future development*)
375 type envv = (int * penv) list; (*over variants*)
377 (*. 14.9.01: not used after putting penv-values into itm_
378 make the result of split_* a value of problem-environment .*)
379 fun mkval dsc [] = raise error "mkval called with []"
381 | mkval dsc ts = list2isalist ((type_of o hd) ts) ts;
383 fun mkval' x = mkval e_term x;
387 (*. get the constant value from a penv .*)
388 fun getval (id, values) =
390 [] => raise error ("penv_value: no values in '"^
391 (Sign.string_of_term (sign_of Tools.thy) id))
393 | (v1::v2::_) => (case v1 of
394 Const ("Script.Arbfix",_) => (id, v2)
397 val e_ = (term_of o the o (parse thy)) "e_::bool";
398 val ev = (term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0";
399 val v_ = (term_of o the o (parse thy)) "v_";
400 val vv = (term_of o the o (parse thy)) "x";
401 val r_ = (term_of o the o (parse thy)) "err_::bool";
402 val rv1 = (term_of o the o (parse thy)) "#0";
403 val rv2 = (term_of o the o (parse thy)) "eps";
405 val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv;
407 [(Free ("e_","bool"),
408 Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#0","RealDef.real")),
409 (Free ("v_","RealDef.real"),Free ("x","RealDef.real")),
410 (Free ("err_","bool"),Free ("#0","RealDef.real"))] : (term * term) list
414 (*23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc
416 (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
417 =(presently) Mis (? should be Inc initially, and Mis after match_itms?)
418 (1.2) Syn,Typ,Sup: not related to oris
419 Syn, Typ (presently) should be accepted in appl_add (instead Error')
420 Sup (presently) should be accepted in appl_add (instead Error')
421 _could_ be w.r.t current vat (and then _is_ related to vat
422 Mis should _not_ be made Inc ((presently, by appl_add & match_itms)
423 - dsc in itm_ is timeconsuming -- keep id for respective queries ?
424 - order of items in ppc should be stable w.r.t order of itms
426 - stepwise input of itms --- match_itms (in one go) ..not coordinated
428 - match_itms / match_itms_oris ..2 versions ?!
429 (fast, for refine / slow, for modeling)
431 - clarify: efficiency <--> simplicity !!!
432 ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc
433 | take int for perserving order of item ppc in itms
434 | make all(!?) handling of itms stable against reordering(?)
435 | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)
436 -"- "#undef" ?= not touched ?= (id,..)
437 -----------------------------------------------------------------
439 def: type pbt = (field, (dsc, pid))
441 (1) fmz + pbt -> oris
442 (2) input + oris -> itm
443 (3) match_itms : schnell(?) f"ur refine
444 match_itms_oris : r"uckmeldung f"ur item ppc
446 (1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)
447 ---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!
449 (3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;
450 wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:
451 (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ????
458 (*the internal representation of a models' item
460 4.9.01: not consistent:
461 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
462 (involves 'is_error');
463 bool in itm really necessary ???*)
465 Cor of (term * (* description *)
466 (term list)) * (* for list: elem-wise input *)
467 (*split_dts <-> comp_dts*)
468 (term * (term list)) (* elem of penv *)
469 (*9.5.03: ---- is already for script -- penv delayed to future*)
472 | Inc of (term * (term list)) * (term * (term list)) (*lists,
473 + init_pbl WN.11.03 FIXXME: empty penv .. bad
474 init_pbl should return Mis !!!*)
475 | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
476 | Mis of (term * term) (* after re-specification pbt-item not found
477 in pbl: only dsc, pid_*)
478 | Par of cterm'; (*internal state from fun parsitm*)
480 type vats = int list; (*variants in formalizations*)
482 (*.data-type for working on pbl/met-ppc:
483 in pbl initially holds descriptions (only) for user guidance.*)
485 int * (* id =0 .. untouched - descript (only) from init
486 23.3.02: seems to correspond to ori (fun insert_ppc)
487 <> maintain order in item ppc?*)
488 vats * (* variants - copy from ori *)
489 bool * (* input on this item is not/complete *)
490 string * (* #Given | #Find | #Relate *)
492 (* use"ME/sequent.sml";
494 val e_itm = (0,[],false,"e_itm",Syn"e_itm"):itm;
495 (*in CalcTree/Subproblem an 'untouched' model is created
496 FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
497 fun untouched (itms: itm list) =
498 foldl and_ (true ,map ((curry op= 0) o #1) itms);
503 > untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")];
504 val it = false : bool*)
510 (* find most frequent variant v in itms *)
512 fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);
514 fun cnt itms v = (v,(length o (filter (curry op= v)) o
515 flat o (map #2)) (itms:itm list));
516 fun vts_cnt vts itms = map (cnt itms) vts;
517 fun max2 [] = raise error "max2 of []"
519 let fun mx (a,x) [] = (a,x)
520 | mx (a,x) ((b,y)::ys) =
521 if x < y then mx (b,y) ys else mx (a,x) ys;
524 (*. find the variant with most items already input .*)
526 let val vts = (vts_cnt (vts_in itms)) itms;
527 in if vts = [] then 0 else (fst o max2) vts end;
530 (* TODO ev. make more efficient by avoiding flat *)
531 fun mk_e (Cor (_, iv)) = [getval iv]
534 | mk_e (Inc (_, iv)) = [getval iv]
537 fun mk_en vt ((i,vts,b,f,itm_):itm) =
538 if vt mem vts then mk_e itm_ else [];
539 (*. extract the environment from an item list;
540 takes the variant with most items .*)
542 let val vt = max_vt itms
543 in (flat o (map (mk_en vt))) itms end;
547 (*. example as provided by an author, complete w.r.t. pbt specified
548 not touched by any user action .*)
549 type ori = (int * (* id: 10.3.00ff impl. only <>0 .. touched
550 21.3.02: insert_ppc needs it ! ?:purpose maintain
551 order in item ppc ???*)
552 vats * (* variants 21.3.02: related to pbt..discard ?*)
553 string * (* #Given | #Find | #Relate 21.3.02: discard ?*)
554 term * (* description *)
555 term list (* isalist2list t | [t] *)
557 val e_ori_ = (0,[],"",e_term,[e_term]):ori;
558 val e_ori = (0,[],"",e_term,[e_term]):ori;
560 fun ori2str ((i,vs,fi,t,ts):ori) =
561 "("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^
562 (term2str t)^", "^((strs2str o (map term2str)) ts)^")";
564 let val s = !show_types
565 val _ = show_types:= true
566 val str = (strs2str' o (map (linefeed o ori2str)))
567 val _ = show_types:= s
570 (*.an or without leading integer.*)
571 type preori = (vats *
575 fun preori2str ((vs,fi,t,ts):preori) =
576 "("^((strs2str o (map string_of_int)) vs)^", "^fi^", "^
577 (term2str t)^", "^((strs2str o (map term2str)) ts)^")";
578 val preoris2str = (strs2str' o (map (linefeed o preori2str)));
580 (*. given the input value (from split_dts)
581 make the value in a problem-env according to description-type .*)
582 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
583 (*9.5.03 penv-concept postponed *)
584 fun pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v =
586 then [v] (*eg. [r=Arbfix]*)
587 else (case v of (*eg. eps=#0*)
588 (Const ("op =",_) $ l $ r) => [r,l]
589 | _ => raise error ("pbl_ids Tools.nam: no equality "
590 ^(Sign.string_of_term (sign_of thy) v)))
591 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v]
592 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v]
593 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v]
594 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v]
595 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v]
596 | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v]
597 | pbl_ids thy _ v = raise error ("pbl_ids: not implemented for "
598 ^(Sign.string_of_term (sign_of thy) v));
600 val t as t1 $ t2 = str2term "antiDerivativeName M_b";
603 val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
604 val (d,argl) = strip_comb t;
605 is_dsc d; (*see split_dts*)
610 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
611 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
613 val (dsc,vl) = (split_dts o term_of o the o (parse thy)) "solveFor x";
614 val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term
615 val vl = Free ("x","RealDef.real") : term
617 val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
619 val it = [Free ("x","RealDef.real")] : term list
621 val (dsc,vl) = (split_dts o term_of o the o(parse thy))
622 "errorBound (eps=#0)";
623 val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_";
625 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *)
627 (*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))
628 make the value in a problem-env according to description-type .*)
629 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
630 fun pbl_ids' (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) vs =
632 [] => raise error ("pbl_ids' Tools.nam called with []")
633 | [t] => (case t of (*eg. eps=#0*)
634 (Const ("op =",_) $ l $ r) => [r,l]
635 | _ => raise error ("pbl_ids' Tools.nam: no equality "
636 ^(Sign.string_of_term (sign_of thy) t)))
637 | vs' => vs (*14.9.01: ???TODO *))
638 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs
639 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs
640 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs
641 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs
642 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))vs = vs
643 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))vs = vs
645 raise error ("pbl_ids': not implemented for "
647 (*9.5.03 penv postponed: pbl_ids'*)
648 fun pbl_ids' thy d vs = [comp_ts (d, vs)];
651 (*14.9.01: not used after putting values for penv into itm_
652 WN.5.5.03: used in upd .. upd_envv*)
653 fun upd_penv thy penv dsc (id, vl) =
654 (writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
655 writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
656 writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
657 overwrite (penv, (id, pbl_ids thy dsc vl))
661 val (dsc,vl) = (split_did o term_of o the o (parse thy)) "solveFor x";
662 val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
663 val penv = upd_penv thy penv dsc (id, vl);
664 [(Free ("v_","RealDef.real"),
665 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")])]
666 : (term * term list) list
668 val (dsc,vl) = (split_did o term_of o the o(parse thy))"errorBound (eps=#0)";
669 val (dsc,id) = (split_did o term_of o the o(parse thy))"errorBound err_";
670 upd_penv thy penv dsc (id, vl);
671 [(Free ("v_","RealDef.real"),
672 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")]),
673 (Free ("err_","bool"),
674 [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")])]
675 : (term * term list) list ^.........!!!!
678 (*WN.9.5.03: not reconsidered; looks strange !!!*)
679 fun upd thy envv dsc (id, vl) i =
680 let val penv = case assoc (envv, i) of
683 val penv' = upd_penv thy penv dsc (id, vl);
687 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
688 val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";
689 val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";
690 upd thy envv dsc (id, vl) i;
691 val it = (2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])
692 : int * (term * term list) list*)
695 (*14.9.01: not used after putting pre-penv into itm_*)
696 fun upd_envv thy (envv:envv) (vats:vats) dsc id vl =
697 let val vats = if length vats = 0
698 then (*unknown id to _all_ variants*)
699 if length envv = 0 then [1]
700 else (intsto o length) envv
702 fun isin vats (i,_) = i mem vats;
703 val envs_notin_vat = filter_out (isin vats) envv;
704 in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end;
706 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
709 val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";
710 val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";
711 val envv = upd_envv thy envv vats dsc id vl;
712 val envv = [(2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])]
713 : (int * (term * term list) list) list
716 val (dsc,vl) = (split_did o term_of o the o(parse thy))"maximum A";
717 val (dsc,id) = (split_did o term_of o the o(parse thy))"maximum m_";
718 upd_envv thy envv vats dsc id vl;
719 [(1,[(Free ("m_","bool"),[Free ("A","bool")])]),
721 [(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")]),
722 (Free ("m_","bool"),[Free ("A","bool")])]),
723 (3,[(Free ("m_","bool"),[Free ("A","bool")])])]
724 : (int * (term * term list) list) list
728 val (d,ts) = (split_dts o term_of o the o (parse thy))
729 "fixedValues [r=Arbfix]";
730 val (_,id) = (split_did o term_of o the o (parse thy))"fixedValues fix_";
732 val env = upd_envv thy env vats d id (mkval ts);
735 (*. update envv by folding from a list of arguments .*)
736 fun upds_envv thy envv [] = envv
737 | upds_envv thy envv ((vs, dsc, id, vl)::ps) =
738 upds_envv thy (upd_envv thy envv vs dsc id vl) ps;
739 (* eval test-maximum.sml until Specify_Method ...
740 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
741 val met = (#ppc o get_met) mI;
744 val eargs = flat eargs;
745 val (vs, dsc, id, vl) = hd eargs;
746 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
748 val (vs, dsc, id, vl) = hd (tl eargs);
749 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
751 val (vs, dsc, id, vl) = hd (tl (tl eargs));
752 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
754 val (vs, dsc, id, vl) = hd (tl (tl (tl eargs)));
755 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
757 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
758 (Free ("m_","bool"),[Free (#,#)]),
759 (Free ("vs_","bool List.list"),[# $ # $ Const #]),
760 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
762 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
763 (Free ("m_","bool"),[Free (#,#)]),
764 (Free ("vs_","bool List.list"),[# $ # $ Const #]),
765 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
767 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
768 (Free ("m_","bool"),[Free (#,#)]),
769 (Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *)
771 (*for _output_ of the items of a Model*)
773 Correct of cterm' (*labels a correct formula (type cterm')*)
774 | SyntaxE of string (**)
775 | TypeE of string (**)
776 | False of cterm' (*WN050618 notexistent in itm_: only used in Where*)
777 | Incompl of cterm' (**)
778 | Superfl of string (**)
780 fun item2str (Correct s) ="Correct "^s
781 | item2str (SyntaxE s) ="SyntaxE "^s
782 | item2str (TypeE s) ="TypeE "^s
783 | item2str (False s) ="False "^s
784 | item2str (Incompl s) ="Incompl "^s
785 | item2str (Superfl s) ="Superfl "^s
786 | item2str (Missing s) ="Missing "^s;
787 (*make string for error-msgs*)
788 fun itm__2str thy (Cor ((d,ts), penv)) =
789 "Cor " ^ string_of_cterm (comp_dts thy(d,ts)) ^" ,"^ pen2str thy penv
790 | itm__2str thy (Syn c) = "Syn "^c
791 | itm__2str thy (Typ c) = "Typ "^c
792 | itm__2str thy (Inc ((d,ts), penv)) =
793 "Inc " ^ string_of_cterm (comp_dts thy(d,ts)) ^" ,"^ pen2str thy penv
794 | itm__2str thy (Sup (d,ts)) = "Sup "^(string_of_cterm (comp_dts thy(d,ts)))
795 | itm__2str thy (Mis (d,pid))=
796 "Mis "^ Sign.string_of_term (sign_of thy) d ^
797 " "^ Sign.string_of_term (sign_of thy) pid
798 | itm__2str thy (Par s) = "Trm "^s;
799 fun itm_2str t = itm__2str (assoc_thy "Isac.thy") t;
800 fun itm2str thy ((i,is,b,s,itm_):itm) =
801 "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^
802 s^" ,"^(itm__2str thy itm_)^")";
803 val linefeed = (curry op^) "\n";
804 fun itms2str thy itms = strs2str' (map (linefeed o (itm2str thy)) itms);
805 fun w_itms2str thy itms = writeln (itms2str thy itms);
807 fun init_item str = SyntaxE str;
818 fun ppc2str {Given=Given,Where=Where,Find=Find,With=With,Relate=Relate}=
819 ("{Given =" ^ (strs2str Given ) ^
820 ",Where=" ^ (strs2str Where) ^
821 ",Find =" ^ (strs2str Find ) ^
822 ",With =" ^ (strs2str With ) ^
823 ",Relate=" ^ (strs2str Relate) ^ "}");
828 fun item_ppc ({Given = gi,Where= wh,
829 Find = fi,With = wi,Relate= re}: string ppc) =
830 {Given = map init_item gi,Where= map init_item wh,
831 Find = map init_item fi,With = map init_item wi,
832 Relate= map init_item re}:item ppc;
833 fun itemppc2str ({Given=Given,Where=Where,
834 Find=Find,With=With,Relate=Relate}:item ppc)=
835 ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
836 ",Where=" ^ ((strs2str' o (map item2str)) Where) ^
837 ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
838 ",With =" ^ ((strs2str' o (map item2str)) With ) ^
839 ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
841 fun de_item (Correct x) = x
842 | de_item (SyntaxE x) = x
843 | de_item (TypeE x) = x
844 | de_item (False x) = x
845 | de_item (Incompl x) = x
846 | de_item (Superfl x) = x
847 | de_item (Missing x) = x;
848 val empty_ppc ={Given = [],
852 Relate= []}:item ppc;
853 val empty_ppc_ct' ={Given = [],
857 Relate= []}:cterm' ppc;
861 Matches of pblID * item ppc
862 | NoMatch of pblID * item ppc;
863 fun match2str (Matches (pI, ppc)) =
864 "Matches ("^(strs2str pI)^", "^(itemppc2str ppc)^")"
865 | match2str(NoMatch (pI, ppc)) =
866 "NoMatch ("^(strs2str pI)^", "^(itemppc2str ppc)^")";
867 fun matchs2str ms = (strs2str o (map match2str)) ms;
868 fun pblID_of_match (Matches (pI,_)) = pI
869 | pblID_of_match (NoMatch (pI,_)) = pI;
871 (*10.03 for Refine_Problem*)
873 Match_ of pblID * ((itm list) * ((bool * term) list))
876 (*. the refined pbt is the last_element Matches in the list .*)
877 fun is_matches (Matches _) = true
878 | is_matches _ = false;
879 fun matches_pblID (Matches (pI,_)) = pI;
880 fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms)
881 handle _ => []:pblID;
882 fun refined_IDitms ms = ((find_first is_matches) o rev) ms;
884 (*. the refined pbt is the last_element Matches in the list,
885 for Refine_Problem, tryrefine .*)
886 fun is_matches_ (Match_ _) = true
887 | is_matches_ _ = false;
888 fun refined_ ms = ((find_first is_matches_) o rev) ms;
891 fun ts_in (Cor ((_,ts),_)) = ts
892 | ts_in (Syn (c)) = []
893 | ts_in (Typ (c)) = []
894 | ts_in (Inc ((_,ts),_)) = ts
895 | ts_in (Sup (_,ts)) = ts
896 | ts_in (Mis _) = [];
898 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
899 val unique = (term_of o the o (parse Real.thy)) "UnIqE_tErM";
900 fun d_in (Cor ((d,_),_)) = d
901 | d_in (Syn (c)) = (writeln("*** d_in: Syn ("^c^")"); unique)
902 | d_in (Typ (c)) = (writeln("*** d_in: Typ ("^c^")"); unique)
903 | d_in (Inc ((d,_),_)) = d
904 | d_in (Sup (d,_)) = d
905 | d_in (Mis (d,_)) = d;
907 fun dts2str (d,ts) = pair2str (term2str d, terms2str ts);
908 fun penvval_in (Cor ((d,_),(_,ts))) = [comp_ts (d,ts)]
909 | penvval_in (Syn (c)) = (writeln("*** penvval_in: Syn ("^c^")"); [])
910 | penvval_in (Typ (c)) = (writeln("*** penvval_in: Typ ("^c^")"); [])
911 | penvval_in (Inc (_,(_,ts))) = ts
912 | penvval_in (Sup dts) = (writeln("*** penvval_in: Sup "^(dts2str dts)); [])
913 | penvval_in (Mis (d,t)) = (writeln("*** penvval_in: Mis "^
914 (pair2str(term2str d, term2str t))); []);
917 (*. check a predicate labelled with indication of incomplete substitution;
918 rls -> (*for eval_true*)
919 bool * (*have _all_ variables(Free) from the model-pattern
920 been substituted by a value from the pattern's environment ?*)
921 Term.term (*the precondition*)
923 bool * (*has the precondition evaluated to true*)
924 Term.term (*the precondition (for map)*)
926 fun evalprecond prls (false, pre) =
927 (*NOT ALL Free's have been substituted, eg. because of incomplete model*)
929 | evalprecond prls (true, pre) =
930 (* val (prls, pre) = (prls, hd pres');
931 val (prls, pre) = (prls, hd (tl pres'));
933 if eval_true (assoc_thy "Isac.thy") (*for Pattern.match *)
934 [pre] prls (*pre parsed, prls.thy*)
938 fun pre2str (b, t) = pair2str(bool2str b, term2str t);
939 fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
941 (*. check preconditions, return true if all true .*)
942 fun check_preconds' _ [] _ _ = [] (*empty preconditions are true*)
943 | check_preconds' prls pres pbl _(*FIXME.WN0308 mvat re-introduce*) =
944 (* val (prls, pres, pbl, _) = (prls, where_, probl, 0);
945 val (prls, pres, pbl, _) = (prls, pre, itms, mvat);
947 let val env = mk_env pbl;
948 val pres' = map (subst_atomic_all env) pres;
949 in map (evalprecond prls) pres' end;
951 fun check_preconds thy prls pres pbl =
952 check_preconds' prls pres pbl (max_vt pbl);
957 (*----------------------------24.3.02: done too much-----
958 (**. copy the already input items from probl to meth (in PblObj):
959 for each item in met search the related one in pbl,
960 items not found in probl are (1) inserted as 'untouched' (0,...),
961 and (2) completed from oris (via max_vt)
962 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ "uberkomplett 21.2.02 ------------ .**)
963 (* val (pbl, met) = (itms, ppc);
965 fun copy_pbl thy oris pbl met =
966 let val vt = max_vt pbl;
967 fun vt_and_dsc d' ((i,v,f,d,ts):ori) =
968 vt mem v andalso d'= d
969 fun cpy its [] (f, (d, id)) =
970 if length its = 0 (*no dsc found in pbl*)
971 then case find_first (vt_and_dsc d) oris
972 of Some (i,v,_,_,ts) =>
973 [(i,v,true,f, Cor ((d,ts), (id,pbl_ids' thy d ts)))]
974 | None => [(0,[],false,f,Mis (d, id))]
976 | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =
977 if d = d_in itm_ andalso i<>0 (*already touched by user*)
978 then cpy (its @ [it]) itms pb else cpy its itms pb;
979 in ((flat o (map (cpy [] pbl))) met):itm list end;
982 (**. copy the already input items from probl to meth (in PblObj):
983 for each item in met search the related one in pbl,
984 items not found in probl are inserted as 'untouched' (0,...)
985 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ "uberkomplett 21.2.02 ------------ .**)
986 (* val (pbl, met) = (itms, ppc);
988 fun copy_pbl (pbl:itm list) met =
989 let fun cpy its [] (f, (d, id)) =
990 if length its = 0 (*no dsc found in pbl*)
991 then [(0,[],false,f,Mis (d, id))]
993 | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =
994 if d = d_in itm_ andalso i<>0 (*already touched by user*)
995 then cpy (its @ [it]) itms pb else cpy its itms pb;
996 in ((flat o (map (cpy [] pbl))) met):itm list end;
999 (**. copy the already input items from probl to meth (in PblObj):
1000 for each item in met search the related one in pbl
1001 (missing items are requested by nxt_spec) .**)
1002 (* val (pbl, met) = (itms, ppc);
1004 fun copy_pbl (pbl:itm list) met =
1005 let fun cpy its [] (f, (d, id)) = its
1006 | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =
1007 if d = d_in itm_ andalso i<>0 (*already touched by user*)
1008 then cpy (its @ [it]) itms pb
1009 else cpy its itms pb;
1010 in ((flat o (map (cpy [] pbl))) met):itm list end;
1012 (*. copy pbt to met (in Specify_Method)
1013 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
1014 (2) filter (dsc(pbt) = dsc(oris)) oris; -> newitms;
1015 (3) pbt @ newitms .*)
1016 (* val (pbl, met) = (itms, pbt);
1018 fun copy_pbl (pbl:itm list) met oris =
1019 let fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;
1020 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
1021 Some _ => false | None => true;
1022 (*1*)val mis = ((map (cons2 (fst, fst o snd))) o (filter (notmem pbl))) met;
1024 fun eqdsc_ori d ((_,_,_,d',_):ori) = d = d';
1025 fun ori2itmMis f ((i,v,_,d,ts):ori) = (i,v,false,f,Mis (d,ts)):itm;
1026 fun oris2itms oris mis1 = ((map (ori2itmMis (fst mis1)))
1027 o (filter ((eqdsc_ori o snd) mis1))) oris;
1028 val news = (flat o (map (oris2itms oris))) mis;
1030 ----------------------------24.3.02: done too much-----*)
1037 (* ---------------------------------------------NOT UPTODATE !!! 4.9.01
1038 eval test-maximum.sml until Specify_Method ...
1039 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
1040 val met = (#ppc o get_met) mI;
1043 [((1,[1,2,3],true,"#Given",Cor ((Const #,[#]),[])),
1044 [([1,2,3],Const ("Descript.fixedValues","bool List.list => Tools.nam"),
1045 Free ("fix_","bool List.list"),Const # $ Free # $ Const (#,#))])]
1046 : (itm * (vats * term * term * term) list) list
1048 upds_envv thy [] (flat eargs);
1050 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
1051 (Free ("m_","bool"),[Free (#,#)]),
1052 (Free ("vs_","bool List.list"),[# $ # $ (# $ #)]),
1053 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
1055 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
1056 (Free ("m_","bool"),[Free (#,#)]),
1057 (Free ("vs_","bool List.list"),[# $ # $ (# $ #)]),
1058 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
1060 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
1061 (Free ("m_","bool"),[Free (#,#)]),
1062 (Free ("vs_","bool List.list"),[# $ # $ (# $ #)])])] : envv
1065 (*----------------------------------------------------------*)
1068 (*----------------------------------------------------------*)