1open HolKernel Parse boolTheory boolLib 2 3val _ = set_trace "Unicode" 0 4 5val tprint = testutils.tprint 6val OK = testutils.OK 7val die = testutils.die 8 9val _ = tprint "Preterm free variables 1" 10val fvs = Preterm.ptfvs (Parse.Preterm`\x. x`) 11val _ = if null fvs then OK() else die "" 12 13val _ = tprint "Preterm free variables 2" 14val fvs = Preterm.ptfvs (Parse.Preterm`\x:bool. x`) 15val _ = if null fvs then OK() else die "" 16 17fun substtest (M, x, N, result) = let 18 open testutils 19in 20 tprint("Testing ["^term_to_string M^"/"^term_to_string x^"] ("^ 21 term_to_string N^") = "^term_to_string result); 22 require (check_result (aconv result)) (Term.subst[x |-> M]) N 23end 24 25val x = mk_var("x", Type.alpha) 26val xfun = mk_var("x", Type.alpha --> Type.alpha) 27val y = mk_var("y", Type.alpha) 28val Id = mk_abs(x,x) 29val Idy = mk_abs(y,y) 30 31(* tests that substitutions work, deferred until this point so that we get 32 access to the parser (which is implicitly a test of the parser too) *) 33 34val tests = [(x,x,y,y), 35 (x,y,y,x), 36 (x,x,x,x), 37 (y,x,Id,Id), 38 (Id,xfun,xfun,Id), 39 (x,y,Id,Idy), 40 (y,x,``\y. y ^x : 'b``, ``\z. z ^y :'b``)] 41 42(* test for the INST_TYPE bug that allows instantiation to cause a 43 free variable to become captured. *) 44val inst_type_test = let 45 val _ = tprint "Testing HOL Light INST_TYPE bug" 46 val ximpnx = prove( 47 ``(x ==> ~x) = ~x``, 48 ASM_CASES_TAC ``x:bool`` THEN ASM_REWRITE_TAC []) 49 val nximpx = prove( 50 ``(~x ==> x) = x``, 51 ASM_CASES_TAC ``x:bool`` THEN ASM_REWRITE_TAC []) 52 val xandnx = prove( 53 ``~(x /\ ~x) /\ ~(~x /\ x)``, 54 ASM_CASES_TAC ``x:bool`` THEN ASM_REWRITE_TAC []) 55 val x_b = mk_var("x", bool) 56 val x_a = mk_var("x", alpha) 57 val P = mk_var("P", alpha --> bool --> bool) 58 val Pxaxb = list_mk_comb(P, [x_a, x_b]) 59 val exxPxaxb = mk_exists(x_b, Pxaxb) 60 val nonempty_t = mk_var("nonempty", (bool --> bool) --> bool) 61 val f = mk_var("f", bool --> bool) 62 val nonempty_rhs = mk_abs(f, mk_exists(x_b, mk_comb(f, x_b))) 63 val nonempty_eqn = mk_eq(nonempty_t, nonempty_rhs) 64 val nonempty_exists = 65 EQT_ELIM (REWRITE_CONV [EXISTS_REFL] 66 (mk_exists(nonempty_t, nonempty_eqn))) 67 val nonempty_th = ASSUME nonempty_eqn 68 val nonempty_Px = ASSUME (mk_comb(nonempty_t, mk_comb(P, x_a))) 69 val exxPxaxb_th = ASSUME exxPxaxb 70 val nonempty_Px_th = RIGHT_BETA (AP_THM nonempty_th (mk_comb(P, x_a))) 71 val Pxx' = rhs (concl nonempty_Px_th) 72 val Pxx'_eq_Pxx = ALPHA Pxx' exxPxaxb 73 val th0 = EQ_MP Pxx'_eq_Pxx (EQ_MP nonempty_Px_th nonempty_Px) 74 val th1 = INST_TYPE [alpha |-> bool] th0 75 val uvneg = ``\u v. v = ~u`` 76 val th2 = INST [inst [alpha |-> bool] P |-> uvneg] th1 77 val uvneg_x = mk_comb(uvneg, x_b) 78 val uvneg_nonempty = 79 EQT_ELIM 80 (CONV_RULE 81 (RAND_CONV (REWRITE_CONV [nonempty_th] THENC BETA_CONV THENC 82 QUANT_CONV BETA_CONV THENC REWRITE_CONV [EXISTS_REFL])) 83 (AP_TERM nonempty_t (BETA_CONV uvneg_x))) 84 val th3 = BETA_RULE (PROVE_HYP uvneg_nonempty th2) 85 val th4 = REWRITE_RULE [EQ_IMP_THM, ximpnx, nximpx, xandnx] th3 86 val final_th = CHOOSE (nonempty_t, nonempty_exists) th4 87in 88 if same_const (concl final_th) (mk_const("F", bool)) then die "" 89 else OK() 90end 91 92(* Test for the experimental kernel's INST_TYPE bug (discovered by Peter 93 Homeier in June 2009). *) 94exception ExitOK 95val _ = let 96 val _ = tprint "Testing for expk INST_TYPE bug" 97 fun x ty = mk_var("x", ty) 98 fun y ty = mk_var("y", ty) 99 val a = alpha 100 val b = beta 101 val t1 = list_mk_abs ([x a,x b], x a) 102 val t1_applied = list_mk_comb(t1, [x a, y b]) 103 val t1_th = RIGHT_LIST_BETA (REFL t1_applied) 104 val t2 = list_mk_abs([x a,x a], x a) 105 val t2_applied = list_mk_comb(t2, [x a, y a]) 106 val t2_th = RIGHT_LIST_BETA (REFL t2_applied) 107 val t1_inst = INST_TYPE [beta |-> alpha] t1_th (* bug *) 108 val bad1 = TRANS (SYM t1_inst) t2_th 109 handle HOL_ERR _ => raise ExitOK 110 val bad2 = INST_TYPE [alpha |-> bool] bad1 111 val Falsity = EQ_MP (INST [x bool |-> T, y bool |-> F] bad2) TRUTH 112in 113 if aconv (concl Falsity) F then die "" else die "Huh???" 114end handle ExitOK => OK() 115 116val _ = Process.atExit (fn () => let 117 fun rm s = FileSys.remove ("scratchTheory." ^ s) 118 handle _ => () 119 in 120 app rm ["sml", "sig", "dat"] 121 end) 122 123fun test f x = f x orelse die "" 124val oldconstants_test = let 125 val _ = tprint "Identity of old constants test" 126 val defn1_t = mk_eq(mk_var("foo", bool), boolSyntax.T) 127 val defn2_t = mk_eq(mk_var("foo", bool), boolSyntax.F) 128 val defn1 = new_definition("foo", defn1_t) 129 val defn2 = new_definition("foo2", defn2_t) 130 val defn3 = new_definition("foo3", defn1_t) 131 val c1 = lhs (concl defn1) 132 val c2 = lhs (concl defn2) 133 val c3 = lhs (concl defn3) 134 val _ = test (fn (c1,c2) => Term.compare(c1, c2) <> EQUAL) (c1, c2) 135 val _ = test (not o uncurry aconv) (c1, c2) 136 val _ = test (not o uncurry aconv) (c1, c3) 137 val _ = test (not o uncurry aconv) (c2, c3) 138 val _ = test (String.isPrefix "old" o #Name o dest_thy_const) c1 139 val _ = test (String.isPrefix "old" o #Name o dest_thy_const) c2 140 val _ = Feedback.emit_MESG := false 141 val _ = Feedback.emit_WARNING := false 142 val _ = new_theory "foo" 143 val defn1 = new_definition("c", mk_eq(mk_var("c", bool), boolSyntax.T)) 144 val _ = new_theory "foo" 145 val defn2 = new_definition("c", mk_eq(mk_var("c", bool), boolSyntax.T)) 146 val c1 = lhs (concl defn1) 147 val c2 = lhs (concl defn2) 148 val _ = test (fn (c1, c2) => Term.compare(c1,c2) <> EQUAL) (c1, c2) 149 val _ = test (not o uncurry aconv) (c1, c2) 150in 151 OK() 152end 153 154val _ = tprint "Testing functional-pretype 1 (pattern)" 155val t = Parse.Term `x <> y ==> x <> y` handle HOL_ERR _ => die "" 156val _ = OK() 157 158val _ = tprint "Testing functional-pretype 2 (simple case)" 159val t = Parse.Term `case x of T => F` handle HOL_ERR _ => die "" 160val _ = OK() 161 162val _ = tprint "Testing functional-pretype 3 (ignored constraint)" 163val quiet_parse = trace ("show_typecheck_errors", 0) Parse.Term 164val _ = case Lib.total quiet_parse `(\x.x) : 'a -> 'b` of 165 NONE => OK() 166 | SOME _ => die "(\\x.x):'a->'b checked" 167 168val _ = tprint "Testing parsing of case expressions with function type" 169val t = Parse.Term `(case T of T => (\x. x) | F => (~)) y` 170val _ = case Lib.total (find_term (same_const boolSyntax.bool_case)) t of 171 NONE => die "" 172 | SOME _ => OK() 173 174val _ = tprint "Testing parsing of case expressions with leading bar" 175val t_opt = SOME (trace ("syntax_error", 0) Parse.Term 176 `case T of | T => F | F => T`) 177 handle HOL_ERR _ => NONE 178val _ = case t_opt of 179 SOME t => 180 if Lib.can (find_term (same_const boolSyntax.bool_case)) t then 181 OK() 182 else die "" 183 | NONE => die "" 184 185val _ = tprint "Testing parsing of _ variables (1)" 186val t = case Lib.total Parse.Term `case b of T => F | _ => T` of 187 NONE => die "" 188 | SOME _ => OK() 189val _ = tprint "Testing parsing of _ variables (2)" 190val t = case Lib.total Parse.Term `case b of T => F | _1 => T` of 191 NONE => die "" 192 | SOME _ => OK() 193val _ = tprint "Testing independence of case branch vars" 194val t = case Lib.total Parse.Term `v (case b of T => F | v => T)` of 195 NONE => die "" 196 | SOME _ => OK() 197 198val _ = tprint "Testing higher-order match 1" 199local 200val thy = current_theory() 201val fmap_ty = let val () = new_type("fmap", 2) in mk_type("fmap", [alpha,beta]) 202 end 203val submap = let 204 val () = new_constant("SUBMAP", fmap_ty --> fmap_ty --> bool) 205in 206 prim_mk_const{Thy = thy, Name = "SUBMAP"} 207end 208val pair_ty = let val () = new_type("prod", 2) in 209 mk_thy_type{Thy = thy, Tyop = "prod", Args = [alpha,beta]} 210 end 211val fmpair_ty = mk_thy_type{Thy = thy, Tyop = "prod", Args = [fmap_ty, gamma]} 212val num_ty = let val () = new_type("num", 0) 213 in mk_thy_type{Thy = thy, Tyop = "num", Args = []} 214 end 215val lt = let val () = new_constant("<", num_ty --> num_ty --> bool) 216 in 217 prim_mk_const{Thy = thy, Name = "<"} 218 end 219val FST = let val () = new_constant("FST", pair_ty --> alpha) 220 in 221 mk_thy_const{Thy = thy, Name = "FST", Ty = fmpair_ty --> fmap_ty} 222 end 223val R = mk_var("R", alpha --> alpha --> bool) 224val f = mk_var("f", num_ty --> alpha) 225val f' = mk_var("f", num_ty --> fmpair_ty) 226val m = mk_var("m", num_ty) 227val n = mk_var("n", num_ty) 228val ant = let 229 val () = new_constant("ant", (alpha --> alpha --> bool) --> 230 (num_ty --> alpha) --> bool) 231in 232 prim_mk_const{Thy = thy, Name = "ant"} 233end 234val th = let 235 val concl = 236 list_mk_forall([m,n], 237 mk_imp(list_mk_comb(lt,[m,n]), 238 list_mk_comb(R,[mk_comb(f,m), mk_comb(f,n)]))) 239in 240 mk_thm([], list_mk_forall([R,f], 241 mk_imp(list_mk_comb(ant, [R,f]), concl))) 242end 243val goal = list_mk_forall([m,n], 244 mk_imp(list_mk_comb(lt, [m,n]), 245 list_mk_comb(submap, 246 [mk_comb(FST, mk_comb(f',m)), 247 mk_comb(FST, mk_comb(f',n))]))) 248val expected = let 249 val ant' = Term.inst [alpha |-> fmap_ty] ant 250 val abs = mk_abs(n, mk_comb(FST, mk_comb(f',n))) 251in 252 list_mk_comb(ant', [submap, abs]) 253end 254in 255val num_ty = num_ty 256val int_ty = let val () = new_type ("int", 0) 257 in 258 mk_thy_type{Thy = thy, Tyop = "int", Args = []} 259 end 260val _ = 261 case Lib.total (VALID (HO_MATCH_MP_TAC th)) ([], goal) of 262 SOME ([([],subgoal)],_) => if aconv subgoal expected then OK() 263 else die "" 264 | _ => die "" 265end (* local *) 266 267val _ = app testutils.convtest [ 268 ("COND_CONV(1)", Conv.COND_CONV, ���if b then (\x:'a. x) else (\y.y)���, 269 ���(\a:'a.a)���) 270]; 271 272val _ = tprint "Testing type-specific Unicode overload 1" 273val _ = set_trace "Unicode" 1 274val _ = overload_on (UnicodeChars.delta, ``$! :(('a -> 'b)->bool)->bool``) 275fun checkparse () = let 276 val tm = Lib.with_flag (Globals.notify_on_tyvar_guess, false) 277 Parse.Term 278 `!x. P x` 279 val randty = type_of (rand tm) 280in 281 if Type.compare(randty, alpha --> bool) <> EQUAL then die "" 282 else OK() 283end 284val _ = checkparse() 285 286(* bounce Unicode trace - and repeat *) 287val _ = tprint "Testing type-specific Unicode overload 2" 288val _ = set_trace "Unicode" 0 289val _ = set_trace "Unicode" 1 290val _ = checkparse () 291 292(* test for type abbreviation bug caused by stale types in a TypeNet.*) 293val _ = tprint "Testing stale type abbreviations bug" 294val _ = new_type ("foo", 1) 295val _ = type_abbrev("bar", ``:bool foo``) 296val _ = new_type ("foo", 0) 297val _ = type_abbrev("baz", ``:foo``) handle _ => die "" 298val _ = OK() 299 300 301(* pretty-printing tests - turn Unicode off *) 302val tpp = let open testutils 303 in 304 unicode_off (raw_backend testutils.tpp) 305 end 306 307fun typp s = let 308 open testutils 309 val ty = Parse.Type [QUOTE s] 310 val _ = tprint ("Testing p/printing of "^s) 311 val res = unicode_off (raw_backend type_to_string) ty 312in 313 if s <> res then die "" else OK() 314end 315 316val _ = app typp [":bool", ":bool -> bool", ":'a -> bool", 317 ":'a -> 'b -> 'c", 318 ":(bool -> bool) -> 'a"] 319local 320 open testutils 321 val ct = current_theory 322 val _ = new_type ("option", 1) 323 val ty = mk_thy_type{Thy = ct(), Tyop = "option", Args = [alpha --> beta]} 324 val _ = tprint ("Testing p/printing of (min_grammar) (('a -> 'b) "^ct()^"$option)") 325 val pfn = 326 PP.pp_to_string 70 (#1 (print_from_grammars min_grammars)) 327 |> raw_backend 328 |> unicode_off 329 val s = pfn ty 330in 331val _ = if s = "('a -> 'b) "^ct()^"$option" then OK() 332 else die s 333end 334 335 336val _ = app tpp ["(if P then q else r) s", 337 "(if P then q else r) s t", 338 "f ((if P then q else r) s t u)", 339 "let x = T in x /\\ y", 340 "let x = (let y = T in y /\\ F) in x \\/ z", 341 "(let x = T in \\y. x /\\ y) p", 342 "let x = p and y = x in x /\\ y", 343 "let x = T ; y = F in x /\\ y", 344 "let x = T ; y = F and z = T in x /\\ y \\/ z", 345 "f ($/\\ p)", 346 "(((p /\\ q) /\\ r) /\\ s) /\\ t", 347 "!x. P (x /\\ y)", 348 "P (!x. Q x)", 349 "\\x. ?y. P x y", 350 "P (\\x. ?y. Q x y)", 351 "(:'a)"] 352 353val _ = tpp "x = y" 354val _ = Lib.with_flag (testutils.linewidth, 10) tpp "xxxxxx =\nyyyyyy" 355 356val _ = add_rule {term_name = "=", 357 fixity = Infix(NONASSOC, 100), 358 block_style = (AroundSamePrec, (PP.CONSISTENT,0)), 359 paren_style = OnlyIfNecessary, 360 pp_elements = [HardSpace 1, TOK "=", BreakSpace(1,2)]} 361val _ = Lib.with_flag (testutils.linewidth, 10) tpp "xxxxxx =\n yyyyyy" 362val _ = Lib.with_flag (testutils.linewidth, 30) tpp 363 "fffff verylongarg1\n\ 364 \ verylongarg2 verylongarg3"; 365val _ = Lib.with_flag (testutils.linewidth, 30) tpp 366 "ffff longarg1\n\ 367 \ (fff longarg2 longarg3\n\ 368 \ longarg4) longarg5\n\ 369 \ longarg6 longarg7"; 370 371val _ = print "** Tests with Unicode on PP.avoid_unicode both on\n" 372val _ = let 373 open testutils 374 fun md f = trace ("Unicode", 1) (trace ("PP.avoid_unicode", 1) f) 375 fun texp (i,out) = md tpp_expected 376 {testf = standard_tpp_message, input = i, output = out} 377 val _ = temp_overload_on ("���", ``T``) 378in 379 app (md tpp) ["!x. p x /\\ q x", "\\x. x", "\\x::p. x /\\ y", 380 "!x::p. q x \\/ r x", "!x. x /\\ T <=> x"]; 381 app texp [("���x. p x", "!x. p x"), ("x ��� y", "x /\\ y"), 382 ("��x. x", "\\x. x")]; 383 temp_clear_overloads_on "���" 384end 385 386val _ = print "** Tests with Unicode on\n" 387val _ = let 388 open testutils 389 fun md f = trace ("Unicode", 1) f 390in 391 app (md tpp) ["����p", "��p"] 392end 393 394 395val _ = print "** Tests with pp_dollar_escapes = 0.\n" 396val _ = set_trace "pp_dollar_escapes" 0 397val _ = app tpp ["(/\\)", "(if)"] 398val _ = set_trace "pp_dollar_escapes" 1 399 400val _ = new_type ("foo", 2) 401val _ = new_constant ("con", ``:'a -> ('a,'b)foo``) 402val _ = set_trace "types" 1 403val _ = print "** Tests with 'types' trace on.\n" 404val _ = tpp "(con (x :'a) :('a, 'b) foo)" 405val _ = tpp "\\(x :'a) (y :'a). x = y" 406val _ = tpp "(ARB (x :'a) :'b)" 407 408(* pretty-printing - tests of colouring *) 409val _ = Parse.current_backend := PPBackEnd.vt100_terminal 410val _ = set_trace "types" 0 411val _ = set_trace "Unicode" 0 412fun tpp (s,expected) = let 413 val t = Parse.Term [QUOTE s] 414 val _ = tprint ("Testing (colour-)printing of `"^s^"`") 415 val res = ppstring pp_term t 416in 417 if res = expected then OK() 418 else die (testutils.clear (" Expected >" ^ expected ^ "<; got >"^res^"<")) 419end 420 421fun bound s = "\^[[0;32m" ^ s ^ "\^[[0m" 422fun free s = "\^[[0;1;34m" ^ s ^ "\^[[0m" 423val concat = String.concat 424 425val bx = bound "x" 426val fy = free "y" 427val fp = free "p" 428val fx = free "x" 429 430val _ = app tpp [ 431 ("\\x. x /\\ y", concat ["\\", bx, ". ", bx, " /\\ ", fy]), 432 ("!x. x /\\ y", concat ["!", bx, ". ", bx, " /\\ ", fy]), 433 ("let x = p in x /\\ y", 434 concat ["let ",bx, " = ", fp, " in ", bx, " /\\ ", fy]), 435 ("let f x = x /\\ p in f x /\\ y", 436 concat ["let ",bound "f", " ", bx, " = ", bx, " /\\ ", fp, " in ", 437 bound "f", " ", fx, " /\\ ", fy]), 438 ("!(x:'a)::p (x:'a). q x", 439 concat ["!",bx,"::",fp, " ", fx,". ",free "q"," ",bx]), 440 ("RES_FORALL (p (x:'a)) (\\x. RES_FORALL (p (x:'a)) (\\y. q x y))", 441 concat ["!(",bx,"::",fp," ",fx,") (",bound "y","::",fp," ",bx,"). ", 442 free "q", " ", bx, " ", bound "y"]) 443] 444 445open testutils 446val condprinter_test = tpp_expected 447 |> Lib.with_flag (linewidth,!Globals.linewidth) 448 |> unicode_off 449 |> raw_backend 450val test = condprinter_test 451val condprinter_tests = 452 [ 453 {input = "if oless e1 e2 /\\ oless x y /\\ foobabbbbbbb\n\ 454 \then p /\\ q /\\ r /\\ ppppp xxxx yyyyy\n\ 455 \else if (e1 = e2) /\\ k1 <> k2\n\ 456 \then T else if (e1 = e2) /\\ (k1 = k2) /\\ oless t1 t2\n\ 457 \then T else F", 458 testf = K ("Large COND 1"), 459 output = "if oless e1 e2 /\\ oless x y /\\ foobabbbbbbb then\n\ 460 \ p /\\ q /\\ r /\\ ppppp xxxx yyyyy\n\ 461 \else if (e1 = e2) /\\ k1 <> k2 then T\n\ 462 \else if (e1 = e2) /\\ (k1 = k2) /\\ oless t1 t2 then T\n\ 463 \else F"}, 464 {input = "if oless e1 e2 /\\ oless x y /\\ foobabb\n\ 465 \then p /\\ q /\\ r /\\ ppppp xxxx\n\ 466 \else if (e1 = e2) /\\ k1 <> k2\n\ 467 \then T else if (e1 = e2) /\\ (k1 = k2) /\\ oless t1 t2\n\ 468 \then T else F", 469 testf = K ("Large COND 2"), 470 output = "if oless e1 e2 /\\ oless x y /\\ foobabb then\ 471 \ p /\\ q /\\ r /\\ ppppp xxxx\n\ 472 \else if (e1 = e2) /\\ k1 <> k2 then T\n\ 473 \else if (e1 = e2) /\\ (k1 = k2) /\\ oless t1 t2 then T\n\ 474 \else F"}, 475 {input = "if really quite a long guard when looked at closely then\n\ 476 \ let quite_a_long_variable_name = another_long_name \\/ x ;\n\ 477 \ another_longish_name = y \\/ z\n\ 478 \ in\n\ 479 \ f x\n\ 480 \else\n\ 481 \ g y", 482 testf = K "Large then-branch", 483 output = "if really quite a long guard when looked at closely then\n\ 484 \ (let\n\ 485 \ quite_a_long_variable_name = another_long_name \\/ x ;\n\ 486 \ another_longish_name = y \\/ z\n\ 487 \ in\n\ 488 \ f x)\n\ 489 \else g y"}, 490 {input = "f\n\ 491 \ (if really quite a long guard when looked at closely then\n\ 492 \ a moderately complicated then_branch\n\ 493 \ else an else_branch)", 494 testf = K "Ladge COND as rand", 495 output = "f\n\ 496 \ (if really quite a long guard when looked at closely then\n\ 497 \ a moderately complicated then_branch\n\ 498 \ else an else_branch)"} 499 ] 500val _ = app condprinter_test condprinter_tests 501 502val _ = let 503 open testutils 504 val _ = tprint (standard_tpp_message "|- p") 505 val res = thm_to_string (ASSUME (mk_var("p", Type.bool))) 506in 507 if res = " [.] |- p" then OK() else die "" 508end 509 510val _ = temp_add_rule { paren_style = NotEvenIfRand, fixity = Prefix 2200, 511 block_style = (AroundEachPhrase, (PP.CONSISTENT,0)), 512 pp_elements = [TOK "/"], term_name = "div" }; 513val _ = test {input = "f /x", 514 testf = (fn s => "Prefix op without parens: "^s), 515 output = "f /x"} 516 517fun bfnprinter gs be sys (ppfns : term_pp_types.ppstream_funs) gravs depth t = 518 let 519 val (bvar, body) = dest_abs t 520 in 521 if aconv bvar body then #add_string ppfns "I" 522 else if aconv body boolSyntax.T then #add_string ppfns "(K T)" 523 else if aconv body boolSyntax.F then #add_string ppfns "(K F)" 524 else if aconv body (mk_neg bvar) then #add_string ppfns "neg" 525 else raise term_pp_types.UserPP_Failed 526 end handle HOL_ERR _ => raise term_pp_types.UserPP_Failed 527 528val _ = temp_add_user_printer("boolfunction", ``v : bool -> bool``, 529 bfnprinter) 530 531val _ = test {input = "\\x:bool. x", 532 testf = (K "Boolean identity with special user printer"), 533 output = "I"} 534val _ = test {input = "\\x:'a. x", 535 testf = (K "Non-boolean identity with special user printer"), 536 output = "\\x. x"} 537val _ = test { 538 input = "\\x:bool. T", 539 testf = (K "Constant T with type :bool -> bool w/special user printer"), 540 output = "(K T)" 541 } 542val _ = test { 543 input = "\\x:'a. T", 544 testf = (K "Constant T with type :'a -> bool w/special user printer"), 545 output = "\\x. T" 546 } 547 548 549 550(* test DiskThms *) 551val _ = let 552 val _ = tprint "Testing DiskThms" 553 val filename = OS.FileSys.tmpName () 554 val _ = DiskThms.write_file filename [("AND_CLAUSES", boolTheory.AND_CLAUSES), 555 ("OR_CLAUSES", boolTheory.OR_CLAUSES)] 556 val readresult = DiskThms.read_file filename 557 val ((nm1,th1), (nm2, th2)) = 558 case readresult of 559 [x,y] => (x,y) 560 | _ => die "" 561in 562 nm1 = "AND_CLAUSES" andalso nm2 = "OR_CLAUSES" andalso 563 aconv (th1 |> concl) (concl boolTheory.AND_CLAUSES) andalso 564 aconv (th2 |> concl) (concl boolTheory.OR_CLAUSES) andalso 565 (OK(); true) orelse 566 die "" 567end 568 569val _ = let 570 val _ = tprint "REWRITE with T (if this appears to hang it has failed)" 571 val t = mk_disj(mk_var("p", bool),T) 572 val (sgs,vfn) = REWRITE_TAC [TRUTH] ([], t) 573in 574 if null sgs andalso aconv (concl (vfn [])) t then OK() 575 else die "" 576end 577 578val _ = let 579 val _ = tprint "EVERY_CONJ_CONV" 580 fun mkb s = mk_var(s, bool) 581 val p = mkb "p" 582 val q = mkb "q" 583 val t = list_mk_conj [T, mk_var("p", bool), mk_var("q",bool)] 584 val I = mk_abs(p, p) 585 val I_thm = SYM (BETA_CONV (mk_comb(I,q))) 586 fun I_CONV t = if aconv t T then ALL_CONV t 587 else REWR_CONV I_thm t 588 val result = EVERY_CONJ_CONV I_CONV t 589 val expected = mk_conj(mk_comb(I, p), mk_comb(I, q)) 590in 591 if aconv (rhs (concl result)) expected then OK() 592 else die "" 593end 594 595val _ = let 596 fun B i = mk_var("x" ^ Int.toString i, bool) 597 fun jump ti i = if i > ti then i - 1 else i 598 fun gentest nm unit lmk c = let 599 val expected = lmk(List.tabulate(3, B)) 600 fun test (ai,ti) = 601 let 602 fun mk i = if i = ai then mk_comb(mk_abs(B 0,B 0), B (jump ti i)) 603 else if i = ti then mk_comb(mk_abs(B 1, B 1), unit) 604 else B (jump ti i) 605 val t = lmk (List.tabulate(4, mk)) 606 val _ = tprint (nm ^ " (" ^ Int.toString ai ^ "," ^ 607 Int.toString ti ^ ")") 608 val res = QCONV (c (TRY_CONV BETA_CONV)) t |> concl |> rhs 609 in 610 if aconv expected res then OK() 611 else die ("got " ^ term_to_string res) 612 end 613 fun row i = List.tabulate (4, fn j => (i,j)) 614 val pairs = List.tabulate (4, row) |> List.concat 615 |> filter (fn (i,j) => i <> j) 616 in 617 List.app test pairs 618 end 619in 620 gentest "EVERY_CONJ_CONV" T list_mk_conj EVERY_CONJ_CONV ; 621 gentest "EVERY_DISJ_CONV" F list_mk_disj EVERY_DISJ_CONV 622end 623 624 625val _ = tprint "Testing (foo THENL [...]) when foo solves" 626val _ = (ACCEPT_TAC TRUTH THENL [ACCEPT_TAC TRUTH]) ([], ``T``) 627 handle HOL_ERR _ => die "" 628val _ = OK() 629 630val _ = tprint "Testing save_thm rejecting names" 631val badnames = ["::", "nil", "true", "false", "ref", "="] 632fun test s = (save_thm(s, TRUTH); die ("Failed to reject: "^s)) 633 handle HOL_ERR _ => () 634val _ = List.app test badnames 635val _ = OK() 636 637val _ = let 638 val _ = tprint "Testing VALIDATE (1)" 639 val th' = Thm.mk_oracle_thm "Testing" ([], ``p' ==> q``) ; 640 val th = Thm.mk_oracle_thm "Testing" ([], ``p ==> q``) ; 641 val uth' = UNDISCH_ALL th' ; 642 val uth = UNDISCH_ALL th ; 643 644 val g = ([], ``p ==> q``) : goal ; 645 val ([g'], _) = STRIP_TAC g ; 646 val ([], _) = (FIRST (map (VALID o ACCEPT_TAC) [uth', uth])) g' ; 647 val ([_], _) = (VALIDATE (FIRST (map ACCEPT_TAC [uth', uth]))) g' ; 648 val true = (VALID (FIRST (map ACCEPT_TAC [uth', uth])) g' ; false) 649 handle HOL_ERR _ => true ; 650in OK() 651end handle _ => die "" 652 653fun goal_equal ((asms1, g1), (asms2, g2)) = 654 ListPair.allEq (fn p => Term.compare p = EQUAL) (asms1,asms2) andalso 655 aconv g1 g2 656 657val _ = let 658 val _ = tprint "Testing VALIDATE (2)" 659 val g = ([], ``(p ==> q) ==> r``) : goal 660 val tac = STRIP_TAC THEN VALIDATE (POP_ASSUM (ASSUME_TAC o UNDISCH)) 661 val (ngs, vf) = VALID tac g 662 663 val tac1 = (VALIDATE (ASSUME_TAC (ASSUME ``x /\ y``))) 664 val tac2 = (SUBGOAL_THEN ``x /\ y`` ASSUME_TAC ) 665 666 val (ngs1, _) = VALID tac1 g 667 val (ngs2, _) = VALID tac2 g 668in 669 if ListPair.allEq goal_equal (ngs1, ngs2) then OK() 670 else die "final equality" 671end handle _ => die "" 672 673val _ = let 674 val _ = tprint "Testing structural list-tactics" 675 val tac = REPEAT DISCH_TAC THEN REPEAT CONJ_TAC THEN_LT 676 EVERY_LT [ (ROTATE_LT 2), 677 (SPLIT_LT 2 (REVERSE_LT, ROTATE_LT 1)), 678 (HEADGOAL (POP_ASSUM ACCEPT_TAC)), 679 (REPEAT_LT (ALLGOALS (POP_ASSUM (fn _ => ALL_TAC)) 680 THEN_LT HEADGOAL (POP_ASSUM ACCEPT_TAC))) ] ; 681 val th = prove (``a ==> b ==> c ==> d ==> a /\ b /\ c /\ d``, tac) ; 682in if hyp th = [] then OK() else die "" 683end handle _ => die "" 684 685val _ = let 686 val _ = tprint "Testing USE_SG_THEN" 687 val tac = REPEAT DISCH_TAC THEN CONJ_TAC THEN_LT USE_SG_THEN ASSUME_TAC 1 2 688 THENL [POP_ASSUM MATCH_MP_TAC THEN CONJ_TAC, DISJ1_TAC] 689 THEN (FIRST_ASSUM ACCEPT_TAC) 690 val th = prove (``p ==> q ==> (p /\ q ==> r) ==> r /\ (r \/ s)``, tac) ; 691in if hyp th = [] then OK() else die "" 692end handle _ => die "" 693 694val _ = let 695 val _ = tprint "Testing USE_SG_THEN and VALIDATE_LT" 696 val tac = CONJ_TAC THEN REPEAT DISCH_TAC 697 THEN_LT EVERY_LT [VALIDATE_LT (USE_SG_THEN ACCEPT_TAC 1 2), 698 NTH_GOAL (REPEAT STRIP_TAC) 1 ] 699 THEN (POP_ASSUM MATCH_MP_TAC) 700 THEN_LT NTH_GOAL CONJ_TAC 2 701 THEN (FIRST_ASSUM ACCEPT_TAC) 702 val g = ``(p ==> q ==> (p /\ q ==> r) ==> r) /\ 703 (p ==> q ==> (p ==> r) ==> r)`` 704 val th = prove (g, tac) ; 705in if hyp th = [] then OK() else die "" 706end handle _ => die "" 707 708val _ = let 709 val _ = tprint "Removing type abbreviation" 710 val _ = temp_type_abbrev ("foo", ``:'a -> bool``) 711 val s1 = type_to_string ``:bool -> bool`` 712 val _ = s1 = ":bool foo" orelse die "" 713 val _ = temp_remove_type_abbrev "foo" 714 val s2 = type_to_string ``:bool -> bool`` 715in 716 if s2 = ":bool -> bool" then OK() else die "" 717end 718 719fun nc (s,ty) = 720 (new_constant(s,ty); prim_mk_const{Name = s, Thy = current_theory()}) 721 722val _ = let 723 val _ = tprint "irule 1 (basic match-mp)" 724 val P = nc("P", alpha --> beta --> bool) 725 val Q = nc("Q", ``:'d -> 'b -> 'c -> bool``) 726 val R = nc("R", beta --> mk_vartype "'e" --> bool) 727 val f = nc("f", ``:'c -> 'e``) 728 val th = mk_thm([], 729 ``!x u. ^P u x ==> !y. ^Q w x y ==> ^R x (^f y)``) 730 val g = ([] : term list, ``^R a (^f b) : bool``) 731 val exsg1 = ``?u. ^P u a`` and exsg2 = ``?w. ^Q w a b`` 732 val (sgs, vf) = irule th g 733 val verdict = 734 case sgs of 735 [([], sg)] => let val (sg1,sg2) = dest_conj sg 736 in 737 aconv sg1 exsg1 andalso aconv sg2 exsg2 738 end 739 | _ => false 740in 741 if verdict then OK() else die "" 742end 743 744val _ = let 745 val _ = tprint "irule 2 (shared existential)" 746 val g = ([]: term list, ``a:'a = b``) 747 val expected = ``?y:'a. (a = y) /\ (y = b)`` 748 val (sgs, vf) = irule EQ_TRANS g 749in 750 case sgs of 751 [([], sg)] => if aconv sg expected then OK() else die "" 752 | _ => die "" 753end 754 755val _ = let 756 val _ = tprint "irule 3 (thm from goal)" 757 val P = nc("P", ``:'a -> bool``) 758 val Q = nc("Q", ``:'a -> bool``) 759 val g = ([``!x. ^P x ==> ^Q x``], ``^Q (b:'a)``) 760 val (sgs, vf) = POP_ASSUM irule g 761 val rth = vf (map mk_thm sgs) 762 val _ = aconv (concl rth) (#2 g) andalso length (hyp rth) = 1 andalso 763 aconv (hd (hyp rth)) (hd (#1 g)) orelse die "" 764in 765 case sgs of 766 [([], sg)] => if aconv sg ``^P (b:'a)`` then OK() 767 else die "" 768 | _ => die "" 769end 770 771val _ = let 772 val _ = tprint "irule 4 (thm from goal, extra vars)" 773 val g = ([``!x:'a y:'a. PP x y ==> QQ y (f y:'a)``], 774 ``(QQ:'a -> 'a -> bool) a (f a)``) 775 val (sgs, vf) = POP_ASSUM irule g 776 val rth = vf (map mk_thm sgs) 777in 778 case sgs of 779 [([], sg)] => if aconv sg ``?x:'a. PP x (a:'a)`` then OK() 780 else die "" 781 | _ => die "" 782end 783 784val _ = hide "P" 785val _ = hide "f" 786val _ = hide "c" 787 788val _ = let 789 open testutils 790 val _ = tprint "irule 5 (as match_accept_tac)" 791 val g = ``(!x:'a. P x) ==> P a`` 792in 793 require (check_result (aconv g o concl)) 794 (fn g => prove(g, DISCH_THEN irule)) 795 g 796end 797 798val _ = let 799 val _ = tprint "irule 6 (JD)" 800 val _ = nc ("IMAGE", ``:('a -> 'b) -> ('a -> bool) -> ('b -> bool)``) 801 val tm = ``P x /\ U u ==> T' w ==> S' u w /\ V v ==> IMAGE f s x`` 802 val thm = mk_thm ([], tm) 803 val g = ``IMAGE a b c`` 804 val (sgs, vf) = irule thm ([], g) 805 val r_thm = vf (map mk_thm sgs) 806in 807 if aconv (concl r_thm) g then OK() else die "" 808end 809 810val _ = let 811 val _ = tprint "irule 7 (JD)" 812 val tm = ``!(f:'a -> 'b) s x u w v. 813 P x /\ U u ==> T' w ==> S' u w /\ V v ==> IMAGE f s x`` 814 val thm = ASSUME tm 815 val g = ``IMAGE (a:'a -> 'b) b c`` 816 val (sgs, vf) = irule thm ([], g) 817 val r_thm = vf (map mk_thm sgs) 818in 819 if aconv (concl r_thm) g then OK() else die "" 820end 821 822val _ = hide "Q" 823val _ = hide "P" 824 825val _ = let 826 open mp_then 827 val _ = tprint "mp_then + goal_assum 1" 828 val asl = [``P (x:'a):bool``, ``R (ARB:'b) (y:'a):bool``] 829 val g = (asl, ``?x:'a y:'b. Q x (f y : 'c) /\ R y x``) 830 val (res, _) = goal_assum (first_assum o mp_then Any mp_tac) g 831 val expected = ``Q (y:'a) (f (ARB:'b) : 'c) : bool`` 832in 833 case res of 834 [(asl',g')] => 835 (case Lib.list_compare Term.compare (asl,asl') of 836 EQUAL => if aconv expected g' then OK() 837 else die ("Got "^term_to_string g'^ 838 "; expected "^term_to_string expected) 839 | _ => die ("Got back changed asm list: " ^ 840 String.concatWith ", " (map term_to_string asl'))) 841 | _ => die ("Tactic returned wrong number of sub-goals ("^ 842 Int.toString (length res)^")") 843end 844 845val _ = hide "f" 846val _ = hide "R" 847 848val _ = let 849 val _ = tprint "drule 1" 850 val asl = [``P (c:ind):bool``, ``!x:ind. P x ==> ?y:'a. Q x y``] 851 val g = (asl, ``?a:ind (b:'a). Q a b``) 852 val (res, _) = first_assum drule g 853 val expectedg = ``(?y:'a. Q (c:ind) y) ==> ?a b. Q a b`` 854in 855 case res of 856 [(asl', g')] => 857 (case Lib.list_compare Term.compare (asl,asl') of 858 EQUAL => if aconv g' expectedg then OK() 859 else die ("Got " ^ term_to_string g'^ 860 "; expected " ^ term_to_string expectedg) 861 | _ => die ("Got back changed asm list: "^ 862 String.concatWith ", " (map term_to_string asl'))) 863 | _ => die ("Tactic returned wrong number of sub-goals (" ^ 864 Int.toString (length res)) 865end; 866 867val _ = let 868 val _ = tprint "drule 2" 869 val _ = new_type("list", 1) 870 val _ = new_constant ("LENGTH", ``:'a list -> num``) 871 val _ = new_constant ("zero", ``:num``) 872 val _ = new_constant ("some_n", ``:num``) 873 val th = mk_thm([], ``!x l:'a list. (<) x (LENGTH l) ==> (<) x some_n``) 874 val asl = [``(<) v (LENGTH (m:ind list))``] 875 val g = (asl, ``?a:ind (b:'a). Q a b``) 876 val (res, _) = drule th g 877 val expectedg = ``(<) v some_n ==> ?a:ind b:'a. Q a b`` 878in 879 case res of 880 [(asl', g')] => 881 (case Lib.list_compare Term.compare (asl,asl') of 882 EQUAL => if aconv g' expectedg then OK() 883 else die ("Got " ^ term_to_string g'^ 884 "; expected " ^ term_to_string expectedg) 885 | _ => die ("Got back changed asm list: "^ 886 String.concatWith ", " (map term_to_string asl'))) 887 | _ => die ("Tactic returned wrong number of sub-goals (" ^ 888 Int.toString (length res)) 889end; 890 891val _ = let 892 val _ = tprint "drule 3" 893 val asl = [``~p ==> q``, ``~p``] 894 val g = (asl, ``r:bool``) 895 val (res, _) = pop_assum drule g 896 val expectedg = ``q ==> r`` 897in 898 case res of 899 [(asl', g')] => 900 (case Lib.list_compare Term.compare ([``~p``], asl') of 901 EQUAL => if aconv g' expectedg then OK() 902 else die ("Got " ^ term_to_string g'^ 903 "; expected " ^ term_to_string expectedg) 904 | _ => die ("Got back changed asm list: "^ 905 String.concatWith ", " (map term_to_string asl'))) 906 | _ => die ("Tactic returned wrong number of sub-goals (" ^ 907 Int.toString (length res)) 908end; 909 910val _ = let 911 open mp_then 912 val _ = tprint "mp_then (concl) 1" 913 val asl = [``p ==> q``, ``~q``] 914 val g = (asl, ``r:bool``) 915 val (res, _) = pop_assum (first_assum o mp_then Concl mp_tac) g 916 val expectedg = ``~p ==> r`` 917in 918 case res of 919 [(asl', g')] => 920 (case Lib.list_compare Term.compare ([``~q``], asl') of 921 EQUAL => if aconv g' expectedg then OK() 922 else die ("Got " ^ term_to_string g'^ 923 "; expected " ^ term_to_string expectedg) 924 | _ => die ("Got back changed asm list: "^ 925 String.concatWith ", " (map term_to_string asl'))) 926 | _ => die ("Tactic returned wrong number of sub-goals (" ^ 927 Int.toString (length res)) 928end; 929 930val _ = let 931 open mp_then 932 val _ = tprint "mp_then (concl) 2" 933 val asl = [``p ==> ~q``, ``q:bool``] 934 val g = (asl, ``r:bool``) 935 val (res, _) = pop_assum (first_assum o mp_then Concl mp_tac) g 936 val expectedg = ``~p ==> r`` 937in 938 case res of 939 [(asl', g')] => 940 (case Lib.list_compare Term.compare ([``q:bool``], asl') of 941 EQUAL => if aconv g' expectedg then OK() 942 else die ("Got " ^ term_to_string g'^ 943 "; expected " ^ term_to_string expectedg) 944 | _ => die ("Got back changed asm list: "^ 945 String.concatWith ", " (map term_to_string asl'))) 946 | _ => die ("Tactic returned wrong number of sub-goals (" ^ 947 Int.toString (length res)) 948end; 949 950 951val _ = let 952 open mp_then 953 val _ = tprint "mp_then (pat) 1" 954 val asl = [``P (x:'a) /\ ~p /\ r ==> ~q``, ``~p:bool``, ``r:bool``] 955 val g = (asl, ``r:bool``) 956 val (res, _) = pop_assum (first_assum o mp_then (Pat `$~`) mp_tac) g 957 val expectedg = ``(P(x:'a) /\ r ==> ~q) ==> r`` 958in 959 case res of 960 [(asl', g')] => 961 (case Lib.list_compare Term.compare ([``~p``, ``r:bool``], asl') of 962 EQUAL => if aconv g' expectedg then OK() 963 else die ("Got " ^ term_to_string g'^ 964 "; expected " ^ term_to_string expectedg) 965 | _ => die ("Got back changed asm list: "^ 966 String.concatWith ", " (map term_to_string asl'))) 967 | _ => die ("Tactic returned wrong number of sub-goals (" ^ 968 Int.toString (length res)) 969end; 970 971 972val _ = let 973 open mp_then 974 val _ = tprint "mp_then (pat) 2" 975 val asl = [``!x. P (x:'a) /\ ~p /\ r ==> ~q``, ``P(c:'a):bool``, ``r:bool``] 976 val g = (asl, ``r:bool``) 977 val (res, _) = 978 pop_assum (first_assum o mp_then (Pat `P (x:'a) : bool`) mp_tac) g 979 val expectedg = ``(~p /\ r ==> ~q) ==> r`` 980in 981 case res of 982 [(asl', g')] => 983 (case Lib.list_compare Term.compare ([���P(c:'a):bool���, ���r:bool���], asl') of 984 EQUAL => if aconv g' expectedg then OK() 985 else die ("Got " ^ term_to_string g'^ 986 "; expected " ^ term_to_string expectedg) 987 | _ => die ("Got back changed asm list: "^ 988 String.concatWith ", " (map term_to_string asl'))) 989 | _ => die ("Tactic returned wrong number of sub-goals (" ^ 990 Int.toString (length res)) 991end; 992 993val _ = let 994 open mp_then 995 val _ = tprint "mp_then (pat) 3" 996 val _ = new_type("list", 1) 997 val _ = new_type("ti", 0) 998 val _ = hide "foo" 999 val _ = new_constant("EVERY", ``:('a -> bool) -> 'a list -> bool``) 1000 val asl = [``EVERY (x:'a -> bool) ls``, 1001 ``!x:ti y. foo x y /\ EVERY y (ls:'a list) ==> gg x``, 1002 ``foo (a:ti) (x:'a -> bool):bool``, ``bar (x:'a -> bool):bool``] 1003 val g = (List.rev asl, ``gg (a:ti):bool``) 1004 val (res, _) = 1005 first_x_assum (first_assum o mp_then (Pat `EVERY`) mp_tac) g 1006 val expectedg = ``(!x':ti. foo x' (x:'a -> bool) ==> gg x') ==> gg a`` 1007 val expectedasl = [``bar (x:'a -> bool):bool``, 1008 ``foo (a:ti) (x:'a -> bool):bool``, 1009 ``EVERY (x:'a -> bool) ls``] 1010in 1011 case res of 1012 [(asl', g')] => 1013 (case Lib.list_compare Term.compare (expectedasl, asl') of 1014 EQUAL => if aconv g' expectedg then OK() 1015 else die ("Got " ^ term_to_string g'^ 1016 "; expected " ^ term_to_string expectedg) 1017 | _ => die ("Got back changed asm list: "^ 1018 String.concatWith ", " (map term_to_string asl'))) 1019 | _ => die ("Tactic returned wrong number of sub-goals (" ^ 1020 Int.toString (length res)) 1021end; 1022 1023val _ = let 1024 open mp_then Portable 1025 val _ = tprint "mp_then (backtracking pat)" 1026 val gh567_1_def = new_definition("gh567_1_def", ���gh567_1 p <=> p /\ F���) 1027 val gh567_2_def = new_definition("gh567_2_def", ���gh567_2 p <=> p /\ T���) 1028 val _ = temp_overload_on ("gh567", ���gh567_1���) 1029 val _ = temp_overload_on ("gh567", ���gh567_2���) 1030 val tm1 = gh567_1_def |> SPEC_ALL |> concl |> lhs |> rator 1031 val asl = [���!b. ^tm1 b ==> b���, ���^tm1 F���] 1032 val g = boolSyntax.F 1033 val tac = first_x_assum (first_x_assum o mp_then (Pat ���gh567���) assume_tac) 1034in 1035 case verdict tac (fn _ => ()) (asl,g) of 1036 FAIL ((), e) => die ("Got exception: " ^ General.exnMessage e) 1037 | PASS (sgs, _) => 1038 if list_eq (pair_eq (list_eq aconv) aconv) sgs [([F], F)] then 1039 OK() 1040 else die ("Wrong subgoals") 1041end 1042 1043 1044val _ = let 1045 val _ = tprint "drule_all 1" 1046 val asl = [``!x:ind. P x /\ R x ==> ?y:'a. Q x y``, 1047 ``P (c:ind):bool``, ``R (d:ind):bool``, 1048 ``P (d:ind):bool``] 1049 val g = (asl, ``?a:ind (b:'a). Q a b``) 1050 val (res, _) = first_assum drule_all g 1051 val expectedg = ``(?y:'a. Q (d:ind) y) ==> ?a b. Q a b`` 1052in 1053 case res of 1054 [(asl', g')] => 1055 (case Lib.list_compare Term.compare (asl,asl') of 1056 EQUAL => if aconv g' expectedg then OK() 1057 else die ("Got " ^ term_to_string g'^ 1058 "; expected " ^ term_to_string expectedg) 1059 | _ => die ("Got back changed asm list: "^ 1060 String.concatWith ", " (map term_to_string asl'))) 1061 | _ => die ("Tactic returned wrong number of sub-goals (" ^ 1062 Int.toString (length res)) 1063end; 1064 1065val _ = let 1066 val _ = tprint "dxrule_all 1" 1067 val imp = ``!x:ind. P x /\ R x ==> ?y:'a. Q x y`` 1068 val asl = [imp, ``P (c:ind):bool``, ``R (d:ind):bool``, ``P (d:ind):bool``] 1069 val g = (asl, ``?a:ind (b:'a). Q a b``) 1070 val (res, _) = first_assum dxrule_all g 1071 val expectedg = ``(?y:'a. Q (d:ind) y) ==> ?a b. Q a b`` 1072 val expected_asl = [imp, ``P (c:ind):bool``] 1073in 1074 case res of 1075 [(asl', g')] => 1076 (case Lib.list_compare Term.compare (expected_asl,asl') of 1077 EQUAL => if aconv g' expectedg then OK() 1078 else die ("Got " ^ term_to_string g'^ 1079 "; expected " ^ term_to_string expectedg) 1080 | _ => die ("Got back wrong asm list: "^ 1081 String.concatWith ", " (map term_to_string asl'))) 1082 | _ => die ("Tactic returned wrong number of sub-goals (" ^ 1083 Int.toString (length res)) 1084end; 1085 1086 1087fun dolvtests(modname,empty,insert,match) = let 1088 val n = List.foldl (fn ((k,v),acc) => insert (acc,k,v)) empty 1089 [(([],``R x y:bool``), 1), 1090 (([], ``!s:'a. f s = T``), 2), 1091 (([``f:'a -> bool``], ``!s:'a. f s = T``), 3), 1092 (([``f:'a -> bool``], ``f (s:'a) = T``), 4) 1093 ] 1094 fun test (nm, pat, expected) = 1095 let 1096 open testutils 1097 val _ = tprint (modname ^ ": " ^ nm) 1098 in 1099 require (check_result (equal expected)) 1100 (fn pat => List.map snd (match (n,pat))) 1101 pat 1102 end 1103in 1104 List.app test [("exact", ``f x y : bool``, [1]), 1105 ("one extra", ``f a x y : bool``, [1]), 1106 ("lvar 1", ``g (z:'a) = T``, [1]), 1107 ("lvar 2", ``f (z:'a) = T``, [4,1]), 1108 ("quant eq 1", ``!z:'a. g z = T``, [2]), 1109 ("quant lv match", ``!z:'a. f z = T``, [3,2]) 1110 ] 1111end 1112 1113val _ = dolvtests("LVTermNet", LVTermNet.empty, LVTermNet.insert, 1114 LVTermNet.match) 1115val _ = dolvtests("LVTermNetFunctor", 1116 LVTermNetFunctorApplied.PrintMap.empty, 1117 LVTermNetFunctorApplied.PrintMap.insert, 1118 LVTermNetFunctorApplied.PrintMap.match) 1119 1120(* set up overloading situation with < and + overloaded to num and int *) 1121val thy = current_theory() 1122val ilt = (new_constant("ilt", int_ty --> (int_ty --> bool)); 1123 mk_thy_const{Thy = thy, Name = "ilt", 1124 Ty = int_ty --> (int_ty --> bool)}) 1125val _ = overload_on("<", ilt) 1126 1127val _ = set_fixity "+" (Infixl 500) 1128val _ = set_fixity "<" (Infix(NONASSOC, 450)) 1129 1130val nplus = (new_constant("nplus", num_ty --> (num_ty --> num_ty)); 1131 mk_thy_const{Thy = thy, Name = "nplus", 1132 Ty = num_ty --> (num_ty --> num_ty)}) 1133val _ = overload_on("+", nplus) 1134 1135val iplus = (new_constant("iplus", int_ty --> (int_ty --> int_ty)); 1136 mk_thy_const{Thy = thy, Name = "iplus", 1137 Ty = int_ty --> (int_ty --> int_ty)}) 1138val _ = overload_on("+", iplus) 1139 1140val _ = tprint "Checking error message on x + y < T parse (w/ints around)" 1141val ptie = TermParse.preterm (term_grammar()) (type_grammar()) `x + y < T` 1142val res = let 1143 open errormonad Preterm 1144 infix >- >> 1145 val checked = 1146 ptie >- (fn pt => typecheck_phase1 NONE pt >> overloading_resolution pt) 1147in 1148 case checked Pretype.Env.empty of 1149 Error (OvlNoType(s,_), _) => if s = "<" orelse s = "+" then OK() 1150 else die "" 1151 | _ => die "" 1152end 1153 1154val _ = List.app substtest tests 1155 1156val _ = print "Testing cond-printer after set_grammar_ancestry\n" 1157val _ = set_trace "PP.avoid_unicode" 1 1158val _ = set_grammar_ancestry ["bool"] 1159val _ = app condprinter_test condprinter_tests 1160 1161val _ = let 1162 open Exn 1163 fun badtac (asl,g) = ([], fn [] => ASSUME ``p:bool`` | _ => raise Fail "") 1164 val vtac = VALID badtac 1165 fun checkmsg P f (os, ofn, m) = os = "Tactical" andalso ofn = f andalso P m 1166 fun checkv P = checkmsg P "VALID" 1167 fun checkvl P = checkmsg P "VALID_LT" 1168 val _ = tprint "VALID-checking (normal)" 1169 val _ = require is_result vtac ([``p:bool``], ``p:bool``) 1170 val _ = tprint "VALID-checking (bad concl)" 1171 val expectedmsg1 = "Invalid tactic: theorem has wrong conclusion p" 1172 val _ = require (check_HOL_ERR (checkv (equal expectedmsg1))) vtac 1173 ([``p:bool``, ``q:bool``], ``P:bool``) 1174 val _ = tprint "VALID-checking (bad hyp)" 1175 val expectedmsg2 = "Invalid tactic: theorem has bad hypothesis p" 1176 val _ = require (check_HOL_ERR (checkv (equal expectedmsg2))) vtac 1177 ([], ``p:bool``) 1178in 1179 () 1180end 1181