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 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
11 "--------------------- NTH ---------------------------------------------------";
12 "--------------------- Length ------------------------------------------------";
13 "--------------------- tl ----------------------------------------------------";
14 "-----------------------------------------------------------------------------";
15 "-----------------------------------------------------------------------------";
17 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
18 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
19 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
20 (* ML representation *)
21 val t1 = @{term "{|| ||}"};
22 val t2 = @{term "{||1,2,3||}"};
25 if Print_Mode.setmp []
26 (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t1
28 then () else error "CHANGED pretty printing of '{|| ||}'";
30 if Print_Mode.setmp []
31 (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t2
32 = "{|| 1::'a, 2::'a, 3::'a ||}"
33 then () else error "CHANGED pretty printing of '{||1,2,3||}'"
36 Syntax.read_term_global @{theory} "{|| ||}";
37 Syntax.read_term_global @{theory} "{||1,2,3||}";
39 "--------------------- NTH ---------------------------------------------------";
40 "--------------------- NTH ---------------------------------------------------";
41 "--------------------- NTH ---------------------------------------------------";
42 val prog_expr = assoc_rls "prog_expr"
44 val t = str2term "NTH 1 [a,b,c,d,e]";
46 val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_NIL};
48 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_NIL}) t;
49 if UnparseC.term t' = "a" then ()
50 else error "NTH 1 [a,b,c,d,e] = a ..changed";
52 val t = str2term "NTH 3 [a,b,c,d,e]";
53 val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const ("List.list.Cons", _) $ Free ("a", _) $
54 (Const ("List.list.Cons", _) $ Free ("b", _) $
55 (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
57 val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
59 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
60 if UnparseC.term t' = "NTH (3 + -1) [b, c, d, e]" then ()
61 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
63 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
64 val t = str2term "NTH 3 [a,b,c,d,e]";
66 Rewrite.trace_on := false;
67 val SOME (t', _) = rewrite_set_ thy false prog_expr t;
68 Rewrite.trace_on := false;
69 if UnparseC.term t' = "c" then ()
70 else error "NTH 3 [a,b,c,d,e] = c ..changed";
72 "--------------------- Length ------------------------------------------------";
73 "--------------------- Length ------------------------------------------------";
74 "--------------------- Length ------------------------------------------------";
75 val prog_expr = assoc_rls "prog_expr"
77 val thy = @{theory ListC};
78 val t = str2term "Length [1, 1, 1]";
79 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
80 UnparseC.term t = "1 + Length [1, 1]";
81 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
82 UnparseC.term t = "1 + (1 + Length [1])";
83 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
84 UnparseC.term t = "1 + (1 + (1 + Length []))";
85 val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
86 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
87 val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
88 if UnparseC.term t = "1 + (1 + (1 + 0))" then ()
89 else error "Length [1, 1, 1] = 1 + (1 + (1 + 0)) ..changed";
91 val t = str2term "Length [1, 1, 1]";
92 val SOME (t, asm) = rewrite_set_ thy false prog_expr t;
93 if UnparseC.term t = "3" then ()
94 else error "Length [1, 1, 1] = 3 ..prog_expr changed";
96 val t = str2term "Length [1, 1, 1]";
97 val t = eval_prog_expr thy prog_expr t;
98 case t of Free ("3", _) => ()
99 | _ => error "Length [1, 1, 1] = 3 ..eval_prog_expr changed";