wneuper/isa: comparison test/Tools/isac/MathEngBasic/rewrite.sml

equal deleted inserted replaced

-:bb153a08645b
+:d77aa0992e0f
 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
 (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
 "----- step 1: LHS, RHS of rule";
 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
 o Logic.strip_imp_concl) r;
-UnparseC.term2str r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
+UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
-UnparseC.term2str LHS = "?b / (?a * ?b)"; UnparseC.term2str RHS = "(1::?'a) / ?a";
+UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term RHS = "(1::?'a) / ?a";
 "----- step 2: the rule instantiated";
 val r' = Envir.subst_term
 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
-UnparseC.term2str r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
+UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
 "----- step 3: get the (instantiated) assumption(s)";
 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
-UnparseC.term2str (hd p') = "x \<noteq> 0";
+UnparseC.term (hd p') = "x \<noteq> 0";
 "=====vvv make asms without Trueprop ---vvv";
 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
 (Logic.count_prems r', [], r'));
 case p' of
 [Const ("HOL.Not", _) $ (Const ("HOL.eq", _)
 | _ => error "rewrite.sml assumption changed";
 "=====^^^ make asms without Trueprop ---^^^";
 "----- step 4: get the (instantiated) RHS";
 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
 o Logic.strip_imp_concl) r';
-UnparseC.term2str t' = "1 / 2";
+UnparseC.term t' = "1 / 2";
 "----------- step through 'fun rewrite_terms_'  ---------";
 "----------- step through 'fun rewrite_terms_'  ---------";
 "----------- step through 'fun rewrite_terms_'  ---------";
 "----- step 0: args for rewrite_terms_, local fun";
 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
 writeln "----------- rewrite_terms_  1---------------------------";
-if UnparseC.term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
+if UnparseC.term t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
 else error "rewrite.sml rewrite_terms_ [x = 0]";
 val equs = [str2term "M_b 0 = 0"];
 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
 writeln "----------- rewrite_terms_  2---------------------------";
-if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
+if UnparseC.term t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
 val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
 writeln "----------- rewrite_terms_  3---------------------------";
-if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
+if UnparseC.term t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
 "----------- rewrite_inst_ bdvs -------------------------";
 "----------- rewrite_inst_ bdvs -------------------------";
 			      [(Num_Calc ("EqSystem.occur'_exactly'_in",
 				      eval_occur_exactly_in
 					  "#eval_occur_exactly_in_"))
 			       ])
 		  false bdvs (num_str @{separate_bdvs_add) t;
-(writeln o UnparseC.term2str) t;
+(writeln o UnparseC.term) t;
-if UnparseC.term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
+if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
 then () else error "rewrite.sml rewrite_inst_ bdvs";
 > trace_rewrite:=true;
 trace_rewrite:=false;--------------------------------------------*)
 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
 val subs = [(@{term "bdv"}, @{term  "x"})];
 val rls = norm_Rational_noadd_fractions;
 val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
-if UnparseC.term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x ^^^ 2 / 2)" andalso
+if UnparseC.term t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x ^^^ 2 / 2)" andalso
-UnparseC.terms2str asms = "[]" then {}
+UnparseC.terms asms = "[]" then {}
 else error "this was NONE with Isabelle2013-2 ?!?"
 "----- rewrite_ rat_mult_poly_r--------------------------";
 val thm = @{thm rat_mult_poly_r};
 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
 val erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
 writeln "===== maximally simplified example =====================";
 val t = @{term "a / b * (x / x ^^^ 2)"};
 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
-UnparseC.term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
+UnparseC.term t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
 (*checked visually: trace_rewrite looks like above for 2009*)
 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
 (*t' = t''; (*false because of further rewrites in t'*)*)
 val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
 val precond = parse_patt thy "(?l::real) is_expanded";
 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
 val preinst = Envir.subst_term inst precond;
