1signature TypeBasePure = 2sig 3 type hol_type = Type.hol_type 4 type term = Term.term 5 type thm = Thm.thm 6 7 type tyinfo 8 type typeBase 9 type simpfrag = simpfrag.simpfrag 10 type rcd_fieldinfo = {ty: hol_type, accessor: term, fupd : term} 11 12 13 datatype shared_thm = ORIG of thm 14 | COPY of (string * string) * thm 15 type mk_datatype_record = 16 {ax : shared_thm, 17 induction : shared_thm, 18 case_def : thm, 19 case_cong : thm, 20 case_eq : thm, 21 nchotomy : thm, 22 size : (term * shared_thm) option, 23 encode : (term * shared_thm) option, 24 lift : term option, 25 one_one : thm option, 26 distinct : thm option, 27 fields : (string * rcd_fieldinfo) list, 28 accessors : thm list, 29 updates : thm list, 30 destructors : thm list, 31 recognizers : thm list} 32 33 val mk_datatype_info_no_simpls : mk_datatype_record -> tyinfo 34 val gen_std_rewrs : tyinfo -> thm list 35 val add_std_simpls : tyinfo -> tyinfo 36 val mk_datatype_info : mk_datatype_record -> tyinfo 37 38 val gen_datatype_info : {ax:thm,ind:thm,case_defs:thm list} -> tyinfo list 39 40 val mk_nondatatype_info 41 : hol_type * 42 {nchotomy : thm option, 43 induction : thm option, 44 size : (term * thm) option, 45 encode : (term * thm) option} -> tyinfo 46 47 val pp_tyinfo : tyinfo Parse.pprinter 48 49 val ty_of : tyinfo -> hol_type 50 val ty_name_of : tyinfo -> string * string 51 52 val axiom_of : tyinfo -> thm 53 val induction_of : tyinfo -> thm 54 val constructors_of : tyinfo -> term list 55 val destructors_of : tyinfo -> thm list 56 val recognizers_of : tyinfo -> thm list 57 val case_const_of : tyinfo -> term 58 val case_cong_of : tyinfo -> thm 59 val case_def_of : tyinfo -> thm 60 val case_eq_of : tyinfo -> thm 61 val nchotomy_of : tyinfo -> thm 62 val distinct_of : tyinfo -> thm option 63 val one_one_of : tyinfo -> thm option 64 val fields_of : tyinfo -> (string * rcd_fieldinfo) list 65 val accessors_of : tyinfo -> thm list 66 val updates_of : tyinfo -> thm list 67 val simpls_of : tyinfo -> simpfrag 68 val size_of : tyinfo -> (term * thm) option 69 val encode_of : tyinfo -> (term * thm) option 70 val lift_of : tyinfo -> term option 71 val extra_of : tyinfo -> ThyDataSexp.t list 72 73 val axiom_of0 : tyinfo -> shared_thm 74 val induction_of0 : tyinfo -> shared_thm 75 val size_of0 : tyinfo -> (term * shared_thm) option 76 val encode_of0 : tyinfo -> (term * shared_thm) option 77 78 val put_nchotomy : thm -> tyinfo -> tyinfo 79 val put_simpls : simpfrag -> tyinfo -> tyinfo 80 val add_rewrs : thm list -> tyinfo -> tyinfo 81 val add_ssfrag_convs: simpfrag.convdata list -> tyinfo -> tyinfo 82 val put_induction : shared_thm -> tyinfo -> tyinfo 83 val put_axiom : shared_thm -> tyinfo -> tyinfo 84 val put_size : term * shared_thm -> tyinfo -> tyinfo 85 val put_encode : term * shared_thm -> tyinfo -> tyinfo 86 val put_lift : term -> tyinfo -> tyinfo 87 val put_fields : (string * rcd_fieldinfo) list -> tyinfo -> tyinfo 88 val put_accessors : thm list -> tyinfo -> tyinfo 89 val put_updates : thm list -> tyinfo -> tyinfo 90 val put_destructors : thm list -> tyinfo -> tyinfo 91 val put_recognizers : thm list -> tyinfo -> tyinfo 92 val put_extra : ThyDataSexp.t list -> tyinfo -> tyinfo 93 val add_extra : ThyDataSexp.t list -> tyinfo -> tyinfo 94 95 (* Functional databases of datatype facts and associated operations *) 96 97 val empty : typeBase 98 val insert : typeBase -> tyinfo -> typeBase 99 val fold : (hol_type * tyinfo * 'b -> 'b) -> 'b -> typeBase -> 100 'b 101(* val add : typeBase -> tyinfo -> typeBase *) 102 103 val fetch : typeBase -> hol_type -> tyinfo option 104 val prim_get : typeBase -> string * string -> tyinfo option 105 val get : typeBase -> string -> tyinfo list 106 (* get returns list of tyinfos for types with that tyop *) 107 108 val listItems : typeBase -> tyinfo list 109 val toPmatchThry : typeBase -> {Thy:string,Tyop:string} -> 110 {constructors : term list, case_const : term} option 111 112 (* Support for polytypism *) 113 114 val typeValue : (hol_type -> term option) * 115 (hol_type -> term option) * 116 (hol_type -> term) -> hol_type -> term 117 val tyValue : (hol_type -> term option) * 118 (hol_type -> term option) * 119 (hol_type -> term) -> hol_type -> term 120 121 val type_size : typeBase -> hol_type -> term 122 val type_encode : typeBase -> hol_type -> term 123 val type_lift : typeBase -> hol_type -> term 124 125 val cinst : hol_type -> term -> term 126 127 val is_constructor : typeBase -> term -> bool 128 129 val mk_case : typeBase -> term * (term * term) list -> term 130 val dest_case : typeBase -> term -> term * term * (term * term) list 131 val is_case : typeBase -> term -> bool 132 val strip_case : typeBase -> term -> term * (term * term) list 133 134 val mk_record : typeBase -> hol_type * (string * term) list -> term 135 val dest_record : typeBase -> term -> hol_type * (string * term) list 136 val is_record : typeBase -> term -> bool 137 138 val dest_record_type : typeBase -> hol_type -> (string * rcd_fieldinfo) list 139 val is_record_type : typeBase -> hol_type -> bool 140 141 val toSEXP : tyinfo -> ThyDataSexp.t 142 val fromSEXP : ThyDataSexp.t -> tyinfo option 143 144end 145