1open HolKernel Parse boolLib simpLib
2open testutils boolSimps BackchainingLib
3
4val _ = Portable.catch_SIGINT()
5
6fun infloop_protect (startstr : string) (endfn : 'a -> bool)
7    (f : 'b -> 'a) (x : 'b) =
8    let
9      val _ =  tprint startstr
10      val r = f x
11    in
12      if endfn r then
13        (OK(); (true, SOME r))
14      else
15        die "FAILED\n"
16    end handle Interrupt => die "FAILED"
17             | e => die ("EXN: "^General.exnMessage e)
18
19(* earlier versions of the simplifier would go into an infinite loop on
20   terms of this form. *)
21val const_term = ``(ARB : bool -> bool) ((ARB : bool -> bool) ARB)``
22val test_term = ``^const_term /\ x /\ y``
23
24val (test1_flag, result1) =
25    infloop_protect
26      "AC looping (if test appears to hang, it has failed)"
27      (K true)
28      (QCONV (SIMP_CONV bool_ss
29                        [AC CONJ_ASSOC CONJ_COMM]))
30      test_term
31
32(* test that AC works with the arguments messed up *)
33fun test2P th2 = aconv (rhs (concl (valOf result1))) (rhs (concl th2))
34val (test2_flag, _) =
35    infloop_protect "Permuted AC arguments"
36                    test2P
37                    (QCONV (SIMP_CONV bool_ss
38                                      [AC CONJ_COMM CONJ_ASSOC]))
39                    test_term
40
41(* test bounded simplification *)
42fun test3P th = aconv (rhs (concl th)) ``P(f (g (x:'a):'a) : 'a):bool``
43val (test3_flag, _) =
44    infloop_protect
45      "Bounded rewrites (if test appears to hang, it has failed)"
46      test3P
47      (QCONV (SIMP_CONV bool_ss
48                        [Once (Q.ASSUME `x:'a = f (y:'a)`),
49                         Q.ASSUME `y:'a = g (x:'a)`]))
50      ``P (x:'a) : bool``
51
52(* test abbreviations in tactics *)
53fun test4P (sgs, vfn) =
54    length sgs = 1 andalso
55    (let val (asms, gl) = hd sgs
56     in
57       aconv gl ``Q (f (x:'a) : 'b) : bool`` andalso
58       length asms = 1 andalso
59       aconv (hd asms) ``P (f (x:'a) : 'b) : bool``
60     end)
61
62val (test4_flag, _) =
63    infloop_protect
64      "Abbreviations + ASM_SIMP_TAC"
65      test4P
66      (ASM_SIMP_TAC bool_ss [markerSyntax.Abbr`y`])
67      ([``Abbrev (y:'b = f (x : 'a))``, ``P (y:'b) : bool``],
68       ``Q (y:'b) : bool``)
69
70(* test that bounded rewrites get applied to both branches, and also that
71   the bound on the rewrite allows it to apply at all (normally it wouldn't)
72*)
73val goal5 = ``(x:'a = y) <=> (y = x)``
74val test5P =
75    infloop_protect
76        "Bounded rewrites branch, and bypass permutative loop check"
77        (fn (sgs, vf) => null sgs andalso let
78                           val th = vf []
79                         in
80                           aconv (concl th) goal5 andalso null (hyp th)
81                         end)
82        (fn g => (EQ_TAC THEN STRIP_TAC THEN
83                  SIMP_TAC bool_ss [Once EQ_SYM_EQ] THEN
84                  POP_ASSUM ACCEPT_TAC) g)
85        ([], goal5)
86
87val test5_flag = #1 test5P
88
89(* test that being a bounded rewrite overrides detection of loops in
90   mk_rewrites code *)
91val (test6_flag, _) = let
92  open boolSimps
93  val rwt_th = ASSUME ``!x:'a. (f:'a -> 'b) x = if P x then z
94                                     else let x = g x in f x``
95  val Pa_th = ASSUME ``P (a:'a) : bool``
96  fun doit t = (QCONV (SIMP_CONV bool_ss [Pa_th, Once rwt_th]) t,
97                QCONV (SIMP_CONV bool_ss [Pa_th, rwt_th]) t)
98  fun check (th1, th2) =
99      aconv (rhs (concl th1)) ``z:'b`` andalso length (hyp th1) = 2 andalso
100      aconv (rhs (concl th2)) ``f (a:'a):'b``
101in
102  infloop_protect
103      "Bounded rewrites override mk_rewrites loop check"
104      check
105      doit
106      ``f (a:'a) : 'b``
107end
108
109(* test that a bounded rewrite on a variable gets a chance to fire at all *)
110val (test7_flag, _) = let
111  open pureSimps
112  val rwt_th = ASSUME ``!x:'a. x:'a = f x``
113  val t = ``x:'a = z``
114  fun doit t = QCONV (SIMP_CONV pure_ss [Once rwt_th]) t
115  fun check th = aconv (rhs (concl th)) ``f (x:'a):'a = z``
116in
117  infloop_protect
118      "Bounded rwts on variables don't get decremented prematurely"
119      check
120      doit
121      t
122end
123
124(* test that a bound on a rewrite applies to all derived rewrite theorems *)
125val (test8_flag, _) = let
126  open boolSimps
127  val rwt_th = ASSUME ``(p:bool = x) /\ (q:bool = x)``
128  val t = ``p /\ q``
129  fun doit t = QCONV (SIMP_CONV bool_ss [Once rwt_th]) t
130  fun check th = not (aconv (rhs (concl th)) ``x:bool``)
131in
132  infloop_protect
133      "Bound on rewrites applies to all derived theorems jointly."
134      check
135      doit
136      t
137end
138
139(* test that congruence rule for conditional expressions is working OK *)
140val (test9_flag,_) = let
141  open boolSimps
142  val t = ``if a then f a:'a else g a``
143  val result = ``if a then f T:'a else g F``
144  fun doit t = QCONV (SIMP_CONV bool_ss []) t
145  fun check th = aconv (rhs (concl th)) result
146in
147  infloop_protect "Congruence for conditional expressions" check doit t
148end
149
150val (test10_flag,_) = let
151  open boolSimps
152  val t = ``I (f:'b -> 'c) o I (g:'a -> 'b)``
153  val result = ``(f:'b -> 'c) o I (g:'a -> 'b)``
154  val doit = QCONV (SIMP_CONV (bool_ss ++ combinSimps.COMBIN_ss)
155                              [SimpL ``$o``])
156  fun check th = aconv (rhs (concl th)) result
157in
158  infloop_protect "SimpL on operator returning non-boolean" check doit t
159end
160
161
162val (test11_flag,_) = let
163  open boolSimps
164  val t = ``(!n:'a. P n n) ==> ?m. P c m``
165  val result = ``T``
166  val doit = QCONV (SIMP_CONV (bool_ss ++ SatisfySimps.SATISFY_ss) [])
167  fun check th = aconv (rhs (concl th)) result
168in
169  infloop_protect "Satisfy" check doit t
170end
171
172val _ = let
173  val asm = ``Abbrev(f = (\x. x /\ y))``
174  val g = ([asm], ``p /\ y``)
175  val doit = ASM_SIMP_TAC bool_ss []
176  fun geq (asl1, g1) (asl2, g2) =
177      aconv g1 g2 andalso
178      case (asl1, asl2) of
179           ([a1], [a2]) => aconv a1 asm andalso aconv a2 asm
180         | _ => false
181  fun check (sgs, vfn) = let
182    val sgs_ok =
183      case sgs of
184          [goal] => geq goal ([asm], ``(f:bool -> bool) p``)
185        | _ => false
186  in
187    sgs_ok andalso geq (dest_thm (vfn [mk_thm (hd sgs)])) g
188  end
189in
190  infloop_protect "Abbrev-simplification with abstraction" check doit g
191end
192
193(* rewrites on F and T *)
194val TF = mk_eq(T,F)
195val FT = mk_eq(F,T)
196
197val _ = let
198  val t = TF
199  val doit = QCONV (SIMP_CONV bool_ss [ASSUME TF, ASSUME FT])
200  fun check th = th |> concl |> rhs |> aconv F
201in
202  infloop_protect "assume T=F and F=T (if hangs, it's failed)" check doit t
203end
204
205
206(* conjunction congruence *)
207val _ = let
208  val t = list_mk_conj [TF,FT,TF]
209  val doit = QCONV (SIMP_CONV (bool_ss ++ CONJ_ss) [])
210  fun check th = th |> concl |> rhs |> aconv F
211in
212  infloop_protect "CONJ_ss with T=F and F=T assumptions (if hangs, it's failed)" check doit t
213end
214
215(* ---------------------------------------------------------------------- *)
216
217val _ = let
218  val _ = tprint "Cond_rewr.mk_cond_rewrs on ``hyp ==> (T = e)``"
219in
220  case Lib.total Cond_rewr.mk_cond_rewrs
221                 (ASSUME ``P x ==> (T = Q y)``, BoundedRewrites.UNBOUNDED)
222   of
223      NONE => die "FAILED!"
224    | SOME _ => OK()
225end
226
227local
228  fun die_r l =
229    die ("\n  FAILED!  Incorrectly generated rewrites\n  " ^
230         String.concatWith "\n  " (map (thm_to_string o #1) l))
231fun testb (s, thm, c) =
232  let
233    val _ = tprint ("Cond_rewr.mk_cond_rewrs on "^s)
234  in
235    case Lib.total Cond_rewr.mk_cond_rewrs(thm, BoundedRewrites.UNBOUNDED)
236     of
237        NONE => die "EXN-FAILED!"
238      | SOME l => if length l = c then OK() else die_r l
239  end
240val lem1 = prove(���a <> b ==> (a = ~b)���,
241                 ASM_CASES_TAC ���a:bool��� THEN ASM_REWRITE_TAC[])
242val marker = GSYM markerTheory.Abbrev_def
243in
244val _ = app testb [
245  ("���hyp ==> b���", ASSUME ���(!b x y. (P x y = b) ==> b)���, 0),
246  ("���hyp ==> ~b���", ASSUME ���(!b x y. (p x y = b) ==> ~b)���, 0),
247  ("���hyp ==> b=e���", ASSUME ���(!b:bool x y. (p x y = b) ==> (b = e))���, 2),
248  ("���a <> b ==> (a = ~b)", lem1, 2),
249  ("x = Abbrev x", marker, 2)
250]
251
252val _ = tprint "Cond_rewr.mk_cond_rewrs on bounded x <=> Abbrev x"
253val _ = let
254  val b = BoundedRewrites.BOUNDED (ref 1)
255in
256  case Lib.total Cond_rewr.mk_cond_rewrs (marker, b) of
257      NONE => die "EXN-FAILED!"
258    | SOME (rs as [(th',b')]) =>
259        if concl th' ~~ (marker |> concl |> strip_forall |> #2) then OK()
260        else die_r rs
261    | SOME rs => die_r rs
262end
263end (* local fun testb ... *)
264
265val _ = Process.exit Process.success
266