src/Pure/defs.ML
changeset 19628 de019ddcd89e
parent 19624 3b6629701a79
child 19692 bad13b32c0f3
     1.1 --- a/src/Pure/defs.ML	Sat May 13 02:51:35 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Sat May 13 02:51:37 2006 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val empty: T
     1.5    val merge: T * T -> T
     1.6    val define: (string * typ -> typ list) ->
     1.7 -    bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
     1.8 +    bool -> bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
     1.9  end
    1.10  
    1.11  structure Defs: DEFS =
    1.12 @@ -50,17 +50,12 @@
    1.13  
    1.14  structure Items = GraphFun(type key = item val ord = item_ord);
    1.15  
    1.16 -fun declare_edge (i, j) =
    1.17 -  Items.default_node (i, ()) #>
    1.18 -  Items.default_node (j, ()) #>
    1.19 -  Items.add_edge_acyclic (i, j);
    1.20 -
    1.21  fun propagate_deps insts deps =
    1.22    let
    1.23      fun inst_item (Constant c) = Symtab.lookup_list insts c
    1.24        | inst_item (Instance _) = [];
    1.25      fun inst_edge i j =
    1.26 -      fold declare_edge (tl (product (i :: inst_item i) (j :: inst_item j)));
    1.27 +      fold Items.add_edge_acyclic (tl (product (i :: inst_item i) (j :: inst_item j)));
    1.28    in Items.fold (fn (i, (_, (_, js))) => fold (inst_edge i) js) deps deps end;
    1.29  
    1.30  
    1.31 @@ -126,7 +121,7 @@
    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 +fun define const_typargs unchecked is_def module name lhs rhs defs = defs
    1.37      |> map_defs (fn (specs, insts, deps) =>
    1.38    let
    1.39      val (c, T) = lhs;
    1.40 @@ -134,27 +129,27 @@
    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 lhs' = make_item (c, args);
    1.45 +    val rhs' =
    1.46 +      if unchecked then []
    1.47 +      else rhs |> map_filter (fn (c', T') =>
    1.48 +        let val args' = const_typargs (c', T') in
    1.49 +          if gen_subset (op =) (args', rec_args) then NONE
    1.50 +          else SOME (make_item (c', if no_overloading_of defs c' then [] else args'))
    1.51 +        end);
    1.52 +
    1.53      val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs});
    1.54      val specs' = specs
    1.55        |> Symtab.default (c, (false, Inttab.empty))
    1.56        |> Symtab.map_entry c (fn (_, sps) =>
    1.57            (disjoint_specs c spec sps; (no_overloading, Inttab.update spec sps)));
    1.58 -
    1.59 -    val lhs' = make_item (c, args);
    1.60 -    val rhs' = rhs |> map_filter (fn (c', T') =>
    1.61 -      let val args' = const_typargs (c', T') in
    1.62 -        if gen_subset (op =) (args', rec_args) then NONE
    1.63 -        else SOME (make_item (c', if no_overloading_of defs c' then [] else args'))
    1.64 -      end);
    1.65 -
    1.66      val insts' = insts |> fold (fn i as Instance (c, _) =>
    1.67          Symtab.insert_list (op =) (c, i) | _ => I) (lhs' :: rhs');
    1.68      val deps' = deps
    1.69 -      |> fold (fn r => declare_edge (r, lhs')) rhs'
    1.70 +      |> fold (Items.default_node o rpair ()) (lhs' :: rhs')
    1.71 +      |> Items.add_deps_acyclic (lhs', rhs')
    1.72        |> propagate_deps insts'
    1.73 -      handle Items.CYCLES cycles =>
    1.74 -        if no_overloading then error (cycle_msg cycles)
    1.75 -        else (warning (cycle_msg cycles ^ "\nUnchecked overloaded specification: " ^ name); deps);
    1.76 +      handle Items.CYCLES cycles => error (cycle_msg cycles);
    1.77  
    1.78    in (specs', insts', deps') end);
    1.79