wneuper/isa: comparison test/Tools/isac/ProgLang/prog

equal deleted inserted replaced

-:873f40b097bb
+:c4b24621077e
 "-------- fun eval_is_even ---------------------------------------------------------------------";
 "-------- fun eval_is_even ---------------------------------------------------------------------";
 "-------- fun eval_is_even ---------------------------------------------------------------------";
-val t = TermC.parse_test @{context} "2 is_even";
+val t = ParseC.parse_test @{context} "2 is_even";
 eval_is_even "aaa" "Prog_Expr.is_even" t "ccc";
 "~~~~~ fun eval_is_even , args:"; val ((thmid:string), "Prog_Expr.is_even", (t as (Const _ $ arg)), _) =
 ("aaa", "Prog_Expr.is_even", t, "ccc");
 (*if*) TermC.is_num arg (*then*);
 val i = arg |> HOLogic.dest_number |> snd;
 SOME (TermC.mk_thmid thmid (string_of_int n) "",
 				  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})));
 if UnparseC.term t' = "(2 is_even) = True" then () else error "(2 is_even) = True  CHANGED";
-val t = TermC.parse_test @{context} "3 is_even";
+val t = ParseC.parse_test @{context} "3 is_even";
 case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of
 SOME (str, t') =>
 if str = "aaa_" andalso UnparseC.term t' = "(3 is_even) = False" then ()
 else error "eval_is_even (3 is_even) CHANGED 1"
 | NONE => error "eval_is_even (3 is_even) CHANGED 2";
-val t = TermC.parse_test @{context} "a ::real";
+val t = ParseC.parse_test @{context} "a ::real";
 val NONE =
 eval_is_even "aaa" "Prog_Expr.is_even" t "ccc";
 case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of
 SOME _ => error "eval_is_even (a is_even) CHANGED"
 | NONE => ();
 val t = TermC.parseNEW' ctxt "2 is_num";
 case rewrite_set_ ctxt false tval_rls t of
 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
 | _ => error "2 is_num CHANGED";
-val t = TermC.parse_test @{context} "2 * x is_num";
+val t = ParseC.parse_test @{context} "2 * x is_num";
 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
 if UnparseC.term t' = "(2 * x is_num) = False" then ()
 else error "(2 * x is_num) = False CHANGED";
-val t = TermC.parse_test @{context} "- 2 is_num";
+val t = ParseC.parse_test @{context} "- 2 is_num";
 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
 if UnparseC.term t' = "(- 2 is_num) = True" then ()
 else error "(- 2 is_num) = False CHANGED";
-val t = TermC.parse_test @{context} "- 1 is_num";
+val t = ParseC.parse_test @{context} "- 1 is_num";
 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
 if UnparseC.term t' = "(- 1 is_num) = True" then ()
 else error "(- 1 is_num) = False CHANGED";
-val t = TermC.parse_test @{context} "0 is_num";
+val t = ParseC.parse_test @{context} "0 is_num";
 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
 if UnparseC.term t' = "(0 is_num) = True" then ()
 else error "(0 is_num) = False CHANGED";
-val t = TermC.parse_test @{context} "AA is_num";
+val t = ParseC.parse_test @{context} "AA is_num";
 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
 if UnparseC.term t' = "(AA is_num) = False" then ()
 else error "(0 is_num) = False CHANGED";
 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
 val thy = @{theory}
 val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge")
-val t = TermC.parse_test @{context} "x = 0";
+val t = ParseC.parse_test @{context} "x = 0";
 val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
-val t = TermC.parse_test @{context} "(x + 1) = (x + 1)";
+val t = ParseC.parse_test @{context} "(x + 1) = (x + 1)";
 val (Const _(*op0,t0*) $ t1 $ t2 ) = t
 val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
 if UnparseC.term t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED";
-val t as Const _ $ v $ c = TermC.parse_test @{context} "1 = 0";
+val t as Const _ $ v $ c = ParseC.parse_test @{context} "1 = 0";
 val false = variable_constant_pair (v, c);
 val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
 if UnparseC.term t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED";
-val t = TermC.parse_test @{context} "0 = 0";
+val t = ParseC.parse_test @{context} "0 = 0";
 val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
 if UnparseC.term t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";
 "-------- occurs_in ----------------------------------------------------------------------------";
 "-------- occurs_in ----------------------------------------------------------------------------";
 "-------- occurs_in ----------------------------------------------------------------------------";
 val t = @{term "x::real"};
 if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";
-val t = TermC.parse_test @{context} "x occurs_in x";
+val t = ParseC.parse_test @{context} "x occurs_in x";
 val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs_in" t 0;
 if UnparseC.term t' = "x occurs_in x = True" then ()
 else error "x occurs_in x = True ..changed";
 "------- some_occur_in";
 "---------fun eval_argument_of -----------------------------------------------------------------";
 "---------fun eval_argument_of -----------------------------------------------------------------";
 "---------fun eval_argument_of -----------------------------------------------------------------";
-val t = TermC.parse_test @{context} "argument_in (M_b x)";
+val t = ParseC.parse_test @{context} "argument_in (M_b x)";
 val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument_in" t 0;
 if UnparseC.term t' = "(argument_in M_b x) = x" then ()
 else error "atools.sml:(argument_in M_b x) = x  ???";
 "-------- fun matchsub -------------------------------------------------------------------------";
 "-------- fun matchsub -------------------------------------------------------------------------";
 "-------- fun matchsub -------------------------------------------------------------------------";
-if matchsub thy (TermC.parse_test @{context} "(a + (b + c))") (TermC.parse_patt_test @{theory} "?x + (?y + ?z)")
+if matchsub thy (ParseC.parse_test @{context} "(a + (b + c))") (ParseC.parse_patt_test @{theory} "?x + (?y + ?z)")
 then () else error "tools.sml matchsub a + (b + c)";
-if matchsub thy (TermC.parse_test @{context} "(a + (b + c)) + d") (TermC.parse_patt_test @{theory} "?x + (?y + ?z)")
+if matchsub thy (ParseC.parse_test @{context} "(a + (b + c)) + d") (ParseC.parse_patt_test @{theory} "?x + (?y + ?z)")
 then () else error "tools.sml matchsub (a + (b + c)) + d";
 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
 "see: --------- search for Or_to_List ---";
 case or2list @{term True} of Const (\<^const_name>\<open>UniversalList\<close>, _) => ()
 | _ => error "TermC.UniversalList changed 1";
 case or2list @{term False} of Const (\<^const_name>\<open>Nil\<close>, _) => ()
 | _ => error "TermC.UniversalList changed 2";
-val t =  (TermC.parse_test @{context} "x=3");
+val t =  (ParseC.parse_test @{context} "x=3");
 if UnparseC.term (or2list t) = "[x = 3]" then ()
 else error "or2list changed";
-val t =  (TermC.parse_test @{context} "x=3 | x=-3 | x=0");
+val t =  (ParseC.parse_test @{context} "x=3 | x=-3 | x=0");
 if UnparseC.term (or2list t) = "[x = 3, x = - 3, x = 0]" then ()
 else error "HOL.eq ? HOL.disj ? changed";

changeset 60660	c4b24621077e
parent 60650	06ec8abfd3bc
child 60663	2197e3597cba