# HG changeset patch # User Walther Neuper # Date 1282131609 -7200 # Node ID 6c53fe2519e5d54e47e5d56a031e31a646e76477 # Parent 4afbcd0087995dcb5ca4a6af265d92bd62cf1f20 established thy-ctxt strategy (1..2) for ME/mstools.sml strategy in 2 steps: (1) update isac to Isabelle2009-2 with minimal changes (a) 'parse thy' left as is 'str2t' --> 'str2term_' according to (b) 'comp_dts thy' left as is, but returns term NOT cterm (b) pretty printing '*2str' always without thy | ctxt pretty printing '*2str_' always with ctxt (2) make parsing dependent on context of calculation (a) 'parse thy' --> 'parse ctxt' simplified by searchin 'thy' (b) nothin to do diff -r 4afbcd008799 -r 6c53fe2519e5 .hgignore --- a/.hgignore Tue Aug 17 09:05:51 2010 +0200 +++ b/.hgignore Wed Aug 18 13:40:09 2010 +0200 @@ -5,6 +5,7 @@ *.jar .DS_Store +*.orig syntax: regexp diff -r 4afbcd008799 -r 6c53fe2519e5 src/Tools/isac/CLEANUP --- a/src/Tools/isac/CLEANUP Tue Aug 17 09:05:51 2010 +0200 +++ b/src/Tools/isac/CLEANUP Wed Aug 18 13:40:09 2010 +0200 @@ -5,76 +5,33 @@ rm #* rm .#* rm *.tar* + rm *.orig cd .. cd ME rm *~ rm #* rm .#* rm *.tar* + rm *.orig cd .. cd xmlsrc rm *~ rm #* rm .#* rm *.tar* + rm *.orig cd .. cd FE-interface rm *~ rm #* rm .#* rm *.tar* + rm *.orig cd .. cd IsacKnowledge rm *~ rm #* rm .#* rm *.tar* + rm *.orig cd .. -cd systest - rm *~ - rm #* - rm .#* - rm *.tar* - cd ../.. -cd smltest - rm *~ - rm #* - rm .#* - rm *.tar* - cd ../ -cd smltest/FE-interface - rm *~ - rm #* - rm .#* - rm *.tar* - cd ../.. -cd smltest/IsacKnowledge - rm *~ - rm #* - rm .#* - rm *.tar* - cd ../.. -cd smltest/ME - rm *~ - rm #* - rm .#* - rm *.tar* - cd ../.. -cd smltest/Scripts - rm *~ - rm #* - rm .#* - rm *.tar* - cd ../.. -cd smltest/xmlsrc - rm *~ - rm #* - rm .#* - rm *.tar* - cd ../.. -cd sml/systest - rm *~ - rm #* - rm .#* - rm *.tar* - cd .. diff -r 4afbcd008799 -r 6c53fe2519e5 src/Tools/isac/Isac_Mathengine.thy --- a/src/Tools/isac/Isac_Mathengine.thy Tue Aug 17 09:05:51 2010 +0200 +++ b/src/Tools/isac/Isac_Mathengine.thy Wed Aug 18 13:40:09 2010 +0200 @@ -9,6 +9,9 @@ $ cd "/home/neuper/proto2/isac/src/sml" $ isabelle-process HOL HOL-Isac ML> use_thy "Isac_Mathengine"; + +12345678901234567890123456789012345678901234567890123456789012345678901234567890 + 10 20 30 40 50 60 70 80 *) header {* Loading the isac mathengine *} @@ -30,9 +33,16 @@ use_thy"Scripts/Script" use "Scripts/scrtools.sml" +ML {* +member; +@{term 111}; +*} + use "ME/mstools.sml" + + (* use "ME/ctree.sml" use "ME/ptyps.sml" diff -r 4afbcd008799 -r 6c53fe2519e5 src/Tools/isac/ME/calchead.sml --- a/src/Tools/isac/ME/calchead.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/src/Tools/isac/ME/calchead.sml Wed Aug 18 13:40:09 2010 +0200 @@ -1177,7 +1177,7 @@ | eq_untouched _ _ = false; val ppc' = ( - (*writeln("### insert_ppc: itm= "^(itm2str itm));*) + (*writeln("### insert_ppc: itm= "^(itm2str_ itm));*) case seek_ppc (#1 itm) ppc of (* val Some xxx = seek_ppc (#1 itm) ppc; *) @@ -1276,7 +1276,7 @@ (* val Add itm = appl_add thy sel oris pbl ppc ct; *) let - (*val _= writeln("###specify_additem: itm= "^(itm2str itm));*) + (*val _= writeln("###specify_additem: itm= "^(itm2str_ itm));*) val pbl' = insert_ppc thy itm pbl val ((p,Pbl),_,_,pt') = generate1 thy (case sel of @@ -1507,7 +1507,7 @@ (* val Add itm = appl_add thy sel oris pbl ppc ct; *) let - (*val _=writeln("###nxt_specif_additem: itm= "^(itm2str itm));*) + (*val _=writeln("###nxt_specif_additem: itm= "^(itm2str_ itm));*) val pbl' = insert_ppc thy itm pbl val (tac,tac_) = case sel of @@ -1939,8 +1939,8 @@ (* writeln (oris2str pors); - writeln (itms2str thy pits); - writeln (itms2str thy mits); + writeln (itms2str_ thy pits); + writeln (itms2str_ thy mits); *) diff -r 4afbcd008799 -r 6c53fe2519e5 src/Tools/isac/ME/ctree.sml --- a/src/Tools/isac/ME/ctree.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/src/Tools/isac/ME/ctree.sml Wed Aug 18 13:40:09 2010 +0200 @@ -646,7 +646,7 @@ (*| Match_Problem' (pI, (ok, (itms, pre))) => "Match_Problem' "^(spair2str (strs2str pI, spair2str (bool2str ok, - spair2str ("itms2str itms", + spair2str ("itms2str_ itms", "items2str pre"))))*) | Add_Given' cterm' => "Add_Given' "(*^cterm'*) | Del_Given' cterm' => "Del_Given' "(*^cterm'*) @@ -659,7 +659,7 @@ | Specify_Problem' (pI, (ok, (itms, pre))) => "Specify_Problem' "^(spair2str (strs2str pI, spair2str (bool2str ok, - spair2str ("itms2str itms", + spair2str ("itms2str_ itms", "items2str pre")))) | Specify_Method' (pI,oris,itms) => "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )" @@ -1510,7 +1510,7 @@ (apfst bool2str)))) bts; fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) = "("^bool2str b^", "^pos_2str p^", "^term2str hdf^ - ", "^itms2str (assoc_thy "Isac.thy") itms^ + ", "^itms2str_ (assoc_thy "Isac.thy") itms^ ", "^preconds2str prec^", \n"^spec2str spec^" )"; diff -r 4afbcd008799 -r 6c53fe2519e5 src/Tools/isac/ME/inform.sml --- a/src/Tools/isac/ME/inform.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/src/Tools/isac/ME/inform.sml Wed Aug 18 13:40:09 2010 +0200 @@ -252,7 +252,7 @@ (*this ^ should raise the exn on unability of re-parsing dts*) in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) | parsitm dI (itm as (i,v,_,f, Par _)) = - raise error ("parsitm ("^itm2str dI itm^ + raise error ("parsitm ("^itm2str_ dI itm^ "): Par should be internal"); (*separate a list to a pair of elements that do NOT satisfy the predicate, @@ -358,7 +358,7 @@ (#1 (some_spec ospec spec), oris, []:itm list, ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel)); val iii = appl_adds dI oris ppc pbt (selct::ss); - writeln(itms2str thy iii); + writeln(itms2str_ thy iii); val itm = appl_add' dI oris ppc pbt selct; val ppc = insert_ppc' itm ppc; @@ -370,7 +370,7 @@ val _::selct::ss = (selct::ss); val itm = appl_add' dI oris ppc pbt selct; val ppc = insert_ppc' itm ppc; - writeln(itms2str thy ppc); + writeln(itms2str_ thy ppc); val _::selct::ss = (selct::ss); val itm = appl_add' dI oris ppc pbt selct; @@ -393,7 +393,7 @@ fun par2fstr ((_,_,_,f, Par s):itm) = (f, s) | par2fstr itm = raise error ("par2fstr: called with "^ - itm2str (assoc_thy "Isac.thy") itm); + itm2str_ (assoc_thy "Isac.thy") itm); fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts)) | itms2fstr (_,_,_,f, Syn str) = (f, str) | itms2fstr (_,_,_,f, Typ str) = (f, str) @@ -401,7 +401,7 @@ | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts)) | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t)) | itms2fstr (itm as (_,_,_,f, Par _)) = - raise error ("parsitm ("^itm2str (assoc_thy "Isac.thy") itm^ + raise error ("parsitm ("^itm2str_ (assoc_thy "Isac.thy") itm^ "): Par should be internal"); fun imodel2fstr iitems = 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'; diff -r 4afbcd008799 -r 6c53fe2519e5 src/Tools/isac/Scripts/term_G.sml --- a/src/Tools/isac/Scripts/term_G.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/src/Tools/isac/Scripts/term_G.sml Wed Aug 18 13:40:09 2010 +0200 @@ -295,8 +295,8 @@ fun mk_prop t = Trueprop $ t; val true_as_term = Const("True",bool); val false_as_term = Const("False",bool); -val true_as_cterm = cterm_of HOL true_as_term; -val false_as_cterm = cterm_of HOL false_as_term; +val true_as_cterm = cterm_of (theory "HOL") true_as_term; +val false_as_cterm = cterm_of (theory "HOL") false_as_term; infixr 5 -->; (*2002 /Pure/term.ML *) infixr --->; (*2002 /Pure/term.ML *) @@ -1255,11 +1255,10 @@ *** Free ( R, RealDef.real) *) (*version for testing local to theories*) -fun str2t thy str = (term_of o the o (parse thy )) str; - -fun str2term str = (term_of o the o (parse (assoc_thy "Isac.thy"))) str; -fun str2termN str = (term_of o the o (parseN (assoc_thy "Isac.thy"))) str; +fun str2term_ thy str = (term_of o the o (parse thy)) str; +fun str2term str = (term_of o the o (parse (theory "Isac"))) str; fun strs2terms ss = map str2term ss; +fun str2termN str = (term_of o the o (parseN (theory "Isac"))) str; (*+ makes a substitution from the output of Pattern.match +*) (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*) diff -r 4afbcd008799 -r 6c53fe2519e5 src/Tools/isac/calcelems.sml --- a/src/Tools/isac/calcelems.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/src/Tools/isac/calcelems.sml Wed Aug 18 13:40:09 2010 +0200 @@ -131,12 +131,13 @@ (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently from rls, and then contain both Script _AND_ Rfuns !!!*) +fun thy2ctxt thy' = ProofContext.init_global (theory thy'); (*FIXXXME thy-ctxt*) (*ctxt for retrieval of all thms in HOL; FIXME make this local?*) -val ctxt_HOL = ProofContext.init_global (theory "Complex_Main"); -val HOL = ProofContext.theory_of ctxt_HOL; +(*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*) +val ctxt_HOL = thy2ctxt "Complex_Main"; (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*) -fun ctxt_Isac _ = ProofContext.init_global (theory "Isac"); +fun ctxt_Isac _ = thy2ctxt "Isac"; fun Isac _ = ProofContext.theory_of (ctxt_Isac""); val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" ); diff -r 4afbcd008799 -r 6c53fe2519e5 test/Tools/isac/IsacKnowledge/atools.sml --- a/test/Tools/isac/IsacKnowledge/atools.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/test/Tools/isac/IsacKnowledge/atools.sml Wed Aug 18 13:40:09 2010 +0200 @@ -23,9 +23,9 @@ "----------- occurs_in -------------------------------------------"; "----------- occurs_in -------------------------------------------"; "----------- occurs_in -------------------------------------------"; -fun str2t str = (term_of o the o (parse thy )) str; +fun str2term str = (term_of o the o (parse thy )) str; fun term2s t = Sign.string_of_term (sign_of thy) t; -val t = str2t "x"; +val t = str2term "x"; if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f"; val t = str2term "x occurs_in x"; @@ -53,7 +53,7 @@ "----------- argument_of -----------------------------------------"; "----------- argument_of -----------------------------------------"; "----------- argument_of -----------------------------------------"; -val t = str2t "argument_in (M_b x)"; +val t = str2term "argument_in (M_b x)"; val Some (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0; if term2s t' = "(argument_in M_b x) = x" then () else raise error "atools.sml:(argument_in M_b x) = x ???"; diff -r 4afbcd008799 -r 6c53fe2519e5 test/Tools/isac/IsacKnowledge/biegelinie.sml --- a/test/Tools/isac/IsacKnowledge/biegelinie.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/test/Tools/isac/IsacKnowledge/biegelinie.sml Wed Aug 18 13:40:09 2010 +0200 @@ -30,20 +30,20 @@ "----------- the rules -------------------------------------------"; "----------- the rules -------------------------------------------"; "----------- the rules -------------------------------------------"; -fun str2t str = (term_of o the o (parse Biegelinie.thy)) str; +fun str2term str = (term_of o the o (parse Biegelinie.thy)) str; fun term2s t = Sign.string_of_term (sign_of Biegelinie.thy) t; fun rewrit thm str = fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str)); -val t = rewrit Belastung_Querkraft (str2t "- q_ x = - q_0"); term2s t; +val t = rewrit Belastung_Querkraft (str2term "- q_ x = - q_0"); term2s t; if term2s t = "Q' x = - q_0" then () else raise error "/biegelinie.sml: Belastung_Querkraft"; -val t = rewrit Querkraft_Moment (str2t "Q x = - q_0 * x + c"); term2s t; +val t = rewrit Querkraft_Moment (str2term "Q x = - q_0 * x + c"); term2s t; if term2s t = "M_b' x = - q_0 * x + c" then () else raise error "/biegelinie.sml: Querkraft_Moment"; -val t = rewrit Moment_Neigung (str2t "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x"); +val t = rewrit Moment_Neigung (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x"); term2s t; if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then () else raise error "biegelinie.sml: Moment_Neigung"; @@ -125,7 +125,7 @@ "----------- IntegrierenUndKonstanteBestimmen by rewriting -------"; "----------- IntegrierenUndKonstanteBestimmen by rewriting -------"; "----------- IntegrierenUndKonstanteBestimmen by rewriting -------"; -val t = str2t "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"; +val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"; val t = rewrit Moment_Neigung t; term2s t; (*was "EI * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" ### before declaring "y''" as a constant *) @@ -191,18 +191,18 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; -val pits = get_obj g_pbl pt (fst p);writeln (itms2str thy pits); -(*if itms2str thy pits = ... all 5 model-items*) -val mits = get_obj g_met pt (fst p); writeln (itms2str thy mits); -if itms2str thy mits = "[]" then () +val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits); +(*if itms2str_ ctxt pits = ... all 5 model-items*) +val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits); +if itms2str_ ctxt mits = "[]" then () else raise error "biegelinie.sml: Bsp 7.27 #2"; val (p,_,f,nxt,_,pt) = me nxt p c pt; case nxt of (_,Add_Given "FunktionsVariable x") => () | _ => raise error "biegelinie.sml: Bsp 7.27 #4a"; val (p,_,f,nxt,_,pt) = me nxt p c pt; -val mits = get_obj g_met pt (fst p);writeln (itms2str thy mits); -(*if itms2str thy mits = ... all 6 guard-items*) +val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits); +(*if itms2str_ ctxt mits = ... all 6 guard-items*) case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () | _ => raise error "biegelinie.sml: Bsp 7.27 #4b"; diff -r 4afbcd008799 -r 6c53fe2519e5 test/Tools/isac/IsacKnowledge/diffapp.sml --- a/test/Tools/isac/IsacKnowledge/diffapp.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/test/Tools/isac/IsacKnowledge/diffapp.sml Wed Aug 18 13:40:09 2010 +0200 @@ -283,10 +283,10 @@ | _ => raise error "diffapp.sml: max-exp me, nxt = Specify_Method"; val oris = fst3 (get_obj g_origin pt (fst p)); writeln(oris2str oris); -val pits = get_obj g_pbl pt (fst p); writeln(itms2str thy pits); +val pits = get_obj g_pbl pt (fst p); writeln(itms2str_ ctxt pits); val (p,_,f,nxt,_,pt) = me nxt p c pt; -val mits = get_obj g_met pt (fst p); writeln(itms2str thy mits); +val mits = get_obj g_met pt (fst p); writeln(itms2str_ ctxt mits); val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -311,7 +311,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris); -val pits = get_obj g_pbl pt (fst p);writeln(itms2str thy pits); +val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits); val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -344,7 +344,7 @@ (*val nxt = Refine_Tacitly ["univariate","equation"])*) val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris); -val pits = get_obj g_pbl pt (fst p);writeln(itms2str thy pits); +val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits); val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -377,11 +377,11 @@ val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris); -val pits = get_obj g_pbl pt (fst p);writeln(itms2str thy pits); -val pits = get_obj g_pbl pt [];writeln(itms2str thy pits); +val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits); +val pits = get_obj g_pbl pt [];writeln(itms2str_ ctxt pits); -val mits = get_obj g_met pt (fst p);writeln(itms2str thy mits); -val mits = get_obj g_met pt [];writeln(itms2str thy mits); +val mits = get_obj g_met pt (fst p);writeln(itms2str_ ctxt mits); +val mits = get_obj g_met pt [];writeln(itms2str_ ctxt mits); itms2args thy ["DiffApp","max_by_calculus"] mits; @@ -426,14 +426,14 @@ fetchProposedTactic 1; val ((pt,p),_) = get_calc 1; val mits = get_obj g_met pt (fst p); - writeln (itms2str thy mits); + writeln (itms2str_ ctxt mits); (* - if itms2str thy mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd rs_) ,(t_, [hd rs_])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_ ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0_, [v__0]))]" then () + if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd rs_) ,(t_, [hd rs_])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_ ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0_, [v__0]))]" then () else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1"; *) (*FIXME: the environments contain identifers, and NOT values ?!?!?*) (* WN051209 while extending 'fun step' for initac, this became better ... - if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then () + if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then () else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1"; *) diff -r 4afbcd008799 -r 6c53fe2519e5 test/Tools/isac/IsacKnowledge/eqsystem.sml --- a/test/Tools/isac/IsacKnowledge/eqsystem.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/test/Tools/isac/IsacKnowledge/eqsystem.sml Wed Aug 18 13:40:09 2010 +0200 @@ -813,7 +813,7 @@ -----fun refin' ff: -> (writeln o (itms2str Isac.thy)) itms; +> (writeln o (itms2str_ (thy2ctxt "Isac"))) itms; [ (1 ,[1] ,true ,#Given ,Cor equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2, @@ -828,7 +828,7 @@ (true, length_ [c, c_2] = 2)] ----- fun match_oris': -> (writeln o (itms2str Isac.thy)) itms; +> (writeln o (itms2str_ (thy2ctxt "Isac"))) itms; > (writeln o pres2str) pre'; ..as in refin' @@ -895,7 +895,8 @@ | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution"; val (p,_,f,nxt,_,pt) = me nxt p c pt; -val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl; +val PblObj {probl,...} = get_obj I pt [5]; + (writeln o (itms2str_ (thy2ctxt "Isac"))) probl; (*[ (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])), (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])), @@ -963,7 +964,8 @@ | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution b"; val (p,_,f,nxt,_,pt) = me nxt p c pt; -val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl; +val PblObj {probl,...} = get_obj I pt [5]; + (writeln o (itms2str_ (thy2ctxt "Isac"))) probl; (*[ (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])), (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])), diff -r 4afbcd008799 -r 6c53fe2519e5 test/Tools/isac/IsacKnowledge/integrate.sml --- a/test/Tools/isac/IsacKnowledge/integrate.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/test/Tools/isac/IsacKnowledge/integrate.sml Wed Aug 18 13:40:09 2010 +0200 @@ -36,14 +36,14 @@ "----------- parsing ---------------------------------------------"; "----------- parsing ---------------------------------------------"; "----------- parsing ---------------------------------------------"; -fun str2t str = (term_of o the o (parse Integrate.thy)) str; +fun str2term str = (term_of o the o (parse Integrate.thy)) str; fun term2s t = Sign.string_of_term (sign_of Integrate.thy) t; -val t = str2t "Integral x D x"; -val t = str2t "Integral x^^^2 D x"; +val t = str2term "Integral x D x"; +val t = str2term "Integral x^^^2 D x"; atomty t; -val t = str2t "ff x is_f_x"; +val t = str2term "ff x is_f_x"; case t of Const ("Integrate.is'_f'_x", _) $ _ => () | _ => raise error "integrate.sml: parsing: ff x is_f_x"; @@ -64,27 +64,27 @@ Thm ("not_false",not_false) ], scr = EmptyScr}; -val subs = [(str2t "bdv", str2t "x")]; +val subs = [(str2term "bdv", str2term "x")]; fun rewrit thm str = fst (the (rewrite_inst_ Integrate.thy tless_true conditions_in_integration_rules true subs thm str)); -val str = rewrit integral_const (str2t "Integral 1 D x"); term2s str; -val str = rewrit integral_const (str2t "Integral M'/EJ D x"); term2s str; -val str = (rewrit integral_const (str2t "Integral x D x")) - handle OPTION => str2t "no_rewrite"; +val str = rewrit integral_const (str2term "Integral 1 D x"); term2s str; +val str = rewrit integral_const (str2term "Integral M'/EJ D x"); term2s str; +val str = (rewrit integral_const (str2term "Integral x D x")) + handle OPTION => str2term "no_rewrite"; -val str = rewrit integral_var (str2t "Integral x D x"); term2s str; -val str = (rewrit integral_var (str2t "Integral a D x")) - handle OPTION => str2t "no_rewrite"; +val str = rewrit integral_var (str2term "Integral x D x"); term2s str; +val str = (rewrit integral_var (str2term "Integral a D x")) + handle OPTION => str2term "no_rewrite"; -val str = rewrit integral_add (str2t "Integral x + 1 D x"); term2s str; +val str = rewrit integral_add (str2term "Integral x + 1 D x"); term2s str; -val str = rewrit integral_mult (str2t "Integral M'/EJ * x^^^3 D x");term2s str; -val str = (rewrit integral_mult (str2t "Integral x * x D x")) - handle OPTION => str2t "no_rewrite"; +val str = rewrit integral_mult (str2term "Integral M'/EJ * x^^^3 D x");term2s str; +val str = (rewrit integral_mult (str2term "Integral x * x D x")) + handle OPTION => str2term "no_rewrite"; -val str = rewrit integral_pow (str2t "Integral x^^^3 D x"); term2s str; +val str = rewrit integral_pow (str2term "Integral x^^^3 D x"); term2s str; "----------- test add_new_c, is_f_x ------------------------------"; @@ -112,27 +112,27 @@ (*WN080222 replace call_new_c with add_new_c---------------------- -val term = str2t "new_c (c * x^^^2 + c_2)"; +val term = str2term "new_c (c * x^^^2 + c_2)"; val Some (_,t') = eval_new_c 0 0 term 0; if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then () else raise error "integrate.sml: eval_new_c ???"; -val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)"; +val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2)"; val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t'; if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then () else raise error "integrate.sml: matches new_c = False"; -val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)"; +val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)"; val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t'; if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True" then () else raise error "integrate.sml: matches new_c = True"; -val t = str2t "ff x is_f_x"; +val t = str2term "ff x is_f_x"; val Some (_,t') = eval_is_f_x "" "" t thy; term2s t'; if term2s t' = "(ff x is_f_x) = True" then () else raise error "integrate.sml: eval_is_f_x --> true"; -val t = str2t "q_0/2 * L * x is_f_x"; +val t = str2term "q_0/2 * L * x is_f_x"; val Some (_,t') = eval_is_f_x "" "" t thy; term2s t'; if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then () else raise error "integrate.sml: eval_is_f_x --> false"; @@ -153,15 +153,15 @@ fun rewrit thm t = fst (the (rewrite_inst_ Integrate.thy tless_true conditions_in_integration true subs thm t)); -val t = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s t; +val t = rewrit call_for_new_c (str2term "x ^^^ 2 / 2"); term2s t; val t = (rewrit call_for_new_c t) - handle OPTION => str2t "no_rewrite"; + handle OPTION => str2term "no_rewrite"; val t = rewrit call_for_new_c - (str2t "ff x = q_0/2 *L*x"); term2s t; + (str2term "ff x = q_0/2 *L*x"); term2s t; val t = (rewrit call_for_new_c - (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x")) - handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite"; + (str2term "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x")) + handle OPTION => (*NOT: + new_c ..=..!!*)str2term "no_rewrite"; --------------------------------------------------------------------*) @@ -347,7 +347,7 @@ if F1_ = F2_ then () else raise error "integrate.sml: unequal find's"; val ((dsc as Const ("Integrate.antiDerivativeName", _)) - $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff"; + $ Free ("ff", F3_type)) = str2term "antiDerivativeName ff"; if is_dsc dsc then () else raise error "integrate.sml: no description"; if F1_type = F3_type then () else raise error "integrate.sml: unequal types in find's"; diff -r 4afbcd008799 -r 6c53fe2519e5 test/Tools/isac/IsacKnowledge/poly.sml --- a/test/Tools/isac/IsacKnowledge/poly.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/test/Tools/isac/IsacKnowledge/poly.sml Wed Aug 18 13:40:09 2010 +0200 @@ -356,7 +356,7 @@ val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -(writeln o (itms2str thy)) (get_obj g_pbl pt (fst p)); +(writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; diff -r 4afbcd008799 -r 6c53fe2519e5 test/Tools/isac/ME/calchead.sml --- a/test/Tools/isac/ME/calchead.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/test/Tools/isac/ME/calchead.sml Wed Aug 18 13:40:09 2010 +0200 @@ -210,7 +210,7 @@ (*val nxt = Specify_Theory "DiffApp.thy" : tac*) -val itms = get_obj g_pbl pt (fst p);writeln(itms2str thy itms); +val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms); val nxt = tac2tac_ pt p nxt; val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; diff -r 4afbcd008799 -r 6c53fe2519e5 test/Tools/isac/ME/ctree.sml --- a/test/Tools/isac/ME/ctree.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/test/Tools/isac/ME/ctree.sml Wed Aug 18 13:40:09 2010 +0200 @@ -72,13 +72,13 @@ val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* nxt = Add_Given "equality (x + 1 = 2)" - (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p)); + (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p)); +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p)); +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -421,13 +421,13 @@ val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* nxt = Add_Given "equality (x + 1 = 2)" - (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p)); + (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p)); +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p)); +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; diff -r 4afbcd008799 -r 6c53fe2519e5 test/Tools/isac/ME/inform.sml --- a/test/Tools/isac/ME/inform.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/test/Tools/isac/ME/inform.sml Wed Aug 18 13:40:09 2010 +0200 @@ -371,11 +371,11 @@ (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*) val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)]; (*val nxt = ("Model_Problem", ...*) - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "fixedValues [r = Arbfix]"*) - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; (*[ (0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])), (0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])), @@ -384,7 +384,7 @@ (*the empty CalcHead is checked w.r.t the model and re-established as such*) val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec); - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () else raise error "informtest.sml: diff.behav. max 1"; (*there is one input to the model (could be more)*) @@ -392,7 +392,7 @@ input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"], Find ["maximum", "valuesFor"], Relate ["relations"]], Pbl, e_spec); - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () else raise error "informtest.sml: diff.behav. max 2"; @@ -402,7 +402,7 @@ Find ["maximum A", "valuesFor [a,b]"], Relate ["relations [A=a*b, a/2=r*sin alpha, \ \b/2=r*cos alpha]"]], Pbl, e_spec); - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl; + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl; if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*) (*this input is complete in variant 1 (variant 3 does not work yet)*) @@ -412,7 +412,7 @@ Relate ["relations [A=a*b, \ \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl, e_spec); - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl; + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl; modifycalcheadOK2xml 111 (bool2str b) ocalhd; *) @@ -522,8 +522,8 @@ print_depth 5; writeln"-----------------------------------------------------------"; spec; -writeln (itms2str thy probl); -writeln (itms2str thy meth); +writeln (itms2str_ ctxt probl); +writeln (itms2str_ ctxt meth); writeln (istate2str istate); print_depth 3; @@ -547,12 +547,12 @@ (*("Isac.thy", ["derivative_of", "function"], ["diff", "differentiate_on_R"]) : spec*) -writeln (itms2str thy probl); +writeln (itms2str_ ctxt probl); (*[ (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), (3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*) -writeln (itms2str thy meth); +writeln (itms2str_ ctxt meth); (*[ (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), @@ -592,12 +592,12 @@ (*("Isac.thy", ["derivative_of", "function"], ["diff", "differentiate_on_R"]) : spec*) -writeln (itms2str thy probl); +writeln (itms2str_ ctxt probl); (*[ (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), (3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*) -writeln (itms2str thy meth); +writeln (itms2str_ ctxt meth); (*[ (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), diff -r 4afbcd008799 -r 6c53fe2519e5 test/Tools/isac/ME/me.sml --- a/test/Tools/isac/ME/me.sml Tue Aug 17 09:05:51 2010 +0200 +++ b/test/Tools/isac/ME/me.sml Wed Aug 18 13:40:09 2010 +0200 @@ -344,23 +344,23 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; (*xt = Add_Given "solveFor x"*) - writeln (itms2str thy (get_obj g_pbl pt (fst p))); + writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p))); (*[ (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])), (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])), (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*) val (pt,p) = complete_mod (pt, p); - if itms2str thy (get_obj g_pbl pt (fst p)) = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then () + if itms2str_ ctxt (get_obj g_pbl pt (fst p)) = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then () else raise error "completetest.sml: new behav. in complete_mod 1"; - writeln (itms2str thy (get_obj g_pbl pt (fst p))); + writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p))); (*[ (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])), (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])), (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*) val mits = get_obj g_met pt (fst p); - if itms2str thy mits = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" + if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then () else raise error "completetest.sml: new behav. in complete_mod 2"; - writeln (itms2str thy mits); + writeln (itms2str_ ctxt mits); (*[ (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])), (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])), @@ -446,7 +446,7 @@ (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]), (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*) val pits = get_obj g_pbl pt (fst p); - writeln (itms2str thy pits); + writeln (itms2str_ ctxt pits); (*[ (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])), (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])), @@ -456,7 +456,7 @@ val mits = get_obj g_met pt (fst p); val mits = complete_metitms oris pits [] ((#ppc o get_met) ["DiffApp","max_by_calculus"]); - writeln (itms2str thy mits); + writeln (itms2str_ ctxt mits); (*[ (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])), @@ -467,7 +467,7 @@ (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x. 0 <= x & x <= 2 * r}])), (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*) - if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then () + if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then () else raise error "completetest.sml: new behav. in complete_metitms 1"; @@ -494,7 +494,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*) val pits = get_obj g_pbl pt (fst p); - writeln (itms2str thy pits); + writeln (itms2str_ ctxt pits); (*[ (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])), (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])), @@ -502,9 +502,9 @@ (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*) val (pt,p) = complete_mod (pt,p); val pits = get_obj g_pbl pt (fst p); - if itms2str thy pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]" + if itms2str_ ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]" then () else raise error "completetest.sml: new behav. in complete_mod 3"; - writeln (itms2str thy pits); + writeln (itms2str_ ctxt pits); (*[ (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])), @@ -512,9 +512,9 @@ (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*) val mits = get_obj g_met pt (fst p); - if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" + if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then () else raise error "completetest.sml: new behav. in complete_mod 3"; - writeln (itms2str thy mits); + writeln (itms2str_ ctxt mits); (*[ (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),