wneuper/isa: comparison test/Tools/isac/Knowledge/polyeq-1.sml

equal deleted inserted replaced

-:59106f9e08cc
+:e96abd81a321
 "-----------------------------------------------------------------";
 "------ polyeq- 1.sml ---------------------------------------------";
 "----------- tests on predicates in problems ---------------------";
 "----------- test matching problems ------------------------------";
 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
+"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
 "----------- lin.eq degree_0 -------------------------------------";
 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
 "-----------------------------------------------------------------";
 "----------- tests on predicates in problems ---------------------";
 "----------- tests on predicates in problems ---------------------";
 "----------- tests on predicates in problems ---------------------";
-Rewrite.trace_on:=true;  (*true false*)
+Rewrite.trace_on:=false;  (*true false*)
 val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
-if ((UnparseC.term t) = "-8 - 2 * x + x \<up> 2") then ()
+if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
 else  error "polyeq.sml: diff.behav. in lhs";
 val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
 if (UnparseC.term t) = "True" then ()
 	      "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
 if (UnparseC.term t) = "False" then ()
 else  error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
 val t5 = (Thm.term_of o the o (TermC.parse thy))
 	      "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
 if (UnparseC.term t) = "True" then ()
 else  error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
 val t = (Thm.term_of o the o (parseold thy)) "7";
 ##################################################################################*)
+"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
+"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
+"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
+(* termorder hacked by MG, adapted later by WN *)
+(** )local ( *. for make_polynomial_in .*)
+open Term;  (* for type order = EQUAL | LESS | GREATER *)
+fun pr_ord EQUAL = "EQUAL"
+| pr_ord LESS  = "LESS"
+| pr_ord GREATER = "GREATER";
+fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
+| dest_hd' x (t as Free (a, T)) =
+if x = t then ((("|||||||||||||", 0), T), 0)                        (*WN*)
+else (((a, 0), T), 1)
+| dest_hd' _ (Var v) = (v, 2)
+| dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
+| dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
+| dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
+fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
+Free (var, _) $ Free (pot, _)) =
+(if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
+case x of                                                          (*WN*)
+	    (Free (xstr, _)) =>
+		    if xstr = var
+then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
+1000 * (the (TermC.int_opt_of_string pot)))
+else (if pr then tracing (idt "#" i ^ "x <> Free  --> " ^ "3") else (); 3)
+	  | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
+| size_of_term' i pr x (t as Abs (_, _, body)) =
+(if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
+1 + size_of_term' (i + 1) pr x body)
+| size_of_term' i pr x (f $ t) =
+let
+val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
+val s1 = size_of_term' (i + 1) pr x f
+val s2 = size_of_term' (i + 1) pr x t
+val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
+in (s1 + s2) end
+| size_of_term' i pr x t =
+(if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
+case t of
+Free (subst, _) =>
+(case x of
+	     Free (xstr, _) =>
+if xstr = subst
+then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
+else (if pr then tracing (idt "#" i ^ "x <> Free  --> " ^ "1") else (); 1)
+	   | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
+| _ => (if pr then tracing (idt "#" i ^ "bot        --> " ^ "1") else (); 1));
+fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)
+let
+val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
+val ord =
+case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
+val _  = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
+in ord end
+| term_ord' i pr x _ (t, u) =
+let
+val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
+val ord =
+	  case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
+	    EQUAL =>
+	      let val (f, ts) = strip_comb t and (g, us) = strip_comb u
+in
+	        (case hd_ord (i + 1) pr x (f, g) of
+	           EQUAL => (terms_ord x (i + 1) pr) (ts, us)
+	         | ord => ord)
+	      end
+	  | ord => ord
+val _  = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
+in ord end
+and hd_ord i pr x (f, g) =                                        (* ~ term.ML *)
+let
+val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
+val ord = prod_ord
+(prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
+(dest_hd' x f, dest_hd' x g)
+val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
+in ord end
+and terms_ord x i pr (ts, us) =
+let
+val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
+val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
+val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
+in ord end
+(** )in( *local*)
+fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
+((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
+	case subst of
+	  (_, x) :: _ =>
+term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
+	| _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
+(** )end;( *local*)
+\<close> ML \<open>
+val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
+if ord_make_polynomial_in true @{theory} subs (t1, t2) then ()  else error "still GREATER?";
+val x = TermC.str2term "x ::real";
+val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
+if 2006 = size_of_term' 1 true x t1
+then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
+val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
+if 3004 = size_of_term' 1 true x t2
+then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
 val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
 val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
 val ppp  = (Thm.term_of o the o (TermC.parse thy)) ppp';
 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
-if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
+if UnparseC.term t' = "- 6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
-if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
+if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2 + 0" then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
-val ttt' = "(3*x + 5)/18";
+val ttt' = "(3*x + 5)/18 ::real";
 val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
 (*============ inhibit exn WN120316 ==============================================
 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
-============ inhibit exn WN120316 ==============================================*)
 "----------- lin.eq degree_0 -------------------------------------";
 "----------- lin.eq degree_0 -------------------------------------";
 "----------- lin.eq degree_0 -------------------------------------";

changeset 60342	e96abd81a321
parent 60340	0ee698b0a703
child 60344	f0a87542dae0