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