1.1 --- a/test/Tools/isac/ProgLang/listC.sml Thu Apr 09 12:03:14 2020 +0200
1.2 +++ b/test/Tools/isac/ProgLang/listC.sml Thu Apr 09 17:13:17 2020 +0200
1.3 @@ -46,7 +46,7 @@
1.4 val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_NIL};
1.5 atomty thm;
1.6 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (num_str @{thm NTH_NIL}) t;
1.7 -if term2str t' = "a" then ()
1.8 +if UnparseC.term2str t' = "a" then ()
1.9 else error "NTH 1 [a,b,c,d,e] = a ..changed";
1.10
1.11 val t = str2term "NTH 3 [a,b,c,d,e]";
1.12 @@ -57,7 +57,7 @@
1.13 val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_CONS};
1.14 atomty thm;
1.15 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (num_str @{thm NTH_CONS}) t;
1.16 -if term2str t' = "NTH (3 + -1) [b, c, d, e]" then ()
1.17 +if UnparseC.term2str t' = "NTH (3 + -1) [b, c, d, e]" then ()
1.18 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
1.19
1.20 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
1.21 @@ -66,7 +66,7 @@
1.22 trace_rewrite := false;
1.23 val SOME (t', _) = rewrite_set_ thy false prog_expr t;
1.24 trace_rewrite := false;
1.25 -if term2str t' = "c" then ()
1.26 +if UnparseC.term2str t' = "c" then ()
1.27 else error "NTH 3 [a,b,c,d,e] = c ..changed";
1.28
1.29 "--------------------- LENGTH ------------------------------------------------";
1.30 @@ -77,20 +77,20 @@
1.31 val thy = @{theory ListC};
1.32 val t = str2term "LENGTH [1, 1, 1]";
1.33 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
1.34 -term2str t = "1 + LENGTH [1, 1]";
1.35 +UnparseC.term2str t = "1 + LENGTH [1, 1]";
1.36 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
1.37 -term2str t = "1 + (1 + LENGTH [1])";
1.38 +UnparseC.term2str t = "1 + (1 + LENGTH [1])";
1.39 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
1.40 -term2str t = "1 + (1 + (1 + LENGTH []))";
1.41 +UnparseC.term2str t = "1 + (1 + (1 + LENGTH []))";
1.42 val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
1.43 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
1.44 val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
1.45 -if term2str t = "1 + (1 + (1 + 0))" then ()
1.46 +if UnparseC.term2str t = "1 + (1 + (1 + 0))" then ()
1.47 else error "LENGTH [1, 1, 1] = 1 + (1 + (1 + 0)) ..changed";
1.48
1.49 val t = str2term "LENGTH [1, 1, 1]";
1.50 val SOME (t, asm) = rewrite_set_ thy false prog_expr t;
1.51 -if term2str t = "3" then ()
1.52 +if UnparseC.term2str t = "3" then ()
1.53 else error "LENGTH [1, 1, 1] = 3 ..prog_expr changed";
1.54
1.55 val t = str2term "LENGTH [1, 1, 1]";