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