1open HolKernel Parse 2open Defn 3 4open testutils 5 6fun test msg f x = (tprint msg; require (check_result (K true)) f x) 7 8val _ = print "\n" 9 10val def1 = test "Defn with IFF" (Hol_defn "foo") `foo p <=> p /\ F`; 11 12(* check parsability of quantified equation *) 13val _ = test "Parse quantified eqn" Defn.parse_absyn (Absyn`���x. bar x = foo x`) 14 15val x_def = new_definition("x_def", ``x = \y. F``) 16 17val def3 = test "Constant as parameter (=)" (Hol_defn "baz1") `baz1 x = (x /\ F)` 18val def4 = 19 test "Constant as parameter (<=>)" (Hol_defn "baz2") `baz2 x <=> x /\ F` 20val def5 = 21 test "Type-constrainted constant as parameter" 22 (Hol_defn "baz3") `baz3 (x:bool) <=> x /\ F` 23val _ = 24 test "Constant as parameter under quantifier" 25 Defn.parse_absyn (Absyn`!y. baz4 x y = (x /\ y)`) 26 27val def6 = test "Case expression with multiple underscores" 28 (Hol_defn "f1") 29 `(f1 x y = case (x, y:'a) of (T, _) => T | (_,_) => F)` 30val def7 = test "Case expression with underscores of different types" 31 (Hol_defn "f2") 32 `(f2 x y = case (x, y:'a) of (T, _) => T | _ => F)` 33 34val def8 = test "Case expression with variables of different types" 35 (Hol_defn "f3") 36 `f3 x = case x of (f,T,_) => ~f | (_,F,f) => f F`; 37 38val _ = overload_on ("=", ``T``) 39val _ = test "Definition with overloaded =" (Hol_defn "f4") `f4 x y = (x /\ y)` 40 41val _ = temp_overload_on("foo", ``bool$F``) 42val _ = Hol_defn "F" `F f x <=> x \/ f x`; 43val _ = tpp_expected{ 44 input="foo", 45 output="foo", 46 testf = (fn _ => "Printing after definition on unoverloaded name") 47}; 48 49fun define q = 50 let 51 val (tm, names) = Defn.parse_absyn (Parse.Absyn q) 52 in 53 Defn.mk_defn (hd names) tm 54 end 55fun exnlookfor sl (Exn (HOL_ERR {message,...})) = 56 if List.all (fn s => String.isSubstring s message) sl then OK() 57 else 58 die ("\nBad exception message:\n "^message) 59 | exnlookfor _ (Exn e) = 60 die ("\nException not a HOL_ERR;\n "^General.exnMessage e) 61 | exnlookfor _ _ = die ("\nExecution unexpectedly successful") 62 63fun badvarcheck r = 64 exnlookfor ["Simple definition failed", "Free variables in rhs"] r 65 66fun wfunivq r = 67 exnlookfor ["Universally quantified equation as argument"] r 68 69val _ = tprint "Excess vars on RHS of def reported correctly(=,no !)" 70val _ = timed define badvarcheck `ll20180807A x = (x /\ y)` 71 72val _ = tprint "Excess vars on RHS of def reported correctly(=,!)" 73val _ = timed define badvarcheck `!x. ll20180807B x = (x /\ y)`; 74 75val _ = tprint "Excess vars on RHS of def reported correctly(<=>,no !)" 76val _ = timed define badvarcheck `ll20180807C x <=> x /\ y`; 77 78val _ = tprint "Excess vars on RHS of def reported correctly(<=>,!)" 79val _ = timed define badvarcheck `!x. ll20180807D x <=> x /\ y`; 80 81val _ = tprint "Better message for use of q-fied eqn in wfrec def" 82val _ = timed define wfunivq `!x. ll20180807E x <=> y /\ ll20180807E (x ==> y)`; 83