1.1 --- a/.hgignore Tue Aug 17 09:05:51 2010 +0200
1.2 +++ b/.hgignore Wed Aug 18 13:40:09 2010 +0200
1.3 @@ -5,6 +5,7 @@
1.4 *.jar
1.5 .DS_Store
1.6
1.7 +*.orig
1.8
1.9 syntax: regexp
1.10
2.1 --- a/src/Tools/isac/CLEANUP Tue Aug 17 09:05:51 2010 +0200
2.2 +++ b/src/Tools/isac/CLEANUP Wed Aug 18 13:40:09 2010 +0200
2.3 @@ -5,76 +5,33 @@
2.4 rm #*
2.5 rm .#*
2.6 rm *.tar*
2.7 + rm *.orig
2.8 cd ..
2.9 cd ME
2.10 rm *~
2.11 rm #*
2.12 rm .#*
2.13 rm *.tar*
2.14 + rm *.orig
2.15 cd ..
2.16 cd xmlsrc
2.17 rm *~
2.18 rm #*
2.19 rm .#*
2.20 rm *.tar*
2.21 + rm *.orig
2.22 cd ..
2.23 cd FE-interface
2.24 rm *~
2.25 rm #*
2.26 rm .#*
2.27 rm *.tar*
2.28 + rm *.orig
2.29 cd ..
2.30 cd IsacKnowledge
2.31 rm *~
2.32 rm #*
2.33 rm .#*
2.34 rm *.tar*
2.35 + rm *.orig
2.36 cd ..
2.37 -cd systest
2.38 - rm *~
2.39 - rm #*
2.40 - rm .#*
2.41 - rm *.tar*
2.42 - cd ../..
2.43 -cd smltest
2.44 - rm *~
2.45 - rm #*
2.46 - rm .#*
2.47 - rm *.tar*
2.48 - cd ../
2.49 -cd smltest/FE-interface
2.50 - rm *~
2.51 - rm #*
2.52 - rm .#*
2.53 - rm *.tar*
2.54 - cd ../..
2.55 -cd smltest/IsacKnowledge
2.56 - rm *~
2.57 - rm #*
2.58 - rm .#*
2.59 - rm *.tar*
2.60 - cd ../..
2.61 -cd smltest/ME
2.62 - rm *~
2.63 - rm #*
2.64 - rm .#*
2.65 - rm *.tar*
2.66 - cd ../..
2.67 -cd smltest/Scripts
2.68 - rm *~
2.69 - rm #*
2.70 - rm .#*
2.71 - rm *.tar*
2.72 - cd ../..
2.73 -cd smltest/xmlsrc
2.74 - rm *~
2.75 - rm #*
2.76 - rm .#*
2.77 - rm *.tar*
2.78 - cd ../..
2.79 -cd sml/systest
2.80 - rm *~
2.81 - rm #*
2.82 - rm .#*
2.83 - rm *.tar*
2.84 - cd ..
3.1 --- a/src/Tools/isac/Isac_Mathengine.thy Tue Aug 17 09:05:51 2010 +0200
3.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Wed Aug 18 13:40:09 2010 +0200
3.3 @@ -9,6 +9,9 @@
3.4 $ cd "/home/neuper/proto2/isac/src/sml"
3.5 $ isabelle-process HOL HOL-Isac
3.6 ML> use_thy "Isac_Mathengine";
3.7 +
3.8 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
3.9 + 10 20 30 40 50 60 70 80
3.10 *)
3.11
3.12 header {* Loading the isac mathengine *}
3.13 @@ -30,9 +33,16 @@
3.14 use_thy"Scripts/Script"
3.15 use "Scripts/scrtools.sml"
3.16
3.17 +ML {*
3.18 +member;
3.19 +@{term 111};
3.20 +*}
3.21 +
3.22 use "ME/mstools.sml"
3.23
3.24
3.25 +
3.26 +
3.27 (*
3.28 use "ME/ctree.sml"
3.29 use "ME/ptyps.sml"
4.1 --- a/src/Tools/isac/ME/calchead.sml Tue Aug 17 09:05:51 2010 +0200
4.2 +++ b/src/Tools/isac/ME/calchead.sml Wed Aug 18 13:40:09 2010 +0200
4.3 @@ -1177,7 +1177,7 @@
4.4 | eq_untouched _ _ = false;
4.5 val ppc' =
4.6 (
4.7 - (*writeln("### insert_ppc: itm= "^(itm2str itm));*)
4.8 + (*writeln("### insert_ppc: itm= "^(itm2str_ itm));*)
4.9 case seek_ppc (#1 itm) ppc of
4.10 (* val Some xxx = seek_ppc (#1 itm) ppc;
4.11 *)
4.12 @@ -1276,7 +1276,7 @@
4.13 (* val Add itm = appl_add thy sel oris pbl ppc ct;
4.14 *)
4.15 let
4.16 - (*val _= writeln("###specify_additem: itm= "^(itm2str itm));*)
4.17 + (*val _= writeln("###specify_additem: itm= "^(itm2str_ itm));*)
4.18 val pbl' = insert_ppc thy itm pbl
4.19 val ((p,Pbl),_,_,pt') =
4.20 generate1 thy (case sel of
4.21 @@ -1507,7 +1507,7 @@
4.22 (* val Add itm = appl_add thy sel oris pbl ppc ct;
4.23 *)
4.24 let
4.25 - (*val _=writeln("###nxt_specif_additem: itm= "^(itm2str itm));*)
4.26 + (*val _=writeln("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
4.27 val pbl' = insert_ppc thy itm pbl
4.28 val (tac,tac_) =
4.29 case sel of
4.30 @@ -1939,8 +1939,8 @@
4.31 (*
4.32 writeln (oris2str pors);
4.33
4.34 - writeln (itms2str thy pits);
4.35 - writeln (itms2str thy mits);
4.36 + writeln (itms2str_ thy pits);
4.37 + writeln (itms2str_ thy mits);
4.38 *)
4.39
4.40
5.1 --- a/src/Tools/isac/ME/ctree.sml Tue Aug 17 09:05:51 2010 +0200
5.2 +++ b/src/Tools/isac/ME/ctree.sml Wed Aug 18 13:40:09 2010 +0200
5.3 @@ -646,7 +646,7 @@
5.4 (*| Match_Problem' (pI, (ok, (itms, pre))) =>
5.5 "Match_Problem' "^(spair2str (strs2str pI,
5.6 spair2str (bool2str ok,
5.7 - spair2str ("itms2str itms",
5.8 + spair2str ("itms2str_ itms",
5.9 "items2str pre"))))*)
5.10 | Add_Given' cterm' => "Add_Given' "(*^cterm'*)
5.11 | Del_Given' cterm' => "Del_Given' "(*^cterm'*)
5.12 @@ -659,7 +659,7 @@
5.13 | Specify_Problem' (pI, (ok, (itms, pre))) =>
5.14 "Specify_Problem' "^(spair2str (strs2str pI,
5.15 spair2str (bool2str ok,
5.16 - spair2str ("itms2str itms",
5.17 + spair2str ("itms2str_ itms",
5.18 "items2str pre"))))
5.19 | Specify_Method' (pI,oris,itms) =>
5.20 "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"
5.21 @@ -1510,7 +1510,7 @@
5.22 (apfst bool2str)))) bts;
5.23 fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) =
5.24 "("^bool2str b^", "^pos_2str p^", "^term2str hdf^
5.25 - ", "^itms2str (assoc_thy "Isac.thy") itms^
5.26 + ", "^itms2str_ (assoc_thy "Isac.thy") itms^
5.27 ", "^preconds2str prec^", \n"^spec2str spec^" )";
5.28
5.29
6.1 --- a/src/Tools/isac/ME/inform.sml Tue Aug 17 09:05:51 2010 +0200
6.2 +++ b/src/Tools/isac/ME/inform.sml Wed Aug 18 13:40:09 2010 +0200
6.3 @@ -252,7 +252,7 @@
6.4 (*this ^ should raise the exn on unability of re-parsing dts*)
6.5 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
6.6 | parsitm dI (itm as (i,v,_,f, Par _)) =
6.7 - raise error ("parsitm ("^itm2str dI itm^
6.8 + raise error ("parsitm ("^itm2str_ dI itm^
6.9 "): Par should be internal");
6.10
6.11 (*separate a list to a pair of elements that do NOT satisfy the predicate,
6.12 @@ -358,7 +358,7 @@
6.13 (#1 (some_spec ospec spec), oris, []:itm list,
6.14 ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
6.15 val iii = appl_adds dI oris ppc pbt (selct::ss);
6.16 - writeln(itms2str thy iii);
6.17 + writeln(itms2str_ thy iii);
6.18
6.19 val itm = appl_add' dI oris ppc pbt selct;
6.20 val ppc = insert_ppc' itm ppc;
6.21 @@ -370,7 +370,7 @@
6.22 val _::selct::ss = (selct::ss);
6.23 val itm = appl_add' dI oris ppc pbt selct;
6.24 val ppc = insert_ppc' itm ppc;
6.25 - writeln(itms2str thy ppc);
6.26 + writeln(itms2str_ thy ppc);
6.27
6.28 val _::selct::ss = (selct::ss);
6.29 val itm = appl_add' dI oris ppc pbt selct;
6.30 @@ -393,7 +393,7 @@
6.31
6.32 fun par2fstr ((_,_,_,f, Par s):itm) = (f, s)
6.33 | par2fstr itm = raise error ("par2fstr: called with "^
6.34 - itm2str (assoc_thy "Isac.thy") itm);
6.35 + itm2str_ (assoc_thy "Isac.thy") itm);
6.36 fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts))
6.37 | itms2fstr (_,_,_,f, Syn str) = (f, str)
6.38 | itms2fstr (_,_,_,f, Typ str) = (f, str)
6.39 @@ -401,7 +401,7 @@
6.40 | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts))
6.41 | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t))
6.42 | itms2fstr (itm as (_,_,_,f, Par _)) =
6.43 - raise error ("parsitm ("^itm2str (assoc_thy "Isac.thy") itm^
6.44 + raise error ("parsitm ("^itm2str_ (assoc_thy "Isac.thy") itm^
6.45 "): Par should be internal");
6.46
6.47 fun imodel2fstr iitems =
7.1 --- a/src/Tools/isac/ME/mstools.sml Tue Aug 17 09:05:51 2010 +0200
7.2 +++ b/src/Tools/isac/ME/mstools.sml Wed Aug 18 13:40:09 2010 +0200
7.3 @@ -7,6 +7,8 @@
7.4
7.5 use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*);
7.6 use"mstools.sml";
7.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
7.8 + 10 20 30 40 50 60 70 80
7.9 *)
7.10
7.11 signature SPECIFY_TOOLS =
7.12 @@ -23,19 +25,19 @@
7.13 | TypeE of string
7.14 val item2str : item -> string
7.15 type itm
7.16 - val itm2str : Theory.theory -> itm -> string
7.17 + val itm2str_ : Proof.context -> itm -> string
7.18 datatype
7.19 itm_ =
7.20 - Cor of (Term.term * Term.term list) * (Term.term * Term.term list)
7.21 - | Inc of (Term.term * Term.term list) * (Term.term * Term.term list)
7.22 - | Mis of Term.term * Term.term
7.23 + Cor of (term * term list) * (term * term list)
7.24 + | Inc of (term * term list) * (term * term list)
7.25 + | Mis of term * term
7.26 | Par of cterm'
7.27 - | Sup of Term.term * Term.term list
7.28 + | Sup of term * term list
7.29 | Syn of cterm'
7.30 | Typ of cterm'
7.31 val itm_2str : itm_ -> string
7.32 - val itm__2str : Theory.theory -> itm_ -> string
7.33 - val itms2str : Theory.theory -> itm list -> string
7.34 + val itm_2str_ : Proof.context -> itm_ -> string
7.35 + val itms2str_ : Proof.context -> itm list -> string
7.36 type 'a ppc
7.37 val ppc2str :
7.38 {Find: string list, With: string list, Given: string list,
7.39 @@ -47,7 +49,7 @@
7.40 val match2str : match -> string
7.41 datatype
7.42 match_ =
7.43 - Match_ of pblID * (itm list * (bool * Term.term) list)
7.44 + Match_ of pblID * (itm list * (bool * term) list)
7.45 | NoMatch_
7.46 val matchs2str : match list -> string
7.47 type ori
7.48 @@ -57,108 +59,107 @@
7.49 val preori2str : preori -> string
7.50 val preoris2str : preori list -> string
7.51 type penv
7.52 - (* val penv2str : Theory.theory -> penv -> string *)
7.53 + (* val penv2str_ : Proof.context -> penv -> string *)
7.54 type vats
7.55 (*----------------------------------------------------------------------*)
7.56 - val all_ts_in : itm_ list -> Term.term list
7.57 + val all_ts_in : itm_ list -> term list
7.58 val check_preconds :
7.59 'a ->
7.60 rls ->
7.61 - Term.term list -> itm list -> (bool * Term.term) list
7.62 + term list -> itm list -> (bool * term) list
7.63 val check_preconds' :
7.64 rls ->
7.65 - Term.term list ->
7.66 - itm list -> 'a -> (bool * Term.term) list
7.67 - (* val chkpre2item : rls -> Term.term -> bool * item *)
7.68 - val pres2str : (bool * Term.term) list -> string
7.69 - (* val evalprecond : rls -> Term.term -> bool * Term.term *)
7.70 + term list ->
7.71 + itm list -> 'a -> (bool * term) list
7.72 + (* val chkpre2item : rls -> term -> bool * item *)
7.73 + val pres2str : (bool * term) list -> string
7.74 + (* val evalprecond : rls -> term -> bool * term *)
7.75 (* val cnt : itm list -> int -> int * int *)
7.76 - val comp_dts : Theory.theory -> Term.term * Term.term list -> Thm.cterm
7.77 - val comp_dts' : Term.term * Term.term list -> Term.term
7.78 - val comp_dts'' : Term.term * Term.term list -> string
7.79 - val comp_ts : Term.term * Term.term list -> Term.term
7.80 - val d_in : itm_ -> Term.term
7.81 + val comp_dts : theory -> term * term list -> term
7.82 + val comp_dts' : term * term list -> term
7.83 + val comp_dts'' : term * term list -> string
7.84 + val comp_ts : term * term list -> term
7.85 + val d_in : itm_ -> term
7.86 val de_item : item -> cterm'
7.87 - val dest_list : Term.term * Term.term list -> Term.term list (* for testing *)
7.88 - val dest_list' : Term.term -> Term.term list
7.89 - val dts2str : Term.term * Term.term list -> string
7.90 + val dest_list : term * term list -> term list (* for testing *)
7.91 + val dest_list' : term -> term list
7.92 + val dts2str : term * term list -> string
7.93 val e_itm : itm
7.94 - (* val e_listBool : Term.term *)
7.95 - (* val e_listReal : Term.term *)
7.96 + (* val e_listBool : term *)
7.97 + (* val e_listReal : term *)
7.98 val e_ori : ori
7.99 val e_ori_ : ori
7.100 val empty_ppc : item ppc
7.101 (* val empty_ppc_ct' : cterm' ppc *)
7.102 - (* val getval : Term.term * Term.term list -> Term.term * Term.term *)
7.103 + (* val getval : term * term list -> term * term *)
7.104 (*val head_precond :
7.105 domID * pblID * 'a ->
7.106 - Term.term Library.option ->
7.107 + term option ->
7.108 rls ->
7.109 - Term.term list ->
7.110 - itm list -> 'b -> Term.term * (bool * Term.term) list*)
7.111 + term list ->
7.112 + itm list -> 'b -> term * (bool * term) list*)
7.113 (* val init_item : string -> item *)
7.114 (* val is_matches : match -> bool *)
7.115 (* val is_matches_ : match_ -> bool *)
7.116 - val is_var : Term.term -> bool
7.117 + val is_var : term -> bool
7.118 (* val item_ppc :
7.119 string ppc -> item ppc *)
7.120 val itemppc2str : item ppc -> string
7.121 - val linefeed : string -> string
7.122 (* val matches_pblID : match -> pblID *)
7.123 val max2 : ('a * int) list -> 'a * int
7.124 val max_vt : itm list -> int
7.125 - val mk_e : itm_ -> (Term.term * Term.term) list
7.126 - val mk_en : int -> itm -> (Term.term * Term.term) list
7.127 - val mk_env : itm list -> (Term.term * Term.term) list
7.128 - val mkval : 'a -> Term.term list -> Term.term
7.129 - val mkval' : Term.term list -> Term.term
7.130 + val mk_e : itm_ -> (term * term) list
7.131 + val mk_en : int -> itm -> (term * term) list
7.132 + val mk_env : itm list -> (term * term) list
7.133 + val mkval : 'a -> term list -> term
7.134 + val mkval' : term list -> term
7.135 (* val pblID_of_match : match -> pblID *)
7.136 - val pbl_ids : Theory.theory -> Term.term -> Term.term -> Term.term list
7.137 - val pbl_ids' : 'a -> Term.term -> Term.term list -> Term.term list
7.138 - (* val pen2str : Theory.theory -> Term.term * Term.term list -> string *)
7.139 - val penvval_in : itm_ -> Term.term list
7.140 + val pbl_ids : Proof.context -> term -> term -> term list
7.141 + val pbl_ids' : 'a -> term -> term list -> term list
7.142 + (* val pen2str : theory -> term * term list -> string *)
7.143 + val penvval_in : itm_ -> term list
7.144 val refined : match list -> pblID
7.145 val refined_ :
7.146 - match_ list -> match_ Library.option
7.147 + match_ list -> match_ option
7.148 (* val refined_IDitms :
7.149 - match list -> match Library.option *)
7.150 - val split_dts : 'a -> Term.term -> Term.term * Term.term list
7.151 - val split_dts' : Term.term * Term.term -> Term.term list
7.152 - (* val take_apart : Term.term -> Term.term list *)
7.153 - (* val take_apart_inv : Term.term list -> Term.term *)
7.154 - val ts_in : itm_ -> Term.term list
7.155 - (* val unique : Term.term *)
7.156 + match list -> match option *)
7.157 + val split_dts : 'a -> term -> term * term list
7.158 + val split_dts' : term * term -> term list
7.159 + (* val take_apart : term -> term list *)
7.160 + (* val take_apart_inv : term list -> term *)
7.161 + val ts_in : itm_ -> term list
7.162 + (* val unique : term *)
7.163 val untouched : itm list -> bool
7.164 val upd :
7.165 - Theory.theory ->
7.166 - (''a * (''b * Term.term list) list) list ->
7.167 - Term.term ->
7.168 - ''b * Term.term -> ''a -> ''a * (''b * Term.term list) list
7.169 + Proof.context ->
7.170 + (''a * (''b * term list) list) list ->
7.171 + term ->
7.172 + ''b * term -> ''a -> ''a * (''b * term list) list
7.173 val upd_envv :
7.174 - Theory.theory ->
7.175 + Proof.context ->
7.176 envv ->
7.177 vats ->
7.178 - Term.term -> Term.term -> Term.term -> envv
7.179 + term -> term -> term -> envv
7.180 val upd_penv :
7.181 - Theory.theory ->
7.182 - (''a * Term.term list) list ->
7.183 - Term.term -> ''a * Term.term -> (''a * Term.term list) list
7.184 + Proof.context ->
7.185 + (''a * term list) list ->
7.186 + term -> ''a * term -> (''a * term list) list
7.187 (* val upds_envv :
7.188 - Theory.theory ->
7.189 + Proof.context ->
7.190 envv ->
7.191 - (vats * Term.term * Term.term * Term.term) list ->
7.192 + (vats * term * term * term) list ->
7.193 envv *)
7.194 val vts_cnt : int list -> itm list -> (int * int) list
7.195 val vts_in : itm list -> int list
7.196 - (* val w_itms2str : Theory.theory -> itm list -> unit *)
7.197 + (* val w_itms2str_ : Proof.context -> itm list -> unit *)
7.198 end
7.199
7.200 (*----------------------------------------------------------*)
7.201 structure SpecifyTools : SPECIFY_TOOLS =
7.202 struct
7.203 (*----------------------------------------------------------*)
7.204 -val e_listReal = (term_of o the o (parse Script.thy)) "[]::(real list)";
7.205 -val e_listBool = (term_of o the o (parse Script.thy)) "[]::(bool list)";
7.206 +val e_listReal = (term_of o the o (parse (theory "Script"))) "[]::(real list)";
7.207 +val e_listBool = (term_of o the o (parse (theory "Script"))) "[]::(bool list)";
7.208
7.209 (*.take list-term apart w.r.t. handling elementwise input.*)
7.210 fun take_apart t =
7.211 @@ -197,18 +198,28 @@
7.212 WN050903 we do NOT know which is from subtheory, description or term;
7.213 typecheck thus may lead to TYPE-error 'unknown constant';
7.214 solution: typecheck with Isac.thy; i.e. arg 'thy' superfluous*)
7.215 -fun comp_dts thy (d,[]) =
7.216 - cterm_of ((sign_of o assoc_thy) "Isac.thy")
7.217 +(*fun comp_dts thy (d,[]) =
7.218 + cterm_of (*(sign_of o assoc_thy) "Isac.thy"*)
7.219 + (theory "Isac")
7.220 (*comp_dts:FIXXME stay with term for efficiency !!!*)
7.221 (if is_reall_dsc d then (d $ e_listReal)
7.222 else if is_booll_dsc d then (d $ e_listBool)
7.223 else d)
7.224 | comp_dts thy (d,ts) =
7.225 - (cterm_of ((sign_of o assoc_thy) "Isac.thy")
7.226 + (cterm_of (*(sign_of o assoc_thy) "Isac.thy"*)
7.227 + (theory "Isac")
7.228 (*comp_dts:FIXXME stay with term for efficiency !!*)
7.229 (d $ (comp_ts (d, ts)))
7.230 handle _ => raise error ("comp_dts: "^(term2str d)^
7.231 - " $ "^(term2str (hd ts))));
7.232 + " $ "^(term2str (hd ts))));*)
7.233 +fun comp_dts thy (d,[]) =
7.234 + (if is_reall_dsc d then (d $ e_listReal)
7.235 + else if is_booll_dsc d then (d $ e_listBool)
7.236 + else d)
7.237 + | comp_dts thy (d,ts) =
7.238 + (d $ (comp_ts (d, ts)))
7.239 + handle _ => raise error ("comp_dts: "^(term2str d)^
7.240 + " $ "^(term2str (hd ts)));
7.241 (*25.8.03*)
7.242 fun comp_dts' (d,[]) =
7.243 if is_reall_dsc d then (d $ e_listReal)
7.244 @@ -365,10 +376,10 @@
7.245 type penv = (term (*err_*)
7.246 * (term list) (*[#0, epsilon] 9.5.03 outcommented*)
7.247 ) list;
7.248 -fun pen2str thy (t, ts) =
7.249 - pair2str(Syntax.string_of_term GOON (sign_of thy) t,
7.250 - (strs2str' o map (Sign.string_of_term (sign_of thy))) ts);
7.251 -fun penv2str thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv;
7.252 +fun pen2str ctxt (t, ts) =
7.253 + pair2str(Syntax.string_of_term ctxt t,
7.254 + (strs2str' o map (Syntax.string_of_term ctxt)) ts);
7.255 +fun penv2str_ thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv;
7.256
7.257 (*
7.258 9.5.03: still unused, but left for eventual future development*)
7.259 @@ -388,7 +399,7 @@
7.260 fun getval (id, values) =
7.261 case values of
7.262 [] => raise error ("penv_value: no values in '"^
7.263 - (Sign.string_of_term (sign_of Tools.thy) id))
7.264 + (Syntax.string_of_term (thy2ctxt "Tools") id))
7.265 | [v] => (id, v)
7.266 | (v1::v2::_) => (case v1 of
7.267 Const ("Script.Arbfix",_) => (id, v2)
7.268 @@ -535,7 +546,7 @@
7.269 | mk_e (Sup _) = []
7.270 | mk_e (Mis _) = [];
7.271 fun mk_en vt ((i,vts,b,f,itm_):itm) =
7.272 - if vt mem vts then mk_e itm_ else [];
7.273 + if member op = vts vt then mk_e itm_ else [];
7.274 (*. extract the environment from an item list;
7.275 takes the variant with most items .*)
7.276 fun mk_env itms =
7.277 @@ -580,25 +591,24 @@
7.278 (*. given the input value (from split_dts)
7.279 make the value in a problem-env according to description-type .*)
7.280 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
7.281 -(*9.5.03 penv-concept postponed *)
7.282 -fun pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v =
7.283 +fun pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v =
7.284 if is_list v
7.285 then [v] (*eg. [r=Arbfix]*)
7.286 else (case v of (*eg. eps=#0*)
7.287 (Const ("op =",_) $ l $ r) => [r,l]
7.288 | _ => raise error ("pbl_ids Tools.nam: no equality "
7.289 - ^(Sign.string_of_term (sign_of thy) v)))
7.290 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v]
7.291 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v]
7.292 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v]
7.293 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v]
7.294 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v]
7.295 - | pbl_ids thy (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v]
7.296 - | pbl_ids thy _ v = raise error ("pbl_ids: not implemented for "
7.297 - ^(Sign.string_of_term (sign_of thy) v));
7.298 + ^(Syntax.string_of_term ctxt v)))
7.299 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v]
7.300 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v]
7.301 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v]
7.302 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v]
7.303 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v]
7.304 + | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v]
7.305 + | pbl_ids ctxt _ v = raise error ("pbl_ids: not implemented for "
7.306 + ^(Syntax.string_of_term ctxt v));
7.307 (*
7.308 val t as t1 $ t2 = str2term "antiDerivativeName M_b";
7.309 -pbl_ids thy t1 t2;
7.310 +pbl_ids ctxt t1 t2;
7.311
7.312 val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
7.313 val (d,argl) = strip_comb t;
7.314 @@ -606,7 +616,7 @@
7.315 dest_list (d,argl);
7.316 val (_ $ v) = t;
7.317 is_list v;
7.318 - pbl_ids thy d v;
7.319 + pbl_ids ctxt d v;
7.320 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
7.321 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
7.322
7.323 @@ -615,13 +625,13 @@
7.324 val vl = Free ("x","RealDef.real") : term
7.325
7.326 val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
7.327 - pbl_ids thy dsc vl;
7.328 + pbl_ids ctxt dsc vl;
7.329 val it = [Free ("x","RealDef.real")] : term list
7.330
7.331 val (dsc,vl) = (split_dts o term_of o the o(parse thy))
7.332 "errorBound (eps=#0)";
7.333 val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_";
7.334 - pbl_ids thy dsc vl;
7.335 + pbl_ids ctxt dsc vl;
7.336 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *)
7.337
7.338 (*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))
7.339 @@ -633,7 +643,7 @@
7.340 | [t] => (case t of (*eg. eps=#0*)
7.341 (Const ("op =",_) $ l $ r) => [r,l]
7.342 | _ => raise error ("pbl_ids' Tools.nam: no equality "
7.343 - ^(Sign.string_of_term (sign_of thy) t)))
7.344 + ^(Syntax.string_of_term (ctxt_Isac"")t)))
7.345 | vs' => vs (*14.9.01: ???TODO *))
7.346 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs
7.347 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs
7.348 @@ -650,11 +660,11 @@
7.349
7.350 (*14.9.01: not used after putting values for penv into itm_
7.351 WN.5.5.03: used in upd .. upd_envv*)
7.352 -fun upd_penv thy penv dsc (id, vl) =
7.353 +fun upd_penv ctxt penv dsc (id, vl) =
7.354 (writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
7.355 writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
7.356 writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
7.357 - overwrite (penv, (id, pbl_ids thy dsc vl))
7.358 + overwrite (penv, (id, pbl_ids ctxt dsc vl))
7.359 );
7.360 (*
7.361 val penv = [];
7.362 @@ -678,8 +688,8 @@
7.363 (*WN.9.5.03: not reconsidered; looks strange !!!*)
7.364 fun upd thy envv dsc (id, vl) i =
7.365 let val penv = case assoc (envv, i) of
7.366 - Some e => e
7.367 - | None => [];
7.368 + SOME e => e
7.369 + | NONE => [];
7.370 val penv' = upd_penv thy penv dsc (id, vl);
7.371 in (i, penv') end;
7.372 (*
7.373 @@ -699,7 +709,7 @@
7.374 if length envv = 0 then [1]
7.375 else (intsto o length) envv
7.376 else vats
7.377 - fun isin vats (i,_) = i mem vats;
7.378 + fun isin vats (i,_) = member op = vats i;
7.379 val envs_notin_vat = filter_out (isin vats) envv;
7.380 in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end;
7.381 (*
7.382 @@ -777,32 +787,34 @@
7.383 | Incompl of cterm' (**)
7.384 | Superfl of string (**)
7.385 | Missing of cterm';
7.386 -fun item2str (Correct s) ="Correct "^s
7.387 - | item2str (SyntaxE s) ="SyntaxE "^s
7.388 - | item2str (TypeE s) ="TypeE "^s
7.389 - | item2str (False s) ="False "^s
7.390 - | item2str (Incompl s) ="Incompl "^s
7.391 - | item2str (Superfl s) ="Superfl "^s
7.392 - | item2str (Missing s) ="Missing "^s;
7.393 +fun item2str (Correct s) ="Correct " ^ s
7.394 + | item2str (SyntaxE s) ="SyntaxE " ^ s
7.395 + | item2str (TypeE s) ="TypeE " ^ s
7.396 + | item2str (False s) ="False " ^ s
7.397 + | item2str (Incompl s) ="Incompl " ^ s
7.398 + | item2str (Superfl s) ="Superfl " ^ s
7.399 + | item2str (Missing s) ="Missing " ^ s;
7.400 (*make string for error-msgs*)
7.401 -fun itm__2str thy (Cor ((d,ts), penv)) =
7.402 - "Cor " ^ string_of_cterm (comp_dts thy(d,ts)) ^" ,"^ pen2str thy penv
7.403 - | itm__2str thy (Syn c) = "Syn "^c
7.404 - | itm__2str thy (Typ c) = "Typ "^c
7.405 - | itm__2str thy (Inc ((d,ts), penv)) =
7.406 - "Inc " ^ string_of_cterm (comp_dts thy(d,ts)) ^" ,"^ pen2str thy penv
7.407 - | itm__2str thy (Sup (d,ts)) = "Sup "^(string_of_cterm (comp_dts thy(d,ts)))
7.408 - | itm__2str thy (Mis (d,pid))=
7.409 - "Mis "^ Sign.string_of_term (sign_of thy) d ^
7.410 - " "^ Sign.string_of_term (sign_of thy) pid
7.411 - | itm__2str thy (Par s) = "Trm "^s;
7.412 -fun itm_2str t = itm__2str (assoc_thy "Isac.thy") t;
7.413 -fun itm2str thy ((i,is,b,s,itm_):itm) =
7.414 +fun itm_2str_ ctxt (Cor ((d,ts), penv)) =
7.415 + "Cor " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ,"
7.416 + ^ pen2str ctxt penv
7.417 + | itm_2str_ ctxt (Syn c) = "Syn " ^ c
7.418 + | itm_2str_ ctxt (Typ c) = "Typ " ^ c
7.419 + | itm_2str_ ctxt (Inc ((d,ts), penv)) =
7.420 + "Inc " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ,"
7.421 + ^ pen2str ctxt penv
7.422 + | itm_2str_ ctxt (Sup (d,ts)) =
7.423 + "Sup " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts))
7.424 + | itm_2str_ ctxt (Mis (d,pid))=
7.425 + "Mis "^ Syntax.string_of_term ctxt d ^
7.426 + " "^ Syntax.string_of_term ctxt pid
7.427 + | itm_2str_ ctxt (Par s) = "Trm "^s;
7.428 +fun itm_2str t = itm_2str_ (thy2ctxt "Isac") t;
7.429 +fun itm2str_ ctxt ((i,is,b,s,itm_):itm) =
7.430 "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^
7.431 - s^" ,"^(itm__2str thy itm_)^")";
7.432 -val linefeed = (curry op^) "\n";
7.433 -fun itms2str thy itms = strs2str' (map (linefeed o (itm2str thy)) itms);
7.434 -fun w_itms2str thy itms = writeln (itms2str thy itms);
7.435 + s^" ,"^(itm_2str_ ctxt itm_)^")";
7.436 +fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
7.437 +fun w_itms2str_ ctxt itms = writeln (itms2str_ ctxt itms);
7.438
7.439 fun init_item str = SyntaxE str;
7.440
7.441 @@ -896,7 +908,7 @@
7.442 | ts_in (Mis _) = [];
7.443 (*WN050629 unused*)
7.444 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
7.445 -val unique = (term_of o the o (parse Real.thy)) "UnIqE_tErM";
7.446 +val unique = (term_of o the o (parse (theory "Real"))) "UnIqE_tErM";
7.447 fun d_in (Cor ((d,_),_)) = d
7.448 | d_in (Syn (c)) = (writeln("*** d_in: Syn ("^c^")"); unique)
7.449 | d_in (Typ (c)) = (writeln("*** d_in: Typ ("^c^")"); unique)
7.450 @@ -918,10 +930,10 @@
7.451 rls -> (*for eval_true*)
7.452 bool * (*have _all_ variables(Free) from the model-pattern
7.453 been substituted by a value from the pattern's environment ?*)
7.454 -Term.term (*the precondition*)
7.455 +term (*the precondition*)
7.456 ->
7.457 bool * (*has the precondition evaluated to true*)
7.458 -Term.term (*the precondition (for map)*)
7.459 +term (*the precondition (for map)*)
7.460 .*)
7.461 fun evalprecond prls (false, pre) =
7.462 (*NOT ALL Free's have been substituted, eg. because of incomplete model*)
7.463 @@ -969,9 +981,9 @@
7.464 fun cpy its [] (f, (d, id)) =
7.465 if length its = 0 (*no dsc found in pbl*)
7.466 then case find_first (vt_and_dsc d) oris
7.467 - of Some (i,v,_,_,ts) =>
7.468 + of SOME (i,v,_,_,ts) =>
7.469 [(i,v,true,f, Cor ((d,ts), (id,pbl_ids' thy d ts)))]
7.470 - | None => [(0,[],false,f,Mis (d, id))]
7.471 + | NONE => [(0,[],false,f,Mis (d, id))]
7.472 else its
7.473 | cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =
7.474 if d = d_in itm_ andalso i<>0 (*already touched by user*)
7.475 @@ -1018,7 +1030,7 @@
7.476 fun copy_pbl (pbl:itm list) met oris =
7.477 let fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;
7.478 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
7.479 - Some _ => false | None => true;
7.480 + SOME _ => false | NONE => true;
7.481 (*1*)val mis = ((map (cons2 (fst, fst o snd))) o (filter (notmem pbl))) met;
7.482
7.483 fun eqdsc_ori d ((_,_,_,d',_):ori) = d = d';
8.1 --- a/src/Tools/isac/Scripts/term_G.sml Tue Aug 17 09:05:51 2010 +0200
8.2 +++ b/src/Tools/isac/Scripts/term_G.sml Wed Aug 18 13:40:09 2010 +0200
8.3 @@ -295,8 +295,8 @@
8.4 fun mk_prop t = Trueprop $ t;
8.5 val true_as_term = Const("True",bool);
8.6 val false_as_term = Const("False",bool);
8.7 -val true_as_cterm = cterm_of HOL true_as_term;
8.8 -val false_as_cterm = cterm_of HOL false_as_term;
8.9 +val true_as_cterm = cterm_of (theory "HOL") true_as_term;
8.10 +val false_as_cterm = cterm_of (theory "HOL") false_as_term;
8.11
8.12 infixr 5 -->; (*2002 /Pure/term.ML *)
8.13 infixr --->; (*2002 /Pure/term.ML *)
8.14 @@ -1255,11 +1255,10 @@
8.15 *** Free ( R, RealDef.real) *)
8.16
8.17 (*version for testing local to theories*)
8.18 -fun str2t thy str = (term_of o the o (parse thy )) str;
8.19 -
8.20 -fun str2term str = (term_of o the o (parse (assoc_thy "Isac.thy"))) str;
8.21 -fun str2termN str = (term_of o the o (parseN (assoc_thy "Isac.thy"))) str;
8.22 +fun str2term_ thy str = (term_of o the o (parse thy)) str;
8.23 +fun str2term str = (term_of o the o (parse (theory "Isac"))) str;
8.24 fun strs2terms ss = map str2term ss;
8.25 +fun str2termN str = (term_of o the o (parseN (theory "Isac"))) str;
8.26
8.27 (*+ makes a substitution from the output of Pattern.match +*)
8.28 (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*)
9.1 --- a/src/Tools/isac/calcelems.sml Tue Aug 17 09:05:51 2010 +0200
9.2 +++ b/src/Tools/isac/calcelems.sml Wed Aug 18 13:40:09 2010 +0200
9.3 @@ -131,12 +131,13 @@
9.4 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
9.5 from rls, and then contain both Script _AND_ Rfuns !!!*)
9.6
9.7 +fun thy2ctxt thy' = ProofContext.init_global (theory thy'); (*FIXXXME thy-ctxt*)
9.8
9.9 (*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
9.10 -val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");
9.11 -val HOL = ProofContext.theory_of ctxt_HOL;
9.12 +(*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*)
9.13 +val ctxt_HOL = thy2ctxt "Complex_Main";
9.14 (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
9.15 -fun ctxt_Isac _ = ProofContext.init_global (theory "Isac");
9.16 +fun ctxt_Isac _ = thy2ctxt "Isac";
9.17 fun Isac _ = ProofContext.theory_of (ctxt_Isac"");
9.18
9.19 val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" );
10.1 --- a/test/Tools/isac/IsacKnowledge/atools.sml Tue Aug 17 09:05:51 2010 +0200
10.2 +++ b/test/Tools/isac/IsacKnowledge/atools.sml Wed Aug 18 13:40:09 2010 +0200
10.3 @@ -23,9 +23,9 @@
10.4 "----------- occurs_in -------------------------------------------";
10.5 "----------- occurs_in -------------------------------------------";
10.6 "----------- occurs_in -------------------------------------------";
10.7 -fun str2t str = (term_of o the o (parse thy )) str;
10.8 +fun str2term str = (term_of o the o (parse thy )) str;
10.9 fun term2s t = Sign.string_of_term (sign_of thy) t;
10.10 -val t = str2t "x";
10.11 +val t = str2term "x";
10.12 if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f";
10.13
10.14 val t = str2term "x occurs_in x";
10.15 @@ -53,7 +53,7 @@
10.16 "----------- argument_of -----------------------------------------";
10.17 "----------- argument_of -----------------------------------------";
10.18 "----------- argument_of -----------------------------------------";
10.19 -val t = str2t "argument_in (M_b x)";
10.20 +val t = str2term "argument_in (M_b x)";
10.21 val Some (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;
10.22 if term2s t' = "(argument_in M_b x) = x" then ()
10.23 else raise error "atools.sml:(argument_in M_b x) = x ???";
11.1 --- a/test/Tools/isac/IsacKnowledge/biegelinie.sml Tue Aug 17 09:05:51 2010 +0200
11.2 +++ b/test/Tools/isac/IsacKnowledge/biegelinie.sml Wed Aug 18 13:40:09 2010 +0200
11.3 @@ -30,20 +30,20 @@
11.4 "----------- the rules -------------------------------------------";
11.5 "----------- the rules -------------------------------------------";
11.6 "----------- the rules -------------------------------------------";
11.7 -fun str2t str = (term_of o the o (parse Biegelinie.thy)) str;
11.8 +fun str2term str = (term_of o the o (parse Biegelinie.thy)) str;
11.9 fun term2s t = Sign.string_of_term (sign_of Biegelinie.thy) t;
11.10 fun rewrit thm str =
11.11 fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));
11.12
11.13 -val t = rewrit Belastung_Querkraft (str2t "- q_ x = - q_0"); term2s t;
11.14 +val t = rewrit Belastung_Querkraft (str2term "- q_ x = - q_0"); term2s t;
11.15 if term2s t = "Q' x = - q_0" then ()
11.16 else raise error "/biegelinie.sml: Belastung_Querkraft";
11.17
11.18 -val t = rewrit Querkraft_Moment (str2t "Q x = - q_0 * x + c"); term2s t;
11.19 +val t = rewrit Querkraft_Moment (str2term "Q x = - q_0 * x + c"); term2s t;
11.20 if term2s t = "M_b' x = - q_0 * x + c" then ()
11.21 else raise error "/biegelinie.sml: Querkraft_Moment";
11.22
11.23 -val t = rewrit Moment_Neigung (str2t "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
11.24 +val t = rewrit Moment_Neigung (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
11.25 term2s t;
11.26 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
11.27 else raise error "biegelinie.sml: Moment_Neigung";
11.28 @@ -125,7 +125,7 @@
11.29 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
11.30 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
11.31 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
11.32 -val t = str2t "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
11.33 +val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
11.34 val t = rewrit Moment_Neigung t; term2s t;
11.35 (*was "EI * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
11.36 ### before declaring "y''" as a constant *)
11.37 @@ -191,18 +191,18 @@
11.38 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.39 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.40
11.41 -val pits = get_obj g_pbl pt (fst p);writeln (itms2str thy pits);
11.42 -(*if itms2str thy pits = ... all 5 model-items*)
11.43 -val mits = get_obj g_met pt (fst p); writeln (itms2str thy mits);
11.44 -if itms2str thy mits = "[]" then ()
11.45 +val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
11.46 +(*if itms2str_ ctxt pits = ... all 5 model-items*)
11.47 +val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
11.48 +if itms2str_ ctxt mits = "[]" then ()
11.49 else raise error "biegelinie.sml: Bsp 7.27 #2";
11.50
11.51 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.52 case nxt of (_,Add_Given "FunktionsVariable x") => ()
11.53 | _ => raise error "biegelinie.sml: Bsp 7.27 #4a";
11.54 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.55 -val mits = get_obj g_met pt (fst p);writeln (itms2str thy mits);
11.56 -(*if itms2str thy mits = ... all 6 guard-items*)
11.57 +val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
11.58 +(*if itms2str_ ctxt mits = ... all 6 guard-items*)
11.59 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
11.60 | _ => raise error "biegelinie.sml: Bsp 7.27 #4b";
11.61
12.1 --- a/test/Tools/isac/IsacKnowledge/diffapp.sml Tue Aug 17 09:05:51 2010 +0200
12.2 +++ b/test/Tools/isac/IsacKnowledge/diffapp.sml Wed Aug 18 13:40:09 2010 +0200
12.3 @@ -283,10 +283,10 @@
12.4 | _ => raise error "diffapp.sml: max-exp me, nxt = Specify_Method";
12.5
12.6 val oris = fst3 (get_obj g_origin pt (fst p)); writeln(oris2str oris);
12.7 -val pits = get_obj g_pbl pt (fst p); writeln(itms2str thy pits);
12.8 +val pits = get_obj g_pbl pt (fst p); writeln(itms2str_ ctxt pits);
12.9
12.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.11 -val mits = get_obj g_met pt (fst p); writeln(itms2str thy mits);
12.12 +val mits = get_obj g_met pt (fst p); writeln(itms2str_ ctxt mits);
12.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.15 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.16 @@ -311,7 +311,7 @@
12.17 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.18
12.19 val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
12.20 -val pits = get_obj g_pbl pt (fst p);writeln(itms2str thy pits);
12.21 +val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
12.22
12.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.25 @@ -344,7 +344,7 @@
12.26 (*val nxt = Refine_Tacitly ["univariate","equation"])*)
12.27
12.28 val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
12.29 -val pits = get_obj g_pbl pt (fst p);writeln(itms2str thy pits);
12.30 +val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
12.31
12.32 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.33 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.34 @@ -377,11 +377,11 @@
12.35
12.36 val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
12.37
12.38 -val pits = get_obj g_pbl pt (fst p);writeln(itms2str thy pits);
12.39 -val pits = get_obj g_pbl pt [];writeln(itms2str thy pits);
12.40 +val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
12.41 +val pits = get_obj g_pbl pt [];writeln(itms2str_ ctxt pits);
12.42
12.43 -val mits = get_obj g_met pt (fst p);writeln(itms2str thy mits);
12.44 -val mits = get_obj g_met pt [];writeln(itms2str thy mits);
12.45 +val mits = get_obj g_met pt (fst p);writeln(itms2str_ ctxt mits);
12.46 +val mits = get_obj g_met pt [];writeln(itms2str_ ctxt mits);
12.47
12.48 itms2args thy ["DiffApp","max_by_calculus"] mits;
12.49
12.50 @@ -426,14 +426,14 @@
12.51 fetchProposedTactic 1;
12.52 val ((pt,p),_) = get_calc 1;
12.53 val mits = get_obj g_met pt (fst p);
12.54 - writeln (itms2str thy mits);
12.55 + writeln (itms2str_ ctxt mits);
12.56 (*
12.57 - 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 ()
12.58 + 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 ()
12.59 else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
12.60 *)
12.61 (*FIXME: the environments contain identifers, and NOT values ?!?!?*)
12.62 (* WN051209 while extending 'fun step' for initac, this became better ...
12.63 - 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 ()
12.64 + 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 ()
12.65 else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
12.66 *)
12.67
13.1 --- a/test/Tools/isac/IsacKnowledge/eqsystem.sml Tue Aug 17 09:05:51 2010 +0200
13.2 +++ b/test/Tools/isac/IsacKnowledge/eqsystem.sml Wed Aug 18 13:40:09 2010 +0200
13.3 @@ -813,7 +813,7 @@
13.4
13.5
13.6 -----fun refin' ff:
13.7 -> (writeln o (itms2str Isac.thy)) itms;
13.8 +> (writeln o (itms2str_ (thy2ctxt "Isac"))) itms;
13.9 [
13.10 (1 ,[1] ,true ,#Given ,Cor equalities
13.11 [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
13.12 @@ -828,7 +828,7 @@
13.13 (true, length_ [c, c_2] = 2)]
13.14
13.15 ----- fun match_oris':
13.16 -> (writeln o (itms2str Isac.thy)) itms;
13.17 +> (writeln o (itms2str_ (thy2ctxt "Isac"))) itms;
13.18 > (writeln o pres2str) pre';
13.19 ..as in refin'
13.20
13.21 @@ -895,7 +895,8 @@
13.22 | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
13.23
13.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.25 -val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl;
13.26 +val PblObj {probl,...} = get_obj I pt [5];
13.27 + (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
13.28 (*[
13.29 (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]])),
13.30 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
13.31 @@ -963,7 +964,8 @@
13.32 | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
13.33
13.34 val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.35 -val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl;
13.36 +val PblObj {probl,...} = get_obj I pt [5];
13.37 + (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
13.38 (*[
13.39 (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]])),
13.40 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
14.1 --- a/test/Tools/isac/IsacKnowledge/integrate.sml Tue Aug 17 09:05:51 2010 +0200
14.2 +++ b/test/Tools/isac/IsacKnowledge/integrate.sml Wed Aug 18 13:40:09 2010 +0200
14.3 @@ -36,14 +36,14 @@
14.4 "----------- parsing ---------------------------------------------";
14.5 "----------- parsing ---------------------------------------------";
14.6 "----------- parsing ---------------------------------------------";
14.7 -fun str2t str = (term_of o the o (parse Integrate.thy)) str;
14.8 +fun str2term str = (term_of o the o (parse Integrate.thy)) str;
14.9 fun term2s t = Sign.string_of_term (sign_of Integrate.thy) t;
14.10
14.11 -val t = str2t "Integral x D x";
14.12 -val t = str2t "Integral x^^^2 D x";
14.13 +val t = str2term "Integral x D x";
14.14 +val t = str2term "Integral x^^^2 D x";
14.15 atomty t;
14.16
14.17 -val t = str2t "ff x is_f_x";
14.18 +val t = str2term "ff x is_f_x";
14.19 case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
14.20 | _ => raise error "integrate.sml: parsing: ff x is_f_x";
14.21
14.22 @@ -64,27 +64,27 @@
14.23 Thm ("not_false",not_false)
14.24 ],
14.25 scr = EmptyScr};
14.26 -val subs = [(str2t "bdv", str2t "x")];
14.27 +val subs = [(str2term "bdv", str2term "x")];
14.28 fun rewrit thm str =
14.29 fst (the (rewrite_inst_ Integrate.thy tless_true
14.30 conditions_in_integration_rules
14.31 true subs thm str));
14.32 -val str = rewrit integral_const (str2t "Integral 1 D x"); term2s str;
14.33 -val str = rewrit integral_const (str2t "Integral M'/EJ D x"); term2s str;
14.34 -val str = (rewrit integral_const (str2t "Integral x D x"))
14.35 - handle OPTION => str2t "no_rewrite";
14.36 +val str = rewrit integral_const (str2term "Integral 1 D x"); term2s str;
14.37 +val str = rewrit integral_const (str2term "Integral M'/EJ D x"); term2s str;
14.38 +val str = (rewrit integral_const (str2term "Integral x D x"))
14.39 + handle OPTION => str2term "no_rewrite";
14.40
14.41 -val str = rewrit integral_var (str2t "Integral x D x"); term2s str;
14.42 -val str = (rewrit integral_var (str2t "Integral a D x"))
14.43 - handle OPTION => str2t "no_rewrite";
14.44 +val str = rewrit integral_var (str2term "Integral x D x"); term2s str;
14.45 +val str = (rewrit integral_var (str2term "Integral a D x"))
14.46 + handle OPTION => str2term "no_rewrite";
14.47
14.48 -val str = rewrit integral_add (str2t "Integral x + 1 D x"); term2s str;
14.49 +val str = rewrit integral_add (str2term "Integral x + 1 D x"); term2s str;
14.50
14.51 -val str = rewrit integral_mult (str2t "Integral M'/EJ * x^^^3 D x");term2s str;
14.52 -val str = (rewrit integral_mult (str2t "Integral x * x D x"))
14.53 - handle OPTION => str2t "no_rewrite";
14.54 +val str = rewrit integral_mult (str2term "Integral M'/EJ * x^^^3 D x");term2s str;
14.55 +val str = (rewrit integral_mult (str2term "Integral x * x D x"))
14.56 + handle OPTION => str2term "no_rewrite";
14.57
14.58 -val str = rewrit integral_pow (str2t "Integral x^^^3 D x"); term2s str;
14.59 +val str = rewrit integral_pow (str2term "Integral x^^^3 D x"); term2s str;
14.60
14.61
14.62 "----------- test add_new_c, is_f_x ------------------------------";
14.63 @@ -112,27 +112,27 @@
14.64
14.65
14.66 (*WN080222 replace call_new_c with add_new_c----------------------
14.67 -val term = str2t "new_c (c * x^^^2 + c_2)";
14.68 +val term = str2term "new_c (c * x^^^2 + c_2)";
14.69 val Some (_,t') = eval_new_c 0 0 term 0;
14.70 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
14.71 else raise error "integrate.sml: eval_new_c ???";
14.72
14.73 -val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
14.74 +val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
14.75 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
14.76 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
14.77 else raise error "integrate.sml: matches new_c = False";
14.78
14.79 -val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
14.80 +val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
14.81 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
14.82 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
14.83 then () else raise error "integrate.sml: matches new_c = True";
14.84
14.85 -val t = str2t "ff x is_f_x";
14.86 +val t = str2term "ff x is_f_x";
14.87 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t';
14.88 if term2s t' = "(ff x is_f_x) = True" then ()
14.89 else raise error "integrate.sml: eval_is_f_x --> true";
14.90
14.91 -val t = str2t "q_0/2 * L * x is_f_x";
14.92 +val t = str2term "q_0/2 * L * x is_f_x";
14.93 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t';
14.94 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()
14.95 else raise error "integrate.sml: eval_is_f_x --> false";
14.96 @@ -153,15 +153,15 @@
14.97 fun rewrit thm t =
14.98 fst (the (rewrite_inst_ Integrate.thy tless_true
14.99 conditions_in_integration true subs thm t));
14.100 -val t = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s t;
14.101 +val t = rewrit call_for_new_c (str2term "x ^^^ 2 / 2"); term2s t;
14.102 val t = (rewrit call_for_new_c t)
14.103 - handle OPTION => str2t "no_rewrite";
14.104 + handle OPTION => str2term "no_rewrite";
14.105
14.106 val t = rewrit call_for_new_c
14.107 - (str2t "ff x = q_0/2 *L*x"); term2s t;
14.108 + (str2term "ff x = q_0/2 *L*x"); term2s t;
14.109 val t = (rewrit call_for_new_c
14.110 - (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
14.111 - handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite";
14.112 + (str2term "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
14.113 + handle OPTION => (*NOT: + new_c ..=..!!*)str2term "no_rewrite";
14.114 --------------------------------------------------------------------*)
14.115
14.116
14.117 @@ -347,7 +347,7 @@
14.118 if F1_ = F2_ then () else raise error "integrate.sml: unequal find's";
14.119
14.120 val ((dsc as Const ("Integrate.antiDerivativeName", _))
14.121 - $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";
14.122 + $ Free ("ff", F3_type)) = str2term "antiDerivativeName ff";
14.123 if is_dsc dsc then () else raise error "integrate.sml: no description";
14.124 if F1_type = F3_type then ()
14.125 else raise error "integrate.sml: unequal types in find's";
15.1 --- a/test/Tools/isac/IsacKnowledge/poly.sml Tue Aug 17 09:05:51 2010 +0200
15.2 +++ b/test/Tools/isac/IsacKnowledge/poly.sml Wed Aug 18 13:40:09 2010 +0200
15.3 @@ -356,7 +356,7 @@
15.4 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
15.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.7 -(writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
15.8 +(writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
15.9 val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.1 --- a/test/Tools/isac/ME/calchead.sml Tue Aug 17 09:05:51 2010 +0200
16.2 +++ b/test/Tools/isac/ME/calchead.sml Wed Aug 18 13:40:09 2010 +0200
16.3 @@ -210,7 +210,7 @@
16.4
16.5 (*val nxt = Specify_Theory "DiffApp.thy" : tac*)
16.6
16.7 -val itms = get_obj g_pbl pt (fst p);writeln(itms2str thy itms);
16.8 +val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
16.9
16.10 val nxt = tac2tac_ pt p nxt;
16.11 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
17.1 --- a/test/Tools/isac/ME/ctree.sml Tue Aug 17 09:05:51 2010 +0200
17.2 +++ b/test/Tools/isac/ME/ctree.sml Wed Aug 18 13:40:09 2010 +0200
17.3 @@ -72,13 +72,13 @@
17.4 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
17.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.6 (* nxt = Add_Given "equality (x + 1 = 2)"
17.7 - (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
17.8 + (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
17.9 *)
17.10 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.11 -(* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
17.12 +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
17.13 *)
17.14 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.15 -(* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
17.16 +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
17.17 *)
17.18 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.19 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.20 @@ -421,13 +421,13 @@
17.21 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
17.22 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.23 (* nxt = Add_Given "equality (x + 1 = 2)"
17.24 - (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
17.25 + (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
17.26 *)
17.27 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.28 -(* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
17.29 +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
17.30 *)
17.31 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.32 -(* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
17.33 +(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
17.34 *)
17.35 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.36 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
18.1 --- a/test/Tools/isac/ME/inform.sml Tue Aug 17 09:05:51 2010 +0200
18.2 +++ b/test/Tools/isac/ME/inform.sml Wed Aug 18 13:40:09 2010 +0200
18.3 @@ -371,11 +371,11 @@
18.4 (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)
18.5 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];
18.6 (*val nxt = ("Model_Problem", ...*)
18.7 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
18.8 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.9
18.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.11 (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
18.12 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
18.13 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.14 (*[
18.15 (0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),
18.16 (0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),
18.17 @@ -384,7 +384,7 @@
18.18
18.19 (*the empty CalcHead is checked w.r.t the model and re-established as such*)
18.20 val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);
18.21 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
18.22 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.23 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";
18.24
18.25 (*there is one input to the model (could be more)*)
18.26 @@ -392,7 +392,7 @@
18.27 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
18.28 Find ["maximum", "valuesFor"],
18.29 Relate ["relations"]], Pbl, e_spec);
18.30 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
18.31 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.32 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 ()
18.33 else raise error "informtest.sml: diff.behav. max 2";
18.34
18.35 @@ -402,7 +402,7 @@
18.36 Find ["maximum A", "valuesFor [a,b]"],
18.37 Relate ["relations [A=a*b, a/2=r*sin alpha, \
18.38 \b/2=r*cos alpha]"]], Pbl, e_spec);
18.39 - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl;
18.40 + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.41 if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)
18.42
18.43 (*this input is complete in variant 1 (variant 3 does not work yet)*)
18.44 @@ -412,7 +412,7 @@
18.45 Relate ["relations [A=a*b, \
18.46 \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
18.47 Pbl, e_spec);
18.48 - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl;
18.49 + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.50
18.51 modifycalcheadOK2xml 111 (bool2str b) ocalhd;
18.52 *)
18.53 @@ -522,8 +522,8 @@
18.54 print_depth 5;
18.55 writeln"-----------------------------------------------------------";
18.56 spec;
18.57 -writeln (itms2str thy probl);
18.58 -writeln (itms2str thy meth);
18.59 +writeln (itms2str_ ctxt probl);
18.60 +writeln (itms2str_ ctxt meth);
18.61 writeln (istate2str istate);
18.62
18.63 print_depth 3;
18.64 @@ -547,12 +547,12 @@
18.65 (*("Isac.thy",
18.66 ["derivative_of", "function"],
18.67 ["diff", "differentiate_on_R"]) : spec*)
18.68 -writeln (itms2str thy probl);
18.69 +writeln (itms2str_ ctxt probl);
18.70 (*[
18.71 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
18.72 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
18.73 (3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
18.74 -writeln (itms2str thy meth);
18.75 +writeln (itms2str_ ctxt meth);
18.76 (*[
18.77 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
18.78 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
18.79 @@ -592,12 +592,12 @@
18.80 (*("Isac.thy",
18.81 ["derivative_of", "function"],
18.82 ["diff", "differentiate_on_R"]) : spec*)
18.83 -writeln (itms2str thy probl);
18.84 +writeln (itms2str_ ctxt probl);
18.85 (*[
18.86 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
18.87 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
18.88 (3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
18.89 -writeln (itms2str thy meth);
18.90 +writeln (itms2str_ ctxt meth);
18.91 (*[
18.92 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
18.93 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
19.1 --- a/test/Tools/isac/ME/me.sml Tue Aug 17 09:05:51 2010 +0200
19.2 +++ b/test/Tools/isac/ME/me.sml Wed Aug 18 13:40:09 2010 +0200
19.3 @@ -344,23 +344,23 @@
19.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.6 (*xt = Add_Given "solveFor x"*)
19.7 - writeln (itms2str thy (get_obj g_pbl pt (fst p)));
19.8 + writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));
19.9 (*[
19.10 (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),
19.11 (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),
19.12 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)
19.13 val (pt,p) = complete_mod (pt, p);
19.14 - 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 ()
19.15 + 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 ()
19.16 else raise error "completetest.sml: new behav. in complete_mod 1";
19.17 - writeln (itms2str thy (get_obj g_pbl pt (fst p)));
19.18 + writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));
19.19 (*[
19.20 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
19.21 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
19.22 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
19.23 val mits = get_obj g_met pt (fst p);
19.24 - 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]))]"
19.25 + 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]))]"
19.26 then () else raise error "completetest.sml: new behav. in complete_mod 2";
19.27 - writeln (itms2str thy mits);
19.28 + writeln (itms2str_ ctxt mits);
19.29 (*[
19.30 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
19.31 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
19.32 @@ -446,7 +446,7 @@
19.33 (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
19.34 (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)
19.35 val pits = get_obj g_pbl pt (fst p);
19.36 - writeln (itms2str thy pits);
19.37 + writeln (itms2str_ ctxt pits);
19.38 (*[
19.39 (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
19.40 (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
19.41 @@ -456,7 +456,7 @@
19.42 val mits = get_obj g_met pt (fst p);
19.43 val mits = complete_metitms oris pits []
19.44 ((#ppc o get_met) ["DiffApp","max_by_calculus"]);
19.45 - writeln (itms2str thy mits);
19.46 + writeln (itms2str_ ctxt mits);
19.47 (*[
19.48 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
19.49 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
19.50 @@ -467,7 +467,7 @@
19.51 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
19.52 0 <= x & x <= 2 * r}])),
19.53 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
19.54 - 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 ()
19.55 + 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 ()
19.56 else raise error "completetest.sml: new behav. in complete_metitms 1";
19.57
19.58
19.59 @@ -494,7 +494,7 @@
19.60 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.61 (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
19.62 val pits = get_obj g_pbl pt (fst p);
19.63 - writeln (itms2str thy pits);
19.64 + writeln (itms2str_ ctxt pits);
19.65 (*[
19.66 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
19.67 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
19.68 @@ -502,9 +502,9 @@
19.69 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
19.70 val (pt,p) = complete_mod (pt,p);
19.71 val pits = get_obj g_pbl pt (fst p);
19.72 - 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]]))]"
19.73 + 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]]))]"
19.74 then () else raise error "completetest.sml: new behav. in complete_mod 3";
19.75 - writeln (itms2str thy pits);
19.76 + writeln (itms2str_ ctxt pits);
19.77 (*[
19.78 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
19.79 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
19.80 @@ -512,9 +512,9 @@
19.81 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
19.82 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
19.83 val mits = get_obj g_met pt (fst p);
19.84 - 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]))]"
19.85 + 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]))]"
19.86 then () else raise error "completetest.sml: new behav. in complete_mod 3";
19.87 - writeln (itms2str thy mits);
19.88 + writeln (itms2str_ ctxt mits);
19.89 (*[
19.90 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
19.91 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),