1structure Type :> Type = 2struct 3 4open Feedback Lib KernelTypes 5 6infix |-> 7infixr --> 8 9val WARN = HOL_WARNING "Type"; 10fun ERR f msg = HOL_ERR {origin_structure = "Type", 11 origin_function = f, 12 message = msg} 13 14type type_key = {Thy : string, Tyop : string } 15type type_info = KernelSig.kernelid * int 16 17val operator_table = KernelSig.new_table() 18 19fun prim_delete_type (k as {Thy, Tyop}) = 20 ignore (KernelSig.retire_name(operator_table, {Thy = Thy, Name = Tyop})) 21 22fun prim_new_type {Thy,Tyop} n = let 23 val _ = n >= 0 orelse failwith "invalid arity" 24in 25 ignore (KernelSig.insert(operator_table,{Thy=Thy,Name=Tyop},n)) 26end 27 28fun thy_types s = let 29 fun foldthis (kn,(_,arity),acc) = 30 if #Thy kn = s then (#Name kn, arity) :: acc 31 else acc 32in 33 KernelSig.foldl foldthis [] operator_table 34end 35 36fun del_segment s = KernelSig.del_segment(operator_table, s) 37 38fun minseg s = {Thy = "min", Tyop = s} 39val _ = prim_new_type (minseg "fun") 2 40val _ = prim_new_type (minseg "bool") 0 41val _ = prim_new_type (minseg "ind") 0 42 43val funref = #1 (KernelSig.find(operator_table, {Thy="min", Name = "fun"})) 44 45fun uptodate_type (Tyv s) = true 46 | uptodate_type (Tyapp(info, args)) = KernelSig.uptodate_id info andalso 47 List.all uptodate_type args 48 49fun dest_vartype (Tyv s) = s 50 | dest_vartype _ = raise ERR "dest_vartype" "Type not a vartype" 51 52fun is_vartype (Tyv _) = true 53 | is_vartype _ = false 54 55val gen_tyvar_prefix = "%%gen_tyvar%%" 56 57fun num2name i = gen_tyvar_prefix ^ Lib.int_to_string i 58val nameStrm = Lib.mk_istream (fn x => x + 1) 0 num2name 59 60fun gen_tyvar () = Tyv (state(next nameStrm)) 61 62fun is_gen_tyvar (Tyv name) = String.isPrefix gen_tyvar_prefix name 63 | is_gen_tyvar _ = false; 64 65fun first_decl caller s = let 66 val possibilities = KernelSig.listName operator_table s 67in 68 case possibilities of 69 [] => raise ERR caller ("No such type: "^s) 70 | [x] => #2 x 71 | x::xs => (WARN caller ("More than one possibility for "^s); #2 x) 72end 73 74fun mk_type (opname, args) = let 75 val (id,aty) = first_decl "mk_type" opname 76in 77 if length args = aty then 78 Tyapp (id, args) 79 else 80 raise ERR "mk_type" 81 ("Expecting "^Int.toString aty^" arguments for "^opname) 82end 83 84val bool = mk_type("bool", []) 85val ind = mk_type("ind", []) 86 87fun dest_type (Tyv _) = raise ERR "dest_type" "Type a variable" 88 | dest_type (Tyapp(id, args)) = let 89 val {Thy, Name} = KernelSig.name_of_id id 90 in 91 (Name, args) 92 end 93 94fun is_type (Tyapp _) = true | is_type _ = false 95 96fun mk_thy_type {Thy, Tyop, Args} = 97 case KernelSig.peek(operator_table, {Thy = Thy, Name = Tyop}) of 98 NONE => raise ERR "mk_thy_type" ("No such type: "^Thy ^ "$" ^ Tyop) 99 | SOME (i,arity) => 100 if arity = length Args then Tyapp(i, Args) 101 else raise ERR "mk_thy_type" ("Expecting "^Int.toString arity^ 102 " arguments for "^Tyop) 103 104fun dest_thy_type (Tyv _) = raise ERR "dest_thy_type" "Type a variable" 105 | dest_thy_type (Tyapp(id, args)) = 106 {Thy = KernelSig.seg_of id, Tyop = KernelSig.name_of id, Args = args} 107 108fun decls s = let 109 fun foldthis ({Thy,Name},v,acc) = if Name = s then {Thy=Thy,Tyop=Name}::acc 110 else acc 111in 112 KernelSig.foldl foldthis [] operator_table 113end 114 115fun op_arity {Thy,Tyop} = 116 Option.map (#2) (KernelSig.peek(operator_table, {Thy=Thy,Name=Tyop})) 117 118fun type_vars_set acc [] = acc 119 | type_vars_set acc ((t as Tyv s) :: rest) = 120 type_vars_set (HOLset.add(acc, t)) rest 121 | type_vars_set acc (Tyapp(_, args) :: rest) = 122 type_vars_set acc (args @ rest) 123 124fun compare (Tyv s1, Tyv s2) = String.compare(s1, s2) 125 | compare (Tyv _, _) = LESS 126 | compare (Tyapp _, Tyv _) = GREATER 127 | compare (Tyapp(i, iargs), Tyapp(j, jargs)) = let 128 in 129 case KernelSig.id_compare(i,j) of 130 EQUAL => Lib.list_compare compare (iargs, jargs) 131 | x => x 132 end 133 134val empty_tyset = HOLset.empty compare 135 136fun type_vars ty = HOLset.listItems (type_vars_set empty_tyset [ty]) 137 138val type_varsl = HOLset.listItems o type_vars_set empty_tyset 139 140fun exists_tyvar P = let 141 fun occ (w as Tyv _) = P w 142 | occ (Tyapp(_, Args)) = List.exists occ Args 143in 144 occ 145end 146 147fun type_var_in v = 148 if is_vartype v then exists_tyvar (equal v) 149 else raise ERR "type_var_in" "not a type variable" 150 151val polymorphic = exists_tyvar (fn _ => true) 152 153fun (ty1 --> ty2) = Tyapp(funref, [ty1, ty2]) 154 155fun dom_rng (Tyv _) = raise ERR "dom_rng" "Type a variable" 156 | dom_rng (Tyapp(i, args)) = if i = funref then (hd args, hd (tl args)) 157 else raise ERR "dom_rng" 158 "Type not a function type" 159 160val alpha = Tyv "'a" 161val beta = Tyv "'b"; 162val gamma = Tyv "'c" 163val delta = Tyv "'d" 164val etyvar = Tyv "'e" 165val ftyvar = Tyv "'f" 166 167val varcomplain = ref true 168val _ = register_btrace ("Vartype Format Complaint", varcomplain) 169 170fun mk_vartype "'a" = alpha | mk_vartype "'b" = beta 171 | mk_vartype "'c" = gamma | mk_vartype "'d" = delta 172 | mk_vartype "'e" = etyvar | mk_vartype "'f" = ftyvar 173 | mk_vartype s = if Lexis.allowed_user_type_var s then Tyv s 174 else (if !varcomplain then 175 WARN "mk_vartype" "non-standard syntax" 176 else (); Tyv s) 177 178fun ty_sub [] _ = SAME 179 | ty_sub theta (Tyapp(tyc,Args)) 180 = (case delta_map (ty_sub theta) Args 181 of SAME => SAME 182 | DIFF Args' => DIFF (Tyapp(tyc, Args'))) 183 | ty_sub theta v = 184 case Lib.subst_assoc (equal v) theta 185 of NONE => SAME 186 | SOME ty => DIFF ty 187 188fun type_subst theta = delta_apply (ty_sub theta) 189 190(* val type_subst0 = type_subst 191fun type_subst theta = Profile.profile "type_subst" (type_subst0 theta) *) 192 193 194local 195 fun MERR s = raise ERR "raw_match_type" s 196 fun lookup x ids = 197 let fun look [] = if Lib.mem x ids then SOME x else NONE 198 | look ({redex,residue}::t) = if x=redex then SOME residue else look t 199 in look end 200in 201fun tymatch [] [] Sids = Sids 202 | tymatch ((v as Tyv _)::ps) (ty::obs) (Sids as (S,ids)) = 203 tymatch ps obs 204 (case lookup v ids S 205 of NONE => if v=ty then (S,v::ids) else ((v |-> ty)::S,ids) 206 | SOME ty1 => if ty1=ty then Sids else MERR "double bind") 207 | tymatch (Tyapp(c1,A1)::ps) (Tyapp(c2,A2)::obs) Sids = 208 if c1=c2 then tymatch (A1@ps) (A2@obs) Sids 209 else MERR "different tyops" 210 | tymatch any other thing = MERR "different constructors" 211end 212(* 213fun raw_match_type (v as Tyv _) ty (Sids as (S,ids)) = 214 (case lookup v ids S 215 of NONE => if v=ty then (S,v::ids) else ((v |-> ty)::S,ids) 216 | SOME ty1 => if ty1=ty then Sids else MERR "double bind") 217 | raw_match_type (Tyapp(c1,A1)) (Tyapp(c2,A2)) Sids = 218 if c1=c2 then rev_itlist2 raw_match_type A1 A2 Sids 219 else MERR "different tyops" 220 | raw_match_type _ _ _ = MERR "different constructors" 221*) 222fun raw_match_type pat ob Sids = tymatch [pat] [ob] Sids 223 224fun match_type_restr fixed pat ob = fst (raw_match_type pat ob ([],fixed)) 225fun match_type_in_context pat ob S = fst (raw_match_type pat ob (S,[])) 226 227fun match_type pat ob = match_type_in_context pat ob [] 228 229 230fun size acc tylist = 231 case tylist of 232 [] => acc 233 | [] :: tys => size acc tys 234 | (ty::tys1) :: tys2 => let 235 in 236 case ty of 237 Tyv _ => size (1 + acc) (tys1 :: tys2) 238 | Tyapp(_, args) => size (1 + acc) (args :: tys1 :: tys2) 239 end 240 241fun type_size ty = size 0 [[ty]] 242 243end (* struct *) 244