1.1 --- a/test/Tools/isac/Interpret/script.sml Thu Jul 21 12:01:56 2011 +0200
1.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Jul 21 16:57:21 2011 +0200
1.3 @@ -15,7 +15,6 @@
1.4 "-----------------------------------------------------------------";
1.5 "-----------------------------------------------------------------";
1.6
1.7 -(*========== inhibit exn 110503 ================================================
1.8
1.9 "----------- WN0509 why does next_tac doesnt find Substitute -----";
1.10 "----------- WN0509 why does next_tac doesnt find Substitute -----";
1.11 @@ -29,7 +28,9 @@
1.12 \ (let q___ = Take (M_b v_v = q__); \
1.13 \ (M1__::bool) = ((Substitute [v_ = 0])) q___ \
1.14 \ in True)";
1.15 +(*========== inhibit exn 110721 ================================================
1.16 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.17 +(========= inhibit exn 110721 ================================================*)
1.18
1.19 val str = (*#2#*)
1.20 "Script BiegelinieScript \
1.21 @@ -71,8 +72,12 @@
1.22 \ M2__ = Substitute [v_ = 2] q___ \
1.23 \ in True)"
1.24 ;
1.25 +
1.26 +(*========== inhibit exn 110721 ================================================
1.27 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.28 atomty sc';
1.29 +========== inhibit exn 110721 ================================================*)
1.30 +
1.31 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.32 (*---------------------------------------------------------------------
1.33 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
1.34 @@ -84,10 +89,13 @@
1.35 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.36 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.37 "FunktionsVariable x"];
1.38 +
1.39 val (dI',pI',mI') =
1.40 ("Biegelinie",["MomentBestimmte","Biegelinien"],
1.41 ["IntegrierenUndKonstanteBestimmen"]);
1.42 +
1.43 val p = e_pos'; val c = [];
1.44 +
1.45 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.46 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.47 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.48 @@ -96,8 +104,10 @@
1.49 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.50 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.51 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.52 +
1.53 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.54 | _ => error "script.sml, doesnt find Substitute #2";
1.55 +(*========== inhibit exn 110721 ================================================
1.56 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.57 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
1.58 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
1.59 @@ -108,12 +118,15 @@
1.60 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.61 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.62 (*---------------------------------------------------------------------*)
1.63 +
1.64 case nxt of (_, End_Proof') => ()
1.65 | _ => error "script.sml, doesnt find Substitute #3";
1.66 (*---------------------------------------------------------------------*)
1.67 (*the reason, that next_tac didnt find the 2nd Substitute, was that
1.68 the Take inbetween was missing, and thus the 2nd Substitute was applied
1.69 the last formula in ctree, and not to argument from script*)
1.70 +========== inhibit exn 110721 ================================================*)
1.71 +
1.72
1.73
1.74 "----------- WN0509 Substitute 2nd part --------------------------";
1.75 @@ -132,10 +145,13 @@
1.76 \ M1__ = Substitute [e1__] M1__ \
1.77 \ in True)"
1.78 ;
1.79 +(*========== inhibit exn 110721 ================================================
1.80 (*---^^^-OK-----------------------------------------------------------------*)
1.81 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.82 atomty sc';
1.83 (*---vvv-NOT ok-------------------------------------------------------------*)
1.84 +========== inhibit exn 110721 ================================================*)
1.85 +
1.86 val str = (*Substitute @@ Substitute does NOT work???*)
1.87 "Script BiegelinieScript \
1.88 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.89 @@ -173,6 +189,8 @@
1.90 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.91 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.92 | _ => error "script.sml, doesnt find Substitute #2";
1.93 +
1.94 +(*========== inhibit exn 110721 ================================================
1.95 trace_rewrite:=true;
1.96 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
1.97 trace_rewrite:=false;
1.98 @@ -190,12 +208,16 @@
1.99 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
1.100 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
1.101 thus corrected eval_argument_in OK*)
1.102 +========== inhibit exn 110721 ================================================*)
1.103
1.104 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.105 -val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]";
1.106 +val e1__ = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
1.107 +(*========== inhibit exn 110721 ================================================
1.108 val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
1.109 +
1.110 if term2str e1__ = "M_b 0 = 0" then () else
1.111 -error"script.sml diff.beh. eval_listexpr_ nth_ 1 [...";
1.112 +error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
1.113 +========== inhibit exn 110721 ================================================*)
1.114
1.115 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
1.116 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
1.117 @@ -205,6 +227,7 @@
1.118 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
1.119
1.120 val l__ = str2term"lhs (M_b 0 = 0)";
1.121 +(*========== inhibit exn 110721 ================================================
1.122 val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;
1.123 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;
1.124
1.125 @@ -212,12 +235,14 @@
1.126 trace_rewrite:=true;
1.127 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
1.128 trace_rewrite:=false;
1.129 +========== inhibit exn 110721 ================================================*)
1.130
1.131 show_mets();
1.132
1.133 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.134 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.135 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.136 +
1.137 states:=[];
1.138 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.139 ("Test", ["sqroot-test","univariate","equation","test"],
1.140 @@ -229,11 +254,22 @@
1.141 autoCalculate 1 (Step 1);
1.142 val ((pt, p), _) = get_calc 1; show_pt pt;
1.143 val appltacs = sel_appl_atomic_tacs pt p;
1.144 +
1.145 +(*
1.146 +(*These SHOULD be the same*)
1.147 + print_depth(999);
1.148 + appltacs;
1.149 + [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
1.150 + Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
1.151 + Calculate "times"];*)
1.152 +
1.153 +(*========== inhibit exn 110721 ================================================
1.154 if appltacs =
1.155 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
1.156 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
1.157 Calculate "times"] then ()
1.158 else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
1.159 +========== inhibit exn 110721 ================================================*)
1.160
1.161 trace_script := true;
1.162 trace_script := false;
1.163 @@ -241,11 +277,13 @@
1.164 val ((pt, p), _) = get_calc 1; show_pt pt;
1.165 val appltacs = sel_appl_atomic_tacs pt p;
1.166
1.167 +(*========== inhibit exn 110721 ================================================
1.168 "----- WN080102 these vvv do not work, because locatetac starts the search\
1.169 \1 stac too low";
1.170 +(* ERROR: assy: call by ([3], Pbl) *)
1.171 applyTactic 1 p (hd appltacs);
1.172 autoCalculate 1 CompleteCalc;
1.173 -============ inhibit exn 110503 ==============================================*)
1.174 +============ inhibit exn 110721 ==============================================*)
1.175
1.176 "----------- fun init_form, fun get_stac -------------------------";
1.177 "----------- fun init_form, fun get_stac -------------------------";
2.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Thu Jul 21 12:01:56 2011 +0200
2.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Thu Jul 21 16:57:21 2011 +0200
2.3 @@ -1,10 +1,6 @@
2.4 -(* tests on tools for scripts
2.5 - author: Walther Neuper
2.6 - 060605,
2.7 +(* Title: tests on tools for scripts
2.8 + Author: Walther Neuper 060605
2.9 (c) due to copyright terms
2.10 -
2.11 -use"../smltest/Scripts/scrtools.sml";
2.12 -use"scrtools.sml";
2.13 *)
2.14 "-----------------------------------------------------------------";
2.15 "table of contents -----------------------------------------------";
2.16 @@ -26,31 +22,31 @@
2.17 atomty auto_script;
2.18
2.19 store_met
2.20 - (prep_met Test.thy "met_testinter" [] e_metID
2.21 + (prep_met @{theory "Test"} "met_testinter" [] e_metID
2.22 (["Test","test_interSteps_1"]:metID,
2.23 - [("#Given" ,["Term t_"]),
2.24 + [("#Given" ,["Term t_t"]),
2.25 ("#Find" ,["normalform n_n"])
2.26 ],
2.27 - {rew_ord'="dummy_ord",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,
2.28 + {rew_ord' = "dummy_ord", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
2.29 crls=tval_rls, nrls=e_rls},
2.30 -"Script Stepwise t_ = \
2.31 - \(Try (Rewrite_Set discard_minus_ False) @@ \
2.32 - \ Try (Rewrite_Set expand_poly_ False) @@ \
2.33 - \ Try (Repeat (Calculate times)) @@ \
2.34 - \ Try (Rewrite_Set order_mult_rls_ False) @@ \
2.35 - \ Try (Rewrite_Set simplify_power_ False) @@ \
2.36 - \ Try (Rewrite_Set calc_add_mult_pow_ False) @@\
2.37 - \ Try (Rewrite_Set reduce_012_mult_ False) @@ \
2.38 - \ Try (Rewrite_Set order_add_rls_ False) @@ \
2.39 - \ Try (Rewrite_Set collect_numerals_ False) @@ \
2.40 - \ Try (Rewrite_Set reduce_012_ False) @@ \
2.41 - \ Try (Rewrite_Set discard_parentheses_ False))\
2.42 - \ t_"
2.43 +"Script Stepwise t_t = \
2.44 + \(Try (Rewrite_Set discard_minus False) @@ \
2.45 + \ Try (Rewrite_Set expand_poly False) @@ \
2.46 + \ Try (Repeat (Calculate TIMES)) @@ \
2.47 + \ Try (Rewrite_Set order_mult_rls False) @@ \
2.48 + \ Try (Rewrite_Set simplify_power False) @@ \
2.49 + \ Try (Rewrite_Set calc_add_mult_pow False) @@ \
2.50 + \ Try (Rewrite_Set reduce_012_mult False) @@ \
2.51 + \ Try (Rewrite_Set order_add_rls False) @@ \
2.52 + \ Try (Rewrite_Set collect_numerals False) @@ \
2.53 + \ Try (Rewrite_Set reduce_012 False) @@ \
2.54 + \ Try (Rewrite_Set discard_parentheses False)) \
2.55 + \ t_t"
2.56 (*presently this script cannot become equal in types to auto_script, because:
2.57 - this t_ must be either 'real' or 'bool' #1#,
2.58 + this t_t must be either 'real' or 'bool' #1#,
2.59 while the auto_script must be 'z and type-instantiated before usage*)
2.60 ));
2.61 -show_mets();
2.62 +show_mets();
2.63 val {scr = Script parsed_script,...} = get_met ["Test","test_interSteps_1"];
2.64 writeln(term2str parsed_script);
2.65 atomty parsed_script;
2.66 @@ -115,42 +111,43 @@
2.67 "-------- test the same called by interSteps norm_Rational -------";
2.68 "-------- test the same called by interSteps norm_Rational -------";
2.69 "-------- test the same called by interSteps norm_Rational -------";
2.70 +
2.71 val Seq {scr = Script auto_script,...} = assoc_rls "norm_Rational";
2.72 writeln(term2str auto_script);
2.73 atomty auto_script;
2.74 -(***
2.75 -*** Const (Script.Stepwise, ['z, 'z] => 'z)
2.76 -*** . Free (t_, 'z)
2.77 -*** . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
2.78 -*** . . Const (Script.Try, ['a => 'a, 'a] => 'a)
2.79 -*** . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
2.80 -*** . . . . Free (discard_minus_, Script.ID)
2.81 -*** . . . . Const (False, bool)
2.82 -*** . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
2.83 -*** . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
2.84 -*** . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
2.85 -*** . . . . . Free (rat_mult_poly, Script.ID)
2.86 -*** . . . . . Const (False, bool)
2.87 -*** . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
2.88 -*** . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
2.89 -*** . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
2.90 -*** . . . . . . Free (make_rat_poly_with_parentheses, Script.ID)
2.91 -*** . . . . . . Const (False, bool)
2.92 -*** . . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
2.93 -*** . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
2.94 -*** . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
2.95 -*** . . . . . . . Free (cancel_p_rls, Script.ID)
2.96 -*** . . . . . . . Const (False, bool)
2.97 -*** . . . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
2.98 -*** . . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
2.99 -*** . . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
2.100 -*** . . . . . . . . Free (norm_Rational_rls, Script.ID)
2.101 -*** . . . . . . . . Const (False, bool)
2.102 -*** . . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
2.103 -*** . . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
2.104 -*** . . . . . . . . Free (discard_parentheses_, Script.ID)
2.105 -*** . . . . . . . . Const (False, bool)
2.106 -*** . . Free (t_, 'a)
2.107 +(***
2.108 +*** Const (Script.Stepwise, 'z => 'z => 'z)
2.109 +*** . Free (t_t, 'z)
2.110 +*** . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
2.111 +*** . . Const (Script.Try, ('a => 'a) => 'a => 'a)
2.112 +*** . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
2.113 +*** . . . . Free (discard_minus, ID)
2.114 +*** . . . . Const (HOL.False, bool)
2.115 +*** . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
2.116 +*** . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
2.117 +*** . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
2.118 +*** . . . . . Free (rat_mult_poly, ID)
2.119 +*** . . . . . Const (HOL.False, bool)
2.120 +*** . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
2.121 +*** . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
2.122 +*** . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
2.123 +*** . . . . . . Free (make_rat_poly_with_parentheses, ID)
2.124 +*** . . . . . . Const (HOL.False, bool)
2.125 +*** . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
2.126 +*** . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
2.127 +*** . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
2.128 +*** . . . . . . . Free (cancel_p_rls, ID)
2.129 +*** . . . . . . . Const (HOL.False, bool)
2.130 +*** . . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
2.131 +*** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
2.132 +*** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
2.133 +*** . . . . . . . . Free (norm_Rational_rls, ID)
2.134 +*** . . . . . . . . Const (HOL.False, bool)
2.135 +*** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
2.136 +*** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
2.137 +*** . . . . . . . . Free (discard_parentheses1, ID)
2.138 +*** . . . . . . . . Const (HOL.False, bool)
2.139 +*** . . Const (empty, 'a)
2.140 ***)
2.141 states:=[];
2.142 CalcTree
3.1 --- a/test/Tools/isac/ProgLang/termC.sml Thu Jul 21 12:01:56 2011 +0200
3.2 +++ b/test/Tools/isac/ProgLang/termC.sml Thu Jul 21 16:57:21 2011 +0200
3.3 @@ -2,6 +2,7 @@
3.4 Author: Walther Neuper 051006,
3.5 (c) due to copyright terms
3.6 *)
3.7 +
3.8 "--------------------------------------------------------";
3.9 "table of contents --------------------------------------";
3.10 "--------------------------------------------------------";
3.11 @@ -17,200 +18,228 @@
3.12 "--------------------------------------------------------";
3.13
3.14
3.15 -(*===== inhibit exn ============================================================
3.16 "----------- inst_bdv -----------------------------------";
3.17 "----------- inst_bdv -----------------------------------";
3.18 "----------- inst_bdv -----------------------------------";
3.19 -if (term2str o prop_of o num_str) @{thm d1_isolate_add2} =
3.20 - "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)" then ()
3.21 -else error "termC.sml d1_isolate_add2";
3.22 -val subst = [(str2term "bdv", str2term "x")];
3.23 -val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
3.24 -val t' = inst_bdv subst t;
3.25 -if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
3.26 -else error "termC.sml inst_bdv 1";
3.27
3.28 -if string_of_thm (num_str @{thm separate_bdvs_add}) =
3.29 - "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
3.30 - \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
3.31 -else error "termC.sml separate_bdvs_add";
3.32 -val subst = [(str2term"bdv_1",str2term"c"),
3.33 - (str2term"bdv_2",str2term"c_2"),
3.34 - (str2term"bdv_3",str2term"c_3"),
3.35 - (str2term"bdv_4",str2term"c_4")];
3.36 -val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
3.37 -val t' = inst_bdv subst t;
3.38 -if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
3.39 - \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
3.40 -else error "termC.sml inst_bdv 2";
3.41 + if (term2str o prop_of o num_str) @{thm d1_isolate_add2} =
3.42 + "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)"
3.43 + then ()
3.44 + else error "termC.sml d1_isolate_add2";
3.45 + val subst = [(str2term "bdv", str2term "x")];
3.46 + val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
3.47 + val t' = inst_bdv subst t;
3.48 + if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)"
3.49 + then ()
3.50 + else error "termC.sml inst_bdv 1";
3.51
3.52 +(*===== inhibit exn AK110721 ============================================================
3.53 + if string_of_thm (num_str @{thm separate_bdvs_add}) =
3.54 + "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
3.55 + \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\""
3.56 + then ()
3.57 + else error "termC.sml separate_bdvs_add";
3.58 +===== inhibit exn AK110721 ============================================================*)
3.59 +
3.60 + val subst = [(str2term "bdv_1", str2term "c"),
3.61 + (str2term "bdv_2", str2term "c_2"),
3.62 + (str2term "bdv_3", str2term "c_3"),
3.63 + (str2term "bdv_4", str2term "c_4")];
3.64 + val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
3.65 + val t' = inst_bdv subst t;
3.66 +
3.67 + if term2str t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
3.68 + \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
3.69 + then ()
3.70 + else error "termC.sml inst_bdv 2";
3.71
3.72 "----------- subst_atomic_all ---------------------------";
3.73 "----------- subst_atomic_all ---------------------------";
3.74 "----------- subst_atomic_all ---------------------------";
3.75 -val t = str2term "(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
3.76 -val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
3.77 - (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
3.78 -val (all_Free_subst, t') = subst_atomic_all env t;
3.79 -if all_Free_subst andalso
3.80 - term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
3.81 -else error "termC.sml subst_atomic_all should be 'true'";
3.82
3.83 + val t = str2term "(tl vs_vs) from vs_vs occur_exactly_in (nth_nth 1 (es_es::bool list))";
3.84 + val env = [(str2term "vs_vs::real list", str2term "[c, c_2]"),
3.85 + (str2term "es_es::bool list", str2term "[c_2 = 0, c + c_2 = 1]")];
3.86 + val (all_Free_subst, t') = subst_atomic_all env t;
3.87
3.88 -val (all_Free_subst, t') = subst_atomic_all (tl env) t;
3.89 -if not all_Free_subst andalso
3.90 - term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
3.91 -else error "termC.sml subst_atomic_all should be 'false'";
3.92 -===== inhibit exn ============================================================*)
3.93 +(*===== inhibit exn AK110721 ============================================================
3.94 +(*all_Free_subst; (*false !!!*)*)
3.95 + if all_Free_subst andalso
3.96 + term2str t' = "tl [c, c_2] from [c, c_2] occur_exactly_in nth_nth 1 [c_2 = 0, c + c_2 = 1]"
3.97 + then ()
3.98 + else error "termC.sml subst_atomic_all should be 'true'";
3.99 +===== inhibit exn AK110721 ============================================================*)
3.100
3.101 + val (all_Free_subst, t') = subst_atomic_all (tl env) t;
3.102 + if not all_Free_subst andalso
3.103 + term2str t' = "tl vs_vs from vs_vs occur_exactly_in nth_nth 1 [c_2 = 0, c + c_2 = 1]" then ()
3.104 + else error "termC.sml subst_atomic_all should be 'false'";
3.105
3.106 "----------- Pattern.match ------------------------------";
3.107 "----------- Pattern.match ------------------------------";
3.108 "----------- Pattern.match ------------------------------";
3.109 -(*===== inhibit exn ============================================================
3.110 -val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
3.111 -val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
3.112 -(* !^^^^^^^^!... necessary for Pattern.match*)
3.113 -val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
3.114 -(*val insts =
3.115 - ([],
3.116 - [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
3.117 - (("a",0),Free ("3","RealDef.real"))])
3.118 - : (indexname * typ) list * (indexname * term) list*)
3.119 +(*===== inhibit exn AK110721 ============================================================
3.120 +(* ERROR: exception Option raised (line 81 of "General/basics.ML")*)
3.121 +(* works without the "^^^2" *)
3.122 +(* exception is called in
3.123 + fun the (SOME x) = x
3.124 + | the NONE = raise Option;
3.125 +*)
3.126 + val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
3.127 + val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
3.128 +===== inhibit exn AK110721 ============================================================*)
3.129
3.130 -"----- throws exn MATCH...";
3.131 -val t = str2term "x";
3.132 -(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))
3.133 -handle MATCH => ([(* (Term.indexname * Term.typ) *)],
3.134 - [(* (Term.indexname * Term.term) *)]);
3.135 -Pattern.MATCH;
3.136 +(*===== inhibit exn AK110721 ============================================================
3.137 + (* !^^^^^^^^!... necessary for Pattern.match*)
3.138 + val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
3.139 + (*val insts =
3.140 + ([],
3.141 + [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
3.142 + (("a",0),Free ("3","RealDef.real"))])
3.143 + : (indexname * typ) list * (indexname * term) list*)
3.144
3.145 -val thy = @{theory "Complex_Main"};
3.146 -val PARSE = Syntax.read_term_global thy;
3.147 -val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real");
3.148 -"-------";
3.149 -val (tye, tme) =
3.150 - (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
3.151 -"-------";
3.152 -val (tye, tme) = Pattern.match thy (Logic.varify_global pa, tm) (Vartab.empty,
3.153 - Vartab.empty);
3.154 -"-------";
3.155 -val (tyenv, tenv) = Pattern.match thy (Logic.varify_global pa, tm)
3.156 - (Vartab.empty, Vartab.empty);
3.157 -Vartab.dest tenv;
3.158 -match thy tm (Logic.varify pa);
3.159 -===== inhibit exn ============================================================*)
3.160 + "----- throws exn MATCH...";
3.161 + val t = str2term "x";
3.162 + (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))
3.163 + handle MATCH => ([(* (Term.indexname * Term.typ) *)],
3.164 + [(* (Term.indexname * Term.term) *)]);
3.165 + Pattern.MATCH;
3.166 +===== inhibit exn AK110721 ============================================================*)
3.167 +
3.168 + val thy = @{theory "Complex_Main"};
3.169 + val PARSE = Syntax.read_term_global thy;
3.170 + val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real");
3.171 + "-------";
3.172 + val (tye, tme) =
3.173 + (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
3.174 + "-------";
3.175 + val (tye, tme) = Pattern.match thy (Logic.varify_global pa, tm) (Vartab.empty,
3.176 + Vartab.empty);
3.177 + "-------";
3.178 + val (tyenv, tenv) = Pattern.match thy (Logic.varify_global pa, tm)
3.179 + (Vartab.empty, Vartab.empty);
3.180 + Vartab.dest tenv;
3.181 +
3.182 +(*===== inhibit exn AK110721 ============================================================
3.183 +(* AK110721
3.184 + Logic.varify should probably be Logic.varify_global*)
3.185 +
3.186 + Pattern.match thy tm (Logic.varify pa);
3.187 +===== inhibit exn AK110721 ============================================================*)
3.188
3.189 "----------- fun matches --------------------------------";
3.190 "----------- fun matches --------------------------------";
3.191 "----------- fun matches --------------------------------";
3.192 -(*test/../Knowledge/polyeq.sml:
3.193 - Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
3.194 -(*test/../Interpret/ptyps.sml:
3.195 - |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
3.196 -val thy = @{theory "Complex_Main"};
3.197 + (*test/../Knowledge/polyeq.sml:
3.198 + Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
3.199 + (*test/../Interpret/ptyps.sml:
3.200 + |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
3.201 +
3.202 + val thy = @{theory "Complex_Main"};
3.203
3.204 "----- test 1: OK";
3.205 -val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*)
3.206 -tracing "paIsa=..."; atomty pa; tracing "...=paIsa";
3.207 + val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*)
3.208 + tracing "paIsa=..."; atomty pa; tracing "...=paIsa";
3.209 (***
3.210 *** Const (op =, real => real => bool)
3.211 *** . Var ((a, 0), real)
3.212 *** . Const (Groups.zero_class.zero, real)
3.213 ***)
3.214 "----- test 1a true";
3.215 -val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"}; (*<<<<<<<---------------*)
3.216 -if matches thy tm pa then ()
3.217 - else error "termC.sml diff.behav. in matches true 1";
3.218 + val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"}; (*<<<<<<<---------------*)
3.219 + if matches thy tm pa then ()
3.220 + else error "termC.sml diff.behav. in matches true 1";
3.221 "----- test 1b false";
3.222 -val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"}; (*<<<<<<<---------------*)
3.223 -if matches thy tm pa then error "termC.sml diff.behav. in matches false 1"
3.224 + val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"}; (*<<<<<<<---------------*)
3.225 + if matches thy tm pa then error "termC.sml diff.behav. in matches false 1"
3.226 else ();
3.227
3.228 "----- test 2: Nok";
3.229 -val pa = Logic.varify_global (str2term "a = (0::real)");(*<<<<<<<-------------*)
3.230 -tracing "paLo2=..."; atomty pa; tracing "...=paLo2";
3.231 + val pa = Logic.varify_global (str2term "a = (0::real)");(*<<<<<<<-------------*)
3.232 + tracing "paLo2=..."; atomty pa; tracing "...=paLo2";
3.233 (***
3.234 *** Const (op =, real => real => bool)
3.235 *** . Var ((a, 0), real)
3.236 *** . Var ((0, 0), real)
3.237 ***)
3.238 "----- test 2a true";
3.239 -val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
3.240 -if matches thy tm pa then ()
3.241 - else error "termC.sml diff.behav. in matches true 2";
3.242 + val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
3.243 + if matches thy tm pa then ()
3.244 + else error "termC.sml diff.behav. in matches true 2";
3.245 "----- test 2b false";
3.246 -val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
3.247 -if matches thy tm pa then ()
3.248 - else error "termC.sml diff.behav. in matches false 2";
3.249 + val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
3.250 + if matches thy tm pa then ()
3.251 + else error "termC.sml diff.behav. in matches false 2";
3.252 (* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!!
3.253 if matches thy tm pa then error "termC.sml diff.behav. in matches false 2"
3.254 else ();*)
3.255
3.256 "----- test 3: OK";
3.257 -val pa = free2var (str2term "a = (0::real)");(*<<<<<<<-------------*)
3.258 -tracing "paF2=..."; atomty pa; tracing "...=paF2";
3.259 + val pa = free2var (str2term "a = (0::real)");(*<<<<<<<-------------*)
3.260 + tracing "paF2=..."; atomty pa; tracing "...=paF2";
3.261 (***
3.262 *** Const (op =, real => real => bool)
3.263 *** . Var ((a, 0), real)
3.264 *** . Free (0, real)
3.265 ***)
3.266 "----- test 3a true";
3.267 -val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
3.268 -if matches thy tm pa then ()
3.269 - else error "termC.sml diff.behav. in matches true 3";
3.270 + val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
3.271 + if matches thy tm pa then ()
3.272 + else error "termC.sml diff.behav. in matches true 3";
3.273 "----- test 3b false";
3.274 -val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
3.275 -if matches thy tm pa then error "termC.sml diff.behav. in matches false 3"
3.276 - else ();
3.277 + val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
3.278 + if matches thy tm pa then error "termC.sml diff.behav. in matches false 3"
3.279 + else ();
3.280
3.281 "----- test 4=3 with specific data";
3.282 -val pa = free2var (str2term "M_b 0");
3.283 + val pa = free2var (str2term "M_b 0");
3.284 "----- test 4a true";
3.285 -val tm = str2term "M_b 0";
3.286 -if matches thy tm pa then ()
3.287 - else error "termC.sml diff.behav. in matches true 4";
3.288 + val tm = str2term "M_b 0";
3.289 + if matches thy tm pa then ()
3.290 + else error "termC.sml diff.behav. in matches true 4";
3.291 "----- test 4b false";
3.292 -val tm = str2term "M_b x";
3.293 -if matches thy tm pa then error "termC.sml diff.behav. in matches false 4"
3.294 - else ();
3.295 + val tm = str2term "M_b x";
3.296 + if matches thy tm pa then error "termC.sml diff.behav. in matches false 4"
3.297 + else ();
3.298
3.299
3.300 "----------- fun parse, fun parse_patt, fun T_a2real ----";
3.301 "----------- fun parse, fun parse_patt, fun T_a2real ----";
3.302 "----------- fun parse, fun parse_patt, fun T_a2real ----";
3.303 (*Makarius.1003
3.304 -ML {* @{term "2::int"} *}
3.305
3.306 -term "(1.24444) :: real"
3.307 + @{term "2::int"}
3.308
3.309 -ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}
3.310 + term "(1.24444) :: real"
3.311
3.312 -Toplevel.debug := true;
3.313 + numbers_to_string @{term "%x. (-9993::int) + x + 1"}
3.314
3.315 -literal types:
3.316 -PolyML.addPrettyPrinter
3.317 + Toplevel.debug := true;
3.318 +
3.319 + literal types:
3.320 + PolyML.addPrettyPrinter
3.321 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
3.322 -*)(* pretty types:
3.323 -PolyML.addPrettyPrinter
3.324 - (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
3.325 -print_depth 99;
3.326 *)
3.327 -val thy = @{theory "Complex_Main"};
3.328 -val str = "x + z";
3.329 -parse thy str;
3.330 +(* pretty types:
3.331 + PolyML.addPrettyPrinter
3.332 + (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
3.333 + print_depth 99;
3.334 +*)
3.335 + val thy = @{theory "Complex_Main"};
3.336 + val str = "x + z";
3.337 + parse thy str;
3.338 "---------------";
3.339 -val str = "x + 2*z";
3.340 -val t = (Syntax.read_term_global thy str);
3.341 -val t = numbers_to_string (Syntax.read_term_global thy str);
3.342 -val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
3.343 -cterm_of thy t;
3.344 -val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
3.345 + val str = "x + 2*z";
3.346 + val t = (Syntax.read_term_global thy str);
3.347 + val t = numbers_to_string (Syntax.read_term_global thy str);
3.348 + val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
3.349 + cterm_of thy t;
3.350 + val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
3.351
3.352 "===== fun parse_patt caused error in fun T_a2real ===";
3.353 -val thy = @{theory "Poly"};
3.354 -parse_patt thy "?p is_addUnordered";
3.355 -parse_patt thy "?p :: real";
3.356 + val thy = @{theory "Poly"};
3.357 + parse_patt thy "?p is_addUnordered";
3.358 + parse_patt thy "?p :: real";
3.359
3.360 "===== extend parse to string with markup===";
3.361 (*
3.362 @@ -224,127 +253,131 @@
3.363 "----------- uminus_to_string ---------------------------";
3.364 "----------- uminus_to_string ---------------------------";
3.365 "----------- uminus_to_string ---------------------------";
3.366 -val t1 = numbers_to_string @{term "-2::real"};
3.367 -val t2 = numbers_to_string @{term "- 2::real"};
3.368 -if uminus_to_string t2 = t1 then ()
3.369 -else error "termC.sml diff.behav. in uminus_to_string";
3.370 + val t1 = numbers_to_string @{term "-2::real"};
3.371 + val t2 = numbers_to_string @{term "- 2::real"};
3.372 + if uminus_to_string t2 = t1
3.373 + then ()
3.374 + else error "termC.sml diff.behav. in uminus_to_string";
3.375
3.376 "----------- *** prep_pbt: syntax error in '#Where' of [v";
3.377 "----------- *** prep_pbt: syntax error in '#Where' of [v";
3.378 "----------- *** prep_pbt: syntax error in '#Where' of [v";
3.379 "===== deconstruct datatype typ ===";
3.380 -val str = "?a";
3.381 -val t = (thy, str) |>> thy2ctxt
3.382 - |-> ProofContext.read_term_pattern
3.383 - |> numbers_to_string;
3.384 -val Var (("a", 0), ty) = t;
3.385 -val TVar ((str, i), srt) = ty;
3.386 -if str = "'a" andalso i = 1 andalso srt = [] then ()
3.387 -else error "termC.sml type-structure of \"?a\" changed";
3.388 + val str = "?a";
3.389 + val t = (thy, str) |>> thy2ctxt
3.390 + |-> ProofContext.read_term_pattern
3.391 + |> numbers_to_string;
3.392 + val Var (("a", 0), ty) = t;
3.393 + val TVar ((str, i), srt) = ty;
3.394 + if str = "'a" andalso i = 1 andalso srt = []
3.395 + then ()
3.396 + else error "termC.sml type-structure of \"?a\" changed";
3.397
3.398 "----- real type in pattern ---";
3.399 -val str = "?a :: real";
3.400 -val t = (thy, str) |>> thy2ctxt
3.401 - |-> ProofContext.read_term_pattern
3.402 - |> numbers_to_string;
3.403 -val Var (("a", 0), ty) = t;
3.404 -val Type (str, tys) = ty;
3.405 -if str = "RealDef.real" andalso tys = [] andalso ty = HOLogic.realT then ()
3.406 -else error "termC.sml type-structure of \"?a :: real\" changed";
3.407 + val str = "?a :: real";
3.408 + val t = (thy, str) |>> thy2ctxt
3.409 + |-> ProofContext.read_term_pattern
3.410 + |> numbers_to_string;
3.411 + val Var (("a", 0), ty) = t;
3.412 + val Type (str, tys) = ty;
3.413 + if str = "RealDef.real" andalso tys = [] andalso ty = HOLogic.realT
3.414 + then ()
3.415 + else error "termC.sml type-structure of \"?a :: real\" changed";
3.416
3.417 "===== Not (matchsub (?a + (?b + ?c)) t_t |... ===";
3.418 -val (thy, str) = (thy, "Not (matchsub (?a + (?b + ?c)) t_t | " ^
3.419 - " matchsub (?a + (?b - ?c)) t_t | " ^
3.420 - " matchsub (?a - (?b + ?c)) t_t | " ^
3.421 - " matchsub (?a + (?b - ?c)) t_t )");
3.422 + val (thy, str) = (thy, "Not (matchsub (?a + (?b + ?c)) t_t | " ^
3.423 + " matchsub (?a + (?b - ?c)) t_t | " ^
3.424 + " matchsub (?a - (?b + ?c)) t_t | " ^
3.425 + " matchsub (?a + (?b - ?c)) t_t )");
3.426 "----- read_term_pattern ---";
3.427 -val t = (thy, str) |>> thy2ctxt
3.428 - |-> ProofContext.read_term_pattern
3.429 - |> numbers_to_string;
3.430 -(*show_types := true; TODO.WN110304 reanimate
3.431 -val t1 = typ_a2real t;
3.432 -if term2str t1 = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
3.433 -then () else error "termC.sml type-structure of \"?a :: real\" changed expl";
3.434 -show_types := false;*)
3.435 + val t = (thy, str) |>> thy2ctxt
3.436 + |-> ProofContext.read_term_pattern
3.437 + |> numbers_to_string;
3.438 +(* TODO.WN110304 reanimate
3.439 + show_types := true;
3.440 + val t1 = typ_a2real t;
3.441 + if term2str t1 = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
3.442 + then () else error "termC.sml type-structure of \"?a :: real\" changed expl";
3.443 + show_types := false;*)
3.444
3.445
3.446
3.447 "----------- check writeln, tracing for string markup ---";
3.448 "----------- check writeln, tracing for string markup ---";
3.449 "----------- check writeln, tracing for string markup ---";
3.450 -val t = @{term "x + 1"};
3.451 -val str_markup = (Syntax.string_of_term
3.452 - (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
3.453 -val str = Print_Mode.setmp [] (Syntax.string_of_term
3.454 - (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
3.455 + val t = @{term "x + 1"};
3.456 + val str_markup = (Syntax.string_of_term
3.457 + (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
3.458 + val str = Print_Mode.setmp [] (Syntax.string_of_term
3.459 + (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
3.460
3.461 -writeln "----------------writeln str_markup---";
3.462 -writeln str_markup;
3.463 -writeln "----------------writeln str---";
3.464 -writeln str;
3.465 -writeln "----------------SAME output: no markup----";
3.466 + writeln "----------------writeln str_markup---";
3.467 + writeln str_markup;
3.468 + writeln "----------------writeln str---";
3.469 + writeln str;
3.470 + writeln "----------------SAME output: no markup----";
3.471
3.472 -writeln "----------------writeln PolyML.makestring str_markup---";
3.473 -writeln (PolyML.makestring str_markup);
3.474 -writeln "----------------writeln PolyML.makestring str---";
3.475 -writeln (PolyML.makestring str);
3.476 -writeln "----------------DIFFERENT output----";
3.477 + writeln "----------------writeln PolyML.makestring str_markup---";
3.478 + writeln (PolyML.makestring str_markup);
3.479 + writeln "----------------writeln PolyML.makestring str---";
3.480 + writeln (PolyML.makestring str);
3.481 + writeln "----------------DIFFERENT output----";
3.482
3.483 -tracing "----------------tracing str_markup---";
3.484 -tracing str_markup;
3.485 -tracing "----------------tracing str---";
3.486 -tracing str;
3.487 -tracing "----------------SAME output: no markup----";
3.488 + tracing "----------------tracing str_markup---";
3.489 + tracing str_markup;
3.490 + tracing "----------------tracing str---";
3.491 + tracing str;
3.492 + tracing "----------------SAME output: no markup----";
3.493
3.494 -tracing "----------------writeln PolyML.makestring str_markup---";
3.495 -tracing (PolyML.makestring str_markup);
3.496 -tracing "----------------writeln PolyML.makestring str---";
3.497 -tracing (PolyML.makestring str);
3.498 -tracing "----------------DIFFERENT output----";
3.499 + tracing "----------------writeln PolyML.makestring str_markup---";
3.500 + tracing (PolyML.makestring str_markup);
3.501 + tracing "----------------writeln PolyML.makestring str---";
3.502 + tracing (PolyML.makestring str);
3.503 + tracing "----------------DIFFERENT output----";
3.504 (*
3.505 -redirect_tracing "/home/neuper/tmp/trace.sml";
3.506 -tracing "----------------writeln str_markup---";
3.507 -tracing str_markup;
3.508 -tracing "----------------writeln str---";
3.509 -tracing str;
3.510 -tracing "----------------DIFFERENT output----";
3.511 + redirect_tracing "/home/neuper/tmp/trace.sml";
3.512 + tracing "----------------writeln str_markup---";
3.513 + tracing str_markup;
3.514 + tracing "----------------writeln str---";
3.515 + tracing str;
3.516 + tracing "----------------DIFFERENT output----";
3.517 *)
3.518
3.519 "----------- check writeln, tracing for string markup ---";
3.520 -val t = @{term "x + 1"};
3.521 -val str_markup = (Syntax.string_of_term
3.522 - (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
3.523 -val str = Print_Mode.setmp [] (Syntax.string_of_term
3.524 - (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
3.525 + val t = @{term "x + 1"};
3.526 + val str_markup = (Syntax.string_of_term
3.527 + (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
3.528 + val str = Print_Mode.setmp [] (Syntax.string_of_term
3.529 + (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
3.530
3.531 -writeln "----------------writeln str_markup---";
3.532 -writeln str_markup;
3.533 -writeln "----------------writeln str---";
3.534 -writeln str;
3.535 -writeln "----------------SAME output: no markup----";
3.536 + writeln "----------------writeln str_markup---";
3.537 + writeln str_markup;
3.538 + writeln "----------------writeln str---";
3.539 + writeln str;
3.540 + writeln "----------------SAME output: no markup----";
3.541
3.542 -writeln "----------------writeln PolyML.makestring str_markup---";
3.543 -writeln (PolyML.makestring str_markup);
3.544 -writeln "----------------writeln PolyML.makestring str---";
3.545 -writeln (PolyML.makestring str);
3.546 -writeln "----------------DIFFERENT output----";
3.547 + writeln "----------------writeln PolyML.makestring str_markup---";
3.548 + writeln (PolyML.makestring str_markup);
3.549 + writeln "----------------writeln PolyML.makestring str---";
3.550 + writeln (PolyML.makestring str);
3.551 + writeln "----------------DIFFERENT output----";
3.552
3.553 -tracing "----------------tracing str_markup---";
3.554 -tracing str_markup;
3.555 -tracing "----------------tracing str---";
3.556 -tracing str;
3.557 -tracing "----------------SAME output: no markup----";
3.558 + tracing "----------------tracing str_markup---";
3.559 + tracing str_markup;
3.560 + tracing "----------------tracing str---";
3.561 + tracing str;
3.562 + tracing "----------------SAME output: no markup----";
3.563
3.564 -tracing "----------------writeln PolyML.makestring str_markup---";
3.565 -tracing (PolyML.makestring str_markup);
3.566 -tracing "----------------writeln PolyML.makestring str---";
3.567 -tracing (PolyML.makestring str);
3.568 -tracing "----------------DIFFERENT output----";
3.569 + tracing "----------------writeln PolyML.makestring str_markup---";
3.570 + tracing (PolyML.makestring str_markup);
3.571 + tracing "----------------writeln PolyML.makestring str---";
3.572 + tracing (PolyML.makestring str);
3.573 + tracing "----------------DIFFERENT output----";
3.574 (*
3.575 -redirect_tracing "/home/neuper/tmp/trace.sml";
3.576 -tracing "----------------writeln str_markup---";
3.577 -tracing str_markup;
3.578 -tracing "----------------writeln str---";
3.579 -tracing str;
3.580 -tracing "----------------DIFFERENT output----";
3.581 + redirect_tracing "/home/neuper/tmp/trace.sml";
3.582 + tracing "----------------writeln str_markup---";
3.583 + tracing str_markup;
3.584 + tracing "----------------writeln str---";
3.585 + tracing str;
3.586 + tracing "----------------DIFFERENT output----";
3.587 *)
4.1 --- a/test/Tools/isac/ProgLang/tools.sml Thu Jul 21 12:01:56 2011 +0200
4.2 +++ b/test/Tools/isac/ProgLang/tools.sml Thu Jul 21 16:57:21 2011 +0200
4.3 @@ -1,12 +1,8 @@
4.4 -(* tests on Tools
4.5 - author: Walther Neuper
4.6 - WN071229,
4.7 +(* Title: tests on Tools
4.8 + Author: Walther Neuper WN071229,
4.9 (c) due to copyright terms
4.10 -
4.11 -use"../smltest/Scripts/tools.sml";
4.12 -use"tools.sml";
4.13 *)
4.14 -val thy = Real.thy;
4.15 +val thy = @{theory "Real"};
4.16
4.17 "-----------------------------------------------------------------";
4.18 "table of contents -----------------------------------------------";
4.19 @@ -25,3 +21,4 @@
4.20
4.21 if matchsub thy (str2term "(a + (b + c)) + d") (str2term "?x + (?y + ?z)")
4.22 then () else error "tools.sml matchsub (a + (b + c)) + d";
4.23 +
5.1 --- a/test/Tools/isac/Test_Isac.thy Thu Jul 21 12:01:56 2011 +0200
5.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Jul 21 16:57:21 2011 +0200
5.3 @@ -101,8 +101,8 @@
5.4 use "ProgLang/calculate.sml" (*part.*)
5.5 use "ProgLang/rewrite.sml" (*part.*)
5.6 (*use "ProgLang/listg.sml" 2002*)
5.7 -(*use "ProgLang/scrtools.sml" 2002*)
5.8 -(*use "ProgLang/tools.sml" 2002*)
5.9 + use "ProgLang/scrtools.sml" (*complete*)
5.10 + use "ProgLang/tools.sml" (*complete*)
5.11 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
5.12 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
5.13 use "Minisubpbl/000-comments.sml"
5.14 @@ -124,7 +124,7 @@
5.15 use "Interpret/calchead.sml" (*! *)
5.16 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*)
5.17 use "Interpret/rewtools.sml" (*! *)
5.18 - use "Interpret/script.sml" (*!TODO*)
5.19 + use "Interpret/script.sml" (*!TODO/part*)
5.20 (*use "Interpret/solve.sml" !TODO*)
5.21 (*use "Interpret/inform.sml" !TODO*)
5.22 use "Interpret/mathengine.sml" (*!part.*)
6.1 --- a/test/Tools/isac/Test_Some.thy Thu Jul 21 12:01:56 2011 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Thu Jul 21 16:57:21 2011 +0200
6.3 @@ -7,17 +7,19 @@
6.4
6.5 ML{* writeln "**** run the test ***************************************" *}
6.6
6.7 -use"../../../test/Tools/isac/Frontend/interface.sml"
6.8 +use"../../../test/Tools/isac/Interpret/script.sml"
6.9
6.10 ML{*
6.11
6.12
6.13 -*}
6.14 -ML{*
6.15 +
6.16
6.17 *}
6.18 ML{*
6.19 -
6.20 +*}
6.21 +ML{*
6.22 +*}
6.23 +ML{*
6.24 *}
6.25 ML{*
6.26 *}