1open Parse boolLib HolKernel testutils 2 3val _ = tprint "Testing Q.EXISTS ... " 4 5val th = Q.EXISTS (`?f. f T T = T`, `$/\`) (REWRITE_CONV [] ``T /\ T``) 6 handle HOL_ERR _ => die "FAILED!" 7 8val _ = OK() 9 10val _ = tprint "Testing Q.REFINE_EXISTS_TAC" 11 12val asm = ``!x1:'a x2:'a y1:'b y2:'b. (f x1 y1:'c = f x2 y2) <=> (x1 = x2) /\ (y1 = y2)`` 13val goal = ``?a:'c b:'d. Q a b`` 14val (sgs, vfn) = Q.REFINE_EXISTS_TAC `f x y` ([asm], goal) 15 handle _ => die "FAILED!" 16val expected_sg = ``?x:'a y:'b b:'d. Q (f x y:'c) b`` 17val result = 18 case sgs of 19 [g as ([a],g')] => if aconv a asm andalso aconv g' expected_sg 20 then vfn [mk_thm g] 21 else die "FAILED!" 22 | _ => die "FAILED!" 23val _ = if aconv (concl result) goal then 24 case hyp result of 25 [a] => if aconv a asm then OK() else die "FAILED!" 26 | _ => die "FAILED!" 27 else die "FAILED!" 28 29(* combinator *) 30val _ = new_definition("I_DEF", ``I = \x:'a. x``); 31 32(* fake arithmetic *) 33val _ = new_type ("num", 0) 34val _ = new_constant ("*", ``:num -> num -> num``) 35val _ = new_constant ("+", ``:num -> num -> num``) 36val _ = new_constant ("<", ``:num -> num -> bool``) 37val _ = new_constant ("SUC", ``:num -> num``) 38val _ = new_constant ("zero", ``:num``) 39val _ = set_fixity "+" (Infixl 500) 40val _ = set_fixity "*" (Infixl 600) 41val _ = set_fixity "<" (Infix(NONASSOC, 450)) 42 43fun aconvdie m t1 t2 = aconv t1 t2 orelse die ("FAILED! (" ^ m ^ " wrong)") 44 45val _ = tprint "Q.MATCH_RENAME_TAC 1" 46val gl0 = ([``x < y``], ``x = z:num``) 47val expected_a0 = ``a < y`` 48val expected_c0 = ``a = b:num`` 49val (sgs, _) = Q.MATCH_RENAME_TAC `a = b` gl0 50val _ = case sgs of 51 [([a], c)] => (aconvdie "assumption" a expected_a0; 52 aconvdie "goal" c expected_c0; 53 OK()) 54 | _ => die "FAILED!" 55 56val _ = tprint "Q.MATCH_RENAME_TAC 2" 57val glmrt2 = ([] : term list, ``f ((h : 'a -> 'b) s) = s``) 58val expected_mrt2 = ``(f : 'b -> 'a) z = v`` 59val (sgs, _) = Q.MATCH_RENAME_TAC `f z = v` glmrt2 60val _ = case sgs of 61 [([], c)] => (aconvdie "conclusion" c expected_mrt2; OK()) 62 | _ => die "FAILED!" 63 64val _ = tprint "Q.MATCH_RENAME_TAC 3" 65val glmrt3 = ([] : term list, ``f zero zero = (z:'a)``) 66val expected_mrt3 = ``f (a:num) a = (u:'a)`` 67val (sgs, _) = Q.MATCH_RENAME_TAC `f b a = u` glmrt3 68val _ = case sgs of 69 [([], c)] => (aconvdie "conclusion" c expected_mrt3; OK()) 70 | _ => die "FAILED!" 71 72val _ = tprint "Q.MATCH_ABBREV_TAC 1" 73val expected_mat1c = ``f (a:num) a = (u:'a)`` 74val expected_mat1a1 = ``Abbrev (b = zero)`` 75val expected_mat1a2 = ``Abbrev (a:num = b)`` 76val expected_mat1a3 = ``Abbrev (u:'a = z)`` 77val (sgs, _) = Q.MATCH_ABBREV_TAC `f b a = u` glmrt3 78val _ = case sgs of 79 [([a1,a2,a3], c)] => 80 let 81 val _ = aconvdie "assumption #1" a1 expected_mat1a1 82 val _ = aconvdie "assumption #2" a2 expected_mat1a2 83 val _ = aconvdie "assumption #3" a3 expected_mat1a3 84 val _ = aconvdie "goal conclusion" c expected_mat1c 85 in 86 OK() 87 end 88 | _ => die "FAILED! (new goal of wrong shape)" 89 90val _ = tprint "Q.MATCH_ABBREV_TAC 2" 91val expected_mat2c = ``(f : 'b -> 'a) z = v`` 92(* first assumption is most recently created *) 93val expected_mat2a1 = ``Abbrev(v : 'a = s)`` 94val expected_mat2a2 = ``Abbrev(z :'b = h (v:'a))`` 95val (sgs, _) = Q.MATCH_ABBREV_TAC `f z = v` glmrt2 96val _ = case sgs of 97 [([a1, a2], c)] => 98 let 99 val _ = aconvdie "goal conclusion" c expected_mat2c 100 val _ = aconvdie "assumption #1" a1 expected_mat2a1 101 val _ = aconvdie "assumption #2" a2 expected_mat2a2 102 in 103 OK() 104 end 105 | _ => die "FAILED! (new goal of wrong shape)" 106 107val _ = tprint "Q.MATCH_GOALSUB_RENAME_TAC 1" 108val gl1 = ([] : term list, 109 ``!x. x * SUC (SUC zero) < y * (z + SUC zero) * (y + a)``) 110val expected_result1 = 111 ``!x. x * SUC (SUC zero) < y * (z + SUC zero) * (y + c)`` 112val (sgs, _) = Q.MATCH_GOALSUB_RENAME_TAC `y + c` gl1 113val _ = case sgs of 114 [([], t)] => (aconvdie "goal" t expected_result1; OK()) 115 | _ => die "FAILED!" 116 117val _ = tprint "Q.MATCH_GOALSUB_ABBREV_TAC 1" 118val gl1 = ([] : term list, 119 ``!x. x * SUC (SUC zero) < y * (z + SUC zero) * (y + a)``) 120val expected_result1 = 121 ``!x. x * SUC (SUC zero) < y * s * (y + a)`` 122val expected_abbrev = 123 ``Abbrev(s = z + SUC zero)`` 124val (sgs, _) = Q.MATCH_GOALSUB_ABBREV_TAC `y * s` gl1 125val _ = case sgs of 126 [([a], t)] => (aconvdie "assumption" a expected_abbrev; 127 aconvdie "goal" t expected_result1; 128 OK()) 129 | _ => die "FAILED!" 130 131val _ = tprint "Q.MATCH_GOALSUB_RENAME_TAC 2" 132val gl2 = ([] : term list, 133 ``!x. x * SUC zero < y * (z + SUC zero) * (z + SUC (SUC zero))``) 134val expected_result2 = ``!x. x * c < y * (a + c) * (a + SUC c)`` 135val (sgs, _) = Q.MATCH_GOALSUB_RENAME_TAC `a + c` gl2 136val _ = case sgs of 137 [([], t)] => 138 (aconvdie "goal conclusion" t expected_result2; OK()) 139 | _ => die "FAILED!" 140 141val _ = tprint "Q.MATCH_GOALSUB_RENAME_TAC 3" 142val gl2a = ([] : term list, ``!x. x * SUC zero < z``) 143val expected_result2a = #2 gl2a 144val (sgs, _) = Q.MATCH_GOALSUB_RENAME_TAC `SUC` gl2a 145val _ = case sgs of 146 [([], t)] => 147 (aconvdie "goal conclusion" t expected_result2a; OK()) 148 | _ => die "FAILED!" 149 150 151val _ = tprint "Q.MATCH_ASMSUB_RENAME_TAC 1" 152val gl3 = ([``P (x:num): bool``, ``Q (x < SUC (SUC (SUC zero))) : bool``], 153 ``x + y < SUC (SUC zero)``); 154val expected_a1 = ``P (x:num) : bool`` 155val expected_a2 = ``Q (x < n) : bool`` 156val expected_c = ``x + y < SUC (SUC zero)`` 157val (sgs, _) = Q.MATCH_ASMSUB_RENAME_TAC `x < n` gl3 158val _ = case sgs of 159 [([a1, a2], c)] => (aconvdie "assumption #1" a1 expected_a1; 160 aconvdie "assumption #2" a2 expected_a2; 161 aconvdie "goal conclusion" c expected_c; 162 OK()) 163 | _ => die "FAILED!" 164 165val _ = tprint "Q.MATCH_ASMSUB_ABBREV_TAC 1" 166val gl3 = ([``P (x:num): bool``, ``Q (x < SUC (SUC (SUC zero))) : bool``], 167 ``x + y < SUC (SUC zero)``); 168val expected_a1 = ``Abbrev(two = SUC (SUC zero))`` 169val expected_a2 = ``P (x:num) : bool`` 170val expected_a3 = ``Q (x < SUC two) : bool`` 171val expected_c = ``x + y < two`` 172val (sgs, _) = Q.MATCH_ASMSUB_ABBREV_TAC `x < _ two` gl3 173val _ = case sgs of 174 [([a1, a2, a3], c)] => 175 (aconvdie "assumption #1" a1 expected_a1; 176 aconvdie "assumption #2" a2 expected_a2; 177 aconvdie "assumption #3" a3 expected_a3; 178 aconvdie "goal conclusion" c expected_c; 179 OK()) 180 | _ => die "FAILED!" 181 182val _ = tprint "Q.PAT_ABBREV_TAC (gh252)" 183val (sgs, _) = Q.PAT_ABBREV_TAC `v = I x` ([], ``I p /\ v``) 184val _ = OK() 185 186fun shouldfail f x = 187 (f x ; die "FAILED!") handle HOL_ERR _ => OK() 188 189val _ = tprint "Q.PAT_ABBREV_TAC (gh262) 1" 190val (sgs, _) = 191 Q.PAT_ABBREV_TAC `v = (x < SUC w)` ([], ``y < SUC zero ==> y < z``) 192val _ = case sgs of 193 [([abb], sg)] => 194 if Term.aconv abb ``Abbrev(v = y < SUC zero)`` andalso 195 Term.aconv sg ``v ==> y < z`` 196 then OK() 197 else die "FAILED!" 198 | _ => die "FAILED!" 199 200val _ = tprint "Q.PAT_ABBREV_TAC (gh262) 2" 201val _ = shouldfail (Q.PAT_ABBREV_TAC `v = (x < SUC z)`) 202 ([], ``!x. x < SUC zero``) 203 204val _ = tprint "Q.PAT_ABBREV_TAC (gh262) 3" 205val _ = shouldfail (Q.PAT_ABBREV_TAC `v = (x < SUC z)`) 206 ([], ``!y. y < SUC zero``) 207 208val _ = tprint "Q.PAT_ABBREV_TAC (gh262) 4" 209val _ = shouldfail (Q.PAT_ABBREV_TAC `v = (x < SUC z)`) 210 ([], ``(!y. y < SUC zero) /\ y < zero``) 211 212val _ = tprint "Q.PAT_ABBREV_TAC (gh262) 5" 213val (sgs,_) = Q.PAT_ABBREV_TAC `v = (x < SUC z)` 214 ([], ``(!y. y < SUC zero) /\ u < SUC (SUC zero)``) 215val _ = case sgs of 216 [([abb], sg)] => 217 if Term.aconv abb ``Abbrev (v = u < SUC (SUC zero))`` andalso 218 Term.aconv sg ``(!y. y < SUC zero) /\ v`` 219 then OK() 220 else die "FAILED!" 221 | _ => die "FAILED!" 222 223val _ = tprint "Q.PAT_ABBREV_TAC (gh262) 6" 224val (sgs,_) = Q.PAT_ABBREV_TAC `v = (x < SUC z)` 225 ([], ``(!x. x < SUC zero) /\ u < SUC (SUC zero)``) 226val _ = case sgs of 227 [([abb], sg)] => 228 if Term.aconv abb ``Abbrev (v = u < SUC (SUC zero))`` andalso 229 Term.aconv sg ``(!y. y < SUC zero) /\ v`` 230 then OK() 231 else die "FAILED!" 232 | _ => die "FAILED!" 233 234fun tactest (nm, tac, g, expected) = 235 let 236 val _ = tprint nm 237 val (sgs, _) = tac g 238 in 239 if list_compare (pair_compare(list_compare Term.compare, Term.compare)) 240 (sgs, expected) = EQUAL 241 then 242 OK() 243 else die "FAILED!" 244 end 245 246val fa_y = ``!y:'a. P y`` 247val fa_n = ``!n:num. SUC n < zero`` 248val _ = new_type ("int", 0) 249val _ = new_constant ("int_plus1", ``:int -> int``) 250val fa_i = ``!i:int. Q i`` 251val _ = overload_on("SUC", ``int_plus1``) 252val _ = List.app tactest [ 253 ("Q.SPEC_THEN 1", FIRST_X_ASSUM (Q.SPEC_THEN `x` MP_TAC), 254 ([fa_y, fa_n], ``x < x``), 255 [([fa_y], ``SUC x < zero ==> x < x``)]), 256 257 ("Q.SPEC_THEN 2", FIRST_X_ASSUM (Q.SPEC_THEN `SUC x` MP_TAC), 258 ([fa_y, fa_n], ``x < f (y:int)``), 259 [([fa_y], ``SUC (SUC x) < zero ==> x < f (y:int)``)]), 260 261 ("Q.SPEC_THEN 3", FIRST_X_ASSUM (Q.SPEC_THEN `SUC j` MP_TAC), 262 ([fa_y, fa_i, fa_n], ``x < f (y:int)``), 263 [([fa_y, fa_n], ``Q (int_plus1 j) ==> x < f (y:int)``)]), 264 265 ("Q.SPECL_THEN 1", FIRST_X_ASSUM (Q.SPECL_THEN [`SUC x`, `x`] MP_TAC), 266 ([fa_y, fa_n, ``!j k. j < k``], ``x < x``), 267 [([fa_y, fa_n], ``SUC x < x ==> x < x``)]), 268 269 ("Q.SPECL_THEN 2", FIRST_X_ASSUM (Q.SPECL_THEN [`SUC x`, `x`] MP_TAC), 270 ([fa_y, fa_n, fa_i, ``!j k. j < k``], ``x < x``), 271 [([fa_y, fa_n, fa_i], ``SUC x < x ==> x < x``)]), 272 273 ("Q.SPECL_THEN 3", FIRST_X_ASSUM (Q.SPECL_THEN [`SUC x`, `x`] MP_TAC), 274 ([fa_y, fa_n, fa_i, ``!j (k:int). j < f k``, ``!a b. a < b``], 275 ``x < x``), 276 [([fa_y, fa_n, fa_i, ``!j (k:int). j < f k``], 277 ``SUC x < x ==> x < x``)]), 278 279 ("Q.SPECL_THEN 4", FIRST_X_ASSUM (Q.SPECL_THEN [`SUC x`, `j`] MP_TAC), 280 ([fa_y, fa_n, fa_i, ``!j (k:int). j < f k``, ``!a b. a < b``], 281 ``x < x``), 282 [([fa_y, fa_n, fa_i, ``!a b. a < b``], 283 ``SUC x < f (j:int) ==> x < x``)]) 284 ] 285 286val _ = tprint "Q.GENL variable order" 287val vnms = ASSUME ``!x:'a y:'a z:'a. P x y z`` 288 |> SPEC_ALL 289 |> Q.GENL [`x`, `y`, `z`] 290 |> concl |> strip_forall |> #1 |> map (#1 o dest_var) 291val _ = if vnms = ["x", "y", "z"] then OK() else die "FAILED!" 292 293val _ = tprint "Q.MATCH_RENAME_TAC on overloads" 294val foo1_def = new_definition("foo1_def", ``foo1 x y z = (x ==> y /\ z)``); 295val foo2_def = new_definition("foo2_def", ``foo2 x y z = (x ==> y \/ z)``); 296val _ = overload_on("foo", ``foo1``); 297val _ = overload_on("foo", ``foo2``); 298 299val th = TAC_PROOF(([], ``foo1 F x y``), 300 Q.MATCH_RENAME_TAC `foo F a b` >> 301 REWRITE_TAC [foo1_def]) handle HOL_ERR _ => die "FAILED!" 302val _ = OK() 303 304val _ = tprint "Q.RENAME1 on overloads" 305val th = TAC_PROOF(([], ``?v. foo1 v x y``), 306 Q.RENAME1_TAC `foo _ a b` >> 307 Q.EXISTS_TAC `F` >> 308 REWRITE_TAC [foo1_def]) handle HOL_ERR _ => die "FAILED!" 309val _ = OK() 310 311val _ = tprint "Q.kRENAME_TAC(1)" 312val th = TAC_PROOF (([``foo1 a b c``, ``foo2 d e f``], ``?x y z. foo1 x y z``), 313 Q.kRENAME_TAC [`foo u v w`] 314 (MAP_EVERY Q.EXISTS_TAC [`u`, `v`, `w`] THEN 315 FIRST_ASSUM ACCEPT_TAC)) 316 handle HOL_ERR _ => die "FAILED!" 317val _ = OK() 318 319val _ = tprint "Q.kRENAME_TAC(2)" 320val th = TAC_PROOF (([``foo2 a b c``, ``foo1 d e f``], ``?x y z. foo1 x y z``), 321 Q.kRENAME_TAC [`foo u v w`] 322 (MAP_EVERY Q.EXISTS_TAC [`u`, `v`, `w`] THEN 323 FIRST_ASSUM ACCEPT_TAC)) 324 handle HOL_ERR _ => die "FAILED!" 325val _ = OK() 326 327val _ = tprint "PAT_ABBREV_TAC respects Parse.hide" 328val _ = new_definition ("gh431_def", ``gh431 x = ~x``); 329val _ = hide "gh431" 330val th = (Q.PAT_ABBREV_TAC `gh431 = T` THEN Q.UNABBREV_TAC `gh431` THEN 331 REWRITE_TAC []) 332 ([], ``p /\ T = p``) handle HOL_ERR _ => die "FAILED\n" 333val _ = OK() 334 335val _ = new_definition ("gh425a_def", ``gh425a a = a``); 336val _ = new_definition ("gh425b_def", ``gh425b p = (p ==> T)``); 337val _ = overload_on ("gh425", ``gh425a``); 338val _ = overload_on ("gh425", ``gh425b``); 339val buf = ref ([] : string list) 340fun app s = buf := s :: !buf 341fun testquiet f x = 342 (buf := []; 343 let val result = 344 (Lib.with_flag (Feedback.MESG_outstream, app) o 345 Lib.with_flag (Feedback.ERR_outstream, app) o 346 Lib.with_flag (Feedback.WARNING_outstream, app) o 347 Lib.with_flag (Globals.interactive, true)) (Lib.total f) x 348 val _ = 349 null (!buf) orelse 350 die ("\n FAILED : buf contains " ^ String.concatWith "\n" (!buf)) 351 in 352 result 353 end); 354 355val _ = tprint "(Interactive) PAT_ASSUM quiet about tyvar guesses(1)" 356val result = testquiet 357 (Q.PAT_X_ASSUM `gh425a (g x)` mp_tac) 358 ([``gh425a (f T) : bool``], ``p /\ q``) 359val _ = case result of 360 SOME ([([], t)],_) => 361 if aconv t ``gh425a (f T) ==> p /\ q`` then OK() 362 else die "\nFAILED - Incorrect result" 363 | _ => die "\nFAILED - Incorrect result" 364 365val _ = tprint "(Interactive) PAT_ASSUM quiet about tyvar guesses(2)" 366val _ = testquiet 367 (Q.PAT_X_ASSUM `gh245 (g x)` mp_tac) 368 ([``gh425a (f T) : bool``], ``p /\ q``) 369val _ = OK() 370 371val _ = tprint "(Interactive) PAT_ASSUM quiet about tyvar guesses(3)" 372val _ = testquiet 373 (Q.PAT_X_ASSUM `gh245 x` mp_tac) 374 ([``gh425b (f T) : bool``], ``p /\ q``) 375val _ = OK() 376 377val _ = tprint "(Interactive) RENAME_TAC quiet about tyvar guesses(1)" 378val _ = testquiet (Q.RENAME_TAC [���f x /\ _���]) 379 ([], ���(gg : num -> bool) n /\ p���) 380val _ = OK() 381 382val _ = tprint "(Interactive) RENAME_TAC quiet about tyvar guesses(2)" 383val _ = testquiet (Q.RENAME_TAC [���SUC n���]) ([], ���p /\ q���) 384val _ = OK() 385 386val _ = tprint "(Interactive) RENAME_TAC quiet about tyvar guesses(3)" 387val _ = testquiet (Q.RENAME_TAC [���SUC n���]) ([���P (SUC x) ==> Q���], ���p /\ q���) 388val _ = OK() 389 390val _ = tprint "(Interactive) RENAME_TAC quiet about tyvar guesses(4)" 391val _ = testquiet (Q.RENAME_TAC [���SUC n���]) ([���Pr ==> Q���], ���P (SUC x) /\ q���) 392val _ = OK() 393 394 395val _ = Process.exit Process.success; 396