1(* ===================================================================== *) 2(* FILE : Type.sml *) 3(* DESCRIPTION : HOL types. *) 4(* *) 5(* AUTHOR : (c) Konrad Slind, University of Calgary *) 6(* DATE : August 26, 1991 *) 7(* UPDATE : October 94. Type signature implementation moved from *) 8(* symtab.sml, which is now gone. *) 9(* Modified : September 22, 1997, Ken Larsen (functor removal) *) 10(* April 12, 1998, Konrad Slind *) 11(* July, 2000, Konrad Slind *) 12(* ===================================================================== *) 13 14structure Type :> Type = 15struct 16 17open Feedback Lib KernelTypes; infix |->; 18 19type hol_type = KernelTypes.hol_type; 20 21val ERR = mk_HOL_ERR "Type"; 22val WARN = HOL_WARNING "Type"; 23 24 25(*--------------------------------------------------------------------------- 26 Create the signature for HOL types 27 ---------------------------------------------------------------------------*) 28 29val typesig = KernelSig.new_table() 30fun prim_delete_type (k as {Thy, Tyop}) = 31 ignore (KernelSig.retire_name(typesig, {Thy = Thy, Name = Tyop})) 32 33fun prim_new_type {Thy,Tyop} n = let 34 val _ = n >= 0 orelse failwith "invalid arity" 35in 36 ignore (KernelSig.insert(typesig,{Thy=Thy,Name=Tyop},n)) 37end 38fun del_segment s = KernelSig.del_segment(typesig, s) 39 40fun uptodate_type (Tyv s) = true 41 | uptodate_type (Tyapp((info,_), args)) = 42 KernelSig.uptodate_id info andalso List.all uptodate_type args 43 44 45 46 47(*---------------------------------------------------------------------------* 48 * Builtin type operators (fun, bool, ind). These are in every HOL * 49 * signature, and it is convenient to nail them down here. * 50 *---------------------------------------------------------------------------*) 51 52local open KernelSig 53in 54val fun_tyid = insert(typesig, {Thy = "min", Name = "fun"}, 2) 55val fun_tyc = (fun_tyid, 2) 56val bool_tyid = insert(typesig, {Thy = "min", Name = "bool"}, 0) 57val ind_tyid = insert(typesig, {Thy = "min", Name = "ind"}, 0) 58end 59 60 61(*--------------------------------------------------------------------------- 62 Some basic values 63 ---------------------------------------------------------------------------*) 64 65val bool = Tyapp ((bool_tyid,0),[]) 66val ind = Tyapp ((ind_tyid,0), []); 67 68(*--------------------------------------------------------------------------- 69 Function types 70 ---------------------------------------------------------------------------*) 71 72infixr 3 -->; 73fun (X --> Y) = Tyapp (fun_tyc, [X,Y]); 74 75fun dom_rng (Tyapp(tyc,[X,Y])) = 76 if tyc=fun_tyc then (X,Y) 77 else raise ERR "dom_rng" "not a function type" 78 | dom_rng _ = raise ERR "dom_rng" "not a function type"; 79 80(*---------------------------------------------------------------------------* 81 * Create a compound type, in a specific segment, and in the current theory. * 82 *---------------------------------------------------------------------------*) 83 84fun make_type (tyc as (_,arity)) Args (fnstr,name) = 85 if arity = length Args then Tyapp(tyc,Args) else 86 raise ERR fnstr (String.concat 87 [name," needs ", int_to_string arity, 88 " arguments, but was given ", int_to_string(length Args)]); 89 90fun mk_thy_type {Thy,Tyop,Args} = let 91 open KernelSig 92 val knm = {Thy=Thy, Name = Tyop} 93in 94 case peek(typesig,{Thy=Thy,Name=Tyop}) of 95 SOME const => make_type const Args ("mk_thy_type", name_toString knm) 96 | NONE => raise ERR "mk_thy_type" 97 ("the type operator "^quote Tyop^ 98 " has not been declared in theory "^quote Thy^".") 99end 100 101fun decls nm = let 102 fun foldthis({Thy,Name},_,acc) = if Name = nm then 103 {Tyop=Name,Thy=Thy} :: acc 104 else acc 105in 106 KernelSig.foldl foldthis [] typesig 107end 108 109local 110 fun first_decl Tyop = let 111 fun foldthis({Thy,Name},tycon,acc) = 112 if Name = Tyop then tycon :: acc 113 else acc 114 in 115 case KernelSig.foldl foldthis [] typesig of 116 [] => raise ERR "mk_type" (Lib.quote Tyop^" has not been declared") 117 | [c] => c 118 | c::_ => (WARN "mk_type" "more than one possibility"; c) 119 end 120in 121 122fun mk_type (Tyop,Args) = 123 make_type (first_decl Tyop) Args ("mk_type",Tyop); 124end 125 126(*---------------------------------------------------------------------------* 127 * Take a type apart. * 128 *---------------------------------------------------------------------------*) 129 130local open KernelTypes KernelSig 131in 132fun break_type (Tyapp p) = p | break_type _ = raise ERR "break_type" ""; 133 134fun dest_thy_type (Tyapp((tyc,_),A)) = {Thy=seg_of tyc,Tyop=name_of tyc,Args=A} 135 | dest_thy_type _ = raise ERR "dest_thy_type" ""; 136 137fun dest_type (Tyapp((tyc,_),A)) = (name_of tyc, A) 138 | dest_type _ = raise ERR "dest_type" "" 139end; 140 141(*---------------------------------------------------------------------------* 142 * Return arity of putative type operator * 143 *---------------------------------------------------------------------------*) 144 145fun op_arity {Thy,Tyop} = 146 case KernelSig.peek(typesig,{Thy=Thy,Name=Tyop}) of 147 SOME (id, a) => SOME a 148 | NONE => NONE 149 150(*--------------------------------------------------------------------------- 151 Declared types in a theory segment 152 ---------------------------------------------------------------------------*) 153 154fun thy_types s = let 155 fun xlate (knm, (id,arity)) = (KernelSig.name_of id, arity) 156in 157 map xlate (KernelSig.listThy typesig s) 158end; 159 160 161(*---------------------------------------------------------------------------* 162 * Type variables * 163 *---------------------------------------------------------------------------*) 164 165val alpha = Tyv "'a" 166val beta = Tyv "'b"; 167val gamma = Tyv "'c" 168val delta = Tyv "'d" 169val etyvar = Tyv "'e" 170val ftyvar = Tyv "'f" 171 172val varcomplain = ref true 173val _ = register_btrace ("Vartype Format Complaint", varcomplain) 174 175fun mk_vartype "'a" = alpha | mk_vartype "'b" = beta 176 | mk_vartype "'c" = gamma | mk_vartype "'d" = delta 177 | mk_vartype "'e" = etyvar | mk_vartype "'f" = ftyvar 178 | mk_vartype s = if Lexis.allowed_user_type_var s then Tyv s 179 else (if !varcomplain then 180 WARN "mk_vartype" "non-standard syntax" 181 else (); Tyv s) 182 183fun dest_vartype (Tyv s) = s 184 | dest_vartype _ = raise ERR "dest_vartype" "not a type variable"; 185 186fun is_vartype (Tyv _) = true | is_vartype _ = false; 187val is_type = not o is_vartype; 188 189(*---------------------------------------------------------------------------* 190 * The variables in a type. * 191 *---------------------------------------------------------------------------*) 192 193local fun tyvars (Tyapp(_,Args)) vlist = tyvarsl Args vlist 194 | tyvars v vlist = Lib.insert v vlist 195 and tyvarsl L vlist = rev_itlist tyvars L vlist 196in 197fun type_vars ty = rev(tyvars ty []) 198fun type_varsl L = rev(tyvarsl L []) 199end; 200 201 202(*--------------------------------------------------------------------------- 203 Does there exist a type variable v in a type such that P(v) holds. 204 Returns false if there are no type variables in the type. 205 ---------------------------------------------------------------------------*) 206 207fun exists_tyvar P = 208 let fun occ (w as Tyv _) = P w 209 | occ (Tyapp(_,Args)) = Lib.exists occ Args 210 in occ end; 211 212(*--------------------------------------------------------------------------- 213 Does a type variable occur in a type 214 ---------------------------------------------------------------------------*) 215 216fun type_var_in v = 217 if is_vartype v then exists_tyvar (equal v) 218 else raise ERR "type_var_occurs" "not a type variable" 219 220(*---------------------------------------------------------------------------* 221 * Substitute in a type, trying to preserve existing structure. * 222 *---------------------------------------------------------------------------*) 223 224fun ty_sub [] _ = SAME 225 | ty_sub theta (Tyapp(tyc,Args)) 226 = (case delta_map (ty_sub theta) Args 227 of SAME => SAME 228 | DIFF Args' => DIFF (Tyapp(tyc, Args'))) 229 | ty_sub theta v = 230 case Lib.subst_assoc (equal v) theta 231 of NONE => SAME 232 | SOME ty => DIFF ty 233 234fun type_subst theta = delta_apply (ty_sub theta) 235 236 237(*---------------------------------------------------------------------------* 238 * Is a type polymorphic? * 239 *---------------------------------------------------------------------------*) 240 241fun polymorphic (Tyv _) = true 242 | polymorphic (Tyapp(_,Args)) = exists polymorphic Args 243 244 245(*--------------------------------------------------------------------------- 246 This matching algorithm keeps track of identity bindings 247 v |-> v in a separate area. This eliminates the need for 248 post-match normalization of substitutions coming from the 249 matching algorithm. 250 ---------------------------------------------------------------------------*) 251 252local 253 fun MERR s = raise ERR "raw_match_type" s 254 fun lookup x ids = 255 let fun look [] = if Lib.mem x ids then SOME x else NONE 256 | look ({redex,residue}::t) = if x=redex then SOME residue else look t 257 in look end 258in 259fun tymatch [] [] Sids = Sids 260 | tymatch ((v as Tyv name)::ps) (ty::obs) (Sids as (S,ids)) = 261 tymatch ps obs 262 (case lookup v ids S 263 of NONE => if v=ty then (S,v::ids) else ((v |-> ty)::S,ids) 264 | SOME ty1 => if ty1=ty then Sids else 265 MERR ("double bind on type variable "^name)) 266 | tymatch (Tyapp(c1,A1)::ps) (Tyapp(c2,A2)::obs) Sids = 267 if c1=c2 then tymatch (A1@ps) (A2@obs) Sids 268 else let val n1 = KernelSig.id_toString (fst c1) 269 val n2 = KernelSig.id_toString (fst c2) 270 in MERR ("attempt to match different tyops: "^n1^" against "^n2) 271 end 272 | tymatch any other thing = MERR "different constructors" 273end 274 275fun raw_match_type pat ob Sids = tymatch [pat] [ob] Sids 276 277fun match_type_restr fixed pat ob = fst (raw_match_type pat ob ([],fixed)) 278fun match_type_in_context pat ob S = fst (raw_match_type pat ob (S,[])) 279 280fun match_type pat ob = match_type_in_context pat ob [] 281 282 283 284(*--------------------------------------------------------------------------- 285 An order on types 286 ---------------------------------------------------------------------------*) 287 288fun compare (Tyv s1, Tyv s2) = String.compare (s1,s2) 289 | compare (Tyv _, _) = LESS 290 | compare (Tyapp _, Tyv _) = GREATER 291 | compare (Tyapp((c1,_),A1), Tyapp((c2,_),A2)) = 292 case KernelSig.id_compare (c1, c2) 293 of EQUAL => Lib.list_compare compare (A1,A2) 294 | x => x; 295 296(*--------------------------------------------------------------------------- 297 Automatically generated type variables. The unusual names make 298 it unlikely that the names will clash with user-created 299 type variables. 300 ---------------------------------------------------------------------------*) 301 302local val gen_tyvar_prefix = "%%gen_tyvar%%" 303 fun num2name i = gen_tyvar_prefix ^ Int.toString i 304 val nameStrm = Portable.make_counter{inc=1,init=0} 305in 306fun gen_tyvar () = Tyv(num2name(nameStrm())) 307 308fun is_gen_tyvar (Tyv name) = String.isPrefix gen_tyvar_prefix name 309 | is_gen_tyvar _ = false; 310end; 311 312fun size acc tylist = 313 case tylist of 314 [] => acc 315 | [] :: tys => size acc tys 316 | (ty::tys1) :: tys2 => let 317 in 318 case ty of 319 Tyv _ => size (1 + acc) (tys1 :: tys2) 320 | Tyapp(_, args) => size (1 + acc) (args :: tys1 :: tys2) 321 end 322 323fun type_size ty = size 0 [[ty]] 324 325end (* Type *) 326