meaningful error message on failing merges of coercion tables
authortraytel
Sat Dec 17 15:53:58 2011 +0100 (2011-12-17)
changeset 4593532f769f94ea4
parent 45934 9321cd2572fe
child 45936 0724e56b5dea
meaningful error message on failing merges of coercion tables
src/Tools/subtyping.ML
     1.1 --- a/src/Tools/subtyping.ML	Tue Dec 20 11:40:56 2011 +0100
     1.2 +++ b/src/Tools/subtyping.ML	Sat Dec 17 15:53:58 2011 +0100
     1.3 @@ -32,6 +32,14 @@
     1.4  fun make_data (coes, full_graph, coes_graph, tmaps) =
     1.5    Data {coes = coes, full_graph = full_graph, coes_graph = coes_graph, tmaps = tmaps};
     1.6  
     1.7 +fun merge_error_coes (a, b) =
     1.8 +  error ("Cannot merge coercion tables.\nConflicting declarations for coercions from " ^
     1.9 +    quote a ^ " to " ^ quote b ^ ".");
    1.10 +
    1.11 +fun merge_error_tmaps C =
    1.12 +  error ("Cannot merge coercion map tables.\nConflicting declarations for the constructor " ^
    1.13 +    quote C ^ ".");
    1.14 +
    1.15  structure Data = Generic_Data
    1.16  (
    1.17    type T = data;
    1.18 @@ -42,10 +50,11 @@
    1.19        Data {coes = coes2, full_graph = full_graph2, coes_graph = coes_graph2, tmaps = tmaps2}) =
    1.20      make_data (Symreltab.merge (eq_pair (op aconv)
    1.21          (eq_pair (eq_pair (eq_list (op =)) (eq_list (op =))) (eq_list (op aconv))))
    1.22 -        (coes1, coes2),
    1.23 +        (coes1, coes2) handle Symreltab.DUP key => merge_error_coes key,
    1.24        Graph.merge (op =) (full_graph1, full_graph2),
    1.25        Graph.merge (op =) (coes_graph1, coes_graph2),
    1.26 -      Symtab.merge (eq_pair (op aconv) (op =)) (tmaps1, tmaps2));
    1.27 +      Symtab.merge (eq_pair (op aconv) (op =)) (tmaps1, tmaps2)
    1.28 +        handle Symtab.DUP key => merge_error_tmaps key);
    1.29  );
    1.30  
    1.31  fun map_data f =