1 (* Title: Model for (sub-)calculations.
2 Various representations: item and ppc for frontend, itm_ and itm for internal functions.
3 The former are related to structure Specify, the latter to structure Chead --
4 -- apt to re-arrangement of structures
5 Author: Walther Neuper 170207
6 (c) due to copyright terms
12 val oris2str : ori list -> string
15 = Correct of Celem.cterm' | False of Celem.cterm' | Incompl of Celem.cterm' | Missing of Celem.cterm' | Superfl of string
16 | SyntaxE of string | TypeE of string
17 datatype itm_ = Cor of (term * (term list)) * (term * (term list))
18 | Syn of Celem.cterm' | Typ of Celem.cterm' | Inc of (term * (term list)) * (term * (term list))
19 | Sup of (term * (term list)) | Mis of (term * term) | Par of Celem.cterm'
20 val itm_2str : itm_ -> string
21 val itm_2str_ : Proof.context -> itm_ -> string
23 val itm2str_ : Proof.context -> itm -> string
24 val itms2str_ : Proof.context -> itm list -> string
27 val empty_ppc : item ppc
28 val ppc2str : {Find: string list, Given: string list, Relate: string list, Where: string list,
29 With: string list} -> string
30 val itemppc2str : item ppc -> string
33 val comp_dts : term * term list -> term
34 val comp_dts' : term * term list -> term
35 val comp_dts'' : term * term list -> string
36 val comp_ts : term * term list -> term
37 val split_dts : term -> term * term list
38 val split_dts' : term * term -> term list
39 val pbl_ids' : term -> term list -> term list
40 val mkval' : term list -> term
42 val d_in : itm_ -> term
43 val ts_in : itm_ -> term list
44 val penvval_in : itm_ -> term list
45 val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *)
46 val max_vt : itm list -> int
48 val dest_list' : term -> term list
50 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
52 val penv2str_ : Proof.context -> penv -> string (* NONE *)
54 val preoris2str : preori list -> string
55 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
57 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
59 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
60 val untouched : itm list -> bool
62 val upds_envv : Proof.context -> envv -> (vats * term * term * term) list -> envv
63 val item_ppc : string ppc -> item ppc
64 val all_ts_in : itm_ list -> term list
65 val pres2str : (bool * term) list -> string
68 structure Model(**) : MODEL(**) =
70 (*==========================================================================
71 23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc
73 (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
74 =(presently) Mis (? should be Inc initially, and Mis after match_itms?)
75 (1.2) Syn,Typ,Sup: not related to oris
76 Syn, Typ (presently) should be accepted in appl_add (instead Error')
77 Sup (presently) should be accepted in appl_add (instead Error')
78 _could_ be w.r.t current vat (and then _is_ related to vat
79 Mis should _not_ be made Inc ((presently, by appl_add & match_itms)
80 - dsc in itm_ is timeconsuming -- keep id for respective queries ?
81 - order of items in ppc should be stable w.r.t order of itms
83 - stepwise input of itms --- match_itms (in one go) ..not coordinated
85 - match_itms / match_itms_oris ..2 versions ?!
86 (fast, for refine / slow, for modeling)
88 - clarify: efficiency <--> simplicity !!!
89 ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc
90 | take int for perserving order of item ppc in itms
91 | make all(!?) handling of itms stable against reordering(?)
92 | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)
93 -"- "#undef" ?= not touched ?= (id,..)
94 -----------------------------------------------------------------
96 def: type pbt = (field, (dsc, pid)) *** design considerations ***
99 (2) input + oris -> itm
100 (3) match_itms : schnell(?) f"ur refine
101 match_itms_oris : r"uckmeldung f"ur item ppc
103 (1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)
104 ---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!
106 (3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;
107 wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:
108 (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ????
110 ==========================================================================*)
112 val script_parse = the o (@{theory Script} |> Celem.thy2ctxt |> TermC.parseNEW);
113 val e_listReal = script_parse "[]::(real list)";
114 val e_listBool = script_parse "[]::(bool list)";
116 (* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]","[b]"] *)
118 let val elems = TermC.isalist2list t
119 in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
120 fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
121 let val elems = (flat o (map TermC.isalist2list)) ts;
122 in TermC.list2isalist (type_of (hd elems)) elems end;
124 fun is_var (Free _) = true
127 (* this may decompose an object-language isa-list;
128 use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)
129 fun dest_list' t = if TermC.is_list t then TermC.isalist2list t else [t];
130 (* special handling for lists. ?WN:14.5.03 ??!? *)
131 fun dest_list (d, ts) =
133 if LTool.is_list_dsc d andalso not (LTool.is_unl d) andalso not (is_var t) (*..for pbt*)
134 then TermC.isalist2list t
136 in (flat o (map dest)) ts end;
138 (* revert split_dts only for ts; compare comp_dts *)
139 fun comp_ts (d, ts) =
140 if LTool.is_list_dsc d
141 then if TermC.is_list (hd ts)
142 then if LTool.is_unl d
143 then (hd ts) (* e.g. someList [1,3,2] *)
144 else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)
145 else (hd ts) (* a variable or metavariable for a list *)
147 fun comp_dts (d, []) =
148 if LTool.is_reall_dsc d
149 then (d $ e_listReal)
150 else if LTool.is_booll_dsc d then (d $ e_listBool) else d
151 | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))
152 handle _ => error ("comp_dts: " ^ Celem.term2str d ^ " $ " ^ Celem.term2str (hd ts));
153 fun comp_dts' (d, []) =
154 if LTool.is_reall_dsc d
155 then (d $ e_listReal)
156 else if LTool.is_booll_dsc d then (d $ e_listBool) else d
157 | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))
158 handle _ => error ("comp_dts': " ^ Celem.term2str d ^ " $ " ^ Celem.term2str (hd ts));
159 fun comp_dts'' (d, []) =
160 if LTool.is_reall_dsc d
161 then Celem.term2str (d $ e_listReal)
162 else if LTool.is_booll_dsc d
163 then Celem.term2str (d $ e_listBool)
164 else Celem.term2str d
165 | comp_dts'' (d, ts) = Celem.term2str (d $ (comp_ts (d, ts)))
166 handle _ => error ("comp_dts'': " ^ Celem.term2str d ^ " $ " ^ Celem.term2str (hd ts));
168 (* decompose an input into description, terms (ev. elems of lists),
169 and the value for the problem-environment; inv to comp_dts *)
170 fun split_dts (t as d $ arg) =
172 then if LTool.is_list_dsc d andalso TermC.is_list arg andalso LTool.is_unl d |> not
173 then (d, take_apart arg)
175 else (Celem.e_term, dest_list' t)
177 let val t' as (h, _) = strip_comb t;
180 then (h, dest_list t')
181 else (Celem.e_term, dest_list' t)
183 (* version returning ts only *)
184 fun split_dts' (d, arg) =
186 then if LTool.is_list_dsc d
187 then if TermC.is_list arg
188 then if LTool.is_unl d
189 then ([arg]) (* e.g. someList [1,3,2] *)
190 else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
191 else ([arg]) (* a variable or metavariable for a list *)
193 else (dest_list' arg)
194 (* WN170204: Warning "redundant"
195 | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
196 let val (h,argl) = strip_comb t
200 else (dest_list (h,argl))
203 WN050903 we do NOT know which is from subtheory, description or term;
204 typecheck thus may lead to TYPE-error 'unknown constant';
205 solution: typecheck with (Thy_Info_get_theory "Isac"); i.e. arg 'thy' superfluous*)
206 (*fun comp_dts thy (d,[]) =
207 Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac"*)
208 (Thy_Info_get_theory "Isac")
209 (*comp_dts:FIXXME stay with term for efficiency !!!*)
210 (if is_reall_dsc d then (d $ e_listReal)
211 else if is_booll_dsc d then (d $ e_listBool)
214 (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac"*)
215 (Thy_Info_get_theory "Isac")
216 (*comp_dts:FIXXME stay with term for efficiency !!*)
217 (d $ (comp_ts (d, ts)))
218 handle _ => error ("comp_dts: "^(term2str d)^
219 " $ "^(term2str (hd ts))));*)
221 (* 27.8.01: problem-environment
222 WN.6.5.03: FIXXME reconsider if penv is worth the effort --
223 -- just rerun a whole expl with num/var may show the same ?!
224 WN.9.5.03: penv-concept stalled, immediately generate script env !
225 but [#0, epsilon] only outcommented for eventual reconsideration *)
226 type penv = (* problem-environment *)
228 * (term list) (* [#0, epsilon] 9.5.03 outcommented *)
230 fun pen2str ctxt (t, ts) =
231 pair2str (Celem.term_to_string' ctxt t, (strs2str' o map (Celem.term_to_string' ctxt)) ts);
232 fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv;
234 (* get the constant value from a penv *)
235 fun getval (id, values) =
237 [] => error ("penv_value: no values in '" ^ Celem.term2str id)
239 | (v1 :: v2 :: _) => (case v1 of
240 Const ("Script.Arbfix",_) => (id, v2)
243 (* 9.5.03: still unused, but left for eventual future development *)
244 type envv = (int * penv) list; (* over variants *)
246 (* 14.9.01: not used after putting penv-values into itm_
247 make the result of split_* a value of problem-environment *)
248 fun mkval _(*dsc*) [] = error "mkval called with []"
250 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
251 fun mkval' x = mkval Celem.e_term x;
253 (* the internal representation of a models' item
254 4.9.01: not consistent:
255 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
256 (involves 'is_error');
257 bool in itm really necessary ???*)
259 Cor of (term * (* description *)
260 (term list)) * (* for list: elem-wise input *)
261 (term * (term list)) (* elem of penv ---- penv delayed to future *)
262 | Syn of Celem.cterm'
263 | Typ of Celem.cterm'
264 | Inc of (term * (term list)) * (term * (term list)) (*lists,
265 + init_pbl WN.11.03 FIXXME: empty penv .. bad; init_pbl should return Mis !!! *)
266 | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
267 | Mis of (term * term) (* after re-specification pbt-item not found in pbl: only dsc, pid_*)
268 | Par of Celem.cterm'; (* internal state from fun parsitm *)
270 type vats = int list; (* variants in formalizations *)
272 (* data-type for working on pbl/met-ppc:
273 in pbl initially holds descriptions (only) for user guidance *)
275 int * (* id =0 .. untouched - descript (only) from init
276 seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc? *)
277 vats * (* variants - copy from ori *)
278 bool * (* input on this item is not/complete *)
279 string * (* #Given | #Find | #Relate *)
281 val e_itm = (0, [], false, "e_itm", Syn "e_itm");
283 (* in CalcTree/Subproblem an 'untouched' model is created
284 FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
285 fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : itm -> int)) itms);
287 (* find most frequent variant v in itms *)
288 fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);
290 fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map #2)) itms);
291 fun vts_cnt vts itms = map (cnt itms) vts;
292 fun max2 [] = error "max2 of []"
295 fun mx (a,x) [] = (a,x)
296 | mx (a, x) ((b,y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
299 (* find the variant with most items already input *)
301 let val vts = (vts_cnt (vts_in itms)) itms;
302 in if vts = [] then 0 else (fst o max2) vts end;
304 (* TODO ev. make more efficient by avoiding flat *)
305 fun mk_e (Cor (_, iv)) = [getval iv]
308 | mk_e (Inc (_, iv)) = [getval iv]
311 | mk_e _ = error "mk_e: uncovered case in fun.def.";
312 fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];
314 (* extract the environment from an item list; takes the variant with most items *)
316 let val vt = max_vt itms
317 in (flat o (map (mk_en vt))) itms end;
319 (* example as provided by an author, complete w.r.t. pbt specified
320 not touched by any user action *)
322 (int * (* id: 10.3.00ff impl. only <>0 .. touched
323 21.3.02: insert_ppc needs it ! ?:purpose maintain order in item ppc ??? *)
324 vats * (* variants 21.3.02: related to pbt..discard ? *)
325 string * (* #Given | #Find | #Relate 21.3.02: discard ? *)
326 term * (* description *)
327 term list (* isalist2list t | [t] *)
329 val e_ori = (0, [], "", Celem.e_term, [Celem.e_term]) : ori;
331 fun ori2str (i, vs, fi, t, ts) =
332 "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^
333 Celem.term2str t ^ ", " ^ (strs2str o (map Celem.term2str)) ts ^ ")";
334 val oris2str = strs2str' o (map (Celem.linefeed o ori2str));
336 (* an or without leading integer *)
337 type preori = (vats * string * term * term list);
338 fun preori2str (vs, fi, t, ts) =
339 "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
340 Celem.term2str t ^ ", " ^ (strs2str o (map Celem.term2str)) ts ^ ")";
341 val preoris2str = (strs2str' o (map (Celem.linefeed o preori2str)));
343 (* given the input value (from split_dts)
344 make the value in a problem-env according to description-type
345 28.8.01: .nam and .una impl. properly, others copied .. TODO.
346 19/03/15 17:33, Makarius wrote:
347 >>> val i = case HOLogic.dest_number t of
348 >>> (Type ("Nat.nat", []), i) => i
349 >> Formal names should never be hardwired as ML string constants. Use
350 >> @{type_name nat} above, or better @{typ nat} for the whole type *)
351 fun pbl_ids ctxt (Const(_, Type ("fun", [_, Type ("Tools.nam", _)]))) v =
353 then [v] (*eg. [r=Arbfix]*)
355 (case v of (*eg. eps=#0*) (Const ("HOL.eq", _) $ l $ r) => [r, l]
356 | _ => error ("pbl_ids Tools.nam: no equality " ^ Celem.term_to_string' ctxt v))
357 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.una", _)]))) v = [v]
358 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.unl", _)]))) v = [v]
359 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.str", _)]))) v = [v]
360 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.toreal", _)]))) v = [v]
361 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.toreall", _)])))v = [v]
362 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.unknown" ,_)])))v = [v]
363 | pbl_ids _ _ v = error ("pbl_ids: not implemented for " ^ Celem.term2str v);
365 (* given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))
366 make the value in a problem-env according to description-type.
367 28.8.01: .nam and .una impl. properly, others copied .. TODO
368 fun pbl_ids' (Const(_, Type ("fun", [_, Type ("Tools.nam", _)]))) vs =
370 [] => error ("pbl_ids' Tools.nam called with []")
372 (case t of (*eg. eps=#0*)
373 (Const ("HOL.eq",_) $ l $ r) => [r,l]
374 | _ => error ("pbl_ids' Tools.nam: no equality " ^ term2str t))
375 | _ => vs (*14.9.01: ???TODO *))
376 | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.una", _)]))) vs = vs
377 | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.unl", _)]))) vs = vs
378 | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.str", _)]))) vs = vs
379 | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.toreal", _)]))) vs = vs
380 | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.toreall", _)])))vs = vs
381 | pbl_ids' (Const (_, Type ("fun", [_, Type("Tools.unknown", _)])))vs = vs
382 | pbl_ids' _ vs = error ("pbl_ids': not implemented for " ^ terms2str vs);*)
384 (* 9.5.03 penv postponed: pbl_ids' *)
385 fun pbl_ids' d vs = [comp_ts (d, vs)];
387 (* 14.9.01: not used after putting values for penv into itm_
388 WN.5.5.03: used in upd .. upd_envv *)
389 fun upd_penv ctxt penv dsc (id, vl) =
390 (tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
391 tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
392 tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
393 overwrite (penv, (id, pbl_ids ctxt dsc vl))
396 (* WN.9.5.03: not reconsidered; looks strange !!!*)
397 fun upd thy envv dsc (id, vl) i =
398 let val penv = case assoc (envv, i) of
401 val penv' = upd_penv thy penv dsc (id, vl);
404 (* 14.9.01: not used after putting pre-penv into itm_*)
405 fun upd_envv thy envv vats dsc id vl =
406 let val vats = if length vats = 0
407 then (*unknown id to _all_ variants*)
408 if length envv = 0 then [1]
409 else (intsto o length) envv
411 fun isin vats (i, _) = member op = vats i;
412 val envs_notin_vat = filter_out (isin vats) envv;
413 in (map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat end;
415 (* update envv by folding from a list of arguments *)
416 fun upds_envv _ envv [] = envv
417 | upds_envv thy envv ((vs, dsc, id, vl) :: ps) =
418 upds_envv thy (upd_envv thy envv vs dsc id vl) ps;
420 (* for _output_ of the items of a Model *)
422 Correct of Celem.cterm' (* labels a correct formula (type cterm') *)
423 | SyntaxE of string (**)
424 | TypeE of string (**)
425 | False of Celem.cterm' (* WN050618 notexistent in itm_: only used in Where *)
426 | Incompl of Celem.cterm' (**)
427 | Superfl of string (**)
428 | Missing of Celem.cterm';
429 fun item2str (Correct s) ="Correct " ^ s
430 | item2str (SyntaxE s) ="SyntaxE " ^ s
431 | item2str (TypeE s) ="TypeE " ^ s
432 | item2str (False s) ="False " ^ s
433 | item2str (Incompl s) ="Incompl " ^ s
434 | item2str (Superfl s) ="Superfl " ^ s
435 | item2str (Missing s) ="Missing " ^ s;
436 (*make string for error-msgs*)
437 fun itm_2str_ ctxt (Cor ((d, ts), penv)) =
438 "Cor " ^ Celem.term_to_string' ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
439 | itm_2str_ _ (Syn c) = "Syn " ^ c
440 | itm_2str_ _ (Typ c) = "Typ " ^ c
441 | itm_2str_ ctxt (Inc ((d, ts), penv)) =
442 "Inc " ^ Celem.term_to_string' ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
443 | itm_2str_ ctxt (Sup (d, ts)) =
444 "Sup " ^ Celem.term_to_string' ctxt (comp_dts (d, ts))
445 | itm_2str_ ctxt (Mis (d, pid)) =
446 "Mis "^ Celem.term_to_string' ctxt d ^ " " ^ Celem.term_to_string' ctxt pid
447 | itm_2str_ _ (Par s) = "Trm "^s;
448 fun itm_2str t = itm_2str_ (Celem.thy2ctxt' "Isac") t;
449 fun itm2str_ ctxt ((i, is, b, s, itm_):itm) =
450 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
451 s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
452 fun itms2str_ ctxt itms = strs2str' (map (Celem.linefeed o (itm2str_ ctxt)) itms);
453 fun init_item str = SyntaxE str;
456 {Given : 'a list, Where: 'a list, Find : 'a list, With : 'a list, Relate: 'a list};
457 fun ppc2str {Given = Given, Where = Where, Find = Find, With = With, Relate = Relate}=
458 "{Given =" ^ strs2str Given ^ ",Where=" ^ strs2str Where ^ ",Find =" ^ strs2str Find ^
459 ",With =" ^ strs2str With ^ ",Relate=" ^ strs2str Relate ^ "}";
461 fun item_ppc {Given = gi, Where= wh, Find = fi, With = wi, Relate= re} =
462 {Given = map init_item gi, Where= map init_item wh, Find = map init_item fi,
463 With = map init_item wi, Relate= map init_item re};
464 fun itemppc2str ({Given=Given,Where=Where,
465 Find=Find,With=With,Relate=Relate}:item ppc)=
466 ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
467 ",Where=" ^ ((strs2str' o (map item2str)) Where) ^
468 ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
469 ",With =" ^ ((strs2str' o (map item2str)) With ) ^
470 ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
472 val empty_ppc = {Given = [], Where= [], Find = [], With = [], Relate= []};
474 fun ts_in (Cor ((_, ts), _)) = ts
477 | ts_in (Inc ((_, ts), _)) = ts
478 | ts_in (Sup (_, ts)) = ts
480 | ts_in _ = error "ts_in: uncovered case in fun.def.";
482 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
483 val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";
484 fun d_in (Cor ((d ,_), _)) = d
485 | d_in (Syn c) = (tracing ("*** d_in: Syn ("^c^")"); unique)
486 | d_in (Typ c) = (tracing ("*** d_in: Typ ("^c^")"); unique)
487 | d_in (Inc ((d, _), _)) = d
488 | d_in (Sup (d, _)) = d
489 | d_in (Mis (d, _)) = d
490 | d_in _ = error "d_in: uncovered case in fun.def.";
492 fun dts2str (d, ts) = pair2str (Celem.term2str d, Celem.terms2str ts);
493 fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)]
494 | penvval_in (Syn (c)) = (tracing("*** penvval_in: Syn ("^c^")"); [])
495 | penvval_in (Typ (c)) = (tracing("*** penvval_in: Typ ("^c^")"); [])
496 | penvval_in (Inc (_, (_, ts))) = ts
497 | penvval_in (Sup dts) = (tracing ("*** penvval_in: Sup "^(dts2str dts)); [])
498 | penvval_in (Mis (d, t)) = (tracing ("*** penvval_in: Mis " ^
499 pair2str(Celem.term2str d, Celem.term2str t)); [])
500 | penvval_in _ = error "penvval_in: uncovered case in fun.def.";
502 (* check a predicate labelled with indication of incomplete substitution;
503 rls -> (* for eval_true *)
504 bool * (* have _all_ variables(Free) from the model-pattern
505 been substituted by a value from the pattern's environment ?*)
506 term -> (* the precondition *)
507 bool * (* has the precondition evaluated to true *)
508 term (* the precondition (for map) *)
510 fun pre2str (b, t) = pair2str(bool2str b, Celem.term2str t);
511 fun pres2str pres = strs2str' (map (Celem.linefeed o pre2str) pres);