author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 56334  6b3739fee456 
child 58826  2ed2eaabe3df 
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 
40283  13 
val setup: theory > theory 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

15 

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

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

18 

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

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

20 

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

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

23 

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

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

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

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

27 
full_graph: int Graph.T, 
52432  28 
(*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

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

30 
tmaps: (term * variance list) Symtab.table, (*map functions*) 
51327  31 
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

32 

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

33 
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

34 
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

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

36 

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

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

38 
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

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

40 

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

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

42 
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

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

44 

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

45 
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

46 
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

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

48 

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

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

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

51 
type T = data; 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

52 
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

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

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

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

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

57 
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

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

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

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

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

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

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

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

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

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

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

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

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

71 
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

72 
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

73 

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

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

75 
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

76 
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

77 
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

78 

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

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

80 
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

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

82 

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

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

84 
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

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

86 

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

88 

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

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

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

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

92 
val coerce_args_of = #coerce_args o rep_data; 
40281
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 

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

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

97 

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

98 
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

99 

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

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

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

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

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

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

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

106 

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

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

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

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

113 
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

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

115 

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

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

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

118 

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

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

120 

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

121 
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

122 
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

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

124 

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

125 
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

126 
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

127 
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

128 

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

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

130 

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

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

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

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

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

135 
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

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

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

138 
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

139 

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

140 

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

142 

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

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

144 

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

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

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

149 

40282  150 

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

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

152 

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

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

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

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

156 

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

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

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

159 
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

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

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

162 
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

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

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

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

168 
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

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

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

172 

55301  173 
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

174 

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

175 

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

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

177 

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

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

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

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

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

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

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

184 
 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

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

186 

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

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

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

189 
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

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

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

192 

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

193 

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

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

195 

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

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

197 
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

198 

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

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

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

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

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

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

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

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

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

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

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

210 

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

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

212 

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

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

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

215 

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

216 

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

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

218 

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

219 
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

220 
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

221 
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

222 
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

223 
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

224 
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

225 
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

226 
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

227 

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

228 

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

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

230 

55301  231 
fun maybe_new_node s G = perhaps (try (Graph.new_node s)) G; 
232 
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

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 

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

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

237 

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

238 
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

239 
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

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

241 

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

242 
val gen_msg = eval_err oo gen_err 
40836  243 

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

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

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

246 
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

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

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

249 
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

250 
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

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

252 

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

253 
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

254 

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

257 

40836  258 
fun err_appl_msg ctxt msg tye bs t T u U () = 
55301  259 
let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U] in 
260 
(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

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

263 

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

264 
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

265 
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

266 
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

267 
("\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

268 
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

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

270 

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

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

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

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

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

277 
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

278 
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

279 
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

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

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

282 
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

283 
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

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

285 
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

286 
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

287 
in eval_error (err ++> ("\n" ^ msg)) end; 
40281
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 

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

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

292 

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

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

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

295 
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

296 
fun update _ [] = old 
51327  297 
 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

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

299 
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

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

301 
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

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

303 

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

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

306 
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

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

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

309 
 gen _ cs bs (Bound i) tye_idx = 
43278  310 
(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

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

312 
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

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

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

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

316 
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

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

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

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

321 
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

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

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

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

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

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

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

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

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

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

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

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

334 
end; 
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 

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

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

339 

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

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

341 

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

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

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

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

349 

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

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

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

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

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

355 

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

356 
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

357 
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

358 

40282  359 

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

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

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

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

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

365 

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

366 

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

367 
(* simplify constraints *) 
40282  368 

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

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

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

371 
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

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

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

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

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

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

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

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

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

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

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

382 
 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

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

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

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

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

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

388 
 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

389 
handle NO_UNIFIER (msg, _) => 
51248  390 
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

391 
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

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

393 
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

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

395 
done 
755562fd2d9d
apply unifying substitution before building the constraint graph
traytel
parents:
49660
diff
changeset

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

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

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

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

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

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

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

403 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

422 
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

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

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

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

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

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

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

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

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

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

436 
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

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

438 
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

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

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

441 
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

442 
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

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

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

447 
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

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

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

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

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

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

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

458 
end; 
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 

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

461 
(* do simplification *) 
40282  462 

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

463 
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

464 

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

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

467 

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

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

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

472 
in 

473 
map_filter 

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

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

477 

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

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

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

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

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

483 

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

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

486 
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

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

489 
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

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

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

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

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

495 

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

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

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

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

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

503 
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

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

505 

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

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

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

508 
 'a::S 
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 
/ / \ \ 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

512 

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

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

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

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

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

519 
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

520 
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

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

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

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

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

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

527 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

558 
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

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

562 
in 

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

564 
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

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

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

568 
else if not super andalso 
40836  569 
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

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

571 
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

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

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

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

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

578 

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

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

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

583 
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

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

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

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

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

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

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

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

595 
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

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

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

598 
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

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

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

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

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

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

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

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

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

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

611 
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

612 
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

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

614 
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

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

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

617 
[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

618 
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

619 
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

620 
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

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

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

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

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

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

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

627 

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

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

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

630 

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

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

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

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

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

635 
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

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

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

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

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

641 

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

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

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

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

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

649 
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

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

651 
fold 
40836  652 
(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

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

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

656 

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

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

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

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

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

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

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

663 
end; 
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 

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

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

668 

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

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

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

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

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 

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

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

890 

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

891 

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

893 

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

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

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

896 
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

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

898 

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

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

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

904 

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

905 
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

906 
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

907 

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

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

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

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

914 
else 

915 
(case Ts of 

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

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

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

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

920 
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

921 

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

922 
(*retry flag needed to adjust the type lists, when given a map over type constructor fun*) 
55305  923 
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

924 
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

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

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

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

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

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

930 
 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

931 

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

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

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

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

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

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

937 

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

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

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

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

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

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

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

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

948 
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

949 
val trans_co = singleton (Variable.polymorphic ctxt) 
51335  950 
(fold safe_app coercions (mk_identity dummyT)); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

953 
(trans_co, ((Ts, Us), coercions)) 
45059  954 
end; 
955 

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

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

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

958 
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

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

960 

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

961 
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

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

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

965 

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

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

968 

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

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

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

971 

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

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

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

974 

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

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

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

977 
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

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

980 
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

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

983 
val new_edges = 
49560  984 
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

985 
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

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

987 

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

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

990 
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

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

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

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

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

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

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

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

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

999 

45059  1000 
fun delete_coercion raw_t context = 
1001 
let 

1002 
val ctxt = Context.proof_of context; 

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

1004 

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

1005 
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

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

1009 
Syntax.string_of_typ ctxt (fastype_of t)); 

1010 

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

1012 
handle TYPE _ => err_coercion false; 

1013 

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

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

1015 
handle TYPE _ => err_coercion false; 
45059  1016 

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

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

1018 
handle TYPE _ => err_coercion false; 
45059  1019 

1020 
fun delete_and_insert tab G = 

1021 
let 

1022 
val pairs = 

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

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

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

49564  1027 
fun reinsert pair (G, xs) = 
1028 
(case Graph.irreducible_paths G pair of 

1029 
[] => (G, xs) 

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

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

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

1033 
(fold Symreltab.update ins tab', G'', restrict_graph G'') 
45059  1034 
end 
1035 

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

1036 
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

1037 
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

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

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

1040 
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

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

1042 
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

1043 
 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

1044 
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

1045 
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

1046 
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

1047 
 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

1048 
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

1049 
error ("Cannot delete the automatically derived coercion:\n" ^ 
45059  1050 
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

1051 
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

1052 
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

1053 
(Pretty.big_list "Deleting one of the coercions:" (map show_term ts)) ^ 
45059  1054 
"\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

1055 
else err_coercion true); 
45059  1056 
in 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

1057 
map_coes_and_graphs coercion_data_update context 
45059  1058 
end; 
1059 

1060 
fun print_coercions ctxt = 

1061 
let 

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

1062 
fun separate _ [] = ([], []) 
52432  1063 
 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

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

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

1066 
(Symreltab.dest (coes_of ctxt)); 
52432  1067 
fun show_coercion ((a, b), (t, ((Ts, Us), _))) = 
1068 
Pretty.item [Pretty.block 

1069 
[Syntax.pretty_typ ctxt (Type (a, Ts)), Pretty.brk 1, 

1070 
Pretty.str "<:", Pretty.brk 1, 

1071 
Syntax.pretty_typ ctxt (Type (b, Us)), Pretty.brk 3, 

1072 
Pretty.block 

55763  1073 
[Pretty.keyword2 "using", Pretty.brk 1, 
52432  1074 
Pretty.quote (Syntax.pretty_term ctxt t)]]]; 
1075 

1076 
val type_space = Proof_Context.type_space ctxt; 

1077 
val tmaps = 

1078 
sort (Name_Space.extern_ord ctxt type_space o pairself #1) 

1079 
(Symtab.dest (tmaps_of ctxt)); 

53539  1080 
fun show_map (c, (t, _)) = 
52432  1081 
Pretty.block 
53539  1082 
[Name_Space.pretty ctxt type_space c, Pretty.str ":", 
52432  1083 
Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt t)]; 
45059  1084 
in 
52432  1085 
[Pretty.big_list "coercions between base types:" (map show_coercion simple), 
1086 
Pretty.big_list "other coercions:" (map show_coercion complex), 

1087 
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

1088 
end > Pretty.writeln_chunks; 
45059  1089 

1090 

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

1091 
(* theory setup *) 
40283  1092 

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

1093 
val parse_coerce_args = 
51327  1094 
Args.$$$ "+" >> K PERMIT  Args.$$$ "" >> K FORBID  Args.$$$ "0" >> K LEAVE 
40283  1095 

1096 
val setup = 

1097 
Context.theory_map add_term_check #> 

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

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

1099 
(Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t)))) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

1103 
"deletion of coercions" #> 

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

1105 
(Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t)))) 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

1106 
"declaration of new map functions" #> 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

1107 
Attrib.setup @{binding coercion_args} 
55954  1108 
(Args.const {proper = false, strict = false}  Scan.lift (Scan.repeat1 parse_coerce_args) >> 
51319
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

1109 
(fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec))))) 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

1110 
"declaration of new constants with coercioninvariant arguments"; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

1111 

45059  1112 

1113 
(* outer syntax commands *) 

1114 

1115 
val _ = 

52432  1116 
Outer_Syntax.improper_command @{command_spec "print_coercions"} 
1117 
"print information about coercions" 

1118 
(Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of))); 

45059  1119 

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

1120 
end; 