1open HolKernel Parse boolLib normalForms;
2
3open testutils;
4
5val _ = let
6  val p = mk_var("p", bool)
7  val q = mk_var("q", bool)
8  val v1 = genvar bool
9  val v2 = genvar bool
10  val t1 = mk_conj(p,q)
11  val C = normalForms.PRETTIFY_VARS_CONV
12  val gt1 = mk_abs(v1, mk_conj(v1, p))
13  val gt2 = list_mk_abs([q, v1,v2], list_mk_conj([p,q,v1,q,v2]))
14  fun test (t1,t2) = convtest ("PRETTIFY_CONV "^term_to_string t1, C, t1, t2)
15in
16  app test [(t1, t1), (mk_abs(p,t1), mk_abs(p,t1)),
17            (v1, v1), (gt1, ``\v. v /\ p``),
18            (gt2, ``\q v v0. p /\ q /\ v /\ q /\ v0``)]
19end
20
21val _ = Parse.reveal "C";
22
23fun normalForms_test (fname, function :conv, problem, result) = let
24  val padr = StringCvt.padRight #" ";
25  val padl = StringCvt.padLeft #" ";
26  val f_s = padr 16 fname;
27  val p_s = padr 25 (term_to_string problem);
28  val r_s = padl 10 (term_to_string result);
29  val _ = tprint (f_s ^ p_s ^ " = " ^ r_s);
30in
31    require_msg (check_result (fn tm => (result ~~ (rhs (concl tm)))))
32                (term_to_string o rhs o concl)
33                function (* 'b -> 'a *)
34                problem  (* 'b *)
35end;
36
37val test_cases =
38  [("PRETTIFY_VARS_CONV", PRETTIFY_VARS_CONV,
39    (rhs (concl (DEF_CNF_CONV ``~(p <=> q) ==> q /\ r``))),
40   ``?v x. (x \/ p \/ q) /\ (x \/ ~p \/ ~q) /\ (p \/ ~q \/ ~x) /\
41           (q \/ ~p \/ ~x) /\ (v \/ ~q \/ ~r) /\ (r \/ ~v) /\ (q \/ ~v) /\
42           (v \/ x)``),
43(* "No numerals currently allowed"
44   ("SKI_CONV", SKI_CONV, ``?f. !y. f y = y + 1``,
45    ``$? (S (K $!) (S (S (K S) (S (K (S (K $=))) I)) (K (S $+ (K 1)))))``),
46 *)
47   ("SKI_CONV", SKI_CONV, ``\x:'a. ((f :'a->'a->'a) x o (g :'a->'a))``,
48    ``S (S (K $o) (f :'a->'a->'a)) (K (g :'a->'a))``),
49   ("SKI_CONV", SKI_CONV, ``\x y. (f :'a->'a->'a) x y``,
50    ``S (S (K S) (S (K K) (f :'a->'a->'a))) (K I)``),
51   ("SKI_CONV", SKI_CONV, ``$? = \P. P ($@ P)``, ``$? = S I $@``),
52   ("SKI_CONV", SKI_CONV, ``$==> = \a b. ~a \/ b``,
53    ``$==> = S (S (K S) (S (K K) (S (K $\/) $~))) (K I)``),
54   ("SKI_CONV", SKI_CONV, ``$! = \P. K T = P``, ``$! = S (K ($= (K T))) I``),
55   ("SKI_CONV", SKI_CONV, ``!x:'a y:'a. P x y``,
56    ``$! (S (K $!) (S (S (K S) (S (K K) (P :'a->'a->bool))) (K I)))``),
57   ("SKI_CONV", SKI_CONV, ``!x:'a y:'a. P y x``,
58    ``$! (S (K $!) (S (K (S (P :'a->'a->bool))) K))``),
59   ("SKI_CONV", SKI_CONV, ``(P = Q) <=> (!x. P x <=> Q x)``,
60    ``(P = Q <=> $! (S (S (K $<=>) P) Q))``),
61(* "No numerals currently allowed"
62   ("SKICo_CONV", SKICo_CONV, ``?f. !y. f y = y + 1``,
63    ``$? ($! o C (S o $o $=) (C $+ 1))``),
64 *)
65   ("SKICo_CONV", SKICo_CONV, ``\x:'a. ((f :'a->'a->'a) x o (g :'a->'a))``,
66    ``C ($o o (f :'a->'a->'a)) (g :'a->'a)``),
67   ("SKICo_CONV", SKICo_CONV, ``\x y. (f :'a->'a->'a) x y``,
68    ``C ($o o (f :'a->'a->'a)) I``),
69   ("SKICo_CONV", SKICo_CONV, ``$? = \P. P ($@ P)``, ``$? = S I $@``),
70   ("SKICo_CONV", SKICo_CONV, ``$==> = \a b. ~a \/ b``,
71    ``$==> = C ($o o $\/ o $~) I``),
72   ("SKICo_CONV", SKICo_CONV, ``$! = \P. K T = P``, ``$! = $= (K T)``),
73   ("SKICo_CONV", SKICo_CONV, ``!x y. (P :'a->'a->bool) x y``,
74    ``$! ($! o C ($o o (P :'a->'a->bool)) I)``),
75   ("SKICo_CONV", SKICo_CONV, ``!x y. (P :'a->'a->bool) y x``,
76    ``$! ($! o C (P :'a->'a->bool))``),
77   ("SKICo_CONV", SKICo_CONV, ``(P = Q) = (!x. P x = Q x)``,
78    ``(P = Q <=> $! (S ($= o P) Q))``),
79   ("SIMPLIFY_CONV", SIMPLIFY_CONV, ``(!x y. P x \/ (P y /\ F)) ==> ?z. P z``,
80    ``(!x. P x) ==> ?z. P z``),
81   ("NNF_CONV", NNF_CONV, ``(!x. P(x)) ==> ((?y. Q(y)) = (?z. P(z) /\ Q(z)))``,
82    ``((?y. Q y) \/ !z. ~P z \/ ~Q z) /\ ((!y. ~Q y) \/ ?z. P z /\ Q z) \/
83      ?x. ~P x``),
84   ("NNF_CONV", NNF_CONV, ``~(~(x = y) = z) = ~(x = ~(y = z))``,
85    ``(((x \/ y) /\ (~x \/ ~y) \/ z) /\ ((x \/ ~y) /\ (~x \/ y) \/ ~z) \/
86       (x \/ (y \/ ~z) /\ (~y \/ z)) /\ (~x \/ (y \/ z) /\ (~y \/ ~z))) /\
87      (((x \/ y) /\ (~x \/ ~y) \/ ~z) /\ ((x \/ ~y) /\ (~x \/ y) \/ z) \/
88       (x \/ (y \/ z) /\ (~y \/ ~z)) /\ (~x \/ (y \/ ~z) /\ (~y \/ z)))``),
89   ("SKOLEMIZE_CONV", SKOLEMIZE_CONV,
90    ``!x. (?y. Q y \/ !z. ~P z \/ ~Q z) \/ ~P x``,
91    ``?y. !x. (Q (y x) \/ !z. ~P z \/ ~Q z) \/ ~P x``),
92   ("TAUTOLOGY_CONV", TAUTOLOGY_CONV, ``p \/ r \/ ~p \/ ~q``, T),
93   ("CONTRACT_CONV", CONTRACT_CONV, ``(p \/ r) \/ p \/ ~q``, ``r \/ p \/ ~q``)
94  ];
95
96val _ = List.app (ignore o normalForms_test) test_cases;
97
98val _ = Process.exit Process.success;
99