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