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!*);
10 12345678901234567890123456789012345678901234567890123456789012345678901234567890
11 10 20 30 40 50 60 70 80
14 signature SPECIFY_TOOLS =
26 val item2str : item -> string
28 val itm2str_ : Proof.context -> itm -> string
31 Cor of (term * term list) * (term * term list)
32 | Inc of (term * term list) * (term * term list)
35 | Sup of term * term list
38 val itm_2str : itm_ -> string
39 val itm_2str_ : Proof.context -> itm_ -> string
40 val itms2str_ : Proof.context -> itm list -> string
43 {Find: string list, With: string list, Given: string list,
44 Where: string list, Relate: string list} -> string
47 Matches of pblID * item ppc
48 | NoMatch of pblID * item ppc
49 val match2str : match -> string
52 Match_ of pblID * (itm list * (bool * term) list)
54 val matchs2str : match list -> string
56 val ori2str : ori -> string
57 val oris2str : ori list -> string
59 val preori2str : preori -> string
60 val preoris2str : preori list -> string
62 (* val penv2str_ : Proof.context -> penv -> string *)
64 (*----------------------------------------------------------------------*)
65 val all_ts_in : itm_ list -> term list
69 term list -> itm list -> (bool * 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
88 (* val e_listBool : term *)
89 (* val e_listReal : term *)
92 val empty_ppc : item ppc
93 (* val empty_ppc_ct' : cterm' ppc *)
94 (* val getval : term * term list -> term * term *)
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
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
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
135 (''a * (''b * term list) list) list ->
137 ''b * term -> ''a -> ''a * (''b * term list) list
142 term -> term -> term -> envv
145 (''a * term list) list ->
146 term -> ''a * term -> (''a * term list) list
150 (vats * term * term * term) list ->
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 *)
157 (*----------------------------------------------------------*)
158 structure SpecifyTools : SPECIFY_TOOLS =
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)";
164 (*.take list-term apart w.r.t. handling elementwise input.*)
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);
172 > t = (take_apart_inv o take_apart) t;
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;
181 ts = (take_apart o take_apart_inv) ts;
187 (*.revert split_dts only for ts; compare comp_dts.*)
188 fun comp_ts (d, ts) =
190 then if is_list (hd ts)
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*)
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"*)
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)
208 | comp_dts thy (d,ts) =
209 (cterm_of (*(sign_of o assoc_thy) "Isac.thy"*)
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)
219 | comp_dts thy (d,ts) =
220 (d $ (comp_ts (d, ts)))
221 handle _ => raise error ("comp_dts: "^(term2str d)^
222 " $ "^(term2str (hd ts)));
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)
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);
240 > val t = str2term "valuesFor [a,b]";
241 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
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);
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}"
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);
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);
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
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
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)
290 | comp_dts'' (d,ts) = term2str (d $ (comp_ts (d, ts)))
291 handle _ => raise error ("comp_dts'': "^(term2str d)^
292 " $ "^(term2str (hd ts)));
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];
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
309 (*.special handling for lists. ?WN:14.5.03 ??!?*)
310 fun dest_list (d,ts) =
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;
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 ->
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) =
327 then if is_list_dsc 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*)
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))
340 (* tests see fun comp_dts
342 > val t = str2term "someList []";
343 > val (_,ts) = split_dts thy t; writeln (terms2str ts);
345 > val t = str2term "valuesFor []";
346 > val (_,ts) = split_dts thy t; writeln (terms2str ts);
349 (*.version returning ts only.*)
350 fun split_dts' (d, arg) =
352 then if is_list_dsc 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*)
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))
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
376 type penv = (term (*err_*)
377 * (term list) (*[#0, epsilon] 9.5.03 outcommented*)
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;
385 9.5.03: still unused, but left for eventual future development*)
386 type envv = (int * penv) list; (*over variants*)
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 []"
392 | mkval dsc ts = list2isalist ((type_of o hd) ts) ts;
394 fun mkval' x = mkval e_term x;
398 (*. get the constant value from a penv .*)
399 fun getval (id, values) =
401 [] => raise error ("penv_value: no values in '"^
402 (Syntax.string_of_term (thy2ctxt' "Tools") id))
404 | (v1::v2::_) => (case v1 of
405 Const ("Script.Arbfix",_) => (id, v2)
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";
416 val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]: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
425 (*23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc
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
437 - stepwise input of itms --- match_itms (in one go) ..not coordinated
439 - match_itms / match_itms_oris ..2 versions ?!
440 (fast, for refine / slow, for modeling)
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 -----------------------------------------------------------------
450 def: type pbt = (field, (dsc, pid))
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
457 (1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)
458 ---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!
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 ????
469 (*the internal representation of a models' item
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 ???*)
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*)
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*)
491 type vats = int list; (*variants in formalizations*)
493 (*.data-type for working on pbl/met-ppc:
494 in pbl initially holds descriptions (only) for user guidance.*)
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 *)
503 (* use"ME/sequent.sml";
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);
514 > untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")];
515 val it = false : bool*)
521 (* find most frequent variant v in itms *)
523 fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);
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 []"
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;
535 (*. find the variant with most items already input .*)
537 let val vts = (vts_cnt (vts_in itms)) itms;
538 in if vts = [] then 0 else (fst o max2) vts end;
541 (* TODO ev. make more efficient by avoiding flat *)
542 fun mk_e (Cor (_, iv)) = [getval iv]
545 | mk_e (Inc (_, iv)) = [getval iv]
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 .*)
553 let val vt = max_vt itms
554 in (flat o (map (mk_en vt))) itms end;
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] *)
568 val e_ori_ = (0,[],"",e_term,[e_term]):ori;
569 val e_ori = (0,[],"",e_term,[e_term]):ori;
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)^")";
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
581 (*.an or without leading integer.*)
582 type preori = (vats *
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)));
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 =
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));
610 val t as t1 $ t2 = str2term "antiDerivativeName M_b";
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*)
620 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
621 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
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
627 val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
629 val it = [Free ("x","RealDef.real")] : term list
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_";
635 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *)
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 =
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 (ctxt_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
655 raise error ("pbl_ids': not implemented for "
657 (*9.5.03 penv postponed: pbl_ids'*)
658 fun pbl_ids' thy d vs = [comp_ts (d, vs)];
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))
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
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 ^.........!!!!
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
693 val penv' = upd_penv thy penv dsc (id, vl);
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*)
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
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;
716 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
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
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")])]),
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
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_";
742 val env = upd_envv thy env vats d id (mkval ts);
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;
754 val eargs = flat eargs;
755 val (vs, dsc, id, vl) = hd eargs;
756 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
758 val (vs, dsc, id, vl) = hd (tl eargs);
759 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
761 val (vs, dsc, id, vl) = hd (tl (tl eargs));
762 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
764 val (vs, dsc, id, vl) = hd (tl (tl (tl eargs)));
765 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
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"),[# $ # $ (# $ #)])]),
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"),[# $ # $ (# $ #)])]),
777 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
778 (Free ("m_","bool"),[Free (#,#)]),
779 (Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *)
781 (*for _output_ of the items of a Model*)
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 (**)
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)) ^ " ,"
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)) ^ " ,"
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);
819 fun init_item str = SyntaxE str;
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) ^ "}");
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) ^ "}");
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 = [],
864 Relate= []}:item ppc;
865 val empty_ppc_ct' ={Given = [],
869 Relate= []}:cterm' ppc;
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;
883 (*10.03 for Refine_Problem*)
885 Match_ of pblID * ((itm list) * ((bool * term) list))
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;
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;
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 _) = [];
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;
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))); []);
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*)
935 bool * (*has the precondition evaluated to true*)
936 term (*the precondition (for map)*)
938 fun evalprecond prls (false, pre) =
939 (*NOT ALL Free's have been substituted, eg. because of incomplete model*)
941 | evalprecond prls (true, pre) =
942 (* val (prls, pre) = (prls, hd pres');
943 val (prls, pre) = (prls, hd (tl pres'));
945 if eval_true (assoc_thy "Isac.thy") (*for Pattern.match *)
946 [pre] prls (*pre parsed, prls.thy*)
950 fun pre2str (b, t) = pair2str(bool2str b, term2str t);
951 fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
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);
959 let val env = mk_env pbl;
960 val pres' = map (subst_atomic_all env) pres;
961 in map (evalprecond prls) pres' end;
963 fun check_preconds thy prls pres pbl =
964 check_preconds' prls pres pbl (max_vt pbl);
969 (*----------------------------24.3.02: done too much-----
970 (**. copy the already input items from probl to meth (in PblObj):
971 for each item in met search the related one in pbl,
972 items not found in probl are (1) inserted as 'untouched' (0,...),
973 and (2) completed from oris (via max_vt)
974 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ "uberkomplett 21.2.02 ------------ .**)
975 (* val (pbl, met) = (itms, ppc);
977 fun copy_pbl thy oris pbl met =
978 let val vt = max_vt pbl;
979 fun vt_and_dsc d' ((i,v,f,d,ts):ori) =
980 vt mem v andalso d'= d
981 fun cpy its [] (f, (d, id)) =
982 if length its = 0 (*no dsc found in pbl*)
983 then case find_first (vt_and_dsc d) oris
984 of SOME (i,v,_,_,ts) =>
985 [(i,v,true,f, Cor ((d,ts), (id,pbl_ids' thy d ts)))]
986 | NONE => [(0,[],false,f,Mis (d, id))]
988 | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =
989 if d = d_in itm_ andalso i<>0 (*already touched by user*)
990 then cpy (its @ [it]) itms pb else cpy its itms pb;
991 in ((flat o (map (cpy [] pbl))) met):itm list end;
994 (**. copy the already input items from probl to meth (in PblObj):
995 for each item in met search the related one in pbl,
996 items not found in probl are inserted as 'untouched' (0,...)
997 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ "uberkomplett 21.2.02 ------------ .**)
998 (* val (pbl, met) = (itms, ppc);
1000 fun copy_pbl (pbl:itm list) met =
1001 let fun cpy its [] (f, (d, id)) =
1002 if length its = 0 (*no dsc found in pbl*)
1003 then [(0,[],false,f,Mis (d, id))]
1005 | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =
1006 if d = d_in itm_ andalso i<>0 (*already touched by user*)
1007 then cpy (its @ [it]) itms pb else cpy its itms pb;
1008 in ((flat o (map (cpy [] pbl))) met):itm list end;
1011 (**. copy the already input items from probl to meth (in PblObj):
1012 for each item in met search the related one in pbl
1013 (missing items are requested by nxt_spec) .**)
1014 (* val (pbl, met) = (itms, ppc);
1016 fun copy_pbl (pbl:itm list) met =
1017 let fun cpy its [] (f, (d, id)) = its
1018 | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =
1019 if d = d_in itm_ andalso i<>0 (*already touched by user*)
1020 then cpy (its @ [it]) itms pb
1021 else cpy its itms pb;
1022 in ((flat o (map (cpy [] pbl))) met):itm list end;
1024 (*. copy pbt to met (in Specify_Method)
1025 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
1026 (2) filter (dsc(pbt) = dsc(oris)) oris; -> newitms;
1027 (3) pbt @ newitms .*)
1028 (* val (pbl, met) = (itms, pbt);
1030 fun copy_pbl (pbl:itm list) met oris =
1031 let fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;
1032 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
1033 SOME _ => false | NONE => true;
1034 (*1*)val mis = ((map (cons2 (fst, fst o snd))) o (filter (notmem pbl))) met;
1036 fun eqdsc_ori d ((_,_,_,d',_):ori) = d = d';
1037 fun ori2itmMis f ((i,v,_,d,ts):ori) = (i,v,false,f,Mis (d,ts)):itm;
1038 fun oris2itms oris mis1 = ((map (ori2itmMis (fst mis1)))
1039 o (filter ((eqdsc_ori o snd) mis1))) oris;
1040 val news = (flat o (map (oris2itms oris))) mis;
1042 ----------------------------24.3.02: done too much-----*)
1049 (* ---------------------------------------------NOT UPTODATE !!! 4.9.01
1050 eval test-maximum.sml until Specify_Method ...
1051 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
1052 val met = (#ppc o get_met) mI;
1055 [((1,[1,2,3],true,"#Given",Cor ((Const #,[#]),[])),
1056 [([1,2,3],Const ("Descript.fixedValues","bool List.list => Tools.nam"),
1057 Free ("fix_","bool List.list"),Const # $ Free # $ Const (#,#))])]
1058 : (itm * (vats * term * term * term) list) list
1060 upds_envv thy [] (flat eargs);
1062 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
1063 (Free ("m_","bool"),[Free (#,#)]),
1064 (Free ("vs_","bool List.list"),[# $ # $ (# $ #)]),
1065 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
1067 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
1068 (Free ("m_","bool"),[Free (#,#)]),
1069 (Free ("vs_","bool List.list"),[# $ # $ (# $ #)]),
1070 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
1072 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
1073 (Free ("m_","bool"),[Free (#,#)]),
1074 (Free ("vs_","bool List.list"),[# $ # $ (# $ #)])])] : envv
1077 (*----------------------------------------------------------*)
1080 (*----------------------------------------------------------*)