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 ctxt = Proof_Context.init_global @{theory}
48 val prog_expr = get_rls @{context} "prog_expr"
50 val t = TermC.parse_test @{context} "NTH 1 [a,b,c,d,e]";
51 TermC.atom_trace_detail @{context} t;
52 val thm = Thm.prop_of @{thm NTH_NIL};
53 TermC.atom_trace_detail @{context} thm;
54 val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t;
55 if UnparseC.term t' = "a" then ()
56 else error "NTH 1 [a,b,c,d,e] = a ..changed";
58 val t = TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]";
59 case TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]" of
60 Const (\<^const_name>\<open>NTH\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
61 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $
62 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $
63 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("c", _) $
64 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $
65 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => ()
66 | _ => error "ListC.NTH changed";
67 val thm = Thm.prop_of @{thm NTH_CONS};
68 TermC.atom_trace_detail @{context} thm;
69 val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_CONS} t;
70 if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then ()
71 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
73 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
74 val t = TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]";
75 TermC.atom_trace_detail @{context} t;
77 val SOME (t', _) = rewrite_set_ ctxt false prog_expr t;
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 = get_rls @{context} "prog_expr"
86 val thy = @{theory ListC};
87 val t = TermC.parse_test @{context} "Length [1, 1, 1]";
88 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
89 UnparseC.term t = "1 + Length [1, 1]";
90 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
91 UnparseC.term t = "1 + (1 + Length [1])";
92 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
93 UnparseC.term t = "1 + (1 + (1 + Length []))";
94 val NONE = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
95 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t;
96 val NONE = rewrite_ ctxt 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.parse_test @{context} "Length [1, 1, 1]";
101 val SOME (t, asm) = rewrite_set_ ctxt 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.parse_test @{context} "Length [1, 1, 1]";
106 val t = eval_prog_expr ctxt prog_expr t;
108 Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => ()
109 | _ => error "Length [1, 1, 1] = 3 ..eval_prog_expr changed";