wneuper/isa: comparison test/Tools/isac/ProgLang/evaluate.sml

equal deleted inserted replaced

-:17db21aa9aed
+:73ee61385493
 "----------- fun calculate_ --------------------------------------------------------------------";
 "----------- fun calculate_ --------------------------------------------------------------------";
 "----------- fun calculate_ --------------------------------------------------------------------";
 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
-val t = TermC.str2term "((1+2)*4/3)^^^2";
+val t = TermC.str2term "((1+2)*4/3) \<up> 2";
 val thy = @{theory};
 val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
 val plus =   ("Groups.plus_class.plus",eval_binop "#add_") : string * Eval_Def.eval_fn;
 val divide = ("Rings.divide_class.divide"  ,eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
 val pow =    ("Prog_Expr.pow"  ,eval_binop "#power_") : string * Eval_Def.eval_fn;
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t);
 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
 val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
-if UnparseC.term t' = "(3 * 4 / 3) ^^^ 2" then () else error "calculate_  1 + 2 = 3  changed";
+if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_  1 + 2 = 3  changed";
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
 val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
-if UnparseC.term t'' = "(12 / 3) ^^^ 2" then () else error "calculate_  3 * 4 = 12  changed";
+if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_  3 * 4 = 12  changed";
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
 val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
-if UnparseC.term t''' = "4 ^^^ 2" then () else error "calculate_  12 / 3 = 4  changed";
+if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_  12 / 3 = 4  changed";
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
-val SOME ("#: 4 ^^^ 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
+val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
 val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
 if UnparseC.term t'''' = "16" then () else error "calculate_  12 / 3 = 4  changed";
 "----------- calculate from Prog --------------------------------- -----------------------------";
 "----------- calculate from Prog --------------------------------- -----------------------------";
 "----------- calculate from Prog --------------------------------- -----------------------------";
 val thy = @{theory "Test"};
-val fmz = ["realTestGiven (((1+2)*4/3)^^^2)", "realTestFind s"];
+val fmz = ["realTestGiven (((1+2)*4/3) \<up> 2)", "realTestFind s"];
 val (dI',pI',mI') =
 ("Test",["calculate", "test"],["Test", "test_calculate"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)
+(*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3)  \<up> #2)")*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "----------- calculate check test-root-equ --------------";
 "----------- calculate check test-root-equ --------------";
 "----------- calculate check test-root-equ --------------";
 (*(1): 2nd Test_simplify didn't work:
 val ct =
-"sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
+"sqrt (x \<up> 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
 > val rls = ("Test_simplify");
 > val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
-val ct = "sqrt (x ^^^ 2 + -3 * x) =
+val ct = "sqrt (x \<up> 2 + -3 * x) =
 (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
 ie. cancel does not work properly
 *)
 val thy = @{theory "Test"};
 val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
 val ct = ThmC_Def.num_to_Free @{term
-"sqrt (x ^^^ 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};
+"sqrt (x \<up> 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};
 case calculate_ thy op_ ct of
 SOME _ => ()
 | NONE => error "calculate_ test-root-equ changed";
 (*
-sqrt (x ^^^ 2 + -3 * x) =\
+sqrt (x \<up> 2 + -3 * x) =\
 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
 ............... does not work *)
 (*--------------(2): does divide work in Test_simplify ?: ------*)
 val thy = @{theory Test};
 (*** -------------
 *** Const ( Nat.power, ['a, nat] => 'a)
 *** . Free ( 1, 'a)
 *** . Free ( aaa, nat) *)
-val t = TermC.str2term "1 ^^^ aaa";
+val t = TermC.str2term "1 \<up> aaa";
 TermC.atomty t;
 (****
 *** Const (Prog_Expr.pow, real => real => real)
 *** . Free (1, real)
 *** . Free (aaa, real)
 val t = (Thm.term_of o the o (TermC.parse thy)) "12 / 3";
 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
 "12 / 3 = 4";
 val thy = @{theory Test};
-val t = (Thm.term_of o the o (TermC.parse thy)) "4 ^^^ 2";
+val t = (Thm.term_of o the o (TermC.parse thy)) "4 \<up> 2";
 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
 "4 ^ 2 = 16";
-val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
+val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) \<up> 2";
 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
 "1 + 2 = 3";
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
 UnparseC.term t;
-"(3 * 4 / 3) ^^^ 2";
+"(3 * 4 / 3) \<up> 2";
 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
 "3 * 4 = 12";
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
 UnparseC.term t;
-"(12 / 3) ^^^ 2";
+"(12 / 3) \<up> 2";
 val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
 "12 / 3 = 4";
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
 UnparseC.term t;
-"4 ^^^ 2";
+"4 \<up> 2";
 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
-"4 ^^^ 2 = 16";
+"4 \<up> 2 = 16";
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
 UnparseC.term t;
 "16";
 if it <> "16" then error "evaluate.sml: new behaviour in calculate_"
 else ();
 (*13.9.02 *** calc: operator = pow not defined*)
-val t = (Thm.term_of o the o (TermC.parse thy)) "3^^^2";
+val t = (Thm.term_of o the o (TermC.parse thy)) "3 \<up> 2";
 val SOME (thmID,thm) =
 adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
 (*** calc: operator = pow not defined*)
 val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
 "----------- get_pair with 3 args --------------------------------";
 val (thy, op_, ef, arg) =
 (thy, "EqSystem.occur'_exactly'_in",
 assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,
 TermC.str2term
-"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
+"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L \<up> 2) / 2"
 );
 val SOME (str, simpl) = get_pair thy op_ ef arg;
 if str =
-"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
+"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L \<up> 2) / 2 = True"
 then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
 "----------- calculate (2 * x is_const) -----------------";
 "----------- calculate (2 * x is_const) -----------------";
 if str =  "#divide_e-4_-2" andalso UnparseC.term term = "-4 / -2 = 2"
 then () else error "get_pair  -4 / -2   changed";
 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
-val t = (Thm.term_of o the o (TermC.parse thy)) "2 ^^^ 3";
+val t = (Thm.term_of o the o (TermC.parse thy)) "2 \<up> 3";
 val SOME (str, term) = get_pair thy isa_str eval_fn t;
-if str =  "#: 2 ^^^ 3 = 8" andalso UnparseC.term term = "2 ^^^ 3 = 8"
+if str =  "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8"
-then () else error "get_pair  2 ^^^ 3   changed";
+then () else error "get_pair  2 \<up> 3   changed";
 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
 (*--------------------------------------------------------------------vvvvvvvvvv*)

changeset 60242	73ee61385493
parent 60230	0ca0f9363ad3
child 60270	844610c5c943