1open HolKernel Parse boolLib bossLib 2open testutils 3 4val _ = print "\n" 5 6fun listprint pr xs = 7 "[" ^ String.concatWith "," (map pr xs) ^ "]" 8 9 10fun test_CONV (c,nm) (t, expected) = let 11 val _ = tprint (nm^" on `"^term_to_string t^"`") 12 val th = Conv.QCONV c t 13in 14 if aconv (rhs (concl th)) expected then OK() 15 else die "FAILED!\n" 16end handle HOL_ERR _ => die "FAILED (not even an eqn)!" 17 18val _ = set_trace "Unicode" 0 19 20val _ = app (test_CONV (EVAL,"EVAL")) [ 21 (``option_CASE (NONE : 'a option) (n:'b) f``, ``n:'b``), 22 (``option_CASE (SOME (x:'a)) (n:'b) f``, ``f (x:'a):'b``), 23 (``list_CASE ((h::t) : 'a list) (n:'b) f``, 24 ``f (h:'a) (t:'a list):'b``), 25 (``sum_CASE (INL 3) (\n. n) f``, ``3``), 26 (``INL (x:'a) = INR (y:'b)``, ``F``), 27 (``INL (x:'a) = INL x'``, ``x:'a = x'``) 28]; 29 30val tydef_th = prove( 31 ``?p. FST p /\ SND p``, 32 EXISTS_TAC ``(T,T)`` THEN REWRITE_TAC []); 33 34val _ = tprint "new_type_definition error message" 35val _ = 36 ignore (new_type_definition("mytydef", tydef_th)) 37 handle HOL_ERR {origin_function, message, origin_structure} => 38 if origin_function <> "new_type_definition" orelse 39 origin_structure <> "Theory.Definition" orelse 40 message <> "at Thm.prim_type_definition:\nexpected a theorem of the form \"?x. P x\"" 41 then 42 die "FAILED" 43 else OK() 44 45val _ = tprint "Q.MATCH_ABBREV_TAC with underscores" 46val goal = ([] : term list, ``(n + 10) * y <= 42315 /\ !x y:'a. x < f y``) 47val (sgs, _) = Q.MATCH_ABBREV_TAC `a * _ <= b /\ _` goal 48val expectedg = ``(a:num) * y <= b /\ !x y:'a. x < f y`` 49val exab1 = ``Abbrev((a:num) = n + 10)`` 50val exab2 = ``Abbrev((b:num) = 42315)`` 51val _ = case sgs of 52 [(asms, g')] => 53 if aconv g' expectedg andalso op_mem aconv exab1 asms andalso 54 op_mem aconv exab2 asms andalso length asms = 2 55 then 56 OK() 57 else die "FAILED!" 58 | _ => die "FAILED!" 59 60val _ = tprint "qhdtm_x_assum (1)" 61val goal = ([``x = 3``, ``FACT n = 10``], ``n + x = 7``) 62val (sgs, _) = qhdtm_x_assum `FACT` mp_tac goal 63val expectedg = ``(FACT n = 10) ==> (n + x = 7)`` 64val expecteda = ``x = 3`` 65val _ = case sgs of 66 [([a], g)] => if aconv g expectedg andalso aconv a expecteda then 67 OK() 68 else die "FAILED!" 69 | _ => die "FAILED!" 70 71local 72 73open match_goal 74 75val n = ref 0; 76 77fun test_assert P x = 78 (tprint ("match_goal "^(Int.toString (!n))); n := !n + 1; 79 if P x then OK() else die "FAILED!") 80 81val (test1:matcher * mg_tactic) = 82 (mg.a "H" `P_ /\ Q_`, 83 fn (t,a) => 84 kill_asm(t"H") 85 \\ strip_assume_tac(t"H" )) 86 87val P = mk_var("P",bool) 88val Q = mk_var("Q",bool) 89 90val (g1:goal) = ([boolSyntax.mk_conj(P,Q)], boolSyntax.mk_neg(P)) 91 92val res1 = 93 test_assert (goals_eq [([Q,P],boolSyntax.mk_neg(P))] o #1) 94 (match1_tac test1 g1) 95 96val test2 = 97 [ 98 ([mg.abc `if b_ then _ else _`], 99 fn (t,a) => (Cases_on`^(a"b")`)) 100 ,([],(K ALL_TAC):mg_tactic) 101 ] 102 103val res1' = test_assert (goals_eq [g1] o #1) (first_match_tac test2 g1) 104 105val g2 = ([``x:bool = if P then x' else x''``, ``x:bool``],``yi = if x then x'' else (ARB:bool)``) 106 107val res2 = test_assert (equal 2 o length o #1) 108 (first_match_tac test2 g2) 109 110val (test3:matcher list * mg_tactic) = 111 ([ mg.a "h1" `f_ _ = _`, 112 mg.a "h2" `f_ _ = _` 113 ], 114 fn (a,t) => 115 disch_then (drule_thm (a"h1")) 116 \\ disch_then (drule_thm (a"h2")) 117 \\ disch_then ACCEPT_TAC) 118 119val g3 = ( 120 [``f (x:num) = 3n``, 121 ``g (y:num) = 5n``, 122 ``f (y:num) = 4n``], 123 ``(!(a:num) g (b:num) z1 z2. (f a = z1) ==> (g b = z2) ==> z1 + z2 < 7n) ==> 3 + 4 < 7n``) 124 125val res3 = test_assert (List.null o #1) 126 (match_tac test3 g3) 127 128val (test4:matcher list * mg_tactic) = 129 ([ mg.a "h1" `f_ _ = _`, 130 mg.a "h2" `f_ _ = _`, 131 mg.cb `(f_ _ = _) ==> _` 132 ], 133 fn (a,t) => 134 disch_then (drule_thm (a"h1")) 135 \\ disch_then (drule_thm (a"h2"))) 136 137val g4 = ( 138 [``f (x:num) = 3n``, 139 ``g (y:num) = 5n``, 140 ``f (y:num) = 4n``], 141 ``(!(a:num) g (b:num) z1 z2. (f a = z1) ==> (g b = z2) ==> z1 + z2 < 10n) ==> 3 + 4 < 10n``) 142 143val res4 = test_assert (aconv ``3 + 4 < 10n ==> 3 + 4 < 10n`` o #2 o hd o #1) 144 (match_tac test4 g4) 145 146in end 147 148local 149val tyis = TypeBase.elts() 150fun check tyi = 151 let 152 open TypeBasePure Portable 153 val tynm = let val (thy,opn) = ty_name_of tyi in thy^"$"^opn end 154 val _ = tprint ("Checking simpls for "^tynm) 155 val simpls = map concl $ #rewrs $ simpls_of tyi 156 val simpls_set = HOLset.addList(empty_tmset, simpls) 157 in 158 if HOLset.numItems simpls_set = length simpls then OK() 159 else die "Duplicates exist" 160 end 161in 162val _ = app check tyis 163end (* local *) 164 165 166local 167val _ = Globals.interactive := true 168val _ = Feedback.emit_MESG := false 169val _ = Datatype`testrcd = <| fld1 : num ; fld2 : bool |>`; 170 171fun test (msg, c) = 172 let 173 val _ = tprint ("Record constructor injectivity ("^msg^")") 174 in 175 require_msg (check_result (aconv ``(x:num = y) /\ (a <=> b)``)) 176 term_to_string (rhs o concl o c) 177 ``testrcd x a = testrcd y b``; 178 () 179 end 180in 181val _ = List.app test [("simp", SIMP_CONV (srw_ss()) []), ("EVAL", EVAL)] 182end (* local *) 183 184local 185 open listSyntax 186 fun mkl nm = mk_var(nm, mk_list_type alpha) 187 val appl_t = list_mk_append (map mkl ["x", "y", "z"]) 188 val appr_t = mk_append(mkl "x", mk_append(mkl "y", mkl"z")) 189in 190val _ = tprint "Std simp left-normalises list" 191val _ = require_msg (check_result (aconv appl_t o rhs o concl)) thm_to_string 192 (QCONV (SIMP_CONV (srw_ss()) [])) appr_t 193val _ = tprint "Simp -* APPEND_ASSOC leaves list unchanged" 194val _ = require_msg (check_result (aconv appr_t o rhs o concl)) thm_to_string 195 (QCONV (SIMP_CONV (srw_ss() -* ["APPEND_ASSOC"]) [])) appr_t 196val _ = tprint "Simp -* list.APPEND_ASSOC leaves list unchanged" 197val _ = require_msg (check_result (aconv appr_t o rhs o concl)) thm_to_string 198 (QCONV (SIMP_CONV (srw_ss() -* ["list.APPEND_ASSOC"]) [])) 199 appr_t 200val _ = tprint "Simp -* list.APPEND_ASSOC.1 leaves list unchanged" 201val _ = require_msg (check_result (aconv appr_t o rhs o concl)) thm_to_string 202 (QCONV (SIMP_CONV (srw_ss() -* ["list.APPEND_ASSOC.1"]) [])) 203 appr_t 204val _ = tprint "Simp Excl APPEND_ASSOC leaves list unchanged" 205val _ = require_msg (check_result (aconv appr_t o rhs o concl)) thm_to_string 206 (QCONV (SIMP_CONV (srw_ss()) [Excl "APPEND_ASSOC"])) appr_t 207val _ = tprint "Simp Excl list.APPEND_ASSOC leaves list unchanged" 208val _ = require_msg (check_result (aconv appr_t o rhs o concl)) thm_to_string 209 (QCONV (SIMP_CONV (srw_ss()) [Excl "list.APPEND_ASSOC"])) 210 appr_t 211val _ = shouldfail { 212 checkexn = (fn UNCHANGED => true | _ => false), 213 printarg = fn _ => "simp Excl on arith d.p. leaves input unchanged", 214 printresult = thm_to_string, 215 testfn = SIMP_CONV (srw_ss() ++ ARITH_ss) [Excl "NUM_ARITH_DP"] 216 } ���4 < x ==> 2 < x��� 217end 218 219val _ = tprint "find num->num includes SUC" 220val _ = require_msg (check_result (tmem numSyntax.suc_tm)) 221 (listprint term_to_string) 222 find_consts ���:num->num��� 223val _ = tprint "find 'a includes SUC" 224val _ = require_msg (check_result (tmem numSyntax.suc_tm)) 225 (listprint term_to_string) 226 find_consts ���:'a��� 227val _ = tprint "find 'a->'a includes SUC" 228val _ = require_msg (check_result (tmem numSyntax.suc_tm)) 229 (listprint term_to_string) 230 find_consts ���:'a->'a��� 231val _ = tprint "find 'b->'b includes SUC" 232val _ = require_msg (check_result (tmem numSyntax.suc_tm)) 233 (listprint term_to_string) 234 find_consts ���:'b->'b��� 235val _ = tprint "find 'a -> 'b -> 'c doesn't include SUC" 236val _ = require_msg (check_result (not o tmem numSyntax.suc_tm)) 237 (listprint term_to_string) 238 find_consts ���:'a->'b->'c��� 239val _ = tprint "find_thy [bool,relation] 'a -> 'a doesn't include SUC" 240val _ = require_msg (check_result (not o tmem numSyntax.suc_tm)) 241 (listprint term_to_string) 242 (find_consts_thy ["bool", "relation"]) ���:'a->'a��� 243val _ = tprint "find_thy [bool,relation] 'a -> 'a includes RTC" 244val _ = require_msg (check_result (tmem ���relation$RTC���)) 245 (listprint term_to_string) 246 (find_consts_thy ["bool", "relation"]) ���:'a->'a��� 247val _ = tprint "find_thy [bool,relation] num -> num doesn't include RTC" 248val _ = require_msg (check_result (not o tmem ���relation$RTC���)) 249 (listprint term_to_string) 250 (find_consts_thy ["bool", "relation"]) ���:num->num��� 251 252val _ = new_constant("foo", ���:'a -> num���) 253 254val _ = tprint "find 'a finds new constant" 255val _ = require_msg (check_result (tmem ���foo���)) (listprint term_to_string) 256 find_consts ���:'a��� 257 258 259val _ = new_constant ("split", ``:num list -> (num list # num list) ``) 260local 261 val quotation = ` 262 bar �� = 263 case split �� of 264 (��1, ��2) => if EVEN (bar ��1) then 2 else bar ��2` 265 266 val mkdef = quietly (Defn.mk_defn "bar") 267 fun test q = 268 let 269 val (tm,_) = Defn.parse_absyn (Parse.Absyn q) 270 in 271 (mkdef tm, mkdef tm) 272 end 273 fun is_nested (DefnBase.NESTREC _ ) = true | is_nested _ = false 274 fun check_defs (d1,d2) = 275 is_nested d1 andalso is_nested d2 andalso 276 length (Defn.tcs_of d1) = length (Defn.tcs_of d2) 277 val ppd = PP.pp_to_string 65 DefnBase.pp_defn 278 fun prdefpair (d1,d2) = ppd d1 ^ "\n vs\n" ^ ppd d2 279in 280val _ = tprint "TFL nested recursion + Unicode parameter name" 281val _ = require_msg (check_result check_defs) prdefpair test quotation 282end 283 284val goalpp = 285 HOLPP.pp_to_string 75 ( 286 HOLPP.block HOLPP.CONSISTENT 0 o 287 HOLPP.pr_list goalStack.pp_goal [HOLPP.NL, HOLPP.NL] 288 ) 289fun testtac tac = #1 o VALID tac 290 291val _ = let 292 val _ = tprint "tmCases_on (.doc file example)" 293 val g = ([], ���MAP (f:num -> num) l = []���) 294 val expected = [([] : term list, ���MAP (f:num -> num) [] = []���), 295 ([] : term list , ���MAP (f:num -> num) (e::es) = []���)] 296in 297 require_msg (check_result (list_eq goal_eq expected)) 298 goalpp 299 (testtac (tmCases_on (mk_var("l", alpha)) ["", "e es"])) 300 g 301end 302 303val _ = let 304 val _ = tprint "tmCases_on (bound l)" 305 val g = ([], ���!l. MAP (f:num -> num) l = []���) 306 val expected = [([] : term list, ���MAP (f:num -> num) [] = []���), 307 ([] : term list , ���MAP (f:num -> num) (e::es) = []���)] 308in 309 require_msg (check_result (list_eq goal_eq expected)) 310 goalpp 311 (testtac (tmCases_on (mk_var("l", alpha)) ["", "e es"])) 312 g 313end 314 315val _ = let 316 val _ = tprint "resolve_then/IRULE hyp order preserved" 317 val th1 = rich_listTheory.is_prefix_el 318 val g = ([], ���?m n. EL m (l1:'a list) = EL n l2 /\ m <= n /\ EVEN n���) 319 val expected = 320 [([] : term list, 321 ���?n. (l1:'a list) <<= l2 /\ n < LENGTH l1 /\ n < LENGTH l2 /\ n <= n /\ 322 EVEN n���)] 323in 324 require_msg (check_result (list_eq goal_eq expected)) 325 goalpp 326 (testtac ((goal_assum o resolve_then Any mp_tac) th1)) 327 g 328end 329 330val gstest_goal = 331 ([``x <= b``, ``b - x = b - y``, ``y <= b``], ``x * y < 10``); 332val _ = 333 shouldfail { 334 checkexn = check_HOL_ERRexn (fn(_,s2,_) => s2 = "CHANGED_TAC"), 335 printarg = fn _ => "fs with ordering failure", 336 printresult = goalpp, 337 testfn = testtac (CHANGED_TAC (fs [arithmeticTheory.SUB_CANCEL])) 338 } gstest_goal 339 340val _ = tprint "gs with ordering works" 341val _ = require_msg 342 (check_result 343 (goals_eq [([���y <= b���, ���x:num = y���], ���y ** 2 < 10���)])) 344 goalpp 345 (testtac (gs[arithmeticTheory.SUB_CANCEL])) 346 gstest_goal 347 348val _ = tprint "gvs with ordering works" 349val _ = require_msg 350 (check_result 351 (goals_eq [([���x <= b���], ���x ** 2 < 10���)])) 352 goalpp 353 (testtac (gvs[arithmeticTheory.SUB_CANCEL])) 354 gstest_goal 355 356fun test_tac_Case nm ok_case_arg tq tac = let 357 val t = Parse.typed_parse_in_context bool [] tq 358 val _ = tprint (nm^" on `"^term_to_string t^"`") 359 val (goals, _) = tac ([], t) 360 fun ok_case t = ok_case_arg (markerSyntax.dest_Case t) 361 handle HOL_ERR _ => false 362 fun has_ok_Case (asms, _) = Lib.exists ok_case asms 363 val missing = filter (not o has_ok_Case) goals 364in 365 if null missing 366 then OK () 367 else die (int_to_string (length missing) ^ " goals missing Case.\nFAILED!\n") 368end handle HOL_ERR _ => die "FAILED (tactic failed)!\n" 369 370val _ = test_tac_Case "list ind" (K true) 371 `!xs. NULL xs` 372 (recInduct 373 (name_ind_cases [] listTheory.list_induction) 374 \\ rpt strip_tac) 375 376val _ = test_tac_Case "OLEAST deep intro" (K true) 377 `THE (OLEAST n. n > SUC 3) < 8` 378 (DEEP_INTRO_TAC 379 (name_ind_cases [] whileTheory.OLEAST_INTRO) 380 \\ rpt strip_tac) 381 382val (is_rev_rules, is_rev_ind, is_rev_cases) = Hol_reln` 383 (is_rev [] []) /\ 384 (!x xs ys. is_rev xs ys ==> is_rev (CONS x xs) (SNOC x ys))`; 385 386val _ = test_tac_Case "is_rev rule ind" (K true) 387 `!xs ys. is_rev xs ys ==> !zs. is_rev ys zs ==> zs = xs` 388 (ho_match_mp_tac 389 (name_ind_cases [] is_rev_ind) 390 \\ rpt strip_tac) 391 392val f_def = Define` 393 f [] = [] /\ 394 f (x :: xs) = x :: f2 xs /\ 395 f2 [] = [] /\ 396 f2 (x :: xs) = x :: f xs`; 397val f_ind = theorem "f_ind"; 398 399val diff_names_test = let 400 val thm = name_ind_cases [F,T] f_ind 401 val cases = find_terms (can markerSyntax.dest_Case) (concl thm) 402 val ok = length (op_mk_set term_eq cases) = length cases 403 in 404 if ok then OK () else die "diff_names_test: duplicates" 405 end handle HOL_ERR _ => die "diff_names_test: exception" 406 407val _ = test_tac_Case "is_rev rule ind" 408 (can (find_term (fn t => same_const T t orelse same_const F t))) 409 `(!xs : 'a list. f xs = xs) /\ (!xs : 'a list. f2 xs = xs)` 410 (ho_match_mp_tac 411 (name_ind_cases [F, T] f_ind) 412 \\ rpt strip_tac) 413 414val ss = srw_ss() 415val _ = convtest ("standard simp on h::t = []", SIMP_CONV ss [], 416 ���h::t = [] : 'a list���, ���F���) 417val _ = BasicProvers.recreate_sset_at_parentage (parents "list") 418val _ = shouldfail {checkexn = fn UNCHANGED => true | _ => false, 419 printarg = K "after setting parents, same raises UNCHANGED", 420 printresult = term_to_string, 421 testfn = rhs o concl o SIMP_CONV (srw_ss()) []} 422 ���h::t = [] : 'a list��� 423val _ = convtest ("adjusted simp_conv on set comprehension", 424 SIMP_CONV (srw_ss()) [], 425 ���y IN {x | x < 10}���, ���y < 10���) 426val _ = convtest ("stored simp_conv still fine on h::t = []", SIMP_CONV ss [], 427 ���h::t = [] : 'a list���, ���F���) 428val _ = tprint "Tactic simp[] on set comprehension" 429val _ = require_msg (check_result (aconv ���y < 10��� o #2 o hd o #1)) 430 (term_to_string o #2 o hd o #1) 431 (simp[]) ([], ���y IN {x | x < 10}���) 432