author  wenzelm 
Thu, 07 Apr 2016 20:51:52 +0200  
changeset 62908  d7009a515733 
parent 59936  b8ffc3dc9e24 
child 67149  e61557884799 
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 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

14 

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

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

17 

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

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

19 

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

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

22 

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

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

24 
{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

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

26 
full_graph: int Graph.T, 
52432  27 
(*coercions graph restricted to base types  for efficiency reasons stored in the context*) 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

28 
coes_graph: int Graph.T, 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

29 
tmaps: (term * variance list) Symtab.table, (*map functions*) 
51327  30 
coerce_args: coerce_arg list Symtab.table (*special constants with noncoercible arguments*)}; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

31 

51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

32 
fun make_data (coes, full_graph, coes_graph, tmaps, coerce_args) = 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

33 
Data {coes = coes, full_graph = full_graph, coes_graph = coes_graph, 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

34 
tmaps = tmaps, coerce_args = coerce_args}; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

35 

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

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

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

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

39 

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

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

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

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

43 

51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

44 
fun merge_error_coerce_args C = 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

45 
error ("Cannot merge tables for constants with coercioninvariant arguments.\n" ^ 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

46 
"Conflicting declarations for the constant " ^ quote C ^ "."); 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

47 

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

48 
structure Data = Generic_Data 
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 
type T = data; 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

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

53 
fun merge 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

54 
(Data {coes = coes1, full_graph = full_graph1, coes_graph = coes_graph1, 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

55 
tmaps = tmaps1, coerce_args = coerce_args1}, 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

56 
Data {coes = coes2, full_graph = full_graph2, coes_graph = coes_graph2, 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

57 
tmaps = tmaps2, coerce_args = coerce_args2}) = 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

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

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

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

63 
Symtab.merge (eq_pair (op aconv) (op =)) (tmaps1, tmaps2) 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

64 
handle Symtab.DUP key => merge_error_tmaps key, 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

65 
Symtab.merge (eq_list (op =)) (coerce_args1, coerce_args2) 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

66 
handle Symtab.DUP key => merge_error_coerce_args key); 
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 

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

69 
fun map_data f = 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

70 
Data.map (fn Data {coes, full_graph, coes_graph, tmaps, coerce_args} => 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

72 

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

73 
fun map_coes_and_graphs f = 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

75 
let val (coes', full_graph', coes_graph') = f (coes, full_graph, coes_graph); 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

76 
in (coes', full_graph', coes_graph', tmaps, coerce_args) end); 
40281
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 
fun map_tmaps f = 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

79 
map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) => 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

80 
(coes, full_graph, coes_graph, f tmaps, coerce_args)); 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

81 

4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

82 
fun map_coerce_args f = 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

83 
map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) => 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

85 

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

87 

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

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

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

90 
val tmaps_of = #tmaps o rep_data; 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

91 
val coerce_args_of = #coerce_args o rep_data; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

92 

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

93 

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

94 

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

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

96 

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

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

98 

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

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

100 
fun t_of s = Type (s, []); 
40286  101 

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

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

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

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

105 

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

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

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

110 
val is_funtype = fn (Type ("fun", [_, _])) => true  _ => false; 
51335  111 

112 
fun mk_identity T = Abs (Name.uu, T, Bound 0); 

43591
d4cbd6feffdf
collapse map functions with identity subcoercions to identities;
traytel
parents:
43278
diff
changeset

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

114 

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

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

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

117 

55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

118 
exception COERCION_GEN_ERROR of unit > string * Buffer.T; 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

119 

55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

120 
infixr ++> (*composition with deferred error message*) 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

121 
fun (err : unit > string * Buffer.T) ++> s = 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

122 
err #> apsnd (Buffer.add s); 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

123 

55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

124 
fun eval_err err = 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

125 
let val (s, buf) = err () 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

126 
in s ^ Markup.markup Markup.text_fold (Buffer.content buf) end; 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

127 

55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

128 
fun eval_error err = error (eval_err err); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

129 

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

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

