1(*---------------------------------------------------------------------------* 2 * Define a HOL datatype and derive a bunch of theorems from it. Return * 3 * these encapsulated in an element of the TypeBasePure.tyinfo type. * 4 * * 5 * Examples of use: * 6 * * 7 * local open Datatype * 8 * in * 9 * val term_ty_def = * 10 * Hol_datatype `term = Var of 'a * 11 * | Const of 'a * 12 * | App of term => term` * 13 * * 14 * val subst_ty_def = * 15 * Hol_datatype `subst = Fail | Subst of ('a#'a term) list` * 16 * end; * 17 * * 18 * * 19 * Returns a great deal of information about the datatype: theorems, * 20 * definition of case-constant, induction tactics, etc. * 21 * * 22 * Side-effects: it adds the definition of the type and the definition * 23 * of the case-construct to the current theory. * 24 * * 25 * Notice that, at least using the current mechanism for defining types, * 26 * a great many theories get loaded in: numbers, lists, trees, etc. when * 27 * this module is loaded. If your formalization doesn't want to have these * 28 * as parents, then TypeBasePure.mk_datatype_info can be used directly. * 29 *---------------------------------------------------------------------------*) 30 31(* Interactive: 32 33 app load ["ind_types", "ParseDatatype", "RecordType"]; 34 open Rsyntax ParseDatatype; 35*) 36 37structure Datatype :> Datatype = 38struct 39 40open HolKernel Parse boolLib Prim_rec ParseDatatype DataSize 41local open ind_typeTheory in end; 42 43type hol_type = Type.hol_type 44type thm = Thm.thm 45type tyinfo = TypeBasePure.tyinfo 46type typeBase = TypeBasePure.typeBase 47type 'a quotation = 'a Portable.frag list 48type AST = ParseDatatype.AST; 49 50type record_rw_names = string list 51 52type field_name = string 53type field_names = string list 54type constructor = string * hol_type list 55 56(*--------------------------------------------------------------------------- 57 A tyspec is a type specification. The first component is a type 58 variable whose name (less the leading quote) is the name of the new 59 type. Each such is accompanied by a list of constructor specifications. 60 Such a spec. is a string (the constructor name) and a list of types that 61 are the arguments of that constructor. Recursive occurrences of the 62 types are marked by occurrences of the corresponding type variables. 63 ---------------------------------------------------------------------------*) 64 65type tyspec = hol_type * constructor list 66 67 68(* Fix the grammar used by this file *) 69val ambient_grammars = Parse.current_grammars(); 70val _ = Parse.temp_set_grammars arithmeticTheory.arithmetic_grammars; 71 72val ERR = mk_HOL_ERR "Datatype"; 73 74val empty_stringset = HOLset.empty String.compare 75 76(*--------------------------------------------------------------------------- 77 Basic datatype definition support 78 ---------------------------------------------------------------------------*) 79 80val define_type = ind_types.define_type; 81 82(*---------------------------------------------------------------------------*) 83(* Generate a string that, when evaluated as ML, will create the given type. *) 84(* Copied from TheoryPP.sml. Parameterized by strings representing code that *) 85(* builds type variables or compound types. *) 86(*---------------------------------------------------------------------------*) 87 88val extern_type = TheoryPP.pp_type 89 90fun with_parens pfn x = 91 let open Portable PP 92 in block CONSISTENT 1 [add_string "(", pfn x, add_string ")"] 93 end 94 95fun pp_fields fields = 96 let open Portable PP 97 fun pp_field (s,ty) = 98 block CONSISTENT 0 [ 99 add_string ("("^Lib.quote s), 100 add_string ",", 101 extern_type "U" "T" ty, 102 add_string ")" 103 ] 104 in 105 block CONSISTENT 0 [ 106 add_string "let fun T s t A = mk_thy_type{Thy=t,Tyop=s,Args=A}", NL, 107 add_string " val U = mk_vartype", NL, 108 add_string "in", NL, 109 block CONSISTENT 1 [ 110 add_string "[", 111 block INCONSISTENT 0 ( 112 pr_list pp_field [add_string ",", add_break (1,0)] fields 113 ), 114 add_string "]" 115 ], 116 add_string "end" 117 ] 118 end 119 120 121(*--------------------------------------------------------------------------- 122 Support for quoted input 123 ---------------------------------------------------------------------------*) 124 125local fun find_dup [] = NONE 126 | find_dup [x] = NONE 127 | find_dup (x::y::xs) = if x=y then SOME x else find_dup (y::xs) 128in 129val duplicate_names = find_dup o Listsort.sort String.compare 130end; 131 132fun prim_mk_type (Thy, Tyop) = let 133 val arity = valOf (Type.op_arity {Thy = Thy, Tyop = Tyop}) 134in 135 Type.mk_thy_type {Thy = Thy, Tyop = Tyop, 136 Args = List.tabulate (arity, fn n => Type.alpha)} 137end 138 139val mk_recordtype_constructor = RecordType.mk_recordtype_constructor 140 141fun check_constrs_unique_in_theory asts = let 142 fun cnames (s, Record _) = [(s,mk_recordtype_constructor s)] 143 | cnames (s, Constructors l) = map (fn s' => (s, #1 s')) l 144 val newtypes = map #1 asts 145 val constrs = List.concat (map cnames asts) 146 val current_types = set_diff (map fst (types "-")) newtypes 147 fun current_constructors (tyname, fm) = let 148 val tys_cons = 149 TypeBase.constructors_of (prim_mk_type (current_theory(), tyname)) 150 handle HOL_ERR _ => [] 151 fun foldthis (c,fm) = 152 if uptodate_term c then 153 Binarymap.insert(fm, #Name (dest_thy_const c), tyname) 154 else fm 155 in 156 foldl foldthis fm tys_cons 157 end 158 val current_constructors = 159 List.foldl current_constructors (Binarymap.mkDict String.compare) 160 current_types 161 fun calculate_intersection ((tyname, conname), acc) = 162 case Binarymap.peek(current_constructors, conname) of 163 NONE => acc 164 | SOME ty' => (tyname, conname, ty') :: acc 165 val common = List.rev (foldl calculate_intersection [] constrs) 166 167 fun warn (newty, conname, oldty) = 168 HOL_WARNING "Datatype" "Hol_datatype" 169 ("Constructor \""^conname^"\" in new type \""^newty^"\"\n\ 170 \ duplicates constructor in type \""^oldty^"\", \ 171 \which will be\n\ 172 \ invalidated by this definition") 173in 174 app warn common 175end 176 177 178local fun tyname_as_tyvar n = mk_vartype ("'" ^ n) 179 fun stage1 (s,Constructors l) = (s,l) 180 | stage1 (s,Record fields) = (s,[(mk_recordtype_constructor s, 181 map snd fields)]) 182 fun check_fields (s,Record fields) = 183 (case duplicate_names (map fst fields) 184 of NONE => () 185 | SOME n => raise ERR "check_fields" ("Duplicate field name: "^n)) 186 | check_fields _ = () 187 fun cnames (s,Record _) A = s::A 188 | cnames (_,Constructors l) A = map fst l @ A 189 fun check_constrs asts = 190 case duplicate_names (itlist cnames asts []) 191 of NONE => () 192 | SOME n => raise ERR "check_constrs" 193 ("Duplicate constructor name: "^n) 194in 195fun to_tyspecs ASTs = 196 let val _ = List.app check_fields ASTs 197 val _ = check_constrs ASTs 198 val _ = check_constrs_unique_in_theory ASTs 199 val asts = map stage1 ASTs 200 val new_type_names = map #1 asts 201 fun mk_hol_ty (dAQ ty) = ty 202 | mk_hol_ty (dVartype s) = mk_vartype s 203 | mk_hol_ty (dTyop{Tyop=s, Args, Thy}) = 204 if Lib.mem s new_type_names andalso 205 (Thy = NONE orelse Thy = SOME (current_theory())) 206 then if null Args then tyname_as_tyvar s 207 else raise ERR "to_tyspecs" 208 ("Omit arguments to new type:"^Lib.quote s) 209 else 210 case Thy of 211 NONE => mk_type(s, map mk_hol_ty Args) 212 | SOME t => mk_thy_type {Tyop = s, Thy = t, 213 Args = map mk_hol_ty Args} 214 fun mk_hol_type pty = let 215 val ty = mk_hol_ty pty 216 in 217 if Theory.uptodate_type ty then ty 218 else let val tyname = #1 (dest_type ty) 219 in raise ERR "to_tyspecs" (tyname^" not up-to-date") 220 end 221 end 222 223 fun constructor (cname, ptys) = (cname, map mk_hol_type ptys) 224 in 225 map (tyname_as_tyvar##map constructor) asts 226 end 227end; 228 229fun tyspecs_of tyg q = to_tyspecs (ParseDatatype.parse tyg q); 230 231val new_asts_datatype = define_type o to_tyspecs; 232fun new_datatype q = 233 new_asts_datatype (ParseDatatype.parse (type_grammar()) q); 234 235 236(*---------------------------------------------------------------------------*) 237(* Determine if a parsed type spec is calling for an enumerated type. *) 238(* Returns false if there is more than one type called for, because an *) 239(* earlier sorting process will ensure that enumerated types are presented *) 240(* singly. *) 241(*---------------------------------------------------------------------------*) 242 243fun is_enum_type_spec astl = 244 case astl of 245 [(ty,Constructors constrs)] => List.all (null o #2) constrs 246 (* recall that constrs is a list of constr-name - type arguments pairs *) 247 | _ => false 248 249 250(*---------------------------------------------------------------------------*) 251(* Build a tyinfo list for an enumerated type. *) 252(*---------------------------------------------------------------------------*) 253 254fun build_enum_tyinfo (tyname, ast) = 255 let open EnumType 256 in case ast 257 of Constructors clist => 258 let val constructors = map #1 clist 259 in case duplicate_names constructors 260 of NONE => (enum_type_to_tyinfo (tyname, constructors)) 261 | SOME s => raise ERR "build_enum"("Duplicate constructor name: "^s) 262 end 263 | otherwise => raise ERR "build_enum_tyinfo" "Should never happen" 264end 265 266fun build_enum_tyinfos astl = let 267 val _ = check_constrs_unique_in_theory astl 268in 269 map build_enum_tyinfo astl 270end 271 272 273(*--------------------------------------------------------------------------- 274 Returns a list of tyinfo thingies 275 ---------------------------------------------------------------------------*) 276 277local 278 fun insert_size {def, const_tyopl} tyinfol = 279 case tyinfol 280 of [] => raise ERR "build_tyinfos" "empty tyinfo list" 281 | tyinfo::rst => 282 let val first_tyname = TypeBasePure.ty_name_of tyinfo 283 fun insert_size info size_eqs = 284 let val tyname = TypeBasePure.ty_name_of info 285 in case assoc2 tyname const_tyopl 286 of SOME(c,tyop) => TypeBasePure.put_size(c,size_eqs) info 287 | NONE => (HOL_MESG 288 ("Can't find size constant for"^(snd tyname)) 289 ; raise ERR "build_tyinfos" "") 290 end 291 in 292 insert_size tyinfo (TypeBasePure.ORIG def) 293 :: map (C insert_size (TypeBasePure.COPY (first_tyname,def))) rst 294 end 295 handle HOL_ERR _ => tyinfol 296in 297 298fun build_tyinfos db {induction,recursion} = 299 let val case_defs = Prim_rec.define_case_constant recursion 300 val tyinfol = TypeBasePure.gen_datatype_info 301 {ax=recursion, ind=induction, case_defs=case_defs} 302 in 303 case define_size recursion db 304 of NONE => (HOL_MESG "Couldn't define size function"; tyinfol) 305 | SOME s => insert_size s tyinfol 306 end 307end; 308 309(* ---------------------------------------------------------------------- 310 Topological sort of datatype declarations so that the system can 311 automatically separate out those types that aren't recursively linked 312 ---------------------------------------------------------------------- *) 313 314fun pretype_ops acc ptysl = 315 (* find all of the operator names in a list of pretype lists *) 316 case ptysl of 317 [] => acc 318 | (ptys :: rest) => let 319 in 320 case ptys of 321 [] => pretype_ops acc rest 322 | (pty :: more_ptys) => let 323 in 324 case pty of 325 dTyop {Args, Thy, Tyop} => 326 pretype_ops (HOLset.add(acc, Tyop)) (Args :: more_ptys :: rest) 327 | _ => pretype_ops acc (more_ptys :: rest) 328 end 329 end 330 331fun build_reference_matrix astl = let 332 (* turns a astl into an adjacency matrix, position (n,m) is true if 333 ast n refers to ast m. *) 334 val newnames = map #1 astl 335 val n = length newnames 336 exception NoDex 337 fun dex s [] = raise NoDex 338 | dex s (h::t) = if s = h then 0 else 1 + dex s t 339 val array = Array2.array(n,n,false) 340 fun refers_to ast = 341 case ast of 342 Record flds => let 343 fun foldthis ((_, pty), acc) = pretype_ops acc [[pty]] 344 in 345 foldl foldthis (HOLset.empty String.compare) flds 346 end 347 | Constructors cs => let 348 fun foldthis ((_, ptys), acc) = pretype_ops acc [ptys] 349 in 350 foldl foldthis (HOLset.empty String.compare) cs 351 end 352 fun record_refs (tyname, ast) = let 353 val i = dex tyname newnames 354 fun appthis s = Array2.update(array, i, dex s newnames, true) 355 handle NoDex => () 356 in 357 HOLset.app appthis (refers_to ast) 358 end 359in 360 app record_refs astl ; 361 array 362end 363 364fun calculate_transitive_closure a = let 365 (* updates a 2D array so that it represents the transitive closure of the 366 relation it used to represent O(n^3) *) 367 open Array2 368 nonfix via 369 val n = nCols a 370 fun check i = 371 modifyi RowMajor 372 (fn (j,k,v) => v orelse (sub(a,j,i) andalso sub(a,i,k))) 373 { base = a, row = 0, col = 0, nrows = NONE, ncols = NONE} 374 fun via i = 375 if i = n then () 376 else (check i ; via (i + 1)) 377in 378 via 0 379end 380 381fun topo_sort a = let 382 (* return the elements of the graph in a topological order, 383 treating elements in loops as equivalent. Function returns a list of 384 lists of integers, where the integers index the nodes. Lists are 385 never empty. If not singleton, this represents a loop *) 386 open Array2 387 val n = nRows a 388 fun findloops () = let 389 (* return a list of lists, not sorted topologically, but which 390 encompasses loop structure *) 391 val done = Array.array(n, false) 392 fun check_row i = let 393 fun findothers acc j = 394 if j = n then List.rev acc 395 else if sub(a, i, j) andalso sub(a, j, i) andalso i <> j then 396 (Array.update(done, j, true); 397 findothers (j::acc) (j + 1)) 398 else findothers acc (j + 1) 399 in 400 findothers [i] 0 401 end 402 fun check_rows i = 403 if i = n then [] 404 else if Array.sub(done, i) then check_rows (i + 1) 405 else (check_row i :: check_rows (i + 1)) 406 in 407 check_rows 0 408 end 409 val blocks = findloops() 410 fun zero_column j = 411 modifyi ColMajor (fn _ => false) 412 {base = a, col = j, row = 0, nrows = NONE, ncols = SOME 1} 413 fun pull_out_next bs = 414 case bs of 415 [] => raise Fail "Can't happen" 416 | [b] => (List.app zero_column b; (b, [])) 417 | b :: rest => let 418 val i = hd b 419 fun check j = 420 (* j and later indices are ok iff : *) 421 j = n orelse 422 ((not (sub(a, i, j)) orelse mem j b) andalso 423 check (j + 1)) 424 in 425 if check 0 then (List.app zero_column b; (b, rest)) 426 else let 427 val (best, rest') = pull_out_next rest 428 in 429 (best, (b :: rest')) 430 end 431 end 432 fun pull_out_oks blist = 433 case blist of 434 [] => [] 435 | _ => let 436 val (b, rest) = pull_out_next blist 437 in 438 b :: pull_out_oks rest 439 end 440in 441 pull_out_oks blocks 442end 443 444fun sort_astl astl = let 445 val adjs = build_reference_matrix astl 446 val _ = calculate_transitive_closure adjs 447 val sorted = topo_sort adjs 448 fun dex_to_astl i = List.nth(astl, i) 449in 450 map (map dex_to_astl) sorted 451end 452 453 454(*---------------------------------------------------------------------------*) 455(* Do the hard work of type definition *) 456(* *) 457(* [tyis] is a list of tyinfos coupled with strings representing how to *) 458(* recreate them (strings which when eval-ed will be a function of type *) 459(* tyinfo -> tyinfo; these functions will be applied to the basic tyinfo *) 460(* created for the record type). *) 461(* *) 462(* [thminfo_list] is of type *) 463(* (string * (string * thm) list * (string * hol_type) list) list, *) 464(* *) 465(* basically an association list from type names to extra stuff. *) 466(* The second component of each triple is theorems which need to be *) 467(* added to the corresponding tyinfos, and they are accompanied by *) 468(* the names under which they have been stored in the theory *) 469(* segment. The third component is field information for that type. *) 470(* *) 471(* [persistp] is true iff we need to adjoin stuff to make the change *) 472(* persistent. *) 473(*---------------------------------------------------------------------------*) 474 475val tyi_compare = 476 inv_img_cmp TypeBasePure.ty_name_of 477 (Lib.pair_compare(String.compare,String.compare)) 478 479fun alist_comp ((s1,_,_), (s2,_,_)) = String.compare(s1,s2); 480 481fun augment_tyinfos tyis thminfo_list = let 482 val tyis = Listsort.sort tyi_compare tyis 483 val thminfo_list = Listsort.sort alist_comp thminfo_list 484 type thmdata = (string * thm) list 485 type flddata = (string * TypeBase.rcd_fieldinfo) list * thm list * thm list 486 fun merge acc tyis (thmi_list : (string * thmdata * flddata) list) = 487 case (tyis, thmi_list) of 488 ([], _ :: _ ) => raise Fail "Datatype.sml: invariant failure 101" 489 | ([],[]) => acc 490 | (_, []) => tyis @ acc 491 | (tyi::tyi_rest, (th_s, thms, flds)::thmi_rest) => let 492 in 493 case String.compare (snd(TypeBasePure.ty_name_of tyi), th_s) of 494 LESS => merge (tyi::acc) tyi_rest thmi_list 495 | GREATER => raise Fail "Datatype.sml: invariant failure 102" 496 | EQUAL => let 497 val tyi' = RecordType.update_tyinfo (SOME flds) (map #2 thms) tyi 498 in 499 merge (tyi' :: acc) tyi_rest thmi_rest 500 end 501 end 502in 503 merge [] tyis thminfo_list 504end 505 506 507local 508 fun add_record_facts (tyinfo, NONE) = tyinfo 509 | add_record_facts (tyinfo, SOME fields) = 510 RecordType.prove_recordtype_thms (tyinfo, fields) 511 fun field_names_of (_,Record l) = SOME (map fst l) 512 | field_names_of _ = NONE 513 fun astpty_map f ast = let 514 open ParseDatatype 515 in 516 case ast of 517 Constructors clist => 518 Constructors (map (fn (s, ptys) => (s, map f ptys)) clist) 519 | Record flds => Record (map (fn (s, pty) => (s, f pty)) flds) 520 end 521 fun reform_tyops prevtypes pty = let 522 open ParseDatatype 523 in 524 case pty of 525 dTyop{Tyop, Thy, Args} => let 526 in 527 case (Lib.assoc1 Tyop prevtypes, Args) of 528 (SOME (_, strset), []) => let 529 val thytyop = 530 case Thy of 531 NONE => hd (Type.decls Tyop) 532 | SOME s => {Thy = s, Tyop = Tyop} 533 val arity = valOf (Type.op_arity thytyop) 534 val _ = arity = HOLset.numItems strset orelse 535 raise ERR "reform_tyops" (Tyop ^ " has unexpected arity") 536 in 537 dTyop{Tyop = Tyop, Thy = Thy, 538 Args = map dVartype (HOLset.listItems strset)} 539 end 540 | _ => dTyop{Tyop = Tyop, Thy = Thy, 541 Args = map (reform_tyops prevtypes) Args} 542 end 543 | _ => pty 544 end 545 546 fun insert_tyarguments prevtypes astl = 547 map (fn (s, dt) => (s, astpty_map (reform_tyops prevtypes) dt)) astl 548 549 fun getfldinfo bigrecinfo = let 550 fun mapthis (s, l) = (s, map (I ## ParseDatatype.pretypeToType) l) 551 in 552 map mapthis bigrecinfo 553 end 554 fun merge_alists alist1 alist2 = let 555 fun recurse acc alist1 alist2 = 556 case (alist1, alist2) of 557 ([], []) => List.rev acc 558 | (_, []) => List.rev acc @ map (fn (s,d) => (s, d, ([],[],[]))) alist1 559 | ([], _) => List.rev acc @ map (fn (s,d) => (s, [],(d,[],[]))) alist2 560 | ((a1k, a1d)::a1s, (a2k, a2d)::a2s) => 561 case String.compare (a1k, a2k) of 562 LESS => recurse ((a1k,a1d,([],[],[])) :: acc) a1s alist2 563 | EQUAL => recurse ((a1k,a1d,(a2d,[],[])) :: acc) a1s a2s 564 | GREATER => recurse ((a2k,[],(a2d,[],[])) :: acc) alist1 a2s 565 fun alistcomp ((s1, d1), (s2, d2)) = String.compare(s1, s2) 566 in 567 recurse [] (Listsort.sort alistcomp alist1) (Listsort.sort alistcomp alist2) 568 end 569 570in 571(*---------------------------------------------------------------------------*) 572(* precondition: astl has been sorted, so that, for example, those *) 573(* ast elements not referring to any others will be present only as *) 574(* singleton lists *) 575(*---------------------------------------------------------------------------*) 576 577fun prim_define_type_from_astl prevtypes f db astl0 = let 578 val astl = insert_tyarguments prevtypes astl0 579in 580 if is_enum_type_spec astl then (db, build_enum_tyinfos astl) 581 else (db, 582 map add_record_facts 583 (zip (build_tyinfos db (new_asts_datatype astl)) 584 (map field_names_of astl))) 585end (* let *) 586end (* local *) 587 588 589fun find_vartypes (pty, acc) = 590 let open ParseDatatype 591 in 592 case pty of 593 dVartype s => HOLset.add(acc, s) 594 | dAQ ty => List.foldl (fn (ty, acc) => HOLset.add(acc, dest_vartype ty)) 595 acc (Type.type_vars ty) 596 | dTyop {Args, ...} => List.foldl find_vartypes acc Args 597 end 598 599fun dtForm_vartypes (dtf, acc) = 600 case dtf of 601 Constructors clist => List.foldl (fn ((s, ptyl), acc) => 602 List.foldl find_vartypes acc ptyl) 603 acc clist 604 | Record fldlist => List.foldl 605 (fn ((s, pty), acc) => find_vartypes (pty, acc)) 606 acc fldlist 607 608 609(*---------------------------------------------------------------------------*) 610(* prevtypes below is an association list mapping the names of types *) 611(* previously defined in this "session" to the list of type variables that *) 612(* occurred on the RHS of the type definitions. *) 613(*---------------------------------------------------------------------------*) 614 615fun define_type_from_astl prevtypes db astl = let 616 val sorted_astll = sort_astl astl 617 val f = define_type_from_astl 618 fun handle_astl (astl, (prevtypes, db, tyinfo_acc)) = let 619 val (db, new_tyinfos) = prim_define_type_from_astl prevtypes f db astl 620 fun addtyi (tyi, db) = TypeBasePure.insert db tyi 621 val alltyvars = 622 List.foldl (fn ((_, dtf), acc) => dtForm_vartypes(dtf, acc)) 623 empty_stringset 624 astl 625 in 626 (prevtypes @ map (fn (s, dtf) => (s, alltyvars)) astl, 627 List.foldl addtyi db new_tyinfos, 628 tyinfo_acc @ new_tyinfos) 629 end 630 val (_,db,tyinfos) = List.foldl handle_astl (prevtypes, db, []) sorted_astll 631in 632 (db, tyinfos) 633end 634 635 636fun primHol_datatype db astl = define_type_from_astl [] db astl; 637 638(*--------------------------------------------------------------------------- 639 640 For a datatype named "ty", Hol_datatype stores the following 641 theorems in the current theory, and in TypeBase.theTypeBase. (Some 642 other definitions and theorems used in defining the datatype are 643 also stored in the current theory, but we will ignore them.) 644 645 1. ty (* datatype characterization theorem *) 646 2. ty_case_def (* case_expression defn *) 647 3. ty_case_cong (* congruence theorem for case expression *) 648 4. ty_induction (* induction thm for datatype *) 649 5. ty_nchotomy (* case completeness *) 650 6. ty_size_def (* size of type defn *) 651 7. ty_to_bool_def (* encoder for the type *) 652 8. lift (* lifter (ML -> HOL) for the type *) 653 9. one_one (* one-one-ness of the constructors *) 654 10. distinct (* distinctness of the constructors *) 655 11. fields (* fields, if it is a record type *) 656 12. accessors (* accessors, if it is a record type *) 657 13. updates (* update fns, if it is a record type *) 658 659 We also adjoin some ML to the current theory so that if the theory 660 gets exported and loaded in a later session, these "datatype" 661 theorems are loaded automatically into theTypeBase. 662 663 ---------------------------------------------------------------------------*) 664 665fun persistent_tyinfo tyinfos = 666 let 667 fun ovl tyi = Parse.overload_on ("case", TypeBasePure.case_const_of tyi) 668 fun save_thms tyi = 669 let 670 open TypeBasePure 671 val tname = snd (ty_name_of tyi) 672 fun name s = tname ^ s 673 fun optsave nm thopt = 674 case thopt of NONE => () | SOME th => ignore (save_thm(name nm, th)) 675 in 676 optsave "_11" (one_one_of tyi); 677 optsave "_distinct" (distinct_of tyi); 678 save_thm(name "_nchotomy", nchotomy_of tyi); 679 save_thm(name "_Axiom", axiom_of tyi); 680 save_thm(name "_induction", induction_of tyi); 681 save_thm(name "_case_cong", case_cong_of tyi); 682 save_thm(name "_case_eq", case_eq_of tyi); 683 () 684 end 685 in 686 TypeBase.export tyinfos; 687 app save_thms tyinfos; 688 app ovl tyinfos; 689 app computeLib.write_datatype_info tyinfos 690 end; 691 692(*---------------------------------------------------------------------------*) 693(* Construct trivial theorem from which structure of original datatype can *) 694(* be recovered. *) 695(*---------------------------------------------------------------------------*) 696 697fun mk_datatype_presentation thy tyspecl = 698 let open ParseDatatype 699 fun mkc (n,_) = prim_mk_const{Name=n,Thy=thy} 700 fun type_dec (tyname,Constructors dforms) = 701 let val constrs = map mkc dforms 702 val tyn_var = mk_var(tyname,list_mk_fun(map type_of constrs,bool)) 703 in 704 list_mk_comb(tyn_var,constrs) 705 end 706 | type_dec (tyname,Record fields) = 707 let 708 val hdc = 709 prim_mk_const{Name = tyname ^ "_" ^ #1 (hd fields), Thy = thy} 710 fun fieldvar (n, _) = let 711 val c = prim_mk_const{Name = tyname ^ "_" ^ n, Thy = thy} 712 val (_, ty) = dom_rng (type_of c) 713 in 714 mk_var(n, ty) 715 end 716 val fvars = map fieldvar fields 717 val tyn_var = mk_var(tyname,hdc |> type_of |> dom_rng |> #1) 718 val record_var = 719 mk_var("record", 720 list_mk_fun(type_of tyn_var::map type_of fvars,bool)) 721 in 722 list_mk_comb(record_var,tyn_var::fvars) 723 end 724 in 725 (fst(hd tyspecl),list_mk_conj (map type_dec tyspecl)) 726 end 727 728fun datatype_thm (n,M) = save_thm 729 ("datatype_"^n, 730 EQT_ELIM (ISPEC M DATATYPE_TAG_THM)); 731 732fun astHol_datatype astl = 733 let 734 val (_,tyinfos) = primHol_datatype (TypeBase.theTypeBase()) astl 735 val _ = Theory.scrub() 736 val _ = datatype_thm (mk_datatype_presentation (current_theory()) astl) 737 val tynames = map TypeBasePure.ty_name_of tyinfos 738 val tynames = map (Lib.quote o snd) tynames 739 val message = "Defined type"^(if length tynames > 1 then "s" else "")^ 740 ": "^String.concat (Lib.commafy tynames) 741 in 742 persistent_tyinfo tyinfos; 743 HOL_MESG message 744 end handle e as HOL_ERR _ => Raise (wrap_exn "Datatype" "Hol_datatype" e); 745 746fun Hol_datatype q = astHol_datatype (ParseDatatype.parse (type_grammar()) q) 747fun Datatype q = astHol_datatype (ParseDatatype.hparse (type_grammar()) q) 748 749val _ = Parse.temp_set_grammars ambient_grammars 750 751end 752