author  blanchet 
Mon, 26 Nov 2012 13:35:05 +0100  
changeset 50222  40e3c3be6bca 
parent 49660  de49d9b4d7bc 
child 51246  755562fd2d9d 
permissions  rwrr 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

1 
(* Title: Tools/subtyping.ML 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

2 
Author: Dmitriy Traytel, TU Muenchen 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

3 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

4 
Coercive subtyping via subtype constraints. 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

5 
*) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

6 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

7 
signature SUBTYPING = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

8 
sig 
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset

9 
val coercion_enabled: bool Config.T 
40284
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

10 
val add_type_map: term > Context.generic > Context.generic 
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

11 
val add_coercion: term > Context.generic > Context.generic 
45059  12 
val print_coercions: Proof.context > unit 
13 
val print_coercion_maps: Proof.context > unit 

40283  14 
val setup: theory > theory 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

15 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

16 

40283  17 
structure Subtyping: SUBTYPING = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

18 
struct 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

19 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

20 
(** coercions data **) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

21 

41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

22 
datatype variance = COVARIANT  CONTRAVARIANT  INVARIANT  INVARIANT_TO of typ; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

23 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

24 
datatype data = Data of 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

25 
{coes: (term * ((typ list * typ list) * term list)) Symreltab.table, (*coercions table*) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

26 
(*full coercions graph  only used at coercion declaration/deletion*) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

27 
full_graph: int Graph.T, 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

28 
(*coercions graph restricted to base types  for efficiency reasons strored in the context*) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

29 
coes_graph: int Graph.T, 
40282  30 
tmaps: (term * variance list) Symtab.table}; (*map functions*) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

31 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

32 
fun make_data (coes, full_graph, coes_graph, tmaps) = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

33 
Data {coes = coes, full_graph = full_graph, coes_graph = coes_graph, tmaps = tmaps}; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

34 

45935
32f769f94ea4
meaningful error message on failing merges of coercion tables
traytel
parents:
45429
diff
changeset

35 
fun merge_error_coes (a, b) = 
32f769f94ea4
meaningful error message on failing merges of coercion tables
traytel
parents:
45429
diff
changeset

36 
error ("Cannot merge coercion tables.\nConflicting declarations for coercions from " ^ 
32f769f94ea4
meaningful error message on failing merges of coercion tables
traytel
parents:
45429
diff
changeset

37 
quote a ^ " to " ^ quote b ^ "."); 
32f769f94ea4
meaningful error message on failing merges of coercion tables
traytel
parents:
45429
diff
changeset

38 

32f769f94ea4
meaningful error message on failing merges of coercion tables
traytel
parents:
45429
diff
changeset

39 
fun merge_error_tmaps C = 
32f769f94ea4
meaningful error message on failing merges of coercion tables
traytel
parents:
45429
diff
changeset

40 
error ("Cannot merge coercion map tables.\nConflicting declarations for the constructor " ^ 
32f769f94ea4
meaningful error message on failing merges of coercion tables
traytel
parents:
45429
diff
changeset

41 
quote C ^ "."); 
32f769f94ea4
meaningful error message on failing merges of coercion tables
traytel
parents:
45429
diff
changeset

42 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

43 
structure Data = Generic_Data 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

44 
( 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

45 
type T = data; 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

46 
val empty = make_data (Symreltab.empty, Graph.empty, Graph.empty, Symtab.empty); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

47 
val extend = I; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

48 
fun merge 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

49 
(Data {coes = coes1, full_graph = full_graph1, coes_graph = coes_graph1, tmaps = tmaps1}, 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

50 
Data {coes = coes2, full_graph = full_graph2, coes_graph = coes_graph2, tmaps = tmaps2}) = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

51 
make_data (Symreltab.merge (eq_pair (op aconv) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

52 
(eq_pair (eq_pair (eq_list (op =)) (eq_list (op =))) (eq_list (op aconv)))) 
45935
32f769f94ea4
meaningful error message on failing merges of coercion tables
traytel
parents:
45429
diff
changeset

53 
(coes1, coes2) handle Symreltab.DUP key => merge_error_coes key, 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

54 
Graph.merge (op =) (full_graph1, full_graph2), 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

55 
Graph.merge (op =) (coes_graph1, coes_graph2), 
45935
32f769f94ea4
meaningful error message on failing merges of coercion tables
traytel
parents:
45429
diff
changeset

56 
Symtab.merge (eq_pair (op aconv) (op =)) (tmaps1, tmaps2) 
32f769f94ea4
meaningful error message on failing merges of coercion tables
traytel
parents:
45429
diff
changeset

57 
handle Symtab.DUP key => merge_error_tmaps key); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

58 
); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

59 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

60 
fun map_data f = 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

61 
Data.map (fn Data {coes, full_graph, coes_graph, tmaps} => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

62 
make_data (f (coes, full_graph, coes_graph, tmaps))); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

63 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

64 
fun map_coes f = 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

65 
map_data (fn (coes, full_graph, coes_graph, tmaps) => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

66 
(f coes, full_graph, coes_graph, tmaps)); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

67 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

68 
fun map_coes_graph f = 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

69 
map_data (fn (coes, full_graph, coes_graph, tmaps) => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

70 
(coes, full_graph, f coes_graph, tmaps)); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

71 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

72 
fun map_coes_and_graphs f = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

