1.1 --- a/test/Tools/isac/ProgLang/listC.sml Mon Jun 21 22:08:01 2021 +0200
1.2 +++ b/test/Tools/isac/ProgLang/listC.sml Sun Jul 18 18:15:27 2021 +0200
1.3 @@ -7,6 +7,7 @@
1.4 "-----------------------------------------------------------------------------";
1.5 "table of contents -----------------------------------------------------------";
1.6 "-----------------------------------------------------------------------------";
1.7 +"----------- correct list_erls -----------------------------------------------------------------";
1.8 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
1.9 "--------------------- NTH ---------------------------------------------------";
1.10 "--------------------- Length ------------------------------------------------";
1.11 @@ -14,6 +15,10 @@
1.12 "-----------------------------------------------------------------------------";
1.13 "-----------------------------------------------------------------------------";
1.14
1.15 +"----------- correct list_erls -----------------------------------------------------------------";
1.16 +"----------- correct list_erls -----------------------------------------------------------------";
1.17 +"----------- correct list_erls -----------------------------------------------------------------";
1.18 +
1.19 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
1.20 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
1.21 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
1.22 @@ -50,22 +55,26 @@
1.23 else error "NTH 1 [a,b,c,d,e] = a ..changed";
1.24
1.25 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
1.26 -val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $
1.27 - (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $
1.28 - (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
1.29 -TermC.atomty t;
1.30 +case TermC.str2term "NTH 3 [a,b,c,d,e]" of
1.31 + Const ("ListC.NTH", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
1.32 + (Const ("List.list.Cons", _) $ Free ("a", _) $
1.33 + (Const ("List.list.Cons", _) $ Free ("b", _) $
1.34 + (Const ("List.list.Cons", _) $ Free ("c", _) $
1.35 + (Const ("List.list.Cons", _) $ Free ("d", _) $
1.36 + (Const ("List.list.Cons", _) $ Free ("e", _) $ Const ("List.list.Nil", _)))))) => ()
1.37 +| _ => error "ListC.NTH changed";
1.38 val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
1.39 TermC.atomty thm;
1.40 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
1.41 -if UnparseC.term t' = "NTH (3 + -1) [b, c, d, e]" then ()
1.42 +if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then ()
1.43 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
1.44
1.45 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
1.46 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
1.47 TermC.atomty t;
1.48 -Rewrite.trace_on := false;
1.49 +Rewrite.trace_on := false; (*true false*)
1.50 val SOME (t', _) = rewrite_set_ thy false prog_expr t;
1.51 -Rewrite.trace_on := false;
1.52 +Rewrite.trace_on := false; (*true false*)
1.53 if UnparseC.term t' = "c" then ()
1.54 else error "NTH 3 [a,b,c,d,e] = c ..changed";
1.55
1.56 @@ -95,6 +104,7 @@
1.57
1.58 val t = TermC.str2term "Length [1, 1, 1]";
1.59 val t = eval_prog_expr thy prog_expr t;
1.60 -case t of Free ("3", _) => ()
1.61 +case t of
1.62 + Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)) => ()
1.63 | _ => error "Length [1, 1, 1] = 3 ..eval_prog_expr changed";
1.64