--- a/src/Pure/defs.ML Thu May 11 19:15:12 2006 +0200
+++ b/src/Pure/defs.ML Thu May 11 19:15:13 2006 +0200
@@ -2,55 +2,126 @@
ID: $Id$
Author: Makarius
-Global well-formedness checks for constant definitions -- covers
-dependencies of simple sub-structural overloading.
+Global well-formedness checks for constant definitions. Covers
+dependencies of simple sub-structural overloading, where type
+arguments are approximated by the outermost type constructor.
*)
signature DEFS =
sig
type T
- val define: (string * typ -> typ list) ->
- bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
val specifications_of: T -> string ->
(serial * {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}) list
val empty: T
- val merge: Pretty.pp -> T * T -> T
+ val merge: T * T -> T
+ val define: (string * typ -> typ list) ->
+ bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
end
structure Defs: DEFS =
struct
+(* dependency items *)
-(** datatype T **)
+(*
+ Constant c covers all instances of c
+
+ Instance (c, a) covers all instances of applications (c, [Type (a, _)])
+
+ Different Constant/Constant or Instance/Instance items represent
+ disjoint sets of instances. The set Constant c subsumes any
+ Instance (c, a) -- dependencies are propagated accordingly.
+*)
+
+datatype item =
+ Constant of string |
+ Instance of string * string;
+
+fun make_item (c, [Type (a, _)]) = Instance (c, a)
+ | make_item (c, _) = Constant c;
+
+fun pretty_item (Constant c) = Pretty.str (quote c)
+ | pretty_item (Instance (c, a)) = Pretty.str (quote c ^ " (type " ^ quote a ^ ")");
+
+fun item_ord (Constant c, Constant c') = fast_string_ord (c, c')
+ | item_ord (Instance ca, Instance ca') = prod_ord fast_string_ord fast_string_ord (ca, ca')
+ | item_ord (Constant _, Instance _) = LESS
+ | item_ord (Instance _, Constant _) = GREATER;
+
+structure Items = GraphFun(type key = item val ord = item_ord);
+
+fun declare_edge (i, j) =
+ Items.default_node (i, ()) #>
+ Items.default_node (j, ()) #>
+ Items.add_edge_acyclic (i, j);
+
+fun propagate_deps insts deps =
+ let
+ fun insts_of c = map (fn a => Instance (c, a)) (Symtab.lookup_list insts c);
+ fun inst_edge (Constant c) (Constant d) = fold declare_edge (product (insts_of c) (insts_of d))
+ | inst_edge (Constant c) j = fold (fn i => declare_edge (i, j)) (insts_of c)
+ | inst_edge i (Constant c) = fold (fn j => declare_edge (i, j)) (insts_of c)
+ | inst_edge (Instance _) (Instance _) = I;
+ in Items.fold (fn (i, (_, (_, js))) => fold (inst_edge i) js) deps deps end;
+
+
+(* specifications *)
type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list};
datatype T = Defs of
- {consts: unit Graph.T,
- specified: spec Inttab.table Symtab.table};
+ {specs: (bool * spec Inttab.table) Symtab.table,
+ insts: string list Symtab.table,
+ deps: unit Items.T};
+
+fun no_overloading_of (Defs {specs, ...}) c =
+ (case Symtab.lookup specs c of
+ SOME (b, _) => b
+ | NONE => false);
-fun make_defs (consts, specified) = Defs {consts = consts, specified = specified};
-fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified));
+fun specifications_of (Defs {specs, ...}) c =
+ (case Symtab.lookup specs c of
+ SOME (_, sps) => Inttab.dest sps
+ | NONE => []);
-fun cyclic cycles =
- "Cyclic dependency of constants:\n" ^
- cat_lines (map (space_implode " -> " o map quote o rev) cycles);
+fun make_defs (specs, insts, deps) = Defs {specs = specs, insts = insts, deps = deps};
+fun map_defs f (Defs {specs, insts, deps}) = make_defs (f (specs, insts, deps));
+
+val empty = make_defs (Symtab.empty, Symtab.empty, Items.empty);
-(* specified consts *)
+(* merge *)
fun disjoint_types T U =
(Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
handle Type.TUNIFY => true;
-fun check_specified c (i, {lhs = T, name = a, ...}: spec) =
+fun disjoint_specs c (i, {lhs = T, name = a, ...}: spec) =
Inttab.forall (fn (j, {lhs = U, name = b, ...}: spec) =>
i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
" for constant " ^ quote c));
+fun cycle_msg css =
+ let
+ fun prt_cycle items = Pretty.block (flat
+ (separate [Pretty.str " -> ", Pretty.brk 1] (map (single o pretty_item) items)));
+ in Pretty.string_of (Pretty.big_list "Cyclic dependency of constants:" (map prt_cycle css)) end;
-(* substructural type arguments *)
+
+fun merge
+ (Defs {specs = specs1, insts = insts1, deps = deps1},
+ Defs {specs = specs2, insts = insts2, deps = deps2}) =
+ let
+ val specs' = (specs1, specs2) |> Symtab.join (fn c => fn ((b, sps1), (_, sps2)) =>
+ (b, Inttab.fold (fn sp2 => (disjoint_specs c sp2 sps1; Inttab.update sp2)) sps2 sps1));
+ val insts' = Symtab.merge_list (op =) (insts1, insts2);
+ val items' = propagate_deps insts' (Items.merge_acyclic (K true) (deps1, deps2))
+ handle Items.CYCLES cycles => error (cycle_msg cycles);
+ in make_defs (specs', insts', items') end;
+
+
+(* define *)
fun struct_less T (Type (_, Us)) = exists (struct_le T) Us
| struct_less _ _ = false
@@ -60,44 +131,35 @@
fun structs_less Ts Us = Ts <> Us andalso structs_le Ts Us;
-(* define consts *)
-
-fun define const_typargs is_def module name lhs rhs = map_defs (fn (consts, specified) =>
+fun define const_typargs is_def module name lhs rhs defs = defs
+ |> map_defs (fn (specs, insts, deps) =>
let
val (c, T) = lhs;
val args = const_typargs lhs;
- val deps = rhs |> map_filter (fn d =>
- if structs_less (const_typargs d) args then NONE else SOME (#1 d));
val no_overloading = forall Term.is_TVar args andalso not (has_duplicates (op =) args);
- val consts' = fold (fn (a, _) => Graph.default_node (a, ())) (lhs :: rhs) consts;
- val consts'' = Graph.add_deps_acyclic (c, deps) consts' handle Graph.CYCLES cycles =>
- if no_overloading then error (cyclic cycles)
- else (warning (cyclic cycles ^ "\nUnchecked overloaded specification: " ^ name); consts');
-
val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs});
- val specified' = specified
- |> Symtab.default (c, Inttab.empty)
- |> Symtab.map_entry c (fn specs => (check_specified c spec specs; Inttab.update spec specs));
- in (consts', specified') end);
-
-fun specifications_of (Defs {specified, ...}) c =
- Inttab.dest (the_default Inttab.empty (Symtab.lookup specified c));
-
-
-(* empty and merge *)
+ val specs' = specs
+ |> Symtab.default (c, (false, Inttab.empty))
+ |> Symtab.map_entry c (fn (_, sps) =>
+ (disjoint_specs c spec sps; (no_overloading, Inttab.update spec sps)));
-val empty = make_defs (Graph.empty, Symtab.empty);
+ val lhs' = make_item (c, if no_overloading then [] else args);
+ val rhs' = rhs |> map_filter (fn (c', T') =>
+ let val args' = const_typargs (c', T') in
+ if structs_less args' args then NONE
+ else SOME (make_item (c', if no_overloading_of defs c' then [] else args'))
+ end);
-fun merge pp
- (Defs {consts = consts1, specified = specified1},
- Defs {consts = consts2, specified = specified2}) =
- let
- val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
- handle Graph.CYCLES cycles => error (cyclic cycles);
- val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
- Inttab.fold (fn spec2 => fn specs1 =>
- (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1);
- in make_defs (consts', specified') end;
+ val insts' = insts
+ |> fold (fn Instance ca => Symtab.insert_list (op =) ca | _ => I) (lhs' :: rhs');
+ val deps' = deps
+ |> fold (fn r => declare_edge (r, lhs')) rhs'
+ |> propagate_deps insts'
+ handle Items.CYCLES cycles =>
+ if no_overloading then error (cycle_msg cycles)
+ else (warning (cycle_msg cycles ^ "\nUnchecked overloaded specification: " ^ name); deps);
+
+ in (specs', insts', deps') end);
end;