1
2val _ =print "\n";
3
4fun die s = (print (s^"\n"); OS.Process.exit OS.Process.failure)
5
6fun tprint s = print (UTF8.padRight #" " 65 s)
7
8fun assert (s, b) =
9    (tprint s; if b() then print "OK\n" else die "FAILED!")
10
11
12open Redblackset
13val es = empty Int.compare
14
15fun m10cmp (i1,i2) = Int.compare(i1 mod 10, i2 mod 10)
16val em10 = empty m10cmp
17val em3 = add(em10, 3)
18val em13 = add(em3, 13)
19
20fun gcSucceeds s res () = UTF8.getChar s = res
21fun gcFails s () = (UTF8.getChar s ; false) handle UTF8.BadUTF8 _ => true
22
23val _ = List.app assert [
24    ("Redblackset.isSubset({},{})", fn () => isSubset(es,es)),
25    ("Redblackset.isSubset({}, {1})",
26     (fn () => isSubset(es,addList(es,[1])))),
27    ("Redblackset.add replaces EQUAL elements",
28     (fn () => listItems em13 = [13])),
29    ("UTF8.getChar \"\" = NONE", gcSucceeds "" NONE),
30    ("UTF8.getChar 0x41 = #\"A\"", gcSucceeds "A" (SOME(("A", 65), ""))),
31    ("UTF8.getChar A\\000 = #\"A\"",
32     gcSucceeds "A\000" (SOME(("A", 65), "\000"))),
33    ("UTF8.getChar 0x2200 = #\"\226\136\128\"",
34     gcSucceeds "\226\136\128" (SOME(("\226\136\128", 8704), ""))),
35    ("UTF8.getChar 0x2200A = #\"\226\136\128\"",
36     gcSucceeds "\226\136\128A" (SOME(("\226\136\128", 8704), "A"))),
37    ("UTF8.getChar 0x2200-0x2000 = #\"\226\136\128\"",
38     gcSucceeds "\226\136\128\226\136\128"
39                (SOME(("\226\136\128", 8704), "\226\136\128"))),
40    ("UTF8.getChar 0x8F fails", gcFails "\128"),
41    ("UTF8.getChar \"\\192\\128\" fails", gcFails "\192\168"),
42    ("UTF8.getChar \"\\252\\129\\129\\129\\129\\129\" fails",
43     gcFails "\252\129\129\129\129\129"),
44    ("UTF8.getChar \"\\244\\129\" fails", gcFails "\244\129"),
45    ("padRight #\" \" on ���", fn () => UTF8.padRight #" " 5 "���" = "���    "),
46    ("padRight #\"a\" on ���", fn () => UTF8.padRight #"a" 5 "���" = "���aaaa"),
47    ("UTF8.substring(\"a\", 0, 1)", fn () => UTF8.substring("a", 0, 1) = "a"),
48    ("UTF8.substring(\"abc\", 0, 3)",
49     fn () => UTF8.substring("abc", 0, 3) = "abc"),
50    ("UTF8.substring(\"abc\", 1, 3)",
51     fn () => (UTF8.substring("abc", 1, 3); false) handle Subscript => true
52                                                        | e => false),
53    ("UTF8.substring(\"ab\", 1, 1)", fn () => UTF8.substring("ab", 1, 1) = "b"),
54    ("UTF8.substring(\"��ab��\", 1, 2)",
55     fn () => UTF8.substring("��ab��", 1, 2) = "ab")
56    ]
57
58val _ = tprint "mapFilter executes L-to-R"
59val _ = let
60  val r = ref 0
61  fun f x = (r := x; if x mod 2 = 1 then raise Fail "foo" else x + 1)
62  val res = Portable.mapfilter f [1,2,3,4]
63in
64  if res = [3,5] then
65    if !r = 4 then print "OK\n"
66    else die ("\n Evaluation in wrong order; !r = " ^ Int.toString (!r))
67  else
68    die ("\n Evaluation gave wrong result: [" ^
69         String.concatWith ", " (map Int.toString res) ^ "]")
70end
71
72val _ = tprint "Checking HOLsexp-reading"
73val _ = let
74  open HOLsexp
75  val el1 = Cons(Symbol "bar", Symbol "baz")
76  val I = Integer
77  val el2 = List [Quote, List [I 1,I 2,I 3,String "\203a\"", String"foo\n",
78                               Symbol "1+", String "xy\028"]]
79  val t_out = List[Symbol "foo ", el1, el2]
80  val outstrm = TextIO.openOut "test.sexp"
81  val _ = TextIO.output(outstrm,
82                        ";; this is an automatically generated test file\n")
83  val _ = TextIO.output(outstrm, HOLPP.pp_to_string 70 printer t_out ^
84                                 "; another comment \n")
85  val _ = TextIO.closeOut outstrm
86  val t_in = HOLsexp_parser.raw_read_file "test.sexp"
87in
88  if t_in = t_out then print "OK\n"
89  else
90    die ("FAILED, read back:\n  "^
91         HOLPP.pp_to_string 70 printer t_in)
92end
93
94val _ = OS.Process.exit OS.Process.success
95