1.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Fri Apr 10 16:16:09 2020 +0200
1.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Fri Apr 10 18:32:36 2020 +0200
1.3 @@ -66,7 +66,7 @@
1.4 val to_ctxt = ContextC.insert_assumptions
1.5 [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt
1.6 val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt;
1.7 -if UnparseC.terms2strs (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
1.8 +if UnparseC.terms_to_strings (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
1.9 then () else error "fun transfer_asms_from_to changed"
1.10
1.11
1.12 @@ -83,27 +83,27 @@
1.13
1.14 val t = str2term "[x = 0, x = 6 / 5]";
1.15 val (t', for_asm) = avoid_contradict t preds;
1.16 -if UnparseC.term2str t' = "[x = 6 / 5]" andalso map UnparseC.term2str for_asm = ["x = 6 / 5"]
1.17 +if UnparseC.term t' = "[x = 6 / 5]" andalso map UnparseC.term for_asm = ["x = 6 / 5"]
1.18 then () else error "avoid_contradict [x = 0, x = 6 / 5] CHANGED";
1.19
1.20 val t = str2term "x = 0";
1.21 val (t', for_asm) = avoid_contradict t preds;
1.22 -if UnparseC.term2str t' = "bool_undef" andalso map UnparseC.term2str for_asm = []
1.23 +if UnparseC.term t' = "bool_undef" andalso map UnparseC.term for_asm = []
1.24 then () else error "avoid_contradict x = 0 CHANGED"; (* "x \<noteq> 0" in preds *)
1.25
1.26 val t = str2term "x = 1";
1.27 val (t', for_asm) = avoid_contradict t preds;
1.28 -if UnparseC.term2str t' = "x = 1" andalso map UnparseC.term2str for_asm = ["x = 1"]
1.29 +if UnparseC.term t' = "x = 1" andalso map UnparseC.term for_asm = ["x = 1"]
1.30 then () else error "avoid_contradict x = 1 CHANGED"; (* "x \<noteq> 1" NOT in preds *)
1.31
1.32 val t = str2term "a + b";
1.33 val (t', for_asm) = avoid_contradict t preds;
1.34 -if UnparseC.term2str t' = "a + b" andalso map UnparseC.term2str for_asm = []
1.35 +if UnparseC.term t' = "a + b" andalso map UnparseC.term for_asm = []
1.36 then () else error "avoid_contradict a + b CHANGED"; (* NOT a predicate *)
1.37
1.38 val t = str2term "[a + b]";
1.39 val (t', for_asm) = avoid_contradict t preds;
1.40 -if UnparseC.term2str t' = "[a + b]" andalso map UnparseC.term2str for_asm = []
1.41 +if UnparseC.term t' = "[a + b]" andalso map UnparseC.term for_asm = []
1.42 then () else error "avoid_contradict [a + b] CHANGED"; (* NOT a predicate *)
1.43
1.44
1.45 @@ -121,7 +121,7 @@
1.46 [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt
1.47 val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
1.48
1.49 -if UnparseC.term2str t = "[x_1 = 1, x_2 = 2, x_3 = 3]" andalso map UnparseC.term2str (get_assumptions new_ctxt) =
1.50 +if UnparseC.term t = "[x_1 = 1, x_2 = 2, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) =
1.51 ["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"]
1.52 then () else error "fun subpbl_to_caller changed 1";
1.53
1.54 @@ -130,7 +130,7 @@
1.55 [str2term "b < (to::int)", str2term "x_2 \<noteq> (2::int)"] ctxt
1.56 val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
1.57
1.58 -if UnparseC.term2str t = "[x_1 = 1, x_3 = 3]" andalso map UnparseC.term2str (get_assumptions new_ctxt) =
1.59 +if UnparseC.term t = "[x_1 = 1, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) =
1.60 ["b < fro", "x_1 = 1", "x_3 = 3", "b < to", "x_2 \<noteq> 2"]
1.61 then () else error "fun subpbl_to_caller changed 2";
1.62
1.63 @@ -155,7 +155,7 @@
1.64 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.65 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)";
1.66
1.67 -(*+*)if (Ctree.get_assumptions pt p |> map UnparseC.term2str) =
1.68 +(*+*)if (Ctree.get_assumptions pt p |> map UnparseC.term) =
1.69 (*+*) ["x \<noteq> 0",
1.70 (*+*) "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",
1.71 (*+*) "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"]
1.72 @@ -201,7 +201,7 @@
1.73 (*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "[x = 0, x = 6 / 5]";
1.74 (*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>2. Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)
1.75
1.76 -(* *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term2str), [
1.77 +(* *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [
1.78 (*0.pre*) "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
1.79 (*1.pre*) "\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
1.80 (*1.pre*) ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
1.81 @@ -247,7 +247,7 @@
1.82 (*NEW*) (Pstate i, c) => (i, c)
1.83 (*NEW*) | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc";
1.84
1.85 -(* *)if eq_set op = (map UnparseC.term2str (get_assumptions ctxt_parent), [
1.86 +(* *)if eq_set op = (map UnparseC.term (get_assumptions ctxt_parent), [
1.87 (*0.pre*) "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
1.88 (*1.pre*) "\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
1.89 (*1.pre*) ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
1.90 @@ -258,7 +258,7 @@
1.91
1.92 val (prog_res', ctxt') =
1.93 ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent;
1.94 -(* *)if eq_set op = (map UnparseC.term2str (get_assumptions ctxt'), [
1.95 +(* *)if eq_set op = (map UnparseC.term (get_assumptions ctxt'), [
1.96 (*0.pre*) "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
1.97 (*1.pre*) "\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
1.98 (*1.pre*) ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
1.99 @@ -305,7 +305,7 @@
1.100 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)
1.101
1.102 (*/-------- final test -----------------------------------------------------------------------\*)
1.103 -if f2str f = "[x = 6 / 5]" andalso map UnparseC.term2str (Ctree.get_assumptions pt p) =
1.104 +if f2str f = "[x = 6 / 5]" andalso map UnparseC.term (Ctree.get_assumptions pt p) =
1.105 ["x = 6 / 5", "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
1.106 "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
1.107 "\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",