1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Interpret/mstools.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,969 @@
1.4 +(* Types and tools for 'modeling' und 'specifying' to be used in
1.5 + modspec.sml. The types are separated from calchead.sml into this file,
1.6 + because some of them are stored in the calc-tree, and thus are required
1.7 + _before_ ctree.sml.
1.8 + author: Walther Neuper
1.9 + (c) due to copyright terms
1.10 +
1.11 +use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*);
1.12 +use"mstools.sml";
1.13 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.14 + 10 20 30 40 50 60 70 80
1.15 +*)
1.16 +
1.17 +signature SPECIFY_TOOLS =
1.18 + sig
1.19 + type envv
1.20 + datatype
1.21 + item =
1.22 + Correct of cterm'
1.23 + | False of cterm'
1.24 + | Incompl of cterm'
1.25 + | Missing of cterm'
1.26 + | Superfl of string
1.27 + | SyntaxE of string
1.28 + | TypeE of string
1.29 + val item2str : item -> string
1.30 + type itm
1.31 + val itm2str_ : Proof.context -> itm -> string
1.32 + datatype
1.33 + itm_ =
1.34 + Cor of (term * term list) * (term * term list)
1.35 + | Inc of (term * term list) * (term * term list)
1.36 + | Mis of term * term
1.37 + | Par of cterm'
1.38 + | Sup of term * term list
1.39 + | Syn of cterm'
1.40 + | Typ of cterm'
1.41 + val itm_2str : itm_ -> string
1.42 + val itm_2str_ : Proof.context -> itm_ -> string
1.43 + val itms2str_ : Proof.context -> itm list -> string
1.44 + type 'a ppc
1.45 + val ppc2str :
1.46 + {Find: string list, With: string list, Given: string list,
1.47 + Where: string list, Relate: string list} -> string
1.48 + datatype
1.49 + match =
1.50 + Matches of pblID * item ppc
1.51 + | NoMatch of pblID * item ppc
1.52 + val match2str : match -> string
1.53 + datatype
1.54 + match_ =
1.55 + Match_ of pblID * (itm list * (bool * term) list)
1.56 + | NoMatch_
1.57 + val matchs2str : match list -> string
1.58 + type ori
1.59 + val ori2str : ori -> string
1.60 + val oris2str : ori list -> string
1.61 + type preori
1.62 + val preori2str : preori -> string
1.63 + val preoris2str : preori list -> string
1.64 + type penv
1.65 + (* val penv2str_ : Proof.context -> penv -> string *)
1.66 + type vats
1.67 + (*----------------------------------------------------------------------*)
1.68 + val all_ts_in : itm_ list -> term list
1.69 + val check_preconds :
1.70 + 'a ->
1.71 + rls ->
1.72 + term list -> itm list -> (bool * term) list
1.73 + val check_preconds' :
1.74 + rls ->
1.75 + term list ->
1.76 + itm list -> 'a -> (bool * term) list
1.77 + (* val chkpre2item : rls -> term -> bool * item *)
1.78 + val pres2str : (bool * term) list -> string
1.79 + (* val evalprecond : rls -> term -> bool * term *)
1.80 + (* val cnt : itm list -> int -> int * int *)
1.81 + val comp_dts : theory -> term * term list -> term
1.82 + val comp_dts' : term * term list -> term
1.83 + val comp_dts'' : term * term list -> string
1.84 + val comp_ts : term * term list -> term
1.85 + val d_in : itm_ -> term
1.86 + val de_item : item -> cterm'
1.87 + val dest_list : term * term list -> term list (* for testing *)
1.88 + val dest_list' : term -> term list
1.89 + val dts2str : term * term list -> string
1.90 + val e_itm : itm
1.91 + (* val e_listBool : term *)
1.92 + (* val e_listReal : term *)
1.93 + val e_ori : ori
1.94 + val e_ori_ : ori
1.95 + val empty_ppc : item ppc
1.96 + (* val empty_ppc_ct' : cterm' ppc *)
1.97 + (* val getval : term * term list -> term * term *)
1.98 + (*val head_precond :
1.99 + domID * pblID * 'a ->
1.100 + term option ->
1.101 + rls ->
1.102 + term list ->
1.103 + itm list -> 'b -> term * (bool * term) list*)
1.104 + (* val init_item : string -> item *)
1.105 + (* val is_matches : match -> bool *)
1.106 + (* val is_matches_ : match_ -> bool *)
1.107 + val is_var : term -> bool
1.108 + (* val item_ppc :
1.109 + string ppc -> item ppc *)
1.110 + val itemppc2str : item ppc -> string
1.111 + (* val matches_pblID : match -> pblID *)
1.112 + val max2 : ('a * int) list -> 'a * int
1.113 + val max_vt : itm list -> int
1.114 + val mk_e : itm_ -> (term * term) list
1.115 + val mk_en : int -> itm -> (term * term) list
1.116 + val mk_env : itm list -> (term * term) list
1.117 + val mkval : 'a -> term list -> term
1.118 + val mkval' : term list -> term
1.119 + (* val pblID_of_match : match -> pblID *)
1.120 + val pbl_ids : Proof.context -> term -> term -> term list
1.121 + val pbl_ids' : 'a -> term -> term list -> term list
1.122 + (* val pen2str : theory -> term * term list -> string *)
1.123 + val penvval_in : itm_ -> term list
1.124 + val refined : match list -> pblID
1.125 + val refined_ :
1.126 + match_ list -> match_ option
1.127 + (* val refined_IDitms :
1.128 + match list -> match option *)
1.129 + val split_dts : 'a -> term -> term * term list
1.130 + val split_dts' : term * term -> term list
1.131 + (* val take_apart : term -> term list *)
1.132 + (* val take_apart_inv : term list -> term *)
1.133 + val ts_in : itm_ -> term list
1.134 + (* val unique : term *)
1.135 + val untouched : itm list -> bool
1.136 + val upd :
1.137 + Proof.context ->
1.138 + (''a * (''b * term list) list) list ->
1.139 + term ->
1.140 + ''b * term -> ''a -> ''a * (''b * term list) list
1.141 + val upd_envv :
1.142 + Proof.context ->
1.143 + envv ->
1.144 + vats ->
1.145 + term -> term -> term -> envv
1.146 + val upd_penv :
1.147 + Proof.context ->
1.148 + (''a * term list) list ->
1.149 + term -> ''a * term -> (''a * term list) list
1.150 + (* val upds_envv :
1.151 + Proof.context ->
1.152 + envv ->
1.153 + (vats * term * term * term) list ->
1.154 + envv *)
1.155 + val vts_cnt : int list -> itm list -> (int * int) list
1.156 + val vts_in : itm list -> int list
1.157 + (* val w_itms2str_ : Proof.context -> itm list -> unit *)
1.158 + end
1.159 +
1.160 +(*----------------------------------------------------------*)
1.161 +structure SpecifyTools : SPECIFY_TOOLS =
1.162 +struct
1.163 +(*----------------------------------------------------------*)
1.164 +val e_listReal = (term_of o the o (parse (theory "Script"))) "[]::(real list)";
1.165 +val e_listBool = (term_of o the o (parse (theory "Script"))) "[]::(bool list)";
1.166 +
1.167 +(*.take list-term apart w.r.t. handling elementwise input.*)
1.168 +fun take_apart t =
1.169 + let val elems = isalist2list t
1.170 + in map ((list2isalist (type_of (hd elems))) o single) elems end;
1.171 +(*val t = str2term "[a, b]";
1.172 +> val ts = take_apart t; writeln (terms2str ts);
1.173 +["[a]","[b]"]
1.174 +
1.175 +> t = (take_apart_inv o take_apart) t;
1.176 +true*)
1.177 +fun take_apart_inv ts =
1.178 + let val elems = (flat o (map isalist2list)) ts;
1.179 + in list2isalist (type_of (hd elems)) elems end;
1.180 +(*val ts = [str2term "[a]", str2term "[b]"];
1.181 +> val t = take_apart_inv ts; term2str t;
1.182 +"[a, b]"
1.183 +
1.184 +ts = (take_apart o take_apart_inv) ts;
1.185 +true*)
1.186 +
1.187 +
1.188 +
1.189 +
1.190 +(*.revert split_dts only for ts; compare comp_dts.*)
1.191 +fun comp_ts (d, ts) =
1.192 + if is_list_dsc d
1.193 + then if is_list (hd ts)
1.194 + then if is_unl d
1.195 + then (hd ts) (*e.g. someList [1,3,2]*)
1.196 + else (take_apart_inv ts)
1.197 + (* SML[ [a], [b] ]SML --> [a,b] *)
1.198 + else (hd ts) (*a variable or metavariable for a list*)
1.199 + else (hd ts);
1.200 +(*.revert split_.
1.201 + WN050903 we do NOT know which is from subtheory, description or term;
1.202 + typecheck thus may lead to TYPE-error 'unknown constant';
1.203 + solution: typecheck with Isac.thy; i.e. arg 'thy' superfluous*)
1.204 +(*fun comp_dts thy (d,[]) =
1.205 + cterm_of (*(sign_of o assoc_thy) "Isac.thy"*)
1.206 + (theory "Isac")
1.207 + (*comp_dts:FIXXME stay with term for efficiency !!!*)
1.208 + (if is_reall_dsc d then (d $ e_listReal)
1.209 + else if is_booll_dsc d then (d $ e_listBool)
1.210 + else d)
1.211 + | comp_dts thy (d,ts) =
1.212 + (cterm_of (*(sign_of o assoc_thy) "Isac.thy"*)
1.213 + (theory "Isac")
1.214 + (*comp_dts:FIXXME stay with term for efficiency !!*)
1.215 + (d $ (comp_ts (d, ts)))
1.216 + handle _ => raise error ("comp_dts: "^(term2str d)^
1.217 + " $ "^(term2str (hd ts))));*)
1.218 +fun comp_dts thy (d,[]) =
1.219 + (if is_reall_dsc d then (d $ e_listReal)
1.220 + else if is_booll_dsc d then (d $ e_listBool)
1.221 + else d)
1.222 + | comp_dts thy (d,ts) =
1.223 + (d $ (comp_ts (d, ts)))
1.224 + handle _ => raise error ("comp_dts: "^(term2str d)^
1.225 + " $ "^(term2str (hd ts)));
1.226 +(*25.8.03*)
1.227 +fun comp_dts' (d,[]) =
1.228 + if is_reall_dsc d then (d $ e_listReal)
1.229 + else if is_booll_dsc d then (d $ e_listBool)
1.230 + else d
1.231 + | comp_dts' (d,ts) = (d $ (comp_ts (d, ts)))
1.232 + handle _ => raise error ("comp_dts': "^(term2str d)^
1.233 + " $ "^(term2str (hd ts)));
1.234 +(*val t = str2term "maximum A";
1.235 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.236 +val it = "maximum A" : cterm
1.237 +> val t = str2term "fixedValues [r=Arbfix]";
1.238 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.239 +"fixedValues [r = Arbfix]"
1.240 +> val t = str2term "valuesFor [a]";
1.241 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.242 +"valuesFor [a]"
1.243 +> val t = str2term "valuesFor [a,b]";
1.244 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.245 +"valuesFor [a, b]"
1.246 +> val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]";
1.247 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.248 +relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"
1.249 +> val t = str2term "boundVariable a";
1.250 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.251 +"boundVariable a"
1.252 +> val t = str2term "interval {x::real. 0 <= x & x <= 2*r}";
1.253 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.254 +"interval {x. 0 <= x & x <= 2 * r}"
1.255 +
1.256 +> val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))";
1.257 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.258 +"equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
1.259 +> val t = str2term "solveFor x";
1.260 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.261 +"solveFor x"
1.262 +> val t = str2term "errorBound (eps=0)";
1.263 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.264 +"errorBound (eps = 0)"
1.265 +> val t = str2term "solutions L";
1.266 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.267 +"solutions L"
1.268 +
1.269 +before 6.5.03:
1.270 +> val t = (term_of o the o (parse thy)) "testdscforlist [#1]";
1.271 +> val (d,ts) = split_dts t;
1.272 +> comp_dts thy (d,ts);
1.273 +val it = "testdscforlist [#1]" : cterm
1.274 +
1.275 +> val t = (term_of o the o (parse thy)) "(A::real)";
1.276 +> val (d,ts) = split_dts t;
1.277 +val d = Const ("empty","empty") : term
1.278 +val ts = [Free ("A","RealDef.real")] : term list
1.279 +> val t = (term_of o the o (parse thy)) "[R=(R::real)]";
1.280 +> val (d,ts) = split_dts t;
1.281 +val d = Const ("empty","empty") : term
1.282 +val ts = [Const # $ Free # $ Free (#,#)] : term list
1.283 +> val t = (term_of o the o (parse thy)) "[#1,#2]";
1.284 +> val (d,ts) = split_dts t;
1.285 +val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
1.286 +*)
1.287 +
1.288 +(*for input_icalhd 11.03*)
1.289 +fun comp_dts'' (d,[]) =
1.290 + if is_reall_dsc d then term2str (d $ e_listReal)
1.291 + else if is_booll_dsc d then term2str (d $ e_listBool)
1.292 + else term2str d
1.293 + | comp_dts'' (d,ts) = term2str (d $ (comp_ts (d, ts)))
1.294 + handle _ => raise error ("comp_dts'': "^(term2str d)^
1.295 + " $ "^(term2str (hd ts)));
1.296 +
1.297 +
1.298 +
1.299 +
1.300 +
1.301 +
1.302 +(* this may decompose an object-language isa-list;
1.303 + use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)
1.304 +fun dest_list' t = if is_list t then isalist2list t else [t];
1.305 +
1.306 +(*fun is_metavar (Free (str, _)) =
1.307 + if (last_elem o explode) str = "_" then true else false
1.308 + | is_metavar _ = false;*)
1.309 +fun is_var (Free _) = true
1.310 + | is_var _ = false;
1.311 +
1.312 +(*.special handling for lists. ?WN:14.5.03 ??!?*)
1.313 +fun dest_list (d,ts) =
1.314 + let fun dest t =
1.315 + if is_list_dsc d andalso not (is_unl d)
1.316 + andalso not (is_var t) (*..for pbt*)
1.317 + then isalist2list t else [t]
1.318 + in (flat o (map dest)) ts end;
1.319 +
1.320 +
1.321 +(*.decompose an input into description, terms (ev. elems of lists),
1.322 + and the value for the problem-environment; inv to comp_dts .*)
1.323 +(*WN.8.6.03: corrected with minimal effort,
1.324 +fn : theory -> term ->
1.325 + term * description
1.326 + term list * lists decomposed for elementwise input
1.327 + term list pbl_ids not _HERE_: dont know which list-elems input*)
1.328 +fun split_dts thy (t as d $ arg) =
1.329 + if is_dsc d
1.330 + then if is_list_dsc d
1.331 + then if is_list arg
1.332 + then if is_unl d
1.333 + then (d, [arg]) (*e.g. someList [1,3,2]*)
1.334 + else (d, take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*)
1.335 + else (d, [arg]) (*a variable or metavariable for a list*)
1.336 + else (d, [arg])
1.337 + else (e_term, dest_list' t(*9.01 ???*))
1.338 + | split_dts thy t = (*either dsc or term*)
1.339 + let val (h,argl) = strip_comb t
1.340 + in if (not o is_dsc) h then (e_term, dest_list' t)
1.341 + else (h, dest_list (h,argl))
1.342 + end;
1.343 +(* tests see fun comp_dts
1.344 +
1.345 +> val t = str2term "someList []";
1.346 +> val (_,ts) = split_dts thy t; writeln (terms2str ts);
1.347 +["[]"]
1.348 +> val t = str2term "valuesFor []";
1.349 +> val (_,ts) = split_dts thy t; writeln (terms2str ts);
1.350 +["[]"]*)
1.351 +
1.352 +(*.version returning ts only.*)
1.353 +fun split_dts' (d, arg) =
1.354 + if is_dsc d
1.355 + then if is_list_dsc d
1.356 + then if is_list arg
1.357 + then if is_unl d
1.358 + then ([arg]) (*e.g. someList [1,3,2]*)
1.359 + else (take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*)
1.360 + else ([arg]) (*a variable or metavariable for a list*)
1.361 + else ([arg])
1.362 + else (dest_list' arg(*9.01 ???*))
1.363 + | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
1.364 + let val (h,argl) = strip_comb t
1.365 + in if (not o is_dsc) h then (dest_list' t)
1.366 + else (dest_list (h,argl))
1.367 + end;
1.368 +
1.369 +
1.370 +
1.371 +
1.372 +
1.373 +(*27.8.01: problem-environment
1.374 +WN.6.5.03: FIXXME reconsider if penv is worth the effort --
1.375 + -- just rerun a whole expl with num/var may show the same ?!
1.376 +WN.9.5.03: penv-concept stalled, immediately generate script env !
1.377 + but [#0, epsilon] only outcommented for eventual reconsideration
1.378 +*)
1.379 +type penv = (term (*err_*)
1.380 + * (term list) (*[#0, epsilon] 9.5.03 outcommented*)
1.381 + ) list;
1.382 +fun pen2str ctxt (t, ts) =
1.383 + pair2str(Syntax.string_of_term ctxt t,
1.384 + (strs2str' o map (Syntax.string_of_term ctxt)) ts);
1.385 +fun penv2str_ thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv;
1.386 +
1.387 +(*
1.388 + 9.5.03: still unused, but left for eventual future development*)
1.389 +type envv = (int * penv) list; (*over variants*)
1.390 +
1.391 +(*. 14.9.01: not used after putting penv-values into itm_
1.392 + make the result of split_* a value of problem-environment .*)
1.393 +fun mkval dsc [] = raise error "mkval called with []"
1.394 + | mkval dsc [t] = t
1.395 + | mkval dsc ts = list2isalist ((type_of o hd) ts) ts;
1.396 +(*WN.12.12.03*)
1.397 +fun mkval' x = mkval e_term x;
1.398 +
1.399 +
1.400 +
1.401 +(*. get the constant value from a penv .*)
1.402 +fun getval (id, values) =
1.403 + case values of
1.404 + [] => raise error ("penv_value: no values in '"^
1.405 + (Syntax.string_of_term (thy2ctxt' "Tools") id))
1.406 + | [v] => (id, v)
1.407 + | (v1::v2::_) => (case v1 of
1.408 + Const ("Script.Arbfix",_) => (id, v2)
1.409 + | _ => (id, v1));
1.410 +(*
1.411 + val e_ = (term_of o the o (parse thy)) "e_::bool";
1.412 + val ev = (term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0";
1.413 + val v_ = (term_of o the o (parse thy)) "v_";
1.414 + val vv = (term_of o the o (parse thy)) "x";
1.415 + val r_ = (term_of o the o (parse thy)) "err_::bool";
1.416 + val rv1 = (term_of o the o (parse thy)) "#0";
1.417 + val rv2 = (term_of o the o (parse thy)) "eps";
1.418 +
1.419 + val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv;
1.420 + map getval penv;
1.421 +[(Free ("e_","bool"),
1.422 + Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#0","RealDef.real")),
1.423 + (Free ("v_","RealDef.real"),Free ("x","RealDef.real")),
1.424 + (Free ("err_","bool"),Free ("#0","RealDef.real"))] : (term * term) list
1.425 +*)
1.426 +
1.427 +
1.428 +(*23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc
1.429 +(1) kinds of itms:
1.430 + (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
1.431 + =(presently) Mis (? should be Inc initially, and Mis after match_itms?)
1.432 + (1.2) Syn,Typ,Sup: not related to oris
1.433 + Syn, Typ (presently) should be accepted in appl_add (instead Error')
1.434 + Sup (presently) should be accepted in appl_add (instead Error')
1.435 + _could_ be w.r.t current vat (and then _is_ related to vat
1.436 + Mis should _not_ be made Inc ((presently, by appl_add & match_itms)
1.437 +- dsc in itm_ is timeconsuming -- keep id for respective queries ?
1.438 +- order of items in ppc should be stable w.r.t order of itms
1.439 +
1.440 +- stepwise input of itms --- match_itms (in one go) ..not coordinated
1.441 + - unify code
1.442 + - match_itms / match_itms_oris ..2 versions ?!
1.443 + (fast, for refine / slow, for modeling)
1.444 +
1.445 +- clarify: efficiency <--> simplicity !!!
1.446 + ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc
1.447 + | take int for perserving order of item ppc in itms
1.448 + | make all(!?) handling of itms stable against reordering(?)
1.449 + | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)
1.450 + -"- "#undef" ?= not touched ?= (id,..)
1.451 +-----------------------------------------------------------------
1.452 +27.3.02:
1.453 +def: type pbt = (field, (dsc, pid))
1.454 +
1.455 +(1) fmz + pbt -> oris
1.456 +(2) input + oris -> itm
1.457 +(3) match_itms : schnell(?) f"ur refine
1.458 + match_itms_oris : r"uckmeldung f"ur item ppc
1.459 +
1.460 +(1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)
1.461 +---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!
1.462 +
1.463 +(3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;
1.464 + wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:
1.465 + (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ????
1.466 + (b)
1.467 +*)
1.468 +
1.469 +
1.470 +
1.471 +
1.472 +(*the internal representation of a models' item
1.473 +
1.474 + 4.9.01: not consistent:
1.475 + after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
1.476 + (involves 'is_error');
1.477 + bool in itm really necessary ???*)
1.478 +datatype itm_ =
1.479 + Cor of (term * (* description *)
1.480 + (term list)) * (* for list: elem-wise input *)
1.481 + (*split_dts <-> comp_dts*)
1.482 + (term * (term list)) (* elem of penv *)
1.483 + (*9.5.03: ---- is already for script -- penv delayed to future*)
1.484 + | Syn of cterm'
1.485 + | Typ of cterm'
1.486 + | Inc of (term * (term list)) * (term * (term list)) (*lists,
1.487 + + init_pbl WN.11.03 FIXXME: empty penv .. bad
1.488 + init_pbl should return Mis !!!*)
1.489 + | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
1.490 + | Mis of (term * term) (* after re-specification pbt-item not found
1.491 + in pbl: only dsc, pid_*)
1.492 + | Par of cterm'; (*internal state from fun parsitm*)
1.493 +
1.494 +type vats = int list; (*variants in formalizations*)
1.495 +
1.496 +(*.data-type for working on pbl/met-ppc:
1.497 + in pbl initially holds descriptions (only) for user guidance.*)
1.498 +type itm =
1.499 + int * (* id =0 .. untouched - descript (only) from init
1.500 + 23.3.02: seems to correspond to ori (fun insert_ppc)
1.501 + <> maintain order in item ppc?*)
1.502 + vats * (* variants - copy from ori *)
1.503 + bool * (* input on this item is not/complete *)
1.504 + string * (* #Given | #Find | #Relate *)
1.505 + itm_; (* *)
1.506 +(* use"ME/sequent.sml";
1.507 + *)
1.508 +val e_itm = (0,[],false,"e_itm",Syn"e_itm"):itm;
1.509 +(*in CalcTree/Subproblem an 'untouched' model is created
1.510 + FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
1.511 +fun untouched (itms: itm list) =
1.512 + foldl and_ (true ,map ((curry op= 0) o #1) itms);
1.513 +(*> untouched [];
1.514 +val it = true : bool
1.515 +> untouched [e_itm];
1.516 +val it = true : bool
1.517 +> untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")];
1.518 +val it = false : bool*)
1.519 +
1.520 +
1.521 +
1.522 +
1.523 +
1.524 +(* find most frequent variant v in itms *)
1.525 +
1.526 +fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);
1.527 +
1.528 +fun cnt itms v = (v,(length o (filter (curry op= v)) o
1.529 + flat o (map #2)) (itms:itm list));
1.530 +fun vts_cnt vts itms = map (cnt itms) vts;
1.531 +fun max2 [] = raise error "max2 of []"
1.532 + | max2 (y::ys) =
1.533 + let fun mx (a,x) [] = (a,x)
1.534 + | mx (a,x) ((b,y)::ys) =
1.535 + if x < y then mx (b,y) ys else mx (a,x) ys;
1.536 +in mx y ys end;
1.537 +
1.538 +(*. find the variant with most items already input .*)
1.539 +fun max_vt itms =
1.540 + let val vts = (vts_cnt (vts_in itms)) itms;
1.541 + in if vts = [] then 0 else (fst o max2) vts end;
1.542 +
1.543 +
1.544 +(* TODO ev. make more efficient by avoiding flat *)
1.545 +fun mk_e (Cor (_, iv)) = [getval iv]
1.546 + | mk_e (Syn _) = []
1.547 + | mk_e (Typ _) = []
1.548 + | mk_e (Inc (_, iv)) = [getval iv]
1.549 + | mk_e (Sup _) = []
1.550 + | mk_e (Mis _) = [];
1.551 +fun mk_en vt ((i,vts,b,f,itm_):itm) =
1.552 + if member op = vts vt then mk_e itm_ else [];
1.553 +(*. extract the environment from an item list;
1.554 + takes the variant with most items .*)
1.555 +fun mk_env itms =
1.556 + let val vt = max_vt itms
1.557 + in (flat o (map (mk_en vt))) itms end;
1.558 +
1.559 +
1.560 +
1.561 +(*. example as provided by an author, complete w.r.t. pbt specified
1.562 + not touched by any user action .*)
1.563 +type ori = (int * (* id: 10.3.00ff impl. only <>0 .. touched
1.564 + 21.3.02: insert_ppc needs it ! ?:purpose maintain
1.565 + order in item ppc ???*)
1.566 + vats * (* variants 21.3.02: related to pbt..discard ?*)
1.567 + string * (* #Given | #Find | #Relate 21.3.02: discard ?*)
1.568 + term * (* description *)
1.569 + term list (* isalist2list t | [t] *)
1.570 + );
1.571 +val e_ori_ = (0,[],"",e_term,[e_term]):ori;
1.572 +val e_ori = (0,[],"",e_term,[e_term]):ori;
1.573 +
1.574 +fun ori2str ((i,vs,fi,t,ts):ori) =
1.575 + "("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^
1.576 + (term2str t)^", "^((strs2str o (map term2str)) ts)^")";
1.577 +val oris2str =
1.578 + let val s = !show_types
1.579 + val _ = show_types:= true
1.580 + val str = (strs2str' o (map (linefeed o ori2str)))
1.581 + val _ = show_types:= s
1.582 + in str end;
1.583 +
1.584 +(*.an or without leading integer.*)
1.585 +type preori = (vats *
1.586 + string *
1.587 + term *
1.588 + term list);
1.589 +fun preori2str ((vs,fi,t,ts):preori) =
1.590 + "("^((strs2str o (map string_of_int)) vs)^", "^fi^", "^
1.591 + (term2str t)^", "^((strs2str o (map term2str)) ts)^")";
1.592 +val preoris2str = (strs2str' o (map (linefeed o preori2str)));
1.593 +
1.594 +(*. given the input value (from split_dts)
1.595 + make the value in a problem-env according to description-type .*)
1.596 +(*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
1.597 +fun pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v =
1.598 + if is_list v
1.599 + then [v] (*eg. [r=Arbfix]*)
1.600 + else (case v of (*eg. eps=#0*)
1.601 + (Const ("op =",_) $ l $ r) => [r,l]
1.602 + | _ => raise error ("pbl_ids Tools.nam: no equality "
1.603 + ^(Syntax.string_of_term ctxt v)))
1.604 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v]
1.605 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v]
1.606 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v]
1.607 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v]
1.608 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v]
1.609 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v]
1.610 + | pbl_ids ctxt _ v = raise error ("pbl_ids: not implemented for "
1.611 + ^(Syntax.string_of_term ctxt v));
1.612 +(*
1.613 +val t as t1 $ t2 = str2term "antiDerivativeName M_b";
1.614 +pbl_ids ctxt t1 t2;
1.615 +
1.616 + val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
1.617 + val (d,argl) = strip_comb t;
1.618 + is_dsc d; (*see split_dts*)
1.619 + dest_list (d,argl);
1.620 + val (_ $ v) = t;
1.621 + is_list v;
1.622 + pbl_ids ctxt d v;
1.623 +[Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
1.624 + (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
1.625 +
1.626 + val (dsc,vl) = (split_dts o term_of o the o (parse thy)) "solveFor x";
1.627 +val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term
1.628 +val vl = Free ("x","RealDef.real") : term
1.629 +
1.630 + val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
1.631 + pbl_ids ctxt dsc vl;
1.632 +val it = [Free ("x","RealDef.real")] : term list
1.633 +
1.634 + val (dsc,vl) = (split_dts o term_of o the o(parse thy))
1.635 + "errorBound (eps=#0)";
1.636 + val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_";
1.637 + pbl_ids ctxt dsc vl;
1.638 +val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *)
1.639 +
1.640 +(*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))
1.641 + make the value in a problem-env according to description-type .*)
1.642 +(*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
1.643 +fun pbl_ids' (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) vs =
1.644 + (case vs of
1.645 + [] => raise error ("pbl_ids' Tools.nam called with []")
1.646 + | [t] => (case t of (*eg. eps=#0*)
1.647 + (Const ("op =",_) $ l $ r) => [r,l]
1.648 + | _ => raise error ("pbl_ids' Tools.nam: no equality "
1.649 + ^(Syntax.string_of_term (thy2ctxt' "Isac")t)))
1.650 + | vs' => vs (*14.9.01: ???TODO *))
1.651 + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs
1.652 + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs
1.653 + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs
1.654 + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs
1.655 + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))vs = vs
1.656 + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))vs = vs
1.657 + | pbl_ids' _ vs =
1.658 + raise error ("pbl_ids': not implemented for "
1.659 + ^(terms2str vs));
1.660 +(*9.5.03 penv postponed: pbl_ids'*)
1.661 +fun pbl_ids' thy d vs = [comp_ts (d, vs)];
1.662 +
1.663 +
1.664 +(*14.9.01: not used after putting values for penv into itm_
1.665 + WN.5.5.03: used in upd .. upd_envv*)
1.666 +fun upd_penv ctxt penv dsc (id, vl) =
1.667 +(writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
1.668 + writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
1.669 + writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
1.670 + overwrite (penv, (id, pbl_ids ctxt dsc vl))
1.671 +);
1.672 +(*
1.673 + val penv = [];
1.674 + val (dsc,vl) = (split_did o term_of o the o (parse thy)) "solveFor x";
1.675 + val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
1.676 + val penv = upd_penv thy penv dsc (id, vl);
1.677 +[(Free ("v_","RealDef.real"),
1.678 + [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")])]
1.679 +: (term * term list) list
1.680 +
1.681 + val (dsc,vl) = (split_did o term_of o the o(parse thy))"errorBound (eps=#0)";
1.682 + val (dsc,id) = (split_did o term_of o the o(parse thy))"errorBound err_";
1.683 + upd_penv thy penv dsc (id, vl);
1.684 +[(Free ("v_","RealDef.real"),
1.685 + [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")]),
1.686 + (Free ("err_","bool"),
1.687 + [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")])]
1.688 +: (term * term list) list ^.........!!!!
1.689 +*)
1.690 +
1.691 +(*WN.9.5.03: not reconsidered; looks strange !!!*)
1.692 +fun upd thy envv dsc (id, vl) i =
1.693 + let val penv = case assoc (envv, i) of
1.694 + SOME e => e
1.695 + | NONE => [];
1.696 + val penv' = upd_penv thy penv dsc (id, vl);
1.697 + in (i, penv') end;
1.698 +(*
1.699 + val i = 2;
1.700 + val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
1.701 + val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";
1.702 + val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";
1.703 + upd thy envv dsc (id, vl) i;
1.704 +val it = (2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])
1.705 + : int * (term * term list) list*)
1.706 +
1.707 +
1.708 +(*14.9.01: not used after putting pre-penv into itm_*)
1.709 +fun upd_envv thy (envv:envv) (vats:vats) dsc id vl =
1.710 + let val vats = if length vats = 0
1.711 + then (*unknown id to _all_ variants*)
1.712 + if length envv = 0 then [1]
1.713 + else (intsto o length) envv
1.714 + else vats
1.715 + fun isin vats (i,_) = member op = vats i;
1.716 + val envs_notin_vat = filter_out (isin vats) envv;
1.717 + in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end;
1.718 +(*
1.719 + val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
1.720 +
1.721 + val vats = [2]
1.722 + val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";
1.723 + val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";
1.724 + val envv = upd_envv thy envv vats dsc id vl;
1.725 +val envv = [(2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])]
1.726 + : (int * (term * term list) list) list
1.727 +
1.728 + val vats = [1,2,3];
1.729 + val (dsc,vl) = (split_did o term_of o the o(parse thy))"maximum A";
1.730 + val (dsc,id) = (split_did o term_of o the o(parse thy))"maximum m_";
1.731 + upd_envv thy envv vats dsc id vl;
1.732 +[(1,[(Free ("m_","bool"),[Free ("A","bool")])]),
1.733 + (2,
1.734 + [(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")]),
1.735 + (Free ("m_","bool"),[Free ("A","bool")])]),
1.736 + (3,[(Free ("m_","bool"),[Free ("A","bool")])])]
1.737 +: (int * (term * term list) list) list
1.738 +
1.739 +
1.740 + val env = []:envv;
1.741 + val (d,ts) = (split_dts o term_of o the o (parse thy))
1.742 + "fixedValues [r=Arbfix]";
1.743 + val (_,id) = (split_did o term_of o the o (parse thy))"fixedValues fix_";
1.744 + val vats = [1,2,3];
1.745 + val env = upd_envv thy env vats d id (mkval ts);
1.746 +*)
1.747 +
1.748 +(*. update envv by folding from a list of arguments .*)
1.749 +fun upds_envv thy envv [] = envv
1.750 + | upds_envv thy envv ((vs, dsc, id, vl)::ps) =
1.751 + upds_envv thy (upd_envv thy envv vs dsc id vl) ps;
1.752 +(* eval test-maximum.sml until Specify_Method ...
1.753 + val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
1.754 + val met = (#ppc o get_met) mI;
1.755 +
1.756 + val envv = [];
1.757 + val eargs = flat eargs;
1.758 + val (vs, dsc, id, vl) = hd eargs;
1.759 + val envv = upds_envv thy envv [(vs, dsc, id, vl)];
1.760 +
1.761 + val (vs, dsc, id, vl) = hd (tl eargs);
1.762 + val envv = upds_envv thy envv [(vs, dsc, id, vl)];
1.763 +
1.764 + val (vs, dsc, id, vl) = hd (tl (tl eargs));
1.765 + val envv = upds_envv thy envv [(vs, dsc, id, vl)];
1.766 +
1.767 + val (vs, dsc, id, vl) = hd (tl (tl (tl eargs)));
1.768 + val envv = upds_envv thy envv [(vs, dsc, id, vl)];
1.769 +[(1,
1.770 + [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
1.771 + (Free ("m_","bool"),[Free (#,#)]),
1.772 + (Free ("vs_","bool List.list"),[# $ # $ Const #]),
1.773 + (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
1.774 + (2,
1.775 + [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
1.776 + (Free ("m_","bool"),[Free (#,#)]),
1.777 + (Free ("vs_","bool List.list"),[# $ # $ Const #]),
1.778 + (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
1.779 + (3,
1.780 + [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
1.781 + (Free ("m_","bool"),[Free (#,#)]),
1.782 + (Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *)
1.783 +
1.784 +(*for _output_ of the items of a Model*)
1.785 +datatype item =
1.786 + Correct of cterm' (*labels a correct formula (type cterm')*)
1.787 + | SyntaxE of string (**)
1.788 + | TypeE of string (**)
1.789 + | False of cterm' (*WN050618 notexistent in itm_: only used in Where*)
1.790 + | Incompl of cterm' (**)
1.791 + | Superfl of string (**)
1.792 + | Missing of cterm';
1.793 +fun item2str (Correct s) ="Correct " ^ s
1.794 + | item2str (SyntaxE s) ="SyntaxE " ^ s
1.795 + | item2str (TypeE s) ="TypeE " ^ s
1.796 + | item2str (False s) ="False " ^ s
1.797 + | item2str (Incompl s) ="Incompl " ^ s
1.798 + | item2str (Superfl s) ="Superfl " ^ s
1.799 + | item2str (Missing s) ="Missing " ^ s;
1.800 +(*make string for error-msgs*)
1.801 +fun itm_2str_ ctxt (Cor ((d,ts), penv)) =
1.802 + "Cor " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ,"
1.803 + ^ pen2str ctxt penv
1.804 + | itm_2str_ ctxt (Syn c) = "Syn " ^ c
1.805 + | itm_2str_ ctxt (Typ c) = "Typ " ^ c
1.806 + | itm_2str_ ctxt (Inc ((d,ts), penv)) =
1.807 + "Inc " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ,"
1.808 + ^ pen2str ctxt penv
1.809 + | itm_2str_ ctxt (Sup (d,ts)) =
1.810 + "Sup " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts))
1.811 + | itm_2str_ ctxt (Mis (d,pid))=
1.812 + "Mis "^ Syntax.string_of_term ctxt d ^
1.813 + " "^ Syntax.string_of_term ctxt pid
1.814 + | itm_2str_ ctxt (Par s) = "Trm "^s;
1.815 +fun itm_2str t = itm_2str_ (thy2ctxt' "Isac") t;
1.816 +fun itm2str_ ctxt ((i,is,b,s,itm_):itm) =
1.817 + "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^
1.818 + s^" ,"^(itm_2str_ ctxt itm_)^")";
1.819 +fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
1.820 +fun w_itms2str_ ctxt itms = writeln (itms2str_ ctxt itms);
1.821 +
1.822 +fun init_item str = SyntaxE str;
1.823 +
1.824 +
1.825 +
1.826 +
1.827 +type 'a ppc =
1.828 + {Given : 'a list,
1.829 + Where: 'a list,
1.830 + Find : 'a list,
1.831 + With : 'a list,
1.832 + Relate: 'a list};
1.833 +fun ppc2str {Given=Given,Where=Where,Find=Find,With=With,Relate=Relate}=
1.834 + ("{Given =" ^ (strs2str Given ) ^
1.835 + ",Where=" ^ (strs2str Where) ^
1.836 + ",Find =" ^ (strs2str Find ) ^
1.837 + ",With =" ^ (strs2str With ) ^
1.838 + ",Relate=" ^ (strs2str Relate) ^ "}");
1.839 +
1.840 +
1.841 +
1.842 +
1.843 +fun item_ppc ({Given = gi,Where= wh,
1.844 + Find = fi,With = wi,Relate= re}: string ppc) =
1.845 + {Given = map init_item gi,Where= map init_item wh,
1.846 + Find = map init_item fi,With = map init_item wi,
1.847 + Relate= map init_item re}:item ppc;
1.848 +fun itemppc2str ({Given=Given,Where=Where,
1.849 + Find=Find,With=With,Relate=Relate}:item ppc)=
1.850 + ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
1.851 + ",Where=" ^ ((strs2str' o (map item2str)) Where) ^
1.852 + ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
1.853 + ",With =" ^ ((strs2str' o (map item2str)) With ) ^
1.854 + ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
1.855 +
1.856 +fun de_item (Correct x) = x
1.857 + | de_item (SyntaxE x) = x
1.858 + | de_item (TypeE x) = x
1.859 + | de_item (False x) = x
1.860 + | de_item (Incompl x) = x
1.861 + | de_item (Superfl x) = x
1.862 + | de_item (Missing x) = x;
1.863 +val empty_ppc ={Given = [],
1.864 + Where= [],
1.865 + Find = [],
1.866 + With = [],
1.867 + Relate= []}:item ppc;
1.868 +val empty_ppc_ct' ={Given = [],
1.869 + Where = [],
1.870 + Find = [],
1.871 + With = [],
1.872 + Relate= []}:cterm' ppc;
1.873 +
1.874 +
1.875 +datatype match =
1.876 + Matches of pblID * item ppc
1.877 +| NoMatch of pblID * item ppc;
1.878 +fun match2str (Matches (pI, ppc)) =
1.879 + "Matches ("^(strs2str pI)^", "^(itemppc2str ppc)^")"
1.880 + | match2str(NoMatch (pI, ppc)) =
1.881 + "NoMatch ("^(strs2str pI)^", "^(itemppc2str ppc)^")";
1.882 +fun matchs2str ms = (strs2str o (map match2str)) ms;
1.883 +fun pblID_of_match (Matches (pI,_)) = pI
1.884 + | pblID_of_match (NoMatch (pI,_)) = pI;
1.885 +
1.886 +(*10.03 for Refine_Problem*)
1.887 +datatype match_ =
1.888 + Match_ of pblID * ((itm list) * ((bool * term) list))
1.889 +| NoMatch_;
1.890 +
1.891 +(*. the refined pbt is the last_element Matches in the list .*)
1.892 +fun is_matches (Matches _) = true
1.893 + | is_matches _ = false;
1.894 +fun matches_pblID (Matches (pI,_)) = pI;
1.895 +fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms)
1.896 + handle _ => []:pblID;
1.897 +fun refined_IDitms ms = ((find_first is_matches) o rev) ms;
1.898 +
1.899 +(*. the refined pbt is the last_element Matches in the list,
1.900 + for Refine_Problem, tryrefine .*)
1.901 +fun is_matches_ (Match_ _) = true
1.902 + | is_matches_ _ = false;
1.903 +fun refined_ ms = ((find_first is_matches_) o rev) ms;
1.904 +
1.905 +
1.906 +fun ts_in (Cor ((_,ts),_)) = ts
1.907 + | ts_in (Syn (c)) = []
1.908 + | ts_in (Typ (c)) = []
1.909 + | ts_in (Inc ((_,ts),_)) = ts
1.910 + | ts_in (Sup (_,ts)) = ts
1.911 + | ts_in (Mis _) = [];
1.912 +(*WN050629 unused*)
1.913 +fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
1.914 +val unique = (term_of o the o (parse (theory "Real"))) "UnIqE_tErM";
1.915 +fun d_in (Cor ((d,_),_)) = d
1.916 + | d_in (Syn (c)) = (writeln("*** d_in: Syn ("^c^")"); unique)
1.917 + | d_in (Typ (c)) = (writeln("*** d_in: Typ ("^c^")"); unique)
1.918 + | d_in (Inc ((d,_),_)) = d
1.919 + | d_in (Sup (d,_)) = d
1.920 + | d_in (Mis (d,_)) = d;
1.921 +
1.922 +fun dts2str (d,ts) = pair2str (term2str d, terms2str ts);
1.923 +fun penvval_in (Cor ((d,_),(_,ts))) = [comp_ts (d,ts)]
1.924 + | penvval_in (Syn (c)) = (writeln("*** penvval_in: Syn ("^c^")"); [])
1.925 + | penvval_in (Typ (c)) = (writeln("*** penvval_in: Typ ("^c^")"); [])
1.926 + | penvval_in (Inc (_,(_,ts))) = ts
1.927 + | penvval_in (Sup dts) = (writeln("*** penvval_in: Sup "^(dts2str dts)); [])
1.928 + | penvval_in (Mis (d,t)) = (writeln("*** penvval_in: Mis "^
1.929 + (pair2str(term2str d, term2str t))); []);
1.930 +
1.931 +
1.932 +(*. check a predicate labelled with indication of incomplete substitution;
1.933 +rls -> (*for eval_true*)
1.934 +bool * (*have _all_ variables(Free) from the model-pattern
1.935 + been substituted by a value from the pattern's environment ?*)
1.936 +term (*the precondition*)
1.937 +->
1.938 +bool * (*has the precondition evaluated to true*)
1.939 +term (*the precondition (for map)*)
1.940 +.*)
1.941 +fun evalprecond prls (false, pre) =
1.942 + (*NOT ALL Free's have been substituted, eg. because of incomplete model*)
1.943 + (false, pre)
1.944 + | evalprecond prls (true, pre) =
1.945 +(* val (prls, pre) = (prls, hd pres');
1.946 + val (prls, pre) = (prls, hd (tl pres'));
1.947 + *)
1.948 + if eval_true (assoc_thy "Isac.thy") (*for Pattern.match *)
1.949 + [pre] prls (*pre parsed, prls.thy*)
1.950 + then (true , pre)
1.951 + else (false , pre);
1.952 +
1.953 +fun pre2str (b, t) = pair2str(bool2str b, term2str t);
1.954 +fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
1.955 +
1.956 +(*. check preconditions, return true if all true .*)
1.957 +fun check_preconds' _ [] _ _ = [] (*empty preconditions are true*)
1.958 + | check_preconds' prls pres pbl _(*FIXME.WN0308 mvat re-introduce*) =
1.959 +(* val (prls, pres, pbl, _) = (prls, where_, probl, 0);
1.960 + val (prls, pres, pbl, _) = (prls, pre, itms, mvat);
1.961 + *)
1.962 + let val env = mk_env pbl;
1.963 + val pres' = map (subst_atomic_all env) pres;
1.964 + in map (evalprecond prls) pres' end;
1.965 +
1.966 +fun check_preconds thy prls pres pbl =
1.967 + check_preconds' prls pres pbl (max_vt pbl);
1.968 +
1.969 +(*----------------------------------------------------------*)
1.970 +end
1.971 +open SpecifyTools;
1.972 +(*----------------------------------------------------------*)