1open HolKernel Parse boolLib
2open ListConv1
3
4open testutils
5
6fun parsetest(s, l) =
7  let
8    fun toN i = numSyntax.mk_numeral (Arbnum.fromInt i)
9    val _ = tprint ("Parsing "^s)
10    val res = Parse.Term [QUOTE s]
11    val l_t = listSyntax.mk_list(map toN l, numSyntax.num)
12  in
13    if aconv res l_t then OK() else die "FAILED!"
14  end
15
16val _ = List.app parsetest [
17      ("[]:num list", []),
18      ("[1]", [1]), ("[1;]", [1]),
19      ("[1;2]", [1,2]), ("[1;2;]", [1,2]),
20      ("[1;2;3]", [1,2,3]), ("[1; 2; 3;]", [1,2,3]), ("[1; 2 ; 3 ; ]", [1,2,3]),
21      ("[ 1 ;   2 ; 3 ; 4 ; ]", [1,2,3,4])
22    ]
23
24datatype 'a exnsum = Some of 'a | Exn of exn
25fun total f x = Some (f x) handle Interrupt => raise Interrupt | e => Exn e
26
27fun test0 nm cmp pr f (x, expected_opt) = let
28  val _ = tprint (StringCvt.padRight #" " 20 nm ^ pr x)
29in
30  case (total f x, expected_opt) of
31      (Some result, SOME expected) =>
32        if cmp(rhs (concl result),expected) <> EQUAL then die "FAILED - BAD RHS"
33        else if not (null (hyp result)) then die "FAILED - HYPS"
34        else if cmp(lhs (concl result),x) <> EQUAL then die "FAILED - BAD LHS"
35        else OK()
36    | (Some _, NONE) => die "FAILED - didn't raise EXN"
37    | (Exn e, SOME _) => die ("FAILED\n  EXN: "^General.exnMessage e)
38    | (Exn _, NONE) => OK()
39end
40
41fun test nm cmp pr f (x, e) = test0 nm cmp pr f (x, SOME e)
42
43val _ = set_trace "Unicode" 0
44
45val _ = app tpp [
46  "MEM a l", "~MEM a l", "x NOTIN {1; 2; 3}",
47  "case l of [] => 0 | h::t => h + LENGTH t",
48  "[1; 2]",
49  "[aaaa; bbbbb; cccc; dddd; eeee; ffff; gggg; hhhh; iiii; \
50  \jjjj; kkkk; llll; mmmm;\n nnnn; oooo]",
51  "f\n\
52  \  [aaaa; bbbb; cccc; dddd; eeee; ffff; gggg; hhhh; iiii; jjjj; kkkk; llll; \
53     \mmmm;\n\
54  \   nnnn; oooo; pppp]"
55]
56
57val _ = tpp_expected {input = "SINGL 3", output = "[3]",
58                      testf = standard_tpp_message}
59
60val _ = app(test "FIRSTN_CONV" Term.compare term_to_string FIRSTN_CONV)
61           [(``FIRSTN 3 [1;2;3;4;5]``, ``[1;2;3]``),
62            (``FIRSTN 4 [1;2;3;4]``, ``[1;2;3;4]``),
63            (``FIRSTN 0 [1;2]``, ``[] : num list``),
64            (``FIRSTN 0 [] : num list``, ``[] : num list``)]
65val _ = app(test "BUTFIRSTN_CONV" Term.compare term_to_string BUTFIRSTN_CONV)
66           [(``BUTFIRSTN 3 [1;2;3;4]``, ``[4]``),
67            (``BUTFIRSTN 0 [1;2]``, ``[1;2]``),
68            (``BUTFIRSTN 3 [1;2;3]``, ``[] : num list``),
69            (``BUTFIRSTN 0 [] : num list``, ``[] : num list``)]
70val _ = app(test "LIST_EQ_SIMP_CONV" Term.compare term_to_string
71                 listSimps.LIST_EQ_SIMP_CONV)
72           [(``(l1:'a list ++ [])::t = p ++ q``, ``(l1:'a list)::t = p ++ q``)]
73
74val _ = Lib.appi (fn i => fn t =>
75                     test0 ("EL_CONV "^Int.toString (i+1))
76                          Term.compare term_to_string EL_CONV t)
77                 [(``EL 1 [3;4;5]``, SOME ``4``),
78                  (``EL 0 [3+1;4;4*2]``, SOME ``3 + 1``),
79                  (``EL 3 [1;2;3]``, NONE),
80                  (``EL 1 (3::x::t)``, NONE),
81                  (``EL 1 [a;b;c:num]``, SOME ``b:num``),
82                  (``EL 3 [a;b;c:num;d]``, SOME ``d:num``)
83                 ]
84
85val _ = Lib.appi (fn i => fn t =>
86                     test0 ("FLAT_CONV "^Int.toString (i + 1))
87                           Term.compare term_to_string FLAT_CONV t)
88                 [(``FLAT ([]:'a list list)``, SOME ``[] : 'a list``),
89                  (``FLAT [[1];[2];[3];[1]]``, SOME ``[1;2;3;1]``),
90                  (``FLAT [[];[];[]:'a list]``, SOME ``[]:'a list``),
91                  (``FLAT [[1+2];[];[2*4]]``, SOME ``[1+2;2*4]``),
92                  (``FLAT [[1+2;3;3*8];[];[];[1+21];[3;4]]``,
93                     SOME ``[1+2;3;3*8;1+21;3;4]``),
94                  (``FLAT ([]::(t:'a list list))``, NONE)
95                 ]
96
97val _ = test0 "FOLDR_CONV 1" Term.compare term_to_string
98              (FOLDR_CONV ALL_CONV)
99              (``FOLDR f 0 [1;2;3;x]``, SOME ``f 1 (f 2 (f 3 (f x 0)))``)
100val _ = test0 "FOLDR_CONV 2" Term.compare term_to_string
101              (FOLDR_CONV (TRY_CONV reduceLib.ADD_CONV))
102              (``FOLDR f (3 + 2) [1 * 4; 3 - 1]``,
103                   SOME ``f (1 * 4) (f (3 - 1) (3 + 2))``)
104val _ = Lib.appi (fn i => fn t =>
105                     test0 ("FOLDR_CONV "^Int.toString (i + 3))
106                           Term.compare term_to_string
107                           (FOLDR_CONV numLib.REDUCE_CONV) t)
108                 [(``FOLDR (+) 0 [0;1;2;3]``, SOME ``6``),
109                  (``FOLDR (-) 0 [3;2;1]``, SOME ``2``),
110                  (``FOLDR $* 1 []``, SOME ``1``)]
111
112val cs = listSimps.list_compset()
113val _ = indexedListsSimps.add_indexedLists_compset cs
114fun ct(s,inp,out) =
115  testutils.convtest ("list_compset - " ^ s, computeLib.CBV_CONV cs, inp, out)
116val _ = List.app ct [
117  ("oHD-NONE", ���oHD ([]:'a list)���, ���NONE : 'a option���),
118  ("oHD-SOME", ���oHD ([3;4]:num list)���, ���SOME 3n���),
119  ("oEL-NONE1", ���oEL 1 ([]:'a list)���, ���NONE : 'a option���),
120  ("oEL-NONE2", ���oEL 2 [3;4]���, ���NONE : num option���),
121  ("oEL-SOME1", ���oEL 0 [3;4]���, ���SOME 3n���),
122  ("oEL-SOME2", ���oEL 4 [3;4;5;6;7;10]���, ���SOME 7n���),
123  ("MAP-NIL", ���MAP SUC []���, ���[] : num list���),
124  ("MAP-CONS", ���MAP SUC [1;2;3]���, ���[2;3;4] : num list���),
125  ("MAP2i-NIL1", ���MAP2i (\i x y. x + i * y) [] []���, ���[] : num list���),
126  ("MAP2i-CONS", ���MAP2i (\i x y. x + i * y) [1;2;3] [4;5;6]���,
127                 ���[1;7;15] : num list���),
128  ("FOLDL1", ���FOLDL $+ 0 [1;2;3;4]���, ���10n���),
129  ("FOLDR1", ���FOLDR (\n a. (n * 2) :: a) [] [1;2;3;4]���, ���[2;4;6;8]���),
130  ("GENLIST", ���GENLIST (\n. 2 * n + 4) 6���, ���[4; 6; 8; 10; 12; 14]���),
131  ("CONS-eq-NIL", ���h::t = []���, ���F���),
132  ("LUPDATE(1)", ���LUPDATE 9 2 [1;2;3;4]���, ���[1;2;9;4]���),
133  ("LUPDATE(2)", ���LUPDATE 9 4 [1;2;3;4]���, ���[1;2;3;4]���),
134  ("SHORTLEX(1)", ���SHORTLEX (<) [1;1] [1;2;3]���, ���T���),
135  ("SHORTLEX(2)", ���SHORTLEX (<) [1;1;4] [1;1;3]���, ���F���),
136  ("SHORTLEX(3)", ���SHORTLEX (<) [1;1;4] [1;1]���, ���F���),
137  ("LLEX(1)", ���LLEX (<) [1;1;1] [1;2]���, ���T���)
138]
139
140val _ = let
141  open BasicProvers listTheory
142  val op using = markerLib.using
143  val usingA = markerLib.usingA
144  val g = ���0 < LENGTH (l:num list)���
145  val expected = [���0 < LENGTH ([]:num list)���, ���0 < LENGTH (SNOC (x:num) l')���]
146  val expected2 =
147      [���0 < LENGTH ([]:num list)���, ������x. 0 < LENGTH (SNOC (x:num) l)���]
148  val expected2a = [[], [���0 < LENGTH (l:num list)���]]
149  infix AND
150  fun (f AND g) x = f x andalso g x
151  fun check1 sgs = list_eq aconv expected (map snd sgs)
152  fun check1a sgs = List.all null (map fst sgs : term list list)
153  fun check2 sgs = list_eq (list_eq aconv) expected2a (map fst sgs)
154  val ppgs = trace ("types", 1) (
155        HOLPP.block HOLPP.CONSISTENT 4 o
156        HOLPP.pr_list goalStack.pp_goal [HOLPP.NL, HOLPP.NL]
157      )
158  val rtcg = ���!y:num x:num. RTC R x (f y) ==> Q x y���
159  val rtc_expected = [���(!m:num n:num. f n = m ==> Q m n) /\
160                       !a b c. (!d. f d = b ==> Q a d) /\ R b c ==>
161                               !d. f d = c ==> Q a d���]
162  val bit_cases = hd (Prim_rec.prove_cases_thm numeralTheory.bit_induction)
163  fun TAC t g = fst (VALID t g)
164in
165  tprint "Cases_on ���m��� using bit_cases";
166  require_msg (check_result (
167                  (list_eq aconv [���0 < ZERO���, ���0 < BIT1 n���, ���0 < BIT2 n���] o
168                   map snd) AND
169                  (List.all null o map fst)
170              ))
171              (HOLPP.pp_to_string 65 ppgs)
172              (TAC $ Cases_on ���m��� using bit_cases) ([], ���0 < m���);
173  tprint "Cases_on ���m��� using EVEN_OR_ODD";
174  require_msg (check_result ((list_eq aconv [���0 < m���, ���0 < m���] o map snd) AND
175                             (list_eq (list_eq aconv) [[���EVEN m���], [���ODD m���]] o
176                              map fst)))
177              (HOLPP.pp_to_string 65 ppgs)
178              (TAC $ Cases_on ���m��� using arithmeticTheory.EVEN_OR_ODD)
179              ([], ���0 < m���);
180  tprint "Cases_on ���m��� using assumption";
181  require_msg (check_result ((list_eq aconv [���0 < 2���, ���0 < 4���] o map snd) AND
182                             (List.all null o map fst)))
183              (HOLPP.pp_to_string 65 ppgs)
184              (TAC $ pop_assum $ usingA $ Cases_on ���m���)
185              ([���!a. a = 2 \/ a = 4���], ���0 < m���);
186  tprint "Cases_on ���l��� using SNOC_CASES";
187  require_msg (check_result (check1 AND check1a))
188              (HOLPP.pp_to_string 65 ppgs)
189              (TAC $ Cases_on ���l��� using SNOC_CASES) ([], g);
190  tprint "Induct_on ���l��� using SNOC_INDUCT";
191  require_msg (check_result ((list_eq aconv expected2 o map snd) AND check2))
192              (HOLPP.pp_to_string 65 ppgs)
193              (TAC (Induct_on ���l��� using SNOC_INDUCT)) ([], g);
194  tprint "Induct_on ���RTC��� using RTC_INDUCT_RIGHT1";
195  require_msg (check_result ((list_eq aconv rtc_expected o map snd)))
196              (HOLPP.pp_to_string 65 ppgs)
197              (TAC $ Induct_on ���RTC��� using relationTheory.RTC_INDUCT_RIGHT1)
198              ([], rtcg)
199end
200