1open HolKernel Parse boolTheory boolLib pairTheory 2open quantHeuristicsLib simpLib boolSimps 3 4(* For manual 5 6val hard_fail = false; 7val quiet = false; 8val _ = Parse.current_backend := PPBackEnd.emacs_terminal; 9 10*) 11 12val _ = Parse.current_backend := PPBackEnd.vt100_terminal; 13 14fun test_conv s conv do_stop quiet (t, r_opt) = 15let 16 open PPBackEnd Parse 17 val lq = UnicodeChars.ldquo 18 val _ = print (if quiet then lq else "Testing "^s^" "^lq); 19 val _ = print_term t; 20 val _ = print (UnicodeChars.rdquo ^ "\n "); 21 val ct = Timer.startCPUTimer(); 22 val thm_opt = SOME (conv t) handle Interrupt => raise Interrupt 23 | _ => NONE; 24 25 val ok = if not (isSome r_opt) then not (isSome thm_opt) else 26 isSome thm_opt andalso 27 let 28 val thm_t = concl (valOf thm_opt); 29 in 30 is_eq thm_t andalso (Term.term_eq (lhs thm_t) t) andalso (aconv (rhs thm_t) (valOf r_opt)) 31 end 32 val quiet = quiet andalso ok 33 val _ = if ok then 34 print_with_style [FG Green] "OK " 35 else 36 (print_with_style [FG OrangeRed] "FAILED ") 37 38 val d_time = #usr (Timer.checkCPUTimer ct); 39 val _ = print ((Time.toString d_time)^ " s"); 40 val _ = if quiet then () else print ("\n "); 41 42 val _ = if quiet then () else 43 let 44 val _ = print "---> "; 45 val _ = if isSome thm_opt then (print_thm (valOf thm_opt);print "\n") 46 else print "-\n" 47 val _ = if (not ok) then 48 (print " EXPECTED "; 49 if isSome r_opt then (print "``";print_term (valOf r_opt);print "``\n") 50 else print "-\n") 51 else () 52 in () end 53 val _ = print "\n"; 54 val _ = if (not ok andalso do_stop) then Process.exit Process.failure else (); 55in 56 () 57end; 58 59val hard_fail = false; 60val hard_fail = true; 61val quiet = false; 62 63(******************************************************************************) 64(* General tests *) 65(******************************************************************************) 66 67 68local 69 val x = mk_var ("x", numLib.num); 70 fun mk_eq_n n = 71 mk_eq (x, numSyntax.term_of_int n) 72 73 fun mk_eq_disj n = 74 if (n = 1) then mk_eq_n 1 else 75 mk_disj (mk_eq_n n, mk_eq_disj (n-1)) 76 77in 78 fun mk_eq_disj_ex n = mk_exists (x, mk_eq_disj n) 79end 80 81local 82 val x = mk_var ("x", numLib.num); 83 fun mk_eq_n n = 84 mk_eq (x, numSyntax.term_of_int n) 85 86 fun mk_eq_disj m n = 87 if (n = 1) then mk_eq_n m else 88 let 89 val n2 = n div 2 90 val n3 = n - n2; 91 in 92 mk_disj (mk_eq_disj m n2, mk_eq_disj (m+n2) n3) 93 end; 94 95in 96 fun mk_eq_disj_ex2 n = mk_exists (x, mk_eq_disj 0 n) 97end 98 99 100val qh_testCases = 101 [(``?x. x = 2``, SOME ``T``), 102 (``?x. f x = f 2``, SOME ``T``), 103 (``?x. f x = 2``, NONE), 104 (``?x. P x /\ (x = 2)``, SOME ``(P 2):bool``), 105 (``?x. ~~(P x /\ (x = 2))``, SOME ``(P 2):bool``), 106 (``?x. P1 x /\ (x = 2) /\ P2 x /\ P3 x /\ P4 x``, SOME ``P1 2 /\ P2 2 /\ P3 2 /\ P4 2``), 107 (``?x. P /\ (x = 2)``, SOME ``P:bool``), 108 (``?x1 x2. P1 x2 ==> ((x1 = 2) /\ P2(x1, x2))``, SOME ``?x2. P1 x2 ==> (P2(2, x2))``), 109 (``?x. P x \/ (x = 2)``, SOME T), 110 (``?x. (x = 2) \/ Q x``, SOME T), 111 (``?x. (f x = f 2) /\ Q``, SOME ``Q:bool``), 112 (``!x. x = 2``, NONE), 113 (``!x. (x = 2) ==> P x``, SOME ``(P 2):bool``), 114 (``!x. (Q x /\ (x = 2)) ==> P x``, SOME ``Q 2 ==> P 2``), 115 (``?x:'a. (?y:'b. (x = f y)) /\ P x``, SOME ``?y:'b. P ((f y):'a)``), 116 (``?x. ~(Q3 x \/ Q x \/ Q2 x \/ ~(x = 2))``, SOME ``~(Q3 2 \/ Q 2 \/ Q2 2)``), 117 (``?x:'a. (!y:'b. (x = f y)) /\ P x``, SOME ``?y:'b. (!y'. f y = f y') /\ P ((f y):'a)``), 118 (``?x:'a. (!y2:'b y:'b y3:'b. (x = f y y2 y3)) /\ P x``, SOME ``?y2:'b y:'b y3:'b. (!y2' y' y3'. f y y2 y3 = f y' y2' y3') /\ P ((f y y2 y3):'a)``), 119 (``?x:'a. Q x /\ (?y:'b. (x = f y)) /\ P x``, SOME ``?y:'b. Q (f y) /\ P ((f y):'a)``), 120 (``?x. if b x then ((x = 2) /\ Q x) else (Q2 x /\ (x = 2))``, 121 SOME ``if b 2 then (Q 2):bool else Q2 2``), 122 (``?!x. (x = 2) /\ P x``, SOME ``(P 2):bool``), 123 (mk_eq_disj_ex 40, SOME T)]; 124 125val qh_test = test_conv "QUANT_INSTANTIATE_CONV []" (QUANT_INSTANTIATE_CONV []) 126val _ = map (qh_test hard_fail quiet) qh_testCases; 127 128 129(******************************************************************************) 130(* QUANT_CONV tests *) 131(******************************************************************************) 132 133val _ = test_conv "INST_QUANT_CONV [(\"x\", `2:num`, [])]" (INST_QUANT_CONV [("x", `2:num`, [])]) hard_fail quiet 134 (``!z. !x. (x = 2:num) ==> P(x, z)``, SOME ``!z. P(2, z)``) 135 136val _ = test_conv "INST_QUANT_CONV [(\"x\", `2:num`, [])]" (INST_QUANT_CONV [("x", `2:num`, [])]) hard_fail quiet 137 (``!z. ?x. (x = 2:num) /\ P(x, z)``, SOME ``!z. P(2, z)``) 138 139val _ = test_conv "INST_QUANT_CONV [(\"x\", `3:num`, [])]" (INST_QUANT_CONV [("x", `3:num`, [])]) hard_fail quiet 140 (``!z. ?x. (x = 2:num) /\ P(x, z)``, NONE) 141 142(* 143QUANT_INSTANTIATE_CONV [] ``?x. if b x then ((x = 2) /\ Q x) else (Q2 x /\ (x = 2))`` 144 145exceptionLocation UNCHANGED 146 (fn () => 147(QUANT_INSTANTIATE_CONV [] ``?x. if b x then ((x = 2) /\ Q x) else (Q2 x /\ (x = 2))``; NONE) 148handle exn => exceptionLocation exn 149 150open PolyML 151PolyML.stackTrace() 152PolyML.Compiler.debug := true 153 154 155free_in ``y:num`` (mk_eq_disj_ex 4000) 156val conv = (QUANT_INSTANTIATE_CONV []) 157 158val (v,t) = dest_forall ``!x. ~~(x = 2) ==> P x`` 159val t = mk_neg t 160 161QUANT_INSTANTIATE_CONV [] ``?x. ~~(x = 2)`` 162QUANT_INSTANTIATE_CONV [] ``?x. if b x then ((x = 2) /\ Q x) else (Q2 x /\ (x = 2))`` 163 164open PolyML 165stackTrace () 166PolyML.debug = 1 167time conv t 168PolyML.profiling 2 169val t = (mk_eq_disj_ex 40) 170val t = (mk_eq_disj_ex2 40) 171val (v,t) = dest_exists ``?x. if b x then ((x = 2) /\ Q x) else (Q2 x /\ (x = 2))`` 172 173 174QUANT_INSTANTIATE_HEURISTIC___debug := 3; 175 176conv ``?y:num. (z = 40)`` 177t 178 179time (QUANT_INSTANTIATE_CONV []) ``?x. 180quantHeuristicsArgsLib 181QUANT_INSTANTIATE_HEURISTIC___debug := 0 182 183((x = 8) \/ (x = 7) \/ (x = 6) \/ (x = 1) \/ (x = 2) \/ (x = 3) \/ (x = 4) \/ (x = 5))`` 184*) 185 186(******************************************************************************) 187(* Pair tests *) 188(******************************************************************************) 189 190val qh_test_pair = test_conv "QUANT_INSTANTIATE_CONV [pair_default_qp]" (QUANT_INSTANTIATE_CONV [pair_default_qp]) 191 192val qh_testCases_pair = 193 [(``?p:('a # 'b). (x = FST p) /\ Q p``, SOME ``?p_2:'b. Q(x:'a,p_2)``), 194 (``?p:('a # 'b). (x = SND p) /\ Q p``, SOME ``?p_1:'a. Q(p_1,x:'b)``), 195 (``?v:'a. (v,X:'b) = Z``, SOME ``X = SND (Z:('a # 'b))``), 196 (``!x. a /\ (\ (a1:'a, t3:'b, a2:'c). P a1 a2 t3) x /\ b x``, 197 SOME ``!a1:'a t3:'b a2:'c. a /\ (\ (a1:'a, t3:'b, a2:'c). P a1 a2 t3) (a1,t3,a2) /\ b (a1,t3,a2)``), 198 (``?v:'a. (v,X:'b) = (a,b)``, SOME ``X:'b = b``)]; 199 200val _ = map (qh_test_pair hard_fail quiet) qh_testCases_pair; 201 202 203 204(******************************************************************************) 205(* Option tests *) 206(******************************************************************************) 207 208val qh_test_option = test_conv "QUANT_INSTANTIATE_CONV [option_qp]" (QUANT_INSTANTIATE_CONV [option_qp]) 209 210val qh_testCases_option = 211 [(``!x:'a option. IS_SOME x ==> P x``, SOME ``!x_x':'a. P (SOME x_x')``), 212 (``?x:'a option. IS_SOME x ==> P x``, SOME T), 213 (``!x:'a option. ~(IS_SOME x) ==> P x``, SOME ``(P (NONE:'a option)):bool``), 214 (``?x. IS_SOME x``, SOME T), 215 (``!x. IS_SOME x``, SOME F), 216 (``?x. IS_NONE x``, SOME T), 217 (``!x. IS_NONE x``, SOME F)]; 218 219val _ = map (qh_test_option hard_fail quiet) qh_testCases_option; 220 221 222(******************************************************************************) 223(* Num tests *) 224(******************************************************************************) 225 226val qh_test_num = test_conv "QUANT_INSTANTIATE_CONV [num_qp]" (QUANT_INSTANTIATE_CONV [num_qp]) 227 228val qh_testCases_num = 229 [(``!x:num. (x + 7 = 2 + 7)``, SOME F), 230 (``!x:num. ~(x = 0) ==> P x``, SOME ``!x_n. P (SUC x_n)``), 231 (``!x:num. x = y``, SOME F), 232 (``!x:num. y = x``, SOME F)]; 233 234val _ = map (qh_test_num hard_fail quiet) qh_testCases_num; 235 236 237(******************************************************************************) 238(* LIST tests *) 239(******************************************************************************) 240 241val qh_test_list = test_conv "QUANT_INSTANTIATE_CONV [list_qp]" (QUANT_INSTANTIATE_CONV [list_qp]) 242 243val qh_testCases_list = 244 [(``!l:'a list. ~(NULL l) ==> P l``, SOME ``!l_h l_t. P (l_h::l_t)``), 245 (``!x. x = y::ys``, SOME F), 246 (``!x. x = []``, SOME F), 247 (``?l. ~(NULL l)``, SOME T), 248 (``?x:'a xs. QQ /\ (x::xs = y::ys) /\ P /\ Q xs``, SOME ``QQ /\ P /\ Q (ys:'a list)``), 249 (``?x. PP ==> ~(x = []) /\ P x``, 250 SOME ``?x_h x_t:'a list. PP ==> P (x_h::x_t)``)]; 251val _ = map (qh_test_list hard_fail quiet) qh_testCases_list; 252 253 254(******************************************************************************) 255(* Option tests *) 256(******************************************************************************) 257 258val qh_test_option = test_conv "QUANT_INSTANTIATE_CONV [option_qp]" (QUANT_INSTANTIATE_CONV [option_qp]) 259 260val qh_testCases_option = 261 [(``!x:'a option. IS_SOME x ==> P x``, SOME ``!x_x':'a. P (SOME x_x')``), 262 (``?x:'a option. IS_SOME x ==> P x``, SOME T), 263 (``!x:'a option. ~(IS_SOME x) ==> P x``, SOME ``(P (NONE:'a option)):bool``), 264 (``?x. IS_SOME x``, SOME T), 265 (``!x. IS_SOME x``, SOME F), 266 (``?x. IS_NONE x``, SOME T), 267 (``!x. IS_NONE x``, SOME F)]; 268 269val _ = map (qh_test_option hard_fail quiet) qh_testCases_option; 270 271(******************************************************************************) 272(* SUM tests *) 273(******************************************************************************) 274 275val qh_test_sum = test_conv "QUANT_INSTANTIATE_CONV [sum_qp]" (QUANT_INSTANTIATE_CONV [sum_qp]) 276 277val qh_testCases_sum = 278 [(``!x:'a + 'b. ISL x ==> P x``, SOME ``!l. P ((INL l):('a + 'b))``), 279 (``!x:'a + 'b. ISR x ==> P x``, SOME ``!r. P ((INR r):('a + 'b))``), 280 (``?x:'a + 'b. ISL x ==> P x``, SOME T), 281 (``?x:'a + 'b. ISR x ==> P x``, SOME T), 282 (``!x:'a + 'b. ~(ISR x) ==> P x``, SOME ``!l. (P ((INL l):('a + 'b)))``), 283 (``!x:'a + 'b. ~(ISL x) ==> P x``, SOME ``!r. (P ((INR r):('a + 'b)))``), 284 (``!p_1 p_2. x <> OUTR p_2 \/ ISL p_2 \/ P p_1 p_2``, SOME ``!p_1. P p_1 (INR x)``), 285 (``?x. ISL x``, SOME T), 286 (``!x. ISL x``, SOME F), 287 (``?x. ISR x``, SOME T), 288 (``!x. ISR x``, SOME F)]; 289 290val _ = map (qh_test_sum hard_fail quiet) qh_testCases_sum; 291 292(******************************************************************************) 293(* Context tests *) 294(******************************************************************************) 295 296val qh_test_direct_context = test_conv "SIMP_CONV (bool_ss++QUANT_INST_ss[direct_context_qp]) []" (SIMP_CONV (bool_ss++QUANT_INST_ss[direct_context_qp]) []) 297 298val qh_testCases_direct_context = 299 [(``(P x) ==> !x. ~(P x) /\ Q x``, SOME ``~(P x)``), 300 (``~(P x) ==> !x. P x /\ Q x``, SOME ``(P (x:'a)):bool``), 301 (``P x ==> ?x. Q x \/ P x``, SOME ``T``) 302] 303 304 305val qh_test_context = test_conv "SIMP_CONV (bool_ss++QUANT_INST_ss[context_qp]) []" (SIMP_CONV (bool_ss++QUANT_INST_ss[context_qp]) []) 306val qh_testCases_context = 307 [(``(!x. P x ==> (x = 2)) ==> (!x. P x ==> Q x)``, SOME ``(!x. P x ==> (x = 2)) ==> P 2 ==> Q 2``), 308 (``(!x. Q x ==> P x) /\ Q 2 ==> (?x. P x)``, SOME T) 309] 310 311val _ = map (qh_test_context hard_fail quiet) qh_testCases_context; 312 313 314val qh_test_context2 = test_conv "SIMP_CONV (bool_ss++QUANT_INST_ss[std_qp]) []" (SIMP_CONV (bool_ss++QUANT_INST_ss[std_qp]) []) 315 316val qh_testCases_context2 = 317 [(``(~(P [])) ==> (!x. P x ==> Q x)``, SOME ``��P [] ��� ���x_h x_t. P (x_h::x_t) ��� Q (x_h::x_t)``), 318 (``(!x. P x ==> ~(x = [])) ==> (!x. P x ==> Q x)``, SOME ``��P [] ��� ���x_h x_t. P (x_h::x_t) ��� Q (x_h::x_t)``), 319 (``(!x. P x ==> ISR x) ==> (!x. P x ==> Q x)``, SOME ``(!l. ~((P:('a + 'b)-> bool) (INL l))) ==> (!r. P (INR r) ==> (Q:('a + 'b)-> bool) (INR r))``), 320 (``(!x. P x ==> ISL x) ==> (!x. P x ==> Q x)``, SOME ``(!r. ~((P:('a + 'b)-> bool) (INR r))) ==> (!l. P (INL l) ==> (Q:('a + 'b)-> bool) (INL l))``)] 321 322val _ = map (qh_test_context2 hard_fail quiet) qh_testCases_context2; 323 324 325(******************************************************************************) 326(* simple tests *) 327(******************************************************************************) 328 329val qh_test_simple = test_conv "SIMPLE_QUANT_INSTANTIATE_CONV" SIMPLE_QUANT_INSTANTIATE_CONV 330 331val qh_testCases_simple = 332 [(``!x. (P x /\ (x = 5) /\ Q x) ==> Z x``, SOME ``(P 5 /\ (5 = 5) /\ Q 5) ==> Z 5``), 333 334 (``?x. (P x /\ (x = 5) /\ Q x)``, SOME ``(P 5 /\ (5 = 5) /\ Q 5)``), 335 336 (``!x. (P x \/ ~(x = 5) \/ Q x)``, SOME ``(P 5 \/ ~(5 = 5) \/ Q 5)``), 337 338 (``?x. (P x /\ x)``, SOME ``P T /\ T``), 339 (``!x. (P x \/ ~x)``, SOME ``P T \/ ~T``), 340 341 (``?x. (x = 5)``, SOME ``5 = 5``), 342 (``!x. ~(5 = x)``, SOME ``~(5 = 5)``), 343 344 (``?!x. (P x /\ (x = 5) /\ Q x)``, SOME ``(P 5 /\ (5 = 5) /\ Q 5)``), 345 346 (``some x. (P x /\ (x = 5) /\ Q x)``, SOME ``if (P 5 /\ (5 = 5) /\ Q 5) then SOME 5 else NONE``), 347 348 (``@x. (P x /\ (x = 5) /\ Q x)``, SOME ``if (P 5 /\ (5 = 5) /\ Q 5) then 5 else @x. F``), 349 350 351 (``!x y z. (P x \/ ~(x = f y z) \/ Q x)``, SOME ``!y:'b z:'c. (P (f y z) \/ ~(f y z = f y z) \/ Q (f y z))``), 352 353 354 (``?x. (P x /\ (5 = x) /\ Q x)``, SOME ``(P 5 /\ (5 = 5) /\ Q 5)``), 355 (``?x. (P x /\ (!z:'a. (5 = x) /\ Q x z))``, SOME ``(P 5 /\ (!z:'a. (5 = 5) /\ Q 5 z))``), 356 (``?x. (P x /\ (?z:'a. (5 = x) /\ Q x z))``, SOME ``(P 5 /\ (?z:'a. (5 = 5) /\ Q 5 z))``), 357 358 (``!x. ~(P x /\ (5 = x) /\ Q x)``, SOME ``~(P 5 /\ (5 = 5) /\ Q 5)``), 359 (``!x. ~(P x /\ (!z:'a. (5 = x) /\ Q x z))``, SOME ``~(P 5 /\ (!z:'a. (5 = 5) /\ Q 5 z))``), 360 (``!x. ~(P x /\ (?z:'a. (5 = x) /\ Q x z))``, SOME ``~(P 5 /\ (?z:'a. (5 = 5) /\ Q 5 z))``), 361 362 (``?x. (x, y) = (X:('a # 'b))``, SOME ``(FST X, y) = (X:('a # 'b))``), 363 (``?x. ((y, x) = (X:('a # 'b)))``, SOME ``(y, SND X) = (X:('a # 'b))``), 364 (``?x. ((3, (y:'a, x:'b), z:'c)) = X``, SOME ``((3,(y:'a,SND (FST (SND X))),z:'c) = X)``), 365 (``?x. (3::4::l = y::x::l')``, SOME ``(3::4::l = y::4::l')``), 366 (``?l'. (3::4::l = y::x::l')``, SOME ``(3::4::l = y::x::l)``), 367 (``?y. (3::4::l = y::x::l')``, SOME ``(3::4::l = 3::x::l')``), 368 (``?x. (SOME x = f)``, SOME ``(SOME (THE f) = f)``) 369] 370 371 372val _ = map (qh_test_simple hard_fail quiet) qh_testCases_simple; 373 374 375val _ = Process.exit Process.success; 376