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