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 43(* check LET_INTRO *) 44 45val _ = let 46 val _ = tprint "Testing pairTools.LET_INTRO" 47 val _ = pairTools.LET_INTRO (ASSUME ``((x,y) = (zw)) ==> (ARB x y):bool``) 48 val _ = pairTools.LET_INTRO (ASSUME ``((x,y) = (z,w)) ==> (ARB x y):bool``) 49 val _ = OK() 50in 51 () 52end handle e => die() 53 54(* parsing of case expressions with conditionals as arms *) 55val _ = tprint "Parsing case expressions with conditional arms" 56val t1 = ``case p:'a#'b of (x,y) => if y = a then x else f x y`` 57val t2 = ``pair_CASE (p:'a # 'b) (\x y. if y = a then x else f x y)`` 58val _ = if aconv t1 t2 then OK() else die() 59 60val _ = print "**** More Inductive Definition tests ****\n" 61open IndDefLib 62fun checkhyps th = if null (hyp th) then () 63 else sdie "FAILED - Hyps in theorem!" 64 65(* emulate the example in examples/monosetScript.sml *) 66val _ = print "*** Testing monoset example\n" 67val _ = new_type ("t", 0) 68val _ = new_type ("list", 1) 69val _ = new_type ("num", 0) 70val _ = new_constant ("v", ``:num -> t``) 71val _ = new_constant ("app", ``:t list -> t``) 72val _ = new_constant ("EVERY", ``:('a -> bool) -> 'a list -> bool``) 73val _ = new_constant ("MEM", ``:'a -> 'a list -> bool``) 74val _ = new_constant ("ZIP", ``:('a list # 'b list) -> ('a # 'b) list``) 75 76val MONO_EVERY = mk_thm([], ``(!x:'a. P x ==> Q x) ==> 77 (EVERY P l ==> EVERY Q l)``) 78val _ = add_mono_thm MONO_EVERY 79 80val (red_rules, red_ind, red_cases) = Hol_reln ` 81 (!n. red f (v n) (v (f n))) /\ 82 (!t0s ts. EVERY (\ (t0,t). red f t0 t) (ZIP (t0s, ts)) ==> 83 red f (app t0s) (app ts)) 84`; 85val _ = checkhyps red_rules 86 87(* emulate Peter's example *) 88val _ = print "*** Testing Peter's example\n" 89val _ = new_constant ("nil", ``:'a list``) 90val _ = new_constant ("SUC", ``:num -> num``) 91val _ = new_constant ("cons", ``:'a -> 'a list -> 'a list``) 92val _ = new_constant ("HD", ``:'a list -> 'a``) 93val _ = new_constant ("TL", ``:'a list -> 'a list``) 94val (ph_rules, ph_ind, ph_cases) = Hol_reln` 95 (WF_CX nil) /\ 96 (!s ty cx. WF_CX cx /\ WF_TYPE cx ty ==> WF_CX (cons (s,ty) cx)) /\ 97 98 (!n cx. WF_CX cx ==> WF_TYPE cx (v n)) /\ 99 (!ts cx s. WF_CX cx /\ MEM (s, HD ts) cx /\ EVERY (\t. WF_TYPE cx t) ts /\ 100 red SUC (HD ts) (HD (TL ts)) ==> 101 WF_TYPE cx (app ts)) 102` 103val _ = checkhyps ph_rules 104 105(* UNCURRY with more than two arguments *) 106val _ = new_constant ("Z", ``:num``) 107val _ = new_constant ("ONE", ``:num``) 108val _ = new_constant ("TWO", ``:num``) 109val _ = print "*** Testing UNCURRY with more than two arguments\n" 110val (u3_rules, u3_ind, u3_cases) = Hol_reln` 111 u3 (Z,ONE,TWO) /\ 112 (!x y z. (\ ((x,y), z). u3 (x,y,z)) ((y,x),z) ==> u3 (x,y,z)) 113` 114val _ = checkhyps u3_rules 115 116(* single rule *) 117val _ = print "*** Testing strong principle for singleton rule\n" 118val _ = new_constant ("+", ``:num -> num -> num``) 119val _ = set_fixity "+" (Infixl 500) 120val (single_rules, single_ind, single_cases) = Hol_reln` 121 (!x y. RTC single x y \/ (x = y + TWO) ==> single x y) 122`; 123val _ = checkhyps single_rules 124 125val _ = print "*** Overloading case constant (pairs)\n" 126val _ = overload_on ("foo", ``\p. case p of (x,y) => x /\ y``) 127val _ = tpp "foo z" 128val _ = set_trace "types" 1 129val _ = trace ("types", 1) tpp "case (p :'a # 'b) of (x,y) => x" 130 131val _ = print "*** Overloading case constant (booleans)\n" 132val _ = overload_on ("bar", ``\b. if b then T else F``) 133val _ = tpp "bar T" 134val _ = trace ("types", 1) tpp "if (b :bool) then (x :'a) else (y :'a)" 135 136(* pairLib conversions etc *) 137fun convtest (nm,conv,t,expected) = 138 let 139 val _ = tprint nm 140 val res = conv t 141 in 142 if aconv (rhs (concl res)) expected then OK() else die() 143 end 144val _ = List.app convtest [ 145 ("PairRules.PBETA_CONV(1)", PairRules.PBETA_CONV, 146 ���(\ (a:'a,b:'b). f (a,b) (c:'c) : 'd) x���, ���(f:'a # 'b -> 'c -> 'd) x c���), 147 ("PairRules.PETA_CONV(1)", PairRules.PETA_CONV, 148 ���(\ (a:'a,b:'b). f (a,b) : 'c)���, ���f : 'a # 'b -> 'c���) 149] 150 151local open pairLib in 152val _ = print "*** new_specification with existential definition\n" 153val th = metisLib.METIS_PROVE[]``?x y z. x ==> z /\ z ==> y``; 154val _ = tprint "Testing 0 constants" 155val nothing_def = new_specification("nothing_def",[],th); 156val _ = OK() 157val _ = tprint "Testing 1 constant" 158val a_def = new_specification("a_def",["a"],th); 159val _ = OK() 160val _ = tprint "Testing 2 constants" 161val pq_def = new_specification("pq_def",["p","q"],th); 162val _ = OK() 163val _ = tprint "Testing 3 constants" 164val rst_def = new_specification("rst_def",["r","s","t"],th); 165val _ = OK() 166end 167 168(* split_pair_case_tac *) 169open pairLib 170val _ = app (ignore o hide) ["aa", "bb", "xx", "pp", "qq"] 171val _ = tprint "split_pair_case_tac (case in goal)" 172val g = ([] : term list, ``case xx of (aa,bb) => aa /\ bb``) 173val (sgs, vfn) = split_pair_case_tac g handle HOL_ERR _ => die () 174val _ = case sgs of 175 [([a], g')] => if aconv (#2 g) g' andalso 176 aconv a ``xx = (aa:bool,bb:bool)`` 177 then OK() 178 else die () 179 | _ => die () 180 181val _ = tprint "split_pair_case_tac (case in assumptions)" 182val a = ``case xx of (aa,bb) => aa /\ bb`` 183val g = ``pp /\ qq`` 184val (sgs, vfn) = split_pair_case_tac ([a], ``pp /\ qq``) 185 handle HOL_ERR _ => die() 186val _ = case sgs of 187 [([a1, a2], g')] => if aconv g' g andalso 188 aconv a1 ``xx = (aa:bool, bb:bool)`` andalso 189 aconv a2 a 190 then OK() 191 else die() 192 | _ => die() 193 194 195val _ = Process.exit Process.success 196