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