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