-UnparseC.term2str preinst;
+UnparseC.term preinst;
 "===== Rational.thy: cancel ===";
 (* pat matched with the current term gives an environment
 (or not: hen the Rrls not applied);
 if pre1 and pre2 evaluate to @{term True} in this environment,
 val erls = rational_erls;
 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
 val asms = map (Envir.subst_term subst) pres;
-if UnparseC.terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
+if UnparseC.terms asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
 then () else error "rewrite.sml: prepat cancel subst";
 if ([], true) = eval__true thy 0 asms [] erls
 then () else error "rewrite.sml: prepat cancel eval__true";
 "===== Rational.thy: add_fractions_p ===";
 		      [Num_Calc ("Poly.is'_multUnordered",
 eval_is_multUnordered "")];
 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
 val asms = map (Envir.subst_term subst) pres;
-if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
+if UnparseC.terms asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
 then () else error "rewrite.sml: prepat order_mult_ subst";
 if ([], true) = eval__true thy 0 asms [] erls
 then () else error "rewrite.sml: prepat order_mult_ eval__true";
 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
 tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := false;
 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
 tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
-if UnparseC.term2str t' = "x * x ^^^ 2" then ()
+if UnparseC.term t' = "x * x ^^^ 2" then ()
 else error "rewrite.sml Poly.is'_multUnordered doesn't work";
 (* for achieving the previous result, the following code was taken apart *)
 "----- rewrite__set_ ---";
 val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
 	    in scan_ chk prepat end;
 	(*.apply the normal_form of a rev-set.*)
 	fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
 	    if chk_prepat thy erls prepat t
-	    then ((*tracing("### app_rev': t = "^(UnparseC.term2str t));*)
+	    then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)
 normal_form t)
 	    else NONE;
 (*fixme val NONE = app_rev' thy rrls t;*)
 "----- app_rev' ---";
 val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
 					    (Vartab.empty, Vartab.empty);
 (*fixme: asms = ["p is_multUnordered"]...instantiate*)
 "----- eval__true ---";
 val asms = (map (Envir.subst_term subst) pres);
-if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
+if UnparseC.terms asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
 else error "rewrite.sml: diff. is_multUnordered, asms";
 val (thy, i, asms, bdv, rls) =
 (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
 [] : (term * term) list, erls);
 case eval__true thy i asms bdv rls of
 (trace1 i (" try thm: " ^ thmid);
 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
 NONE => rew_once ruls asm ct apno thms
 | SOME (ct', asm') =>
-(trace1 i (" rewrites to: " ^ UnparseC.t2str thy ct');
+(trace1 i (" rewrites to: " ^ UnparseC.term_thy thy ct');
 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
 (* once again try the same rule, e.g. associativity against "()"*)
 | Rule.Num_Calc (cc as (op_, _)) =>
 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
 | SOME (_, thm') =>
 let
 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
-Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
+Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.term_thy thy ct ^ " = NONE")
-val _ = trace1 i (" calc. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
+val _ = trace1 i (" calc. to: " ^ UnparseC.term_thy thy ((fst o the) pairopt))
 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
 end
 | Rule.Cal1 (cc as (op_, _)) =>
 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
 val ct = TermC.uminus_to_string ct
 | SOME (_, thm') =>
 let
 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
-Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
+Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.term_thy thy ct ^ " = NONE")
-val _ = trace1 i (" cal1. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
+val _ = trace1 i (" cal1. to: " ^ UnparseC.term_thy thy ((fst o the) pairopt))
 in the pairopt end
 end
 | Rule.Rls_ rls' =>
 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
 | NONE => rew_once ruls asm ct apno thms)
 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
 val ruls = (#rules o Rule.Rule_Set.rep) rls;
-(*    val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.t2str thy ct)*)
+(*    val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_thy thy ct)*)
 val (ct', asm') = rew_once ruls [] ct Noap ruls;
 "~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
 = (ruls, []:term list, ct, Noap, ruls);
 val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
 = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
 		  (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm), ct);
 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
 ;
-(*+*)if UnparseC.term2str r' =
+(*+*)if UnparseC.term r' =
 (*+*)  "\<lbrakk>9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
 (*+*)  "\<Longrightarrow> ((3 + -1 * x + x ^^^ 2) /\n" ^
 (*+*)  "                   (9 * x + -6 * x ^^^ 2 + x ^^^ 3) =\n" ^
 (*+*)  "                   1 / x) =\n" ^
 (*+*)  "                  ((3 + -1 * x + x ^^^ 2) * x =\n" ^
 (*+*)  "                   1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3))"
 (*+*)then () else error "instantiated rule CHANGED";
 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
 ;
-(*+*)if map UnparseC.term2str p' = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
+(*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
 (*+*)then () else error "stored assumptions CHANGED";
 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
 ;
-(*+*)if UnparseC.term2str t' = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
+(*+*)if UnparseC.term t' = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
 (*+*)then () else error "rewritten term (an equality) CHANGED";
 val (simpl_p', nofalse) =
 eval__true thy (i + 1) p' bdv rls;
 "~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
 (*if*) asms = [@{term True}] orelse asms = [] (*else*);
-(*+*)if map UnparseC.term2str asms = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
+(*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
 (*+*)then () else error "asms before chk CHANGED";
 fun chk indets [] = (indets, true) (*return asms<>True until false*)
 | chk indets (a :: asms) =
 (case rewrite__set_ thy (i + 1) false bdv rls a of
 (*this was False; vvvv--- means: indeterminate*)
 val (* SOME (t, a') *)NONE = (*case*)
 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
-(*+*)UnparseC.term2str a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
+(*+*)UnparseC.term a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
 (*
 :
 ####  rls: rateq_erls on: x \<noteq> 0
 :
 #####  try calc: HOL.eq'    <<<------------------------------- here the error comes from
 val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
 val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
 ;
-if UnparseC.term2str lhss = "?a * (?b + ?c)" andalso UnparseC.term2str t = "x * (y + z)" then ()
+if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()
 else error "ARGS FOR Pattern.match CHANGED";
 val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
-if (Envir.subst_term match r |> UnparseC.term2str) = "x * (y + z) = x * y + x * z" then ()
+if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
 else error "Pattern.match CHANGED";
 "----------- fun mk_thm ------------------------------------------------------------------------";
 "----------- fun mk_thm ------------------------------------------------------------------------";
 "----------- fun mk_thm ------------------------------------------------------------------------";
 case parse thy term_str of
 NONE => ()
 | _ => writeln "parse does NOT take patterns with '?'";
 val t1 = (#prop o Thm.rep_thm) (num_str thm);
-if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
+if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
 val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
 if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
 (mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
 case parse thy term_str of
 NONE => ()
 | _ => writeln "parse does NOT take patterns with '?'";
 val t1 = (#prop o Thm.rep_thm) (num_str thm);
-if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
+if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
 val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
 if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
 (mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
 val thy = @{theory};
 val rls = norm_equation;
 val term = str2term "x + 1 = 2";
 val SOME (t, asm) = rewrite_set_ thy false rls term;
-if UnparseC.term2str t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
+if UnparseC.term t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
 "~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);

changeset 59868	d77aa0992e0f
parent 59867	bb153a08645b
child 59870	0042fe0bc764