src/Pure/defs.ML
changeset 17803 e235a57651a1
parent 17712 46c2091e5187
child 17994 6a1a49cba5b3
     1.1 --- a/src/Pure/defs.ML	Sat Oct 08 22:39:40 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Sat Oct 08 22:39:41 2005 +0200
     1.3 @@ -40,12 +40,10 @@
     1.4    (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
     1.5      handle Type.TUNIFY => true;
     1.6  
     1.7 -fun check_specified c specified =
     1.8 -  specified |> Inttab.forall (fn (i, (a, T)) =>
     1.9 -    specified |> Inttab.forall (fn (j, (b, U)) =>
    1.10 -      i = j orelse disjoint_types T U orelse
    1.11 -        error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    1.12 -          " for constant " ^ quote c)));
    1.13 +fun check_specified c (i, (a, T)) = Inttab.forall (fn (j, (b, U)) =>
    1.14 +  i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
    1.15 +    error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    1.16 +      " for constant " ^ quote c));
    1.17  
    1.18  
    1.19  (* monomorphic constants *)
    1.20 @@ -77,14 +75,16 @@
    1.21        handle Graph.CYCLES cycles => err_cyclic cycles;
    1.22  
    1.23      val (c, T) = lhs;
    1.24 +    val spec = (serial (), (name, T));
    1.25      val no_overloading = Type.raw_instance (const_type c, T);
    1.26  
    1.27      val consts' =
    1.28        consts |> declare lhs |> fold declare rhs
    1.29        |> K no_overloading ? add_deps (c, map #1 rhs);
    1.30 -    val specified' =
    1.31 -      specified |> Symtab.default (c, Inttab.empty)
    1.32 -      |> Symtab.map_entry c (Inttab.update (serial (), (name, T)) #> tap (check_specified c));
    1.33 +    val specified' = specified
    1.34 +      |> Symtab.default (c, Inttab.empty)
    1.35 +      |> Symtab.map_entry c (fn specs =>
    1.36 +        (check_specified c spec specs; Inttab.update spec specs));
    1.37      val monomorphic' = monomorphic |> update_monomorphic specified' c;
    1.38    in (consts', specified', monomorphic') end);
    1.39  
    1.40 @@ -99,8 +99,9 @@
    1.41    let
    1.42      val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
    1.43        handle Graph.CYCLES cycles => err_cyclic cycles;
    1.44 -    val specified' = (specified1, specified2)
    1.45 -      |> Symtab.join (fn c => Inttab.merge (K true) #> tap (check_specified c) #> SOME);
    1.46 +    val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
    1.47 +      SOME (Inttab.fold (fn spec2 => fn specs1 =>
    1.48 +        (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1));
    1.49      val monomorphic' = monomorphic
    1.50        |> Symtab.fold (update_monomorphic specified' o #1) specified';
    1.51    in make_defs (consts', specified', monomorphic') end;