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