1 (* Title: tests for ListC
2 Author: Walther Neuper 030501
3 (c) copyright due to lincense terms.
6 "-----------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------";
8 "table of contents -----------------------------------------------------------";
9 "-----------------------------------------------------------------------------";
10 "----------- correct list_erls -----------------------------------------------------------------";
11 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
12 "--------------------- NTH ---------------------------------------------------";
13 "--------------------- Length ------------------------------------------------";
14 "--------------------- tl ----------------------------------------------------";
15 "-----------------------------------------------------------------------------";
16 "-----------------------------------------------------------------------------";
18 "----------- correct list_erls -----------------------------------------------------------------";
19 "----------- correct list_erls -----------------------------------------------------------------";
20 "----------- correct list_erls -----------------------------------------------------------------";
22 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
23 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
24 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
25 (* ML representation *)
26 val t1 = @{term "{|| ||}"};
27 val t2 = @{term "{||1,2,3||}"};
30 if Print_Mode.setmp []
31 (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t1
33 then () else error "CHANGED pretty printing of '{|| ||}'";
35 if Print_Mode.setmp []
36 (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t2
37 = "{|| 1::'a, 2::'a, 3::'a ||}"
38 then () else error "CHANGED pretty printing of '{||1,2,3||}'"
41 Syntax.read_term_global @{theory} "{|| ||}";
42 Syntax.read_term_global @{theory} "{||1,2,3||}";
44 "--------------------- NTH ---------------------------------------------------";
45 "--------------------- NTH ---------------------------------------------------";
46 "--------------------- NTH ---------------------------------------------------";
47 val prog_expr = assoc_rls "prog_expr"
49 val t = TermC.str2term "NTH 1 [a,b,c,d,e]";
51 val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_NIL};
53 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_NIL}) t;
54 if UnparseC.term t' = "a" then ()
55 else error "NTH 1 [a,b,c,d,e] = a ..changed";
57 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
58 case TermC.str2term "NTH 3 [a,b,c,d,e]" of
59 Const ("ListC.NTH", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
60 (Const ("List.list.Cons", _) $ Free ("a", _) $
61 (Const ("List.list.Cons", _) $ Free ("b", _) $
62 (Const ("List.list.Cons", _) $ Free ("c", _) $
63 (Const ("List.list.Cons", _) $ Free ("d", _) $
64 (Const ("List.list.Cons", _) $ Free ("e", _) $ Const ("List.list.Nil", _)))))) => ()
65 | _ => error "ListC.NTH changed";
66 val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
68 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
69 if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then ()
70 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
72 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
73 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
75 Rewrite.trace_on := false;
76 val SOME (t', _) = rewrite_set_ thy false prog_expr t;
77 Rewrite.trace_on := false;
78 if UnparseC.term t' = "c" then ()
79 else error "NTH 3 [a,b,c,d,e] = c ..changed";
81 "--------------------- Length ------------------------------------------------";
82 "--------------------- Length ------------------------------------------------";
83 "--------------------- Length ------------------------------------------------";
84 val prog_expr = assoc_rls "prog_expr"
86 val thy = @{theory ListC};
87 val t = TermC.str2term "Length [1, 1, 1]";
88 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
89 UnparseC.term t = "1 + Length [1, 1]";
90 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
91 UnparseC.term t = "1 + (1 + Length [1])";
92 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
93 UnparseC.term t = "1 + (1 + (1 + Length []))";
94 val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
95 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
96 val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
97 if UnparseC.term t = "1 + (1 + (1 + 0))" then ()
98 else error "Length [1, 1, 1] = 1 + (1 + (1 + 0)) ..changed";
100 val t = TermC.str2term "Length [1, 1, 1]";
101 val SOME (t, asm) = rewrite_set_ thy false prog_expr t;
102 if UnparseC.term t = "3" then ()
103 else error "Length [1, 1, 1] = 3 ..prog_expr changed";
105 val t = TermC.str2term "Length [1, 1, 1]";
106 val t = eval_prog_expr thy prog_expr t;
108 Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)) => ()
109 | _ => error "Length [1, 1, 1] = 3 ..eval_prog_expr changed";