# HG changeset patch
# User wenzelm
# Date 1147102806 -7200
# Node ID 12af4942923d0e5b727fb65327b4d8571bc36a5d
# Parent  d42149a01a0111b033d4f09f41803e4a26c30f8a
simple substructure test for typargs (independent type constructors);

diff -r d42149a01a01 -r 12af4942923d src/Pure/defs.ML
--- a/src/Pure/defs.ML	Mon May 08 17:40:05 2006 +0200
+++ b/src/Pure/defs.ML	Mon May 08 17:40:06 2006 +0200
@@ -2,18 +2,18 @@
     ID:         $Id$
     Author:     Makarius
 
-Global well-formedness checks for constant definitions.  Dependencies
-are only tracked for non-overloaded definitions!
+Global well-formedness checks for constant definitions -- covers
+dependencies of simple sub-structural overloading.
 *)
 
 signature DEFS =
 sig
   type T
-  val define: (string -> typ) -> bool -> string -> string ->
-    string * typ -> (string * typ) list -> T -> T
-  val empty: 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
 end
 
@@ -26,13 +26,16 @@
 type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list};
 
 datatype T = Defs of
- {consts: typ Graph.T,
-    (*constant declarations and dependencies*)
+ {consts: unit Graph.T,
   specified: spec Inttab.table Symtab.table};
 
 fun make_defs (consts, specified) = Defs {consts = consts, specified = specified};
 fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified));
 
+fun cyclic cycles =
+  "Cyclic dependency of constants:\n" ^
+    cat_lines (map (space_implode " -> " o map quote o rev) cycles);
+
 
 (* specified consts *)
 
@@ -47,29 +50,35 @@
         " for constant " ^ quote c));
 
 
+(* substructural type arguments *)
+
+fun struct_less T (Type (_, Us)) = exists (struct_le T) Us
+  | struct_less _ _ = false
+and struct_le T U = T = U orelse struct_less T U;
+
+fun structs_le Ts Us = forall (fn U => exists (fn T => struct_le T U) Ts) Us;
+fun structs_less Ts Us = Ts <> Us andalso structs_le Ts Us;
+
+
 (* define consts *)
 
-fun err_cyclic cycles =
-  error ("Cyclic dependency of constants:\n" ^
-    cat_lines (map (space_implode " -> " o map quote o rev) cycles));
-
-fun define const_type is_def module name lhs rhs = map_defs (fn (consts, specified) =>
+fun define const_typargs is_def module name lhs rhs = map_defs (fn (consts, specified) =>
   let
-    fun declare (a, _) = Graph.default_node (a, const_type a);
-    fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
-      handle Graph.CYCLES cycles => err_cyclic cycles;
+    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 (c, T) = lhs;
+    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 no_overloading = Type.raw_instance (const_type c, T);
-
-    val consts' =
-      consts |> declare lhs |> fold declare rhs
-      |> K no_overloading ? add_deps (c, map #1 rhs);
     val specified' = specified
       |> Symtab.default (c, Inttab.empty)
-      |> Symtab.map_entry c (fn specs =>
-        (check_specified c spec specs; Inttab.update spec specs));
+      |> 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 =
@@ -85,7 +94,7 @@
     Defs {consts = consts2, specified = specified2}) =
   let
     val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
-      handle Graph.CYCLES cycles => err_cyclic cycles;
+      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);