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