author  traytel 
Wed, 17 Aug 2011 19:49:07 +0200  
changeset 45060  9c2568c0a504 
parent 45059  28d3e387f22e 
child 45102  7bb89635eb51 
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 

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

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

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

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

38 
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

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

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

41 
(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

42 
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

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

44 
(eq_pair (eq_pair (eq_list (op =)) (eq_list (op =))) (eq_list (op aconv)))) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

45 
(coes1, coes2), 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

47 
Graph.merge (op =) (coes_graph1, coes_graph2), 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

48 
Symtab.merge (eq_pair (op aconv) (op =)) (tmaps1, tmaps2)); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

50 

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

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

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

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

54 

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

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

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

57 
(f coes, full_graph, coes_graph, tmaps)); 
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 
fun map_coes_graph f = 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

62 

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

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

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

65 
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

66 
in (coes', full_graph', coes_graph', tmaps) end); 
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_tmaps 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, coes_graph, f tmaps)); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

71 

40285  72 
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

73 

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

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

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

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

77 

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

78 

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

79 

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

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

81 

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

82 
fun restrict_graph G = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

83 
Graph.subgraph (fn key => if Graph.get_node G key = 0 then true else false) G; 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

84 

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

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

86 
fun t_of s = Type (s, []); 
40286  87 

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

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

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

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

91 

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

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

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

95 
val is_freeT = fn (TFree _) => true  _ => false; 
40286  96 
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

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

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

99 

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

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

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

102 

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

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

104 

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

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

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

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

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

109 
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

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

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

112 
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

113 

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

114 

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

116 

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

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

118 

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

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

120 
let 
42361  121 
val thy = Proof_Context.theory_of ctxt; 
42386  122 
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

123 

40282  124 

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

125 
(* adjust sorts of parameters *) 
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 not_of_sort x S' S = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

128 
"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

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

130 

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

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

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

133 
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

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

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

136 
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

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

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