131 
(case (T, Type_Infer.deref tye U) of 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

133 
 (Type (a, Ts), Type (b, Us)) => 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

134 
if a <> b then eval_error err else inst_collects tye err Ts Us 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

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

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

137 
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

138 

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

139 

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

141 

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

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

143 

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

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

145 
let 
42361  146 
val thy = Proof_Context.theory_of ctxt; 
59840  147 
val arity_sorts = Proof_Context.arity_sorts ctxt; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

148 

40282  149 

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

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

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

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

155 

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

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

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

158 
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

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

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

161 
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

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

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

164 
else if Type_Infer.is_param xi then 
40286  165 
(Vartab.update_new 
166 
(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

167 
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

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

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

171 

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

173 

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

174 

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

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

176 

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

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

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

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

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

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

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

183 
 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

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

185 

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

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

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

188 
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

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

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

191 

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

194 

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

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

196 
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

197 

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

198 
fun unif (T1, T2) (env as (tye, _)) = 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset

199 
(case apply2 (`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

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

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

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

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

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

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

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

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

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

209 

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

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

211 

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

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

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

214 

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

215 

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

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

217 

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

218 
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

219 
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

220 
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

221 
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

222 
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

223 
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

224 
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

225 
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

226 

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

227 

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

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

229 

55301  230 
fun maybe_new_node s G = perhaps (try (Graph.new_node s)) G; 
231 
fun maybe_new_nodes ss G = fold maybe_new_node ss G; 

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

232 

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

233 

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

234 

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

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

236 

54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

237 
fun gen_err err msg = 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

238 
err ++> ("\nNow trying to infer coercions globally.\n\nCoercion inference failed" ^ 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

239 
(if msg = "" then "" else ":\n" ^ msg) ^ "\n"); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

240 

54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

241 
val gen_msg = eval_err oo gen_err 
40836  242 

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

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

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

245 
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

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

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

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

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

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

251 

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

252 
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

253 

40836  254 
fun unif_failed msg = 
255 
"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

256 

40836  257 
fun err_appl_msg ctxt msg tye bs t T u U () = 
55301  258 
let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U] in 
259 
(unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n\n", 

55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

260 
Buffer.empty > Buffer.add "Coercion Inference:\n\n") 
55301  261 
end; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

262 

54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

263 
fun err_list ctxt err tye Ts = 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

264 
let val (_, Ts') = prep_output ctxt tye [] [] Ts in 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

265 
eval_error (err ++> 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

266 
("\nCannot unify a list of types that should be the same:\n" ^ 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

267 
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

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

269 

54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

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

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

276 
packs ([], []); 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

277 
val msg = 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

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

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

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

281 
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

282 
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

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

284 
Pretty.block [Syntax.pretty_term ctxt (t $ u)]]) 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

285 
ts Ts)); 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

286 
in eval_error (err ++> ("\n" ^ msg)) end; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

287 

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

288 

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

289 

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

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

291 

51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

292 
fun update_coerce_arg ctxt old t = 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

293 
let 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

294 
val mk_coerce_args = the_default [] o Symtab.lookup (coerce_args_of ctxt); 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

295 
fun update _ [] = old 
51327  296 
 update 0 (coerce :: _) = (case coerce of LEAVE => old  PERMIT => true  FORBID => false) 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

297 
 update n (_ :: cs) = update (n  1) cs; 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

298 
val (f, n) = Term.strip_comb (Type.strip_constraints t) > length; 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

299 
in 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

300 
update n (case f of Const (name, _) => mk_coerce_args name  _ => []) 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

301 
end; 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

302 

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

304 
let 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

305 
fun gen _ cs _ (Const (_, T)) tye_idx = (T, tye_idx, cs) 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

306 
 gen _ cs _ (Free (_, T)) tye_idx = (T, tye_idx, cs) 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

307 
 gen _ cs _ (Var (_, T)) tye_idx = (T, tye_idx, cs) 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

308 
 gen _ cs bs (Bound i) tye_idx = 
43278  309 
(snd (nth bs i handle General.Subscript => err_loose i), tye_idx, cs) 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

310 
 gen coerce cs bs (Abs (x, T, t)) tye_idx = 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

312 
in (T > U, tye_idx', cs') end 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

314 
let 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

315 
val (T, tye_idx', cs') = gen coerce cs bs t tye_idx; 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

316 
val coerce' = update_coerce_arg ctxt coerce t; 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

317 
val (U', (tye, idx), cs'') = gen coerce' cs' bs u tye_idx'; 
40286  318 
val U = Type_Infer.mk_param idx []; 
319 
val V = Type_Infer.mk_param (idx + 1) []; 

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

320 
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

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

322 
val error_pack = (bs, t $ u, U, V, U'); 
52432  323 
in 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

324 
if coerce' 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

325 
then (V, tye_idx'', ((U', U), error_pack) :: cs'') 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

326 
else (V, 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

327 
strong_unify ctxt (U, U') tye_idx'' 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

328 
handle NO_UNIFIER (msg, _) => error (gen_msg err msg), 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

329 
cs'') 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

331 
in 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

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

334 

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

335 

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

336 

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

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

338 

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

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

340 

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

342 
let 
42388  343 
val thy = Proof_Context.theory_of ctxt; 
344 

40285  345 
val coes_graph = coes_graph_of ctxt; 
346 
val tmaps = tmaps_of ctxt; 

59840  347 
val arity_sorts = Proof_Context.arity_sorts ctxt; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

348 

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

349 
fun split_cs _ [] = ([], []) 
40282  350 
 split_cs f (c :: cs) = 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset

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

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

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

354 

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

355 
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

356 
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

357 

40282  358 

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

359 
(* check whether constraint simplification will terminate using weak unification *) 
40282  360 

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

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

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

364 

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

365 

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

366 
(* simplify constraints *) 
40282  367 

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

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

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

370 
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

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

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

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

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

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

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

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

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

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

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

381 
 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

382 
handle NO_UNIFIER (msg, _) => 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

383 
err_list ctxt (gen_err err 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

384 
("failed to unify invariant arguments w.r.t. to the known map function\n" ^ 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

387 
 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

388 
handle NO_UNIFIER (msg, _) => 
51248  389 
error (gen_msg err ("failed to unify invariant arguments\n" ^ msg)))); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

390 
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

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

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

393 
val (ch, done') = 
51246
755562fd2d9d
apply unifying substitution before building the constraint graph
traytel
parents:
49660
diff
changeset

394 
done 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset

395 
> map (apfst (apply2 (Type_Infer.deref tye'))) 
51246
755562fd2d9d
apply unifying substitution before building the constraint graph
traytel
parents:
49660
diff
changeset

396 
> (if not (null new) then rpair [] else split_cs test_update); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

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

402 
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

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

404 
val n = length Ts; 
40286  405 
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

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

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

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

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

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

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

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

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

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

417 
let 
40286  418 
val [TVar (xi, S)] = filter Type_Infer.is_paramT TU; 
419 
val [T] = filter_out Type_Infer.is_paramT TU; 

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

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

421 
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

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

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

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

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

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

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

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

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

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

435 
else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

436 
else 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

437 
error (gen_msg err (quote (Syntax.string_of_typ ctxt T1) ^ 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

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

439 
 (Type (a, Ts), Type (b, Us)) => 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

440 
if a <> b then 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

441 
error (gen_msg err "different constructors") (fst tye_idx) error_pack 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

446 
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

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

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

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

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

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

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

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

458 

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

459 

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

460 
(* do simplification *) 
40282  461 

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

462 
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

463 

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

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

466 

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

467 
fun find_cycle_packs nodes = 
40836  468 
let 
469 
val (but_last, last) = split_last nodes 

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

471 
in 

472 
map_filter 

40838  473 
(fn (TU, pack) => if member (op =) pairs TU then SOME pack else NONE) 
40836  474 
cs' 
475 
end; 

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

476 

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

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

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

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

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

482 

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

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

485 
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

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

488 
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

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

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

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

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

494 

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

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

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

499 
(fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts; 
55301  500 
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

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

502 
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

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

504 

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

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

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

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

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

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

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

511 

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

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

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

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

516 
let 
42388  517 
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

518 
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

519 
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

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

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

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

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

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

526 

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

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

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

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

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

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

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

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

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

537 
fold 
40836  538 
(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

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

540 
err_bound ctxt 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

541 
(gen_err err ("constraint cycle not unifiable\n" ^ msg)) (fst tye_idx) 
40836  542 
(find_cycle_packs cycle))) 
543 
cycles tye_idx 

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

544 
in 
40836  545 
collapse (tye, idx) cycles G 
546 
end 

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

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

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

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

551 
let 
40836  552 
(*all cycles collapse to one node, 
553 
because all of them share at least the nodes x and y*) 

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

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

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

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

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

558 
val G' = fold Typ_Graph.del_node (tl nodes) G; 
40836  559 
fun check_and_gen super T' = 
560 
let val U = Type_Infer.deref tye T'; 

561 
in 

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

563 
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

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

565 
if super andalso 
40836  566 
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

567 
else if not super andalso 
40836  568 
Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes) 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

569 
else 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

570 
err_bound ctxt (gen_err err "cycle elimination produces inconsistent graph") 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

571 
(fst tye_idx) 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

572 
(maps find_cycle_packs cycles @ find_error_pack super T') 
40836  573 
end; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

574 
in 
40836  575 
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

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

577 

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

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

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

582 
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

583 
val raw_bound = get_bound G key; 
40286  584 
val bound = map (Type_Infer.deref tye) raw_bound; 
585 
val not_params = filter_out Type_Infer.is_paramT bound; 

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

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

588 
NONE => NONE 
40282  589 
 SOME S => 
40286  590 
SOME 
591 
(map nameT 

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

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

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

594 
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

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

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

597 
else SOME (tightest lower S styps_and_sorts (map nameT not_params) 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

598 
handle BOUND_ERROR msg => err_bound ctxt (gen_err err msg) tye 
55301  599 
(maps (find_error_pack (not lower)) raw_bound)); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

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

606 
let 
40286  607 
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

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

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

610 
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

611 
then apfst (Vartab.update (xi, T)) tye_idx 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

612 
else 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

613 
err_bound ctxt 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

614 
(gen_err err 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

615 
(Pretty.string_of (Pretty.block 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

616 
[Pretty.str "assigned base type", Pretty.brk 1, 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

617 
Pretty.quote (Syntax.pretty_typ ctxt T), Pretty.brk 1, 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

618 
Pretty.str "clashes with the upper bound of variable", Pretty.brk 1, 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

619 
Syntax.pretty_typ ctxt (TVar (xi, S))]))) 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

620 
tye 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

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

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

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

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

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

626 

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

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

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

629 

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

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

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

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

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

634 
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

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

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

637 
assign_alternating ts 
40836  638 
(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

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

640 

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

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

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

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

645 
let 
40286  646 
val max_params = 
647 
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

648 
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

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

650 
fold 
40836  651 
(fn Ts => fn tye_idx' => unify_list Ts tye_idx' 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

655 

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

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

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

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

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

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

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

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

663 

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

664 

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

665 

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

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

667 

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

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

669 
let 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset

670 
fun gen (T1, T2) = 
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset

671 
(case apply2 (Type_Infer.deref tye) (T1, T2) of 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

673 
if a = b 
51335  674 
then mk_identity T1 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

676 
(case Symreltab.lookup (coes_of ctxt) (a, b) of 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

677 
NONE => 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

678 
raise COERCION_GEN_ERROR (err ++> 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

679 
(Pretty.string_of o Pretty.block) 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

680 
[Pretty.quote (Syntax.pretty_typ ctxt T1), Pretty.brk 1, 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

681 
Pretty.str "is not a subtype of", Pretty.brk 1, 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

682 
Pretty.quote (Syntax.pretty_typ ctxt T2)]) 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

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

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

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

688 
(*immediate error  cannot fix complex coercion with the global algorithm*) 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

689 
NONE => 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

690 
eval_error (err ++> 
55304  691 
("No coercion known for type constructors: " ^ 
692 
quote (Proof_Context.markup_type ctxt a) ^ " and " ^ 

693 
quote (Proof_Context.markup_type ctxt b))) 

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

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

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

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

697 
val coT = range_type (fastype_of co_before); 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

698 
val insts = 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

699 
inst_collect tye (err ++> "Could not insert complex coercion") 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

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

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

702 
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

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

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

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

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

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

708 
let 
51335  709 
fun sub_co (COVARIANT, TU) = (SOME (gen TU), NONE) 
710 
 sub_co (CONTRAVARIANT, TU) = (SOME (gen (swap TU)), NONE) 

711 
 sub_co (INVARIANT, (T, _)) = (NONE, SOME T) 

712 
 sub_co (INVARIANT_TO T, _) = (NONE, NONE); 

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

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

714 
 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

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

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

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

718 
if Type.could_unify (T1, T2) 
51335  719 
then mk_identity T1 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

720 
else 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

721 
raise COERCION_GEN_ERROR 
55304  722 
(err ++> 
723 
("No map function for " ^ quote (Proof_Context.markup_type ctxt a) 

724 
^ " known")) 

51335  725 
 SOME (tmap, variances) => 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

726 
let 
51335  727 
val (used_coes, invarTs) = 
728 
map_split sub_co (variances ~~ (Ts ~~ Us)) 

729 
>> map_filter I 

730 
> map_filter I; 

731 
val Tinsts = ts_of (map fastype_of used_coes) @ invarTs; 

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

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

733 
if null (filter (not o is_identity) used_coes) 
51335  734 
then mk_identity (Type (a, Ts)) 
735 
else Term.list_comb (instantiate tmap Tinsts, used_coes) 

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

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

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

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

739 
if Type.could_unify (T, U) 
51335  740 
then mk_identity T 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

741 
else raise COERCION_GEN_ERROR (err ++> 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

742 
(Pretty.string_of o Pretty.block) 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

743 
[Pretty.str "Cannot generate coercion from", Pretty.brk 1, 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

744 
Pretty.quote (Syntax.pretty_typ ctxt T), Pretty.brk 1, 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

745 
Pretty.str "to", Pretty.brk 1, 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

746 
Pretty.quote (Syntax.pretty_typ ctxt U)])); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

749 
end; 
40836  750 

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

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

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

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

754 
(case Symreltab.lookup (coes_of ctxt) (C, "fun") of 
55304  755 
NONE => 
756 
eval_error (err ++> ("No complex coercion from " ^ 

757 
quote (Proof_Context.markup_type ctxt C) ^ " to " ^ 

758 
quote (Proof_Context.markup_type ctxt "fun"))) 

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

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

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

761 
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

762 
val coT = range_type (fastype_of co_before); 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

763 
val insts = 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

764 
inst_collect tye (err ++> "Could not insert complex coercion") 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

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

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

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

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

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

770 
end) 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

771 
 T' => 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

772 
eval_error (err ++> 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

773 
(Pretty.string_of o Pretty.block) 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

774 
[Pretty.str "No complex coercion from", Pretty.brk 1, 
55304  775 
Pretty.quote (Syntax.pretty_typ ctxt T'), Pretty.brk 1, 
776 
Pretty.str "to", Pretty.brk 1, Proof_Context.pretty_type ctxt "fun"])); 

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

777 

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

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

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

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

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

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

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

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

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

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

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

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

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

791 
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

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

793 
in 
40836  794 
if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U') 
795 
then (t' $ u', T) 

55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

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

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

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

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

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

801 

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

802 

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

803 

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

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

805 

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

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

808 
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

809 

51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

810 
fun inf _ _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx) 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

811 
 inf _ _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx) 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

812 
 inf _ _ (t as (Var (_, T))) tye_idx = (t, T, tye_idx) 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

813 
 inf _ bs (t as (Bound i)) tye_idx = 
43278  814 
(t, snd (nth bs i handle General.Subscript => err_loose i), tye_idx) 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

815 
 inf coerce bs (Abs (x, T, t)) tye_idx = 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

816 
let val (t', U, tye_idx') = inf coerce ((x, T) :: bs) t tye_idx 
40836  817 
in (Abs (x, T, t'), T > U, tye_idx') end 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

818 
 inf coerce bs (t $ u) tye_idx = 
40836  819 
let 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

820 
val (t', T, tye_idx') = inf coerce bs t tye_idx; 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

821 
val coerce' = update_coerce_arg ctxt coerce t; 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

822 
val (u', U, (tye, idx)) = inf coerce' bs u tye_idx'; 
40836  823 
val V = Type_Infer.mk_param idx []; 
824 
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

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

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

827 
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

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

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

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

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

832 
let 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

833 
val err' = err ++> "Local coercion insertion on the operator failed:\n"; 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

834 
val co = function_of ctxt err' tye T; 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

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

837 
(t'', strong_unify ctxt (W > V, T'') tye_idx'' 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

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

839 
end; 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

840 
val err' = err ++> 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

841 
((if t' aconv t'' then "" 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

842 
else "Successfully coerced the operator to a function of type:\n" ^ 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

843 
Syntax.string_of_typ ctxt 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

844 
(the_single (snd (prep_output ctxt tye' bs [] [W > V]))) ^ "\n") ^ 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

845 
(if coerce' then "Local coercion insertion on the operand failed:\n" 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

846 
else "Local coercion insertion on the operand disallowed:\n")); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

847 
val (u'', U', tye_idx') = 
52432  848 
if coerce' then 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

849 
let val co = gen_coercion ctxt err' tye' (U, W); 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

850 
in inf coerce' bs (if is_identity co then u else co $ u) (tye', idx') end 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

851 
else (u, U, (tye', idx')); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

853 
(t'' $ u'', strong_unify ctxt (U', W) tye_idx' 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

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

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

857 

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

858 
fun infer_single t tye_idx = 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

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

861 

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

862 
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

863 
handle COERCION_GEN_ERROR err => 
40836  864 
let 
865 
fun gen_single t (tye_idx, constraints) = 

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

866 
let val (_, tye_idx', constraints') = 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

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

869 

40836  870 
val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []); 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

871 
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

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

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

875 

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

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

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

878 

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

879 

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

880 

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

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

882 

40283  883 
(* term check *) 
884 

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

885 
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

886 

58826  887 
val _ = 
888 
Theory.setup 

889 
(Context.theory_map 

890 
(Syntax_Phases.term_check ~100 "coercions" 

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

892 

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

893 

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

895 

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

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

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

898 
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

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

900 

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

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

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

906 

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

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

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

909 

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

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

912 
if U = U' then 
51335  913 
if null (Term.add_tvarsT U []) then INVARIANT_TO U :: gen_arg_var (Ts, Us) 
914 
else if Term.is_TVar U then INVARIANT :: gen_arg_var (Ts, Us) 

915 
else error ("Invariant xi and yi should be variables or variablefree:" ^ err_str t) 

916 
else 

917 
(case Ts of 

918 
[] => error ("Different numbers of functions and variant arguments\n" ^ err_str t) 

919 
 (T, T') :: Ts => 

920 
if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us) 

921 
else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us) 

922 
else error ("Functions do not apply to arguments correctly:" ^ err_str t)); 

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

923 

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

924 
(*retry flag needed to adjust the type lists, when given a map over type constructor fun*) 
55305  925 
fun check_map_fun fis (Type (C1, Ts)) (Type (C2, Us)) _ = 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

926 
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

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

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

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

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

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

932 
 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

933 

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

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

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

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

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

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

939 

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

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

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

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

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

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

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

947 
end; 
45059  948 
val path = hd (Graph.irreducible_paths G (a, b)); 
949 
val path' = fst (split_last path) ~~ tl path; 

950 
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

951 
val trans_co = singleton (Variable.polymorphic ctxt) 
51335  952 
(fold safe_app coercions (mk_identity dummyT)); 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset

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

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

955 
(trans_co, ((Ts, Us), coercions)) 
45059  956 
end; 
957 

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

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

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

960 
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

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

962 

55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

963 
fun err_coercion () = 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

964 
error ("Bad type for a coercion:\n" ^ 
45059  965 
Syntax.string_of_term ctxt t ^ " :: " ^ 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

967 

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

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

970 

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

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

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

973 

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

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

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

976 

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

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

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

979 
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

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

982 
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

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

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

987 
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

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

989 

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

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

992 
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

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

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

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

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

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

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

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

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

1001 

45059  1002 
fun delete_coercion raw_t context = 
1003 
let 

1004 
val ctxt = Context.proof_of context; 

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

1006 

55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1007 
fun err_coercion the = 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1008 
error ("Not" ^ 
45059  1009 
(if the then " the defined " else " a ") ^ "coercion:\n" ^ 
1010 
Syntax.string_of_term ctxt t ^ " :: " ^ 

1011 
Syntax.string_of_typ ctxt (fastype_of t)); 

1012 

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

1014 
handle TYPE _ => err_coercion false; 

1015 

54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

1017 
handle TYPE _ => err_coercion false; 
45059  1018 

54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

1020 
handle TYPE _ => err_coercion false; 
45059  1021 

1022 
fun delete_and_insert tab G = 

1023 
let 

1024 
val pairs = 

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

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

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

49564  1029 
fun reinsert pair (G, xs) = 
1030 
(case Graph.irreducible_paths G pair of 

1031 
[] => (G, xs) 

1032 
 _ => (Graph.add_edge pair G, (pair, transitive_coercion ctxt tab' G' pair) :: xs)); 

45059  1033 
val (G'', ins) = fold reinsert pairs (G', []); 
1034 
in 

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

1035 
(fold Symreltab.update ins tab', G'', restrict_graph G'') 
45059  1036 
end 
1037 

55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1038 
fun show_term t = 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1039 
Pretty.block [Syntax.pretty_term ctxt t, 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1040 
Pretty.str " :: ", Syntax.pretty_typ ctxt (fastype_of t)]; 
45059  1041 

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

1042 
fun coercion_data_update (tab, G, _) = 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1043 
(case Symreltab.lookup tab (a, b) of 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1044 
NONE => err_coercion false 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1045 
 SOME (t', (_, [])) => 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1046 
if t aconv t' 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1047 
then delete_and_insert tab G 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1048 
else err_coercion true 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1049 
 SOME (t', (_, ts)) => 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1050 
if t aconv t' then 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1051 
error ("Cannot delete the automatically derived coercion:\n" ^ 
45059  1052 
Syntax.string_of_term ctxt t ^ " :: " ^ 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1053 
Syntax.string_of_typ ctxt (fastype_of t) ^ "\n\n" ^ 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1054 
Pretty.string_of 
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1055 
(Pretty.big_list "Deleting one of the coercions:" (map show_term ts)) ^ 
45059  1056 
"\nwill also remove the transitive coercion.") 
55303
35354009ca25
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
wenzelm
parents:
55302
diff
changeset

1057 
else err_coercion true); 
45059  1058 
in 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

1059 
map_coes_and_graphs coercion_data_update context 
45059  1060 
end; 
1061 

1062 
fun print_coercions ctxt = 

1063 
let 

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

1064 
fun separate _ [] = ([], []) 
52432  1065 
 separate P (x :: xs) = (if P x then apfst else apsnd) (cons x) (separate P xs); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

1068 
(Symreltab.dest (coes_of ctxt)); 
52432  1069 
fun show_coercion ((a, b), (t, ((Ts, Us), _))) = 
1070 
Pretty.item [Pretty.block 

1071 
[Syntax.pretty_typ ctxt (Type (a, Ts)), Pretty.brk 1, 

1072 
Pretty.str "<:", Pretty.brk 1, 

1073 
Syntax.pretty_typ ctxt (Type (b, Us)), Pretty.brk 3, 

1074 
Pretty.block 

55763  1075 
[Pretty.keyword2 "using", Pretty.brk 1, 
52432  1076 
Pretty.quote (Syntax.pretty_term ctxt t)]]]; 
1077 

1078 
val type_space = Proof_Context.type_space ctxt; 

1079 
val tmaps = 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset

1080 
sort (Name_Space.extern_ord ctxt type_space o apply2 #1) 
52432  1081 
(Symtab.dest (tmaps_of ctxt)); 
53539  1082 
fun show_map (c, (t, _)) = 
52432  1083 
Pretty.block 
53539  1084 
[Name_Space.pretty ctxt type_space c, Pretty.str ":", 
52432  1085 
Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt t)]; 
45059  1086 
in 
52432  1087 
[Pretty.big_list "coercions between base types:" (map show_coercion simple), 
1088 
Pretty.big_list "other coercions:" (map show_coercion complex), 

1089 
Pretty.big_list "coercion maps:" (map show_map tmaps)] 

56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55954
diff
changeset

1090 
end > Pretty.writeln_chunks; 
45059  1091 

1092 

58826  1093 
(* attribute setup *) 
40283  1094 

51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

1095 
val parse_coerce_args = 
51327  1096 
Args.$$$ "+" >> K PERMIT  Args.$$$ "" >> K FORBID  Args.$$$ "0" >> K LEAVE 
40283  1097 

58826  1098 
val _ = 
1099 
Theory.setup 

1100 
(Attrib.setup @{binding coercion} 

1101 
(Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t)))) 

1102 
"declaration of new coercions" #> 

1103 
Attrib.setup @{binding coercion_delete} 

1104 
(Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t)))) 

1105 
"deletion of coercions" #> 

1106 
Attrib.setup @{binding coercion_map} 

1107 
(Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t)))) 

1108 
"declaration of new map functions" #> 

1109 
Attrib.setup @{binding coercion_args} 

1110 
(Args.const {proper = false, strict = false}  Scan.lift (Scan.repeat1 parse_coerce_args) >> 

1111 
(fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec))))) 

1112 
"declaration of new constants with coercioninvariant arguments"); 

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

1113 

45059  1114 

1115 
(* outer syntax commands *) 

1116 

1117 
val _ = 

59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59840
diff
changeset

1118 
Outer_Syntax.command @{command_keyword print_coercions} 
52432  1119 
"print information about coercions" 
1120 
(Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of))); 

45059  1121 

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

1122 
end; 