1(* tests for Hol_datatype *)
2
3open HolKernel Parse
4open testutils
5
6val _ = Feedback.set_trace "Theory.save_thm_reporting" 0;
7
8fun Hol_datatype q = let
9  open TextIO Feedback
10  val _ = Datatype.Hol_datatype q
11      handle e => (output(stdErr, "Exception raised: "^exn_to_string e);
12                   Process.exit Process.failure)
13in
14  ()
15end
16
17val Datatype = Datatype.Datatype
18
19fun primrec_test ty = let
20  val rcd = {nchotomy = TypeBase.nchotomy_of ty,
21             case_def = TypeBase.case_def_of ty}
22  open Prim_rec
23in
24  (prove_case_elim_thm rcd, prove_case_rand_thm rcd)
25end
26
27val _ = Hol_datatype `type1 = one_constructor`
28
29val _ = let
30  val _ = tprint "type_to_string immediately after type defn"
31  val s = prim_mk_const{Thy = "scratch", Name = "one_constructor"}
32                       |> type_of |> Parse.type_to_string
33in
34  if s = ":type1" then OK()
35  else die ("\nFAILED: got \"" ^ String.toString s ^ "\"; not \":type1\"")
36end
37
38
39val _ = Hol_datatype `type2 = ##`;
40val _ = Hol_datatype `type3 = /\`;
41val _ = Hol_datatype `type4 = /\ | \/ | feh`;
42val _ = Hol_datatype `type5 = foo of num | bar of 'a`;
43
44val _ = map primrec_test [``:type1``, ``:type4``, ``:'a type5``]
45
46val _ = Hol_datatype `foo = NIL | CONS of 'a => foo`;
47val _ = Hol_datatype `list = NIL | :: of 'a => list`;
48val _ = Hol_datatype `void = Void`;
49val _ = Hol_datatype `pair = CONST of 'a#'b`;
50val _ = Hol_datatype `onetest = OOOO of one`;
51val _ = Hol_datatype `tri = Hi | Lo | Fl`;
52val _ = Hol_datatype `iso = ISO of 'a`;
53val _ = Hol_datatype `ty = C1 of 'a
54          | C2
55          | C3 of 'a => 'b => ty
56          | C4 of ty => 'c => ty => 'a => 'b
57          | C5 of ty => ty`;
58val _ = primrec_test ``:('a,'b,'c)ty``
59val _ = Hol_datatype `bintree = LEAF of 'a | TREE of bintree => bintree`;
60val _ = Hol_datatype `typ = C of one => (one#one)
61                      => (one -> one -> 'a list)
62                      => ('a,one#one,'a list) ty`;
63val _ = primrec_test ``:'a typ``
64val _ = Hol_datatype `Typ = D of one # (one#one)
65                      # (one -> one -> 'a list)
66                      # ('a, one#one, 'a list) ty`;
67val _ = primrec_test ``:'a Typ``
68val _ = Hol_datatype`ftyp = ftypC1 of num => (num -> num) => ftyp
69                          | ftypC2 of bool => (num -> bool)`;
70val _ = primrec_test ``:ftyp``
71
72val _ = Hol_datatype `
73       var = V of num ;
74
75     atexp = var_exp of var
76           | let_exp of dec => exp ;
77
78       exp = aexp    of atexp
79           | app_exp of exp => atexp
80           | fn_exp  of match ;
81
82     match = match  of rule
83           | matchl of rule => match ;
84
85      rule = rule of pat => exp ;
86
87       dec = val_dec   of valbind
88           | local_dec of dec => dec
89           | seq_dec   of dec => dec ;
90
91   valbind = bind  of pat => exp
92           | bindl of pat => exp => valbind
93           | rec_bind of valbind ;
94
95       pat = wild_pat
96           | var_pat of var`;
97
98val state = Type`:ind->bool`;
99val nexp  = Type`:^state -> ind`;
100val bexp  = Type`:^state -> bool`;
101
102val _ = Hol_datatype `comm = skip
103            | :=    of bool list => ^nexp
104            | ;;    of comm => comm
105            | if    of ^bexp => comm => comm
106            | while of ^bexp => comm`;
107
108val _ = Hol_datatype
109          `ascii = ASCII of bool=>bool=>bool=>bool=>bool=>bool=>bool=>bool`;
110
111val _ = Hol_datatype`
112          small_record = <| fld1 : num -> bool ; fld2 : num |>
113`;
114
115val _ = Hol_datatype`squish_record = <|fld1:bool|>`
116val _ = Hol_datatype`poly_squish_record = <|fld1:'a->'b|>`
117val _ = Datatype.Datatype`parentest1 = C (('a,'b)fun)`
118
119val _ = tprint "Parse polymorphic record literal"
120val r = with_flag (Globals.guessing_tyvars, false) Parse.Term
121                  `<| fld1 := SUC |>`
122val rnd = repeat rand r
123val fupd_t = repeat rator r
124val (args, _) = strip_fun (type_of fupd_t)
125val fty = hd args
126val (d,r) = dom_rng fty
127val _ = if type_of rnd = ``:(num, num)poly_squish_record`` andalso
128           Type.compare(d,r) = EQUAL
129        then OK()
130        else die "FAILED!"
131val _ = tprint "TypeBase.mk_record on polymorphic record"
132val _ =
133    case Lib.total TypeBase.mk_record
134                   (``:(num,num)poly_squish_record``, [("fld1", ``SUC``)]) of
135        NONE => die "FAILED!"
136      | SOME _ => OK()
137
138val _ = Hol_datatype`K = <| F : 'a -> bool; S : num |>`
139
140val _ = Datatype.big_record_size := 10;
141val _ = Hol_datatype`
142  big_record = <| fld3 : num ; fld4: bool ; fld5 : num -> num;
143                  fld6 : bool -> bool ; fld7 : 'a -> num ;
144                  fld8 : num -> num ; fld9: bool # num ;
145                  fld10 : num + bool ; fld11 : bool option ;
146                  fld12 : bool ; fld13 : num |>`
147
148(* Tom Ridge's example from 2009/04/23 *)
149val _ = Hol_datatype `
150  command2 =
151     Skip2
152   | Seq2 of bool # command2 # command2
153   | IfThenElse2 of bool # num # command2 # command2
154   | While2 of (num # num) # bool # command2
155`;
156
157(* this version raises a different error *)
158val _ = Hol_datatype `
159  tr20090423 =
160     trSkip2
161   | trSeq2 of bool # tr20090423 # tr20090423
162   | trIfThenElse2 of bool # num # tr20090423 # tr20090423
163   | trWhile2 of (num # num) # bool # tr20090423
164`;
165
166(* both of these were fixed by r6750, which explicitly handles the product
167   type, and recursions underneath it. *)
168
169(* r6750 does not handle the following correctly though *)
170val _ = Hol_datatype`
171  fake_pair = FP of 'a => 'b
172`;
173
174val _ = add_infix_type {Assoc = RIGHT, Name = "fake_pair",
175                        ParseName = SOME "**", Prec = 70}
176
177val _ = Hol_datatype`
178  trprime = trpSkip
179      | trpSeq of bool ** trprime ** trprime
180      | trpIf of bool ** num ** trprime ** trprime
181      | trpW of (num ** num) ** bool ** trprime
182`;
183
184(* can see it "more directly" with
185val spec =
186    [(``:'trp``,
187      [("trpSkip", []),
188       ("trpSeq", [``:bool ** 'trp ** 'trp``]),
189       ("trpIf", [``:bool ** num ** 'trp ** 'trp``]),
190       ("trpW", [``:(num ** num) ** bool ** 'trp``])])]
191val result = ind_types.define_type spec handle e => Raise e;
192
193- note also that switching the order of the trpSeq and trpIf entries in the
194  list above makes it work again.  I.e.,
195
196val spec' =
197    [(``:'trp``,
198      [("trpSkip", []),
199       ("trpIf", [``:bool ** num ** 'trp ** 'trp``]),
200       ("trpSeq", [``:bool ** 'trp ** 'trp``]),
201       ("trpW", [``:(num ** num) ** bool ** 'trp``])])]
202val result = ind_types.define_type spec' handle e => Raise e;
203
204- works.
205
206*)
207
208(* Ramana Kumar's example from 2010/08/19 *)
209val _ = Hol_datatype`pointer = pnil | pref of 'a`
210val _ = Hol_datatype`failure = <| head : 'a pointer; tail : failure pointer |>`
211
212(* Ramana Kumar's examples from 2010/08/25 *)
213val _ = Hol_datatype `t1 = c1 of 'a => t1 itself `;
214val _ = Hol_datatype `t2 = c2 of t2 t1 itself ` ;
215
216val _ = Hol_datatype `u1 = d1 of 'a itself`;
217val _ = Hol_datatype `u2 = d2 of 'a u1 `;
218val _ = Hol_datatype `u3 = d3 of u4 u2 u1 ;
219                      u4 = d4 of u3 u1 `;
220
221(* Ramana Kumar's TypeNet bug from 2010/08/25 *)
222val _ = Hol_datatype `foo = fooC of 'a`
223val _ = Hol_datatype `foo = fooC' of num`
224
225(* from uvm-hol, 2016/10/03
226     issue is/was lexing of r-paren/semi-colon agglomerations
227*)
228val _ = Datatype.Datatype `
229  uvmhol1 = uvmholC uvmhol2 num (num -> bool);
230  uvmhol2 = uvmholD1 num | uvmHOLD2 uvmhol1
231`;
232
233val _ = Datatype.Datatype`
234  uvmhol3 = <| uvmfld1 : num # (num -> bool); uvmfld2 : bool |>
235`;
236
237val _ = tprint "Testing independence of case variables"
238val t = Lib.total Parse.Term `case (x:valbind) of
239                                bind p e => 3
240                              | bindl p' e p => 4
241                              | p => 5`
242val _ = case t of NONE => (print "FAILED!\n"; Process.exit Process.failure)
243                | SOME _ => OK()
244
245val _ = set_trace "Unicode" 0
246
247fun pptest (nm, t, expected) = let
248  val _ = tprint ("Pretty-printing of "^nm)
249  val s = Parse.term_to_string t
250in
251  if s = expected then OK()
252  else die ("FAILED!\n  Expected \""^expected^"\"; got \""^s^"\"")
253end
254
255fun s t = let open HolKernel boolLib
256          in
257            rhs (concl (simpLib.SIMP_CONV (BasicProvers.srw_ss()) [] t))
258          end
259
260val _ = Hol_datatype`ovlrcd = <| id : num ; opn : num -> num |>`
261val _ = overload_on ("ID", ``f.id``)
262val _ = overload_on ("inv", ``f.opn``)
263val _ = overload_on ("ovlfoo", ``\n r:ovlrcd. opn_fupd (K (K n)) r``)
264
265val _ = type_abbrev ("ms", ``:'a -> num``)
266val _ = Hol_datatype`
267  polyrcd = <| pfld1 : 'a ms ; pfld2 : 'b -> bool ; pfld3 : num|>
268`;
269
270val _ = Datatype.Datatype`
271  polyrcd2 = <| p2fld1 : 'a ms ; p2fld2 : 'a # 'b -> bool ; p2fld3 : num |>
272`
273
274val _ = List.app pptest
275        [("specific upd overload", ``ovlfoo 2 x``, "ovlfoo 2 x"),
276         ("field selection", ``r.fld2``, "r.fld2"),
277         ("field sel. for fn type", ``r.fld1 x``, "r.fld1 x"),
278         ("singleton field update",
279          ``r with fld1 := (\x. T)``, "r with fld1 := (\\x. T)"),
280         ("multi-field update", ``r with <| fld2 := 3; fld1 := x |>``,
281          "r with <|fld2 := 3; fld1 := x|>"),
282         ("big field selection", ``r.fld3``, "r.fld3"),
283         ("big field selection (simped)", s ``r.fld3``, "r.fld3"),
284         ("big field selection (fn type)", ``r.fld7``, "r.fld7"),
285         ("big field selection (fn type, simped)", s ``r.fld7``, "r.fld7"),
286         ("big singleton update", ``r with fld3 := 4``, "r with fld3 := 4"),
287         ("big singleton update (simped)", s ``r with fld3 := 4``,
288          "r with fld3 := 4"),
289         ("big multi-update", ``r with <| fld3 := 6; fld9 := (T,6)|>``,
290          "r with <|fld3 := 6; fld9 := (T,6)|>"),
291         ("big multi-update (simped)",
292          s ``r with <| fld3 := 6; fld9 := (T,6)|>``,
293          "r with <|fld3 := 6; fld9 := (T,6)|>"),
294         ("overloaded bare var.fld", ``ID``, "ID"),
295         ("overloaded var.fld with args", ``inv x``, "inv x"),
296         ("poly simple upd", ``r : ('c,num) polyrcd with pfld1 := K 1``,
297            "r with pfld1 := K 1"),
298         ("poly simple seln", ``(r : ('c,'d)polyrcd).pfld1``, "r.pfld1"),
299         ("bare ('a,'b) polyrcd_pfld1",
300             ``polyrcd_pfld1 : ('a,'b) polyrcd -> 'a ms``, "polyrcd_pfld1"),
301         ("bare ('a,'b) polyrcd_pfld1_fupd",
302            ``polyrcd_pfld1_fupd :
303                ('a ms -> 'a ms) -> ('a,'b) polyrcd -> ('a,'b) polyrcd``,
304            "pfld1_fupd"),
305         ("bare (num,num) polyrcd_pfld1",
306            ``polyrcd_pfld1 : (num,num) polyrcd -> num ms``, "polyrcd_pfld1"),
307         ("bare ('c,'d) polyrcd_pfld1",
308            ``polyrcd_pfld1 : ('c,'d) polyrcd -> 'c ms``, "polyrcd_pfld1"),
309         ("bare ('c,'d) polyrcd_pfld3",
310            ``polyrcd_pfld3 : ('c,'d) polyrcd -> num``, "polyrcd_pfld3"),
311         ("bare ('c,'d) polyrcd_pfld1_fupd",
312            ``polyrcd_pfld1_fupd :
313                ('c ms -> 'c ms) -> ('c,'d) polyrcd -> ('c,'d) polyrcd``,
314            "pfld1_fupd"),
315         ("one-arg polyrcd_pfld1_fupd",
316            ``polyrcd_pfld1_fupd f : ('a,'b) polyrcd -> ('a,'b) polyrcd``,
317            "pfld1_fupd f")
318         ]
319
320val _ = with_flag (Globals.linewidth, 40) pptest
321                  ("multiline record 1",
322                   ``<|fld1 := a very long expression indeed ;
323                       fld2 := also a long expression|>``,
324                  "<|fld1 := a very long expression indeed;\n\
325                  \  fld2 := also a long expression|>")
326
327val _ = with_flag (Globals.linewidth, 40) pptest
328                  ("multiline record 2",
329                   ``<|fld3 := a very long expression indeed ;
330                       fld4 := also a long expression|>``,
331                  "<|fld3 := a very long expression indeed;\n\
332                  \  fld4 := also a long expression|>")
333
334val _ = app convtest [
335      ("EVAL field K-composition", computeLib.CBV_CONV computeLib.the_compset,
336       ``<| fld1 updated_by K t1 o K t2 |>``,
337       ``<| fld1 := t1 |>``)
338    ]
339
340
341val _ = Feedback.emit_MESG := false
342
343(* a test for Hol_defn that requires a datatype: *)
344(* mutrec defs with sums *)
345val _ = tprint "Mutrec defn with sums"
346val _ = Hol_datatype `foo2 = F1 of unit | F2 of foo2 + num`
347val _ = Defn.Hol_defn "foo"`
348(foo1 (F1 ()) = F1 ()) /\
349(foo1 (F2 sf) = F2 (foo2 sf)) /\
350(foo2 (INR n) = INL (F1 ())) /\
351(foo2 (INL f) = INL (foo1 f))` handle HOL_ERR _ => die "FAILED!"
352val _ = OK()
353
354val _ = tprint "Non-recursive num"
355val _ = Datatype.Datatype `num = C10 num$num | C11 num | C12 scratch$num`;
356val (d,r) = dom_rng (type_of ``C10``)
357val _ = Type.compare(d, numSyntax.num) = EQUAL orelse die "FAILED!"
358val (d,r) = dom_rng (type_of ``C11``)
359val _ = Type.compare(d, numSyntax.num) <> EQUAL orelse die "FAILED!"
360val (d,r) = dom_rng (type_of ``C12``)
361val _ = Type.compare(d, numSyntax.num) <> EQUAL orelse die "FAILED!"
362val _ = OK()
363
364val _ = tprint "Datatype and antiquote (should be quick)"
365val num = numSyntax.num
366val _ = Datatype.Datatype `dtypeAQ = C13 ^num bool | C14 (^num -> bool)`
367val _ = OK()
368
369val _ = tprint "Records with polymorphic fields 1"
370val _ = (``polyrcd_pfld1_fupd :
371             ('c ms -> 'e ms) -> ('c,'d) polyrcd -> ('e,'d)polyrcd``;
372         OK(); true)
373        orelse die "FAILED!"
374
375val _ = tprint "Records with polymorphic fields 2"
376val _ = (``polyrcd2_p2fld1_fupd :
377             ('a ms -> 'a ms) -> ('a,'b) polyrcd2 -> ('a,'b)polyrcd2``;
378         OK(); true)
379        orelse die "FAILED!"
380
381val _ = tprint "Records with polymorphic fields 3"
382val _ = (``polyrcd2_p2fld2_fupd :
383             (('a # 'b -> bool) -> ('a # 'c -> bool)) ->
384             ('a,'b) polyrcd2 -> ('a,'c)polyrcd2``;
385         OK(); true)
386        orelse die "FAILED!"
387
388val _ = tprint "Records with polymorphic fields 4"
389val _ =
390  case Lib.total (trace("show_typecheck_errors", 0) Parse.Term)
391       `polyrcd2_p2fld1_fupd :
392             ('a ms -> 'b ms) -> ('a,'c) polyrcd2 -> ('b,'c)polyrcd2`
393  of
394    NONE => OK()
395  | _ => die "FAILED!";
396
397
398val _ = tprint "Testing overriding calls in mutual recursive style";
399val _ = quiet_warnings (fn () =>
400           (Datatype`a2 = A num ; b = B 'a`;
401            Datatype`a2 = A num ; b = B 'a `;
402            Datatype `foo = Foo`;
403            Datatype`a = A ; b = B `;
404            Datatype`a2 = A ; b = B `;
405            Datatype`a2 = A ; b2 = B `;
406            Datatype `foo = Foo`)) () handle _ => die "FAILED!"
407val _ = OK()
408
409val _ = tprint "Test for prove_case_elim_thm (20171201)";
410val _ = quiet_warnings (fn () =>
411          Datatype `pcet20171201 = C20171201 num | D20171201 (num -> bool)`) ()
412          handle _ => die "FAILED!"
413val _ = OK()
414
415val _ = Process.exit Process.success;
416