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