diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Interpret/mstools.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Interpret/mstools.sml Wed Aug 25 16:20:07 2010 +0200 @@ -0,0 +1,969 @@ +(* Types and tools for 'modeling' und 'specifying' to be used in + modspec.sml. The types are separated from calchead.sml into this file, + because some of them are stored in the calc-tree, and thus are required + _before_ ctree.sml. + author: Walther Neuper + (c) due to copyright terms + +use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*); +use"mstools.sml"; +12345678901234567890123456789012345678901234567890123456789012345678901234567890 + 10 20 30 40 50 60 70 80 +*) + +signature SPECIFY_TOOLS = + sig + type envv + datatype + item = + Correct of cterm' + | False of cterm' + | Incompl of cterm' + | Missing of cterm' + | Superfl of string + | SyntaxE of string + | TypeE of string + val item2str : item -> string + type itm + val itm2str_ : Proof.context -> itm -> string + datatype + itm_ = + Cor of (term * term list) * (term * term list) + | Inc of (term * term list) * (term * term list) + | Mis of term * term + | Par of cterm' + | Sup of term * term list + | Syn of cterm' + | Typ of cterm' + val itm_2str : itm_ -> string + val itm_2str_ : Proof.context -> itm_ -> string + val itms2str_ : Proof.context -> itm list -> string + type 'a ppc + val ppc2str : + {Find: string list, With: string list, Given: string list, + Where: string list, Relate: string list} -> string + datatype + match = + Matches of pblID * item ppc + | NoMatch of pblID * item ppc + val match2str : match -> string + datatype + match_ = + Match_ of pblID * (itm list * (bool * term) list) + | NoMatch_ + val matchs2str : match list -> string + type ori + val ori2str : ori -> string + val oris2str : ori list -> string + type preori + val preori2str : preori -> string + val preoris2str : preori list -> string + type penv + (* val penv2str_ : Proof.context -> penv -> string *) + type vats + (*----------------------------------------------------------------------*) + val all_ts_in : itm_ list -> term list + val check_preconds : + 'a -> + rls -> + term list -> itm list -> (bool * term) list + val check_preconds' : + rls -> + term list -> + itm list -> 'a -> (bool * term) list + (* val chkpre2item : rls -> term -> bool * item *) + val pres2str : (bool * term) list -> string + (* val evalprecond : rls -> term -> bool * term *) + (* val cnt : itm list -> int -> int * int *) + val comp_dts : theory -> term * term list -> term + val comp_dts' : term * term list -> term + val comp_dts'' : term * term list -> string + val comp_ts : term * term list -> term + val d_in : itm_ -> term + val de_item : item -> cterm' + val dest_list : term * term list -> term list (* for testing *) + val dest_list' : term -> term list + val dts2str : term * term list -> string + val e_itm : itm + (* val e_listBool : term *) + (* val e_listReal : term *) + val e_ori : ori + val e_ori_ : ori + val empty_ppc : item ppc + (* val empty_ppc_ct' : cterm' ppc *) + (* val getval : term * term list -> term * term *) + (*val head_precond : + domID * pblID * 'a -> + term option -> + rls -> + term list -> + itm list -> 'b -> term * (bool * term) list*) + (* val init_item : string -> item *) + (* val is_matches : match -> bool *) + (* val is_matches_ : match_ -> bool *) + val is_var : term -> bool + (* val item_ppc : + string ppc -> item ppc *) + val itemppc2str : item ppc -> string + (* val matches_pblID : match -> pblID *) + val max2 : ('a * int) list -> 'a * int + val max_vt : itm list -> int + val mk_e : itm_ -> (term * term) list + val mk_en : int -> itm -> (term * term) list + val mk_env : itm list -> (term * term) list + val mkval : 'a -> term list -> term + val mkval' : term list -> term + (* val pblID_of_match : match -> pblID *) + val pbl_ids : Proof.context -> term -> term -> term list + val pbl_ids' : 'a -> term -> term list -> term list + (* val pen2str : theory -> term * term list -> string *) + val penvval_in : itm_ -> term list + val refined : match list -> pblID + val refined_ : + match_ list -> match_ option + (* val refined_IDitms : + match list -> match option *) + val split_dts : 'a -> term -> term * term list + val split_dts' : term * term -> term list + (* val take_apart : term -> term list *) + (* val take_apart_inv : term list -> term *) + val ts_in : itm_ -> term list + (* val unique : term *) + val untouched : itm list -> bool + val upd : + Proof.context -> + (''a * (''b * term list) list) list -> + term -> + ''b * term -> ''a -> ''a * (''b * term list) list + val upd_envv : + Proof.context -> + envv -> + vats -> + term -> term -> term -> envv + val upd_penv : + Proof.context -> + (''a * term list) list -> + term -> ''a * term -> (''a * term list) list + (* val upds_envv : + Proof.context -> + envv -> + (vats * term * term * term) list -> + envv *) + val vts_cnt : int list -> itm list -> (int * int) list + val vts_in : itm list -> int list + (* val w_itms2str_ : Proof.context -> itm list -> unit *) + end + +(*----------------------------------------------------------*) +structure SpecifyTools : SPECIFY_TOOLS = +struct +(*----------------------------------------------------------*) +val e_listReal = (term_of o the o (parse (theory "Script"))) "[]::(real list)"; +val e_listBool = (term_of o the o (parse (theory "Script"))) "[]::(bool list)"; + +(*.take list-term apart w.r.t. handling elementwise input.*) +fun take_apart t = + let val elems = isalist2list t + in map ((list2isalist (type_of (hd elems))) o single) elems end; +(*val t = str2term "[a, b]"; +> val ts = take_apart t; writeln (terms2str ts); +["[a]","[b]"] + +> t = (take_apart_inv o take_apart) t; +true*) +fun take_apart_inv ts = + let val elems = (flat o (map isalist2list)) ts; + in list2isalist (type_of (hd elems)) elems end; +(*val ts = [str2term "[a]", str2term "[b]"]; +> val t = take_apart_inv ts; term2str t; +"[a, b]" + +ts = (take_apart o take_apart_inv) ts; +true*) + + + + +(*.revert split_dts only for ts; compare comp_dts.*) +fun comp_ts (d, ts) = + if is_list_dsc d + then if is_list (hd ts) + then if is_unl d + then (hd ts) (*e.g. someList [1,3,2]*) + else (take_apart_inv ts) + (* SML[ [a], [b] ]SML --> [a,b] *) + else (hd ts) (*a variable or metavariable for a list*) + else (hd ts); +(*.revert split_. + WN050903 we do NOT know which is from subtheory, description or term; + typecheck thus may lead to TYPE-error 'unknown constant'; + solution: typecheck with Isac.thy; i.e. arg 'thy' superfluous*) +(*fun comp_dts thy (d,[]) = + cterm_of (*(sign_of o assoc_thy) "Isac.thy"*) + (theory "Isac") + (*comp_dts:FIXXME stay with term for efficiency !!!*) + (if is_reall_dsc d then (d $ e_listReal) + else if is_booll_dsc d then (d $ e_listBool) + else d) + | comp_dts thy (d,ts) = + (cterm_of (*(sign_of o assoc_thy) "Isac.thy"*) + (theory "Isac") + (*comp_dts:FIXXME stay with term for efficiency !!*) + (d $ (comp_ts (d, ts))) + handle _ => raise error ("comp_dts: "^(term2str d)^ + " $ "^(term2str (hd ts))));*) +fun comp_dts thy (d,[]) = + (if is_reall_dsc d then (d $ e_listReal) + else if is_booll_dsc d then (d $ e_listBool) + else d) + | comp_dts thy (d,ts) = + (d $ (comp_ts (d, ts))) + handle _ => raise error ("comp_dts: "^(term2str d)^ + " $ "^(term2str (hd ts))); +(*25.8.03*) +fun comp_dts' (d,[]) = + if is_reall_dsc d then (d $ e_listReal) + else if is_booll_dsc d then (d $ e_listBool) + else d + | comp_dts' (d,ts) = (d $ (comp_ts (d, ts))) + handle _ => raise error ("comp_dts': "^(term2str d)^ + " $ "^(term2str (hd ts))); +(*val t = str2term "maximum A"; +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +val it = "maximum A" : cterm +> val t = str2term "fixedValues [r=Arbfix]"; +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +"fixedValues [r = Arbfix]" +> val t = str2term "valuesFor [a]"; +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +"valuesFor [a]" +> val t = str2term "valuesFor [a,b]"; +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +"valuesFor [a, b]" +> val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"; +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]" +> val t = str2term "boundVariable a"; +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +"boundVariable a" +> val t = str2term "interval {x::real. 0 <= x & x <= 2*r}"; +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +"interval {x. 0 <= x & x <= 2 * r}" + +> val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +"equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))" +> val t = str2term "solveFor x"; +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +"solveFor x" +> val t = str2term "errorBound (eps=0)"; +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +"errorBound (eps = 0)" +> val t = str2term "solutions L"; +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +"solutions L" + +before 6.5.03: +> val t = (term_of o the o (parse thy)) "testdscforlist [#1]"; +> val (d,ts) = split_dts t; +> comp_dts thy (d,ts); +val it = "testdscforlist [#1]" : cterm + +> val t = (term_of o the o (parse thy)) "(A::real)"; +> val (d,ts) = split_dts t; +val d = Const ("empty","empty") : term +val ts = [Free ("A","RealDef.real")] : term list +> val t = (term_of o the o (parse thy)) "[R=(R::real)]"; +> val (d,ts) = split_dts t; +val d = Const ("empty","empty") : term +val ts = [Const # $ Free # $ Free (#,#)] : term list +> val t = (term_of o the o (parse thy)) "[#1,#2]"; +> val (d,ts) = split_dts t; +val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED +*) + +(*for input_icalhd 11.03*) +fun comp_dts'' (d,[]) = + if is_reall_dsc d then term2str (d $ e_listReal) + else if is_booll_dsc d then term2str (d $ e_listBool) + else term2str d + | comp_dts'' (d,ts) = term2str (d $ (comp_ts (d, ts))) + handle _ => raise error ("comp_dts'': "^(term2str d)^ + " $ "^(term2str (hd ts))); + + + + + + +(* this may decompose an object-language isa-list; + use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*) +fun dest_list' t = if is_list t then isalist2list t else [t]; + +(*fun is_metavar (Free (str, _)) = + if (last_elem o explode) str = "_" then true else false + | is_metavar _ = false;*) +fun is_var (Free _) = true + | is_var _ = false; + +(*.special handling for lists. ?WN:14.5.03 ??!?*) +fun dest_list (d,ts) = + let fun dest t = + if is_list_dsc d andalso not (is_unl d) + andalso not (is_var t) (*..for pbt*) + then isalist2list t else [t] + in (flat o (map dest)) ts end; + + +(*.decompose an input into description, terms (ev. elems of lists), + and the value for the problem-environment; inv to comp_dts .*) +(*WN.8.6.03: corrected with minimal effort, +fn : theory -> term -> + term * description + term list * lists decomposed for elementwise input + term list pbl_ids not _HERE_: dont know which list-elems input*) +fun split_dts thy (t as d $ arg) = + if is_dsc d + then if is_list_dsc d + then if is_list arg + then if is_unl d + then (d, [arg]) (*e.g. someList [1,3,2]*) + else (d, take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*) + else (d, [arg]) (*a variable or metavariable for a list*) + else (d, [arg]) + else (e_term, dest_list' t(*9.01 ???*)) + | split_dts thy t = (*either dsc or term*) + let val (h,argl) = strip_comb t + in if (not o is_dsc) h then (e_term, dest_list' t) + else (h, dest_list (h,argl)) + end; +(* tests see fun comp_dts + +> val t = str2term "someList []"; +> val (_,ts) = split_dts thy t; writeln (terms2str ts); +["[]"] +> val t = str2term "valuesFor []"; +> val (_,ts) = split_dts thy t; writeln (terms2str ts); +["[]"]*) + +(*.version returning ts only.*) +fun split_dts' (d, arg) = + if is_dsc d + then if is_list_dsc d + then if is_list arg + then if is_unl d + then ([arg]) (*e.g. someList [1,3,2]*) + else (take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*) + else ([arg]) (*a variable or metavariable for a list*) + else ([arg]) + else (dest_list' arg(*9.01 ???*)) + | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*) + let val (h,argl) = strip_comb t + in if (not o is_dsc) h then (dest_list' t) + else (dest_list (h,argl)) + end; + + + + + +(*27.8.01: problem-environment +WN.6.5.03: FIXXME reconsider if penv is worth the effort -- + -- just rerun a whole expl with num/var may show the same ?! +WN.9.5.03: penv-concept stalled, immediately generate script env ! + but [#0, epsilon] only outcommented for eventual reconsideration +*) +type penv = (term (*err_*) + * (term list) (*[#0, epsilon] 9.5.03 outcommented*) + ) list; +fun pen2str ctxt (t, ts) = + pair2str(Syntax.string_of_term ctxt t, + (strs2str' o map (Syntax.string_of_term ctxt)) ts); +fun penv2str_ thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv; + +(* + 9.5.03: still unused, but left for eventual future development*) +type envv = (int * penv) list; (*over variants*) + +(*. 14.9.01: not used after putting penv-values into itm_ + make the result of split_* a value of problem-environment .*) +fun mkval dsc [] = raise error "mkval called with []" + | mkval dsc [t] = t + | mkval dsc ts = list2isalist ((type_of o hd) ts) ts; +(*WN.12.12.03*) +fun mkval' x = mkval e_term x; + + + +(*. get the constant value from a penv .*) +fun getval (id, values) = + case values of + [] => raise error ("penv_value: no values in '"^ + (Syntax.string_of_term (thy2ctxt' "Tools") id)) + | [v] => (id, v) + | (v1::v2::_) => (case v1 of + Const ("Script.Arbfix",_) => (id, v2) + | _ => (id, v1)); +(* + val e_ = (term_of o the o (parse thy)) "e_::bool"; + val ev = (term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0"; + val v_ = (term_of o the o (parse thy)) "v_"; + val vv = (term_of o the o (parse thy)) "x"; + val r_ = (term_of o the o (parse thy)) "err_::bool"; + val rv1 = (term_of o the o (parse thy)) "#0"; + val rv2 = (term_of o the o (parse thy)) "eps"; + + val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv; + map getval penv; +[(Free ("e_","bool"), + Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#0","RealDef.real")), + (Free ("v_","RealDef.real"),Free ("x","RealDef.real")), + (Free ("err_","bool"),Free ("#0","RealDef.real"))] : (term * term) list +*) + + +(*23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc +(1) kinds of itms: + (1.1) untouched: for modeling only dsc displayed(impossible after match_itms) + =(presently) Mis (? should be Inc initially, and Mis after match_itms?) + (1.2) Syn,Typ,Sup: not related to oris + Syn, Typ (presently) should be accepted in appl_add (instead Error') + Sup (presently) should be accepted in appl_add (instead Error') + _could_ be w.r.t current vat (and then _is_ related to vat + Mis should _not_ be made Inc ((presently, by appl_add & match_itms) +- dsc in itm_ is timeconsuming -- keep id for respective queries ? +- order of items in ppc should be stable w.r.t order of itms + +- stepwise input of itms --- match_itms (in one go) ..not coordinated + - unify code + - match_itms / match_itms_oris ..2 versions ?! + (fast, for refine / slow, for modeling) + +- clarify: efficiency <--> simplicity !!! + ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc + | take int for perserving order of item ppc in itms + | make all(!?) handling of itms stable against reordering(?) + | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???) + -"- "#undef" ?= not touched ?= (id,..) +----------------------------------------------------------------- +27.3.02: +def: type pbt = (field, (dsc, pid)) + +(1) fmz + pbt -> oris +(2) input + oris -> itm +(3) match_itms : schnell(?) f"ur refine + match_itms_oris : r"uckmeldung f"ur item ppc + +(1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid) +---------- ^^^^^ --- dh. pbt meist als argument zu viel !!! + +(3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht; + wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????: + (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ???? + (b) +*) + + + + +(*the internal representation of a models' item + + 4.9.01: not consistent: + after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation + (involves 'is_error'); + bool in itm really necessary ???*) +datatype itm_ = + Cor of (term * (* description *) + (term list)) * (* for list: elem-wise input *) + (*split_dts <-> comp_dts*) + (term * (term list)) (* elem of penv *) + (*9.5.03: ---- is already for script -- penv delayed to future*) + | Syn of cterm' + | Typ of cterm' + | Inc of (term * (term list)) * (term * (term list)) (*lists, + + init_pbl WN.11.03 FIXXME: empty penv .. bad + init_pbl should return Mis !!!*) + | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*) + | Mis of (term * term) (* after re-specification pbt-item not found + in pbl: only dsc, pid_*) + | Par of cterm'; (*internal state from fun parsitm*) + +type vats = int list; (*variants in formalizations*) + +(*.data-type for working on pbl/met-ppc: + in pbl initially holds descriptions (only) for user guidance.*) +type itm = + int * (* id =0 .. untouched - descript (only) from init + 23.3.02: seems to correspond to ori (fun insert_ppc) + <> maintain order in item ppc?*) + vats * (* variants - copy from ori *) + bool * (* input on this item is not/complete *) + string * (* #Given | #Find | #Relate *) + itm_; (* *) +(* use"ME/sequent.sml"; + *) +val e_itm = (0,[],false,"e_itm",Syn"e_itm"):itm; +(*in CalcTree/Subproblem an 'untouched' model is created + FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*) +fun untouched (itms: itm list) = + foldl and_ (true ,map ((curry op= 0) o #1) itms); +(*> untouched []; +val it = true : bool +> untouched [e_itm]; +val it = true : bool +> untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")]; +val it = false : bool*) + + + + + +(* find most frequent variant v in itms *) + +fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list); + +fun cnt itms v = (v,(length o (filter (curry op= v)) o + flat o (map #2)) (itms:itm list)); +fun vts_cnt vts itms = map (cnt itms) vts; +fun max2 [] = raise error "max2 of []" + | max2 (y::ys) = + let fun mx (a,x) [] = (a,x) + | mx (a,x) ((b,y)::ys) = + if x < y then mx (b,y) ys else mx (a,x) ys; +in mx y ys end; + +(*. find the variant with most items already input .*) +fun max_vt itms = + let val vts = (vts_cnt (vts_in itms)) itms; + in if vts = [] then 0 else (fst o max2) vts end; + + +(* TODO ev. make more efficient by avoiding flat *) +fun mk_e (Cor (_, iv)) = [getval iv] + | mk_e (Syn _) = [] + | mk_e (Typ _) = [] + | mk_e (Inc (_, iv)) = [getval iv] + | mk_e (Sup _) = [] + | mk_e (Mis _) = []; +fun mk_en vt ((i,vts,b,f,itm_):itm) = + if member op = vts vt then mk_e itm_ else []; +(*. extract the environment from an item list; + takes the variant with most items .*) +fun mk_env itms = + let val vt = max_vt itms + in (flat o (map (mk_en vt))) itms end; + + + +(*. example as provided by an author, complete w.r.t. pbt specified + not touched by any user action .*) +type ori = (int * (* id: 10.3.00ff impl. only <>0 .. touched + 21.3.02: insert_ppc needs it ! ?:purpose maintain + order in item ppc ???*) + vats * (* variants 21.3.02: related to pbt..discard ?*) + string * (* #Given | #Find | #Relate 21.3.02: discard ?*) + term * (* description *) + term list (* isalist2list t | [t] *) + ); +val e_ori_ = (0,[],"",e_term,[e_term]):ori; +val e_ori = (0,[],"",e_term,[e_term]):ori; + +fun ori2str ((i,vs,fi,t,ts):ori) = + "("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^ + (term2str t)^", "^((strs2str o (map term2str)) ts)^")"; +val oris2str = + let val s = !show_types + val _ = show_types:= true + val str = (strs2str' o (map (linefeed o ori2str))) + val _ = show_types:= s + in str end; + +(*.an or without leading integer.*) +type preori = (vats * + string * + term * + term list); +fun preori2str ((vs,fi,t,ts):preori) = + "("^((strs2str o (map string_of_int)) vs)^", "^fi^", "^ + (term2str t)^", "^((strs2str o (map term2str)) ts)^")"; +val preoris2str = (strs2str' o (map (linefeed o preori2str))); + +(*. given the input value (from split_dts) + make the value in a problem-env according to description-type .*) +(*28.8.01: .nam and .una impl. properly, others copied .. TODO*) +fun pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v = + if is_list v + then [v] (*eg. [r=Arbfix]*) + else (case v of (*eg. eps=#0*) + (Const ("op =",_) $ l $ r) => [r,l] + | _ => raise error ("pbl_ids Tools.nam: no equality " + ^(Syntax.string_of_term ctxt v))) + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v] + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v] + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v] + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v] + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v] + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v] + | pbl_ids ctxt _ v = raise error ("pbl_ids: not implemented for " + ^(Syntax.string_of_term ctxt v)); +(* +val t as t1 $ t2 = str2term "antiDerivativeName M_b"; +pbl_ids ctxt t1 t2; + + val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; + val (d,argl) = strip_comb t; + is_dsc d; (*see split_dts*) + dest_list (d,argl); + val (_ $ v) = t; + is_list v; + pbl_ids ctxt d v; +[Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $ + (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List.. + + val (dsc,vl) = (split_dts o term_of o the o (parse thy)) "solveFor x"; +val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term +val vl = Free ("x","RealDef.real") : term + + val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_"; + pbl_ids ctxt dsc vl; +val it = [Free ("x","RealDef.real")] : term list + + val (dsc,vl) = (split_dts o term_of o the o(parse thy)) + "errorBound (eps=#0)"; + val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_"; + pbl_ids ctxt dsc vl; +val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *) + +(*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!)) + make the value in a problem-env according to description-type .*) +(*28.8.01: .nam and .una impl. properly, others copied .. TODO*) +fun pbl_ids' (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) vs = + (case vs of + [] => raise error ("pbl_ids' Tools.nam called with []") + | [t] => (case t of (*eg. eps=#0*) + (Const ("op =",_) $ l $ r) => [r,l] + | _ => raise error ("pbl_ids' Tools.nam: no equality " + ^(Syntax.string_of_term (thy2ctxt' "Isac")t))) + | vs' => vs (*14.9.01: ???TODO *)) + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))vs = vs + | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))vs = vs + | pbl_ids' _ vs = + raise error ("pbl_ids': not implemented for " + ^(terms2str vs)); +(*9.5.03 penv postponed: pbl_ids'*) +fun pbl_ids' thy d vs = [comp_ts (d, vs)]; + + +(*14.9.01: not used after putting values for penv into itm_ + WN.5.5.03: used in upd .. upd_envv*) +fun upd_penv ctxt penv dsc (id, vl) = +(writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; + writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; + writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; + overwrite (penv, (id, pbl_ids ctxt dsc vl)) +); +(* + val penv = []; + val (dsc,vl) = (split_did o term_of o the o (parse thy)) "solveFor x"; + val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_"; + val penv = upd_penv thy penv dsc (id, vl); +[(Free ("v_","RealDef.real"), + [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")])] +: (term * term list) list + + val (dsc,vl) = (split_did o term_of o the o(parse thy))"errorBound (eps=#0)"; + val (dsc,id) = (split_did o term_of o the o(parse thy))"errorBound err_"; + upd_penv thy penv dsc (id, vl); +[(Free ("v_","RealDef.real"), + [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")]), + (Free ("err_","bool"), + [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")])] +: (term * term list) list ^.........!!!! +*) + +(*WN.9.5.03: not reconsidered; looks strange !!!*) +fun upd thy envv dsc (id, vl) i = + let val penv = case assoc (envv, i) of + SOME e => e + | NONE => []; + val penv' = upd_penv thy penv dsc (id, vl); + in (i, penv') end; +(* + val i = 2; + val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv; + val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b"; + val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_"; + upd thy envv dsc (id, vl) i; +val it = (2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])]) + : int * (term * term list) list*) + + +(*14.9.01: not used after putting pre-penv into itm_*) +fun upd_envv thy (envv:envv) (vats:vats) dsc id vl = + let val vats = if length vats = 0 + then (*unknown id to _all_ variants*) + if length envv = 0 then [1] + else (intsto o length) envv + else vats + fun isin vats (i,_) = member op = vats i; + val envs_notin_vat = filter_out (isin vats) envv; + in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end; +(* + val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv; + + val vats = [2] + val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b"; + val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_"; + val envv = upd_envv thy envv vats dsc id vl; +val envv = [(2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])] + : (int * (term * term list) list) list + + val vats = [1,2,3]; + val (dsc,vl) = (split_did o term_of o the o(parse thy))"maximum A"; + val (dsc,id) = (split_did o term_of o the o(parse thy))"maximum m_"; + upd_envv thy envv vats dsc id vl; +[(1,[(Free ("m_","bool"),[Free ("A","bool")])]), + (2, + [(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")]), + (Free ("m_","bool"),[Free ("A","bool")])]), + (3,[(Free ("m_","bool"),[Free ("A","bool")])])] +: (int * (term * term list) list) list + + + val env = []:envv; + val (d,ts) = (split_dts o term_of o the o (parse thy)) + "fixedValues [r=Arbfix]"; + val (_,id) = (split_did o term_of o the o (parse thy))"fixedValues fix_"; + val vats = [1,2,3]; + val env = upd_envv thy env vats d id (mkval ts); +*) + +(*. update envv by folding from a list of arguments .*) +fun upds_envv thy envv [] = envv + | upds_envv thy envv ((vs, dsc, id, vl)::ps) = + upds_envv thy (upd_envv thy envv vs dsc id vl) ps; +(* eval test-maximum.sml until Specify_Method ... + val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt []; + val met = (#ppc o get_met) mI; + + val envv = []; + val eargs = flat eargs; + val (vs, dsc, id, vl) = hd eargs; + val envv = upds_envv thy envv [(vs, dsc, id, vl)]; + + val (vs, dsc, id, vl) = hd (tl eargs); + val envv = upds_envv thy envv [(vs, dsc, id, vl)]; + + val (vs, dsc, id, vl) = hd (tl (tl eargs)); + val envv = upds_envv thy envv [(vs, dsc, id, vl)]; + + val (vs, dsc, id, vl) = hd (tl (tl (tl eargs))); + val envv = upds_envv thy envv [(vs, dsc, id, vl)]; +[(1, + [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), + (Free ("m_","bool"),[Free (#,#)]), + (Free ("vs_","bool List.list"),[# $ # $ Const #]), + (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]), + (2, + [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), + (Free ("m_","bool"),[Free (#,#)]), + (Free ("vs_","bool List.list"),[# $ # $ Const #]), + (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]), + (3, + [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), + (Free ("m_","bool"),[Free (#,#)]), + (Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *) + +(*for _output_ of the items of a Model*) +datatype item = + Correct of cterm' (*labels a correct formula (type cterm')*) + | SyntaxE of string (**) + | TypeE of string (**) + | False of cterm' (*WN050618 notexistent in itm_: only used in Where*) + | Incompl of cterm' (**) + | Superfl of string (**) + | Missing of cterm'; +fun item2str (Correct s) ="Correct " ^ s + | item2str (SyntaxE s) ="SyntaxE " ^ s + | item2str (TypeE s) ="TypeE " ^ s + | item2str (False s) ="False " ^ s + | item2str (Incompl s) ="Incompl " ^ s + | item2str (Superfl s) ="Superfl " ^ s + | item2str (Missing s) ="Missing " ^ s; +(*make string for error-msgs*) +fun itm_2str_ ctxt (Cor ((d,ts), penv)) = + "Cor " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ," + ^ pen2str ctxt penv + | itm_2str_ ctxt (Syn c) = "Syn " ^ c + | itm_2str_ ctxt (Typ c) = "Typ " ^ c + | itm_2str_ ctxt (Inc ((d,ts), penv)) = + "Inc " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ," + ^ pen2str ctxt penv + | itm_2str_ ctxt (Sup (d,ts)) = + "Sup " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) + | itm_2str_ ctxt (Mis (d,pid))= + "Mis "^ Syntax.string_of_term ctxt d ^ + " "^ Syntax.string_of_term ctxt pid + | itm_2str_ ctxt (Par s) = "Trm "^s; +fun itm_2str t = itm_2str_ (thy2ctxt' "Isac") t; +fun itm2str_ ctxt ((i,is,b,s,itm_):itm) = + "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^ + s^" ,"^(itm_2str_ ctxt itm_)^")"; +fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms); +fun w_itms2str_ ctxt itms = writeln (itms2str_ ctxt itms); + +fun init_item str = SyntaxE str; + + + + +type 'a ppc = + {Given : 'a list, + Where: 'a list, + Find : 'a list, + With : 'a list, + Relate: 'a list}; +fun ppc2str {Given=Given,Where=Where,Find=Find,With=With,Relate=Relate}= + ("{Given =" ^ (strs2str Given ) ^ + ",Where=" ^ (strs2str Where) ^ + ",Find =" ^ (strs2str Find ) ^ + ",With =" ^ (strs2str With ) ^ + ",Relate=" ^ (strs2str Relate) ^ "}"); + + + + +fun item_ppc ({Given = gi,Where= wh, + Find = fi,With = wi,Relate= re}: string ppc) = + {Given = map init_item gi,Where= map init_item wh, + Find = map init_item fi,With = map init_item wi, + Relate= map init_item re}:item ppc; +fun itemppc2str ({Given=Given,Where=Where, + Find=Find,With=With,Relate=Relate}:item ppc)= + ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^ + ",Where=" ^ ((strs2str' o (map item2str)) Where) ^ + ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^ + ",With =" ^ ((strs2str' o (map item2str)) With ) ^ + ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}"); + +fun de_item (Correct x) = x + | de_item (SyntaxE x) = x + | de_item (TypeE x) = x + | de_item (False x) = x + | de_item (Incompl x) = x + | de_item (Superfl x) = x + | de_item (Missing x) = x; +val empty_ppc ={Given = [], + Where= [], + Find = [], + With = [], + Relate= []}:item ppc; +val empty_ppc_ct' ={Given = [], + Where = [], + Find = [], + With = [], + Relate= []}:cterm' ppc; + + +datatype match = + Matches of pblID * item ppc +| NoMatch of pblID * item ppc; +fun match2str (Matches (pI, ppc)) = + "Matches ("^(strs2str pI)^", "^(itemppc2str ppc)^")" + | match2str(NoMatch (pI, ppc)) = + "NoMatch ("^(strs2str pI)^", "^(itemppc2str ppc)^")"; +fun matchs2str ms = (strs2str o (map match2str)) ms; +fun pblID_of_match (Matches (pI,_)) = pI + | pblID_of_match (NoMatch (pI,_)) = pI; + +(*10.03 for Refine_Problem*) +datatype match_ = + Match_ of pblID * ((itm list) * ((bool * term) list)) +| NoMatch_; + +(*. the refined pbt is the last_element Matches in the list .*) +fun is_matches (Matches _) = true + | is_matches _ = false; +fun matches_pblID (Matches (pI,_)) = pI; +fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms) + handle _ => []:pblID; +fun refined_IDitms ms = ((find_first is_matches) o rev) ms; + +(*. the refined pbt is the last_element Matches in the list, + for Refine_Problem, tryrefine .*) +fun is_matches_ (Match_ _) = true + | is_matches_ _ = false; +fun refined_ ms = ((find_first is_matches_) o rev) ms; + + +fun ts_in (Cor ((_,ts),_)) = ts + | ts_in (Syn (c)) = [] + | ts_in (Typ (c)) = [] + | ts_in (Inc ((_,ts),_)) = ts + | ts_in (Sup (_,ts)) = ts + | ts_in (Mis _) = []; +(*WN050629 unused*) +fun all_ts_in itm_s = (flat o (map ts_in)) itm_s; +val unique = (term_of o the o (parse (theory "Real"))) "UnIqE_tErM"; +fun d_in (Cor ((d,_),_)) = d + | d_in (Syn (c)) = (writeln("*** d_in: Syn ("^c^")"); unique) + | d_in (Typ (c)) = (writeln("*** d_in: Typ ("^c^")"); unique) + | d_in (Inc ((d,_),_)) = d + | d_in (Sup (d,_)) = d + | d_in (Mis (d,_)) = d; + +fun dts2str (d,ts) = pair2str (term2str d, terms2str ts); +fun penvval_in (Cor ((d,_),(_,ts))) = [comp_ts (d,ts)] + | penvval_in (Syn (c)) = (writeln("*** penvval_in: Syn ("^c^")"); []) + | penvval_in (Typ (c)) = (writeln("*** penvval_in: Typ ("^c^")"); []) + | penvval_in (Inc (_,(_,ts))) = ts + | penvval_in (Sup dts) = (writeln("*** penvval_in: Sup "^(dts2str dts)); []) + | penvval_in (Mis (d,t)) = (writeln("*** penvval_in: Mis "^ + (pair2str(term2str d, term2str t))); []); + + +(*. check a predicate labelled with indication of incomplete substitution; +rls -> (*for eval_true*) +bool * (*have _all_ variables(Free) from the model-pattern + been substituted by a value from the pattern's environment ?*) +term (*the precondition*) +-> +bool * (*has the precondition evaluated to true*) +term (*the precondition (for map)*) +.*) +fun evalprecond prls (false, pre) = + (*NOT ALL Free's have been substituted, eg. because of incomplete model*) + (false, pre) + | evalprecond prls (true, pre) = +(* val (prls, pre) = (prls, hd pres'); + val (prls, pre) = (prls, hd (tl pres')); + *) + if eval_true (assoc_thy "Isac.thy") (*for Pattern.match *) + [pre] prls (*pre parsed, prls.thy*) + then (true , pre) + else (false , pre); + +fun pre2str (b, t) = pair2str(bool2str b, term2str t); +fun pres2str pres = strs2str' (map (linefeed o pre2str) pres); + +(*. check preconditions, return true if all true .*) +fun check_preconds' _ [] _ _ = [] (*empty preconditions are true*) + | check_preconds' prls pres pbl _(*FIXME.WN0308 mvat re-introduce*) = +(* val (prls, pres, pbl, _) = (prls, where_, probl, 0); + val (prls, pres, pbl, _) = (prls, pre, itms, mvat); + *) + let val env = mk_env pbl; + val pres' = map (subst_atomic_all env) pres; + in map (evalprecond prls) pres' end; + +fun check_preconds thy prls pres pbl = + check_preconds' prls pres pbl (max_vt pbl); + +(*----------------------------------------------------------*) +end +open SpecifyTools; +(*----------------------------------------------------------*)