1open HolKernel Parse boolLib testutils 2open pairTheory sumTheory optionTheory optionSyntax 3 4val _ = set_trace "Unicode" 0 5 6(* testing for sums *) 7val _ = tpp "case s of INL b => b | INR c => ~c" 8 9(* testing for options *) 10val alpha_option_ty = mk_option alpha 11val alphanone_t = mk_thy_const{Thy = "option", Name = "NONE", Ty = alpha_option_ty} 12 13val _ = tprint "dest_none returns unwrapped type" 14val ty = dest_none alphanone_t 15val _ = if Type.compare(ty, alpha) = EQUAL then OK() 16 else die "FAILED!" 17 18val _ = tpp "case opt of NONE => T | SOME b => b" 19 20(* tests for option monad stuff evaluation *) 21val _ = convtest ("EVAL OPTION_BIND(1)", computeLib.EVAL_CONV, 22 ``OPTION_BIND (SOME T) (\x. SOME x)``, ``SOME T``) 23val _ = convtest ("EVAL OPTION_BIND(2)", computeLib.EVAL_CONV, 24 ���OPTION_BIND NONE (\x:bool. SOME x)���, ���NONE : bool option���) 25 26val _ = convtest ("EVAL OPTION_IGNORE_BIND(1)", computeLib.EVAL_CONV, 27 ``OPTION_IGNORE_BIND (SOME T) (SOME (\x:'a. x))``, 28 ``SOME (\x:'a. x)``) 29val _ = convtest ("EVAL OPTION_IGNORE_BIND(2)", computeLib.EVAL_CONV, 30 ``OPTION_IGNORE_BIND (NONE : bool option) (SOME (\x:'a. x))``, 31 ���NONE : ('a -> 'a) option���) 32 33(* testing for pairs *) 34val die = fn () => die "FAILED!\n" 35fun sdie s = testutils.die ("FAILED!\n "^s^"\n") 36 37val _ = app tpp ["\\(x,y). x /\\ y", 38 "\\(x,y,z). x /\\ y /\\ z", 39 "\\((x,y),z). x /\\ y /\\ z", 40 "(\\(x,y,z). x /\\ y /\\ z) p", 41 "case x of (y,z) => y /\\ z", 42 "f000000000 arg000000000\n\ 43 \ (case x of\n\ 44 \ INL u => u inl00000000000 inl111111111\n\ 45 \ | INR v => v inr00000000000 inr111111111)\n\ 46 \ (arg222222222222 arg333333333 arg444444444)" 47 ] 48 49(* check LET_INTRO *) 50 51val _ = let 52 val _ = tprint "Testing pairTools.LET_INTRO" 53 val _ = pairTools.LET_INTRO (ASSUME ``((x,y) = (zw)) ==> (ARB x y):bool``) 54 val _ = pairTools.LET_INTRO (ASSUME ``((x,y) = (z,w)) ==> (ARB x y):bool``) 55 val _ = OK() 56in 57 () 58end handle e => die() 59 60(* parsing of case expressions with conditionals as arms *) 61val _ = tprint "Parsing case expressions with conditional arms" 62val t1 = ``case p:'a#'b of (x,y) => if y = a then x else f x y`` 63val t2 = ``pair_CASE (p:'a # 'b) (\x y. if y = a then x else f x y)`` 64val _ = if aconv t1 t2 then OK() else die() 65 66val _ = print "**** More Inductive Definition tests ****\n" 67open IndDefLib 68fun checkhyps th = if null (hyp th) then () 69 else sdie "FAILED - Hyps in theorem!" 70 71(* emulate the example in examples/monosetScript.sml *) 72val _ = print "*** Testing monoset example\n" 73val _ = new_type ("t", 0) 74val _ = new_type ("list", 1) 75val _ = new_type ("num", 0) 76val _ = new_constant ("v", ``:num -> t``) 77val _ = new_constant ("app", ``:t list -> t``) 78val _ = new_constant ("EVERY", ``:('a -> bool) -> 'a list -> bool``) 79val _ = new_constant ("MEM", ``:'a -> 'a list -> bool``) 80val _ = new_constant ("ZIP", ``:('a list # 'b list) -> ('a # 'b) list``) 81 82val MONO_EVERY = mk_thm([], ``(!x:'a. P x ==> Q x) ==> 83 (EVERY P l ==> EVERY Q l)``) 84val _ = add_mono_thm MONO_EVERY 85 86val (red_rules, red_ind, red_cases) = Hol_reln ` 87 (!n. red f (v n) (v (f n))) /\ 88 (!t0s ts. EVERY (\ (t0,t). red f t0 t) (ZIP (t0s, ts)) ==> 89 red f (app t0s) (app ts)) 90`; 91val _ = checkhyps red_rules 92 93(* emulate Peter's example *) 94val _ = print "*** Testing Peter's example\n" 95val _ = new_constant ("nil", ``:'a list``) 96val _ = new_constant ("SUC", ``:num -> num``) 97val _ = new_constant ("cons", ``:'a -> 'a list -> 'a list``) 98val _ = new_constant ("HD", ``:'a list -> 'a``) 99val _ = new_constant ("TL", ``:'a list -> 'a list``) 100val (ph_rules, ph_ind, ph_cases) = Hol_reln` 101 (WF_CX nil) /\ 102 (!s ty cx. WF_CX cx /\ WF_TYPE cx ty ==> WF_CX (cons (s,ty) cx)) /\ 103 104 (!n cx. WF_CX cx ==> WF_TYPE cx (v n)) /\ 105 (!ts cx s. WF_CX cx /\ MEM (s, HD ts) cx /\ EVERY (\t. WF_TYPE cx t) ts /\ 106 red SUC (HD ts) (HD (TL ts)) ==> 107 WF_TYPE cx (app ts)) 108` 109val _ = checkhyps ph_rules 110 111(* UNCURRY with more than two arguments *) 112val _ = new_constant ("Z", ``:num``) 113val _ = new_constant ("ONE", ``:num``) 114val _ = new_constant ("TWO", ``:num``) 115val _ = print "*** Testing UNCURRY with more than two arguments\n" 116val (u3_rules, u3_ind, u3_cases) = Hol_reln` 117 u3 (Z,ONE,TWO) /\ 118 (!x y z. (\ ((x,y), z). u3 (x,y,z)) ((y,x),z) ==> u3 (x,y,z)) 119` 120val _ = checkhyps u3_rules 121 122(* single rule *) 123val _ = print "*** Testing strong principle for singleton rule\n" 124val _ = new_constant ("+", ``:num -> num -> num``) 125val _ = set_fixity "+" (Infixl 500) 126val (single_rules, single_ind, single_cases) = Hol_reln` 127 (!x y. RTC single x y \/ (x = y + TWO) ==> single x y) 128`; 129val _ = checkhyps single_rules 130 131val _ = print "*** Overloading case constant (pairs)\n" 132val _ = overload_on ("foo", ``\p. case p of (x,y) => x /\ y``) 133val _ = tpp "foo z" 134val _ = set_trace "types" 1 135val _ = trace ("types", 1) tpp "case (p :'a # 'b) of (x,y) => x" 136 137val _ = print "*** Overloading case constant (booleans)\n" 138val _ = overload_on ("bar", ``\b. if b then T else F``) 139val _ = tpp "bar T" 140val _ = trace ("types", 1) tpp "if (b :bool) then (x :'a) else (y :'a)" 141 142(* pairLib conversions etc *) 143val _ = List.app convtest [ 144 ("PairRules.PBETA_CONV(1)", PairRules.PBETA_CONV, 145 ���(\ (a:'a,b:'b). f (a,b) (c:'c) : 'd) x���, ���(f:'a # 'b -> 'c -> 'd) x c���), 146 ("PairRules.PETA_CONV(1)", PairRules.PETA_CONV, 147 ���(\ (a:'a,b:'b). f (a,b) : 'c)���, ���f : 'a # 'b -> 'c���) 148] 149 150local open pairLib in 151val _ = print "*** new_specification with existential definition\n" 152val th = metisLib.METIS_PROVE[]``?x y z. x ==> z /\ z ==> y``; 153val _ = tprint "Testing 0 constants" 154val nothing_def = new_specification("nothing_def",[],th); 155val _ = OK() 156val _ = tprint "Testing 1 constant" 157val a_def = new_specification("a_def",["a"],th); 158val _ = OK() 159val _ = tprint "Testing 2 constants" 160val pq_def = new_specification("pq_def",["p","q"],th); 161val _ = OK() 162val _ = tprint "Testing 3 constants" 163val rst_def = new_specification("rst_def",["r","s","t"],th); 164val _ = OK() 165end 166 167(* split_pair_case_tac *) 168open pairLib 169val _ = app (ignore o hide) ["aa", "bb", "xx", "pp", "qq"] 170val _ = tprint "split_pair_case_tac (case in goal)" 171val _ = let 172 val g = ([] : term list, ``case xx of (aa,bb) => aa /\ bb``) 173 fun check (sgs, vfn) = 174 case sgs of 175 [([a], g')] => aconv (#2 g) g' andalso 176 aconv a ``xx = (aa:bool,bb:bool)`` 177 | _ => false 178in 179 require (check_result check) split_pair_case_tac g 180end; 181 182val _ = tprint "split_pair_case_tac (case in assumptions)" 183val _ = let 184 val a = ``case xx of (aa,bb) => aa /\ bb`` 185 val g = ``pp /\ qq`` 186 fun check (sgs, vfn) = 187 case sgs of 188 [([a1, a2], g')] => aconv g' g andalso 189 aconv a1 ``xx = (aa:bool, bb:bool)`` andalso 190 aconv a2 a 191 | _ => false 192in 193 require (check_result check) split_pair_case_tac ([a], ``pp /\ qq``) 194end 195 196val _ = Feedback.emit_MESG := false 197val _ = Feedback.emit_WARNING := false 198val _ = delete_const "v" 199 200val _ = tprint "simp (srw_ss()) on one_CASE" 201local open BasicProvers simpLib 202in 203val _ = require_msg (check_result (aconv ``v:'a``)) term_to_string 204 (rhs o concl o SIMP_CONV (srw_ss()) []) 205 ``one_CASE () (v:'a)`` 206end 207 208(* github issue #765; induction principle for pairs is wrong *) 209val _ = hide "p" 210val _ = tprint "Induction principle for pairs" 211val res = Exn.capture (BasicProvers.Induct_on ���p���) ([], ���FST p ��� SND p���) 212val _ = case res of 213 Exn.Res _ => OK() 214 | Exn.Exn e => sdie ("Exception : " ^ General.exnMessage e) 215 216(* removing thy-named fragments *) 217local 218 open simpLib BasicProvers 219in 220val _ = convtest("srw_ss has x = () rewrite", SIMP_CONV (srw_ss()) [], 221 ���x:unit���, ���() : unit���) 222val _ = diminish_srw_ss ["one"] 223val _ = shouldfail {checkexn = fn UNCHANGED => true | _ => false, 224 printarg = K "after diminish\"one\", that no longer works", 225 printresult = thm_to_string, 226 testfn = SIMP_CONV (srw_ss()) []} 227 ���x:unit��� 228end (* local *) 229 230val _ = Process.exit Process.success 231