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