1.1 --- a/src/smltest/IsacKnowledge/polyminus.sml	Thu Dec 27 15:20:44 2007 +0100
     1.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml	Thu Dec 27 17:44:23 2007 +0100
     1.3 @@ -6,13 +6,15 @@
     1.4  use"../smltest/IsacKnowledge/polyminus.sml";
     1.5  use"polyminus.sml";
     1.6  *)
     1.7 -val thy = EqSystem.thy;
     1.8 +val thy = PolyMinus.thy;
     1.9  
    1.10  "-----------------------------------------------------------------";
    1.11  "table of contents -----------------------------------------------";
    1.12  "-----------------------------------------------------------------";
    1.13  "----------- watch order_add_mult  -------------------------------";
    1.14  "----------- build predicate for +- ordering ---------------------";
    1.15 +"----------- build fasse_zuswammen -------------------------------";
    1.16 +"----------- build verschoenere ----------------------------------";
    1.17  "-----------------------------------------------------------------";
    1.18  "-----------------------------------------------------------------";
    1.19  "-----------------------------------------------------------------";
    1.20 @@ -23,6 +25,7 @@
    1.21  "----------- watch order_add_mult  -------------------------------";
    1.22  "----- with these simple variables it works...";
    1.23  trace_rewrite:=true;
    1.24 +trace_rewrite:=false;
    1.25  val t = str2term "((a + d) + c) + b";
    1.26  val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
    1.27  if term2str t = "a + (b + (c + d))" then ()
    1.28 @@ -69,7 +72,6 @@
    1.29  (*@@@ rew_sub gosub: t = d + (b + a + c)
    1.30    @@@ rew_sub begin: t = b + a + c*)
    1.31  
    1.32 -(*#####################################################################
    1.33  
    1.34  "----------- build predicate for +- ordering ---------------------";
    1.35  "----------- build predicate for +- ordering ---------------------";
    1.36 @@ -91,16 +93,22 @@
    1.37      Some ("a kleiner b = True", _) => ()
    1.38    | _ => raise error "polyminus.sml: a kleiner b = True";
    1.39  
    1.40 -"----- test rewrite_, rewrite_set_";
    1.41 +"----- compare tausche_plus with real_num_collect";
    1.42  val od = dummy_ord;
    1.43 +
    1.44  val erls = erls_ordne_alphabetisch;
    1.45  val t = str2term "b + a";
    1.46 -"############################################";
    1.47  val Some (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t;
    1.48  if term2str t = "a + b" then ()
    1.49  else raise error "polyminus.sml: ordne_alphabetisch1 b + a";
    1.50  
    1.51 +val erls = Atools_erls;
    1.52 +val t = str2term "2*a + 3*a";
    1.53 +val Some (t,_) = rewrite_ thy od erls false real_num_collect t; term2str t;
    1.54 +
    1.55 +"----- test rewrite_, rewrite_set_";
    1.56  trace_rewrite:=true;
    1.57 +val erls = erls_ordne_alphabetisch;
    1.58  val t = str2term "b + a";
    1.59  val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
    1.60  if term2str t = "a + b" then ()
    1.61 @@ -136,14 +144,31 @@
    1.62  "----- compile rls for the most complicated terms";
    1.63  val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
    1.64  "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
    1.65 -val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
    1.66 -"5 * e - 8 * g + 6 * f - 9 - 7 * e + 10 * g - 4 * f + 12";
    1.67 +val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; 
    1.68 +if term2str t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
    1.69 +then () else raise error "polyminus.sml: ordne_alphabetisch finished";
    1.70  
    1.71  
    1.72 +"----------- build fasse_zuswammen -------------------------------";
    1.73 +"----------- build fasse_zuswammen -------------------------------";
    1.74 +"----------- build fasse_zuswammen -------------------------------";
    1.75 +val t = str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
    1.76 +val Some (t,_) = rewrite_set_ thy false fasse_zusammen t;
    1.77 +if term2str t = "3 + -2 * e + 2 * f + 2 * g" then ()
    1.78 +else raise error "polyminus.sml: fasse_zusammen finished";
    1.79 +
    1.80 +"----------- build verschoenere ----------------------------------";
    1.81 +"----------- build verschoenere ----------------------------------";
    1.82 +"----------- build verschoenere ----------------------------------";
    1.83 +val t = str2term "3 + -2 * e + 2 * f + 2 * g";
    1.84 +val Some (t,_) = rewrite_set_ thy false verschoenere t;
    1.85 +if term2str t = "3 - 2 * e + 2 * f + 2 * g" then ()
    1.86 +else raise error "polyminus.sml: verschoenere 3 + -2 * e ...";
    1.87 +
    1.88 +trace_rewrite:=true;
    1.89  trace_rewrite:=false;
    1.90  (*
    1.91  use"../smltest/IsacKnowledge/polyminus.sml";
    1.92  use"polyminus.sml";
    1.93    *)
    1.94  
    1.95 -#####################################################################*)