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