src/Pure/defs.ML
changeset 19590 12af4942923d
parent 19569 1c23356a8ea8
child 19613 9bf274ec94cf
     1.1 --- a/src/Pure/defs.ML	Mon May 08 17:40:05 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Mon May 08 17:40:06 2006 +0200
     1.3 @@ -2,18 +2,18 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Global well-formedness checks for constant definitions.  Dependencies
     1.8 -are only tracked for non-overloaded definitions!
     1.9 +Global well-formedness checks for constant definitions -- covers
    1.10 +dependencies of simple sub-structural overloading.
    1.11  *)
    1.12  
    1.13  signature DEFS =
    1.14  sig
    1.15    type T
    1.16 -  val define: (string -> typ) -> bool -> string -> string ->
    1.17 -    string * typ -> (string * typ) list -> T -> T
    1.18 -  val empty: T
    1.19 +  val define: (string * typ -> typ list) ->
    1.20 +    bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
    1.21    val specifications_of: T -> string ->
    1.22     (serial * {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}) list
    1.23 +  val empty: T
    1.24    val merge: Pretty.pp -> T * T -> T
    1.25  end
    1.26  
    1.27 @@ -26,13 +26,16 @@
    1.28  type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list};
    1.29  
    1.30  datatype T = Defs of
    1.31 - {consts: typ Graph.T,
    1.32 -    (*constant declarations and dependencies*)
    1.33 + {consts: unit Graph.T,
    1.34    specified: spec Inttab.table Symtab.table};
    1.35  
    1.36  fun make_defs (consts, specified) = Defs {consts = consts, specified = specified};
    1.37  fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified));
    1.38  
    1.39 +fun cyclic cycles =
    1.40 +  "Cyclic dependency of constants:\n" ^
    1.41 +    cat_lines (map (space_implode " -> " o map quote o rev) cycles);
    1.42 +
    1.43  
    1.44  (* specified consts *)
    1.45  
    1.46 @@ -47,29 +50,35 @@
    1.47          " for constant " ^ quote c));
    1.48  
    1.49  
    1.50 +(* substructural type arguments *)
    1.51 +
    1.52 +fun struct_less T (Type (_, Us)) = exists (struct_le T) Us
    1.53 +  | struct_less _ _ = false
    1.54 +and struct_le T U = T = U orelse struct_less T U;
    1.55 +
    1.56 +fun structs_le Ts Us = forall (fn U => exists (fn T => struct_le T U) Ts) Us;
    1.57 +fun structs_less Ts Us = Ts <> Us andalso structs_le Ts Us;
    1.58 +
    1.59 +
    1.60  (* define consts *)
    1.61  
    1.62 -fun err_cyclic cycles =
    1.63 -  error ("Cyclic dependency of constants:\n" ^
    1.64 -    cat_lines (map (space_implode " -> " o map quote o rev) cycles));
    1.65 -
    1.66 -fun define const_type is_def module name lhs rhs = map_defs (fn (consts, specified) =>
    1.67 +fun define const_typargs is_def module name lhs rhs = map_defs (fn (consts, specified) =>
    1.68    let
    1.69 -    fun declare (a, _) = Graph.default_node (a, const_type a);
    1.70 -    fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
    1.71 -      handle Graph.CYCLES cycles => err_cyclic cycles;
    1.72 +    val (c, T) = lhs;
    1.73 +    val args = const_typargs lhs;
    1.74 +    val deps = rhs |> map_filter (fn d =>
    1.75 +      if structs_less (const_typargs d) args then NONE else SOME (#1 d));
    1.76 +    val no_overloading = forall Term.is_TVar args andalso not (has_duplicates (op =) args);
    1.77  
    1.78 -    val (c, T) = lhs;
    1.79 +    val consts' = fold (fn (a, _) => Graph.default_node (a, ())) (lhs :: rhs) consts;
    1.80 +    val consts'' = Graph.add_deps_acyclic (c, deps) consts' handle Graph.CYCLES cycles =>
    1.81 +      if no_overloading then error (cyclic cycles)
    1.82 +      else (warning (cyclic cycles ^ "\nUnchecked overloaded specification: " ^ name); consts');
    1.83 +
    1.84      val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs});
    1.85 -    val no_overloading = Type.raw_instance (const_type c, T);
    1.86 -
    1.87 -    val consts' =
    1.88 -      consts |> declare lhs |> fold declare rhs
    1.89 -      |> K no_overloading ? add_deps (c, map #1 rhs);
    1.90      val specified' = specified
    1.91        |> Symtab.default (c, Inttab.empty)
    1.92 -      |> Symtab.map_entry c (fn specs =>
    1.93 -        (check_specified c spec specs; Inttab.update spec specs));
    1.94 +      |> Symtab.map_entry c (fn specs => (check_specified c spec specs; Inttab.update spec specs));
    1.95    in (consts', specified') end);
    1.96  
    1.97  fun specifications_of (Defs {specified, ...}) c =
    1.98 @@ -85,7 +94,7 @@
    1.99      Defs {consts = consts2, specified = specified2}) =
   1.100    let
   1.101      val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
   1.102 -      handle Graph.CYCLES cycles => err_cyclic cycles;
   1.103 +      handle Graph.CYCLES cycles => error (cyclic cycles);
   1.104      val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
   1.105        Inttab.fold (fn spec2 => fn specs1 =>
   1.106          (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1);