diff -r 4afbcd008799 -r 6c53fe2519e5 src/Tools/isac/ME/mstools.sml --- a/src/Tools/isac/ME/mstools.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/src/Tools/isac/ME/mstools.sml Wed Aug 18 13:40:09 2010 +0200 @@ -7,6 +7,8 @@ use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*); use"mstools.sml"; +12345678901234567890123456789012345678901234567890123456789012345678901234567890 + 10 20 30 40 50 60 70 80 *) signature SPECIFY_TOOLS = @@ -23,19 +25,19 @@ | TypeE of string val item2str : item -> string type itm - val itm2str : Theory.theory -> itm -> string + val itm2str_ : Proof.context -> itm -> string datatype itm_ = - Cor of (Term.term * Term.term list) * (Term.term * Term.term list) - | Inc of (Term.term * Term.term list) * (Term.term * Term.term list) - | Mis of Term.term * Term.term + 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 * Term.term list + | Sup of term * term list | Syn of cterm' | Typ of cterm' val itm_2str : itm_ -> string - val itm__2str : Theory.theory -> itm_ -> string - val itms2str : Theory.theory -> itm list -> 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, @@ -47,7 +49,7 @@ val match2str : match -> string datatype match_ = - Match_ of pblID * (itm list * (bool * Term.term) list) + Match_ of pblID * (itm list * (bool * term) list) | NoMatch_ val matchs2str : match list -> string type ori @@ -57,108 +59,107 @@ val preori2str : preori -> string val preoris2str : preori list -> string type penv - (* val penv2str : Theory.theory -> penv -> string *) + (* val penv2str_ : Proof.context -> penv -> string *) type vats (*----------------------------------------------------------------------*) - val all_ts_in : itm_ list -> Term.term list + val all_ts_in : itm_ list -> term list val check_preconds : 'a -> rls -> - Term.term list -> itm list -> (bool * Term.term) list + term list -> itm list -> (bool * term) list val check_preconds' : rls -> - Term.term list -> - itm list -> 'a -> (bool * Term.term) list - (* val chkpre2item : rls -> Term.term -> bool * item *) - val pres2str : (bool * Term.term) list -> string - (* val evalprecond : rls -> Term.term -> bool * Term.term *) + 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.theory -> Term.term * Term.term list -> Thm.cterm - val comp_dts' : Term.term * Term.term list -> Term.term - val comp_dts'' : Term.term * Term.term list -> string - val comp_ts : Term.term * Term.term list -> Term.term - val d_in : itm_ -> Term.term + 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 * Term.term list -> Term.term list (* for testing *) - val dest_list' : Term.term -> Term.term list - val dts2str : Term.term * Term.term list -> string + 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.term *) - (* val e_listReal : Term.term *) + (* 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 * Term.term list -> Term.term * Term.term *) + (* val getval : term * term list -> term * term *) (*val head_precond : domID * pblID * 'a -> - Term.term Library.option -> + term option -> rls -> - Term.term list -> - itm list -> 'b -> Term.term * (bool * Term.term) list*) + 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.term -> bool + val is_var : term -> bool (* val item_ppc : string ppc -> item ppc *) val itemppc2str : item ppc -> string - val linefeed : string -> 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 * Term.term) list - val mk_en : int -> itm -> (Term.term * Term.term) list - val mk_env : itm list -> (Term.term * Term.term) list - val mkval : 'a -> Term.term list -> Term.term - val mkval' : Term.term list -> Term.term + 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 : Theory.theory -> Term.term -> Term.term -> Term.term list - val pbl_ids' : 'a -> Term.term -> Term.term list -> Term.term list - (* val pen2str : Theory.theory -> Term.term * Term.term list -> string *) - val penvval_in : itm_ -> Term.term list + 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_ Library.option + match_ list -> match_ option (* val refined_IDitms : - match list -> match Library.option *) - val split_dts : 'a -> Term.term -> Term.term * Term.term list - val split_dts' : Term.term * Term.term -> Term.term list - (* val take_apart : Term.term -> Term.term list *) - (* val take_apart_inv : Term.term list -> Term.term *) - val ts_in : itm_ -> Term.term list - (* val unique : Term.term *) + 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 : - Theory.theory -> - (''a * (''b * Term.term list) list) list -> - Term.term -> - ''b * Term.term -> ''a -> ''a * (''b * Term.term list) list + Proof.context -> + (''a * (''b * term list) list) list -> + term -> + ''b * term -> ''a -> ''a * (''b * term list) list val upd_envv : - Theory.theory -> + Proof.context -> envv -> vats -> - Term.term -> Term.term -> Term.term -> envv + term -> term -> term -> envv val upd_penv : - Theory.theory -> - (''a * Term.term list) list -> - Term.term -> ''a * Term.term -> (''a * Term.term list) list + Proof.context -> + (''a * term list) list -> + term -> ''a * term -> (''a * term list) list (* val upds_envv : - Theory.theory -> + Proof.context -> envv -> - (vats * Term.term * Term.term * Term.term) list -> + (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 : Theory.theory -> itm list -> unit *) + (* val w_itms2str_ : Proof.context -> itm list -> unit *) end (*----------------------------------------------------------*) structure SpecifyTools : SPECIFY_TOOLS = struct (*----------------------------------------------------------*) -val e_listReal = (term_of o the o (parse Script.thy)) "[]::(real list)"; -val e_listBool = (term_of o the o (parse Script.thy)) "[]::(bool list)"; +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 = @@ -197,18 +198,28 @@ 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") +(*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") + (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)))); + " $ "^(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) @@ -365,10 +376,10 @@ type penv = (term (*err_*) * (term list) (*[#0, epsilon] 9.5.03 outcommented*) ) list; -fun pen2str thy (t, ts) = - pair2str(Syntax.string_of_term GOON (sign_of thy) t, - (strs2str' o map (Sign.string_of_term (sign_of thy))) ts); -fun penv2str thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv; +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*) @@ -388,7 +399,7 @@ fun getval (id, values) = case values of [] => raise error ("penv_value: no values in '"^ - (Sign.string_of_term (sign_of Tools.thy) id)) + (Syntax.string_of_term (thy2ctxt "Tools") id)) | [v] => (id, v) | (v1::v2::_) => (case v1 of Const ("Script.Arbfix",_) => (id, v2) @@ -535,7 +546,7 @@ | mk_e (Sup _) = [] | mk_e (Mis _) = []; fun mk_en vt ((i,vts,b,f,itm_):itm) = - if vt mem vts then mk_e itm_ else []; + 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 = @@ -580,25 +591,24 @@ (*. 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*) -(*9.5.03 penv-concept postponed *) -fun pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v = +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 " - ^(Sign.string_of_term (sign_of thy) v))) - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v] - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v] - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v] - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v] - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v] - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v] - | pbl_ids thy _ v = raise error ("pbl_ids: not implemented for " - ^(Sign.string_of_term (sign_of thy) v)); + ^(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 thy t1 t2; +pbl_ids ctxt t1 t2; val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; val (d,argl) = strip_comb t; @@ -606,7 +616,7 @@ dest_list (d,argl); val (_ $ v) = t; is_list v; - pbl_ids thy d 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.. @@ -615,13 +625,13 @@ val vl = Free ("x","RealDef.real") : term val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_"; - pbl_ids thy dsc vl; + 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 thy dsc vl; + 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!!)) @@ -633,7 +643,7 @@ | [t] => (case t of (*eg. eps=#0*) (Const ("op =",_) $ l $ r) => [r,l] | _ => raise error ("pbl_ids' Tools.nam: no equality " - ^(Sign.string_of_term (sign_of thy) t))) + ^(Syntax.string_of_term (ctxt_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 @@ -650,11 +660,11 @@ (*14.9.01: not used after putting values for penv into itm_ WN.5.5.03: used in upd .. upd_envv*) -fun upd_penv thy penv dsc (id, vl) = +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 thy dsc vl)) + overwrite (penv, (id, pbl_ids ctxt dsc vl)) ); (* val penv = []; @@ -678,8 +688,8 @@ (*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 => []; + SOME e => e + | NONE => []; val penv' = upd_penv thy penv dsc (id, vl); in (i, penv') end; (* @@ -699,7 +709,7 @@ if length envv = 0 then [1] else (intsto o length) envv else vats - fun isin vats (i,_) = i mem 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; (* @@ -777,32 +787,34 @@ | 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; +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 thy (Cor ((d,ts), penv)) = - "Cor " ^ string_of_cterm (comp_dts thy(d,ts)) ^" ,"^ pen2str thy penv - | itm__2str thy (Syn c) = "Syn "^c - | itm__2str thy (Typ c) = "Typ "^c - | itm__2str thy (Inc ((d,ts), penv)) = - "Inc " ^ string_of_cterm (comp_dts thy(d,ts)) ^" ,"^ pen2str thy penv - | itm__2str thy (Sup (d,ts)) = "Sup "^(string_of_cterm (comp_dts thy(d,ts))) - | itm__2str thy (Mis (d,pid))= - "Mis "^ Sign.string_of_term (sign_of thy) d ^ - " "^ Sign.string_of_term (sign_of thy) pid - | itm__2str thy (Par s) = "Trm "^s; -fun itm_2str t = itm__2str (assoc_thy "Isac.thy") t; -fun itm2str thy ((i,is,b,s,itm_):itm) = +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 thy itm_)^")"; -val linefeed = (curry op^) "\n"; -fun itms2str thy itms = strs2str' (map (linefeed o (itm2str thy)) itms); -fun w_itms2str thy itms = writeln (itms2str thy itms); + 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; @@ -896,7 +908,7 @@ | 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 Real.thy)) "UnIqE_tErM"; +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) @@ -918,10 +930,10 @@ rls -> (*for eval_true*) bool * (*have _all_ variables(Free) from the model-pattern been substituted by a value from the pattern's environment ?*) -Term.term (*the precondition*) +term (*the precondition*) -> bool * (*has the precondition evaluated to true*) -Term.term (*the precondition (for map)*) +term (*the precondition (for map)*) .*) fun evalprecond prls (false, pre) = (*NOT ALL Free's have been substituted, eg. because of incomplete model*) @@ -969,9 +981,9 @@ fun cpy its [] (f, (d, id)) = if length its = 0 (*no dsc found in pbl*) then case find_first (vt_and_dsc d) oris - of Some (i,v,_,_,ts) => + of SOME (i,v,_,_,ts) => [(i,v,true,f, Cor ((d,ts), (id,pbl_ids' thy d ts)))] - | None => [(0,[],false,f,Mis (d, id))] + | NONE => [(0,[],false,f,Mis (d, id))] else its | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) = if d = d_in itm_ andalso i<>0 (*already touched by user*) @@ -1018,7 +1030,7 @@ fun copy_pbl (pbl:itm list) met oris = let fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_; fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of - Some _ => false | None => true; + SOME _ => false | NONE => true; (*1*)val mis = ((map (cons2 (fst, fst o snd))) o (filter (notmem pbl))) met; fun eqdsc_ori d ((_,_,_,d',_):ori) = d = d';