1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/MathEngBasic/model.sml Sat Oct 26 13:03:16 2019 +0200
1.3 @@ -0,0 +1,470 @@
1.4 +(* Title: Model for (sub-)calculations.
1.5 + Various representations: item and ppc for frontend, itm_ and itm for internal functions.
1.6 + The former are related to structure Specify, the latter to structure Chead --
1.7 + -- apt to re-arrangement of structures
1.8 + Author: Walther Neuper 170207
1.9 + (c) due to copyright terms
1.10 +*)
1.11 +
1.12 +signature MODEL =
1.13 +sig
1.14 + type ori
1.15 + val oris2str : ori list -> string
1.16 + val e_ori : ori
1.17 + datatype item
1.18 + = Correct of Rule.cterm' | False of Rule.cterm' | Incompl of Rule.cterm' | Missing of Rule.cterm' | Superfl of string
1.19 + | SyntaxE of string | TypeE of string
1.20 + datatype itm_ = Cor of (term * (term list)) * (term * (term list))
1.21 + | Syn of Rule.cterm' | Typ of Rule.cterm' | Inc of (term * (term list)) * (term * (term list))
1.22 + | Sup of (term * (term list)) | Mis of (term * term) | Par of Rule.cterm'
1.23 + val itm_2str : itm_ -> string
1.24 + val itm_2str_ : Proof.context -> itm_ -> string
1.25 + type itm
1.26 + val itm2str_ : Proof.context -> itm -> string
1.27 + val itms2str_ : Proof.context -> itm list -> string
1.28 + val e_itm : itm
1.29 + type 'a ppc
1.30 + val empty_ppc : item ppc
1.31 + val ppc2str : {Find: string list, Given: string list, Relate: string list, Where: string list,
1.32 + With: string list} -> string
1.33 + val itemppc2str : item ppc -> string
1.34 +
1.35 + type vats
1.36 + val comp_dts : term * term list -> term
1.37 + val comp_dts' : term * term list -> term
1.38 + val comp_dts'' : term * term list -> string
1.39 + val comp_ts : term * term list -> term
1.40 + val split_dts : term -> term * term list
1.41 + val split_dts' : term * term -> term list
1.42 + val pbl_ids' : term -> term list -> term list
1.43 + val mkval' : term list -> term
1.44 +
1.45 + val d_in : itm_ -> term
1.46 + val ts_in : itm_ -> term list
1.47 + val penvval_in : itm_ -> term list
1.48 + val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *)
1.49 + val vars_of : itm list -> term list
1.50 + val max_vt : itm list -> int
1.51 +
1.52 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.53 + type penv
1.54 + val penv2str_ : Proof.context -> penv -> string (* NONE *)
1.55 + type preori
1.56 + val preoris2str : preori list -> string
1.57 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.58 + (* NONE *)
1.59 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.60 +
1.61 +(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
1.62 + val untouched : itm list -> bool
1.63 + type envv
1.64 + val upds_envv : Proof.context -> envv -> (vats * term * term * term) list -> envv
1.65 + val item_ppc : string ppc -> item ppc
1.66 + val all_ts_in : itm_ list -> term list
1.67 + val pres2str : (bool * term) list -> string
1.68 +end
1.69 +
1.70 +structure Model(**) : MODEL(**) =
1.71 +struct
1.72 +(*==========================================================================
1.73 +23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc
1.74 +(1) kinds of itms:
1.75 + (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
1.76 + =(presently) Mis (? should be Inc initially, and Mis after match_itms?)
1.77 + (1.2) Syn,Typ,Sup: not related to oris
1.78 + Syn, Typ (presently) should be accepted in appl_add (instead Error')
1.79 + Sup (presently) should be accepted in appl_add (instead Error')
1.80 + _could_ be w.r.t current vat (and then _is_ related to vat
1.81 + Mis should _not_ be made Inc ((presently, by appl_add & match_itms)
1.82 +- dsc in itm_ is timeconsuming -- keep id for respective queries ?
1.83 +- order of items in ppc should be stable w.r.t order of itms
1.84 +
1.85 +- stepwise input of itms --- match_itms (in one go) ..not coordinated
1.86 + - unify code
1.87 + - match_itms / match_itms_oris ..2 versions ?!
1.88 + (fast, for refine / slow, for modeling)
1.89 +
1.90 +- clarify: efficiency <--> simplicity !!!
1.91 + ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc
1.92 + | take int for perserving order of item ppc in itms
1.93 + | make all(!?) handling of itms stable against reordering(?)
1.94 + | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)
1.95 + -"- "#undef" ?= not touched ?= (id,..)
1.96 +-----------------------------------------------------------------
1.97 +27.3.02:
1.98 +def: type pbt = (field, (dsc, pid)) *** design considerations ***
1.99 +
1.100 +(1) fmz + pbt -> oris
1.101 +(2) input + oris -> itm
1.102 +(3) match_itms : schnell(?) f"ur refine
1.103 + match_itms_oris : r"uckmeldung f"ur item ppc
1.104 +
1.105 +(1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)
1.106 +---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!
1.107 +
1.108 +(3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;
1.109 + wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:
1.110 + (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ????
1.111 + (b)
1.112 +==========================================================================*)
1.113 +
1.114 +val script_parse = the o (@{theory ProgLang} |> Rule.thy2ctxt |> TermC.parseNEW);
1.115 +val e_listReal = script_parse "[]::(real list)";
1.116 +val e_listBool = script_parse "[]::(bool list)";
1.117 +
1.118 +(* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]","[b]"] *)
1.119 +fun take_apart t =
1.120 + let val elems = TermC.isalist2list t
1.121 + in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
1.122 +fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
1.123 + let val elems = (flat o (map TermC.isalist2list)) ts;
1.124 + in TermC.list2isalist (type_of (hd elems)) elems end;
1.125 +
1.126 +fun is_var (Free _) = true
1.127 + | is_var _ = false;
1.128 +
1.129 +(* special handling for lists. ?WN:14.5.03 ??!? *)
1.130 +fun dest_list (d, ts) =
1.131 + let fun dest t =
1.132 + if Input_Descript.is_list_dsc d andalso not (Input_Descript.is_unl d) andalso not (is_var t) (*..for pbt*)
1.133 + then TermC.isalist2list t
1.134 + else [t]
1.135 + in (flat o (map dest)) ts end;
1.136 +
1.137 +(* revert split_dts only for ts; compare comp_dts *)
1.138 +fun comp_ts (d, ts) =
1.139 + if Input_Descript.is_list_dsc d
1.140 + then if TermC.is_list (hd ts)
1.141 + then if Input_Descript.is_unl d
1.142 + then (hd ts) (* e.g. someList [1,3,2] *)
1.143 + else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)
1.144 + else (hd ts) (* a variable or metavariable for a list *)
1.145 + else (hd ts);
1.146 +fun comp_dts (d, []) =
1.147 + if Input_Descript.is_reall_dsc d
1.148 + then (d $ e_listReal)
1.149 + else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
1.150 + | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))
1.151 + handle _ => error ("comp_dts: " ^ Rule.term2str d ^ " $ " ^ Rule.term2str (hd ts));
1.152 +fun comp_dts' (d, []) =
1.153 + if Input_Descript.is_reall_dsc d
1.154 + then (d $ e_listReal)
1.155 + else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
1.156 + | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))
1.157 + handle _ => error ("comp_dts': " ^ Rule.term2str d ^ " $ " ^ Rule.term2str (hd ts));
1.158 +fun comp_dts'' (d, []) =
1.159 + if Input_Descript.is_reall_dsc d
1.160 + then Rule.term2str (d $ e_listReal)
1.161 + else if Input_Descript.is_booll_dsc d
1.162 + then Rule.term2str (d $ e_listBool)
1.163 + else Rule.term2str d
1.164 + | comp_dts'' (d, ts) = Rule.term2str (d $ (comp_ts (d, ts)))
1.165 + handle _ => error ("comp_dts'': " ^ Rule.term2str d ^ " $ " ^ Rule.term2str (hd ts));
1.166 +
1.167 +(* decompose an input into description, terms (ev. elems of lists),
1.168 + and the value for the problem-environment; inv to comp_dts *)
1.169 +fun split_dts (t as d $ arg) =
1.170 + if Input_Descript.is_dsc d
1.171 + then if Input_Descript.is_list_dsc d andalso TermC.is_list arg andalso Input_Descript.is_unl d |> not
1.172 + then (d, take_apart arg)
1.173 + else (d, [arg])
1.174 + else (Rule.e_term, TermC.dest_list' t)
1.175 + | split_dts t =
1.176 + let val t' as (h, _) = strip_comb t;
1.177 + in
1.178 + if Input_Descript.is_dsc h
1.179 + then (h, dest_list t')
1.180 + else (Rule.e_term, TermC.dest_list' t)
1.181 + end;
1.182 +(* version returning ts only *)
1.183 +fun split_dts' (d, arg) =
1.184 + if Input_Descript.is_dsc d
1.185 + then if Input_Descript.is_list_dsc d
1.186 + then if TermC.is_list arg
1.187 + then if Input_Descript.is_unl d
1.188 + then ([arg]) (* e.g. someList [1,3,2] *)
1.189 + else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
1.190 + else ([arg]) (* a variable or metavariable for a list *)
1.191 + else ([arg])
1.192 + else (TermC.dest_list' arg)
1.193 +(* WN170204: Warning "redundant"
1.194 + | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
1.195 + let val (h,argl) = strip_comb t
1.196 + in
1.197 + if (not o is_dsc) h
1.198 + then (dest_list' t)
1.199 + else (dest_list (h,argl))
1.200 + end;*)
1.201 +(* revert split_:
1.202 + WN050903 we do NOT know which is from subtheory, description or term;
1.203 + typecheck thus may lead to TYPE-error 'unknown constant';
1.204 + solution: typecheck with (Thy_Info_get_theory "Isac_Knowledge"); i.e. arg 'thy' superfluous*)
1.205 +(*fun comp_dts thy (d,[]) =
1.206 + Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
1.207 + (Thy_Info_get_theory "Isac_Knowledge")
1.208 + (*comp_dts:FIXXME stay with term for efficiency !!!*)
1.209 + (if is_reall_dsc d then (d $ e_listReal)
1.210 + else if is_booll_dsc d then (d $ e_listBool)
1.211 + else d)
1.212 + | comp_dts (d,ts) =
1.213 + (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
1.214 + (Thy_Info_get_theory "Isac_Knowledge")
1.215 + (*comp_dts:FIXXME stay with term for efficiency !!*)
1.216 + (d $ (comp_ts (d, ts)))
1.217 + handle _ => error ("comp_dts: "^(term2str d)^
1.218 + " $ "^(term2str (hd ts))));*)
1.219 +
1.220 +(* 27.8.01: problem-environment
1.221 +WN.6.5.03: FIXXME reconsider if penv is worth the effort --
1.222 + -- just rerun a whole expl with num/var may show the same ?!
1.223 +WN.9.5.03: penv-concept stalled, immediately generate script env !
1.224 + but [#0, epsilon] only outcommented for eventual reconsideration *)
1.225 +type penv = (* problem-environment *)
1.226 + (term (* err_ *)
1.227 + * (term list) (* [#0, epsilon] 9.5.03 outcommented *)
1.228 + ) list;
1.229 +fun pen2str ctxt (t, ts) =
1.230 + pair2str (Rule.term_to_string' ctxt t, (strs2str' o map (Rule.term_to_string' ctxt)) ts);
1.231 +fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv;
1.232 +
1.233 +(* get the constant value from a penv *)
1.234 +fun getval (id, values) =
1.235 + case values of
1.236 + [] => error ("penv_value: no values in '" ^ Rule.term2str id)
1.237 + | [v] => (id, v)
1.238 + | (v1 :: v2 :: _) => (case v1 of
1.239 + Const ("Program.Arbfix",_) => (id, v2)
1.240 + | _ => (id, v1));
1.241 +
1.242 +(* 9.5.03: still unused, but left for eventual future development *)
1.243 +type envv = (int * penv) list; (* over variants *)
1.244 +
1.245 +(* 14.9.01: not used after putting penv-values into itm_
1.246 + make the result of split_* a value of problem-environment *)
1.247 +fun mkval _(*dsc*) [] = error "mkval called with []"
1.248 + | mkval _ [t] = t
1.249 + | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
1.250 +fun mkval' x = mkval Rule.e_term x;
1.251 +
1.252 +(* the internal representation of a models' item
1.253 + 4.9.01: not consistent:
1.254 + after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
1.255 + (involves 'is_error');
1.256 + bool in itm really necessary ???*)
1.257 +datatype itm_ =
1.258 + Cor of (term * (* description *)
1.259 + (term list)) * (* for list: elem-wise input *)
1.260 + (term * (term list)) (* elem of penv ---- penv delayed to future *)
1.261 +| Syn of Rule.cterm'
1.262 +| Typ of Rule.cterm'
1.263 +| Inc of (term * (term list)) * (term * (term list)) (*lists,
1.264 + + init_pbl WN.11.03 FIXXME: empty penv .. bad; init_pbl should return Mis !!! *)
1.265 +| Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
1.266 +| Mis of (term * term) (* after re-specification pbt-item not found in pbl: only dsc, pid_*)
1.267 +| Par of Rule.cterm'; (* internal state from fun parsitm *)
1.268 +
1.269 +type vats = int list; (* variants in formalizations *)
1.270 +
1.271 +(* data-type for working on pbl/met-ppc:
1.272 + in pbl initially holds descriptions (only) for user guidance *)
1.273 +type itm =
1.274 + int * (* id =0 .. untouched - descript (only) from init
1.275 + seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc? *)
1.276 + vats * (* variants - copy from ori *)
1.277 + bool * (* input on this item is not/complete *)
1.278 + string * (* #Given | #Find | #Relate *)
1.279 + itm_; (* *)
1.280 +val e_itm = (0, [], false, "e_itm", Syn "e_itm");
1.281 +
1.282 +(* in CalcTree/Subproblem an 'untouched' model is created
1.283 + FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
1.284 +fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : itm -> int)) itms);
1.285 +
1.286 +(* find most frequent variant v in itms *)
1.287 +fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);
1.288 +
1.289 +fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map #2)) itms);
1.290 +fun vts_cnt vts itms = map (cnt itms) vts;
1.291 +fun max2 [] = error "max2 of []"
1.292 + | max2 (y :: ys) =
1.293 + let
1.294 + fun mx (a,x) [] = (a,x)
1.295 + | mx (a, x) ((b,y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
1.296 + in mx y ys end;
1.297 +
1.298 +(* find the variant with most items already input *)
1.299 +fun max_vt itms =
1.300 + let val vts = (vts_cnt (vts_in itms)) itms;
1.301 + in if vts = [] then 0 else (fst o max2) vts end;
1.302 +
1.303 +(* TODO ev. make more efficient by avoiding flat *)
1.304 +fun mk_e (Cor (_, iv)) = [getval iv]
1.305 + | mk_e (Syn _) = []
1.306 + | mk_e (Typ _) = []
1.307 + | mk_e (Inc (_, iv)) = [getval iv]
1.308 + | mk_e (Sup _) = []
1.309 + | mk_e (Mis _) = []
1.310 + | mk_e _ = error "mk_e: uncovered case in fun.def.";
1.311 +fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];
1.312 +
1.313 +(* extract the environment from an item list; takes the variant with most items *)
1.314 +fun mk_env itms =
1.315 + let val vt = max_vt itms
1.316 + in (flat o (map (mk_en vt))) itms end;
1.317 +
1.318 +(* example as provided by an author, complete w.r.t. pbt specified
1.319 + not touched by any user action *)
1.320 +type ori =
1.321 + (int * (* id: 10.3.00ff impl. only <>0 .. touched
1.322 + 21.3.02: insert_ppc needs it ! ?:purpose maintain order in item ppc ??? *)
1.323 + vats * (* variants 21.3.02: related to pbt..discard ? *)
1.324 + string * (* #Given | #Find | #Relate 21.3.02: discard ? *)
1.325 + term * (* description *)
1.326 + term list (* isalist2list t | [t] *)
1.327 + );
1.328 +val e_ori = (0, [], "", Rule.e_term, [Rule.e_term]) : ori;
1.329 +
1.330 +fun ori2str (i, vs, fi, t, ts) =
1.331 + "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^
1.332 + Rule.term2str t ^ ", " ^ (strs2str o (map Rule.term2str)) ts ^ ")";
1.333 +val oris2str = strs2str' o (map (Celem.linefeed o ori2str));
1.334 +
1.335 +(* an or without leading integer *)
1.336 +type preori = (vats * string * term * term list);
1.337 +fun preori2str (vs, fi, t, ts) =
1.338 + "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
1.339 + Rule.term2str t ^ ", " ^ (strs2str o (map Rule.term2str)) ts ^ ")";
1.340 +val preoris2str = (strs2str' o (map (Celem.linefeed o preori2str)));
1.341 +
1.342 +(* 9.5.03 penv postponed: pbl_ids' *)
1.343 +fun pbl_ids' d vs = [comp_ts (d, vs)];
1.344 +
1.345 +(* 14.9.01: not used after putting values for penv into itm_
1.346 + WN.5.5.03: used in upd .. upd_envv *)
1.347 +fun upd_penv ctxt penv dsc (id, vl) =
1.348 +(tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
1.349 + tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
1.350 + tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
1.351 + overwrite (penv, (id, Input_Descript.pbl_ids ctxt dsc vl))
1.352 +);
1.353 +
1.354 +(* WN.9.5.03: not reconsidered; looks strange !!!*)
1.355 +fun upd thy envv dsc (id, vl) i =
1.356 + let val penv = case assoc (envv, i) of
1.357 + SOME e => e
1.358 + | NONE => [];
1.359 + val penv' = upd_penv thy penv dsc (id, vl);
1.360 + in (i, penv') end;
1.361 +
1.362 +(* 14.9.01: not used after putting pre-penv into itm_*)
1.363 +fun upd_envv thy envv vats dsc id vl =
1.364 + let val vats = if length vats = 0
1.365 + then (*unknown id to _all_ variants*)
1.366 + if length envv = 0 then [1]
1.367 + else (intsto o length) envv
1.368 + else vats
1.369 + fun isin vats (i, _) = member op = vats i;
1.370 + val envs_notin_vat = filter_out (isin vats) envv;
1.371 + in (map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat end;
1.372 +
1.373 +(* update envv by folding from a list of arguments *)
1.374 +fun upds_envv _ envv [] = envv
1.375 + | upds_envv thy envv ((vs, dsc, id, vl) :: ps) =
1.376 + upds_envv thy (upd_envv thy envv vs dsc id vl) ps;
1.377 +
1.378 +(* for _output_ of the items of a Model *)
1.379 +datatype item =
1.380 + Correct of Rule.cterm' (* labels a correct formula (type cterm') *)
1.381 + | SyntaxE of string (**)
1.382 + | TypeE of string (**)
1.383 + | False of Rule.cterm' (* WN050618 notexistent in itm_: only used in Where *)
1.384 + | Incompl of Rule.cterm' (**)
1.385 + | Superfl of string (**)
1.386 + | Missing of Rule.cterm';
1.387 +fun item2str (Correct s) ="Correct " ^ s
1.388 + | item2str (SyntaxE s) ="SyntaxE " ^ s
1.389 + | item2str (TypeE s) ="TypeE " ^ s
1.390 + | item2str (False s) ="False " ^ s
1.391 + | item2str (Incompl s) ="Incompl " ^ s
1.392 + | item2str (Superfl s) ="Superfl " ^ s
1.393 + | item2str (Missing s) ="Missing " ^ s;
1.394 +(*make string for error-msgs*)
1.395 +fun itm_2str_ ctxt (Cor ((d, ts), penv)) =
1.396 + "Cor " ^ Rule.term_to_string' ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
1.397 + | itm_2str_ _ (Syn c) = "Syn " ^ c
1.398 + | itm_2str_ _ (Typ c) = "Typ " ^ c
1.399 + | itm_2str_ ctxt (Inc ((d, ts), penv)) =
1.400 + "Inc " ^ Rule.term_to_string' ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
1.401 + | itm_2str_ ctxt (Sup (d, ts)) =
1.402 + "Sup " ^ Rule.term_to_string' ctxt (comp_dts (d, ts))
1.403 + | itm_2str_ ctxt (Mis (d, pid)) =
1.404 + "Mis "^ Rule.term_to_string' ctxt d ^ " " ^ Rule.term_to_string' ctxt pid
1.405 + | itm_2str_ _ (Par s) = "Trm "^s;
1.406 +fun itm_2str t = itm_2str_ (Rule.thy2ctxt' "Isac_Knowledge") t;
1.407 +fun itm2str_ ctxt ((i, is, b, s, itm_):itm) =
1.408 + "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
1.409 + s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
1.410 +fun itms2str_ ctxt itms = strs2str' (map (Celem.linefeed o (itm2str_ ctxt)) itms);
1.411 +fun init_item str = SyntaxE str;
1.412 +
1.413 +type 'a ppc =
1.414 + {Given : 'a list, Where: 'a list, Find : 'a list, With : 'a list, Relate: 'a list};
1.415 +fun ppc2str {Given = Given, Where = Where, Find = Find, With = With, Relate = Relate}=
1.416 + "{Given =" ^ strs2str Given ^ ",Where=" ^ strs2str Where ^ ",Find =" ^ strs2str Find ^
1.417 + ",With =" ^ strs2str With ^ ",Relate=" ^ strs2str Relate ^ "}";
1.418 +
1.419 +fun item_ppc {Given = gi, Where= wh, Find = fi, With = wi, Relate= re} =
1.420 + {Given = map init_item gi, Where= map init_item wh, Find = map init_item fi,
1.421 + With = map init_item wi, Relate= map init_item re};
1.422 +fun itemppc2str ({Given=Given,Where=Where,
1.423 + Find=Find,With=With,Relate=Relate}:item ppc)=
1.424 + ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
1.425 + ",Where=" ^ ((strs2str' o (map item2str)) Where) ^
1.426 + ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
1.427 + ",With =" ^ ((strs2str' o (map item2str)) With ) ^
1.428 + ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
1.429 +
1.430 +val empty_ppc = {Given = [], Where= [], Find = [], With = [], Relate= []};
1.431 +
1.432 +fun ts_in (Cor ((_, ts), _)) = ts
1.433 + | ts_in (Syn _) = []
1.434 + | ts_in (Typ _) = []
1.435 + | ts_in (Inc ((_, ts), _)) = ts
1.436 + | ts_in (Sup (_, ts)) = ts
1.437 + | ts_in (Mis _) = []
1.438 + | ts_in _ = error "ts_in: uncovered case in fun.def.";
1.439 +(*WN050629 unused*)
1.440 +fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
1.441 +val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";
1.442 +fun d_in (Cor ((d ,_), _)) = d
1.443 + | d_in (Syn c) = (tracing ("*** d_in: Syn ("^c^")"); unique)
1.444 + | d_in (Typ c) = (tracing ("*** d_in: Typ ("^c^")"); unique)
1.445 + | d_in (Inc ((d, _), _)) = d
1.446 + | d_in (Sup (d, _)) = d
1.447 + | d_in (Mis (d, _)) = d
1.448 + | d_in _ = error "d_in: uncovered case in fun.def.";
1.449 +
1.450 +fun dts2str (d, ts) = pair2str (Rule.term2str d, Rule.terms2str ts);
1.451 +fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)]
1.452 + | penvval_in (Syn (c)) = (tracing("*** penvval_in: Syn ("^c^")"); [])
1.453 + | penvval_in (Typ (c)) = (tracing("*** penvval_in: Typ ("^c^")"); [])
1.454 + | penvval_in (Inc (_, (_, ts))) = ts
1.455 + | penvval_in (Sup dts) = (tracing ("*** penvval_in: Sup "^(dts2str dts)); [])
1.456 + | penvval_in (Mis (d, t)) = (tracing ("*** penvval_in: Mis " ^
1.457 + pair2str(Rule.term2str d, Rule.term2str t)); [])
1.458 + | penvval_in _ = error "penvval_in: uncovered case in fun.def.";
1.459 +
1.460 +(* check a predicate labelled with indication of incomplete substitution;
1.461 + rls -> (* for eval_true *)
1.462 + bool * (* have _all_ variables(Free) from the model-pattern
1.463 + been substituted by a value from the pattern's environment ?*)
1.464 + term -> (* the precondition *)
1.465 + bool * (* has the precondition evaluated to true *)
1.466 + term (* the precondition (for map) *)
1.467 +*)
1.468 +fun pre2str (b, t) = pair2str(bool2str b, Rule.term2str t);
1.469 +fun pres2str pres = strs2str' (map (Celem.linefeed o pre2str) pres);
1.470 +
1.471 +fun vars_of itms = itms |> mk_env |> map snd
1.472 +
1.473 +end;
1.474 \ No newline at end of file