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