--- a/src/Pure/type.ML Wed Sep 29 13:54:31 1999 +0200
+++ b/src/Pure/type.ML Wed Sep 29 13:55:58 1999 +0200
@@ -7,7 +7,7 @@
signature TYPE =
sig
- (*TFrees vs TVars*)
+ (*TFrees and TVars*)
val no_tvars: typ -> typ
val varifyT: typ -> typ
val unvarifyT: typ -> typ
@@ -21,17 +21,19 @@
classrel: Sorts.classrel,
default: sort,
tycons: int Symtab.table,
+ log_types: string list,
+ univ_witness: (typ * sort) option,
abbrs: (string list * typ) Symtab.table,
arities: Sorts.arities}
+ val classes: type_sig -> class list
val defaultS: type_sig -> sort
val logical_types: type_sig -> string list
-
+ val univ_witness: type_sig -> (typ * sort) option
val subsort: type_sig -> sort * sort -> bool
val eq_sort: type_sig -> sort * sort -> bool
val norm_sort: type_sig -> sort -> sort
- val nonempty_sort: type_sig -> sort list -> sort -> bool
+ val witness_sorts: type_sig -> sort list -> sort list -> (typ * sort) list
val rem_sorts: typ -> typ
-
val tsig0: type_sig
val ext_tsig_classes: type_sig -> (class * class list) list -> type_sig
val ext_tsig_classrel: type_sig -> (class * class) list -> type_sig
@@ -40,12 +42,10 @@
val ext_tsig_abbrs: type_sig -> (string * string list * typ) list -> type_sig
val ext_tsig_arities: type_sig -> (string * sort list * sort)list -> type_sig
val merge_tsigs: type_sig * type_sig -> type_sig
-
val typ_errors: type_sig -> typ * string list -> string list
val cert_typ: type_sig -> typ -> typ
val norm_typ: type_sig -> typ -> typ
val norm_term: type_sig -> term -> term
-
val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
(*type matching*)
@@ -77,13 +77,13 @@
struct
-(*** TFrees vs TVars ***)
+(*** TFrees and TVars ***)
-(*disallow TVars*)
fun no_tvars T =
if null (typ_tvars T) then T
else raise TYPE ("Illegal schematic type variable(s)", [T], []);
+
(* varify, unvarify *)
val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S));
@@ -101,45 +101,49 @@
(case assoc (fmap, a) of
None => TFree f
| Some b => TVar ((b, 0), S));
- in
- map_term_types (map_type_tfree thaw) t
- end;
+ in map_term_types (map_type_tfree thaw) t end;
-(** Freeze TVars in a term; return the "thaw" inverse **)
+(* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)
-fun newName (ix, (pairs,used)) =
+local
+
+fun new_name (ix, (pairs,used)) =
let val v = variant used (string_of_indexname ix)
in ((ix,v)::pairs, v::used) end;
-fun freezeOne alist (ix,sort) =
+fun freeze_one alist (ix,sort) =
TFree (the (assoc (alist, ix)), sort)
handle OPTION =>
raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
-fun thawOne alist (a,sort) = TVar (the (assoc (alist,a)), sort)
+fun thaw_one alist (a,sort) = TVar (the (assoc (alist,a)), sort)
handle OPTION => TFree(a,sort);
-(*This sort of code could replace unvarifyT (?)
- fun freeze_thaw_type T =
- let val used = add_typ_tfree_names (T, [])
- and tvars = map #1 (add_typ_tvars (T, []))
- val (alist, _) = foldr newName (tvars, ([], used))
- in (map_type_tvar (freezeOne alist) T,
- map_type_tfree (thawOne (map swap alist)))
- end;
-*)
+(*this sort of code could replace unvarifyT (?) -- currently unused*)
+fun freeze_thaw_type T =
+ let
+ val used = add_typ_tfree_names (T, [])
+ and tvars = map #1 (add_typ_tvars (T, []));
+ val (alist, _) = foldr new_name (tvars, ([], used));
+ in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
+
+in
fun freeze_thaw t =
- let val used = it_term_types add_typ_tfree_names (t, [])
- and tvars = map #1 (it_term_types add_typ_tvars (t, []))
- val (alist, _) = foldr newName (tvars, ([], used))
- in
- case alist of
- [] => (t, fn x=>x) (*nothing to do!*)
- | _ => (map_term_types (map_type_tvar (freezeOne alist)) t,
- map_term_types (map_type_tfree (thawOne (map swap alist))))
- end;
+ let
+ val used = it_term_types add_typ_tfree_names (t, [])
+ and tvars = map #1 (it_term_types add_typ_tvars (t, []));
+ val (alist, _) = foldr new_name (tvars, ([], used));
+ in
+ (case alist of
+ [] => (t, fn x => x) (*nothing to do!*)
+ | _ => (map_term_types (map_type_tvar (freeze_one alist)) t,
+ map_term_types (map_type_tfree (thaw_one (map swap alist)))))
+ end;
+
+end;
+
(*** type signatures ***)
@@ -147,24 +151,14 @@
(* type type_sig *)
(*
- classes:
- list of all declared classes;
-
- classrel:
- (see Pure/sorts.ML)
-
- default:
- default sort attached to all unconstrained type vars;
-
- tycons:
- association list of all declared types with the number of their
- arguments;
-
- abbrs:
- association list of type abbreviations;
-
- arities:
- (see Pure/sorts.ML)
+ classes: list of all declared classes;
+ classrel: (see Pure/sorts.ML)
+ default: default sort attached to all unconstrained type vars;
+ tycons: table of all declared types with the number of their arguments;
+ log_types: list of logical type constructors sorted by number of arguments;
+ univ_witness: type witnessing non-emptiness of least sort
+ abbrs: table of type abbreviations;
+ arities: (see Pure/sorts.ML)
*)
datatype type_sig =
@@ -173,30 +167,27 @@
classrel: Sorts.classrel,
default: sort,
tycons: int Symtab.table,
+ log_types: string list,
+ univ_witness: (typ * sort) option,
abbrs: (string list * typ) Symtab.table,
arities: Sorts.arities};
fun rep_tsig (TySg comps) = comps;
+fun classes (TySg {classes = cs, ...}) = cs;
fun defaultS (TySg {default, ...}) = default;
-
-fun logical_types (TySg {classrel, arities, tycons, ...}) =
- let
- fun log_class c = Sorts.class_le classrel (c, logicC);
- fun log_type t = exists (log_class o #1) (Symtab.lookup_multi (arities, t));
- in filter log_type (Symtab.keys tycons) end;
+fun logical_types (TySg {log_types, ...}) = log_types;
+fun univ_witness (TySg {univ_witness, ...}) = univ_witness;
(* sorts *)
-(* FIXME declared!? *)
-
fun subsort (TySg {classrel, ...}) = Sorts.sort_le classrel;
fun eq_sort (TySg {classrel, ...}) = Sorts.sort_eq classrel;
fun norm_sort (TySg {classrel, ...}) = Sorts.norm_sort classrel;
-fun nonempty_sort (tsig as TySg {classrel, arities, ...}) hyps S =
- Sorts.nonempty_sort classrel arities hyps S;
+fun witness_sorts (tsig as TySg {classrel, arities, log_types, ...}) =
+ Sorts.witness_sorts (classrel, arities, log_types);
fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
| rem_sorts (TFree (x, _)) = TFree (x, [])
@@ -227,7 +218,7 @@
(* FIXME err_undcl_class! *)
(* 'leq' checks the partial order on classes according to the
- statements in the association list 'a' (i.e. 'classrel')
+ statements in classrel 'a'
*)
fun less a (C, D) = case Symtab.lookup (a, C) of
@@ -249,7 +240,7 @@
-fun of_sort (TySg {classrel, arities, ...}) = Sorts.of_sort classrel arities;
+fun of_sort (TySg {classrel, arities, ...}) = Sorts.of_sort (classrel, arities);
fun check_has_sort (tsig, T, S) =
if of_sort tsig (T, S) then ()
@@ -293,13 +284,25 @@
(** build type signatures **)
-fun make_tsig (classes, classrel, default, tycons, abbrs, arities) =
- TySg {classes = classes, classrel = classrel, default = default,
- tycons = tycons, abbrs = abbrs, arities = arities};
+fun make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities) =
+ TySg {classes = classes, classrel = classrel, default = default, tycons = tycons,
+ log_types = log_types, univ_witness = univ_witness, abbrs = abbrs, arities = arities};
+
+fun rebuild_tsig (TySg {classes, classrel, default, tycons, log_types = _, univ_witness = _, abbrs, arities}) =
+ let
+ fun log_class c = Sorts.class_le classrel (c, logicC);
+ fun log_type (t, _) = exists (log_class o #1) (Symtab.lookup_multi (arities, t));
+ val ts = filter log_type (Symtab.dest tycons);
-val tsig0 = make_tsig ([], Symtab.empty, [], Symtab.empty, Symtab.empty, Symtab.empty);
+ val log_types = map #1 (Library.sort (Library.int_ord o pairself #2) ts);
+ val univ_witness =
+ (case Sorts.witness_sorts (classrel, arities, log_types) [] [classes] of
+ [w] => Some w | _ => None);
+ in make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities) end;
-
+val tsig0 =
+ make_tsig ([], Symtab.empty, [], Symtab.empty, [], None, Symtab.empty, Symtab.empty)
+ |> rebuild_tsig;
(* typ_errors *)
@@ -350,19 +353,14 @@
(** merge type signatures **)
-(*'assoc_union' merges two association lists if the contents associated
- the keys are lists*)
+(* merge classrel *)
fun assoc_union (as1, []) = as1
| assoc_union (as1, (key, l2) :: as2) =
(case assoc_string (as1, key) of
- Some l1 => assoc_union
- (overwrite (as1, (key, l1 union_string l2)), as2)
+ Some l1 => assoc_union (overwrite (as1, (key, l1 union_string l2)), as2)
| None => assoc_union ((key, l2) :: as1, as2));
-
-(* merge classrel *)
-
fun merge_classrel (classrel1, classrel2) =
let
val classrel = transitive_closure (assoc_union (Symtab.dest classrel1, Symtab.dest classrel2))
@@ -375,6 +373,8 @@
(* coregularity *)
+local
+
(* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
fun is_unique_decl ars (t,(C,w)) = case assoc (ars, C) of
@@ -402,17 +402,20 @@
fun check(Cw2) = (check1(Cw1,Cw2); check1(Cw2,Cw1))
in seq check end;
+in
+
fun add_arity classrel ars (tCw as (_,Cw)) =
(is_unique_decl ars tCw; coreg classrel tCw ars; Cw ins ars);
-fun varying_decls t =
- error ("Type constructor " ^ quote t ^ " has varying number of arguments");
+end;
(* 'merge_arities' builds the union of two 'arities' lists;
it only checks the two restriction conditions and inserts afterwards
all elements of the second list into the first one *)
+local
+
fun merge_arities_aux classrel =
let fun test_ar t (ars1, sw) = add_arity classrel ars1 (t,sw);
@@ -423,32 +426,49 @@
| None => c::arities1
in foldl merge_c end;
+in
+
fun merge_arities classrel (a1, a2) =
Symtab.make (merge_arities_aux classrel (Symtab.dest a1, Symtab.dest a2));
+end;
+
+
+(* tycons *)
+
+fun varying_decls t =
+ error ("Type constructor " ^ quote t ^ " has varying number of arguments");
+
fun add_tycons (tycons, tn as (t,n)) =
(case Symtab.lookup (tycons, t) of
Some m => if m = n then tycons else varying_decls t
| None => Symtab.update (tn, tycons));
+
+(* merge_abbrs *)
+
fun merge_abbrs abbrs =
Symtab.merge (op =) abbrs handle Symtab.DUPS dups => raise TERM (dup_tyabbrs dups, []);
-(* 'merge_tsigs' takes the above declared functions to merge two type
- signatures *)
+(* merge_tsigs *)
-fun merge_tsigs(TySg{classes=classes1, default=default1, classrel=classrel1,
- tycons=tycons1, arities=arities1, abbrs=abbrs1},
- TySg{classes=classes2, default=default2, classrel=classrel2,
- tycons=tycons2, arities=arities2, abbrs=abbrs2}) =
- let val classes' = classes1 union_string classes2;
- val classrel' = merge_classrel (classrel1, classrel2);
- val tycons' = foldl add_tycons (tycons1, Symtab.dest tycons2)
- val arities' = merge_arities classrel' (arities1, arities2);
- val default' = Sorts.norm_sort classrel' (default1 @ default2);
- val abbrs' = merge_abbrs(abbrs1, abbrs2);
- in make_tsig(classes', classrel', default', tycons', abbrs', arities') end;
+fun merge_tsigs
+ (TySg {classes = classes1, default = default1, classrel = classrel1, tycons = tycons1,
+ log_types = _, univ_witness = _, arities = arities1, abbrs = abbrs1},
+ TySg {classes = classes2, default = default2, classrel = classrel2, tycons = tycons2,
+ log_types = _, univ_witness = _, arities = arities2, abbrs = abbrs2}) =
+ let
+ val classes' = classes1 union_string classes2;
+ val classrel' = merge_classrel (classrel1, classrel2);
+ val arities' = merge_arities classrel' (arities1, arities2);
+ val tycons' = foldl add_tycons (tycons1, Symtab.dest tycons2);
+ val default' = Sorts.norm_sort classrel' (default1 @ default2);
+ val abbrs' = merge_abbrs (abbrs1, abbrs2);
+ in
+ make_tsig (classes', classrel', default', tycons', [], None, abbrs', arities')
+ |> rebuild_tsig
+ end;
@@ -498,48 +518,47 @@
fun ext_tsig_classes tsig new_classes =
let
- val TySg {classes, classrel, default, tycons, abbrs, arities} = tsig;
+ val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
val (classes',classrel') = extend_classes (classes,classrel,new_classes);
- in
- make_tsig (classes', classrel', default, tycons, abbrs, arities)
- end;
+ in make_tsig (classes', classrel', default, tycons, log_types, univ_witness, abbrs, arities) end;
(* ext_tsig_classrel *)
fun ext_tsig_classrel tsig pairs =
let
- val TySg {classes, classrel, default, tycons, abbrs, arities} = tsig;
+ val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
(* FIXME clean! *)
val classrel' =
merge_classrel (classrel, Symtab.make (map (fn (c1, c2) => (c1, [c2])) pairs));
in
- make_tsig (classes, classrel', default, tycons, abbrs, arities)
+ make_tsig (classes, classrel', default, tycons, log_types, univ_witness, abbrs, arities)
+ |> rebuild_tsig
end;
(* ext_tsig_defsort *)
-fun ext_tsig_defsort(TySg{classes,classrel,tycons,abbrs,arities,...}) default =
- make_tsig (classes, classrel, default, tycons, abbrs, arities);
+fun ext_tsig_defsort
+ (TySg {classes, classrel, default = _, tycons, log_types, univ_witness, abbrs, arities, ...}) default =
+ make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities);
(** add types **)
-fun ext_tsig_types (TySg {classes, classrel, default, tycons, abbrs, arities}) ts =
+fun ext_tsig_types (TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities}) ts =
let
fun check_type (c, n) =
if n < 0 then err_neg_args c
else if is_some (Symtab.lookup (tycons, c)) then err_dup_tycon c
else if is_some (Symtab.lookup (abbrs, c)) then error (ty_confl c)
else ();
- in
- seq check_type ts;
- make_tsig (classes, classrel, default, Symtab.extend (tycons, ts), abbrs,
- Symtab.extend (arities, map (rpair [] o #1) ts))
- end;
+ val _ = seq check_type ts;
+ val tycons' = Symtab.extend (tycons, ts);
+ val arities' = Symtab.extend (arities, map (rpair [] o #1) ts);
+ in make_tsig (classes, classrel, default, tycons', log_types, univ_witness, abbrs, arities') end;
@@ -586,8 +605,10 @@
| msgs => err msgs)
end;
-fun add_abbr (tsig as TySg{classes,classrel,default,tycons,arities,abbrs}, abbr) =
- make_tsig (classes,classrel,default,tycons, Symtab.update (prep_abbr tsig abbr, abbrs), arities);
+fun add_abbr
+ (tsig as TySg {classes, classrel, default, tycons, log_types, univ_witness, arities, abbrs}, abbr) =
+ make_tsig (classes, classrel, default, tycons, log_types, univ_witness,
+ Symtab.update (prep_abbr tsig abbr, abbrs), arities);
fun ext_tsig_abbrs tsig raw_abbrs = foldl add_abbr (tsig, raw_abbrs);
@@ -648,15 +669,15 @@
fun ext_tsig_arities tsig sarities =
let
- val TySg {classes, classrel, default, tycons, arities, abbrs} = tsig;
+ val TySg {classes, classrel, default, tycons, log_types, univ_witness, arities, abbrs} = tsig;
val arities1 =
- List.concat
- (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
- val arities2 = foldl (coregular (classes, classrel, tycons))
- (arities, norm_domain classrel arities1)
+ flat (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
+ val arities2 =
+ foldl (coregular (classes, classrel, tycons)) (arities, norm_domain classrel arities1)
|> Symtab.dest |> close classrel |> Symtab.make;
in
- make_tsig (classes, classrel, default, tycons, abbrs, arities2)
+ make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities2)
+ |> rebuild_tsig
end;
@@ -733,7 +754,7 @@
fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
fun mg_domain a S =
- Sorts.mg_domain classrel arities a S handle TYPE _ => raise TUNIFY;
+ Sorts.mg_domain (classrel, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY;
fun meet ((_, []), tye) = tye
| meet ((TVar (xi, S'), S), tye) =
@@ -885,9 +906,7 @@
val (ts, Ts, unifier) =
TypeInfer.infer_types prt prT const_type classrel arities used freeze
is_param raw_ts' pat_Ts';
- in
- (ts, unifier)
- end;
+ in (ts, unifier) end;
end;