1100619Smpopen HolKernel Parse boolLib simpLib 2100619Smpopen testutils boolSimps BackchainingLib 3100619Smp 4100619Smpval _ = Portable.catch_SIGINT() 5100619Smp 6100619Smpfun infloop_protect (startstr : string) (endfn : 'a -> bool) 7100619Smp (f : 'b -> 'a) (x : 'b) = 8167469Smp let 9100619Smp 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