73 
map_data (fn (coes, full_graph, coes_graph, tmaps) => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

74 
let val (coes', full_graph', coes_graph') = f (coes, full_graph, coes_graph); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

75 
in (coes', full_graph', coes_graph', tmaps) end); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

76 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

77 
fun map_tmaps f = 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

78 
map_data (fn (coes, full_graph, coes_graph, tmaps) => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

79 
(coes, full_graph, coes_graph, f tmaps)); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

80 

40285  81 
val rep_data = (fn Data args => args) o Data.get o Context.Proof; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

82 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

83 
val coes_of = #coes o rep_data; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

84 
val coes_graph_of = #coes_graph o rep_data; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

85 
val tmaps_of = #tmaps o rep_data; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

86 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

87 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

88 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

89 
(** utils **) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

90 

46614
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
45935
diff
changeset

91 
fun restrict_graph G = Graph.restrict (fn x => Graph.get_node G x = 0) G; 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

92 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

93 
fun nameT (Type (s, [])) = s; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

94 
fun t_of s = Type (s, []); 
40286  95 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

96 
fun sort_of (TFree (_, S)) = SOME S 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

97 
 sort_of (TVar (_, S)) = SOME S 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

98 
 sort_of _ = NONE; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

99 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

100 
val is_typeT = fn (Type _) => true  _ => false; 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

101 
val is_stypeT = fn (Type (_, [])) => true  _ => false; 
40282  102 
val is_compT = fn (Type (_, _ :: _)) => true  _ => false; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

103 
val is_freeT = fn (TFree _) => true  _ => false; 
40286  104 
val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi)  _ => false; 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

105 
val is_funtype = fn (Type ("fun", [_, _])) => true  _ => false; 
43591
d4cbd6feffdf
collapse map functions with identity subcoercions to identities;
traytel
parents:
43278
diff
changeset

106 
val is_identity = fn (Abs (_, _, Bound 0)) => true  _ => false; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

107 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

108 
fun instantiate t Ts = Term.subst_TVars 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

109 
((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts) t; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

110 

9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

111 
exception COERCION_GEN_ERROR of unit > string; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

112 

9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

113 
fun inst_collect tye err T U = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

114 
(case (T, Type_Infer.deref tye U) of 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

115 
(TVar (xi, S), U) => [(xi, U)] 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

116 
 (Type (a, Ts), Type (b, Us)) => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

117 
if a <> b then raise error (err ()) else inst_collects tye err Ts Us 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

118 
 (_, U') => if T <> U' then error (err ()) else []) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

119 
and inst_collects tye err Ts Us = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

120 
fold2 (fn T => fn U => fn is => inst_collect tye err T U @ is) Ts Us []; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

121 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

122 

40836  123 
(* unification *) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

124 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

125 
exception NO_UNIFIER of string * typ Vartab.table; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

126 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

127 
fun unify weak ctxt = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

128 
let 
42361  129 
val thy = Proof_Context.theory_of ctxt; 
42386  130 
val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

131 

40282  132 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

133 
(* adjust sorts of parameters *) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

134 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

135 
fun not_of_sort x S' S = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

136 
"Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^ 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

137 
Syntax.string_of_sort ctxt S; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

138 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

139 
fun meet (_, []) tye_idx = tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

140 
 meet (Type (a, Ts), S) (tye_idx as (tye, _)) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

141 
meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

142 
 meet (TFree (x, S'), S) (tye_idx as (tye, _)) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

143 
if Sign.subsort thy (S', S) then tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

144 
else raise NO_UNIFIER (not_of_sort x S' S, tye) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

145 
 meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

146 
if Sign.subsort thy (S', S) then tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

147 
else if Type_Infer.is_param xi then 
40286  148 
(Vartab.update_new 
149 
(xi, Type_Infer.mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1) 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

150 
else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

151 
and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = 
40286  152 
meets (Ts, Ss) (meet (Type_Infer.deref tye T, S) tye_idx) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

153 
 meets _ tye_idx = tye_idx; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

154 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

155 
val weak_meet = if weak then fn _ => I else meet 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

156 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

157 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

158 
(* occurs check and assignment *) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

159 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

160 
fun occurs_check tye xi (TVar (xi', _)) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

161 
if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

162 
else 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

163 
(case Vartab.lookup tye xi' of 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

164 
NONE => () 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

165 
 SOME T => occurs_check tye xi T) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

166 
 occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

167 
 occurs_check _ _ _ = (); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

168 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

169 
fun assign xi (T as TVar (xi', _)) S env = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

170 
if xi = xi' then env 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

171 
else env > weak_meet (T, S) >> Vartab.update_new (xi, T) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

172 
 assign xi T S (env as (tye, _)) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

173 
(occurs_check tye xi T; env > weak_meet (T, S) >> Vartab.update_new (xi, T)); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

174 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

175 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

176 
(* unification *) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

177 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

178 
fun show_tycon (a, Ts) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

179 
quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

180 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

181 
fun unif (T1, T2) (env as (tye, _)) = 
40286  182 
(case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

183 
((true, TVar (xi, S)), (_, T)) => assign xi T S env 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

184 
 ((_, T), (true, TVar (xi, S))) => assign xi T S env 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

185 
 ((_, Type (a, Ts)), (_, Type (b, Us))) => 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

186 
if weak andalso null Ts andalso null Us then env 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

187 
else if a <> b then 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

188 
raise NO_UNIFIER 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

189 
("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

190 
else fold unif (Ts ~~ Us) env 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

191 
 ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye)); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

192 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

193 
in unif end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

194 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

195 
val weak_unify = unify true; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

196 
val strong_unify = unify false; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

197 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

198 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

199 
(* Typ_Graph shortcuts *) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

200 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

201 
fun get_preds G T = Typ_Graph.all_preds G [T]; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

202 
fun get_succs G T = Typ_Graph.all_succs G [T]; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

203 
fun maybe_new_typnode T G = perhaps (try (Typ_Graph.new_node (T, ()))) G; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

204 
fun maybe_new_typnodes Ts G = fold maybe_new_typnode Ts G; 
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists  order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
43591
diff
changeset

205 
fun new_imm_preds G Ts = (* FIXME inefficient *) 
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists  order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
43591
diff
changeset

206 
subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_preds G) Ts)); 
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists  order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
43591
diff
changeset

207 
fun new_imm_succs G Ts = (* FIXME inefficient *) 
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists  order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
43591
diff
changeset

208 
subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_succs G) Ts)); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

209 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

210 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

211 
(* Graph shortcuts *) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

212 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

213 
fun maybe_new_node s G = perhaps (try (Graph.new_node s)) G 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

214 
fun maybe_new_nodes ss G = fold maybe_new_node ss G 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

215 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

216 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

217 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

218 
(** error messages **) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

219 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

220 
infixr ++> (* lazy error msg composition *) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

221 

9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

222 
fun err ++> str = err #> suffix str 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

223 

42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

224 
fun gen_msg err msg = 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

225 
err () ^ "\nNow trying to infer coercions globally.\n\nCoercion inference failed" ^ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

226 
(if msg = "" then "" else ":\n" ^ msg) ^ "\n"; 
40836  227 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

228 
fun prep_output ctxt tye bs ts Ts = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

229 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

230 
val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

231 
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

232 
fun prep t = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

233 
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) 
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
49564
diff
changeset

234 
in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

235 
in (map prep ts', Ts') end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

236 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

237 
fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

238 

40836  239 
fun unif_failed msg = 
240 
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n"; 

42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

241 

40836  242 
fun err_appl_msg ctxt msg tye bs t T u U () = 
243 
let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U] 

42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

244 
in unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n" end; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

245 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

246 
fun err_list ctxt msg tye Ts = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

247 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

248 
val (_, Ts') = prep_output ctxt tye [] [] Ts; 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

249 
val text = 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

250 
msg ^ "\nCannot unify a list of types that should be the same:\n" ^ 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

251 
Pretty.string_of (Pretty.list "[" "]" (map (Syntax.pretty_typ ctxt) Ts')); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

252 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

253 
error text 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

254 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

255 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

256 
fun err_bound ctxt msg tye packs = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

257 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

258 
val (ts, Ts) = fold 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

259 
(fn (bs, t $ u, U, _, U') => fn (ts, Ts) => 
40836  260 
let val (t', T') = prep_output ctxt tye bs [t, u] [U', U] 
40282  261 
in (t' :: ts, T' :: Ts) end) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

262 
packs ([], []); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

263 
val text = msg ^ "\n" ^ Pretty.string_of ( 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

264 
Pretty.big_list "Cannot fulfil subtype constraints:" 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

265 
(map2 (fn [t, u] => fn [T, U] => 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

266 
Pretty.block [ 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

267 
Syntax.pretty_typ ctxt T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

268 
Syntax.pretty_typ ctxt U, Pretty.brk 3, 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

269 
Pretty.str "from function application", Pretty.brk 2, 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

270 
Pretty.block [Syntax.pretty_term ctxt (t $ u)]]) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

271 
ts Ts)) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

272 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

273 
error text 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

274 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

275 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

276 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

277 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

278 
(** constraint generation **) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

279 

40836  280 
fun generate_constraints ctxt err = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

281 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

282 
fun gen cs _ (Const (_, T)) tye_idx = (T, tye_idx, cs) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

283 
 gen cs _ (Free (_, T)) tye_idx = (T, tye_idx, cs) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

284 
 gen cs _ (Var (_, T)) tye_idx = (T, tye_idx, cs) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

285 
 gen cs bs (Bound i) tye_idx = 
43278  286 
(snd (nth bs i handle General.Subscript => err_loose i), tye_idx, cs) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

287 
 gen cs bs (Abs (x, T, t)) tye_idx = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

288 
let val (U, tye_idx', cs') = gen cs ((x, T) :: bs) t tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

289 
in (T > U, tye_idx', cs') end 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

290 
 gen cs bs (t $ u) tye_idx = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

291 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

292 
val (T, tye_idx', cs') = gen cs bs t tye_idx; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

293 
val (U', (tye, idx), cs'') = gen cs' bs u tye_idx'; 
40286  294 
val U = Type_Infer.mk_param idx []; 
295 
val V = Type_Infer.mk_param (idx + 1) []; 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

296 
val tye_idx'' = strong_unify ctxt (U > V, T) (tye, idx + 2) 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

297 
handle NO_UNIFIER (msg, _) => error (gen_msg err msg); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

298 
val error_pack = (bs, t $ u, U, V, U'); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

299 
in (V, (tye_idx''), 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

300 
((U', U), error_pack) :: cs'') end; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

301 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

302 
gen [] [] 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

303 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

304 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

305 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

306 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

307 
(** constraint resolution **) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

308 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

309 
exception BOUND_ERROR of string; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

310 

40836  311 
fun process_constraints ctxt err cs tye_idx = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

312 
let 
42388  313 
val thy = Proof_Context.theory_of ctxt; 
314 

40285  315 
val coes_graph = coes_graph_of ctxt; 
316 
val tmaps = tmaps_of ctxt; 

42388  317 
val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

318 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

319 
fun split_cs _ [] = ([], []) 
40282  320 
 split_cs f (c :: cs) = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

321 
(case pairself f (fst c) of 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

322 
(false, false) => apsnd (cons c) (split_cs f cs) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

323 
 _ => apfst (cons c) (split_cs f cs)); 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

324 

41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

325 
fun unify_list (T :: Ts) tye_idx = 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

326 
fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

327 

40282  328 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

329 
(* check whether constraint simplification will terminate using weak unification *) 
40282  330 

41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

331 
val _ = fold (fn (TU, _) => fn tye_idx => 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

332 
weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, _) => 
40836  333 
error (gen_msg err ("weak unification of subtype constraints fails\n" ^ msg))) cs tye_idx; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

334 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

335 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

336 
(* simplify constraints *) 
40282  337 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

338 
fun simplify_constraints cs tye_idx = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

339 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

340 
fun contract a Ts Us error_pack done todo tye idx = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

341 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

342 
val arg_var = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

343 
(case Symtab.lookup tmaps a of 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

344 
(*everything is invariant for unknown constructors*) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

345 
NONE => replicate (length Ts) INVARIANT 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

346 
 SOME av => snd av); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

347 
fun new_constraints (variance, constraint) (cs, tye_idx) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

348 
(case variance of 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

349 
COVARIANT => (constraint :: cs, tye_idx) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

350 
 CONTRAVARIANT => (swap constraint :: cs, tye_idx) 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

351 
 INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

352 
handle NO_UNIFIER (msg, _) => 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

353 
err_list ctxt (gen_msg err 
45059  354 
"failed to unify invariant arguments w.r.t. to the known map function" ^ msg) 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

355 
(fst tye_idx) (T :: Ts)) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

356 
 INVARIANT => (cs, strong_unify ctxt constraint tye_idx 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

357 
handle NO_UNIFIER (msg, _) => 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

358 
error (gen_msg err ("failed to unify invariant arguments" ^ msg)))); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

359 
val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack)) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

360 
(fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx))); 
49142
0f81eca1e473
more conservative rechecking of processed constraints in subtyping constraint simplification
traytel
parents:
47060
diff
changeset

361 
val test_update = is_typeT orf is_freeT orf is_fixedvarT; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

362 
val (ch, done') = 
40286  363 
if not (null new) then ([], done) 
364 
else split_cs (test_update o Type_Infer.deref tye') done; 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

365 
val todo' = ch @ todo; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

366 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

367 
simplify done' (new @ todo') (tye', idx') 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

368 
end 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

369 
(*xi is definitely a parameter*) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

370 
and expand varleq xi S a Ts error_pack done todo tye idx = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

371 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

372 
val n = length Ts; 
40286  373 
val args = map2 Type_Infer.mk_param (idx upto idx + n  1) (arity_sorts a S); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

374 
val tye' = Vartab.update_new (xi, Type(a, args)) tye; 
40286  375 
val (ch, done') = split_cs (is_compT o Type_Infer.deref tye') done; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

376 
val todo' = ch @ todo; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

377 
val new = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

378 
if varleq then (Type(a, args), Type (a, Ts)) 
40286  379 
else (Type (a, Ts), Type (a, args)); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

380 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

381 
simplify done' ((new, error_pack) :: todo') (tye', idx + n) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

382 
end 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

383 
(*TU is a pair of a parameter and a free/fixed variable*) 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

384 
and eliminate TU done todo tye idx = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

385 
let 
40286  386 
val [TVar (xi, S)] = filter Type_Infer.is_paramT TU; 
387 
val [T] = filter_out Type_Infer.is_paramT TU; 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

388 
val SOME S' = sort_of T; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

389 
val test_update = if is_freeT T then is_freeT else is_fixedvarT; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

390 
val tye' = Vartab.update_new (xi, T) tye; 
40286  391 
val (ch, done') = split_cs (test_update o Type_Infer.deref tye') done; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

392 
val todo' = ch @ todo; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

393 
in 
42388  394 
if Sign.subsort thy (S', S) (*TODO check this*) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

395 
then simplify done' todo' (tye', idx) 
40836  396 
else error (gen_msg err "sort mismatch") 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

397 
end 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

398 
and simplify done [] tye_idx = (done, tye_idx) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

399 
 simplify done (((T, U), error_pack) :: todo) (tye_idx as (tye, idx)) = 
40286  400 
(case (Type_Infer.deref tye T, Type_Infer.deref tye U) of 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

401 
(T1 as Type (a, []), T2 as Type (b, [])) => 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

402 
if a = b then simplify done todo tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

403 
else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

404 
else error (gen_msg err (quote (Syntax.string_of_typ ctxt T1) ^ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

405 
" is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2))) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

406 
 (Type (a, Ts), Type (b, Us)) => 
40836  407 
if a <> b then error (gen_msg err "different constructors") 
408 
(fst tye_idx) error_pack 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

409 
else contract a Ts Us error_pack done todo tye idx 
40282  410 
 (TVar (xi, S), Type (a, Ts as (_ :: _))) => 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

411 
expand true xi S a Ts error_pack done todo tye idx 
40282  412 
 (Type (a, Ts as (_ :: _)), TVar (xi, S)) => 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

413 
expand false xi S a Ts error_pack done todo tye idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

414 
 (T, U) => 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

415 
if T = U then simplify done todo tye_idx 
40282  416 
else if exists (is_freeT orf is_fixedvarT) [T, U] andalso 
40286  417 
exists Type_Infer.is_paramT [T, U] 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

418 
then eliminate [T, U] done todo tye idx 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

419 
else if exists (is_freeT orf is_fixedvarT) [T, U] 
40836  420 
then error (gen_msg err "not eliminated free/fixed variables") 
40282  421 
else simplify (((T, U), error_pack) :: done) todo tye_idx); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

422 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

423 
simplify [] cs tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

424 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

425 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

426 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

427 
(* do simplification *) 
40282  428 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

429 
val (cs', tye_idx') = simplify_constraints cs tye_idx; 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

430 

0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

431 
fun find_error_pack lower T' = map_filter 
40836  432 
(fn ((T, U), pack) => if if lower then T' = U else T' = T then SOME pack else NONE) cs'; 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

433 

0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

434 
fun find_cycle_packs nodes = 
40836  435 
let 
436 
val (but_last, last) = split_last nodes 

437 
val pairs = (last, hd nodes) :: (but_last ~~ tl nodes); 

438 
in 

439 
map_filter 

40838  440 
(fn (TU, pack) => if member (op =) pairs TU then SOME pack else NONE) 
40836  441 
cs' 
442 
end; 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

443 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

444 
(*styps stands either for supertypes or for subtypes of a type T 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

445 
in terms of the subtyperelation (excluding T itself)*) 
40282  446 
fun styps super T = 
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists  order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
43591
diff
changeset

447 
(if super then Graph.immediate_succs else Graph.immediate_preds) coes_graph T 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

448 
handle Graph.UNDEF _ => []; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

449 

40282  450 
fun minmax sup (T :: Ts) = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

451 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

452 
fun adjust T U = if sup then (T, U) else (U, T); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

453 
fun extract T [] = T 
40282  454 
 extract T (U :: Us) = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

455 
if Graph.is_edge coes_graph (adjust T U) then extract T Us 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

456 
else if Graph.is_edge coes_graph (adjust U T) then extract U Us 
40836  457 
else raise BOUND_ERROR "uncomparable types in type list"; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

458 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

459 
t_of (extract T Ts) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

460 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

461 

40282  462 
fun ex_styp_of_sort super T styps_and_sorts = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

463 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

464 
fun adjust T U = if super then (T, U) else (U, T); 
40282  465 
fun styp_test U Ts = forall 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

466 
(fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts; 
42388  467 
fun fitting Ts S U = Sign.of_sort thy (t_of U, S) andalso styp_test U Ts 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

468 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

469 
forall (fn (Ts, S) => exists (fitting Ts S) (T :: styps super T)) styps_and_sorts 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

470 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

471 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

472 
(* computes the tightest possible, correct assignment for 'a::S 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

473 
e.g. in the supremum case (sup = true): 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

474 
 'a::S 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

475 
/ / \ \ 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

476 
/ / \ \ 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

477 
'b::C1 'c::C2 ... T1 T2 ... 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

478 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

479 
sorts  list of sorts [C1, C2, ...] 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

480 
T::Ts  nonempty list of base types [T1, T2, ...] 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

481 
*) 
40282  482 
fun tightest sup S styps_and_sorts (T :: Ts) = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

483 
let 
42388  484 
fun restriction T = Sign.of_sort thy (t_of T, S) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

485 
andalso ex_styp_of_sort (not sup) T styps_and_sorts; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

486 
fun candidates T = inter (op =) (filter restriction (T :: styps sup T)); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

487 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

488 
(case fold candidates Ts (filter restriction (T :: styps sup T)) of 
40836  489 
[] => raise BOUND_ERROR ("no " ^ (if sup then "supremum" else "infimum")) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

490 
 [T] => t_of T 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

491 
 Ts => minmax sup Ts) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

492 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

493 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

494 
fun build_graph G [] tye_idx = (G, tye_idx) 
40282  495 
 build_graph G ((T, U) :: cs) tye_idx = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

496 
if T = U then build_graph G cs tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

497 
else 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

498 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

499 
val G' = maybe_new_typnodes [T, U] G; 
45059  500 
val (G'', tye_idx') = (Typ_Graph.add_edge_acyclic (T, U) G', tye_idx) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

501 
handle Typ_Graph.CYCLES cycles => 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

502 
let 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

503 
val (tye, idx) = 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

504 
fold 
40836  505 
(fn cycle => fn tye_idx' => (unify_list cycle tye_idx' 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

506 
handle NO_UNIFIER (msg, _) => 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

507 
err_bound ctxt 
40836  508 
(gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx) 
509 
(find_cycle_packs cycle))) 

510 
cycles tye_idx 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

511 
in 
40836  512 
collapse (tye, idx) cycles G 
513 
end 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

514 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

515 
build_graph G'' cs tye_idx' 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

516 
end 
40836  517 
and collapse (tye, idx) cycles G = (*nodes nonempty list*) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

518 
let 
40836  519 
(*all cycles collapse to one node, 
520 
because all of them share at least the nodes x and y*) 

521 
val nodes = (distinct (op =) (flat cycles)); 

522 
val T = Type_Infer.deref tye (hd nodes); 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

523 
val P = new_imm_preds G nodes; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

524 
val S = new_imm_succs G nodes; 
46665
919dfcdf6d8a
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
wenzelm
parents:
46614
diff
changeset

525 
val G' = fold Typ_Graph.del_node (tl nodes) G; 
40836  526 
fun check_and_gen super T' = 
527 
let val U = Type_Infer.deref tye T'; 

528 
in 

529 
if not (is_typeT T) orelse not (is_typeT U) orelse T = U 

530 
then if super then (hd nodes, T') else (T', hd nodes) 

42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

531 
else 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

532 
if super andalso 
40836  533 
Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T') 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

534 
else if not super andalso 
40836  535 
Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes) 
536 
else err_bound ctxt (gen_msg err "cycle elimination produces inconsistent graph") 

42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

537 
(fst tye_idx) 
40836  538 
(maps find_cycle_packs cycles @ find_error_pack super T') 
539 
end; 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

540 
in 
40836  541 
build_graph G' (map (check_and_gen false) P @ map (check_and_gen true) S) (tye, idx) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

542 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

543 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

544 
fun assign_bound lower G key (tye_idx as (tye, _)) = 
40286  545 
if Type_Infer.is_paramT (Type_Infer.deref tye key) then 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

546 
let 
40286  547 
val TVar (xi, S) = Type_Infer.deref tye key; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

548 
val get_bound = if lower then get_preds else get_succs; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

549 
val raw_bound = get_bound G key; 
40286  550 
val bound = map (Type_Infer.deref tye) raw_bound; 
551 
val not_params = filter_out Type_Infer.is_paramT bound; 

40282  552 
fun to_fulfil T = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

553 
(case sort_of T of 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

554 
NONE => NONE 
40282  555 
 SOME S => 
40286  556 
SOME 
557 
(map nameT 

42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42402
diff
changeset

558 
(filter_out Type_Infer.is_paramT 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42402
diff
changeset

559 
(map (Type_Infer.deref tye) (get_bound G T))), S)); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

560 
val styps_and_sorts = distinct (op =) (map_filter to_fulfil raw_bound); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

561 
val assignment = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

562 
if null bound orelse null not_params then NONE 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

563 
else SOME (tightest lower S styps_and_sorts (map nameT not_params) 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

564 
handle BOUND_ERROR msg => 
40836  565 
err_bound ctxt (gen_msg err msg) tye (find_error_pack lower key)) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

566 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

567 
(case assignment of 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

568 
NONE => tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

569 
 SOME T => 
40286  570 
if Type_Infer.is_paramT T then tye_idx 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

571 
else if lower then (*upper bound check*) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

572 
let 
40286  573 
val other_bound = map (Type_Infer.deref tye) (get_succs G key); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

574 
val s = nameT T; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

575 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

576 
if subset (op = o apfst nameT) (filter is_typeT other_bound, s :: styps true s) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

577 
then apfst (Vartab.update (xi, T)) tye_idx 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

578 
else err_bound ctxt (gen_msg err ("assigned base type " ^ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

579 
quote (Syntax.string_of_typ ctxt T) ^ 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

580 
" clashes with the upper bound of variable " ^ 
40836  581 
Syntax.string_of_typ ctxt (TVar(xi, S)))) tye (find_error_pack (not lower) key) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

582 
end 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

583 
else apfst (Vartab.update (xi, T)) tye_idx) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

584 
end 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

585 
else tye_idx; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

586 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

587 
val assign_lb = assign_bound true; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

588 
val assign_ub = assign_bound false; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

589 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

590 
fun assign_alternating ts' ts G tye_idx = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

591 
if ts' = ts then tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

592 
else 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

593 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

594 
val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

595 
> fold (assign_ub G) ts; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

596 
in 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

597 
assign_alternating ts 
40836  598 
(filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx' 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

599 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

600 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

601 
(*Unify all weakly connected components of the constraint forest, 
40282  602 
that contain only params. These are the only WCCs that contain 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

603 
params anyway.*) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

604 
fun unify_params G (tye_idx as (tye, _)) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

605 
let 
40286  606 
val max_params = 
607 
filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G); 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

608 
val to_unify = map (fn T => T :: get_preds G T) max_params; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

609 
in 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

610 
fold 
40836  611 
(fn Ts => fn tye_idx' => unify_list Ts tye_idx' 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

612 
handle NO_UNIFIER (msg, _) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts) 
40836  613 
to_unify tye_idx 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

614 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

615 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

616 
fun solve_constraints G tye_idx = tye_idx 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

617 
> assign_alternating [] (Typ_Graph.keys G) G 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

618 
> unify_params G; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

619 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

620 
build_graph Typ_Graph.empty (map fst cs') tye_idx' 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

621 
> solve_constraints 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

622 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

623 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

624 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

625 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

626 
(** coercion insertion **) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

627 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

628 
fun gen_coercion ctxt err tye TU = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

629 
let 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

630 
fun gen (T1, T2) = (case pairself (Type_Infer.deref tye) (T1, T2) of 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

631 
(T1 as (Type (a, [])), T2 as (Type (b, []))) => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

632 
if a = b 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

633 
then Abs (Name.uu, Type (a, []), Bound 0) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

634 
else 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

635 
(case Symreltab.lookup (coes_of ctxt) (a, b) of 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

636 
NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

637 
" is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2)) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

638 
 SOME (co, _) => co) 
45102
7bb89635eb51
correct coercion generation in case of unknown map functions
traytel
parents:
45060
diff
changeset

639 
 (T1 as Type (a, Ts), T2 as Type (b, Us)) => 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

640 
if a <> b 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

641 
then 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

642 
(case Symreltab.lookup (coes_of ctxt) (a, b) of 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

643 
(*immediate error  cannot fix complex coercion with the global algorithm*) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

644 
NONE => error (err () ^ "No coercion known for type constructors: " ^ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

645 
quote a ^ " and " ^ quote b) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

646 
 SOME (co, ((Ts', Us'), _)) => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

647 
let 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

648 
val co_before = gen (T1, Type (a, Ts')); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

649 
val coT = range_type (fastype_of co_before); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

650 
val insts = inst_collect tye (err ++> "Could not insert complex coercion") 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

651 
(domain_type (fastype_of co)) coT; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

652 
val co' = Term.subst_TVars insts co; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

653 
val co_after = gen (Type (b, (map (typ_subst_TVars insts) Us')), T2); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

654 
in 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

655 
Abs (Name.uu, T1, Library.foldr (op $) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

656 
(filter (not o is_identity) [co_after, co', co_before], Bound 0)) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

657 
end) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

658 
else 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

659 
let 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

660 
fun sub_co (COVARIANT, TU) = SOME (gen TU) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

661 
 sub_co (CONTRAVARIANT, TU) = SOME (gen (swap TU)) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

662 
 sub_co (INVARIANT_TO _, _) = NONE; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

663 
fun ts_of [] = [] 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

664 
 ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

665 
in 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

666 
(case Symtab.lookup (tmaps_of ctxt) a of 
45102
7bb89635eb51
correct coercion generation in case of unknown map functions
traytel
parents:
45060
diff
changeset

667 
NONE => 
7bb89635eb51
correct coercion generation in case of unknown map functions
traytel
parents:
45060
diff
changeset

668 
if Type.could_unify (T1, T2) 
7bb89635eb51
correct coercion generation in case of unknown map functions
traytel
parents:
45060
diff
changeset

669 
then Abs (Name.uu, T1, Bound 0) 
7bb89635eb51
correct coercion generation in case of unknown map functions
traytel
parents:
45060
diff
changeset

670 
else raise COERCION_GEN_ERROR 
7bb89635eb51
correct coercion generation in case of unknown map functions
traytel
parents:
45060
diff
changeset

671 
(err ++> "No map function for " ^ quote a ^ " known") 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

672 
 SOME tmap => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

673 
let 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

674 
val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us)); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

675 
in 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

676 
if null (filter (not o is_identity) used_coes) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

677 
then Abs (Name.uu, Type (a, Ts), Bound 0) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

678 
else Term.list_comb 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

679 
(instantiate (fst tmap) (ts_of (map fastype_of used_coes)), used_coes) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

680 
end) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

681 
end 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

682 
 (T, U) => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

683 
if Type.could_unify (T, U) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

684 
then Abs (Name.uu, T, Bound 0) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

685 
else raise COERCION_GEN_ERROR (err ++> "Cannot generate coercion from " ^ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

686 
quote (Syntax.string_of_typ ctxt T) ^ " to " ^ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

687 
quote (Syntax.string_of_typ ctxt U))); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

688 
in 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

689 
gen TU 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

690 
end; 
40836  691 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

692 
fun function_of ctxt err tye T = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

693 
(case Type_Infer.deref tye T of 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

694 
Type (C, Ts) => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

695 
(case Symreltab.lookup (coes_of ctxt) (C, "fun") of 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

696 
NONE => error (err () ^ "No complex coercion from " ^ quote C ^ " to fun") 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

697 
 SOME (co, ((Ts', _), _)) => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

698 
let 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

699 
val co_before = gen_coercion ctxt err tye (Type (C, Ts), Type (C, Ts')); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

700 
val coT = range_type (fastype_of co_before); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

701 
val insts = inst_collect tye (err ++> "Could not insert complex coercion") 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

702 
(domain_type (fastype_of co)) coT; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

703 
val co' = Term.subst_TVars insts co; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

704 
in 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

705 
Abs (Name.uu, Type (C, Ts), Library.foldr (op $) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

706 
(filter (not o is_identity) [co', co_before], Bound 0)) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

707 
end) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

708 
 T' => error (err () ^ "No complex coercion from " ^ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

709 
quote (Syntax.string_of_typ ctxt T') ^ " to fun")); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

710 

9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

711 
fun insert_coercions ctxt (tye, idx) ts = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

712 
let 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

713 
fun insert _ (Const (c, T)) = (Const (c, T), T) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

714 
 insert _ (Free (x, T)) = (Free (x, T), T) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

715 
 insert _ (Var (xi, T)) = (Var (xi, T), T) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

716 
 insert bs (Bound i) = 
43278  717 
let val T = nth bs i handle General.Subscript => err_loose i; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

718 
in (Bound i, T) end 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

719 
 insert bs (Abs (x, T, t)) = 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

720 
let val (t', T') = insert (T :: bs) t; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

721 
in (Abs (x, T, t'), T > T') end 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

722 
 insert bs (t $ u) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

723 
let 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

724 
val (t', Type ("fun", [U, T])) = apsnd (Type_Infer.deref tye) (insert bs t); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

725 
val (u', U') = insert bs u; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

726 
in 
40836  727 
if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U') 
728 
then (t' $ u', T) 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

729 
else (t' $ (gen_coercion ctxt (K "") tye (U', U) $ u'), T) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

730 
end 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

731 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

732 
map (fst o insert []) ts 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

733 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

734 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

735 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

736 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

737 
(** assembling the pipeline **) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

738 

42398  739 
fun coercion_infer_types ctxt raw_ts = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

740 
let 
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42402
diff
changeset

741 
val (idx, ts) = Type_Infer_Context.prepare ctxt raw_ts; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

742 

40836  743 
fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx) 
744 
 inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx) 

745 
 inf _ (t as (Var (_, T))) tye_idx = (t, T, tye_idx) 

746 
 inf bs (t as (Bound i)) tye_idx = 

43278  747 
(t, snd (nth bs i handle General.Subscript => err_loose i), tye_idx) 
40836  748 
 inf bs (Abs (x, T, t)) tye_idx = 
749 
let val (t', U, tye_idx') = inf ((x, T) :: bs) t tye_idx 

750 
in (Abs (x, T, t'), T > U, tye_idx') end 

751 
 inf bs (t $ u) tye_idx = 

752 
let 

753 
val (t', T, tye_idx') = inf bs t tye_idx; 

754 
val (u', U, (tye, idx)) = inf bs u tye_idx'; 

755 
val V = Type_Infer.mk_param idx []; 

756 
val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U > V, T) (tye, idx + 1)) 

42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

757 
handle NO_UNIFIER (msg, tye') => 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

758 
let 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

759 
val err = err_appl_msg ctxt msg tye' bs t T u U; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

760 
val W = Type_Infer.mk_param (idx + 1) []; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

761 
val (t'', (tye', idx')) = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

762 
(t', strong_unify ctxt (W > V, T) (tye, idx + 2)) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

763 
handle NO_UNIFIER _ => 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

764 
let 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

765 
val err' = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

766 
err ++> "\nLocal coercion insertion on the operator failed:\n"; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

767 
val co = function_of ctxt err' tye T; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

768 
val (t'', T'', tye_idx'') = inf bs (co $ t') (tye, idx + 2); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

769 
in 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

770 
(t'', strong_unify ctxt (W > V, T'') tye_idx'' 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

771 
handle NO_UNIFIER (msg, _) => error (err' () ^ msg)) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

772 
end; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

773 
val err' = err ++> (if t' aconv t'' then "" 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

774 
else "\nSuccessfully coerced the operand to a function of type:\n" ^ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

775 
Syntax.string_of_typ ctxt 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

776 
(the_single (snd (prep_output ctxt tye' bs [] [W > V]))) ^ "\n") ^ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

777 
"\nLocal coercion insertion on the operand failed:\n"; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

778 
val co = gen_coercion ctxt err' tye' (U, W); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

779 
val (u'', U', tye_idx') = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

780 
inf bs (if is_identity co then u else co $ u) (tye', idx'); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

781 
in 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

782 
(t'' $ u'', strong_unify ctxt (U', W) tye_idx' 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

783 
handle NO_UNIFIER (msg, _) => raise COERCION_GEN_ERROR (err' ++> msg)) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

784 
end; 
40836  785 
in (tu, V, tye_idx'') end; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

786 

42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

787 
fun infer_single t tye_idx = 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

788 
let val (t, _, tye_idx') = inf [] t tye_idx 
40938
e258f6817add
use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
traytel
parents:
40840
diff
changeset

789 
in (t, tye_idx') end; 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

790 

40938
e258f6817add
use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
traytel
parents:
40840
diff
changeset

791 
val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx) 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

792 
handle COERCION_GEN_ERROR err => 
40836  793 
let 
794 
fun gen_single t (tye_idx, constraints) = 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

795 
let val (_, tye_idx', constraints') = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

796 
generate_constraints ctxt (err ++> "\n") t tye_idx 
40836  797 
in (tye_idx', constraints' @ constraints) end; 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

798 

40836  799 
val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

800 
val (tye, idx) = process_constraints ctxt (err ++> "\n") constraints tye_idx; 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

801 
in 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

802 
(insert_coercions ctxt (tye, idx) ts, (tye, idx)) 
40836  803 
end); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

804 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

805 
val (_, ts'') = Type_Infer.finish ctxt tye ([], ts'); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

806 
in ts'' end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

807 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

808 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

809 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

810 
(** installation **) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

811 

40283  812 
(* term check *) 
813 

42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42405
diff
changeset

814 
val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false); 
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset

815 

40283  816 
val add_term_check = 
45429  817 
Syntax_Phases.term_check ~100 "coercions" 
42402
c7139609b67d
simplified check/uncheck interfaces: result comparison is hardwired by default;
wenzelm
parents:
42398
diff
changeset

818 
(fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

819 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

820 

40283  821 
(* declarations *) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

822 

40284
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

823 
fun add_type_map raw_t context = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

824 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

825 
val ctxt = Context.proof_of context; 
40284
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

826 
val t = singleton (Variable.polymorphic ctxt) raw_t; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

827 

45059  828 
fun err_str t = "\n\nThe provided function has the type:\n" ^ 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

829 
Syntax.string_of_typ ctxt (fastype_of t) ^ 
45059  830 
"\n\nThe general type signature of a map function is:" ^ 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

831 
"\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^ 
45059  832 
"\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)."; 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

833 

41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

834 
val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t)) 
47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
46961
diff
changeset

835 
handle List.Empty => error ("Not a proper map function:" ^ err_str t); 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

836 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

837 
fun gen_arg_var ([], []) = [] 
40282  838 
 gen_arg_var ((T, T') :: Ts, (U, U') :: Us) = 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

839 
if U = U' then 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

840 
if is_stypeT U then INVARIANT_TO U :: gen_arg_var ((T, T') :: Ts, Us) 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

841 
else error ("Invariant xi and yi should be base types:" ^ err_str t) 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

842 
else if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

843 
else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us) 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

844 
else error ("Functions do not apply to arguments correctly:" ^ err_str t) 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

845 
 gen_arg_var (_, Ts) = 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

846 
if forall (op = andf is_stypeT o fst) Ts 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

847 
then map (INVARIANT_TO o fst) Ts 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

848 
else error ("Different numbers of functions and variant arguments\n" ^ err_str t); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

849 

41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

850 
(*retry flag needed to adjust the type lists, when given a map over type constructor fun*) 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

851 
fun check_map_fun fis (Type (C1, Ts)) (Type (C2, Us)) retry = 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

852 
if C1 = C2 andalso not (null fis) andalso forall is_funtype fis 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

853 
then ((map dest_funT fis, Ts ~~ Us), C1) 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

854 
else error ("Not a proper map function:" ^ err_str t) 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

855 
 check_map_fun fis T1 T2 true = 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

856 
let val (fis', T') = split_last fis 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

857 
in check_map_fun fis' T' (T1 > T2) false end 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

858 
 check_map_fun _ _ _ _ = error ("Not a proper map function:" ^ err_str t); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

859 

41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

860 
val res = check_map_fun fis T1 T2 true; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

861 
val res_av = gen_arg_var (fst res); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

862 
in 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

863 
map_tmaps (Symtab.update (snd res, (t, res_av))) context 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

864 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

865 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

866 
fun transitive_coercion ctxt tab G (a, b) = 
45059  867 
let 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

868 
fun safe_app t (Abs (x, T', u)) = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

869 
let 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

870 
val t' = map_types Type_Infer.paramify_vars t; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

871 
in 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

872 
singleton (coercion_infer_types ctxt) (Abs(x, T', (t' $ u))) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

873 
end; 
45059  874 
val path = hd (Graph.irreducible_paths G (a, b)); 
875 
val path' = fst (split_last path) ~~ tl path; 

876 
val coercions = map (fst o the o Symreltab.lookup tab) path'; 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

877 
val trans_co = singleton (Variable.polymorphic ctxt) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

878 
(fold safe_app coercions (Abs (Name.uu, dummyT, Bound 0))); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

879 
val (Ts, Us) = pairself (snd o Term.dest_Type) (Term.dest_funT (type_of trans_co)) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

880 
in 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

881 
(trans_co, ((Ts, Us), coercions)) 
45059  882 
end; 
883 

40284
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

884 
fun add_coercion raw_t context = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

885 
let 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

886 
val ctxt = Context.proof_of context; 
40284
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

887 
val t = singleton (Variable.polymorphic ctxt) raw_t; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

888 

45059  889 
fun err_coercion () = error ("Bad type for a coercion:\n" ^ 
890 
Syntax.string_of_term ctxt t ^ " :: " ^ 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

891 
Syntax.string_of_typ ctxt (fastype_of t)); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

892 

40840  893 
val (T1, T2) = Term.dest_funT (fastype_of t) 
894 
handle TYPE _ => err_coercion (); 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

895 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

896 
val (a, Ts) = Term.dest_Type T1 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

897 
handle TYPE _ => err_coercion (); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

898 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

899 
val (b, Us) = Term.dest_Type T2 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

900 
handle TYPE _ => err_coercion (); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

901 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

902 
fun coercion_data_update (tab, G, _) = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

903 
let 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

904 
val G' = maybe_new_nodes [(a, length Ts), (b, length Us)] G 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

905 
val G'' = Graph.add_edge_trans_acyclic (a, b) G' 
45059  906 
handle Graph.CYCLES _ => error ( 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

907 
Syntax.string_of_typ ctxt T2 ^ " is already a subtype of " ^ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

908 
Syntax.string_of_typ ctxt T1 ^ "!\n\nCannot add coercion of type: " ^ 
45059  909 
Syntax.string_of_typ ctxt (T1 > T2)); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

910 
val new_edges = 
49560  911 
flat (Graph.dest G'' > map (fn ((x, _), ys) => ys > map_filter (fn y => 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

912 
if Graph.is_edge G' (x, y) then NONE else SOME (x, y)))); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

913 
val G_and_new = Graph.add_edge (a, b) G'; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

914 

3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

915 
val tab' = fold 
45059  916 
(fn pair => fn tab => 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

917 
Symreltab.update (pair, transitive_coercion ctxt tab G_and_new pair) tab) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

918 
(filter (fn pair => pair <> (a, b)) new_edges) 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

919 
(Symreltab.update ((a, b), (t, ((Ts, Us), []))) tab); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

920 
in 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

921 
(tab', G'', restrict_graph G'') 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

922 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

923 
in 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

924 
map_coes_and_graphs coercion_data_update context 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

925 
end; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

926 

45059  927 
fun delete_coercion raw_t context = 
928 
let 

929 
val ctxt = Context.proof_of context; 

930 
val t = singleton (Variable.polymorphic ctxt) raw_t; 

931 

932 
fun err_coercion the = error ("Not" ^ 

933 
(if the then " the defined " else " a ") ^ "coercion:\n" ^ 

934 
Syntax.string_of_term ctxt t ^ " :: " ^ 

935 
Syntax.string_of_typ ctxt (fastype_of t)); 

936 

937 
val (T1, T2) = Term.dest_funT (fastype_of t) 

938 
handle TYPE _ => err_coercion false; 

939 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

940 
val (a, Ts) = dest_Type T1 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

941 
handle TYPE _ => err_coercion false; 
45059  942 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

943 
val (b, Us) = dest_Type T2 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

944 
handle TYPE _ => err_coercion false; 
45059  945 

946 
fun delete_and_insert tab G = 

947 
let 

948 
val pairs = 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

949 
Symreltab.fold (fn ((a, b), (_, (_, ts))) => fn pairs => 
45059  950 
if member (op aconv) ts t then (a, b) :: pairs else pairs) tab [(a, b)]; 
951 
fun delete pair (G, tab) = (Graph.del_edge pair G, Symreltab.delete_safe pair tab); 

952 
val (G', tab') = fold delete pairs (G, tab); 

49564  953 
fun reinsert pair (G, xs) = 
954 
(case Graph.irreducible_paths G pair of 

955 
[] => (G, xs) 

956 
 _ => (Graph.add_edge pair G, (pair, transitive_coercion ctxt tab' G' pair) :: xs)); 

45059  957 
val (G'', ins) = fold reinsert pairs (G', []); 
958 
in 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

959 
(fold Symreltab.update ins tab', G'', restrict_graph G'') 
45059  960 
end 
961 

962 
fun show_term t = Pretty.block [Syntax.pretty_term ctxt t, 

963 
Pretty.str " :: ", Syntax.pretty_typ ctxt (fastype_of t)] 

964 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

965 
fun coercion_data_update (tab, G, _) = 
45059  966 
(case Symreltab.lookup tab (a, b) of 
967 
NONE => err_coercion false 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

968 
 SOME (t', (_, [])) => if t aconv t' 
45059  969 
then delete_and_insert tab G 
970 
else err_coercion true 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

971 
 SOME (t', (_, ts)) => if t aconv t' 
45059  972 
then error ("Cannot delete the automatically derived coercion:\n" ^ 
973 
Syntax.string_of_term ctxt t ^ " :: " ^ 

974 
Syntax.string_of_typ ctxt (fastype_of t) ^ 

975 
Pretty.string_of (Pretty.big_list "\n\nDeleting one of the coercions:" 

976 
(map show_term ts)) ^ 

977 
"\nwill also remove the transitive coercion.") 

978 
else err_coercion true); 

979 
in 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

980 
map_coes_and_graphs coercion_data_update context 
45059  981 
end; 
982 

983 
fun print_coercions ctxt = 

984 
let 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

985 
fun separate _ [] = ([], []) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

986 
 separate P (x::xs) = (if P x then apfst else apsnd) (cons x) (separate P xs); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

987 
val (simple, complex) = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

988 
separate (fn (_, (_, ((Ts, Us), _))) => null Ts andalso null Us) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

989 
(Symreltab.dest (coes_of ctxt)); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

990 
fun show_coercion ((a, b), (t, ((Ts, Us), _))) = Pretty.block [ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

991 
Syntax.pretty_typ ctxt (Type (a, Ts)), 
45059  992 
Pretty.brk 1, Pretty.str "<:", Pretty.brk 1, 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

993 
Syntax.pretty_typ ctxt (Type (b, Us)), 
45059  994 
Pretty.brk 3, Pretty.block [Pretty.str "using", Pretty.brk 1, 
995 
Pretty.quote (Syntax.pretty_term ctxt t)]]; 

996 
in 

45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

997 
Pretty.big_list "Coercions:" 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

998 
[Pretty.big_list "between base types:" (map show_coercion simple), 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

999 
Pretty.big_list "other:" (map show_coercion complex)] 
45059  1000 
> Pretty.writeln 
1001 
end; 

1002 

1003 
fun print_coercion_maps ctxt = 

1004 
let 

1005 
fun show_map (x, (t, _)) = Pretty.block [ 

1006 
Pretty.str x, Pretty.str ":", Pretty.brk 1, 

1007 
Pretty.quote (Syntax.pretty_term ctxt t)]; 

1008 
in 

1009 
Pretty.big_list "Coercion maps:" (map show_map (Symtab.dest (tmaps_of ctxt))) 

1010 
> Pretty.writeln 

1011 
end; 

1012 

40283  1013 

1014 
(* theory setup *) 

1015 

1016 
val setup = 

1017 
Context.theory_map add_term_check #> 

40284
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

1018 
Attrib.setup @{binding coercion} 
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

1019 
(Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t)))) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

1020 
"declaration of new coercions" #> 
45059  1021 
Attrib.setup @{binding coercion_delete} 
1022 
(Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t)))) 

1023 
"deletion of coercions" #> 

40297  1024 
Attrib.setup @{binding coercion_map} 
40284
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

1025 
(Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t)))) 
40283  1026 
"declaration of new map functions"; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

1027 

45059  1028 

1029 
(* outer syntax commands *) 

1030 

1031 
val _ = 

46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46665
diff
changeset

1032 
Outer_Syntax.improper_command @{command_spec "print_coercions"} "print all coercions" 
45059  1033 
(Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of))) 
1034 
val _ = 

46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46665
diff
changeset

1035 
Outer_Syntax.improper_command @{command_spec "print_coercion_maps"} "print all coercion maps" 
45059  1036 
(Scan.succeed (Toplevel.keep (print_coercion_maps o Toplevel.context_of))) 
1037 

40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

1038 
end; 