1.1 --- a/src/Tools/isac/Build_Isac.thy Thu Sep 23 14:49:23 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Sep 23 16:38:25 2010 +0200
1.3 @@ -16,8 +16,8 @@
1.4 begin
1.5
1.6 ML {*
1.7 -writeln "**** build the isac kernel = math-engine + Knowledge ***********";
1.8 -writeln "**** build the math-engine *************************************" *}
1.9 +tracing "**** build the isac kernel = math-engine + Knowledge ***********";
1.10 +tracing "**** build the math-engine *************************************" *}
1.11
1.12 ML {* Toplevel.debug := true; *}
1.13 use "library.sml"
1.14 @@ -54,9 +54,9 @@
1.15 use "Frontend/interface.sml"
1.16
1.17 use "print_exn_G.sml"
1.18 -ML {* writeln "**** build math-engine complete **************************" *}
1.19 +ML {* tracing "**** build math-engine complete **************************" *}
1.20
1.21 -ML {* writeln "**** build the Knowledge *********************************" *}
1.22 +ML {* tracing "**** build the Knowledge *********************************" *}
1.23 (*use_thy "Knowledge/Delete"
1.24 use_thy "Knowledge/Descript"
1.25 use_thy "Knowledge/Atools"
1.26 @@ -86,7 +86,7 @@
1.27 use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*)
1.28 use_thy "Knowledge/Isac"
1.29 ML {* check_guhs_unique := false; *}
1.30 -ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *}
1.31 +ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *}
1.32
1.33
1.34 (*
2.1 --- a/src/Tools/isac/Interpret/appl.sml Thu Sep 23 14:49:23 2010 +0200
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu Sep 23 16:38:25 2010 +0200
2.3 @@ -19,16 +19,16 @@
2.4 fun from_pblobj_or_detail_thm thm' p pt =
2.5 let val (pbl,p',rls') = par_pbl_det pt p
2.6 in if pbl
2.7 - then let (*val _= writeln("### from_pblobj_or_detail_thm: pbl=true")*)
2.8 + then let (*val _= tracing("### from_pblobj_or_detail_thm: pbl=true")*)
2.9 val thy' = get_obj g_domID pt p'
2.10 val {rew_ord',erls,(*asm_thm,*)...} =
2.11 get_met (get_obj g_metID pt p')
2.12 - (*val _= writeln("### from_pblobj_or_detail_thm: metID= "^
2.13 + (*val _= tracing("### from_pblobj_or_detail_thm: metID= "^
2.14 (metID2str(get_obj g_metID pt p')))
2.15 - val _= writeln("### from_pblobj_or_detail_thm: erls= "^erls)*)
2.16 + val _= tracing("### from_pblobj_or_detail_thm: erls= "^erls)*)
2.17 in ("OK",thy',rew_ord',erls,(*put_asm*)false)
2.18 end
2.19 - else ((*writeln("### from_pblobj_or_detail_thm: pbl=false");*)
2.20 + else ((*tracing("### from_pblobj_or_detail_thm: pbl=false");*)
2.21 (*case assoc(!ruleset', rls') of !!!FIXME.3.4.03:re-organize !!!
2.22 NONE => ("unknown ruleset '"^rls'^"'","","",Erls,false)
2.23 | SOME rls =>*)
2.24 @@ -138,7 +138,7 @@
2.25 (asm', true) => ([HOLogic.mk_eq sub], asm')
2.26 | (_, false) => ([],[])
2.27 end;
2.28 - (*val _= writeln("### check_elementwise: res= "^(term2str all_results)^
2.29 + (*val _= tracing("### check_elementwise: res= "^(term2str all_results)^
2.30 ", bdv= "^(term2str bdv)^", asm= "^(terms2str asm));*)
2.31 val c' = isalist2list all_results
2.32 val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*)
2.33 @@ -152,7 +152,7 @@
2.34 > val asm = str2term "(x ~= a) & (x ~= b)";
2.35 > val erls = e_rls;
2.36 > val (t, ts) = check_elementwise thy erls all_results (bdv, asm);
2.37 -> term2str t; writeln(terms2str ts);
2.38 +> term2str t; tracing(terms2str ts);
2.39 val it = "[x = a + b, x = b, x = c]" : string
2.40 ["a + b ~= a & a + b ~= b","b ~= a & b ~= b","c ~= a & c ~= b"]
2.41 ... with appropriate erls this should be:
2.42 @@ -404,7 +404,7 @@
2.43 (pos'2str (p,p_)));
2.44 in if msg = "OK"
2.45 then
2.46 - ((*writeln("### applicable_in rls'= "^rls');*)
2.47 + ((*tracing("### applicable_in rls'= "^rls');*)
2.48 (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
2.49 *)
2.50 case rewrite_ thy (assoc_rew_ord ro)
2.51 @@ -497,7 +497,7 @@
2.52 (pos'2str (p,p_)));
2.53 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
2.54 SOME (f',asm) =>
2.55 - ((*writeln("#.# applicable_in Rewrite_Set,2f'= "^f');*)
2.56 + ((*tracing("#.# applicable_in Rewrite_Set,2f'= "^f');*)
2.57 Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
2.58 )
2.59 | NONE => Notappl (rls^" not applicable") end
2.60 @@ -693,21 +693,21 @@
2.61 val thy = assoc_thy thy'
2.62 val metID = (get_obj g_metID pt pp)
2.63 val {crls,...} = get_met metID
2.64 - (*val _=writeln("### applicable_in Check_elementwise: crls= "^crls)
2.65 - val _=writeln("### applicable_in Check_elementwise: pred= "^pred)*)
2.66 + (*val _=tracing("### applicable_in Check_elementwise: crls= "^crls)
2.67 + val _=tracing("### applicable_in Check_elementwise: pred= "^pred)*)
2.68 (*val erl = the (assoc'(!ruleset',crls))*)
2.69 val (f,asm) = case p_ of
2.70 Frm => (get_obj g_form pt p , [])
2.71 | Res => get_obj g_result pt p;
2.72 - (*val _= writeln("### applicable_in Check_elementwise: f= "^f);*)
2.73 + (*val _= tracing("### applicable_in Check_elementwise: f= "^f);*)
2.74 val vp = mk_set thy pt p f ((term_of o the o (parse thy)) pred);
2.75 - (*val (v,p)=vp;val _=writeln("### applicable_in Check_elementwise: vp= "^
2.76 + (*val (v,p)=vp;val _=tracing("### applicable_in Check_elementwise: vp= "^
2.77 pair2str(term2str v,term2str p))*)
2.78 in case f of
2.79 Const ("List.list.Cons",_) $ _ $ _ =>
2.80 Appl (Check_elementwise'
2.81 (f, pred,
2.82 - ((*writeln("### applicable_in Check_elementwise: --> "^
2.83 + ((*tracing("### applicable_in Check_elementwise: --> "^
2.84 (res2str (check_elementwise thy crls f vp)));*)
2.85 check_elementwise thy crls f vp)))
2.86 | Const ("Tools.UniversalList",_) =>
2.87 @@ -756,12 +756,12 @@
2.88 "subproblem_equation_dummy ("^(term2str f)^")"))
2.89 else Notappl "applicable only to equations made explicit"
2.90 | "solve_equation_dummy" =>
2.91 - let (*val _= writeln("### applicable_in: solve_equation_dummy: f= "
2.92 + let (*val _= tracing("### applicable_in: solve_equation_dummy: f= "
2.93 ^f);*)
2.94 val (id',f') = split_dummy (term2str f);
2.95 - (*val _= writeln("### applicable_in: f'= "^f');*)
2.96 + (*val _= tracing("### applicable_in: f'= "^f');*)
2.97 (*val _= (term_of o the o (parse thy)) f';*)
2.98 - (*val _= writeln"### applicable_in: solve_equation_dummy";*)
2.99 + (*val _= tracing"### applicable_in: solve_equation_dummy";*)
2.100 in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
2.101 else if is_expliceq ((term_of o the o (parse thy)) f')
2.102 then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
3.1 --- a/src/Tools/isac/Interpret/calchead.sml Thu Sep 23 14:49:23 2010 +0200
3.2 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Sep 23 16:38:25 2010 +0200
3.3 @@ -618,7 +618,7 @@
3.4 *)
3.5 fun nxt_spec Pbl preok (oris:ori list) ((dI',pI',mI'):spec)
3.6 ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec) =
3.7 - ((*writeln"### nxt_spec Pbl";*)
3.8 + ((*tracing"### nxt_spec Pbl";*)
3.9 if dI'=e_domID andalso dI=e_domID then (Pbl, Specify_Theory dI')
3.10 else if pI'=e_pblID andalso pI=e_pblID then (Pbl, Specify_Problem pI')
3.11 else case find_first (is_error o #5) (pbl:itm list) of
3.12 @@ -626,13 +626,13 @@
3.13 (Pbl, mk_delete
3.14 (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
3.15 | NONE =>
3.16 - ((*writeln"### nxt_spec is_error NONE";*)
3.17 + ((*tracing"### nxt_spec is_error NONE";*)
3.18 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))
3.19 oris pbt pbl of
3.20 (* val SOME (fd,ct') = nxt_add (assoc_thy (if dI=e_domID then dI' else dI))
3.21 oris pbt pbl;
3.22 *)
3.23 - SOME (fd,ct') => ((*writeln"### nxt_spec nxt_add SOME";*)
3.24 + SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
3.25 (Pbl, mk_additem fd ct'))
3.26 | NONE => (*pbl-items complete*)
3.27 if not preok then (Pbl, Refine_Problem pI')
3.28 @@ -657,7 +657,7 @@
3.29 (ppc, (#ppc o get_met) cmI), (dI,pI,mI));
3.30 *)
3.31 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
3.32 - ((*writeln"### nxt_spec Met"; *)
3.33 + ((*tracing"### nxt_spec Met"; *)
3.34 case find_first (is_error o #5) met of
3.35 SOME (_,_,_,fd,itm_) =>
3.36 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
3.37 @@ -665,7 +665,7 @@
3.38 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
3.39 SOME (fd,ct') => (Met, mk_additem fd ct')
3.40 | NONE =>
3.41 - ((*writeln"### nxt_spec Met: nxt_add NONE";*)
3.42 + ((*tracing"### nxt_spec Met: nxt_add NONE";*)
3.43 if dI = e_domID then (Met, Specify_Theory dI')
3.44 else if pI = e_pblID then (Met, Specify_Problem pI')
3.45 else if not preok then (Met, Specify_Method mI)
3.46 @@ -955,7 +955,7 @@
3.47 SOME ((([1], str, dsc, (*[var]*)
3.48 split_dts' (dsc, var))): preori)(*:ori without leading #*))
3.49 handle e as TYPE _ =>
3.50 - (writeln (dashs 70 ^ "\n"
3.51 + (tracing (dashs 70 ^ "\n"
3.52 ^"*** ERROR while creating the items for the model of the ->problem\n"
3.53 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
3.54 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
3.55 @@ -972,7 +972,7 @@
3.56 precondition: copy-named vars are filtered out.*)
3.57 fun matc thy ([]:pat list) _ (oris:preori list) = oris
3.58 | matc thy pbt [] _ =
3.59 - (writeln (dashs 70);
3.60 + (tracing (dashs 70);
3.61 raise error ("actual arg(s) missing for '"^pats2str pbt
3.62 ^"' i.e. should be 'copy-named' by '*_._'"))
3.63 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
3.64 @@ -1049,7 +1049,7 @@
3.65 ^dashs 70)
3.66 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
3.67 val _ = show_types:= s
3.68 - in writeln msg end;
3.69 + in tracing msg end;
3.70
3.71
3.72 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
3.73 @@ -1080,7 +1080,7 @@
3.74 | eq_untouched _ _ = false;
3.75 val ppc' =
3.76 (
3.77 - (*writeln("### insert_ppc: itm= "^(itm2str_ itm));*)
3.78 + (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
3.79 case seek_ppc (#1 itm) ppc of
3.80 (* val SOME xxx = seek_ppc (#1 itm) ppc;
3.81 *)
3.82 @@ -1111,8 +1111,8 @@
3.83
3.84
3.85 (* test-printouts ---
3.86 -val _=writeln("### insert_ppc: (d,ts)="^((Syntax.string_of_term (thy2ctxt thy))(comp_dts thy(d,ts))));
3.87 - val _=writeln("### insert_ppc: pts= "^
3.88 +val _=tracing("### insert_ppc: (d,ts)="^((Syntax.string_of_term (thy2ctxt thy))(comp_dts thy(d,ts))));
3.89 + val _=tracing("### insert_ppc: pts= "^
3.90 (strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) pts);
3.91
3.92
3.93 @@ -1147,7 +1147,7 @@
3.94 Uistate (p,Met) pt
3.95 val pre' = check_preconds thy prls pre met'
3.96 val pb = foldl and_ (true, map fst pre')
3.97 - (*val _=writeln("@@@ specify_additem: Met Add before nxt_spec")*)
3.98 + (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
3.99 val (p_,nxt) =
3.100 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
3.101 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
3.102 @@ -1158,7 +1158,7 @@
3.103 | Err msg =>
3.104 let val pre' = check_preconds thy prls pre met
3.105 val pb = foldl and_ (true, map fst pre')
3.106 - (*val _=writeln("@@@ specify_additem: Met Err before nxt_spec")*)
3.107 + (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
3.108 val (p_,nxt) =
3.109 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
3.110 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
3.111 @@ -1179,7 +1179,7 @@
3.112 (* val Add itm = appl_add thy sel oris pbl ppc ct;
3.113 *)
3.114 let
3.115 - (*val _= writeln("###specify_additem: itm= "^(itm2str_ itm));*)
3.116 + (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
3.117 val pbl' = insert_ppc thy itm pbl
3.118 val ((p,Pbl),_,_,pt') =
3.119 generate1 thy (case sel of
3.120 @@ -1189,7 +1189,7 @@
3.121 Uistate (p,Pbl) pt
3.122 val pre = check_preconds thy prls where_ pbl'
3.123 val pb = foldl and_ (true, map fst pre)
3.124 - (*val _=writeln("@@@ specify_additem: Pbl Add before nxt_spec")*)
3.125 + (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
3.126 val (p_,nxt) =
3.127 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
3.128 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
3.129 @@ -1202,7 +1202,7 @@
3.130 | Err msg =>
3.131 let val pre = check_preconds thy prls where_ pbl
3.132 val pb = foldl and_ (true, map fst pre)
3.133 - (*val _=writeln("@@@ specify_additem: Pbl Err before nxt_spec")*)
3.134 + (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
3.135 val (p_,nxt) =
3.136 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
3.137 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
3.138 @@ -1314,7 +1314,7 @@
3.139 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
3.140 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
3.141 val mI'' = if mI=e_metID then mI' else mI;
3.142 - (*val _=writeln("@@@ specify (Specify_Problem) before nxt_spec")*)
3.143 + (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
3.144 val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
3.145 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
3.146 in ((p,Pbl), (pos,Uistate),
3.147 @@ -1340,7 +1340,7 @@
3.148 val pt = update_metID pt p mID*)
3.149 val (pos,_,_,pt)=
3.150 generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
3.151 - (*val _=writeln("@@@ specify (Specify_Method) before nxt_spec")*)
3.152 + (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
3.153 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
3.154 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
3.155 in (pos, (pos,Uistate),
3.156 @@ -1372,7 +1372,7 @@
3.157 val pb = foldl and_ (true, map fst pre)
3.158 in if domID = dI
3.159 then let
3.160 - (*val _=writeln("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
3.161 + (*val _=tracing("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
3.162 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
3.163 (pbl,met) (ppc,mpc) (dI,pI,mI);
3.164 in ((p,p_), (pos,Uistate),
3.165 @@ -1384,7 +1384,7 @@
3.166 (*val pt = update_domID pt p domID;11.8.03*)
3.167 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
3.168 Uistate (p,p_) pt
3.169 - (*val _=writeln("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
3.170 + (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
3.171 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
3.172 (ppc,mpc) (domID,pI,mI);
3.173 in ((p,p_), (pos,Uistate),
3.174 @@ -1411,7 +1411,7 @@
3.175 (* val Add itm = appl_add thy sel oris pbl ppc ct;
3.176 *)
3.177 let
3.178 - (*val _=writeln("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
3.179 + (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
3.180 val pbl' = insert_ppc thy itm pbl
3.181 val (tac,tac_) =
3.182 case sel of
3.183 @@ -1743,8 +1743,8 @@
3.184 val it = "fixed_values [R]" : cterm
3.185 *)
3.186 fun chktyp thy (n, fs, gs) =
3.187 - ((writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) fs;
3.188 - (writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) gs;
3.189 + ((tracing o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) fs;
3.190 + (tracing o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) gs;
3.191 tag_form thy (nth n fs, nth n gs));
3.192
3.193 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
3.194 @@ -1874,10 +1874,10 @@
3.195
3.196
3.197 (*
3.198 - writeln (oris2str pors);
3.199 + tracing (oris2str pors);
3.200
3.201 - writeln (itms2str_ thy pits);
3.202 - writeln (itms2str_ thy mits);
3.203 + tracing (itms2str_ thy pits);
3.204 + tracing (itms2str_ thy mits);
3.205 *)
3.206
3.207
3.208 @@ -1888,7 +1888,7 @@
3.209 val (pt, (p, _)) = (pt, pos);
3.210 *)
3.211 let val _= if p_ <> Pbl
3.212 - then writeln("###complete_mod: only impl.for Pbl, called with "^
3.213 + then tracing("###complete_mod: only impl.for Pbl, called with "^
3.214 pos'2str pos) else ()
3.215 val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
3.216 get_obj I pt p
3.217 @@ -2161,7 +2161,7 @@
3.218
3.219 (*WN050225 omits the last step, if pt is incomplete*)
3.220 fun show_pt pt =
3.221 - writeln (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
3.222 + tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
3.223
3.224 (*.get a calchead from a PblObj-node in the ctree;
3.225 preconditions must be calculated.*)
4.1 --- a/src/Tools/isac/Interpret/ctree.sml Thu Sep 23 14:49:23 2010 +0200
4.2 +++ b/src/Tools/isac/Interpret/ctree.sml Thu Sep 23 16:38:25 2010 +0200
4.3 @@ -3,7 +3,7 @@
4.4 use"ctree.sml";
4.5 W.N.26.10.99
4.6
4.7 -writeln (pr_ptree pr_short pt);
4.8 +tracing (pr_ptree pr_short pt);
4.9
4.10 val Nd ( _, ns) = pt;
4.11
4.12 @@ -882,7 +882,7 @@
4.13 [Nd("xx2.1.",[]),
4.14 Nd("xx2.2.",[])]),
4.15 Nd("xx3",[])]);
4.16 -> writeln (pr_ptree prfn (!pt));
4.17 +> tracing (pr_ptree prfn (!pt));
4.18 *)
4.19
4.20
4.21 @@ -1063,7 +1063,7 @@
4.22 Nd (b', repl_app bs p (insert b (nth p bs) ps));
4.23 (*
4.24 > type ppobj = string;
4.25 -> writeln (pr_ptree prfn (!pt));
4.26 +> tracing (pr_ptree prfn (!pt));
4.27 val pt = Unsynchronized.ref Empty;
4.28 pt:= insert ("root'":ppobj) EmptyPtree [];
4.29 pt:= insert ("xx1":ppobj) (!pt) [1];
4.30 @@ -1354,15 +1354,15 @@
4.31 ...........===^===*)
4.32
4.33 fun get_asm (b:pos, p:pos) (Nd (PblObj {result=(_,asm),...},_)) =
4.34 - ((*writeln ("### get_asm PblObj:(b,p)= "^
4.35 + ((*tracing ("### get_asm PblObj:(b,p)= "^
4.36 (pair2str(ints2str b, ints2str p)));*)
4.37 (map (rpair b) asm):asms)
4.38 | get_asm (b, p) (Nd (PrfObj {result=(_,asm),...}, [])) =
4.39 - ((*writeln ("### get_asm PrfObj []:(b,p)= "^
4.40 + ((*tracing ("### get_asm PrfObj []:(b,p)= "^
4.41 (pair2str(ints2str b, ints2str p)));*)
4.42 (map (rpair b) asm))
4.43 | get_asm (b, p:pos) (Nd (PrfObj _, nds)) =
4.44 - let (*val _= writeln ("### get_asm PrfObj nds:(b,p)= "^
4.45 + let (*val _= tracing ("### get_asm PrfObj nds:(b,p)= "^
4.46 (pair2str(ints2str b, ints2str p)));*)
4.47 val levdn =
4.48 if p <> [] then (b @ [hd p]:pos, tl p:pos)
4.49 @@ -1371,7 +1371,7 @@
4.50 and gets_asm _ _ [] = []
4.51 | gets_asm (b, p' as p::ps) i (nd::nds) =
4.52 if p < i then []
4.53 - else ((*writeln ("### gets_asm: (b,p')= "^(pair2str(ints2str b,
4.54 + else ((*tracing ("### gets_asm: (b,p')= "^(pair2str(ints2str b,
4.55 ints2str p')));*)
4.56 (get_asm (b @ [i], ps) nd) @ (gets_asm (b, p') (i + 1) nds));
4.57
4.58 @@ -1386,7 +1386,7 @@
4.59 Frm => let val (qs,q) = split_last offset
4.60 in qs @ [q - 1] end
4.61 | _ => offset
4.62 - (*val _= writeln ("... get_assumptions: (b,o)= "^
4.63 + (*val _= tracing ("... get_assumptions: (b,o)= "^
4.64 (pair2str(ints2str base',ints2str offset)))*)
4.65 in gets_asm (base', offset) 1 cn end;
4.66
4.67 @@ -1544,7 +1544,7 @@
4.68 | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
4.69 if p > length ns then raise PTREE "move_dn: pos not existent 3"
4.70 else if is_pblnd (nth p ns) then
4.71 - ((*writeln("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^
4.72 + ((*tracing("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^
4.73 "length ns= "^((string_of_int o length) ns)^
4.74 ", p= "^string_of_int p^", p_= "^pos_2str p_);*)
4.75 case p_ of Res => if p = length ns
4.76 @@ -1763,10 +1763,10 @@
4.77 fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
4.78 | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)
4.79 if g_ostate b = Incomplete
4.80 - then ((*writeln("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*)
4.81 + then ((*tracing("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*)
4.82 [(p,Frm)] @ (get_allpos's (p, 1) bs)
4.83 )
4.84 - else ((*writeln("get_allpos' (p, 1) else: p="^ints2str' p);*)
4.85 + else ((*tracing("get_allpos' (p, 1) else: p="^ints2str' p);*)
4.86 [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
4.87 )
4.88 (*WN041020 here we assume what is presented on the worksheet ?!*)
4.89 @@ -1938,12 +1938,12 @@
4.90 then (Nd (del_res b, children),
4.91 cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
4.92 else (Nd (b, children), cuts)
4.93 - (*val _= writeln("####cut_bottom (P, p)="^pos2str (P @ [p])^
4.94 + (*val _= tracing("####cut_bottom (P, p)="^pos2str (P @ [p])^
4.95 ", Nd=.............................................")
4.96 val _= show_pt pt''
4.97 - val _= writeln("####cut_bottom form='"^
4.98 + val _= tracing("####cut_bottom form='"^
4.99 term2str (get_obj g_form pt'' []))
4.100 - val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^
4.101 + val _= tracing("####cut_bottom cuts#="^string_of_int (length cuts)^
4.102 ", cuts="^pos's2str cuts)*)
4.103 in ((pt'', cuts:pos' list), cutlevup b) end;
4.104
4.105 @@ -1977,14 +1977,14 @@
4.106 then (Nd (del_res b, children),
4.107 cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
4.108 else (Nd (b, children), cuts')
4.109 - (*val _= writeln("#####cut_levup clevup= "^bool2str clevup)
4.110 - val _= writeln("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
4.111 - val _= writeln("#####cut_levup (P, p)="^pos2str (P @ [p])^
4.112 + (*val _= tracing("#####cut_levup clevup= "^bool2str clevup)
4.113 + val _= tracing("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
4.114 + val _= tracing("#####cut_levup (P, p)="^pos2str (P @ [p])^
4.115 ", Nd=.............................................")
4.116 val _= show_pt pt''
4.117 - val _= writeln("#####cut_levup form='"^
4.118 + val _= tracing("#####cut_levup form='"^
4.119 term2str (get_obj g_form pt'' []))
4.120 - val _= writeln("#####cut_levup cuts#="^string_of_int (length cuts)^
4.121 + val _= tracing("#####cut_levup cuts#="^string_of_int (length cuts)^
4.122 ", cuts="^pos's2str cuts)*)
4.123 in if null P then (pt'', (cuts @ cuts'):pos' list)
4.124 else let val (P, p) = split_last P
4.125 @@ -2007,7 +2007,7 @@
4.126 end;
4.127
4.128 fun append_atomic p l f r f' s pt =
4.129 - let (**val _= writeln("#@append_atomic: pos ="^pos2str p)**)
4.130 + let (**val _= tracing("#@append_atomic: pos ="^pos2str p)**)
4.131 val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
4.132 then (*after Take*)
4.133 ((fst (get_obj g_loc pt p), SOME l),
4.134 @@ -2032,7 +2032,7 @@
4.135 (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
4.136 (f',asm),Complete);
4.137 *)
4.138 -((*writeln("##@cappend_atomic: pos ="^pos2str p);*)
4.139 +((*tracing("##@cappend_atomic: pos ="^pos2str p);*)
4.140 apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
4.141 );
4.142 (*TODO.WN050305 redesign the handling of istates*)
4.143 @@ -2050,7 +2050,7 @@
4.144
4.145 (* called by Take *)
4.146 fun append_form p l f pt =
4.147 -((*writeln("##@append_form: pos ="^pos2str p);*)
4.148 +((*tracing("##@append_form: pos ="^pos2str p);*)
4.149 insert (PrfObj {cell = NONE,
4.150 form = (*if existpt p pt
4.151 andalso get_obj g_tac pt p = Empty_Tac
4.152 @@ -2066,22 +2066,22 @@
4.153 val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
4.154 *)
4.155 fun cappend_form pt p loc f =
4.156 -((*writeln("##@cappend_form: pos ="^pos2str p);*)
4.157 +((*tracing("##@cappend_form: pos ="^pos2str p);*)
4.158 apfst (append_form p loc f) (cut_tree pt (p,Frm))
4.159 );
4.160 fun cappend_form pt p loc f =
4.161 -let (*val _= writeln("##@cappend_form: pos ="^pos2str p)
4.162 - val _= writeln("##@cappend_form before cut_tree: loc ="^istate2str loc)*)
4.163 +let (*val _= tracing("##@cappend_form: pos ="^pos2str p)
4.164 + val _= tracing("##@cappend_form before cut_tree: loc ="^istate2str loc)*)
4.165 val (pt', cs) = cut_tree pt (p,Frm)
4.166 val pt'' = append_form p loc f pt'
4.167 - (*val _= writeln("##@cappend_form after append: loc ="^
4.168 + (*val _= tracing("##@cappend_form after append: loc ="^
4.169 istates2str (get_obj g_loc pt'' p))*)
4.170 in (pt'', cs) end;
4.171
4.172
4.173
4.174 fun append_result pt p l f s =
4.175 -((*writeln("##@append_result: pos ="^pos2str p);*)
4.176 +((*tracing("##@append_result: pos ="^pos2str p);*)
4.177 (appl_obj (repl_result (fst (get_obj g_loc pt p),
4.178 SOME l) f s) pt p, [])
4.179 );
4.180 @@ -2089,7 +2089,7 @@
4.181
4.182 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
4.183 fun append_parent p l f r b pt =
4.184 - let (*val _= writeln("###append_parent: pos ="^pos2str p);*)
4.185 + let (*val _= tracing("###append_parent: pos ="^pos2str p);*)
4.186 val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
4.187 then ((fst (get_obj g_loc pt p), SOME l),
4.188 get_obj g_form pt p)
4.189 @@ -2103,13 +2103,13 @@
4.190 result= (e_term,[]),
4.191 ostate= Incomplete}) pt p end;
4.192 fun cappend_parent pt p loc f r b =
4.193 -((*writeln("###cappend_parent: pos ="^pos2str p);*)
4.194 +((*tracing("###cappend_parent: pos ="^pos2str p);*)
4.195 apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
4.196 );
4.197
4.198
4.199 fun append_problem [] l fmz (strs,spec,hdf) _ =
4.200 -((*writeln("###append_problem: pos = []");*)
4.201 +((*tracing("###append_problem: pos = []");*)
4.202 (Nd (PblObj
4.203 {cell = NONE,
4.204 origin= (strs,spec,hdf),
4.205 @@ -2124,7 +2124,7 @@
4.206 ostate= Incomplete},[]))
4.207 )
4.208 | append_problem p l fmz (strs,spec,hdf) pt =
4.209 -((*writeln("###append_problem: pos ="^pos2str p);*)
4.210 +((*tracing("###append_problem: pos ="^pos2str p);*)
4.211 insert (PblObj
4.212 {cell = NONE,
4.213 origin= (strs,spec,hdf),
4.214 @@ -2139,11 +2139,11 @@
4.215 ostate= Incomplete}) pt p
4.216 );
4.217 fun cappend_problem _ [] loc fmz ori =
4.218 -((*writeln("###cappend_problem: pos = []");*)
4.219 +((*tracing("###cappend_problem: pos = []");*)
4.220 (append_problem [] loc fmz ori EmptyPtree,[])
4.221 )
4.222 | cappend_problem pt p loc fmz ori =
4.223 -((*writeln("###cappend_problem: pos ="^pos2str p);*)
4.224 +((*tracing("###cappend_problem: pos ="^pos2str p);*)
4.225 apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm))
4.226 );
4.227
5.1 --- a/src/Tools/isac/Interpret/generate.sml Thu Sep 23 14:49:23 2010 +0200
5.2 +++ b/src/Tools/isac/Interpret/generate.sml Thu Sep 23 16:38:25 2010 +0200
5.3 @@ -318,13 +318,13 @@
5.4 end
5.5
5.6 | generate1 thy (Apply_Method' (_,topt, is)) _ (pos as (p,p_)) pt =
5.7 - ((*writeln("###generate1 Apply_Method': pos = "^pos'2str (p,p_));
5.8 - writeln("###generate1 Apply_Method': topt= "^termopt2str topt);
5.9 - writeln("###generate1 Apply_Method': is = "^istate2str is);*)
5.10 + ((*tracing("###generate1 Apply_Method': pos = "^pos'2str (p,p_));
5.11 + tracing("###generate1 Apply_Method': topt= "^termopt2str topt);
5.12 + tracing("###generate1 Apply_Method': is = "^istate2str is);*)
5.13 case topt of
5.14 SOME t =>
5.15 let val (pt,c) = cappend_form pt p is t
5.16 - (*val _= writeln("###generate1 Apply_Method: after cappend")*)
5.17 + (*val _= tracing("###generate1 Apply_Method: after cappend")*)
5.18 in (pos,c, EmptyMout,pt)
5.19 end
5.20 | NONE =>
5.21 @@ -333,7 +333,7 @@
5.22 ((assoc_thy "Isac.thy"), tac_, is, pos, pt);
5.23 *)
5.24 | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *)
5.25 - let (*val _=writeln("### generate1: Take' pos="^pos'2str (p,p_));*)
5.26 + let (*val _=tracing("### generate1: Take' pos="^pos'2str (p,p_));*)
5.27 val p = let val (ps,p') = split_last p(*no connex to prev.ppobj*)
5.28 in if p'=0 then ps@[1] else p end;
5.29 val (pt,c) = cappend_form pt p l t;
5.30 @@ -374,7 +374,7 @@
5.31 pt) end
5.32
5.33 | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) l (p,p_) pt =
5.34 - let (*val _= writeln("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*)
5.35 + let (*val _= tracing("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*)
5.36 val (pt,c) = cappend_atomic pt p l f
5.37 (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
5.38 val pt = update_branch pt p TransitiveB (*040312*)
5.39 @@ -383,7 +383,7 @@
5.40 pt) end
5.41
5.42 | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) l (p,p_) pt =
5.43 - let (*val _= writeln("###generate1 Rewrite': pos= "^pos'2str (p,p_))*)
5.44 + let (*val _= tracing("###generate1 Rewrite': pos= "^pos'2str (p,p_))*)
5.45 val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete
5.46 val pt = update_branch pt p TransitiveB (*040312*)
5.47 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
5.48 @@ -397,7 +397,7 @@
5.49 (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) =
5.50 (assoc_thy "Isac.thy", tac_, is, pos, pt);
5.51 *)
5.52 - let (*val _=writeln("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*)
5.53 + let (*val _=tracing("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*)
5.54 val (pt,c) = cappend_atomic pt p l f
5.55 (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
5.56 val pt = update_branch pt p TransitiveB (*040312*)
5.57 @@ -415,7 +415,7 @@
5.58 in (*implicit Take*) generate1 thy tac_ is pos' pt end
5.59
5.60 | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
5.61 - let (*val _= writeln("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
5.62 + let (*val _= tracing("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
5.63 val (pt,c) = cappend_atomic pt p l f
5.64 (Rewrite_Set (id_rls rls')) (f',asm) Complete
5.65 val pt = update_branch pt p TransitiveB (*040312*)
5.66 @@ -433,7 +433,7 @@
5.67 in (*implicit Take*) generate1 thy tac_ is pos' pt end
5.68
5.69 | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
5.70 - let (*val _=writeln("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
5.71 + let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
5.72 (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*)
5.73 val (pt,c) = append_result pt p l (scval,map str2term asm) Complete
5.74 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p),
5.75 @@ -445,7 +445,7 @@
5.76 pt) end
5.77
5.78 | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =
5.79 - let(*val _=writeln("###generate1 Check_elementwise': p= "^pos'2str(p,p_))*)
5.80 + let(*val _=tracing("###generate1 Check_elementwise': p= "^pos'2str(p,p_))*)
5.81 val (pt,c) = cappend_atomic pt p l consts
5.82 (Check_elementwise pred) (f',asm) Complete;
5.83 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
5.84 @@ -471,12 +471,12 @@
5.85
5.86 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, f))
5.87 l (p,p_) pt =
5.88 - let (*val _=writeln("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
5.89 + let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
5.90 val (pt,c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
5.91 (oris, (domID, pblID, metID), hdl);
5.92 (*val pbl = init_pbl ((#ppc o get_pbt) pblID);
5.93 val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*)
5.94 - (*val _= writeln("### generate1: is([3],Frm)= "^
5.95 + (*val _= tracing("### generate1: is([3],Frm)= "^
5.96 (istate2str (get_istate pt ([3],Frm))));*)
5.97 val f = Syntax.string_of_term (thy2ctxt thy) f;
5.98 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
6.1 --- a/src/Tools/isac/Interpret/inform.sml Thu Sep 23 14:49:23 2010 +0200
6.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Sep 23 16:38:25 2010 +0200
6.3 @@ -358,7 +358,7 @@
6.4 (#1 (some_spec ospec spec), oris, []:itm list,
6.5 ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
6.6 val iii = appl_adds dI oris ppc pbt (selct::ss);
6.7 - writeln(itms2str_ thy iii);
6.8 + tracing(itms2str_ thy iii);
6.9
6.10 val itm = appl_add' dI oris ppc pbt selct;
6.11 val ppc = insert_ppc' itm ppc;
6.12 @@ -370,7 +370,7 @@
6.13 val _::selct::ss = (selct::ss);
6.14 val itm = appl_add' dI oris ppc pbt selct;
6.15 val ppc = insert_ppc' itm ppc;
6.16 - writeln(itms2str_ thy ppc);
6.17 + tracing(itms2str_ thy ppc);
6.18
6.19 val _::selct::ss = (selct::ss);
6.20 val itm = appl_add' dI oris ppc pbt selct;
6.21 @@ -630,14 +630,14 @@
6.22 (*
6.23 val ({rew_ord, erls, rules,...}, fo, ifo) =
6.24 (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
6.25 - (writeln o trtas2str) fod';
6.26 + (tracing o trtas2str) fod';
6.27 > ["
6.28 (x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","
6.29 (-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","
6.30 (-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","
6.31 (1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
6.32 val it = () : unit
6.33 - (writeln o trtas2str) (map rev_deriv' rifod');
6.34 + (tracing o trtas2str) (map rev_deriv' rifod');
6.35 > ["
6.36 (1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","
6.37 (1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","
6.38 @@ -684,7 +684,7 @@
6.39 | _ => cs';
6.40 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
6.41 end;
6.42 -(* writeln (trtas2str der);
6.43 +(* tracing (trtas2str der);
6.44 *)
6.45
6.46 (*.handle a user-input formula, which may be a CAS-command, too.
7.1 --- a/src/Tools/isac/Interpret/mathengine.sml Thu Sep 23 14:49:23 2010 +0200
7.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Thu Sep 23 16:38:25 2010 +0200
7.3 @@ -96,7 +96,7 @@
7.4 fun loc_solve_ m (pt,pos) =
7.5 let val (msg, cs') = solve m (pt, pos);
7.6 (* val (tacis,dels,(pt',p')) = cs';
7.7 - (writeln o istate2str) (get_istate pt' p');
7.8 + (tracing o istate2str) (get_istate pt' p');
7.9 (term2str o fst) (get_obj g_result pt' (fst p'));
7.10 *)
7.11 in case msg of
7.12 @@ -465,7 +465,7 @@
7.13 let val (pt, p) =
7.14 (* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p);
7.15 p = ([1, 9], Res);
7.16 - (writeln o istate2str) (get_istate pt p);
7.17 + (tracing o istate2str) (get_istate pt p);
7.18 *)
7.19 (*locatetac is here for testing by me; step would suffice in me*)
7.20 case locatetac tac (pt,p) of
8.1 --- a/src/Tools/isac/Interpret/mstools.sml Thu Sep 23 14:49:23 2010 +0200
8.2 +++ b/src/Tools/isac/Interpret/mstools.sml Thu Sep 23 16:38:25 2010 +0200
8.3 @@ -166,7 +166,7 @@
8.4 let val elems = isalist2list t
8.5 in map ((list2isalist (type_of (hd elems))) o single) elems end;
8.6 (*val t = str2term "[a, b]";
8.7 -> val ts = take_apart t; writeln (terms2str ts);
8.8 +> val ts = take_apart t; tracing (terms2str ts);
8.9 ["[a]","[b]"]
8.10
8.11 > t = (take_apart_inv o take_apart) t;
8.12 @@ -340,10 +340,10 @@
8.13 (* tests see fun comp_dts
8.14
8.15 > val t = str2term "someList []";
8.16 -> val (_,ts) = split_dts thy t; writeln (terms2str ts);
8.17 +> val (_,ts) = split_dts thy t; tracing (terms2str ts);
8.18 ["[]"]
8.19 > val t = str2term "valuesFor []";
8.20 -> val (_,ts) = split_dts thy t; writeln (terms2str ts);
8.21 +> val (_,ts) = split_dts thy t; tracing (terms2str ts);
8.22 ["[]"]*)
8.23
8.24 (*.version returning ts only.*)
8.25 @@ -659,9 +659,9 @@
8.26 (*14.9.01: not used after putting values for penv into itm_
8.27 WN.5.5.03: used in upd .. upd_envv*)
8.28 fun upd_penv ctxt penv dsc (id, vl) =
8.29 -(writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
8.30 - writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
8.31 - writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
8.32 +(tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
8.33 + tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
8.34 + tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
8.35 overwrite (penv, (id, pbl_ids ctxt dsc vl))
8.36 );
8.37 (*
8.38 @@ -812,7 +812,7 @@
8.39 "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^
8.40 s^" ,"^(itm_2str_ ctxt itm_)^")";
8.41 fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
8.42 -fun w_itms2str_ ctxt itms = writeln (itms2str_ ctxt itms);
8.43 +fun w_itms2str_ ctxt itms = tracing (itms2str_ ctxt itms);
8.44
8.45 fun init_item str = SyntaxE str;
8.46
8.47 @@ -908,19 +908,19 @@
8.48 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
8.49 val unique = (term_of o the o (parse (theory "Real"))) "UnIqE_tErM";
8.50 fun d_in (Cor ((d,_),_)) = d
8.51 - | d_in (Syn (c)) = (writeln("*** d_in: Syn ("^c^")"); unique)
8.52 - | d_in (Typ (c)) = (writeln("*** d_in: Typ ("^c^")"); unique)
8.53 + | d_in (Syn (c)) = (tracing("*** d_in: Syn ("^c^")"); unique)
8.54 + | d_in (Typ (c)) = (tracing("*** d_in: Typ ("^c^")"); unique)
8.55 | d_in (Inc ((d,_),_)) = d
8.56 | d_in (Sup (d,_)) = d
8.57 | d_in (Mis (d,_)) = d;
8.58
8.59 fun dts2str (d,ts) = pair2str (term2str d, terms2str ts);
8.60 fun penvval_in (Cor ((d,_),(_,ts))) = [comp_ts (d,ts)]
8.61 - | penvval_in (Syn (c)) = (writeln("*** penvval_in: Syn ("^c^")"); [])
8.62 - | penvval_in (Typ (c)) = (writeln("*** penvval_in: Typ ("^c^")"); [])
8.63 + | penvval_in (Syn (c)) = (tracing("*** penvval_in: Syn ("^c^")"); [])
8.64 + | penvval_in (Typ (c)) = (tracing("*** penvval_in: Typ ("^c^")"); [])
8.65 | penvval_in (Inc (_,(_,ts))) = ts
8.66 - | penvval_in (Sup dts) = (writeln("*** penvval_in: Sup "^(dts2str dts)); [])
8.67 - | penvval_in (Mis (d,t)) = (writeln("*** penvval_in: Mis "^
8.68 + | penvval_in (Sup dts) = (tracing("*** penvval_in: Sup "^(dts2str dts)); [])
8.69 + | penvval_in (Mis (d,t)) = (tracing("*** penvval_in: Mis "^
8.70 (pair2str(term2str d, term2str t))); []);
8.71
8.72
9.1 --- a/src/Tools/isac/Interpret/ptyps.sml Thu Sep 23 14:49:23 2010 +0200
9.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Thu Sep 23 16:38:25 2010 +0200
9.3 @@ -517,14 +517,14 @@
9.4 fun insrt d pbt [k] [] = [Ptyp (k, [pbt],[])]
9.5
9.6 | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =
9.7 -((*writeln("### insert 1: ks = "^(strs2str [k])^" k'= "^k');*)
9.8 +((*tracing("### insert 1: ks = "^(strs2str [k])^" k'= "^k');*)
9.9 if k=k'
9.10 then ((Ptyp (k', [pbt], ps))::pys)
9.11 else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)
9.12 ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))
9.13 )
9.14 | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =
9.15 -((*writeln("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
9.16 +((*tracing("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
9.17 if k=k'
9.18 then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)
9.19 else
9.20 @@ -802,11 +802,11 @@
9.21 | scan id ((Ptyp ((i,_,[])))::ps) = [id@[i]] @(scan id ps)
9.22 | scan id ((Ptyp ((i,_,pl)))::ps) =(scan (id@[i]) pl)@(scan id ps);
9.23
9.24 -fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (!ptyps);
9.25 +fun show_ptyps () = (tracing o format_pblIDl o (scan [])) (!ptyps);
9.26 (* ptyps:=[];
9.27 show_ptyps();
9.28 *)
9.29 -fun show_mets () = (writeln o format_pblIDl o (scan [])) (!mets);
9.30 +fun show_mets () = (tracing o format_pblIDl o (scan [])) (!mets);
9.31
9.32
9.33
9.34 @@ -1137,7 +1137,7 @@
9.35 (rev ["linear","system"], fmz, [(*match list*)],
9.36 ((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp));
9.37 *)
9.38 - let val _ = (writeln o ((curry op^)"*** pass ") o strs2str)(pblRD @ [pI])
9.39 + let val _ = (tracing o ((curry op^)"*** pass ") o strs2str)(pblRD @ [pI])
9.40 val {thy,ppc,where_,prls,...} = py
9.41 val oris = prep_ori fmz thy ppc
9.42 (*8.3.02: itms!: oris ev. are _not_ complete here*)
9.43 @@ -1152,7 +1152,7 @@
9.44 refin' pblRD fmz pbls (Ptyp (pI,[py],pys));
9.45 *)
9.46 | refin' pblRD fmz pbls (Ptyp (pI,[py],pys)) =
9.47 - let val _ = (writeln o ((curry op^)"*** pass ") o strs2str) (pblRD @ [pI])
9.48 + let val _ = (tracing o ((curry op^)"*** pass ") o strs2str) (pblRD @ [pI])
9.49 val {thy,ppc,where_,prls,...} = py
9.50 val oris = prep_ori fmz thy ppc;
9.51 (*8.3.02: itms!: oris ev. are _not_ complete here*)
9.52 @@ -1172,7 +1172,7 @@
9.53
9.54 (*. refine a problem; version for tactic Refine_Problem .*)
9.55 fun refin'' thy (pblRD:pblRD) itms pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
9.56 - let (*val _ = writeln("### refin''1: pI="^pI);*)
9.57 + let (*val _ = tracing("### refin''1: pI="^pI);*)
9.58 val {thy,ppc,where_,prls,...} = py
9.59 val (b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
9.60 in if b then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
9.61 @@ -1182,7 +1182,7 @@
9.62 val Ptyp (pI,[py],pys) = app_ptyp I pblID (rev pblID) (!ptyps);
9.63 *)
9.64 | refin'' thy pblRD itms pbls (Ptyp (pI,[py],pys)) =
9.65 - let (*val _ = writeln("### refin''2: pI="^pI);*)
9.66 + let (*val _ = tracing("### refin''2: pI="^pI);*)
9.67 val {thy,ppc,where_,prls,...} = py
9.68 val(b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
9.69 in if b
9.70 @@ -1260,20 +1260,20 @@
9.71
9.72 fun show_pblguhs () =
9.73 (print_depth 999;
9.74 - (writeln o strs2str o (map linefeed)) (coll_pblguhs (!ptyps));
9.75 + (tracing o strs2str o (map linefeed)) (coll_pblguhs (!ptyps));
9.76 print_depth 3);
9.77 fun sort_pblguhs () =
9.78 (print_depth 999;
9.79 - (writeln o strs2str o (map linefeed))
9.80 + (tracing o strs2str o (map linefeed))
9.81 (((sort string_ord) o coll_pblguhs) (!ptyps));
9.82 print_depth 3);
9.83
9.84 fun show_metguhs () =
9.85 (print_depth 999;
9.86 - (writeln o strs2str o (map linefeed)) (coll_metguhs (!mets));
9.87 + (tracing o strs2str o (map linefeed)) (coll_metguhs (!mets));
9.88 print_depth 3);
9.89 fun sort_metguhs () =
9.90 (print_depth 999;
9.91 - (writeln o strs2str o (map linefeed))
9.92 + (tracing o strs2str o (map linefeed))
9.93 (((sort string_ord) o coll_metguhs) (!mets));
9.94 print_depth 3);
10.1 --- a/src/Tools/isac/Interpret/rewtools.sml Thu Sep 23 14:49:23 2010 +0200
10.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Sep 23 16:38:25 2010 +0200
10.3 @@ -73,7 +73,7 @@
10.4 in trm' end;
10.5 (*ML {*
10.6 val trm = @{term "k ~= 0 ==> k * m / (k * n) = m / n"};
10.7 -(writeln o (Syntax.string_of_term @{context})) (sym_trm trm);
10.8 +(tracing o (Syntax.string_of_term @{context})) (sym_trm trm);
10.9 "~ k = (0::'a) ==> m / n = k * m / (k * n)"
10.10 *}*)
10.11
10.12 @@ -121,29 +121,29 @@
10.13 else rew_or_calc lim rts t apno rs')
10.14 and rew_or_calc lim rts t apno (rrs' as (r::rs')) =
10.15 if lim < 0
10.16 - then (writeln ("make_deriv exceeds " ^ int2str (!lim_deriv) ^
10.17 - "with deriv =\n"); writeln (deriv2str rts); rts)
10.18 + then (tracing ("make_deriv exceeds " ^ int2str (!lim_deriv) ^
10.19 + "with deriv =\n"); tracing (deriv2str rts); rts)
10.20 else
10.21 case r of
10.22 Thm (thmid, tm) =>
10.23 (if not (!trace_rewrite) then () else
10.24 - writeln ("### trying thm '" ^ thmid ^ "'");
10.25 + tracing ("### trying thm '" ^ thmid ^ "'");
10.26 case rewrite_ thy ro erls true tm t of
10.27 NONE => rew_once lim rts t apno rs'
10.28 | SOME (t',a') =>
10.29 (if ! trace_rewrite
10.30 - then writeln ("### rewrites to: "^(term2str t')) else();
10.31 + then tracing ("### rewrites to: "^(term2str t')) else();
10.32 rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs'))
10.33 | Calc (c as (op_,_)) =>
10.34 let val _ = if not (!trace_rewrite) then () else
10.35 - writeln ("### trying calc. '" ^ op_ ^ "'")
10.36 + tracing ("### trying calc. '" ^ op_ ^ "'")
10.37 val t = uminus_to_string t
10.38 in case get_calculation_ thy c t of
10.39 NONE => rew_once lim rts t apno rs'
10.40 | SOME (thmid, tm) =>
10.41 (let val SOME (t',a') = rewrite_ thy ro erls true tm t
10.42 val _ = if not (!trace_rewrite) then () else
10.43 - writeln("### calc. to: " ^ (term2str t'))
10.44 + tracing("### calc. to: " ^ (term2str t'))
10.45 val r' = Thm (thmid, tm)
10.46 in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs'
10.47 end)
10.48 @@ -153,7 +153,7 @@
10.49 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
10.50 | Cal1 (cc as (op_,_)) =>
10.51 (let val _= if !trace_rewrite andalso i < ! depth then
10.52 - writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
10.53 + tracing((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
10.54 val ct = uminus_to_string ct
10.55 in case get_calculation_ thy cc ct of
10.56 NONE => (ct, asm)
10.57 @@ -166,7 +166,7 @@
10.58 else raise error("rewrite_set_, rewrite_ \""^
10.59 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
10.60 val _ = if ! trace_rewrite andalso i < ! depth
10.61 - then writeln((idt"="(i+1))^" cal1. to: "^
10.62 + then tracing((idt"="(i+1))^" cal1. to: "^
10.63 (term2str ((fst o the) pairopt)))
10.64 else()
10.65 in the pairopt end
10.66 @@ -248,7 +248,7 @@
10.67 (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t);
10.68 (*
10.69 val rev_rew = reverse_deriv thy e_rls ;
10.70 - writeln(rtas2str rev_rew);
10.71 + tracing(rtas2str rev_rew);
10.72 *)
10.73
10.74 fun eq_Thm (Thm (id1,_), Thm (id2,_)) = id1 = id2
10.75 @@ -684,7 +684,7 @@
10.76 and finds [] = false
10.77 | finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs;
10.78 in
10.79 - (*writeln ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);*)
10.80 + (*tracing ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);*)
10.81 finds (get_rules rls)
10.82 end;
10.83
10.84 @@ -731,7 +731,7 @@
10.85 | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
10.86 filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls')
10.87 | atomic_appl_tacs _ _ _ _ tac =
10.88 - (writeln ("### atomic_appl_tacs: not impl. for tac = '"^ tac2str tac ^"'");
10.89 + (tracing ("### atomic_appl_tacs: not impl. for tac = '"^ tac2str tac ^"'");
10.90 []);
10.91
10.92
11.1 --- a/src/Tools/isac/Interpret/script.sml Thu Sep 23 14:49:23 2010 +0200
11.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Sep 23 16:38:25 2010 +0200
11.3 @@ -183,7 +183,7 @@
11.4 | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a =
11.5 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
11.6 (*| get_t y (Const ("Let",_) $ e1 $ Abs (_,_,e2)) a =
11.7 - (writeln("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2));
11.8 + (tracing("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2));
11.9 case get_t y e1 a of NONE => get_t y e2 a | la => la)
11.10 | get_t y (Abs (_,_,e)) a = get_t y e a*)
11.11 | get_t y (Const ("Let",_) $ e1 $ Abs (_,_,e2)) a =
11.12 @@ -208,7 +208,7 @@
11.13 | get_t y (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
11.14
11.15 | get_t y x _ =
11.16 - ((*writeln ("### get_t yac: list-expr "^(term2str x));*)
11.17 + ((*tracing ("### get_t yac: list-expr "^(term2str x));*)
11.18 NONE)
11.19 in get_t thy body e_term end;
11.20
11.21 @@ -269,7 +269,7 @@
11.22 thus "NONE" must be set at the end of currying (ill designed anyway)*)
11.23 fun upd_env_opt env (SOME a, v) = upd_env env (a,v)
11.24 | upd_env_opt env (NONE, v) =
11.25 - (writeln("*** upd_env_opt: (NONE,"^(term2str v)^")");env);
11.26 + (tracing("*** upd_env_opt: (NONE,"^(term2str v)^")");env);
11.27
11.28
11.29 type dsc = typ; (*<-> nam..unknow in Descript.thy*)
11.30 @@ -546,7 +546,7 @@
11.31 ("#0 <= #2 + x",[44])];
11.32 > val (bdv,pred) = rep_set thy pt p set;
11.33 val bdv = Free ("x","RealDef.real") : term
11.34 -> writeln (Syntax.string_of_term (thy2ctxt thy) pred);
11.35 +> tracing (Syntax.string_of_term (thy2ctxt thy) pred);
11.36 ((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) &
11.37 #0 <= x ^^^ #2 + #5 * x) &
11.38 #0 <= #2 + x
11.39 @@ -578,9 +578,9 @@
11.40 (case stac of
11.41 (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_)=>
11.42 if thmID = thmID_ then
11.43 - if f = f_ then ((*writeln"3### assod ..Ass";*)Ass (m,f'))
11.44 - else ((*writeln"3### assod ..AssWeak";*)AssWeak(m, f'))
11.45 - else ((*writeln"3### assod ..NotAss";*)NotAss)
11.46 + if f = f_ then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
11.47 + else ((*tracing"3### assod ..AssWeak";*)AssWeak(m, f'))
11.48 + else ((*tracing"3### assod ..NotAss";*)NotAss)
11.49 | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $_$f_)=>
11.50 if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_) then
11.51 if f = f_ then Ass (m,f') else AssWeak (m,f')
11.52 @@ -590,19 +590,19 @@
11.53 | assod pt d (m as Rewrite' (thy,rod,rls,put,(thmID,thm),f,(f',asm))) stac =
11.54 (case stac of
11.55 (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
11.56 - ((*writeln("3### assod: stac = "^
11.57 + ((*tracing("3### assod: stac = "^
11.58 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));
11.59 - writeln("3### assod: f(m)= "^
11.60 + tracing("3### assod: f(m)= "^
11.61 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) f));*)
11.62 if thmID = thmID_ then
11.63 - if f = f_ then ((*writeln"3### assod ..Ass";*)Ass (m,f'))
11.64 - else ((*writeln"### assod ..AssWeak";
11.65 - writeln("### assod: f(m) = "^
11.66 + if f = f_ then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
11.67 + else ((*tracing"### assod ..AssWeak";
11.68 + tracing("### assod: f(m) = "^
11.69 (Sign.string_of_term (sign_of(assoc_thy thy)) f));
11.70 - writeln("### assod: f(stac)= "^
11.71 + tracing("### assod: f(stac)= "^
11.72 (Sign.string_of_term(sign_of(assoc_thy thy))f_))*)
11.73 AssWeak (m,f'))
11.74 - else ((*writeln"3### assod ..NotAss";*)NotAss))
11.75 + else ((*tracing"3### assod ..NotAss";*)NotAss))
11.76 | (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =>
11.77 if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_) then
11.78 if f = f_ then Ass (m,f') else AssWeak (m,f')
11.79 @@ -664,12 +664,12 @@
11.80
11.81 | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
11.82 (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
11.83 - ((*writeln("### assod Check'_elementwise: consts= "^(term2str consts)^
11.84 + ((*tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
11.85 ", consts'= "^(term2str consts'));
11.86 atomty consts; atomty consts';*)
11.87 - if consts = consts' then ((*writeln"### assod Check'_elementwise: Ass";*)
11.88 + if consts = consts' then ((*tracing"### assod Check'_elementwise: Ass";*)
11.89 Ass (m, consts_chkd))
11.90 - else ((*writeln"### assod Check'_elementwise: NotAss";*) NotAss))
11.91 + else ((*tracing"### assod Check'_elementwise: NotAss";*) NotAss))
11.92
11.93 | assod pt _ (m as Or_to_List' (ors, list))
11.94 (Const ("Script.Or'_to'_List",_) $ _) =
11.95 @@ -741,7 +741,7 @@
11.96
11.97 | assod pt d m t =
11.98 (if (!trace_script)
11.99 - then writeln("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"^
11.100 + then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"^
11.101 "@@@ tac_ = "^(tac_2str m))
11.102 else ();
11.103 NotAss);
11.104 @@ -839,7 +839,7 @@
11.105 > val tt = (term_of o the o (parse thy))
11.106 "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";
11.107 > atomty tt;
11.108 -ML> writeln(Syntax.string_of_term (thy2ctxt thy)tt);
11.109 +ML> tracing(Syntax.string_of_term (thy2ctxt thy)tt);
11.110 (Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
11.111 #0 + d_d x (x ^^^ #2 + #3 * x)
11.112
11.113 @@ -978,7 +978,7 @@
11.114 let val stac' = eval_listexpr_ (assoc_thy thy) srls
11.115 (subst_atomic (upd_env_opt E (a,v)) stac)
11.116 in (if (!trace_script)
11.117 - then writeln ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^
11.118 + then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^
11.119 term2str stac'^"'")
11.120 else ();
11.121 (a', STac stac'))
11.122 @@ -987,7 +987,7 @@
11.123 let val lexpr' = eval_listexpr_ (assoc_thy thy) srls
11.124 (subst_atomic (upd_env_opt E (a,v)) lexpr)
11.125 in (if (!trace_script)
11.126 - then writeln("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^
11.127 + then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^
11.128 term2str lexpr'^"'")
11.129 else ();
11.130 (a', Expr lexpr'))
11.131 @@ -1038,24 +1038,24 @@
11.132 (* val (ya, (is as (E,l,a,v,S,b),ss),Const ("Let",_) $ e $ (Abs (id,T,body))) =
11.133 (*1*)(((ts,d),Aundef), ((E,[R],a,v,S,b),[(m,EmptyMout,pt,p,[])]), body);
11.134 *)
11.135 - ((*writeln("### assy Let$e$Abs: is=");
11.136 - writeln(istate2str (ScrState is));*)
11.137 + ((*tracing("### assy Let$e$Abs: is=");
11.138 + tracing(istate2str (ScrState is));*)
11.139 case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
11.140 NasApp ((E',l,a,v,S,bb),ss) =>
11.141 let val id' = mk_Free (id, T);
11.142 val E' = upd_env E' (id', v);
11.143 - (*val _=writeln("### assy Let -> NasApp");*)
11.144 + (*val _=tracing("### assy Let -> NasApp");*)
11.145 in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
11.146 | NasNap (v,E) =>
11.147 let val id' = mk_Free (id, T);
11.148 val E' = upd_env E (id', v);
11.149 - (*val _=writeln("### assy Let -> NasNap");*)
11.150 + (*val _=tracing("### assy Let -> NasNap");*)
11.151 in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
11.152 | ay => ay)
11.153
11.154 | assy (ya as (((thy,srls),_),_)) ((E,l,_,v,S,b),ss)
11.155 (Const ("Script.While",_) $ c $ e $ a) =
11.156 - ((*writeln("### assy While $ c $ e $ a, upd_env= "^
11.157 + ((*tracing("### assy While $ c $ e $ a, upd_env= "^
11.158 (subst2str (upd_env E (a,v))));*)
11.159 if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c)
11.160 then assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e
11.161 @@ -1063,7 +1063,7 @@
11.162
11.163 | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss)
11.164 (Const ("Script.While",_) $ c $ e) =
11.165 - ((*writeln("### assy While, l= "^(loc_2str l));*)
11.166 + ((*tracing("### assy While, l= "^(loc_2str l));*)
11.167 if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
11.168 then assy ya ((E, l@[R], a,v,S,b),ss) e
11.169 else NasNap (v, E))
11.170 @@ -1075,19 +1075,19 @@
11.171 else assy ya ((E, l@[ R], a,v,S,b),ss) e2)
11.172
11.173 | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) =
11.174 - ((*writeln("### assy Try $ e $ a, l= "^(loc_2str l));*)
11.175 + ((*tracing("### assy Try $ e $ a, l= "^(loc_2str l));*)
11.176 case assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e of
11.177 ay => ay)
11.178
11.179 | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
11.180 - ((*writeln("### assy Try $ e, l= "^(loc_2str l));*)
11.181 + ((*tracing("### assy Try $ e, l= "^(loc_2str l));*)
11.182 case assy ya ((E, l@[R], a,v,S,b),ss) e of
11.183 ay => ay)
11.184 (* val (ya, ((E,l,_,v,S,b),ss), (Const ("Script.Seq",_) $e1 $ e2 $ a)) =
11.185 (*2*)(ya, ((E , l@[L,R], a,v,S,b),ss), e);
11.186 *)
11.187 | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2 $ a) =
11.188 - ((*writeln("### assy Seq $e1 $ e2 $ a, E= "^(subst2str E));*)
11.189 + ((*tracing("### assy Seq $e1 $ e2 $ a, E= "^(subst2str E));*)
11.190 case assy ya ((E, l@[L,L,R], SOME a,v,S,b),ss) e1 of
11.191 NasNap (v, E) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
11.192 | NasApp ((E,_,_,v,_,_),ss) =>
11.193 @@ -1136,15 +1136,15 @@
11.194 *)
11.195
11.196 | assy (((thy',sr),d),ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
11.197 - ((*writeln("### assy, m = "^tac_2str m);
11.198 - writeln("### assy, (p,p_) = "^pos'2str (p,p_));
11.199 - writeln("### assy, is= ");
11.200 - writeln(istate2str (ScrState is));*)
11.201 + ((*tracing("### assy, m = "^tac_2str m);
11.202 + tracing("### assy, (p,p_) = "^pos'2str (p,p_));
11.203 + tracing("### assy, is= ");
11.204 + tracing(istate2str (ScrState is));*)
11.205 case handle_leaf "locate" thy' sr E a v t of
11.206 (a', Expr s) =>
11.207 - ((*writeln("### assy: listexpr t= "^(term2str t));
11.208 - writeln("### assy, E= "^(env2str E));
11.209 - writeln("### assy, eval(..)= "^(term2str
11.210 + ((*tracing("### assy: listexpr t= "^(term2str t));
11.211 + tracing("### assy, E= "^(env2str E));
11.212 + tracing("### assy, eval(..)= "^(term2str
11.213 (eval_listexpr_ (assoc_thy thy') sr
11.214 (subst_atomic (upd_env_opt E (a',v)) t))));*)
11.215 NasNap (eval_listexpr_ (assoc_thy thy') sr
11.216 @@ -1152,25 +1152,25 @@
11.217 (* val (_,STac stac) = subst_stacexpr E a v t;
11.218 *)
11.219 | (a', STac stac) =>
11.220 - let (*val _=writeln("### assy, stac = "^term2str stac);*)
11.221 + let (*val _=tracing("### assy, stac = "^term2str stac);*)
11.222 val p' = case p_ of Frm => p | Res => lev_on p
11.223 | _ => raise error ("assy: call by "^
11.224 (pos'2str (p,p_)));
11.225 in case assod pt d m stac of
11.226 Ass (m,v') =>
11.227 - let (*val _=writeln("### assy: Ass ("^tac_2str m^", "^
11.228 + let (*val _=tracing("### assy: Ass ("^tac_2str m^", "^
11.229 term2str v'^")");*)
11.230 val (p'',c',f',pt') = generate1 (assoc_thy thy') m
11.231 (ScrState (E,l,a',v',S,true)) (p',p_) pt;
11.232 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
11.233 | AssWeak (m,v') =>
11.234 - let (*val _=writeln("### assy: Ass Weak("^tac_2str m^", "^
11.235 + let (*val _=tracing("### assy: Ass Weak("^tac_2str m^", "^
11.236 term2str v'^")");*)
11.237 val (p'',c',f',pt') = generate1 (assoc_thy thy') m
11.238 (ScrState (E,l,a',v',S,false)) (p',p_) pt;
11.239 in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
11.240 | NotAss =>
11.241 - ((*writeln("### assy, NotAss");*)
11.242 + ((*tracing("### assy, NotAss");*)
11.243 case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
11.244 AssOnly => (NasNap (v, E))
11.245 | gen => (case applicable_in (p,p_) pt
11.246 @@ -1194,26 +1194,26 @@
11.247 *)
11.248 fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
11.249 (Const ("Let",_) $ _) =
11.250 - let (*val _= writeln("### ass_up1 Let$e: is=")
11.251 - val _= writeln(istate2str (ScrState is))*)
11.252 + let (*val _= tracing("### ass_up1 Let$e: is=")
11.253 + val _= tracing(istate2str (ScrState is))*)
11.254 val l = drop_last l; (*comes from e, goes to Abs*)
11.255 val (Const ("Let",_) $ e $ (Abs (i,T,body))) = go l sc;
11.256 val i = mk_Free (i, T);
11.257 val E = upd_env E (i, v);
11.258 - (*val _=writeln("### ass_up2 Let$e: E="^(subst2str E));*)
11.259 + (*val _=tracing("### ass_up2 Let$e: E="^(subst2str E));*)
11.260 in case assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body of
11.261 Assoc iss => Assoc iss
11.262 | NasApp iss => astep_up ys iss
11.263 | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end
11.264
11.265 | ass_up ys (iss as (is,_)) (Abs (_,_,_)) =
11.266 - ((*writeln("### ass_up Abs: is=");
11.267 - writeln(istate2str (ScrState is));*)
11.268 + ((*tracing("### ass_up Abs: is=");
11.269 + tracing(istate2str (ScrState is));*)
11.270 astep_up ys iss) (*TODO 5.9.00: env ?*)
11.271
11.272 | ass_up ys (iss as (is,_)) (Const ("Let",_) $ e $ (Abs (i,T,b)))=
11.273 - ((*writeln("### ass_up Let $ e $ Abs: is=");
11.274 - writeln(istate2str (ScrState is));*)
11.275 + ((*tracing("### ass_up Let $ e $ Abs: is=");
11.276 + tracing(istate2str (ScrState is));*)
11.277 astep_up ys iss) (*TODO 5.9.00: env ?*)
11.278
11.279 (* val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ $ _)) =
11.280 @@ -1236,8 +1236,8 @@
11.281 *)
11.282 let val up = drop_last l;
11.283 val Const ("Script.Seq",_) $ _ $ e2 = go up sc
11.284 - (*val _= writeln("### ass_up Seq$e: is=")
11.285 - val _= writeln(istate2str (ScrState is))*)
11.286 + (*val _= tracing("### ass_up Seq$e: is=")
11.287 + val _= tracing(istate2str (ScrState is))*)
11.288 in case assy (((y,s),d),Aundef) ((E, up@[R], a,v,S,b),ss) e2 of
11.289 NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
11.290 | NasApp iss => astep_up ysa iss
11.291 @@ -1253,13 +1253,13 @@
11.292 (ys, ((E,up,a,v,S,b),ss), (go up sc));
11.293 *)
11.294 | ass_up ysa iss (Const ("Script.Try",_) $ e) =
11.295 - ((*writeln("### ass_up Try $ e");*)
11.296 + ((*tracing("### ass_up Try $ e");*)
11.297 astep_up ysa iss)
11.298
11.299 | ass_up (ys as (y,s,_,d)) ((E,l,_,v,S,b),ss)
11.300 (*(Const ("Script.While",_) $ c $ e $ a) = WN050930 blind fix*)
11.301 (t as Const ("Script.While",_) $ c $ e $ a) =
11.302 - ((*writeln("### ass_up: While c= "^
11.303 + ((*tracing("### ass_up: While c= "^
11.304 (term2str (subst_atomic (upd_env E (a,v)) c)));*)
11.305 if eval_true_ y s (subst_atomic (upd_env E (a,v)) c)
11.306 then (case assy (((y,s),d),Aundef) ((E, l@[L,R], SOME a,v,S,b),ss) e of
11.307 @@ -1321,7 +1321,7 @@
11.308 if 1 < length l
11.309 then
11.310 let val up = drop_last l;
11.311 - (*val _= writeln("### astep_up: E= "^env2str E);*)
11.312 + (*val _= tracing("### astep_up: E= "^env2str E);*)
11.313 in ass_up ys ((E,up,a,v,S,b),ss) (go up sc) end
11.314 else (NasNap (v, E))
11.315 ;
11.316 @@ -1414,9 +1414,9 @@
11.317 *)
11.318 | locate_gen (ts as (thy',srls)) (m:tac_) ((pt,p):ptree * pos')
11.319 (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b)) =
11.320 - let (*val _= writeln("### locate_gen-----------------: is=");
11.321 - val _= writeln( istate2str (ScrState (E,l,a,v,S,b)));
11.322 - val _= writeln("### locate_gen: l= "^loc_2str l^", p= "^pos'2str p)*)
11.323 + let (*val _= tracing("### locate_gen-----------------: is=");
11.324 + val _= tracing( istate2str (ScrState (E,l,a,v,S,b)));
11.325 + val _= tracing("### locate_gen: l= "^loc_2str l^", p= "^pos'2str p)*)
11.326 val thy = assoc_thy thy';
11.327 in case if l=[] orelse ((*init.in solve..Apply_Method...*)
11.328 (last_elem o fst) p = 0 andalso snd p = Res)
11.329 @@ -1433,7 +1433,7 @@
11.330 (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),
11.331 [(m,EmptyMout,pt,p,[])]) );
11.332 *)
11.333 - ((*writeln("### locate_gen Assoc: p'="^(pos'2str p'));*)
11.334 + ((*tracing("### locate_gen Assoc: p'="^(pos'2str p'));*)
11.335 if bb then Steps (ScrState is, ss)
11.336 else if rew_only ss (*andalso 'not bb'= associated weakly*)
11.337 then let val (po,p_) = p
11.338 @@ -1442,7 +1442,7 @@
11.339 instead take p' from Assoc ?????????????????????????????*)
11.340 val (p'',c'',f'',pt'') =
11.341 generate1 thy m (ScrState is) (po',p_) pt;
11.342 - (*val _=writeln("### locate_gen, aft g1: p''="^(pos'2str p''));*)
11.343 + (*val _=tracing("### locate_gen, aft g1: p''="^(pos'2str p''));*)
11.344 (*drop the intermediate steps !*)
11.345 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
11.346 else Steps (ScrState is, ss))
11.347 @@ -1457,14 +1457,14 @@
11.348 [(m,EmptyMout,pt,p,[])]) body of
11.349 Assoc (iss as (is as (_,_,_,_,_,bb),
11.350 ss as ((m',f',pt',p',c')::_))) =>
11.351 - ((*writeln"4### locate_gen Assoc after Fini";*)
11.352 + ((*tracing"4### locate_gen Assoc after Fini";*)
11.353 if rew_only ss
11.354 then let val(p'',c'',f'',pt'') =
11.355 generate1 thy m (ScrState is) p' pt;
11.356 (*drop the intermediate steps !*)
11.357 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
11.358 else NotLocatable)
11.359 - | _ => ((*writeln ("#### locate_gen: after Fini");*)
11.360 + | _ => ((*tracing ("#### locate_gen: after Fini");*)
11.361 NotLocatable))
11.362 end
11.363 | locate_gen _ m _ (sc,_) is =
11.364 @@ -1511,12 +1511,12 @@
11.365 (thy, ptp, E, up@[R,D], body, a, v);
11.366 appy thy ptp E l t a v;
11.367 *)
11.368 - ((*writeln("### appy Let$e$Abs: is=");
11.369 - writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
11.370 + ((*tracing("### appy Let$e$Abs: is=");
11.371 + tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
11.372 case appy thy ptp E (l@[L,R]) e a v of
11.373 Skip (res, E) =>
11.374 - let (*val _= writeln("### appy Let "^(term2str t));
11.375 - val _= writeln("### appy Let: Skip res ="^(term2str res));*)
11.376 + let (*val _= tracing("### appy Let "^(term2str t));
11.377 + val _= tracing("### appy Let: Skip res ="^(term2str res));*)
11.378 (*val (i',b') = variant_abs (i,T,b); WN.15.5.03
11.379 val i = mk_Free(i',T); WN.15.5.03 *)
11.380 val E' = upd_env E (Free (i,T), res);
11.381 @@ -1525,7 +1525,7 @@
11.382
11.383 | appy (thy as (th,sr)) ptp E l
11.384 (t as Const ("Script.While"(*1*),_) $ c $ e $ a) _ v = (*ohne n. 28.9.00*)
11.385 - ((*writeln("### appy While $ c $ e $ a, upd_env= "^
11.386 + ((*tracing("### appy While $ c $ e $ a, upd_env= "^
11.387 (subst2str (upd_env E (a,v))));*)
11.388 if eval_true_ th sr (subst_atomic (upd_env E (a,v)) c)
11.389 then appy thy ptp E (l@[L,R]) e (SOME a) v
11.390 @@ -1533,32 +1533,32 @@
11.391
11.392 | appy (thy as (th,sr)) ptp E l
11.393 (t as Const ("Script.While"(*2*),_) $ c $ e) a v =(*ohne nachdenken 28.9.00*)
11.394 - ((*writeln("### appy While $ c $ e, upd_env= "^
11.395 + ((*tracing("### appy While $ c $ e, upd_env= "^
11.396 (subst2str (upd_env_opt E (a,v))));*)
11.397 if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
11.398 then appy thy ptp E (l@[R]) e a v
11.399 else Skip (v, E))
11.400
11.401 | appy (thy as (th,sr)) ptp E l (t as Const ("If",_) $ c $ e1 $ e2) a v =
11.402 - ((*writeln("### appy If: t= "^(term2str t));
11.403 - writeln("### appy If: c= "^(term2str(subst_atomic(upd_env_opt E(a,v))c)));
11.404 - writeln("### appy If: thy= "^(fst thy));*)
11.405 + ((*tracing("### appy If: t= "^(term2str t));
11.406 + tracing("### appy If: c= "^(term2str(subst_atomic(upd_env_opt E(a,v))c)));
11.407 + tracing("### appy If: thy= "^(fst thy));*)
11.408 if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
11.409 - then ((*writeln("### appy If: true");*)appy thy ptp E (l@[L,R]) e1 a v)
11.410 - else ((*writeln("### appy If: false");*)appy thy ptp E (l@[ R]) e2 a v))
11.411 + then ((*tracing("### appy If: true");*)appy thy ptp E (l@[L,R]) e1 a v)
11.412 + else ((*tracing("### appy If: false");*)appy thy ptp E (l@[ R]) e2 a v))
11.413 (* val (thy, ptp, E, l, (Const ("Script.Repeat",_) $ e $ a), _, v) =
11.414 (thy, ptp, E, (l@[R]), e, a, v);
11.415 *)
11.416 | appy thy ptp E (*env*) l
11.417 (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v =
11.418 - ((*writeln("### appy Repeat a: ");*)
11.419 + ((*tracing("### appy Repeat a: ");*)
11.420 appy thy ptp E (*env*) (l@[L,R]) e (SOME a) v)
11.421 (* val (thy, ptp, E, l, (Const ("Script.Repeat",_) $ e), _, v) =
11.422 (thy, ptp, E, (l@[R]), e, a, v);
11.423 *)
11.424 | appy thy ptp E (*env*) l
11.425 (Const ("Script.Repeat"(*2*),_) $ e) a v =
11.426 - ((*writeln("3### appy Repeat: a= "^
11.427 + ((*tracing("3### appy Repeat: a= "^
11.428 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) a));*)
11.429 appy thy ptp E (*env*) (l@[R]) e a v)
11.430 (* val (thy, ptp, E, l, (t as Const ("Script.Try",_) $ e $ a), _, v)=
11.431 @@ -1567,7 +1567,7 @@
11.432 | appy thy ptp E l
11.433 (t as Const ("Script.Try",_) $ e $ a) _ v =
11.434 (case appy thy ptp E (l@[L,R]) e (SOME a) v of
11.435 - Napp E => ((*writeln("### appy Try "^
11.436 + Napp E => ((*tracing("### appy Try "^
11.437 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
11.438 Skip (v, E))
11.439 | ay => ay)
11.440 @@ -1579,7 +1579,7 @@
11.441 | appy thy ptp E l
11.442 (t as Const ("Script.Try",_) $ e) a v =
11.443 (case appy thy ptp E (l@[R]) e a v of
11.444 - Napp E => ((*writeln("### appy Try "^
11.445 + Napp E => ((*tracing("### appy Try "^
11.446 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
11.447 Skip (v, E))
11.448 | ay => ay)
11.449 @@ -1604,7 +1604,7 @@
11.450 *)
11.451 | appy thy ptp E l
11.452 (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a) _ v =
11.453 - ((*writeln("### appy Seq $ e1 $ e2 $ a, upd_env= "^
11.454 + ((*tracing("### appy Seq $ e1 $ e2 $ a, upd_env= "^
11.455 (subst2str (upd_env E (a,v))));*)
11.456 case appy thy ptp E (l@[L,L,R]) e1 (SOME a) v of
11.457 Skip (v,E) => appy thy ptp E (l@[L,R]) e2 (SOME a) v
11.458 @@ -1640,8 +1640,8 @@
11.459 *)
11.460 | (a', STac stac) =>
11.461 let
11.462 - (*val _= writeln("### appy t, vor stac2tac_ is=");
11.463 - val _= writeln(istate2str (ScrState (E,l,a',v,Sundef,false)));*)
11.464 + (*val _= tracing("### appy t, vor stac2tac_ is=");
11.465 + val _= tracing(istate2str (ScrState (E,l,a',v,Sundef,false)));*)
11.466 val (m,m') = stac2tac_ pt (assoc_thy th) stac
11.467 in case m of
11.468 Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
11.469 @@ -1649,9 +1649,9 @@
11.470 (* val Appl m' = applicable_in p pt m;
11.471 *)
11.472 Appl m' =>
11.473 - ((*writeln("### appy: Appy");*)
11.474 + ((*tracing("### appy: Appy");*)
11.475 Appy (m', (E,l,a',tac_2res m',Sundef,false)))
11.476 - | _ => ((*writeln("### appy: Napp");*)Napp E))
11.477 + | _ => ((*tracing("### appy: Napp");*)Napp E))
11.478 end);
11.479
11.480
11.481 @@ -1665,8 +1665,8 @@
11.482 *)
11.483 fun nxt_up thy ptp (scr as (Script sc)) E l ay
11.484 (t as Const ("Let",_) $ _) a v = (*comes from let=...*)
11.485 - ((*writeln("### nxt_up1 Let$e: is=");
11.486 - writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
11.487 + ((*tracing("### nxt_up1 Let$e: is=");
11.488 + tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
11.489 if ay = Napp_
11.490 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
11.491 else (*Skip_*)
11.492 @@ -1674,8 +1674,8 @@
11.493 val (Const ("Let",_) $ e $ (Abs (i,T,body))) = go up sc;
11.494 val i = mk_Free (i, T);
11.495 val E = upd_env E (i, v);
11.496 - (*val _= writeln("### nxt_up2 Let$e: is=");
11.497 - val _= writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
11.498 + (*val _= tracing("### nxt_up2 Let$e: is=");
11.499 + val _= tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
11.500 in case appy thy ptp (E) (up@[R,D]) body a v of
11.501 Appy lre => Appy lre
11.502 | Napp E => nstep_up thy ptp scr E up Napp_ a v
11.503 @@ -1683,15 +1683,15 @@
11.504
11.505 | nxt_up thy ptp scr E l ay
11.506 (t as Abs (_,_,_)) a v =
11.507 - ((*writeln("### nxt_up Abs: "^
11.508 + ((*tracing("### nxt_up Abs: "^
11.509 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
11.510 nstep_up thy ptp scr E (*enr*) l ay a v)
11.511
11.512 | nxt_up thy ptp scr E l ay
11.513 (t as Const ("Let",_) $ e $ (Abs (i,T,b))) a v =
11.514 - ((*writeln("### nxt_up Let$e$Abs: is=");
11.515 - writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
11.516 - (*writeln("### nxt_up Let e Abs: "^
11.517 + ((*tracing("### nxt_up Let$e$Abs: is=");
11.518 + tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
11.519 + (*tracing("### nxt_up Let e Abs: "^
11.520 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
11.521 nstep_up thy ptp scr (*upd_env*) E (*a,v)*)
11.522 (*eno,upd_env env (iar,res),iar,res,saf*) l ay a v)
11.523 @@ -1725,9 +1725,9 @@
11.524 (Const ("Script.Repeat"(*1*),T) $ e $ _) a v =
11.525 (case appy thy ptp (*upd_env*) E (*a,v)*) ((l@[L,R]):loc_) e a v of
11.526 Appy lr => Appy lr
11.527 - | Napp E => ((*writeln("### nxt_up Repeat a: ");*)
11.528 + | Napp E => ((*tracing("### nxt_up Repeat a: ");*)
11.529 nstep_up thy ptp scr E l Skip_ a v)
11.530 - | Skip (v,E) => ((*writeln("### nxt_up Repeat: Skip res ="^
11.531 + | Skip (v,E) => ((*tracing("### nxt_up Repeat: Skip res ="^
11.532 (Sign.string_of_term(sign_of (assoc_thy thy)) res'));*)
11.533 nstep_up thy ptp scr E l Skip_ a v))
11.534
11.535 @@ -1735,9 +1735,9 @@
11.536 (Const ("Script.Repeat"(*2*),T) $ e) a v =
11.537 (case appy thy ptp (*upd_env*) E (*a,v)*) ((l@[R]):loc_) e a v of
11.538 Appy lr => Appy lr
11.539 - | Napp E => ((*writeln("### nxt_up Repeat a: ");*)
11.540 + | Napp E => ((*tracing("### nxt_up Repeat a: ");*)
11.541 nstep_up thy ptp scr E l Skip_ a v)
11.542 - | Skip (v,E) => ((*writeln("### nxt_up Repeat: Skip res ="^
11.543 + | Skip (v,E) => ((*tracing("### nxt_up Repeat: Skip res ="^
11.544 (Sign.string_of_term(sign_of (assoc_thy thy)) res'));*)
11.545 nstep_up thy ptp scr E l Skip_ a v))
11.546 (* val (thy, ptp, scr, E, l, _,(t as Const ("Script.Try",_) $ e $ _), a, v) =
11.547 @@ -1746,7 +1746,7 @@
11.548 *)
11.549 | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
11.550 (t as Const ("Script.Try",_) $ e $ _) a v =
11.551 - ((*writeln("### nxt_up Try "^
11.552 + ((*tracing("### nxt_up Try "^
11.553 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
11.554 nstep_up thy ptp scr E l Skip_ a v )
11.555 (* val (thy, ptp, scr, E, l, _,(t as Const ("Script.Try",_) $ e), a, v) =
11.556 @@ -1755,7 +1755,7 @@
11.557 *)
11.558 | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
11.559 (t as Const ("Script.Try"(*2*),_) $ e) a v =
11.560 - ((*writeln("### nxt_up Try "^
11.561 + ((*tracing("### nxt_up Try "^
11.562 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
11.563 nstep_up thy ptp scr E l Skip_ a v)
11.564
11.565 @@ -1809,14 +1809,14 @@
11.566 (thy, ptp, sc, E, l, Skip_, a, v);
11.567 *)
11.568 and nstep_up thy ptp (Script sc) E l ay a v =
11.569 - ((*writeln("### nstep_up from: "^(loc_2str l));
11.570 - writeln("### nstep_up from: "^
11.571 + ((*tracing("### nstep_up from: "^(loc_2str l));
11.572 + tracing("### nstep_up from: "^
11.573 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) (go l sc)));*)
11.574 if 1 < length l
11.575 then
11.576 let
11.577 val up = drop_last l;
11.578 - in ((*writeln("### nstep_up to: "^
11.579 + in ((*tracing("### nstep_up to: "^
11.580 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) (go up sc)));*)
11.581 nxt_up thy ptp (Script sc) E up ay (go up sc) a v ) end
11.582 else (*interpreted to end*)
11.583 @@ -1856,8 +1856,8 @@
11.584 *)
11.585 | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body))
11.586 (ScrState (E,l,a,v,s,b)) =
11.587 - ((*writeln("### next_tac-----------------: E= ");
11.588 - writeln( istate2str (ScrState (E,l,a,v,s,b)));*)
11.589 + ((*tracing("### next_tac-----------------: E= ");
11.590 + tracing( istate2str (ScrState (E,l,a,v,s,b)));*)
11.591 case if l=[] then appy thy ptp E [R] body NONE v
11.592 else nstep_up thy ptp sc E l Skip_ a v of
11.593 Skip (v,_) => (*finished*)
12.1 --- a/src/Tools/isac/Interpret/solve.sml Thu Sep 23 14:49:23 2010 +0200
12.2 +++ b/src/Tools/isac/Interpret/solve.sml Thu Sep 23 16:38:25 2010 +0200
12.3 @@ -185,7 +185,7 @@
12.4 end
12.5
12.6 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) =
12.7 - let (*val _=writeln"###solve Free_Solve";*)
12.8 + let (*val _=tracing"###solve Free_Solve";*)
12.9 val p' = lev_dn_ (p,Res);
12.10 val pt = update_metID pt (par_pblobj pt p) e_metID;
12.11 in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*)
12.12 @@ -195,7 +195,7 @@
12.13 ( m, (pt, pos));
12.14 *)
12.15 | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
12.16 - let (*val _=writeln"###solve Check_Postcond";*)
12.17 + let (*val _=tracing"###solve Check_Postcond";*)
12.18 val pp = par_pblobj pt p
12.19 val asm = (case get_obj g_tac pt p of
12.20 Check_elementwise _ => (*collects and instantiates asms*)
12.21 @@ -205,12 +205,12 @@
12.22 val metID = get_obj g_metID pt pp;
12.23 val {srls=srls,scr=sc,...} = get_met metID;
12.24 val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
12.25 - (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
12.26 - val _= writeln("### solve Check_postc, is= "^(istate2str is));*)
12.27 + (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
12.28 + val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
12.29 val thy' = get_obj g_domID pt pp;
12.30 val thy = assoc_thy thy';
12.31 val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
12.32 - (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*)
12.33 + (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
12.34
12.35 in if pp = [] then
12.36 let val is = ScrState (E,l,a,scval,scsaf,b)
12.37 @@ -227,14 +227,14 @@
12.38 val metID = get_obj g_metID pt ppp;
12.39 val sc = (#scr o get_met) metID;
12.40 val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm);
12.41 - (*val _=writeln("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
12.42 - val _=writeln("### solve Check_postc, is(pt)= "^(istate2str is));
12.43 - val _=writeln("### solve Check_postc, is'= "^
12.44 + (*val _=tracing("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
12.45 + val _=tracing("### solve Check_postc, is(pt)= "^(istate2str is));
12.46 + val _=tracing("### solve Check_postc, is'= "^
12.47 (istate2str (E,l,a,scval,scsaf,b)));*)
12.48 val ((p,p_),ps,f,pt) =
12.49 generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
12.50 (ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt;
12.51 - (*val _=writeln("### solve Check_postc, is(pt')= "^
12.52 + (*val _=tracing("### solve Check_postc, is(pt')= "^
12.53 (istate2str (get_istate pt ([3],Res))));
12.54 val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc
12.55 (ScrState (E,l,a,scval,scsaf,b));*)
12.56 @@ -247,11 +247,11 @@
12.57 ("ok",([(Check_Postcond pI,Check_Postcond'(pI, (scval, map term2str asm))),
12.58 ((pp,Res),(ScrState (E,l,a,scval,scsaf,b)))], (pt,(p,p_))));
12.59 val (_,(pt',p')) = cs';
12.60 - (writeln o istate2str) (get_istate pt' p');
12.61 + (tracing o istate2str) (get_istate pt' p');
12.62 (term2str o fst) (get_obj g_result pt' (fst p'));
12.63 *)
12.64
12.65 -(* writeln(istate2str(get_istate pt (p,p_)));
12.66 +(* tracing(istate2str(get_istate pt (p,p_)));
12.67 *)
12.68 | solve (_,End_Proof'') (pt, (p,p_)) =
12.69 ("end-proof",
12.70 @@ -288,7 +288,7 @@
12.71 let
12.72 val thy' = get_obj g_domID pt (par_pblobj pt p);
12.73 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
12.74 -(*val _= writeln("### solve, before locate_gen p="^(pos'2str(p,p_)));*)
12.75 +(*val _= tracing("### solve, before locate_gen p="^(pos'2str(p,p_)));*)
12.76 val d = e_rls; (*FIXME: canon.simplifier for domain is missing
12.77 8.01: generate from domID?*)
12.78 in case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
12.79 @@ -296,8 +296,8 @@
12.80 (* val Steps (is', ss as (m',f',pt',p',c')::_) =
12.81 locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
12.82 *)
12.83 - let (*val _= writeln("### solve, after locate_gen: is= ")
12.84 - val _= writeln(istate2str is')*)
12.85 + let (*val _= tracing("### solve, after locate_gen: is= ")
12.86 + val _= tracing(istate2str is')*)
12.87 (*val nxt_ =
12.88 case p' of (*change from solve to model subpbl*)
12.89 (_,Pbl) => nxt_model_pbl m' (pt',p')
12.90 @@ -351,7 +351,7 @@
12.91 *)
12.92 (*TODO.WN050913 remove unnecessary code below*)
12.93 | nxt_solv (Check_Postcond' (pI,_)) _ (pt, pos as (p,p_)) =
12.94 - let (*val _=writeln"###solve Check_Postcond";*)
12.95 + let (*val _=tracing"###solve Check_Postcond";*)
12.96 val pp = par_pblobj pt p
12.97 val asm = (case get_obj g_tac pt p of
12.98 Check_elementwise _ => (*collects and instantiates asms*)
12.99 @@ -361,17 +361,17 @@
12.100 val metID = get_obj g_metID pt pp;
12.101 val {srls=srls,scr=sc,...} = get_met metID;
12.102 val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
12.103 - (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
12.104 - val _= writeln("### solve Check_postc, is= "^(istate2str is));*)
12.105 + (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
12.106 + val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
12.107 val thy' = get_obj g_domID pt pp;
12.108 val thy = assoc_thy thy';
12.109 val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
12.110 - (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*)
12.111 + (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
12.112 in if pp = [] then
12.113 let val is = ScrState (E,l,a,scval,scsaf,b)
12.114 val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
12.115 - (*val _= writeln"### nxt_solv2 Apply_Method: stored is =";
12.116 - val _= writeln(istate2str is);*)
12.117 + (*val _= tracing"### nxt_solv2 Apply_Method: stored is =";
12.118 + val _= tracing(istate2str is);*)
12.119 val ((p,p_),ps,f,pt) =
12.120 generate1 thy tac_ is (pp,Res) pt;
12.121 in ([(Check_Postcond pI, tac_, ((pp,Res), is))],ps,(pt, (p,p_))) end
12.122 @@ -386,13 +386,13 @@
12.123 val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm)
12.124 val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
12.125 val is = ScrState (E,l,a,scval,scsaf,b)
12.126 - (*val _= writeln"### nxt_solv3 Apply_Method: stored is =";
12.127 - val _= writeln(istate2str is);*)
12.128 + (*val _= tracing"### nxt_solv3 Apply_Method: stored is =";
12.129 + val _= tracing(istate2str is);*)
12.130 val ((p,p_),ps,f,pt) = generate1 thy tac_ is (pp, Res) pt;
12.131 (*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
12.132 in ([(Check_Postcond pI, tac_, ((pp, Res), is))], ps, (pt, (p,p_))) end
12.133 end
12.134 -(* writeln(istate2str(get_istate pt (p,p_)));
12.135 +(* tracing(istate2str(get_istate pt (p,p_)));
12.136 *)
12.137
12.138 (*.start interpreter and do one rewrite.*)
12.139 @@ -422,8 +422,8 @@
12.140 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
12.141 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
12.142 | _ => pos (*somewhere in script*)
12.143 - (*val _= writeln"### nxt_solv4 Apply_Method: stored is =";
12.144 - val _= writeln(istate2str is);*)
12.145 + (*val _= tracing"### nxt_solv4 Apply_Method: stored is =";
12.146 + val _= tracing(istate2str is);*)
12.147 val (pos',c,_,pt) = generate1 (assoc_thy "Isac.thy") tac_ is pos pt;
12.148 in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
12.149
13.1 --- a/src/Tools/isac/Knowledge/Atools.thy Thu Sep 23 14:49:23 2010 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Thu Sep 23 16:38:25 2010 +0200
13.3 @@ -159,8 +159,8 @@
13.4 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
13.5 fun eval_occurs_in _ "Atools.occurs'_in"
13.6 (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
13.7 - ((*writeln("@@@ eval_occurs_in: v= "^(term2str v));
13.8 - writeln("@@@ eval_occurs_in: t= "^(term2str t));*)
13.9 + ((*tracing("@@@ eval_occurs_in: v= "^(term2str v));
13.10 + tracing("@@@ eval_occurs_in: t= "^(term2str t));*)
13.11 if occurs_in v t
13.12 then SOME ((term2str p) ^ " = True",
13.13 Trueprop $ (mk_equality (p, HOLogic.true_const)))
13.14 @@ -403,7 +403,7 @@
13.15 fun eval_equal (thmid:string) "op =" (t as
13.16 (Const (op0,t0) $ t1 $ t2 )) thy =
13.17 if t1 = t2
13.18 - then ((*writeln"... eval_equal: t1 = t2 --> True";*)
13.19 + then ((*tracing"... eval_equal: t1 = t2 --> True";*)
13.20 SOME (mk_thmid thmid op0
13.21 ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
13.22 ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),
13.23 @@ -411,14 +411,14 @@
13.24 )
13.25 else (case (is_atom t1, is_atom t2) of
13.26 (true, true) =>
13.27 - ((*writeln"... eval_equal: t1<>t2, is_atom t1,t2 --> False";*)
13.28 + ((*tracing"... eval_equal: t1<>t2, is_atom t1,t2 --> False";*)
13.29 SOME (mk_thmid thmid op0
13.30 ("("^(term2str t1)^")") ("("^(term2str t2)^")"),
13.31 Trueprop $ (mk_equality (t, false_as_term)))
13.32 )
13.33 - | _ => ((*writeln"... eval_equal: t1<>t2, NOT is_atom t1,t2 --> go-on";*)
13.34 + | _ => ((*tracing"... eval_equal: t1<>t2, NOT is_atom t1,t2 --> go-on";*)
13.35 NONE))
13.36 - | eval_equal _ _ _ _ = (writeln"... eval_equal: error-exit";
13.37 + | eval_equal _ _ _ _ = (tracing"... eval_equal: error-exit";
13.38 NONE);
13.39 (*
13.40 val t = str2term "x ~= 0";
13.41 @@ -468,7 +468,7 @@
13.42 val prop = Trueprop $ (mk_equality (t, rhs))
13.43 in SOME (mk_thmid thmid op0 n1 n2, prop) end
13.44 end
13.45 - | _ => ((*writeln"@@@ eval_cancel NONE";*)NONE))
13.46 + | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
13.47
13.48 | eval_cancel _ _ _ _ = NONE;
13.49
14.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Sep 23 14:49:23 2010 +0200
14.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Thu Sep 23 16:38:25 2010 +0200
14.3 @@ -135,19 +135,19 @@
14.4 (if pr then
14.5 let
14.6 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
14.7 - val _=writeln("t= f@ts= \""^
14.8 + val _=tracing("t= f@ts= \""^
14.9 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
14.10 (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
14.11 - val _=writeln("u= g@us= \""^
14.12 + val _=tracing("u= g@us= \""^
14.13 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
14.14 (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
14.15 - val _=writeln("size_of_term(t,u)= ("^
14.16 + val _=tracing("size_of_term(t,u)= ("^
14.17 (string_of_int(size_of_term' t))^", "^
14.18 (string_of_int(size_of_term' u))^")");
14.19 - val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
14.20 - val _=writeln("terms_ord(ts,us) = "^
14.21 + val _=tracing("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
14.22 + val _=tracing("terms_ord(ts,us) = "^
14.23 ((pr_ord o terms_ord str false)(ts,us)));
14.24 - val _=writeln("-------");
14.25 + val _=tracing("-------");
14.26 in () end
14.27 else ();
14.28 case int_ord (size_of_term' t, size_of_term' u) of
15.1 --- a/src/Tools/isac/Knowledge/Isac.thy Thu Sep 23 14:49:23 2010 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Isac.thy Thu Sep 23 16:38:25 2010 +0200
15.3 @@ -44,7 +44,7 @@
15.4 elements store_*d in any *.ML are not overwritten.*)
15.5
15.6 thehier := the_hier (!thehier) (collect_thydata ());
15.7 -writeln("----------------------------------\n" ^
15.8 +tracing("----------------------------------\n" ^
15.9 "*** insert: not found ... IS OK : \n" ^
15.10 "comes from fill_parents \n" ^
15.11 "----------------------------------\n");
16.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Sep 23 14:49:23 2010 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Thu Sep 23 16:38:25 2010 +0200
16.3 @@ -191,7 +191,7 @@
16.4 Trueprop $ (mk_equality (p, HOLogic.true_const)))
16.5 else SOME ((term2str p) ^ " = True",
16.6 Trueprop $ (mk_equality (p, HOLogic.false_const)))
16.7 - | eval_is_polyrat_in _ _ _ _ = ((*writeln"### no matches";*) NONE);
16.8 + | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);
16.9
16.10 local
16.11 (*.a 'c is coefficient of v' if v does NOT occur in c.*)
16.12 @@ -450,19 +450,19 @@
16.13 (if pr then
16.14 let
16.15 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
16.16 - val _=writeln("t= f@ts= \""^
16.17 + val _=tracing("t= f@ts= \""^
16.18 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
16.19 (commas(map(Syntax.string_of_term (thy2ctxt thy))ts))^"]\"");
16.20 - val _=writeln("u= g@us= \""^
16.21 + val _=tracing("u= g@us= \""^
16.22 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
16.23 (commas(map(Syntax.string_of_term (thy2ctxt thy))us))^"]\"");
16.24 - val _=writeln("size_of_term(t,u)= ("^
16.25 + val _=tracing("size_of_term(t,u)= ("^
16.26 (string_of_int(size_of_term' t))^", "^
16.27 (string_of_int(size_of_term' u))^")");
16.28 - val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
16.29 - val _=writeln("terms_ord(ts,us) = "^
16.30 + val _=tracing("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
16.31 + val _=tracing("terms_ord(ts,us) = "^
16.32 ((pr_ord o terms_ord str false)(ts,us)));
16.33 - val _=writeln("-------");
16.34 + val _=tracing("-------");
16.35 in () end
16.36 else ();
16.37 case int_ord (size_of_term' t, size_of_term' u) of
17.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Sep 23 14:49:23 2010 +0200
17.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Sep 23 16:38:25 2010 +0200
17.3 @@ -1333,19 +1333,19 @@
17.4 (if pr then
17.5 let
17.6 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
17.7 - val _=writeln("t= f@ts= \""^
17.8 + val _=tracing("t= f@ts= \""^
17.9 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
17.10 (commas(map (Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
17.11 - val _=writeln("u= g@us= \""^
17.12 + val _=tracing("u= g@us= \""^
17.13 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
17.14 (commas(map (Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
17.15 - val _=writeln("size_of_term(t,u)= ("^
17.16 + val _=tracing("size_of_term(t,u)= ("^
17.17 (string_of_int(size_of_term' x t))^", "^
17.18 (string_of_int(size_of_term' x u))^")");
17.19 - val _=writeln("hd_ord(f,g) = "^((pr_ord o (hd_ord x))(f,g)));
17.20 - val _=writeln("terms_ord(ts,us) = "^
17.21 + val _=tracing("hd_ord(f,g) = "^((pr_ord o (hd_ord x))(f,g)));
17.22 + val _=tracing("terms_ord(ts,us) = "^
17.23 ((pr_ord o (terms_ord x) str false)(ts, us)));
17.24 - val _=writeln("-------");
17.25 + val _=tracing("-------");
17.26 in () end
17.27 else ();
17.28 case int_ord (size_of_term' x t, size_of_term' x u) of
17.29 @@ -1364,7 +1364,7 @@
17.30
17.31 fun ord_make_polynomial_in (pr:bool) thy subst tu =
17.32 let
17.33 - (* val _=writeln("*** subs variable is: "^(subst2str subst)); *)
17.34 + (* val _=tracing("*** subs variable is: "^(subst2str subst)); *)
17.35 in
17.36 case subst of
17.37 (_,x)::_ => (term_ord' x pr thy tu = LESS)
18.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Thu Sep 23 14:49:23 2010 +0200
18.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Thu Sep 23 16:38:25 2010 +0200
18.3 @@ -68,7 +68,7 @@
18.4 Trueprop $ (mk_equality (p, HOLogic.true_const)))
18.5 else SOME ((term2str p) ^ " = True",
18.6 Trueprop $ (mk_equality (p, HOLogic.false_const)))
18.7 - | eval_is_ratequation_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
18.8 + | eval_is_ratequation_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
18.9
18.10 (*-------------------------rulse-----------------------*)
18.11 val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
19.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Sep 23 14:49:23 2010 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Sep 23 16:38:25 2010 +0200
19.3 @@ -868,9 +868,9 @@
19.4 end;
19.5
19.6 (*. prints a polynom for (internal use only) .*)
19.7 -fun mv_print_poly([]:mv_poly)=writeln("[]\n")
19.8 - | mv_print_poly((x,y)::[])= writeln("("^Int.toString(x)^","^ints2str(y)^")\n")
19.9 - | mv_print_poly((x,y)::p1) = (writeln("("^Int.toString(x)^","^ints2str(y)^"),");mv_print_poly(p1));
19.10 +fun mv_print_poly([]:mv_poly)=tracing("[]\n")
19.11 + | mv_print_poly((x,y)::[])= tracing("("^Int.toString(x)^","^ints2str(y)^")\n")
19.12 + | mv_print_poly((x,y)::p1) = (tracing("("^Int.toString(x)^","^ints2str(y)^"),");mv_print_poly(p1));
19.13
19.14
19.15 (*. division of two multivariate polynomials .*)
19.16 @@ -2047,13 +2047,13 @@
19.17 let
19.18 val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
19.19 val t11'= Unsynchronized.ref (the(term2poly t11 vars));
19.20 -val _= writeln"### add_fract: done t11"
19.21 +val _= tracing"### add_fract: done t11"
19.22 val t12'= Unsynchronized.ref (the(term2poly t12 vars));
19.23 -val _= writeln"### add_fract: done t12"
19.24 +val _= tracing"### add_fract: done t12"
19.25 val t21'= Unsynchronized.ref (the(term2poly t21 vars));
19.26 -val _= writeln"### add_fract: done t21"
19.27 +val _= tracing"### add_fract: done t21"
19.28 val t22'= Unsynchronized.ref (the(term2poly t22 vars));
19.29 -val _= writeln"### add_fract: done t22"
19.30 +val _= tracing"### add_fract: done t22"
19.31 val den= Unsynchronized.ref [];
19.32 val nom= Unsynchronized.ref [];
19.33 val m1= Unsynchronized.ref [];
19.34 @@ -2062,17 +2062,17 @@
19.35
19.36 (
19.37 den :=sort (mv_geq LEX_) (mv_lcm (!t12') (!t22'));
19.38 -writeln"### add_fract: done sort mv_lcm";
19.39 +tracing"### add_fract: done sort mv_lcm";
19.40 m1 :=sort (mv_geq LEX_) (#1(mv_division(!den,!t12',LEX_)));
19.41 -writeln"### add_fract: done sort mv_division t12";
19.42 +tracing"### add_fract: done sort mv_division t12";
19.43 m2 :=sort (mv_geq LEX_) (#1(mv_division(!den,!t22',LEX_)));
19.44 -writeln"### add_fract: done sort mv_division t22";
19.45 +tracing"### add_fract: done sort mv_division t22";
19.46 nom :=sort (mv_geq LEX_)
19.47 (mv_shorten(mv_add(mv_mul(!t11',!m1,LEX_),
19.48 mv_mul(!t21',!m2,LEX_),
19.49 LEX_),
19.50 LEX_));
19.51 -writeln"### add_fract: done sort mv_add";
19.52 +tracing"### add_fract: done sort mv_add";
19.53 (
19.54 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
19.55 $
19.56 @@ -2128,16 +2128,16 @@
19.57 | add_list_of_fractions (x::y::xs) =
19.58 let
19.59 val (t1a,rest1)=direct_cancel(x);
19.60 -val _= writeln"### add_list_of_fractions xs: has done direct_cancel(x)";
19.61 +val _= tracing"### add_list_of_fractions xs: has done direct_cancel(x)";
19.62 val (t2a,rest2)=direct_cancel(y);
19.63 -val _= writeln"### add_list_of_fractions xs: has done direct_cancel(y)";
19.64 +val _= tracing"### add_list_of_fractions xs: has done direct_cancel(y)";
19.65 val (t3a,rest3)=(add_list_of_fractions (add_fract(t1a,t2a)::xs));
19.66 -val _= writeln"### add_list_of_fractions xs: has done add_list_of_fraction xs";
19.67 +val _= tracing"### add_list_of_fractions xs: has done add_list_of_fraction xs";
19.68 val (t4a,rest4)=direct_cancel(t3a);
19.69 -val _= writeln"### add_list_of_fractions xs: has done direct_cancel(t3a)";
19.70 +val _= tracing"### add_list_of_fractions xs: has done direct_cancel(t3a)";
19.71 val rest=rest1 union rest2 union rest3 union rest4;
19.72 in
19.73 - (writeln"### add_list_of_fractions in";
19.74 + (tracing"### add_list_of_fractions in";
19.75 (
19.76 (t4a,rest)
19.77 )
19.78 @@ -2714,7 +2714,7 @@
19.79 (*.transforms sums of at least 2 fractions [3] to
19.80 sums with the least common multiple as nominator.*)
19.81 fun common_nominator_p_ (thy:theory) t =
19.82 -((*writeln("### common_nominator_p_ called");*)
19.83 +((*tracing("### common_nominator_p_ called");*)
19.84 SOME (step_add_list_of_fractions(term2list(t))) handle _ => NONE
19.85 );
19.86 fun common_nominator_ (thy:theory) t =
19.87 @@ -2728,7 +2728,7 @@
19.88 term list) (*casual assumptions in normalform [2] WN0210???SK *)
19.89 option (*NONE: the function is not applicable *).*)
19.90 fun add_fraction_p_ (thy:theory) t =
19.91 -(writeln("### add_fraction_p_ called");
19.92 +(tracing("### add_fraction_p_ called");
19.93 (let val ts = term2list t
19.94 in if 1 < length ts
19.95 then SOME (add_list_of_fractions ts)
19.96 @@ -2942,10 +2942,10 @@
19.97 rewrite_ thy ro eval_rls true (thm_of_thm r) t;
19.98 in case ropt of
19.99 SOME ta => [(r, ta)]
19.100 - | NONE => (writeln("### locate_rule: rewrite "^
19.101 + | NONE => (tracing("### locate_rule: rewrite "^
19.102 (id_of_thm r)^" "^(term2str t)^" = NONE");
19.103 []) end
19.104 - else (writeln("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
19.105 + else (tracing("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
19.106 | locate_rule _ _ _ _ _ _ =
19.107 raise error ("locate_rule: doesnt match rev-sets in istate");
19.108
19.109 @@ -3049,10 +3049,10 @@
19.110 rewrite_ thy ro eval_rls true (thm_of_thm r) t;
19.111 in case ropt of
19.112 SOME ta => [(r, ta)]
19.113 - | NONE => (writeln("### locate_rule: rewrite "^
19.114 + | NONE => (tracing("### locate_rule: rewrite "^
19.115 (id_of_thm r)^" "^(term2str t)^" = NONE");
19.116 []) end
19.117 - else (writeln("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
19.118 + else (tracing("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
19.119 | locate_rule _ _ _ _ _ _ =
19.120 raise error ("locate_rule: doesnt match rev-sets in istate");
19.121
19.122 @@ -3166,10 +3166,10 @@
19.123 rewrite_ thy ro eval_rls true (thm_of_thm r) t;
19.124 in case ropt of
19.125 SOME ta => [(r, ta)]
19.126 - | NONE => (writeln("### locate_rule: rewrite "^
19.127 + | NONE => (tracing("### locate_rule: rewrite "^
19.128 (id_of_thm r)^" "^(term2str t)^" = NONE");
19.129 []) end
19.130 - else (writeln("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
19.131 + else (tracing("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
19.132 | locate_rule _ _ _ _ _ _ =
19.133 raise error ("locate_rule: doesnt match rev-sets in istate");
19.134
19.135 @@ -3310,10 +3310,10 @@
19.136 rewrite_ thy ro eval_rls true (thm_of_thm r) t;
19.137 in case ropt of
19.138 SOME ta => [(r, ta)]
19.139 - | NONE => (writeln("### locate_rule: rewrite "^
19.140 + | NONE => (tracing("### locate_rule: rewrite "^
19.141 (id_of_thm r)^" "^(term2str t)^" = NONE");
19.142 []) end
19.143 - else (writeln("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
19.144 + else (tracing("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
19.145 | locate_rule _ _ _ _ _ _ =
19.146 raise error ("locate_rule: doesnt match rev-sets in istate");
19.147
20.1 --- a/src/Tools/isac/Knowledge/Root.thy Thu Sep 23 14:49:23 2010 +0200
20.2 +++ b/src/Tools/isac/Knowledge/Root.thy Thu Sep 23 16:38:25 2010 +0200
20.3 @@ -114,19 +114,19 @@
20.4 (if pr then
20.5 let
20.6 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
20.7 - val _=writeln("t= f@ts= \""^
20.8 + val _=tracing("t= f@ts= \""^
20.9 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
20.10 (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
20.11 - val _=writeln("u= g@us= \""^
20.12 + val _=tracing("u= g@us= \""^
20.13 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
20.14 (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
20.15 - val _=writeln("size_of_term(t,u)= ("^
20.16 + val _=tracing("size_of_term(t,u)= ("^
20.17 (string_of_int(size_of_term' t))^", "^
20.18 (string_of_int(size_of_term' u))^")");
20.19 - val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
20.20 - val _=writeln("terms_ord(ts,us) = "^
20.21 + val _=tracing("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
20.22 + val _=tracing("terms_ord(ts,us) = "^
20.23 ((pr_ord o terms_ord str false)(ts,us)));
20.24 - val _=writeln("-------");
20.25 + val _=tracing("-------");
20.26 in () end
20.27 else ();
20.28 case int_ord (size_of_term' t, size_of_term' u) of
21.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Sep 23 14:49:23 2010 +0200
21.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Thu Sep 23 16:38:25 2010 +0200
21.3 @@ -175,7 +175,7 @@
21.4 Trueprop $ (mk_equality (p, HOLogic.true_const)))
21.5 else SOME ((term2str p) ^ " = True",
21.6 Trueprop $ (mk_equality (p, HOLogic.false_const)))
21.7 - | eval_is_rootTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
21.8 + | eval_is_rootTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
21.9
21.10 fun eval_is_sqrtTerm_in _ _
21.11 (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _ =
21.12 @@ -184,7 +184,7 @@
21.13 Trueprop $ (mk_equality (p, HOLogic.true_const)))
21.14 else SOME ((term2str p) ^ " = True",
21.15 Trueprop $ (mk_equality (p, HOLogic.false_const)))
21.16 - | eval_is_sqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
21.17 + | eval_is_sqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
21.18
21.19 fun eval_is_normSqrtTerm_in _ _
21.20 (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _ =
21.21 @@ -193,7 +193,7 @@
21.22 Trueprop $ (mk_equality (p, HOLogic.true_const)))
21.23 else SOME ((term2str p) ^ " = True",
21.24 Trueprop $ (mk_equality (p, HOLogic.false_const)))
21.25 - | eval_is_normSqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
21.26 + | eval_is_normSqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
21.27
21.28 (*-------------------------rulse-------------------------*)
21.29 val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
22.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Thu Sep 23 14:49:23 2010 +0200
22.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Thu Sep 23 16:38:25 2010 +0200
22.3 @@ -67,7 +67,7 @@
22.4 Trueprop $ (mk_equality (p, HOLogic.true_const)))
22.5 else SOME ((term2str p) ^ " = True",
22.6 Trueprop $ (mk_equality (p, HOLogic.false_const)))
22.7 - | eval_is_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
22.8 + | eval_is_rootRatAddTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
22.9 *}
22.10 ML {*
22.11 (*-------------------------rulse-------------------------*)
23.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Sep 23 14:49:23 2010 +0200
23.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Sep 23 16:38:25 2010 +0200
23.3 @@ -1212,19 +1212,19 @@
23.4 (if pr then
23.5 let
23.6 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
23.7 - val _=writeln("t= f@ts= " ^ "" ^
23.8 + val _=tracing("t= f@ts= " ^ "" ^
23.9 ((Syntax.string_of_term (thy2ctxt thy)) f)^ "\" @ " ^ "[" ^
23.10 (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]\"");
23.11 - val _=writeln("u= g@us= " ^ "" ^
23.12 + val _=tracing("u= g@us= " ^ "" ^
23.13 ((Syntax.string_of_term (thy2ctxt thy)) g) ^ "\" @ " ^ "[" ^
23.14 (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
23.15 - val _=writeln("size_of_term(t,u)= ("^
23.16 + val _=tracing("size_of_term(t,u)= ("^
23.17 (string_of_int(size_of_term' t)) ^ ", " ^
23.18 (string_of_int(size_of_term' u)) ^ ")");
23.19 - val _=writeln("hd_ord(f,g) = " ^ ((pr_ord o hd_ord)(f,g)));
23.20 - val _=writeln("terms_ord(ts,us) = " ^
23.21 + val _=tracing("hd_ord(f,g) = " ^ ((pr_ord o hd_ord)(f,g)));
23.22 + val _=tracing("terms_ord(ts,us) = " ^
23.23 ((pr_ord o terms_ord str false)(ts,us)));
23.24 - val _=writeln("-------");
23.25 + val _=tracing("-------");
23.26 in () end
23.27 else ();
23.28 case int_ord (size_of_term' t, size_of_term' u) of
24.1 --- a/src/Tools/isac/ProgLang/Tools.sml Thu Sep 23 14:49:23 2010 +0200
24.2 +++ b/src/Tools/isac/ProgLang/Tools.sml Thu Sep 23 16:38:25 2010 +0200
24.3 @@ -71,7 +71,7 @@
24.4
24.5 fun eval_Nth (thmid:string) (op_:string) (t as
24.6 (Const (op0,t0) $ t1 $ t2 )) thy =
24.7 -(writeln"@@@ eval_Nth";
24.8 +(tracing"@@@ eval_Nth";
24.9 if is_num t1 andalso is_list t2
24.10 then
24.11 let
25.1 --- a/src/Tools/isac/ProgLang/Tools.thy Thu Sep 23 14:49:23 2010 +0200
25.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Thu Sep 23 16:38:25 2010 +0200
25.3 @@ -56,12 +56,12 @@
25.4 val EmptyList = (term_of o the o (parse @{theory})) "[]::bool list";
25.5
25.6 (*+ for Or_to_List +*)
25.7 -fun or2list (Const ("True",_)) = (writeln"### or2list True";UniversalList)
25.8 - | or2list (Const ("False",_)) = (writeln"### or2list False";EmptyList)
25.9 +fun or2list (Const ("True",_)) = (tracing"### or2list True";UniversalList)
25.10 + | or2list (Const ("False",_)) = (tracing"### or2list False";EmptyList)
25.11 | or2list (t as Const ("op =",_) $ _ $ _) =
25.12 - (writeln"### or2list _ = _";list2isalist bool [t])
25.13 + (tracing"### or2list _ = _";list2isalist bool [t])
25.14 | or2list ors =
25.15 - (writeln"### or2list _ | _";
25.16 + (tracing"### or2list _ | _";
25.17 let fun get ls (Const ("op |",_) $ o1 $ o2) =
25.18 case o2 of
25.19 Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2
26.1 --- a/src/Tools/isac/ProgLang/calculate.sml Thu Sep 23 14:49:23 2010 +0200
26.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Thu Sep 23 16:38:25 2010 +0200
26.3 @@ -84,15 +84,15 @@
26.4 (* val (thy, op_, ef, (t as (Const(op0,_) $ t1 $ t2))) =
26.5 (thy, op_, eval_fn, ct);
26.6 *)
26.7 - ((*writeln("1.. get_pair: binop = "^op_);*)
26.8 + ((*tracing("1.. get_pair: binop = "^op_);*)
26.9 if op_ = op0 then
26.10 let val popt = ef op_ t thy
26.11 - (*val _ = writeln("2.. get_pair: "^term2str t^" -> "^popt2str popt)*)
26.12 + (*val _ = tracing("2.. get_pair: "^term2str t^" -> "^popt2str popt)*)
26.13 in case popt of
26.14 SOME (id,_) => popt
26.15 | NONE =>
26.16 let val popt = get_pair thy op_ ef t1
26.17 - (*val _ = writeln("3.. get_pair: "^term2str t1^
26.18 + (*val _ = tracing("3.. get_pair: "^term2str t1^
26.19 " -> "^popt2str popt)*)
26.20 in case popt of
26.21 SOME (id,_) => popt
26.22 @@ -101,15 +101,15 @@
26.23 end
26.24 else (*search subterms*)
26.25 let val popt = get_pair thy op_ ef t1
26.26 - (*val _ = writeln("4.. get_pair: "^term2str t^" -> "^popt2str popt)*)
26.27 + (*val _ = tracing("4.. get_pair: "^term2str t^" -> "^popt2str popt)*)
26.28 in case popt of
26.29 SOME (id,_) => popt
26.30 | NONE => get_pair thy op_ ef t2
26.31 end)
26.32 | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2 $ t3)) =(* trinary funs*)
26.33 - ((*writeln("### get_pair 4a: t= "^term2str t);
26.34 - writeln("### get_pair 4a: op_= "^op_);
26.35 - writeln("### get_pair 4a: op0= "^op0);*)
26.36 + ((*tracing("### get_pair 4a: t= "^term2str t);
26.37 + tracing("### get_pair 4a: op_= "^op_);
26.38 + tracing("### get_pair 4a: op0= "^op0);*)
26.39 if op_ = op0 then
26.40 case ef op_ t thy of
26.41 SOME tt => SOME tt
26.42 @@ -127,12 +127,12 @@
26.43 | get_pair thy op_ ef (Bound _) = NONE
26.44 | get_pair thy op_ ef (Abs(a,T,body)) = get_pair thy op_ ef body
26.45 | get_pair thy op_ ef (t1$t2) =
26.46 - let(*val _= writeln("5.. get_pair t1 $ t2: "^term2str t1^"
26.47 + let(*val _= tracing("5.. get_pair t1 $ t2: "^term2str t1^"
26.48 $ "^term2str t2)*)
26.49 val popt = get_pair thy op_ ef t1
26.50 in case popt of
26.51 SOME _ => popt
26.52 - | NONE => ((*writeln"### get_pair: t1 $ t2 -> NONE";*)
26.53 + | NONE => ((*tracing"### get_pair: t1 $ t2 -> NONE";*)
26.54 get_pair thy op_ ef t2)
26.55 end;
26.56 (*
26.57 @@ -225,12 +225,12 @@
26.58 (thy, (the (assoc(!calclist',"order_system"))), t);
26.59 *)
26.60 case get_pair thy op_ eval_fn ct of
26.61 - NONE => ((*writeln("@@@ get_calculation: NONE, op_="^op_);
26.62 - writeln("@@@ get_calculation: ct= ");atomty ct;*)
26.63 + NONE => ((*tracing("@@@ get_calculation: NONE, op_="^op_);
26.64 + tracing("@@@ get_calculation: ct= ");atomty ct;*)
26.65 NONE)
26.66 | SOME (thmid,t) =>
26.67 - ((*writeln("@@@ get_calculation: NONE, op_="^op_);
26.68 - writeln("@@@ get_calculation: ct= ");atomty ct;*)
26.69 + ((*tracing("@@@ get_calculation: NONE, op_="^op_);
26.70 + tracing("@@@ get_calculation: ct= ");atomty ct;*)
26.71 SOME (thmid, (make_thm o (cterm_of thy)) t));
26.72 (*
26.73 > val ct = (the o (parse thy)) "#9 is_const";
26.74 @@ -358,11 +358,11 @@
26.75 (read_instantiate subs thm) handle _ => thm)
26.76 | inst_thm' _ calc = calc;
26.77 fun inst_thm' (subs as (bdv,_)::_) (Thm (id, thm)) =
26.78 - Thm (id, (writeln("@@@ inst_thm': thm= "^(string_of_thmI thm));
26.79 + Thm (id, (tracing("@@@ inst_thm': thm= "^(string_of_thmI thm));
26.80 if bdv mem (vars_str o #prop o rep_thm) thm
26.81 - then (writeln("@@@ inst_thm': read_instantiate, thm="^((string_of_thmI thm)));
26.82 + then (tracing("@@@ inst_thm': read_instantiate, thm="^((string_of_thmI thm)));
26.83 read_instantiate subs thm)
26.84 - else (writeln("@@@ inst_thm': not mem.. "^bdv);
26.85 + else (tracing("@@@ inst_thm': not mem.. "^bdv);
26.86 thm)))
26.87 | inst_thm' _ calc = calc;
26.88
27.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Thu Sep 23 14:49:23 2010 +0200
27.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Thu Sep 23 16:38:25 2010 +0200
27.3 @@ -14,7 +14,7 @@
27.4 (thy, 1, []:(Term.term * Term.term) list, rew_ord, erls, bool,thm,term);
27.5 *)
27.6 fun rewrite__ thy i bdv tless rls put_asm thm ct =
27.7 - ((*writeln ("@@@ r..te__ begin: t = "^(term2str ct));*)
27.8 + ((*tracing ("@@@ r..te__ begin: t = "^(term2str ct));*)
27.9 let
27.10 val (t',asms,lrd,rew) =
27.11 rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
27.12 @@ -39,7 +39,7 @@
27.13 ((inst_bdv bdv) o norm o #prop o rep_thm) thm, ct);
27.14 *)
27.15 and rew_sub thy i bdv tless rls put_asm lrd r t =
27.16 - ((*writeln ("@@@ rew_sub begin: t = "^(term2str t));*)
27.17 + ((*tracing ("@@@ rew_sub begin: t = "^(term2str t));*)
27.18 let (* copy from Pure/thm.ML: fun rewritec *)
27.19 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
27.20 o Logic.strip_imp_concl) r;
27.21 @@ -48,33 +48,33 @@
27.22 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
27.23 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
27.24 o Logic.strip_imp_concl) r';
27.25 - (*val _= writeln("@@@ rew_sub match: t'= "^(term2str t'));*)
27.26 + (*val _= tracing("@@@ rew_sub match: t'= "^(term2str t'));*)
27.27 val _= if ! trace_rewrite andalso i < ! depth andalso p' <> []
27.28 - then writeln((idt"#"(i+1))^" eval asms: "^(term2str r')) else();
27.29 + then tracing((idt"#"(i+1))^" eval asms: "^(term2str r')) else();
27.30 val (t'',p'') = (*conditional rewriting*)
27.31 let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls
27.32 in if nofalse
27.33 then (if ! trace_rewrite andalso i < ! depth andalso p' <> []
27.34 - then writeln((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
27.35 + then tracing((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
27.36 " stored: "^(terms2str simpl_p'))
27.37 else(); (t',simpl_p')) (* + unconditional rew.*)
27.38 else
27.39 (if ! trace_rewrite andalso i < ! depth
27.40 - then writeln((idt"#"(i+1))^" asms false: "^(terms2str p'))
27.41 + then tracing((idt"#"(i+1))^" asms false: "^(terms2str p'))
27.42 else(); raise STOP_REW_SUB (*dont go into subterms of cond*))
27.43 end
27.44 in if perm lhs rhs andalso not (tless bdv (t',t)) (*ordered rewriting*)
27.45 then (if ! trace_rewrite andalso i < ! depth
27.46 - then writeln((idt"#"i)^" not: \""^
27.47 + then tracing((idt"#"i)^" not: \""^
27.48 (term2str t)^"\" > \""^
27.49 (term2str t')^"\"") else ();
27.50 raise NO_REWRITE )
27.51 - else ((*writeln("##@ rew_sub: (t''= "^(term2str t'')^
27.52 + else ((*tracing("##@ rew_sub: (t''= "^(term2str t'')^
27.53 ", p'' ="^(terms2str p'')^", true)");*)
27.54 (t'',p'',[],true))
27.55 end
27.56 ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) =>
27.57 - ((*writeln ("@@@ rew_sub gosub: t = "^(term2str t));*)
27.58 + ((*tracing ("@@@ rew_sub gosub: t = "^(term2str t));*)
27.59 case t of
27.60 Const(s,T) => (Const(s,T),[],lrd,false)
27.61 | Free(s,T) => (Free(s,T),[],lrd,false)
27.62 @@ -120,7 +120,7 @@
27.63 raise error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
27.64 | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
27.65 let val _= if ! trace_rewrite andalso i < ! depth
27.66 - then writeln ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
27.67 + then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
27.68 (term2str t)) else ()
27.69 val (t', asm, rew) = app_rev thy (i+1) rrls t
27.70 in if rew then SOME (t', distinct asm)
27.71 @@ -141,20 +141,20 @@
27.72 case rul of
27.73 Thm (thmid, thm) =>
27.74 (if !trace_rewrite andalso i < ! depth
27.75 - then writeln((idt"#"(i+1))^" try thm: "^thmid) else ();
27.76 + then tracing((idt"#"(i+1))^" try thm: "^thmid) else ();
27.77 case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
27.78 ((#erls o rep_rls) rls) put_asm thm ct of
27.79 NONE => rew_once ruls asm ct apno thms
27.80 | SOME (ct',asm') => (if ! trace_rewrite andalso i < ! depth
27.81 - then writeln((idt"="(i+1))^" rewrites to: "^
27.82 + then tracing((idt"="(i+1))^" rewrites to: "^
27.83 (term2str ct')) else ();
27.84 rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
27.85 | Calc (cc as (op_,_)) =>
27.86 (let val _= if !trace_rewrite andalso i < ! depth then
27.87 - writeln((idt"#"(i+1))^" try calc: "^op_^"'") else ();
27.88 + tracing((idt"#"(i+1))^" try calc: "^op_^"'") else ();
27.89 val ct = uminus_to_string ct
27.90 in case get_calculation_ thy cc ct of
27.91 - NONE => ((*writeln "@@@ rewrite__set_: get_calculation_-> NONE";*)
27.92 + NONE => ((*tracing "@@@ rewrite__set_: get_calculation_-> NONE";*)
27.93 rew_once ruls asm ct apno thms)
27.94 | SOME (thmid, thm') =>
27.95 let
27.96 @@ -165,7 +165,7 @@
27.97 else raise error("rewrite_set_, rewrite_ \""^
27.98 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
27.99 val _ = if ! trace_rewrite andalso i < ! depth
27.100 - then writeln((idt"="(i+1))^" calc. to: "^
27.101 + then tracing((idt"="(i+1))^" calc. to: "^
27.102 (term2str ((fst o the) pairopt)))
27.103 else()
27.104 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end
27.105 @@ -174,7 +174,7 @@
27.106 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
27.107 | Cal1 (cc as (op_,_)) =>
27.108 (let val _= if !trace_rewrite andalso i < ! depth then
27.109 - writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
27.110 + tracing((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
27.111 val ct = uminus_to_string ct
27.112 in case get_calculation1_ thy cc ct of
27.113 NONE => (ct, asm)
27.114 @@ -187,7 +187,7 @@
27.115 else raise error("rewrite_set_, rewrite_ \""^
27.116 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
27.117 val _ = if ! trace_rewrite andalso i < ! depth
27.118 - then writeln((idt"="(i+1))^" cal1. to: "^
27.119 + then tracing((idt"="(i+1))^" cal1. to: "^
27.120 (term2str ((fst o the) pairopt)))
27.121 else()
27.122 in the pairopt end
27.123 @@ -200,7 +200,7 @@
27.124
27.125 val ruls = (#rules o rep_rls) rls;
27.126 val _= if ! trace_rewrite andalso i < ! depth
27.127 - then writeln ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^
27.128 + then tracing ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^
27.129 (term2str ct)) else ()
27.130 val (ct',asm') = rew_once ruls [] ct Noap ruls;
27.131 in if ct = ct' then NONE else SOME (ct', distinct asm') end
27.132 @@ -226,7 +226,7 @@
27.133 (*.apply the normal_form of a rev-set.*)
27.134 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
27.135 if chk_prepat thy erls prepat t
27.136 - then ((*writeln("### app_rev': t = "^(term2str t));*)
27.137 + then ((*tracing("### app_rev': t = "^(term2str t));*)
27.138 normal_form t)
27.139 else NONE;
27.140
27.141 @@ -236,7 +236,7 @@
27.142 | NONE => app_sub thy i rrls t
27.143 end
27.144 and app_sub thy i rrls t =
27.145 - ((*writeln("### app_sub: subterm = "^(term2str t));*)
27.146 + ((*tracing("### app_sub: subterm = "^(term2str t));*)
27.147 case t of
27.148 Const (s, T) => (Const(s, T), [], false)
27.149 | Free (s, T) => (Free(s, T), [], false)
27.150 @@ -300,7 +300,7 @@
27.151 *)
27.152 (*.rewrite using a list of terms.*)
27.153 fun rewrite_terms_ thy ord erls subte t =
27.154 - let (*val _=writeln("### rewrite_terms_ subte= '"^terms2str subte^"' ..."^
27.155 + let (*val _=tracing("### rewrite_terms_ subte= '"^terms2str subte^"' ..."^
27.156 term_detail2str (hd subte)^
27.157 "### rewrite_terms_ t= '"^term2str t^"' ..."^
27.158 term_detail2str t);*)
27.159 @@ -310,13 +310,13 @@
27.160 rew_ (t', asm') (r::rs) t;
27.161 *)
27.162 | rew_ (t', asm') (rules as r::rs) t =
27.163 - let val _ = writeln("rew_ "^term2str t);
27.164 + let val _ = tracing("rew_ "^term2str t);
27.165 val (t'', asm'', lrd, rew) =
27.166 rew_sub thy 1 [] ord erls false [] r t
27.167 in if rew
27.168 - then (writeln("true rew_ "^term2str t'');
27.169 + then (tracing("true rew_ "^term2str t'');
27.170 rew_ (t'', asm' @ asm'') rules t'')
27.171 - else (writeln("false rew_ "^term2str t'');
27.172 + else (tracing("false rew_ "^term2str t'');
27.173 rew_ (t', asm') rs t')
27.174 end
27.175 val (t'', asm'') = rew_ (e_term, []) subte t
27.176 @@ -347,8 +347,8 @@
27.177
27.178
27.179 (* for test-printouts:
27.180 -val _ = writeln("in rew_sub : "^( Syntax.string_of_term (thy2ctxt thy) t))
27.181 -val _ = writeln("in eval_true: prems= "^(commas (map (Syntax.string_of_term (thy2ctxt thy)) prems')))
27.182 +val _ = tracing("in rew_sub : "^( Syntax.string_of_term (thy2ctxt thy) t))
27.183 +val _ = tracing("in eval_true: prems= "^(commas (map (Syntax.string_of_term (thy2ctxt thy)) prems')))
27.184 *)
27.185
27.186
28.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Thu Sep 23 14:49:23 2010 +0200
28.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Thu Sep 23 16:38:25 2010 +0200
28.3 @@ -174,7 +174,7 @@
28.4 (*update environment; t <> empty if coming from listexpr*)
28.5 fun upd_env (env:env) (v,t) =
28.6 let val env' = if t = e_term then env else overwrite (env,(v,t));
28.7 - (*val _= writeln("### upd_env: = "^(subst2str env'));*)
28.8 + (*val _= tracing("### upd_env: = "^(subst2str env'));*)
28.9 in env' end;
28.10
28.11 (*.substitute the scripts environment in a leaf of the scripts parse-tree
28.12 @@ -284,7 +284,7 @@
28.13 in (distinct o (scan [])) body end;
28.14 (*sc = Solve_root_equation ...
28.15 > val ts = stacpbls sc;
28.16 -> writeln (terms2str thy ts);
28.17 +> tracing (terms2str thy ts);
28.18 ["Rewrite square_equation_left True e_",
28.19 "Rewrite_Set SqRoot_simplify False e_",
28.20 "Rewrite_Set rearrange_assoc False e_",
28.21 @@ -424,7 +424,7 @@
28.22 val rules = (#rules o rep_rls) isolate_root;
28.23 val rs = map (rule2stac calclist) rules;
28.24 val tt = @@ rs;
28.25 - atomt tt; writeln (term2str tt);
28.26 + atomt tt; tracing (term2str tt);
28.27 *)
28.28
28.29 val contains_bdv = (not o null o (filter is_bdv) o ids2str o #prop o rep_thm);
28.30 @@ -485,7 +485,7 @@
28.31 raise error ("prep_rls not required for Rrls \""^id^"\"");
28.32 (*
28.33 val Script sc = (#scr o rep_rls o prep_rls) isolate_root;
28.34 - (writeln o term2str) sc;
28.35 + (tracing o term2str) sc;
28.36 val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv;
28.37 - (writeln o term2str) sc;
28.38 + (tracing o term2str) sc;
28.39 *)
29.1 --- a/src/Tools/isac/ProgLang/term.sml Thu Sep 23 14:49:23 2010 +0200
29.2 +++ b/src/Tools/isac/ProgLang/term.sml Thu Sep 23 16:38:25 2010 +0200
29.3 @@ -37,7 +37,7 @@
29.4 ("\n*** "^indent n^"]")
29.5 | atol n (T::Ts) = (ato n T ^ atol n Ts)
29.6 (*in print (ato 0 t ^ "\n") end; TODO TUM10*)
29.7 -in writeln (ato 0 t) end;
29.8 +in tracing (ato 0 t) end;
29.9 (*
29.10 > val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
29.11 > atomtyp T;
29.12 @@ -88,7 +88,7 @@
29.13 | ato (Abs (a, _, body)) n =
29.14 "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1)
29.15 | ato (f $ t) n = (ato f n ^ ato t (n + 1))
29.16 - in writeln ("\n*** -------------" ^ ato t 0 ^ "\n***") end;
29.17 + in tracing ("\n*** -------------" ^ ato t 0 ^ "\n***") end;
29.18
29.19 fun term_detail2str t =
29.20 let fun ato (Const (a, T)) n =
29.21 @@ -105,7 +105,7 @@
29.22 ^ ato body (n + 1)
29.23 | ato (f $ t) n = ato f n ^ ato t (n + 1)
29.24 in "\n*** " ^ ato t 0 ^ "\n***" end;
29.25 -fun atomty t = (writeln o term_detail2str) t; (*WN100907 broken*)
29.26 +fun atomty t = (tracing o term_detail2str) t; (*WN100907 broken*)
29.27
29.28 fun term_str thy (Const(s,_)) = s
29.29 | term_str thy (Free(s,_)) = s
29.30 @@ -278,7 +278,7 @@
29.31 (*
29.32 > val il = str2term "[a=b,c=d,e=f]";
29.33 > val l = isalist2list il;
29.34 -> (writeln o terms2str) l;
29.35 +> (tracing o terms2str) l;
29.36 ["a = b","c = d","e = f"]
29.37
29.38 > val il = str2term "ss___::bool list";
29.39 @@ -833,7 +833,7 @@
29.40 \ [BOOL e_1, REAL v_1])\
29.41 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
29.42 > val ttt = (term_of o the o (parse thy)) scr;
29.43 -> writeln(term2str ttt);
29.44 +> tracing(term2str ttt);
29.45 > atomt ttt;
29.46 *** -------------
29.47 *** Const ( DiffApp.Make'_fun'_by'_explicit)
29.48 @@ -901,7 +901,7 @@
29.49 *** . . . . . . . . . . . . Bound 4 <----- Free ( h_, )
29.50
29.51 > val ttt' = inst_abs thy ttt;
29.52 -> writeln(term2str ttt');
29.53 +> tracing(term2str ttt');
29.54 Script Make_fun_by_explicit f_ v_ eqs_ =
29.55 ... as above ...
29.56 > atomt ttt';
30.1 --- a/src/Tools/isac/library.sml Thu Sep 23 14:49:23 2010 +0200
30.2 +++ b/src/Tools/isac/library.sml Thu Sep 23 16:38:25 2010 +0200
30.3 @@ -92,7 +92,7 @@
30.4 fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;
30.5 fun gen_insI eq pr (x, xs) =
30.6 if gen_mem eq (x, xs)
30.7 - then (writeln ("### occurs twice: "^(pr x)); xs)
30.8 + then (tracing ("### occurs twice: "^(pr x)); xs)
30.9 else x :: xs;
30.10 fun gen_union eq pr (xs, []) = xs
30.11 | gen_union eq pr ([], ys) = ys
30.12 @@ -187,12 +187,12 @@
30.13 val commas = space_implode ",";
30.14
30.15 fun strs2str strl = "[" ^ (commas (map quote strl)) ^ "]";
30.16 -(*> val str = strs2str ["123","asd"]; writeln str;
30.17 +(*> val str = strs2str ["123","asd"]; tracing str;
30.18 val it = "[\"123\", \"asd\"]" : string
30.19 "123", "asd"] *)
30.20 fun strs2str' strl = "[" ^ (commas strl) ^ "]";
30.21 fun list2str strl = "[" ^ (commas strl) ^ "]";
30.22 -(*> val str = list2str ["123","asd"]; writeln str;
30.23 +(*> val str = list2str ["123","asd"]; tracing str;
30.24 val str = "[123, asd]" : string
30.25 [123, asd] *)
30.26 fun spair2str (s1,s2) = "(" ^ (quote s1) ^ ", " ^ (quote s2) ^ ")";
30.27 @@ -206,7 +206,7 @@
30.28 val it = "[(bdv,x),(err,#0)]" : string*)
30.29 fun subs2str' (subs:(string * string) list) = (*12.12.99???*)
30.30 (list2str o (map pair2str)) subs;
30.31 -(*> val subs = subs2str [("bdv","x")]; writeln subs;
30.32 +(*> val subs = subs2str [("bdv","x")]; tracing subs;
30.33 val subs = "[(\"bdv\", \"x\")]" : string
30.34 [("bdv", "x")] *)
30.35 fun con2str land_lor = quote " &| ";
31.1 --- a/src/Tools/isac/print_exn_G.sml Thu Sep 23 14:49:23 2010 +0200
31.2 +++ b/src/Tools/isac/print_exn_G.sml Thu Sep 23 16:38:25 2010 +0200
31.3 @@ -7,12 +7,12 @@
31.4 fun print_exn_unit e =
31.5 case e of
31.6 PTREE str =>
31.7 - (writeln ("Exception PTREE raised:\n" ^ str))
31.8 + (tracing ("Exception PTREE raised:\n" ^ str))
31.9 (* | SCRIPT str =>
31.10 - (writeln ("Exception SCRIPT raised:\n" ^ str))
31.11 + (tracing ("Exception SCRIPT raised:\n" ^ str))
31.12 | TERM (msg,ts) =>
31.13 - (writeln ("Exception TERM raised:\n" ^ msg);
31.14 - seq (writeln o Sign.string_of_term sign) ts)*)
31.15 + (tracing ("Exception TERM raised:\n" ^ msg);
31.16 + seq (tracing o Sign.string_of_term sign) ts)*)
31.17 | e => raise e;
31.18
31.19 (*raises the exception in order to have a polymorphic type!*)
32.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Thu Sep 23 14:49:23 2010 +0200
32.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Thu Sep 23 16:38:25 2010 +0200
32.3 @@ -80,8 +80,8 @@
32.4 autx (j + i) auts ^
32.5 indt j ^ "</"^str^">\n" : xml
32.6 end;
32.7 -(* writeln(authors2xml 2 "MATHAUTHORS" []);
32.8 - writeln(authors2xml 2 "MATHAUTHORS"
32.9 +(* tracing(authors2xml 2 "MATHAUTHORS" []);
32.10 + tracing(authors2xml 2 "MATHAUTHORS"
32.11 ["isac-team 2001", "Richard Lang 2003"]);
32.12 *)
32.13
32.14 @@ -92,7 +92,7 @@
32.15 in (indt j) ^ "<STRINGLIST>\n" ^
32.16 (id2x (j + indentation) ids) ^
32.17 (indt j) ^ "</STRINGLIST>\n" end;
32.18 -(* writeln(id2xml 8 ["linear","univariate","equation"]);
32.19 +(* tracing(id2xml 8 ["linear","univariate","equation"]);
32.20 <STRINGLIST>
32.21 <STRING>linear</STRING>
32.22 <STRING>univariate</STRING>
32.23 @@ -106,7 +106,7 @@
32.24 in (indt j) ^ "<INTLIST>\n" ^
32.25 (int2x (j + i) ids) ^
32.26 (indt j) ^ "</INTLIST>\n" end;
32.27 -(* writeln(ints2xml 3 [1,2,3]);
32.28 +(* tracing(ints2xml 3 [1,2,3]);
32.29 *)
32.30
32.31
32.32 @@ -122,18 +122,18 @@
32.33 ints2xml (j+i) pos ^
32.34 pos_2xml (j+i) pos_ ^
32.35 indt (j) ^ "</" ^ tag ^ ">\n";
32.36 -(* writeln(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));
32.37 +(* tracing(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));
32.38 *)
32.39
32.40 fun formula2xml j term = (*TODO.WN050211: use for _all_ <FORMULA>*)
32.41 indt j ^ "<FORMULA>\n"^
32.42 term2xml j term ^"\n"^
32.43 indt j ^ "</FORMULA>\n" : xml;
32.44 -(* writeln(formula2xml 6 (str2term "1+1=2"));
32.45 +(* tracing(formula2xml 6 (str2term "1+1=2"));
32.46 *)
32.47 fun formulae2xml j [] = ("":xml)
32.48 | formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs;
32.49 -(* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
32.50 +(* tracing(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
32.51 *)
32.52
32.53 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
32.54 @@ -144,11 +144,11 @@
32.55 term2xml (j+i) term ^"\n"^
32.56 indt (j+i) ^ "</FORMULA>\n"^
32.57 indt j ^ "</POSFORM>\n" : xml;
32.58 -(* writeln(posform2xml 6 (([1,2],Frm), str2term "1+1=2"));
32.59 +(* tracing(posform2xml 6 (([1,2],Frm), str2term "1+1=2"));
32.60 *)
32.61 fun posforms2xml j [] = ("":xml)
32.62 | posforms2xml j (r::rs) = posform2xml j r ^ posforms2xml j rs;
32.63 -(* writeln(posforms2xml 6 [(([1],Res), str2term "1+1=2"),(([2],Res), str2term "1+1+1=3")]);
32.64 +(* tracing(posforms2xml 6 [(([1],Res), str2term "1+1=2"),(([2],Res), str2term "1+1+1=3")]);
32.65 *)
32.66
32.67 fun calcref2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
32.68 @@ -217,7 +217,7 @@
32.69 in filt end;
32.70
32.71 (*FIXME.WN040831 model2xml <--?--> pattern2xml*)
32.72 -(*WN.25.8.03: pattern2xml different output with TextIO | writeln !!!
32.73 +(*WN.25.8.03: pattern2xml different output with TextIO | tracing !!!
32.74 the version below is for TextIO: terms2xml makes \n !*)
32.75 (* val (j, p, where_) = (i, ppc, where_);
32.76 *)
32.77 @@ -244,7 +244,7 @@
32.78 | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
32.79 (indt j) ^ "</RELATE>\n");
32.80 (*
32.81 -writeln(pattern2xml 3 ((#ppc o get_pbt)
32.82 +tracing(pattern2xml 3 ((#ppc o get_pbt)
32.83 ["squareroot","univariate","equation","test"]) []);
32.84 *)
32.85
32.86 @@ -318,7 +318,7 @@
32.87 (indt (j+i)) ^ "</RELATE>\n")^
32.88 indt j ^"</MODEL>\n"):xml
32.89 end;
32.90 -(* writeln(model2xml 3 itms []);
32.91 +(* tracing(model2xml 3 itms []);
32.92 *)
32.93
32.94 fun spec2xml j ((dI,pI,mI):spec) =
32.95 @@ -344,7 +344,7 @@
32.96 | _ => "Und")^" </BELONGSTO>\n"^
32.97 spec2xml (j+i) spec ^
32.98 indt j ^"</CALCHEAD>\n"):xml;
32.99 -(* writeln (modspec2xml 2 e_ocalhd);
32.100 +(* tracing (modspec2xml 2 e_ocalhd);
32.101 *)
32.102 fun pos'calchead2xml j (p:pos', (b, p_, head, gfr, pre, spec): ocalhd) =
32.103 (indt j ^"<CALCHEAD status = "^
32.104 @@ -376,14 +376,14 @@
32.105 indt j ^"</SUBSTITUTION>\n"):xml;
32.106 (* val subs = [(str2term "bdv", str2term "x")];
32.107 val subs = ["(bdv, x)"];
32.108 - writeln(subs2xml 0 subs);
32.109 + tracing(subs2xml 0 subs);
32.110 *)
32.111 fun subst2xml j (subst:subst) =
32.112 (indt j ^"<SUBSTITUTION>\n"^
32.113 foldl op^ ("", map (sub2xml (j+i)) subst) ^
32.114 indt j ^"</SUBSTITUTION>\n"):xml;
32.115 (* val subst = [(str2term "bdv", str2term "x")];
32.116 - writeln(subst2xml 0 subst);
32.117 + tracing(subst2xml 0 subst);
32.118 *)
32.119
32.120 (* val (j, str) = ((j+i), form);
32.121 @@ -568,7 +568,7 @@
32.122 (indt j ^"<REWRITETACTIC name=\"Rewrite\">\n"^
32.123 thm'2xml (j+i) thm'^
32.124 indt j ^"</REWRITETACTIC>\n"):xml
32.125 -(* writeln (tac2xml 2 (Rewrite ("all_left",
32.126 +(* tracing (tac2xml 2 (Rewrite ("all_left",
32.127 "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)")));
32.128 val (j, (Rewrite_Inst (subs, thm'))) = (i, tac);
32.129 *)
32.130 @@ -577,7 +577,7 @@
32.131 subs2xml (j+i) subs^
32.132 thm'2xml (j+i) thm'^
32.133 indt j ^"</REWRITEINSTTACTIC>\n"):xml
32.134 -(* writeln (tac2xml 2 (Rewrite_Inst
32.135 +(* tracing (tac2xml 2 (Rewrite_Inst
32.136 (["(bdv,x)"],
32.137 ("all_left",
32.138 "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)"))));
32.139 @@ -698,7 +698,7 @@
32.140 (* val (ContThmInst{thyID, thm, bdvs, thminst, applto, applat, reword,
32.141 asms, lhs, rhs, result, resasms, asmrls}) =
32.142 (context_thy (pt,pos) tac);
32.143 -writeln (contthy2xml 2 (context_thy (pt,pos) tac));
32.144 +tracing (contthy2xml 2 (context_thy (pt,pos) tac));
32.145 *)
32.146 fun contthy2xml j EContThy =
32.147 raise error "contthy2xml called with EContThy"
33.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml Thu Sep 23 14:49:23 2010 +0200
33.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml Thu Sep 23 16:38:25 2010 +0200
33.3 @@ -25,14 +25,14 @@
33.4 (** add and delete users -----------------------------------------------
33.5 FIXXME.8.03 addUser: clear code, because only CalcTrees distinguished**)
33.6 fun adduserOK2xml (cI:calcID) (uI:iterID) =
33.7 - writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n" ^
33.8 + tracing ("@@@@@begin@@@@@\n "^string_of_int uI^" \n" ^
33.9 "<ADDUSER>\n" ^
33.10 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.11 " <USERID> "^string_of_int uI^" </USERID>\n" ^
33.12 "</ADDUSER>\n" ^
33.13 "@@@@@end@@@@@");
33.14 fun deluserOK2xml (cI:calcID) (uI:iterID) =
33.15 - writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n" ^
33.16 + tracing ("@@@@@begin@@@@@\n "^string_of_int uI^" \n" ^
33.17 "<DELUSER>\n" ^
33.18 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.19 " <USERID> "^string_of_int uI^" </USERID>\n" ^
33.20 @@ -41,27 +41,27 @@
33.21 (*---------------------------------------------------------------------*)
33.22
33.23 fun calctreeOK2xml (*uI:iterID*) (cI:calcID) =
33.24 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.25 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.26 "<CALCTREE>\n" ^
33.27 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.28 "</CALCTREE>\n" ^
33.29 "@@@@@end@@@@@");
33.30 fun deconstructcalctreeOK2xml (*uI:userID*) (cI:calcID) =
33.31 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.32 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.33 "<DELCALC>\n" ^
33.34 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.35 "</DELCALC>\n" ^
33.36 "@@@@@end@@@@@");
33.37
33.38 fun iteratorOK2xml (cI:calcID) (p:pos')=
33.39 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.40 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.41 "<CALCITERATOR>\n" ^
33.42 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.43 pos'2xml i ("POSITION", p) ^
33.44 "</CALCITERATOR>\n" ^
33.45 "@@@@@end@@@@@");
33.46 fun iteratorERROR2xml (cI:calcID) =
33.47 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.48 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.49 "<CALCITERATOR>\n" ^
33.50 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.51 " <ERROR> pos does not exist </ERROR>\n" ^
33.52 @@ -69,14 +69,14 @@
33.53 "@@@@@end@@@@@");
33.54
33.55 fun sysERROR2xml (cI:calcID) "" =
33.56 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.57 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.58 "<SYSERROR>\n" ^
33.59 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.60 " <ERROR> in kernel </ERROR>\n" ^
33.61 "</SYSERROR>\n" ^
33.62 "@@@@@end@@@@@")
33.63 | sysERROR2xml (cI:calcID) str =
33.64 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.65 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.66 "<SYSERROR>\n" ^
33.67 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.68 " <ERROR> "^str^" </ERROR>\n" ^
33.69 @@ -84,7 +84,7 @@
33.70 "@@@@@end@@@@@");
33.71
33.72 fun refformulaOK2xml (cI:calcID) p (Form t) =
33.73 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.74 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.75 "<REFFORMULA>\n" ^
33.76 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.77 " <CALCFORMULA>\n"^
33.78 @@ -96,7 +96,7 @@
33.79 "</REFFORMULA>\n" ^
33.80 "@@@@@end@@@@@")
33.81 | refformulaOK2xml (cI:calcID) p (ModSpec modspec) =
33.82 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.83 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.84 "<REFFORMULA>\n" ^
33.85 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.86 pos'calchead2xml i (p, modspec)^
33.87 @@ -104,7 +104,7 @@
33.88 "@@@@@end@@@@@");
33.89
33.90 fun refformulaERROR2xml (cI:calcID) = (*FIXME.WN.29.8.03 unused*)
33.91 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.92 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.93 "<REFFORMULA>\n" ^
33.94 " <ERROR> object is not a formula </ERROR>\n" ^
33.95 "</REFFORMULA>\n" ^
33.96 @@ -113,14 +113,14 @@
33.97 (* val (cI, tac) = (cI, ta);
33.98 *)
33.99 fun gettacticOK2xml (cI:calcID) tac =
33.100 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.101 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.102 "<GETTACTIC>\n" ^
33.103 " <CALCID> "^string_of_int cI^" </CALCID>\n"^
33.104 tac2xml i tac^
33.105 "</GETTACTIC>\n" ^
33.106 "@@@@@end@@@@@");
33.107 fun gettacticERROR2xml (cI:calcID) str =
33.108 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.109 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.110 "<GETTACTIC>\n" ^
33.111 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.112 " <ERROR> "^str^" </ERROR>\n" ^
33.113 @@ -128,7 +128,7 @@
33.114 "@@@@@end@@@@@");
33.115
33.116 fun applicabletacticsOK cI tacs =
33.117 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.118 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.119 "<APPLICABLETACTICS>\n" ^
33.120 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.121 " <TACLIST>\n"^
33.122 @@ -138,7 +138,7 @@
33.123 "@@@@@end@@@@@");
33.124
33.125 fun getasmsOK2xml (cI:calcID) terms =
33.126 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.127 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.128 "<GETASSUMPTIONS>\n" ^
33.129 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.130 " <ASMLIST>\n"^
33.131 @@ -151,7 +151,7 @@
33.132
33.133 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
33.134 fun getaccuasmsOK2xml cI asms =
33.135 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.136 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.137 "<GETACCUMULATEDASMS>\n" ^
33.138 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.139 " <ASMLIST>\n"^
33.140 @@ -165,7 +165,7 @@
33.141 *)
33.142
33.143 fun getintervalOK (cI:calcID) fs =
33.144 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.145 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.146 "<GETELEMENTSFROMTO>\n" ^
33.147 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.148 " <FORMHEADS>\n"^
33.149 @@ -176,7 +176,7 @@
33.150
33.151
33.152 fun matchpbl2xml (cI:calcID) (model_ok, pI, hdl, pbl, pre) =
33.153 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.154 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.155 "<CONTEXTPBL>\n" ^
33.156 " <GUH> " ^ pblID2guh pI ^ " </GUH>\n" ^
33.157 " <STATUS> " ^ (if model_ok
33.158 @@ -190,7 +190,7 @@
33.159 "@@@@@end@@@@@");
33.160
33.161 fun matchmet2xml (cI:calcID) (model_ok, pI, scr, pbl, pre) =
33.162 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.163 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.164 "<CONTEXTMET>\n" ^
33.165 " <GUH> " ^ metID2guh pI ^ " </GUH>\n" ^
33.166 " <STATUS> " ^ (if model_ok
33.167 @@ -203,7 +203,7 @@
33.168
33.169
33.170 fun tryrefineOK2xml (cI:calcID) (ModSpec modspec) =
33.171 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.172 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.173 "<TRYREFINE>\n" ^
33.174 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.175 modspec2xml i modspec ^
33.176 @@ -211,7 +211,7 @@
33.177 "@@@@@end@@@@@");
33.178
33.179 fun appendformulaOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =
33.180 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.181 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.182 "<APPENDFORMULA>\n" ^
33.183 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.184 " <CALCCHANGED>\n" ^
33.185 @@ -224,12 +224,12 @@
33.186 (* appendformulaOK2xml 1 ([2],Frm) ([3],Pbl) ([4],Res);
33.187 *)
33.188 fun appendformulaERROR2xml (cI:calcID) msg =
33.189 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.190 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.191 "<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n" ^
33.192 "@@@@@end@@@@@");
33.193
33.194 fun replaceformulaOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =
33.195 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.196 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.197 "<REPLACEFORMULA>\n" ^
33.198 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.199 " <CALCCHANGED>\n" ^
33.200 @@ -240,12 +240,12 @@
33.201 "</REPLACEFORMULA>\n" ^
33.202 "@@@@@end@@@@@");
33.203 fun replaceformulaERROR2xml (cI:calcID) msg =
33.204 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.205 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.206 "<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n" ^
33.207 "@@@@@end@@@@@");
33.208
33.209 fun message2xml (cI:calcID) e =
33.210 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.211 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.212 "<MESSAGE>\n" ^
33.213 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.214 " <STRING> "^e^" </STRING>\n" ^
33.215 @@ -253,7 +253,7 @@
33.216 "@@@@@end@@@@@");
33.217
33.218 fun setnexttactic2xml (*uI:iterID*) (cI:calcID) e =
33.219 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.220 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.221 "<SETNEXTTACTIC>\n" ^
33.222 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.223 " <MESSAGE> "^e^" </MESSAGE>\n" ^
33.224 @@ -261,7 +261,7 @@
33.225 "@@@@@end@@@@@");
33.226
33.227 fun fetchproposedtacticOK2xml (*uI:userID*) (cI:calcID) tac =
33.228 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.229 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.230 "<NEXTTAC>\n" ^
33.231 " <CALCID> "^string_of_int cI^" </CALCID>\n"^
33.232 tac2xml i tac^
33.233 @@ -271,7 +271,7 @@
33.234 (* fetchproposedtactic2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));
33.235 *)
33.236 fun fetchproposedtacticERROR2xml (*uI:userID*) (cI:calcID) e =
33.237 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.238 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.239 "<NEXTTAC>\n" ^
33.240 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.241 " <ERROR> "^ e ^" </ERROR>\n" ^
33.242 @@ -283,7 +283,7 @@
33.243 GENERATED: the pos' of the new active formula
33.244 .*)
33.245 fun autocalculateOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =
33.246 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.247 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.248 "<AUTOCALC>\n" ^
33.249 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.250 " <CALCCHANGED>\n" ^
33.251 @@ -296,12 +296,12 @@
33.252 (* autocalculate2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));
33.253 *)
33.254 fun autocalculateERROR2xml (cI:calcID) e =
33.255 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.256 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.257 "<CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
33.258 "@@@@@end@@@@@");
33.259
33.260 fun interStepsOK (cI:calcID) (*pos'forms*) (old:pos') (del:pos') (new:pos') =
33.261 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.262 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.263 "<INTERSTEPS>\n" ^
33.264 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.265 " <CALCCHANGED>\n" ^
33.266 @@ -312,12 +312,12 @@
33.267 "</INTERSTEPS>\n" ^
33.268 "@@@@@end@@@@@");
33.269 fun interStepsERROR (cI:calcID) e =
33.270 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.271 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.272 " <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
33.273 "@@@@@end@@@@@");
33.274
33.275 fun modifycalcheadOK2xml (cI:calcID) (chd as (complete,p_,_,_,_,_):ocalhd) =
33.276 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.277 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.278 "<MODIFYCALCHEAD>\n" ^
33.279 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.280 " <STATUS> "^(if complete then "complete"
33.281 @@ -329,7 +329,7 @@
33.282 (* val (cI, contthy) = (cI, (context_thy (pt,pos) tac));
33.283 *)
33.284 fun contextthyOK2xml cI contthy =
33.285 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.286 + tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
33.287 "<CONTEXTTHY>\n" ^
33.288 " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
33.289 contthy2xml i contthy ^
33.290 @@ -338,5 +338,5 @@
33.291
33.292 (*
33.293 fun contextthyNO2xml guh =
33.294 - writeln (datatypes.contextthyNO2xml 0 guh);
33.295 + tracing (datatypes.contextthyNO2xml 0 guh);
33.296 *)
34.1 --- a/src/Tools/isac/xmlsrc/mathml.sml Thu Sep 23 14:49:23 2010 +0200
34.2 +++ b/src/Tools/isac/xmlsrc/mathml.sml Thu Sep 23 16:38:25 2010 +0200
34.3 @@ -28,7 +28,7 @@
34.4
34.5
34.6 fun strs2xml strs = foldl (op ^) ("", strs);
34.7 -(* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]);
34.8 +(* tracing (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]);
34.9 <XXX> xxx </XXX>
34.10 <YYY> yyy </YYY>*)
34.11
34.12 @@ -41,7 +41,7 @@
34.13 indt (j+2*i) ^ "<ISA> " ^ (decode o term2str) t ^ " </ISA>\n" ^
34.14 indt (j+i) ^ "</MATHML>";
34.15 (*val t = str2term "equality e_";
34.16 - writeln (term2xml 8 t);
34.17 + tracing (term2xml 8 t);
34.18 <MATHML>
34.19 <ISA> equality e_ </ISA>
34.20 <MATHML> *)
34.21 @@ -49,7 +49,7 @@
34.22 (*version for TextIO*)
34.23 fun terms2xml j [] = ""
34.24 | terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts;
34.25 -(*version for writeln: extra \n*)
34.26 +(*version for tracing: extra \n*)
34.27 fun terms2xml' j [] = ""
34.28 | terms2xml' j [t] = term2xml j t
34.29 | terms2xml' j (t::ts) = term2xml j t ^"\n"^ terms2xml' j ts;
34.30 @@ -62,11 +62,11 @@
34.31 (*version for TextIO*)
34.32 fun cterms2xml j [] = ""
34.33 | cterms2xml j (t::ts) = cterm2xml j t ^ cterms2xml j ts;
34.34 -(*version for writeln: extra \n*)
34.35 +(*version for tracing: extra \n*)
34.36 fun cterms2xml' j [] = ""
34.37 | cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts;
34.38
34.39 -(* writeln(cterms2xml 5 ["cterm1", "cterm2"]);
34.40 +(* tracing(cterms2xml 5 ["cterm1", "cterm2"]);
34.41 <MATHML>
34.42 <ISA> cterm1 </ISA>
34.43 </MATHML>
35.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Thu Sep 23 14:49:23 2010 +0200
35.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Thu Sep 23 16:38:25 2010 +0200
35.3 @@ -77,7 +77,7 @@
35.4 and nds _ _ [] = ""
35.5 | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
35.6 in nds j [0] h : xml end;
35.7 -(* (writeln o hierarchy_pbl) (!ptyps);
35.8 +(* (tracing o hierarchy_pbl) (!ptyps);
35.9 *)
35.10
35.11 fun pbl_hierarchy2file (path:path) =
35.12 @@ -192,7 +192,7 @@
35.13 (*
35.14 val pblID = ["linear","univariate","equation"];
35.15 val pblID = ["degree_4","polynomial","univariate","equation"];
35.16 -writeln (pbl2xml pblID (get_pbt pblID));
35.17 +tracing (pbl2xml pblID (get_pbt pblID));
35.18 *)
35.19
35.20 (*replace by 'fun calc2xml' as developed for thy in 0607*)
35.21 @@ -270,7 +270,7 @@
35.22 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
35.23 "</NODECONTENT>" : xml;
35.24
35.25 -(* writeln (met2xml ["Test", "solve_linear"]
35.26 +(* tracing (met2xml ["Test", "solve_linear"]
35.27 (get_met ["Test", "solve_linear"]));
35.28 *)
35.29
35.30 @@ -278,14 +278,14 @@
35.31
35.32 (*.write the files using an int-key (pos') as filename.*)
35.33 fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) =
35.34 - (writeln ("### pbl2file: id = " ^ strs2str id);
35.35 + (tracing ("### pbl2file: id = " ^ strs2str id);
35.36 ((str2file (path ^ pos2filename pos)) o (pbl2xml id)) pbl
35.37 );
35.38
35.39 (*.write the files using the guh as filename.*)
35.40 (* *)
35.41 fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) =
35.42 - (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ pos2str pos);
35.43 + (tracing ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ pos2str pos);
35.44 ((str2file (path ^ guh2filename guh)) o (pbl2xml id)) pbl
35.45 );
35.46
35.47 @@ -293,12 +293,12 @@
35.48
35.49 (*.write the files using an int-key (pos') as filename.*)
35.50 fun met2file (path:path) (pos:pos) (id:metID) met =
35.51 - (writeln ("### met2file: id = " ^ strs2str id);
35.52 + (tracing ("### met2file: id = " ^ strs2str id);
35.53 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
35.54
35.55 (*.write the files using the guh as filename.*)
35.56 fun met2file (path:path) (pos:pos) (id:metID) (met as {guh,...}) =
35.57 - (writeln ("### met2file: id = " ^ strs2str id);
35.58 + (tracing ("### met2file: id = " ^ strs2str id);
35.59 ((str2file (path ^ guh2filename guh)) o (met2xml id)) met);
35.60
35.61
36.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Sep 23 14:49:23 2010 +0200
36.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Sep 23 16:38:25 2010 +0200
36.3 @@ -103,7 +103,7 @@
36.4 : (theID * thydata) list
36.5 end;
36.6
36.7 -fun show_thes () = (writeln o format_pblIDl o (scan [])) (!thehier);
36.8 +fun show_thes () = (tracing o format_pblIDl o (scan [])) (!thehier);
36.9
36.10
36.11
36.12 @@ -164,7 +164,7 @@
36.13 | the_hier th ((theID, thydata)::ths) =
36.14 if can_insert theID th
36.15 then let val th' = if exist_the theID th
36.16 - then (writeln ("*** insert: preserved "^strs2str theID);
36.17 + then (tracing ("*** insert: preserved "^strs2str theID);
36.18 th)
36.19 else insrt theID thydata theID th
36.20 in the_hier th' ths end
36.21 @@ -265,7 +265,7 @@
36.22
36.23 (*.analoguous to 'fun met2file'.*)
36.24 fun thydata2file (xmldata:path) (pos:pos) (theID:theID) thydata =
36.25 - (writeln ("### thes2file: id = " ^ strs2str theID);
36.26 + (tracing ("### thes2file: id = " ^ strs2str theID);
36.27 str2file (xmldata ^ theID2filename theID)
36.28 (thydata2xml (theID:theID, thydata)));
36.29
37.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Sep 23 14:49:23 2010 +0200
37.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Thu Sep 23 16:38:25 2010 +0200
37.3 @@ -37,7 +37,8 @@
37.4 "----------- parsing ------------------------------------";
37.5 "----------- parsing ------------------------------------";
37.6 fun str2term str = (term_of o the o (parse thy)) str;
37.7 -fun term2s t = Syntax.string_of_term (thy2ctxt' "Integrate") t;
37.8 +fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term
37.9 + (ProofContext.init_global thy)) t;
37.10
37.11 val t = str2term "Integral x D x";
37.12 val t = str2term "Integral x^^^2 D x";
37.13 @@ -101,15 +102,9 @@
37.14 if term2str cc = "c_3" then () else raise error "integrate.sml: new_c ???";
37.15
37.16 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
37.17 -"####1###################################################";
37.18 -term2str t' = "x ^^^ 2 * c + c_2 = op + (x ^^^ 2 * c + c_2) c_3" --REDO "Groups.plus_class.plus";
37.19 -"####2###################################################";
37.20 -
37.21 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
37.22 else raise error "intergrate.sml: diff. eval_add_new_c";
37.23
37.24 -"####3###################################################";
37.25 -
37.26 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
37.27 val SOME (thmstr, thm) = get_calculation1_ thy cc term;
37.28
37.29 @@ -180,12 +175,18 @@
37.30 "----------- simplify by ruleset reducing make_ratpoly_in";
37.31 "----------- simplify by ruleset reducing make_ratpoly_in";
37.32 "----------- simplify by ruleset reducing make_ratpoly_in";
37.33 -val thy = Isac.thy;
37.34 -val subs = [(str2term"bdv",str2term"x")];
37.35 +val thy = theory "Isac";
37.36 +val subs = [(str2term "bdv", str2term "x")];
37.37 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
37.38
37.39 "----- stepwise from the rulesets in simplify_Integral and below-----";
37.40 (*###*)val rls = norm_Rational_noadd_fractions;
37.41 +"###-1-##################################################";
37.42 +trace_rewrite := true;
37.43 +val SOME (ttt, _) = rewrite_set_inst_ thy true subs rls t;
37.44 +term2str ttt;
37.45 +"###-2-##################################################";
37.46 +
37.47 case rewrite_set_inst_ thy true subs rls t of
37.48 SOME _ => raise error "integrate.sml simplify by ruleset norm_Rational_.#2"
37.49 | NONE => ();
37.50 @@ -195,7 +196,10 @@
37.51 and keeps "..." is_polyexp" as an assumption.
37.52 AFTER CORRECTION in Integrate.ML as above*)
37.53
37.54 +
37.55 +
37.56 (*###*)val rls = order_add_mult_in;
37.57 +"###-3-##################################################";
37.58 val SOME (t,[]) = rewrite_set_ thy true rls t;
37.59 if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)"then()
37.60 else raise error "integrate.sml simplify by ruleset order_add_mult_in #2";
38.1 --- a/test/Tools/isac/Test_Isac.thy Thu Sep 23 14:49:23 2010 +0200
38.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Sep 23 16:38:25 2010 +0200
38.3 @@ -40,18 +40,6 @@
38.4 cd"smltest/ME";
38.5 use"ctree.sml";
38.6 *)
38.7 -
38.8 -ML {*
38.9 -print_depth 2;
38.10 -@{term "equalities"};
38.11 -type_of @{term "[x_1+1=2,x_2=0]"};
38.12 -
38.13 -@{term "solveForVars"};
38.14 -type_of @{term "[x_1,x_2]::real list"};
38.15 -
38.16 -@{term "solution"};
38.17 -type_of @{term "ss''' :: bool list"};
38.18 -*}
38.19 use "Interpret/calchead.sml" (*part.*)
38.20 (*
38.21 use"calchead.sml";
38.22 @@ -78,13 +66,17 @@
38.23 use"diff.sml";
38.24 use"diffapp.sml";
38.25 *)
38.26 -ML {*print_depth 99*}
38.27 +ML {*print_depth 3*}
38.28
38.29 ML {*
38.30 -str2term "a + b";
38.31 -str2term "a - b";
38.32 -str2term "a * b";
38.33 -str2term "a / b";
38.34 +trace_rewrite := true;
38.35 +fun ((i: int) upto j) =
38.36 + if i > j
38.37 + then (if !trace_rewrite then tracing (string_of_int i) else ();
38.38 + [])
38.39 + else (if !trace_rewrite then tracing (string_of_int i) else ();
38.40 + i :: (i + 1 upto j));
38.41 +1 upto 5;
38.42 *}
38.43
38.44 use "Knowledge/integrate.sml";