# HG changeset patch # User wenzelm # Date 1147450269 -7200 # Node ID 3b6629701a79eb839afa42ee8e8cdb4ba9aff192 # Parent 12e6cc4382ae3607c8f9a0925e6f1135c250ce24 tuned; diff -r 12e6cc4382ae -r 3b6629701a79 src/Pure/defs.ML --- a/src/Pure/defs.ML Fri May 12 11:19:41 2006 +0200 +++ b/src/Pure/defs.ML Fri May 12 18:11:09 2006 +0200 @@ -89,7 +89,7 @@ val empty = make_defs (Symtab.empty, Symtab.empty, Items.empty); -(* merge *) +(* disjoint specs *) fun disjoint_types T U = (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false) @@ -101,13 +101,15 @@ error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^ " for constant " ^ quote c)); + +(* merge *) + 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; - fun merge (Defs {specs = specs1, insts = insts1, deps = deps1}, Defs {specs = specs2, insts = insts2, deps = deps2}) = @@ -122,12 +124,15 @@ (* define *) +fun pure_args args = forall Term.is_TVar args andalso not (has_duplicates (op =) args); + 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 no_overloading = forall Term.is_TVar args andalso not (has_duplicates (op =) args); + val no_overloading = pure_args args; + val rec_args = (case args of [Type (_, Ts)] => if pure_args Ts then Ts else [] | _ => []); val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs}); val specs' = specs @@ -135,10 +140,10 @@ |> Symtab.map_entry c (fn (_, sps) => (disjoint_specs c spec sps; (no_overloading, Inttab.update spec sps))); - val lhs' = make_item (c, if no_overloading then [] else args); + val lhs' = make_item (c, args); val rhs' = rhs |> map_filter (fn (c', T') => let val args' = const_typargs (c', T') in - if forall Term.is_TVar args' then NONE + if gen_subset (op =) (args', rec_args) then NONE else SOME (make_item (c', if no_overloading_of defs c' then [] else args')) end);