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
5 author: Walther Neuper, Mathias Lehnfeld
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 : 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 declare_constraints : string -> Proof.context -> Proof.context
85 val declare_constraints' : term list -> Proof.context -> Proof.context
86 val dest_list : term * term list -> term list (* for testing *)
87 val dest_list' : term -> term list
88 val dts2str : term * term list -> string
90 (* val e_listBool : term *)
91 (* val e_listReal : term *)
94 val empty_ppc : item ppc
95 (* val empty_ppc_ct' : cterm' ppc *)
96 (* val getval : term * term list -> term * term *)
102 itm list -> 'b -> term * (bool * term) list*)
103 (* val init_item : string -> item *)
104 (* val is_matches : match -> bool *)
105 (* val is_matches_ : match_ -> bool *)
106 val is_var : term -> bool
108 string ppc -> item ppc *)
109 val itemppc2str : item ppc -> string
110 (* val matches_pblID : match -> pblID *)
111 val max2 : ('a * int) list -> 'a * int
112 val max_vt : itm list -> int
113 val mk_e : itm_ -> (term * term) list
114 val mk_en : int -> itm -> (term * term) list
115 val mk_env : itm list -> (term * term) list
116 val mkval : 'a -> term list -> term
117 val mkval' : term list -> term
118 (* val pblID_of_match : match -> pblID *)
119 val pbl_ids : Proof.context -> term -> term -> term list
120 val pbl_ids' : term -> term list -> term list
121 (* val pen2str : theory -> term * term list -> string *)
122 val penvval_in : itm_ -> term list
123 val refined : match list -> pblID
125 match_ list -> match_ option
126 (* val refined_IDitms :
127 match list -> match option *)
128 val split_dts : term -> term * term list
129 val split_dts' : term * term -> term list
130 (* val take_apart : term -> term list *)
131 (* val take_apart_inv : term list -> term *)
132 val ts_in : itm_ -> term list
133 (* val unique : term *)
134 val untouched : itm list -> bool
137 (''a * (''b * term list) list) list ->
139 ''b * term -> ''a -> ''a * (''b * term list) list
144 term -> term -> term -> envv
147 (''a * term list) list ->
148 term -> ''a * term -> (''a * term list) list
152 (vats * term * term * term) list ->
154 val vts_cnt : int list -> itm list -> (int * int) list
155 val vts_in : itm list -> int list
156 (* val w_itms2str_ : Proof.context -> itm list -> unit *)
157 val get_assumptions : Proof.context -> term list
158 val get_environments : Proof.context -> (term * term) list
159 val insert_assumptions : term list -> Proof.context -> Proof.context
160 val insert_environments : (term * term) list -> Proof.context -> Proof.context
161 val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
162 val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context
166 (*----------------------------------------------------------*)
167 structure SpecifyTools : SPECIFY_TOOLS =
169 (*----------------------------------------------------------*)
170 val script_parse = the o (Thy_Info.get_theory "Script" |> thy2ctxt |> parseNEW);
171 val e_listReal = script_parse "[]::(real list)";
172 val e_listBool = script_parse "[]::(bool list)";
174 (*.take list-term apart w.r.t. handling elementwise input.*)
176 let val elems = isalist2list t
177 in map ((list2isalist (type_of (hd elems))) o single) elems end;
178 (*val t = str2term "[a, b]";
179 > val ts = take_apart t; tracing (terms2str ts);
182 > t = (take_apart_inv o take_apart) t;
184 fun take_apart_inv ts =
185 let val elems = (flat o (map isalist2list)) ts;
186 in list2isalist (type_of (hd elems)) elems end;
187 (*val ts = [str2term "[a]", str2term "[b]"];
188 > val t = take_apart_inv ts; term2str t;
191 ts = (take_apart o take_apart_inv) ts;
197 (*.revert split_dts only for ts; compare comp_dts.*)
198 fun comp_ts (d, ts) =
200 then if is_list (hd ts)
202 then (hd ts) (*e.g. someList [1,3,2]*)
203 else (take_apart_inv ts)
204 (* SML[ [a], [b] ]SML --> [a,b] *)
205 else (hd ts) (*a variable or metavariable for a list*)
208 WN050903 we do NOT know which is from subtheory, description or term;
209 typecheck thus may lead to TYPE-error 'unknown constant';
210 solution: typecheck with (Thy_Info.get_theory "Isac"); i.e. arg 'thy' superfluous*)
211 (*fun comp_dts thy (d,[]) =
212 cterm_of (*(sign_of o assoc_thy) "Isac"*)
213 (Thy_Info.get_theory "Isac")
214 (*comp_dts:FIXXME stay with term for efficiency !!!*)
215 (if is_reall_dsc d then (d $ e_listReal)
216 else if is_booll_dsc d then (d $ e_listBool)
219 (cterm_of (*(sign_of o assoc_thy) "Isac"*)
220 (Thy_Info.get_theory "Isac")
221 (*comp_dts:FIXXME stay with term for efficiency !!*)
222 (d $ (comp_ts (d, ts)))
223 handle _ => error ("comp_dts: "^(term2str d)^
224 " $ "^(term2str (hd ts))));*)
225 fun comp_dts (d,[]) =
226 (if is_reall_dsc d then (d $ e_listReal)
227 else if is_booll_dsc d then (d $ e_listBool)
230 (d $ (comp_ts (d, ts)))
231 handle _ => error ("comp_dts: "^(term2str d)^
232 " $ "^(term2str (hd ts)));
234 fun comp_dts' (d,[]) =
235 if is_reall_dsc d then (d $ e_listReal)
236 else if is_booll_dsc d then (d $ e_listBool)
238 | comp_dts' (d,ts) = (d $ (comp_ts (d, ts)))
239 handle _ => error ("comp_dts': "^(term2str d)^
240 " $ "^(term2str (hd ts)));
241 (*val t = str2term "maximum A";
242 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
243 val it = "maximum A" : cterm
244 > val t = str2term "fixedValues [r=Arbfix]";
245 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
246 "fixedValues [r = Arbfix]"
247 > val t = str2term "valuesFor [a]";
248 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
250 > val t = str2term "valuesFor [a,b]";
251 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
253 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]";
254 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
255 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"
256 > val t = str2term "boundVariable a";
257 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
259 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}";
260 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
261 "interval {x. 0 <= x & x <= 2 * r}"
263 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))";
264 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
265 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
266 > val t = str2term "solveFor x";
267 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
269 > val t = str2term "errorBound (eps=0)";
270 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
271 "errorBound (eps = 0)"
272 > val t = str2term "solutions L";
273 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
277 > val t = (term_of o the o (parse thy)) "testdscforlist [#1]";
278 > val (d,ts) = split_dts t;
279 > comp_dts thy (d,ts);
280 val it = "testdscforlist [#1]" : cterm
282 > val t = (term_of o the o (parse thy)) "(A::real)";
283 > val (d,ts) = split_dts t;
284 val d = Const ("empty","empty") : term
285 val ts = [Free ("A","RealDef.real")] : term list
286 > val t = (term_of o the o (parse thy)) "[R=(R::real)]";
287 > val (d,ts) = split_dts t;
288 val d = Const ("empty","empty") : term
289 val ts = [Const # $ Free # $ Free (#,#)] : term list
290 > val t = (term_of o the o (parse thy)) "[#1,#2]";
291 > val (d,ts) = split_dts t;
292 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
295 (*for input_icalhd 11.03*)
296 fun comp_dts'' (d,[]) =
297 if is_reall_dsc d then term2str (d $ e_listReal)
298 else if is_booll_dsc d then term2str (d $ e_listBool)
300 | comp_dts'' (d,ts) = term2str (d $ (comp_ts (d, ts)))
301 handle _ => error ("comp_dts'': "^(term2str d)^
302 " $ "^(term2str (hd ts)));
309 (* this may decompose an object-language isa-list;
310 use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)
311 fun dest_list' t = if is_list t then isalist2list t else [t];
313 (*fun is_metavar (Free (str, _)) =
314 if (last_elem o Symbol.explode) str = "_" then true else false
315 | is_metavar _ = false;*)
316 fun is_var (Free _) = true
319 (*.special handling for lists. ?WN:14.5.03 ??!?*)
320 fun dest_list (d,ts) =
322 if is_list_dsc d andalso not (is_unl d)
323 andalso not (is_var t) (*..for pbt*)
324 then isalist2list t else [t]
325 in (flat o (map dest)) ts end;
328 (*.decompose an input into description, terms (ev. elems of lists),
329 and the value for the problem-environment; inv to comp_dts .*)
330 (*WN.8.6.03: corrected with minimal effort,
331 fn : theory -> term ->
333 term list * lists decomposed for elementwise input
334 term list pbl_ids not _HERE_: dont know which list-elems input*)
335 fun split_dts (t as d $ arg) =
337 if is_list_dsc d andalso is_list arg andalso is_unl d |> not then
338 (d, take_apart arg) else
340 (e_term, dest_list' t)
342 let val t' as (h, _) = strip_comb t;
344 (h, dest_list t') else
345 (e_term, dest_list' t)
348 (* tests see fun comp_dts
350 > val t = str2term "someList []";
351 > val (_,ts) = split_dts thy t; tracing (terms2str ts);
353 > val t = str2term "valuesFor []";
354 > val (_,ts) = split_dts thy t; tracing (terms2str ts);
357 (*.version returning ts only.*)
358 fun split_dts' (d, arg) =
360 then if is_list_dsc d
363 then ([arg]) (*e.g. someList [1,3,2]*)
364 else (take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*)
365 else ([arg]) (*a variable or metavariable for a list*)
367 else (dest_list' arg(*9.01 ???*))
368 | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
369 let val (h,argl) = strip_comb t
370 in if (not o is_dsc) h then (dest_list' t)
371 else (dest_list (h,argl))
378 (*27.8.01: problem-environment
379 WN.6.5.03: FIXXME reconsider if penv is worth the effort --
380 -- just rerun a whole expl with num/var may show the same ?!
381 WN.9.5.03: penv-concept stalled, immediately generate script env !
382 but [#0, epsilon] only outcommented for eventual reconsideration
384 type penv = (term (*err_*)
385 * (term list) (*[#0, epsilon] 9.5.03 outcommented*)
387 fun pen2str ctxt (t, ts) =
388 pair2str (Print_Mode.setmp [] (Syntax.string_of_term ctxt) t,
390 map (Print_Mode.setmp [] (Syntax.string_of_term ctxt))) ts);
391 fun penv2str_ thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv;
394 9.5.03: still unused, but left for eventual future development*)
395 type envv = (int * penv) list; (*over variants*)
397 (*. 14.9.01: not used after putting penv-values into itm_
398 make the result of split_* a value of problem-environment .*)
399 fun mkval dsc [] = error "mkval called with []"
401 | mkval dsc ts = list2isalist ((type_of o hd) ts) ts;
403 fun mkval' x = mkval e_term x;
407 (*. get the constant value from a penv .*)
408 fun getval (id, values) =
410 [] => error ("penv_value: no values in '" ^ term2str id)
412 | (v1::v2::_) => (case v1 of
413 Const ("Script.Arbfix",_) => (id, v2)
416 val e_ = (term_of o the o (parse thy)) "e_::bool";
417 val ev = (term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0";
418 val v_ = (term_of o the o (parse thy)) "v_";
419 val vv = (term_of o the o (parse thy)) "x";
420 val r_ = (term_of o the o (parse thy)) "err_::bool";
421 val rv1 = (term_of o the o (parse thy)) "#0";
422 val rv2 = (term_of o the o (parse thy)) "eps";
424 val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv;
426 [(Free ("e_","bool"),
427 Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#0","RealDef.real")),
428 (Free ("v_","RealDef.real"),Free ("x","RealDef.real")),
429 (Free ("err_","bool"),Free ("#0","RealDef.real"))] : (term * term) list
433 (*==========================================================================
434 23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc
436 (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
437 =(presently) Mis (? should be Inc initially, and Mis after match_itms?)
438 (1.2) Syn,Typ,Sup: not related to oris
439 Syn, Typ (presently) should be accepted in appl_add (instead Error')
440 Sup (presently) should be accepted in appl_add (instead Error')
441 _could_ be w.r.t current vat (and then _is_ related to vat
442 Mis should _not_ be made Inc ((presently, by appl_add & match_itms)
443 - dsc in itm_ is timeconsuming -- keep id for respective queries ?
444 - order of items in ppc should be stable w.r.t order of itms
446 - stepwise input of itms --- match_itms (in one go) ..not coordinated
448 - match_itms / match_itms_oris ..2 versions ?!
449 (fast, for refine / slow, for modeling)
451 - clarify: efficiency <--> simplicity !!!
452 ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc
453 | take int for perserving order of item ppc in itms
454 | make all(!?) handling of itms stable against reordering(?)
455 | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)
456 -"- "#undef" ?= not touched ?= (id,..)
457 -----------------------------------------------------------------
459 def: type pbt = (field, (dsc, pid)) *** design considerations ***
461 (1) fmz + pbt -> oris
462 (2) input + oris -> itm
463 (3) match_itms : schnell(?) f"ur refine
464 match_itms_oris : r"uckmeldung f"ur item ppc
466 (1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)
467 ---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!
469 (3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;
470 wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:
471 (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ????
473 ==========================================================================*)
475 (*the internal representation of a models' item
477 4.9.01: not consistent:
478 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
479 (involves 'is_error');
480 bool in itm really necessary ???*)
482 Cor of (term * (* description *)
483 (term list)) * (* for list: elem-wise input *)
484 (*split_dts <-> comp_dts*)
485 (term * (term list)) (* elem of penv *)
486 (*9.5.03: ---- is already for script -- penv delayed to future*)
489 | Inc of (term * (term list)) * (term * (term list)) (*lists,
490 + init_pbl WN.11.03 FIXXME: empty penv .. bad
491 init_pbl should return Mis !!!*)
492 | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
493 | Mis of (term * term) (* after re-specification pbt-item not found
494 in pbl: only dsc, pid_*)
495 | Par of cterm'; (*internal state from fun parsitm*)
497 type vats = int list; (*variants in formalizations*)
499 (*.data-type for working on pbl/met-ppc:
500 in pbl initially holds descriptions (only) for user guidance.*)
502 int * (* id =0 .. untouched - descript (only) from init
503 23.3.02: seems to correspond to ori (fun insert_ppc)
504 <> maintain order in item ppc?*)
505 vats * (* variants - copy from ori *)
506 bool * (* input on this item is not/complete *)
507 string * (* #Given | #Find | #Relate *)
509 (* use"ME/sequent.sml";
511 val e_itm = (0,[],false,"e_itm",Syn"e_itm"):itm;
512 (*in CalcTree/Subproblem an 'untouched' model is created
513 FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
514 fun untouched (itms: itm list) =
515 foldl and_ (true ,map ((curry op= 0) o #1) itms);
520 > untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")];
521 val it = false : bool*)
527 (* find most frequent variant v in itms *)
529 fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);
531 fun cnt itms v = (v,(length o (filter (curry op= v)) o
532 flat o (map #2)) (itms:itm list));
533 fun vts_cnt vts itms = map (cnt itms) vts;
534 fun max2 [] = error "max2 of []"
536 let fun mx (a,x) [] = (a,x)
537 | mx (a,x) ((b,y)::ys) =
538 if x < y then mx (b,y) ys else mx (a,x) ys;
541 (*. find the variant with most items already input .*)
543 let val vts = (vts_cnt (vts_in itms)) itms;
544 in if vts = [] then 0 else (fst o max2) vts end;
547 (* TODO ev. make more efficient by avoiding flat *)
548 fun mk_e (Cor (_, iv)) = [getval iv]
551 | mk_e (Inc (_, iv)) = [getval iv]
554 fun mk_en vt ((i,vts,b,f,itm_):itm) =
555 if member op = vts vt then mk_e itm_ else [];
556 (*. extract the environment from an item list;
557 takes the variant with most items .*)
559 let val vt = max_vt itms
560 in (flat o (map (mk_en vt))) itms end;
564 (*. example as provided by an author, complete w.r.t. pbt specified
565 not touched by any user action .*)
566 type ori = (int * (* id: 10.3.00ff impl. only <>0 .. touched
567 21.3.02: insert_ppc needs it ! ?:purpose maintain
568 order in item ppc ???*)
569 vats * (* variants 21.3.02: related to pbt..discard ?*)
570 string * (* #Given | #Find | #Relate 21.3.02: discard ?*)
571 term * (* description *)
572 term list (* isalist2list t | [t] *)
574 val e_ori_ = (0,[],"",e_term,[e_term]):ori;
575 val e_ori = (0,[],"",e_term,[e_term]):ori;
577 fun ori2str ((i,vs,fi,t,ts):ori) =
578 "("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^
579 (term2str t)^", "^((strs2str o (map term2str)) ts)^")";
581 let (*val s = !show_types
582 val _ = show_types:= true*)
583 val str = (strs2str' o (map (linefeed o ori2str)))
584 (*val _ = show_types:= s*)
587 (*.an or without leading integer.*)
588 type preori = (vats *
592 fun preori2str ((vs,fi,t,ts):preori) =
593 "("^((strs2str o (map string_of_int)) vs)^", "^fi^", "^
594 (term2str t)^", "^((strs2str o (map term2str)) ts)^")";
595 val preoris2str = (strs2str' o (map (linefeed o preori2str)));
597 (*. given the input value (from split_dts)
598 make the value in a problem-env according to description-type .*)
599 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
600 fun pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v =
602 then [v] (*eg. [r=Arbfix]*)
603 else (case v of (*eg. eps=#0*)
604 (Const ("HOL.eq",_) $ l $ r) => [r,l]
606 error ("pbl_ids Tools.nam: no equality "
607 ^ Print_Mode.setmp [] (Syntax.string_of_term ctxt) v))
608 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v]
609 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v]
610 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v]
611 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v]
612 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v]
613 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v]
615 error ("pbl_ids: not implemented for " ^ term2str v);
617 val t as t1 $ t2 = str2term "antiDerivativeName M_b";
620 val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
621 val (d,argl) = strip_comb t;
622 is_dsc d; (*see split_dts*)
627 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
628 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
630 val (dsc,vl) = (split_dts o term_of o the o (parse thy)) "solveFor x";
631 val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term
632 val vl = Free ("x","RealDef.real") : term
634 val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
636 val it = [Free ("x","RealDef.real")] : term list
638 val (dsc,vl) = (split_dts o term_of o the o(parse thy))
639 "errorBound (eps=#0)";
640 val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_";
642 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *)
644 (*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))
645 make the value in a problem-env according to description-type .*)
646 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
647 fun pbl_ids' (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) vs =
649 [] => error ("pbl_ids' Tools.nam called with []")
650 | [t] => (case t of (*eg. eps=#0*)
651 (Const ("HOL.eq",_) $ l $ r) => [r,l]
653 error ("pbl_ids' Tools.nam: no equality " ^ term2str t))
654 | vs' => vs (*14.9.01: ???TODO *))
655 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs
656 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs
657 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs
658 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs
659 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))vs = vs
660 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))vs = vs
662 error ("pbl_ids': not implemented for " ^ terms2str vs);
663 (*9.5.03 penv postponed: pbl_ids'*)
664 fun pbl_ids' d vs = [comp_ts (d, vs)];
667 (*14.9.01: not used after putting values for penv into itm_
668 WN.5.5.03: used in upd .. upd_envv*)
669 fun upd_penv ctxt penv dsc (id, vl) =
670 (tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
671 tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
672 tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
673 overwrite (penv, (id, pbl_ids ctxt dsc vl))
677 val (dsc,vl) = (split_did o term_of o the o (parse thy)) "solveFor x";
678 val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
679 val penv = upd_penv thy penv dsc (id, vl);
680 [(Free ("v_","RealDef.real"),
681 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")])]
682 : (term * term list) list
684 val (dsc,vl) = (split_did o term_of o the o(parse thy))"errorBound (eps=#0)";
685 val (dsc,id) = (split_did o term_of o the o(parse thy))"errorBound err_";
686 upd_penv thy penv dsc (id, vl);
687 [(Free ("v_","RealDef.real"),
688 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")]),
689 (Free ("err_","bool"),
690 [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")])]
691 : (term * term list) list ^.........!!!!
694 (*WN.9.5.03: not reconsidered; looks strange !!!*)
695 fun upd thy envv dsc (id, vl) i =
696 let val penv = case assoc (envv, i) of
699 val penv' = upd_penv thy penv dsc (id, vl);
703 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
704 val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";
705 val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";
706 upd thy envv dsc (id, vl) i;
707 val it = (2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])
708 : int * (term * term list) list*)
711 (*14.9.01: not used after putting pre-penv into itm_*)
712 fun upd_envv thy (envv:envv) (vats:vats) dsc id vl =
713 let val vats = if length vats = 0
714 then (*unknown id to _all_ variants*)
715 if length envv = 0 then [1]
716 else (intsto o length) envv
718 fun isin vats (i,_) = member op = vats i;
719 val envs_notin_vat = filter_out (isin vats) envv;
720 in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end;
722 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
725 val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";
726 val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";
727 val envv = upd_envv thy envv vats dsc id vl;
728 val envv = [(2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])]
729 : (int * (term * term list) list) list
732 val (dsc,vl) = (split_did o term_of o the o(parse thy))"maximum A";
733 val (dsc,id) = (split_did o term_of o the o(parse thy))"maximum m_";
734 upd_envv thy envv vats dsc id vl;
735 [(1,[(Free ("m_","bool"),[Free ("A","bool")])]),
737 [(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")]),
738 (Free ("m_","bool"),[Free ("A","bool")])]),
739 (3,[(Free ("m_","bool"),[Free ("A","bool")])])]
740 : (int * (term * term list) list) list
744 val (d,ts) = (split_dts o term_of o the o (parse thy))
745 "fixedValues [r=Arbfix]";
746 val (_,id) = (split_did o term_of o the o (parse thy))"fixedValues fix_";
748 val env = upd_envv thy env vats d id (mkval ts);
751 (*. update envv by folding from a list of arguments .*)
752 fun upds_envv thy envv [] = envv
753 | upds_envv thy envv ((vs, dsc, id, vl)::ps) =
754 upds_envv thy (upd_envv thy envv vs dsc id vl) ps;
755 (* eval test-maximum.sml until Specify_Method ...
756 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
757 val met = (#ppc o get_met) mI;
760 val eargs = flat eargs;
761 val (vs, dsc, id, vl) = hd eargs;
762 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
764 val (vs, dsc, id, vl) = hd (tl eargs);
765 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
767 val (vs, dsc, id, vl) = hd (tl (tl eargs));
768 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
770 val (vs, dsc, id, vl) = hd (tl (tl (tl eargs)));
771 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
773 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
774 (Free ("m_","bool"),[Free (#,#)]),
775 (Free ("vs_","bool List.list"),[# $ # $ Const #]),
776 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
778 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
779 (Free ("m_","bool"),[Free (#,#)]),
780 (Free ("vs_","bool List.list"),[# $ # $ Const #]),
781 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
783 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
784 (Free ("m_","bool"),[Free (#,#)]),
785 (Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *)
787 (*for _output_ of the items of a Model*)
789 Correct of cterm' (*labels a correct formula (type cterm')*)
790 | SyntaxE of string (**)
791 | TypeE of string (**)
792 | False of cterm' (*WN050618 notexistent in itm_: only used in Where*)
793 | Incompl of cterm' (**)
794 | Superfl of string (**)
796 fun item2str (Correct s) ="Correct " ^ s
797 | item2str (SyntaxE s) ="SyntaxE " ^ s
798 | item2str (TypeE s) ="TypeE " ^ s
799 | item2str (False s) ="False " ^ s
800 | item2str (Incompl s) ="Incompl " ^ s
801 | item2str (Superfl s) ="Superfl " ^ s
802 | item2str (Missing s) ="Missing " ^ s;
803 (*make string for error-msgs*)
804 fun itm_2str_ ctxt (Cor ((d,ts), penv)) =
806 Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)) ^
807 " ," ^ pen2str ctxt penv
808 | itm_2str_ ctxt (Syn c) = "Syn " ^ c
809 | itm_2str_ ctxt (Typ c) = "Typ " ^ c
810 | itm_2str_ ctxt (Inc ((d,ts), penv)) =
812 Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)) ^
813 " ," ^ pen2str ctxt penv
814 | itm_2str_ ctxt (Sup (d,ts)) =
816 Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts))
817 | itm_2str_ ctxt (Mis (d,pid))=
818 "Mis "^ Print_Mode.setmp [] (Syntax.string_of_term ctxt) d ^
819 " " ^ Print_Mode.setmp [] (Syntax.string_of_term ctxt) pid
820 | itm_2str_ ctxt (Par s) = "Trm "^s;
821 fun itm_2str t = itm_2str_ (thy2ctxt' "Isac") t;
822 fun itm2str_ ctxt ((i,is,b,s,itm_):itm) =
823 "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^
824 s^" ,"^(itm_2str_ ctxt itm_)^")";
825 fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
826 fun w_itms2str_ ctxt itms = tracing (itms2str_ ctxt itms);
828 fun init_item str = SyntaxE str;
839 fun ppc2str {Given=Given,Where=Where,Find=Find,With=With,Relate=Relate}=
840 ("{Given =" ^ (strs2str Given ) ^
841 ",Where=" ^ (strs2str Where) ^
842 ",Find =" ^ (strs2str Find ) ^
843 ",With =" ^ (strs2str With ) ^
844 ",Relate=" ^ (strs2str Relate) ^ "}");
849 fun item_ppc ({Given = gi,Where= wh,
850 Find = fi,With = wi,Relate= re}: string ppc) =
851 {Given = map init_item gi,Where= map init_item wh,
852 Find = map init_item fi,With = map init_item wi,
853 Relate= map init_item re}:item ppc;
854 fun itemppc2str ({Given=Given,Where=Where,
855 Find=Find,With=With,Relate=Relate}:item ppc)=
856 ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
857 ",Where=" ^ ((strs2str' o (map item2str)) Where) ^
858 ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
859 ",With =" ^ ((strs2str' o (map item2str)) With ) ^
860 ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
862 fun de_item (Correct x) = x
863 | de_item (SyntaxE x) = x
864 | de_item (TypeE x) = x
865 | de_item (False x) = x
866 | de_item (Incompl x) = x
867 | de_item (Superfl x) = x
868 | de_item (Missing x) = x;
869 val empty_ppc ={Given = [],
873 Relate= []}:item ppc;
874 val empty_ppc_ct' ={Given = [],
878 Relate= []}:cterm' ppc;
882 Matches of pblID * item ppc
883 | NoMatch of pblID * item ppc;
884 fun match2str (Matches (pI, ppc)) =
885 "Matches ("^(strs2str pI)^", "^(itemppc2str ppc)^")"
886 | match2str(NoMatch (pI, ppc)) =
887 "NoMatch ("^(strs2str pI)^", "^(itemppc2str ppc)^")";
888 fun matchs2str ms = (strs2str o (map match2str)) ms;
889 fun pblID_of_match (Matches (pI,_)) = pI
890 | pblID_of_match (NoMatch (pI,_)) = pI;
892 (*10.03 for Refine_Problem*)
894 Match_ of pblID * ((itm list) * ((bool * term) list))
897 (*. the refined pbt is the last_element Matches in the list .*)
898 fun is_matches (Matches _) = true
899 | is_matches _ = false;
900 fun matches_pblID (Matches (pI,_)) = pI;
901 fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms)
902 handle _ => []:pblID;
903 fun refined_IDitms ms = ((find_first is_matches) o rev) ms;
905 (*. the refined pbt is the last_element Matches in the list,
906 for Refine_Problem, tryrefine .*)
907 fun is_matches_ (Match_ _) = true
908 | is_matches_ _ = false;
909 fun refined_ ms = ((find_first is_matches_) o rev) ms;
912 fun ts_in (Cor ((_,ts),_)) = ts
913 | ts_in (Syn (c)) = []
914 | ts_in (Typ (c)) = []
915 | ts_in (Inc ((_,ts),_)) = ts
916 | ts_in (Sup (_,ts)) = ts
917 | ts_in (Mis _) = [];
919 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
920 val unique = (term_of o the o (parse (Thy_Info.get_theory "Real"))) "UnIqE_tErM";
921 fun d_in (Cor ((d,_),_)) = d
922 | d_in (Syn (c)) = (tracing("*** d_in: Syn ("^c^")"); unique)
923 | d_in (Typ (c)) = (tracing("*** d_in: Typ ("^c^")"); unique)
924 | d_in (Inc ((d,_),_)) = d
925 | d_in (Sup (d,_)) = d
926 | d_in (Mis (d,_)) = d;
928 fun dts2str (d,ts) = pair2str (term2str d, terms2str ts);
929 fun penvval_in (Cor ((d,_),(_,ts))) = [comp_ts (d,ts)]
930 | penvval_in (Syn (c)) = (tracing("*** penvval_in: Syn ("^c^")"); [])
931 | penvval_in (Typ (c)) = (tracing("*** penvval_in: Typ ("^c^")"); [])
932 | penvval_in (Inc (_,(_,ts))) = ts
933 | penvval_in (Sup dts) = (tracing("*** penvval_in: Sup "^(dts2str dts)); [])
934 | penvval_in (Mis (d,t)) = (tracing("*** penvval_in: Mis "^
935 (pair2str(term2str d, term2str t))); []);
938 (*. check a predicate labelled with indication of incomplete substitution;
939 rls -> (*for eval_true*)
940 bool * (*have _all_ variables(Free) from the model-pattern
941 been substituted by a value from the pattern's environment ?*)
942 term (*the precondition*)
944 bool * (*has the precondition evaluated to true*)
945 term (*the precondition (for map)*)
947 fun evalprecond prls (false, pre) =
948 (*NOT ALL Free's have been substituted, eg. because of incomplete model*)
950 | evalprecond prls (true, pre) =
951 (* val (prls, pre) = (prls, hd pres');
952 val (prls, pre) = (prls, hd (tl pres'));
954 if eval_true (assoc_thy "Isac") (*for Pattern.match *)
955 [pre] prls (*pre parsed, prls.thy*)
959 fun pre2str (b, t) = pair2str(bool2str b, term2str t);
960 fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
962 (* check preconditions, return true if all true *)
963 fun check_preconds' _ [] _ _ = [] (*empty preconditions are true*)
964 | check_preconds' prls pres pbl _(*FIXME.WN0308 mvat re-introduce*) =
965 let val env = mk_env pbl;
966 val pres' = map (subst_atomic_all env) pres;
967 in map (evalprecond prls) pres' end;
969 fun check_preconds thy prls pres pbl =
970 check_preconds' prls pres pbl (max_vt pbl);
972 fun declare_constraints' ts ctxt =
973 fold Variable.declare_constraints (flat (map vars ts)) ctxt;
974 (*WN110613 fun declare_constraints' shall replace fun declare_constraints*)
975 fun declare_constraints t ctxt =
977 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
978 (_, _::_) => (Free (v,T)::get_vars vs)
979 | (_, [] ) => get_vars vs) (*filter out nums as long as
980 we have Free ("123",_)*)
982 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
983 in fold Variable.declare_constraints ts ctxt end;
989 structure ContextData = Proof_Data
990 (type T = Isac_Ctxt list
994 fun unpack_asms (Asm t::ts) = t::(unpack_asms ts)
995 | unpack_asms (Env _::ts) = unpack_asms ts
996 | unpack_asms [] = [];
997 fun unpack_envs (Env t::ts) = t::(unpack_envs ts)
998 | unpack_envs (Asm _::ts) = unpack_envs ts
999 | unpack_envs [] = [];
1001 fun get_assumptions ctxt = ContextData.get ctxt |> unpack_asms;
1002 fun get_environments ctxt = ContextData.get ctxt |> unpack_envs;
1006 fun insert_ctxt data = ContextData.map (fn xs => distinct (data@xs));
1008 fun insert_assumptions asms = map (fn t => Asm t) asms |> insert_ctxt;
1009 fun insert_environments envs = map (fn t => Env t) envs |> insert_ctxt;
1012 (* transfer assumptions from one to another ctxt.
1013 do NOT respect scope: in a calculation identifiers are unique.
1014 but environments are scoped as usual in Luacs-interpretation.
1015 WN110520 redo (1) take declare_constraints (2) with combinators*)
1016 fun transfer_asms_from_to from_ctxt to_ctxt =
1018 val to_vars = get_assumptions to_ctxt |> map vars |> flat
1019 fun transfer [] to_ctxt = to_ctxt
1020 | transfer (from_asm::fas) to_ctxt =
1021 if inter op = (vars from_asm) to_vars = []
1022 then transfer fas to_ctxt
1023 else transfer fas (insert_assumptions [from_asm] to_ctxt)
1024 in transfer (get_assumptions from_ctxt) to_ctxt end
1026 (* exported from a subproblem to the context of the calling method:
1027 # 'scrval': the result of script interpretation and
1028 # those assumptions in the subproblem wich contain a variable known
1029 in the calling method. *)
1030 fun from_subpbl_to_caller sub_ctxt scrval caller_ctxt =
1031 let val caller_ctxt = (scrval |> dest_list' |> insert_assumptions) caller_ctxt
1032 in transfer_asms_from_to sub_ctxt caller_ctxt end;
1034 (*----------------------------------------------------------*)
1037 (*----------------------------------------------------------*)