1open arithmeticTheory HolKernel boolLib Parse testutils
2
3fun fail() = die "FAILED\n"
4
5val _ = tprint "Testing that I can parse num$0"
6val _ = (Parse.Term`num$0`; OK())
7        handle HOL_ERR _ => fail()
8
9val _ = tprint "Testing that I can't parse num$1"
10val _ = (Parse.Term`num$1`; fail()) handle HOL_ERR _ => OK();
11
12
13val _ = tprint "Testing that bool$0 fails"
14val _ = (Parse.Term`bool$0`; fail()) handle HOL_ERR _ => OK()
15
16val _ = tprint "Testing that num$01 fails"
17val _ = (Parse.Term`num$01`; fail()) handle HOL_ERR _ => OK()
18
19val _ = let
20  val _ = tprint "Anthony's pattern-overloading bug"
21  val b2n_def = new_definition("b2n_def", ``b2n b = if b then 1 else 0``)
22  val _ = overload_on ("foo", ``\(x:num#'a),(y:num#'b). b2n (FST x = FST y)``)
23  val res = trace ("PP.catch_withpp_err", 0) term_to_string ``foo(x,y)``
24            handle Fail _ => ""
25in
26  if res <> "" then OK() else fail()
27end
28
29val _ = let
30  val tpp = let open testutils
31            in
32              unicode_off (raw_backend testutils.tpp)
33            end
34in
35  List.app tpp [
36    "case e1 of 0 => (case e2 of 0 => 1 | SUC n => n + 1) | SUC m => m * 2",
37    "case e1 of 0 => 1 | SUC n => case e2 of 0 => 2 | SUC m => 3",
38    "(case x of 0 => (\\x. x) | SUC n => (\\m. m + n)) y",
39    "!a b c d e f g.\n\
40    \    foo' a b /\\ bar a c /\\ baz a c d /\\ qux f g /\\ foo' f g ==>\n\
41    \    (a + b * c = 10 * d + e + f + g)"
42  ] ;
43  trace ("PP.print_firstcasebar", 1) tpp "case e of | 0 => 1 | SUC n => n + 2";
44  trace ("PP.print_firstcasebar", 1) tpp
45    "case f e n longvarname of\n\
46    \| 0 => superlongvarname * secondsuperlongname + 1\n\
47    \| SUC n => n + 2"
48end
49
50
51
52
53fun colourpp_test (testname, s, expected) =
54    testutils.tpp_expected {testf = (fn _ => testname),
55                            input = s,
56                            output = expected}
57
58val _ = Parse.current_backend := PPBackEnd.vt100_terminal
59
60fun bound s = "\^[[0;32m" ^ s ^ "\^[[0m"
61fun free s = "\^[[0;1;34m" ^ s ^ "\^[[0m"
62val concat = String.concat
63
64val colourtests =
65    [("&3 should print as 3", "&3", "3"),
66     ("Pretty-printing of case expression bound variables",
67      "case x of 0 => 1 | SUC n => n * 2",
68      concat ["case ",free "x"," of 0 => 1 | ", "SUC ", bound "n", " => ",
69              bound "n", " * 2"]),
70     ("Pretty-printing of case in rand position",
71      "f (case x of 0 => 1 | SUC n => n * 2)",
72      concat [free "f", " (case ", free "x", " of 0 => 1 | SUC ", bound "n",
73              " => ", bound "n", " * 2)"]),
74     ("Colouring simple LET", "let x = 3 in x + 1",
75      concat ["let ", bound "x", " = 3 in ", bound "x", " + 1"]),
76     ("Colouring simple LET with free on right",
77      "let x = y + 2 in x * 2",
78      concat ["let ", bound "x", " = ", free "y", " + 2 in ", bound "x",
79              " * 2"]),
80     ("Colouring LET with ands",
81      "let x = 10 and y = x + 6 in x + y",
82      concat ["let ", bound "x", " = 10 and ", bound "y", " = ", free "x",
83              " + 6 in ", bound "x", " + ", bound "y"]),
84     ("Colouring LET binding local function",
85      "let f x = x * 2 in x + f 10",
86      concat ["let ", bound "f", " ", bound "x", " = ", bound "x", " * 2 in ",
87              free "x", " + ", bound "f", " 10"])
88    ]
89
90val _ = app colourpp_test colourtests
91
92open groundEval numeralTheory
93
94val _ = overload_on ("B1", ``BIT1``);
95val _ = overload_on ("B2", ``BIT2``);
96val _ = overload_on ("iZ", ``numeral$iZ``);
97val _ = overload_on ("NUM", ``NUMERAL``)
98
99val ncset = HOLset.addList(empty_tmset,
100                           [``NUMERAL``, ``BIT1``, ``BIT2``,
101                            ``0:num``, ``ZERO``]);
102
103val ge0 = GE {constrs = ncset, rwts = Net.empty, case_consts = empty_tmset }
104val ge = List.foldl (fn (th,ge) => add_rwt th ge) ge0
105                    (Rewrite.mk_rewrites numeralTheory.numeral_distrib @
106                     Rewrite.mk_rewrites numeralTheory.numeral_add @
107                     Rewrite.mk_rewrites numeralTheory.numeral_suc @
108                     Rewrite.mk_rewrites numeralTheory.numeral_iisuc)
109
110fun dot t = reduction ge (vTreeOf ge t) t (Conv (fn x => x));
111fun testdot t expected = let
112  val result = dot t
113in
114    aconv (result_term (dot t)) expected andalso
115    result_tree result = KnownValue
116  orelse
117    die ("Reduction of " ^ term_to_string t ^ " didn't give back " ^
118         term_to_string expected)
119end;
120
121val _ = testdot ``1 + 1`` ``2``;
122val _ = testdot ``2 + 1`` ``3``;
123val _ = testdot ``3 + 4`` ``7``;
124val _ = testdot ``4 + 5 + 9`` ``18``;
125
126val _ = testdot ``(\x. x + y) 5`` ``5 + y``;
127val _ = testdot ``(\x. x + x + 1) ((\y. y + 10) 4)`` ``29``;
128