139 
else if Type_Infer.is_param xi then 
40286  140 
(Vartab.update_new 
141 
(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

142 
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

143 
and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = 
40286  144 
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

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

146 

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

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

148 

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

149 

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

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

151 

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

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

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

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

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

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

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

158 
 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

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

160 

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

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

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

163 
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

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

165 
(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

166 

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

167 

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

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

169 

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

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

171 
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

172 

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

173 
fun unif (T1, T2) (env as (tye, _)) = 
40286  174 
(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

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

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

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

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

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

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

181 
("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

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

183 
 ((_, 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

184 

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

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

186 

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

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

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

189 

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

190 

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

191 
(* Typ_Graph shortcuts *) 
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 
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

194 
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

195 
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

196 
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

197 
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

198 
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

199 
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

200 
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

201 

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

202 

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

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

204 

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

205 
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

206 
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

207 

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

208 

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 
(** error messages **) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

211 

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

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

213 

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

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

215 

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

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

217 
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

218 
(if msg = "" then "" else ":\n" ^ msg) ^ "\n"; 
40836  219 

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

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

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

222 
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

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

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

225 
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) 
42284  226 
in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

228 

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

229 
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

230 

40836  231 
fun unif_failed msg = 
232 
"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

233 

40836  234 
fun err_appl_msg ctxt msg tye bs t T u U () = 
235 
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

236 
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

237 

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

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

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

240 
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

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

242 
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

243 
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

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

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

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

247 

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

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

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

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

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

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

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

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

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

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

259 
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

260 
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

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

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

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

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

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

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

267 

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

268 

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

269 

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

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

271 

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

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

274 
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

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

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

277 
 gen cs bs (Bound i) tye_idx = 
43278  278 
(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

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

280 
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

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

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

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

284 
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

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

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

288 
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

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

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

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

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

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

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

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

296 

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

297 

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

298 

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

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

300 

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

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

302 

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

304 
let 
42388  305 
val thy = Proof_Context.theory_of ctxt; 
306 

40285  307 
val coes_graph = coes_graph_of ctxt; 
308 
val tmaps = tmaps_of ctxt; 

42388  309 
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

310 

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

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

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

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

315 
 _ => 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

316 

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

317 
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

318 
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

319 

40282  320 

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

321 
(* check whether constraint simplification will terminate using weak unification *) 
40282  322 

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

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

324 
weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, _) => 
40836  325 
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

326 

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

327 

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

328 
(* simplify constraints *) 
40282  329 

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

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

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

332 
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

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

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

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

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

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

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

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

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

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

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

343 
 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

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

345 
err_list ctxt (gen_msg err 
45059  346 
"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

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

348 
 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

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

350 
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

351 
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

352 
(fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx))); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

354 
val (ch, done') = 
40286  355 
if not (null new) then ([], done) 
356 
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

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

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

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

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

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

362 
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

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

364 
val n = length Ts; 
40286  365 
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

366 
val tye' = Vartab.update_new (xi, Type(a, args)) tye; 
40286  367 
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

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

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

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

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

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

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

375 
(*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

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

377 
let 
40286  378 
val [TVar (xi, S)] = filter Type_Infer.is_paramT TU; 
379 
val [T] = filter_out Type_Infer.is_paramT TU; 

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

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

381 
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

382 
val tye' = Vartab.update_new (xi, T) tye; 
40286  383 
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

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

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

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

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

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

391 
 simplify done (((T, U), error_pack) :: todo) (tye_idx as (tye, idx)) = 
40286  392 
(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

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

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

395 
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

396 
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

397 
" 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

398 
 (Type (a, Ts), Type (b, Us)) => 
40836  399 
if a <> b then error (gen_msg err "different constructors") 
400 
(fst tye_idx) error_pack 

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

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

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

405 
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

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

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

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

411 
else if exists (is_freeT orf is_fixedvarT) [T, U] 
40836  412 
then error (gen_msg err "not eliminated free/fixed variables") 
40282  413 
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

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

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

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

417 

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

418 

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

419 
(* do simplification *) 
40282  420 

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

421 
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

422 

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

423 
fun find_error_pack lower T' = map_filter 
40836  424 
(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

425 

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

426 
fun find_cycle_packs nodes = 
40836  427 
let 
428 
val (but_last, last) = split_last nodes 

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

430 
in 

431 
map_filter 

40838  432 
(fn (TU, pack) => if member (op =) pairs TU then SOME pack else NONE) 
40836  433 
cs' 
434 
end; 

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

435 

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

436 
(*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

437 
in terms of the subtyperelation (excluding T itself)*) 
40282  438 
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

439 
(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

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

441 

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

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

444 
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

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

447 
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

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

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

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

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

453 

40282  454 
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

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

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

458 
(fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts; 
42388  459 
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

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

461 
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

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

463 

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

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

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

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

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

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

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

470 

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

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

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

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

475 
let 
42388  476 
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

477 
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

478 
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

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

480 
(case fold candidates Ts (filter restriction (T :: styps sup T)) of 
40836  481 
[] => 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

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

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

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

485 

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

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

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

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

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

491 
val G' = maybe_new_typnodes [T, U] G; 
45059  492 
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

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

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

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

496 
fold 
40836  497 
(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

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

499 
err_bound ctxt 
40836  500 
(gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx) 
501 
(find_cycle_packs cycle))) 

502 
cycles tye_idx 

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

503 
in 
40836  504 
collapse (tye, idx) cycles G 
505 
end 

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

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

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

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

510 
let 
40836  511 
(*all cycles collapse to one node, 
512 
because all of them share at least the nodes x and y*) 

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

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

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

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

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

517 
val G' = Typ_Graph.del_nodes (tl nodes) G; 
40836  518 
fun check_and_gen super T' = 
519 
let val U = Type_Infer.deref tye T'; 

520 
in 

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

522 
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

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

524 
if super andalso 
40836  525 
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

526 
else if not super andalso 
40836  527 
Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes) 
528 
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

529 
(fst tye_idx) 
40836  530 
(maps find_cycle_packs cycles @ find_error_pack super T') 
531 
end; 

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

532 
in 
40836  533 
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

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

535 

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

536 
fun assign_bound lower G key (tye_idx as (tye, _)) = 
40286  537 
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

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

540 
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

541 
val raw_bound = get_bound G key; 
40286  542 
val bound = map (Type_Infer.deref tye) raw_bound; 
543 
val not_params = filter_out Type_Infer.is_paramT bound; 

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

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

546 
NONE => NONE 
40282  547 
 SOME S => 
40286  548 
SOME 
549 
(map nameT 

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

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

551 
(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

552 
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

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

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

555 
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

556 
handle BOUND_ERROR msg => 
40836  557 
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

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

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

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

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

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

564 
let 
40286  565 
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

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

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

568 
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

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

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

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

572 
" clashes with the upper bound of variable " ^ 
40836  573 
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

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

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

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

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

578 

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

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

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

581 

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

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

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

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

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

586 
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

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

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

589 
assign_alternating ts 
40836  590 
(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

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

592 

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

593 
(*Unify all weakly connected components of the constraint forest, 
40282  594 
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

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

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

597 
let 
40286  598 
val max_params = 
599 
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

600 
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

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

602 
fold 
40836  603 
(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

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

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

607 

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

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

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

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

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

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

613 
> solve_constraints 
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 

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

617 

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

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

619 

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

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

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

622 
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

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

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

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

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

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

628 
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

629 
" 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

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

631 
 ((Type (a, Ts)), (Type (b, Us))) => 
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 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

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

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

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

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

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

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

642 
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

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

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

645 
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

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

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

648 
(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

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

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

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

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

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

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

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

656 
 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

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

658 
(case Symtab.lookup (tmaps_of ctxt) a of 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

659 
NONE => raise COERCION_GEN_ERROR 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

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

663 
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

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

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

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

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

668 
(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

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

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

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

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

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

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

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

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

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

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

679 
end; 
40836  680 

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

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

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

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

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

685 
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

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

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

688 
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

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

690 
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

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

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

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

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

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

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

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

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

699 

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

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

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

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

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

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

705 
 insert bs (Bound i) = 
43278  706 
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

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

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

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

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

711 
 insert bs (t $ u) = 
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 
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

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

715 
in 
40836  716 
if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U') 
717 
then (t' $ u', T) 

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

718 
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

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

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

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

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

723 

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

724 

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

725 

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

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

727 

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

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

730 
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

731 

40836  732 
fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx) 
733 
 inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx) 

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

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

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

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

740 
 inf bs (t $ u) tye_idx = 

741 
let 

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

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

744 
val V = Type_Infer.mk_param idx []; 

745 
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

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

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

748 
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

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

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

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

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

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

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

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

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

757 
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

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

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

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

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

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

763 
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

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

765 
(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

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

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

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

769 
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

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

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

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

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

775 

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

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

777 
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

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

779 

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

780 
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

781 
handle COERCION_GEN_ERROR err => 
40836  782 
let 
783 
fun gen_single t (tye_idx, constraints) = 

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

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

785 
generate_constraints ctxt (err ++> "\n") t tye_idx 
40836  786 
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

787 

40836  788 
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

789 
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

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

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

793 

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

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

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

796 

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

797 

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

798 

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

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

800 

40283  801 
(* term check *) 
802 

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

803 
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

804 

40283  805 
val add_term_check = 
806 
Syntax.add_term_check ~100 "coercions" 

42402
c7139609b67d
simplified check/uncheck interfaces: result comparison is hardwired by default;
wenzelm
parents:
42398
diff
changeset

807 
(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

808 

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

809 

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

811 

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

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

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

814 
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

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

816 

45059  817 
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

818 
Syntax.string_of_typ ctxt (fastype_of t) ^ 
45059  819 
"\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

820 
"\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^ 
45059  821 
"\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

822 

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

823 
val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t)) 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

824 
handle 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

825 

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

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

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

829 
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

830 
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

831 
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

832 
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

833 
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

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

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

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

837 
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

838 

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

839 
(*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

840 
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

841 
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

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

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

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

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

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

847 
 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

848 

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

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

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

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

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

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

854 

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

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

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

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

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

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

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

862 
end; 
45059  863 
val path = hd (Graph.irreducible_paths G (a, b)); 
864 
val path' = fst (split_last path) ~~ tl path; 

865 
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

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

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

868 
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

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

870 
(trans_co, ((Ts, Us), coercions)) 
45059  871 
end; 
872 

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

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

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

875 
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

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

877 

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

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

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

881 

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

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

884 

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

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

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

887 

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

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

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

890 

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

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

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

893 
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

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

896 
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

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

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

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

901 
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

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

903 

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

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

906 
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

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

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

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

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

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

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

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

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

915 

45059  916 
fun delete_coercion raw_t context = 
917 
let 

918 
val ctxt = Context.proof_of context; 

919 
val t = singleton (Variable.polymorphic ctxt) raw_t; 

920 

921 
fun err_coercion the = error ("Not" ^ 

922 
(if the then " the defined " else " a ") ^ "coercion:\n" ^ 

923 
Syntax.string_of_term ctxt t ^ " :: " ^ 

924 
Syntax.string_of_typ ctxt (fastype_of t)); 

925 

926 
val (T1, T2) = Term.dest_funT (fastype_of t) 

927 
handle TYPE _ => err_coercion false; 

928 

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

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

930 
handle TYPE _ => err_coercion false; 
45059  931 

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

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

933 
handle TYPE _ => err_coercion false; 
45059  934 

935 
fun delete_and_insert tab G = 

936 
let 

937 
val pairs = 

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

938 
Symreltab.fold (fn ((a, b), (_, (_, ts))) => fn pairs => 
45059  939 
if member (op aconv) ts t then (a, b) :: pairs else pairs) tab [(a, b)]; 
940 
fun delete pair (G, tab) = (Graph.del_edge pair G, Symreltab.delete_safe pair tab); 

941 
val (G', tab') = fold delete pairs (G, tab); 

942 
fun reinsert pair (G, xs) = (case (Graph.irreducible_paths G pair) of 

943 
[] => (G, xs) 

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

944 
 _ => (Graph.add_edge pair G, (pair, transitive_coercion ctxt tab' G' pair) :: xs)); 
45059  945 
val (G'', ins) = fold reinsert pairs (G', []); 
946 
in 

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

947 
(fold Symreltab.update ins tab', G'', restrict_graph G'') 
45059  948 
end 
949 

950 
fun show_term t = Pretty.block [Syntax.pretty_term ctxt t, 

951 
Pretty.str " :: ", Syntax.pretty_typ ctxt (fastype_of t)] 

952 

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

953 
fun coercion_data_update (tab, G, _) = 
45059  954 
(case Symreltab.lookup tab (a, b) of 
955 
NONE => err_coercion false 

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

956 
 SOME (t', (_, [])) => if t aconv t' 
45059  957 
then delete_and_insert tab G 
958 
else err_coercion true 

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

959 
 SOME (t', (_, ts)) => if t aconv t' 
45059  960 
then error ("Cannot delete the automatically derived coercion:\n" ^ 
961 
Syntax.string_of_term ctxt t ^ " :: " ^ 

962 
Syntax.string_of_typ ctxt (fastype_of t) ^ 

963 
Pretty.string_of (Pretty.big_list "\n\nDeleting one of the coercions:" 

964 
(map show_term ts)) ^ 

965 
"\nwill also remove the transitive coercion.") 

966 
else err_coercion true); 

967 
in 

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

968 
map_coes_and_graphs coercion_data_update context 
45059  969 
end; 
970 

971 
fun print_coercions ctxt = 

972 
let 

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

973 
fun separate _ [] = ([], []) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

974 
 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

975 
val (simple, complex) = 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

976 
separate (fn (_, (_, ((Ts, Us), _))) => null Ts andalso null Us) 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

977 
(Symreltab.dest (coes_of ctxt)); 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

978 
fun show_coercion ((a, b), (t, ((Ts, Us), _))) = Pretty.block [ 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

979 
Syntax.pretty_typ ctxt (Type (a, Ts)), 
45059  980 
Pretty.brk 1, Pretty.str "<:", Pretty.brk 1, 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

981 
Syntax.pretty_typ ctxt (Type (b, Us)), 
45059  982 
Pretty.brk 3, Pretty.block [Pretty.str "using", Pretty.brk 1, 
983 
Pretty.quote (Syntax.pretty_term ctxt t)]]; 

984 
in 

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

985 
Pretty.big_list "Coercions:" 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

986 
[Pretty.big_list "between base types:" (map show_coercion simple), 
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

987 
Pretty.big_list "other:" (map show_coercion complex)] 
45059  988 
> Pretty.writeln 
989 
end; 

990 

991 
fun print_coercion_maps ctxt = 

992 
let 

993 
fun show_map (x, (t, _)) = Pretty.block [ 

994 
Pretty.str x, Pretty.str ":", Pretty.brk 1, 

995 
Pretty.quote (Syntax.pretty_term ctxt t)]; 

996 
in 

997 
Pretty.big_list "Coercion maps:" (map show_map (Symtab.dest (tmaps_of ctxt))) 

998 
> Pretty.writeln 

999 
end; 

1000 

40283  1001 

1002 
(* theory setup *) 

1003 

1004 
val setup = 

1005 
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

1006 
Attrib.setup @{binding coercion} 
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

1007 
(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

1008 
"declaration of new coercions" #> 
45059  1009 
Attrib.setup @{binding coercion_delete} 
1010 
(Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t)))) 

1011 
"deletion of coercions" #> 

40297  1012 
Attrib.setup @{binding coercion_map} 
40284
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

1013 
(Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t)))) 
40283  1014 
"declaration of new map functions"; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

1015 

45059  1016 

1017 
(* outer syntax commands *) 

1018 

1019 
val _ = 

1020 
Outer_Syntax.improper_command "print_coercions" "print all coercions" Keyword.diag 

1021 
(Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of))) 

1022 
val _ = 

1023 
Outer_Syntax.improper_command "print_coercion_maps" "print all coercion maps" Keyword.diag 

1024 
(Scan.succeed (Toplevel.keep (print_coercion_maps o Toplevel.context_of))) 

1025 

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

1026 
end; 