src/Pure/defs.ML
changeset 19624 3b6629701a79
parent 19620 ccd6de95f4a6
child 19628 de019ddcd89e
     1.1 --- a/src/Pure/defs.ML	Fri May 12 11:19:41 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Fri May 12 18:11:09 2006 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4  val empty = make_defs (Symtab.empty, Symtab.empty, Items.empty);
     1.5  
     1.6  
     1.7 -(* merge *)
     1.8 +(* disjoint specs *)
     1.9  
    1.10  fun disjoint_types T U =
    1.11    (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
    1.12 @@ -101,13 +101,15 @@
    1.13        error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    1.14          " for constant " ^ quote c));
    1.15  
    1.16 +
    1.17 +(* merge *)
    1.18 +
    1.19  fun cycle_msg css =
    1.20    let
    1.21      fun prt_cycle items = Pretty.block (flat
    1.22        (separate [Pretty.str " ->", Pretty.brk 1] (map (single o pretty_item) items)));
    1.23    in Pretty.string_of (Pretty.big_list "Cyclic dependency of constants:" (map prt_cycle css)) end;
    1.24  
    1.25 -
    1.26  fun merge
    1.27     (Defs {specs = specs1, insts = insts1, deps = deps1},
    1.28      Defs {specs = specs2, insts = insts2, deps = deps2}) =
    1.29 @@ -122,12 +124,15 @@
    1.30  
    1.31  (* define *)
    1.32  
    1.33 +fun pure_args args = forall Term.is_TVar args andalso not (has_duplicates (op =) args);
    1.34 +
    1.35  fun define const_typargs is_def module name lhs rhs defs = defs
    1.36      |> map_defs (fn (specs, insts, deps) =>
    1.37    let
    1.38      val (c, T) = lhs;
    1.39      val args = const_typargs lhs;
    1.40 -    val no_overloading = forall Term.is_TVar args andalso not (has_duplicates (op =) args);
    1.41 +    val no_overloading = pure_args args;
    1.42 +    val rec_args = (case args of [Type (_, Ts)] => if pure_args Ts then Ts else [] | _ => []);
    1.43  
    1.44      val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs});
    1.45      val specs' = specs
    1.46 @@ -135,10 +140,10 @@
    1.47        |> Symtab.map_entry c (fn (_, sps) =>
    1.48            (disjoint_specs c spec sps; (no_overloading, Inttab.update spec sps)));
    1.49  
    1.50 -    val lhs' = make_item (c, if no_overloading then [] else args);
    1.51 +    val lhs' = make_item (c, args);
    1.52      val rhs' = rhs |> map_filter (fn (c', T') =>
    1.53        let val args' = const_typargs (c', T') in
    1.54 -        if forall Term.is_TVar args' then NONE
    1.55 +        if gen_subset (op =) (args', rec_args) then NONE
    1.56          else SOME (make_item (c', if no_overloading_of defs c' then [] else args'))
    1.57        end);
    1.58