author  wenzelm 
Mon, 03 Feb 2014 15:31:47 +0100  
changeset 55302  d6f7418ea9dd 
parent 55301  792f3cf59d95 
child 55303  35354009ca25 
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 = 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

46 
error ("Cannot merge tables for constants with coercioninvariant arguments.\n" 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

47 
^ "Conflicting declarations for the constant " ^ quote C ^ "."); 
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 

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

74 
fun map_coes 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) => 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

77 

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

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

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

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

81 

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

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

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

84 
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

85 
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

86 

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

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

88 
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

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

90 

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

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

92 
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

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

94 

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

96 

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

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

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

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

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

101 

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

102 

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

103 

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

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

105 

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

106 
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

107 

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

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

109 
fun t_of s = Type (s, []); 
40286  110 

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

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

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

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

114 

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

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

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

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

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

122 
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

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

124 

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

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

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

127 

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

128 
exception COERCION_GEN_ERROR of unit > (string * Pretty.T list); 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

129 

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

130 
infixr ++> +@> (* lazy error msg composition *) 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

131 

54589  132 
fun (err : unit > string * Pretty.T list) ++> (prt : Pretty.T) = 
133 
err #> apsnd (cons prt); 

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

134 
val op +@> = Library.foldl op ++>; 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

135 

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

136 
fun eval_err err = err () 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

137 
> (fn (str, errs) => str ^ Pretty.string_of (Pretty.text_fold (rev errs))); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

138 

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

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

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

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

142 
 (Type (a, Ts), Type (b, Us)) => 
55302
d6f7418ea9dd
just error, not a failed attempt to raise an exception;
wenzelm
parents:
55301
diff
changeset

143 
if a <> b then error (eval_err err) else inst_collects tye err Ts Us 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

146 
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

147 

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

148 

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

150 

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

151 
exception NO_UNIFIER of string * typ Vartab.table; 
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 unify weak ctxt = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

154 
let 
42361  155 
val thy = Proof_Context.theory_of ctxt; 
42386  156 
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

157 

40282  158 

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

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

160 

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

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

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

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

164 

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

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

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

167 
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

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

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

170 
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

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

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

173 
else if Type_Infer.is_param xi then 
40286  174 
(Vartab.update_new 
175 
(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

176 
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

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

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

180 

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

182 

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

183 

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

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

185 

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

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

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

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

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

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

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

192 
 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

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

194 

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

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

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

197 
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

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

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

200 

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

201 

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

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

203 

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

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

205 
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

206 

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

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

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

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

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

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

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

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

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

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

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

218 

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

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

220 

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

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

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

223 

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

224 

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

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

226 

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

227 
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

228 
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

229 
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

230 
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

231 
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

232 
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

233 
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

234 
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

235 

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

236 

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

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

238 

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

241 

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

242 

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

243 

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

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

245 

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

246 
fun gen_err err msg = 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

247 
err +@> [Pretty.fbrk, Pretty.str "Now trying to infer coercions globally.", Pretty.fbrk, 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

248 
Pretty.fbrk, Pretty.str "Coercion inference failed", 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

249 
Pretty.str (if msg = "" then "" else ":\n" ^ msg), Pretty.fbrk]; 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

250 

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

251 
val gen_msg = eval_err oo gen_err 
40836  252 

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

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

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

255 
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

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

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

258 
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

259 
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

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

261 

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

262 
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

263 

40836  264 
fun unif_failed msg = 
265 
"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

266 

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

270 
[Pretty.fbrk, Pretty.fbrk, Pretty.str "Coercion Inference:"]) 

271 
end; 

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

272 

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

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

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

275 
val (_, Ts') = prep_output ctxt tye [] [] Ts; 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

276 
val text = eval_err (err +@> [Pretty.fbrk, 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

277 
Pretty.str "Cannot unify a list of types that should be the same:", Pretty.fbrk, 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

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

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

282 

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

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

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

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

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

289 
packs ([], []); 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

290 
val text = eval_err (err +@> [Pretty.fbrk, Pretty.big_list "Cannot fulfil subtype constraints:" 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

293 
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

294 
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

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

296 
Pretty.block [Syntax.pretty_term ctxt (t $ u)]]) 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

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

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

301 

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

302 

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

303 

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

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

305 

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

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

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

308 
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

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

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

312 
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

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

314 
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

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

316 

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

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

319 
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

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

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

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

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

325 
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

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

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

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

329 
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

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

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

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

334 
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

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

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

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

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

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

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

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

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

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

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

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

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

348 

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

349 

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

350 

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

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

352 

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

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

354 

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

356 
let 
42388  357 
val thy = Proof_Context.theory_of ctxt; 
358 

40285  359 
val coes_graph = coes_graph_of ctxt; 
360 
val tmaps = tmaps_of ctxt; 

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

362 

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

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

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

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

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

368 

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

369 
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

370 
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

371 

40282  372 

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

373 
(* check whether constraint simplification will terminate using weak unification *) 
40282  374 

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

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

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

378 

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

379 

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

380 
(* simplify constraints *) 
40282  381 

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

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

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

384 
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

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

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

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

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

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

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

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

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

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

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

395 
 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

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

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

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

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

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

401 
 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

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

404 
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

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

406 
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

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

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

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

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

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

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

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

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

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

416 
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

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

418 
val n = length Ts; 
40286  419 
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

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

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

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

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

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

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

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

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

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

431 
let 
40286  432 
val [TVar (xi, S)] = filter Type_Infer.is_paramT TU; 
433 
val [T] = filter_out Type_Infer.is_paramT TU; 

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

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

435 
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

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

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

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

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

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

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

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

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

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

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

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

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

452 
 (Type (a, Ts), Type (b, Us)) => 
40836  453 
if a <> b then error (gen_msg err "different constructors") 
454 
(fst tye_idx) error_pack 

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

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

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

459 
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

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

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

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

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

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

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

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

471 

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

472 

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

473 
(* do simplification *) 
40282  474 

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

475 
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

476 

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

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

479 

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

480 
fun find_cycle_packs nodes = 
40836  481 
let 
482 
val (but_last, last) = split_last nodes 

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

484 
in 

485 
map_filter 

40838  486 
(fn (TU, pack) => if member (op =) pairs TU then SOME pack else NONE) 
40836  487 
cs' 
488 
end; 

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

489 

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

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

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

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

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

495 

40282  496 
fun minmax sup (T :: Ts) = 
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 sup then (T, U) else (U, T); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

501 
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

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

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

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

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

507 

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

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

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

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

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

515 
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

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

517 

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

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

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

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

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

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

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

524 

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

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

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

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

529 
let 
42388  530 
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

531 
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

532 
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

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

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

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

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

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

539 

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

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

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

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

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

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

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

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

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

550 
fold 
40836  551 
(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

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

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

554 
(gen_err err ("constraint cycle not unifiable\n" ^ msg)) (fst tye_idx) 
40836  555 
(find_cycle_packs cycle))) 
556 
cycles tye_idx 

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

557 
in 
40836  558 
collapse (tye, idx) cycles G 
559 
end 

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

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

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

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

564 
let 
40836  565 
(*all cycles collapse to one node, 
566 
because all of them share at least the nodes x and y*) 

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

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

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

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

570 
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

571 
val G' = fold Typ_Graph.del_node (tl nodes) G; 
40836  572 
fun check_and_gen super T' = 
573 
let val U = Type_Infer.deref tye T'; 

574 
in 

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

576 
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

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

578 
if super andalso 
40836  579 
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

580 
else if not super andalso 
40836  581 
Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes) 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

582 
else err_bound ctxt (gen_err err "cycle elimination produces inconsistent graph") 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

583 
(fst tye_idx) 
40836  584 
(maps find_cycle_packs cycles @ find_error_pack super T') 
585 
end; 

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

586 
in 
40836  587 
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

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

589 

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

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

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

594 
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

595 
val raw_bound = get_bound G key; 
40286  596 
val bound = map (Type_Infer.deref tye) raw_bound; 
597 
val not_params = filter_out Type_Infer.is_paramT bound; 

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

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

600 
NONE => NONE 
40282  601 
 SOME S => 
40286  602 
SOME 
603 
(map nameT 

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

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

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

606 
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

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

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

609 
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

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

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

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

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

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

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

618 
let 
40286  619 
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

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

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

622 
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

623 
then apfst (Vartab.update (xi, T)) tye_idx 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

626 
" clashes with the upper bound of variable " ^ 
54470
0a7341e3948c
show all involved subtyping constraints that cause coercion inference to fail
traytel
parents:
53539
diff
changeset

627 
Syntax.string_of_typ ctxt (TVar(xi, S)))) tye 
0a7341e3948c
show all involved subtyping constraints that cause coercion inference to fail
traytel
parents:
53539
diff
changeset

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

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

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

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

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

633 

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

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

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

636 

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

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

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

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

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

641 
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

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

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

644 
assign_alternating ts 
40836  645 
(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

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

647 

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

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

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

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

652 
let 
40286  653 
val max_params = 
654 
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

655 
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

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

657 
fold 
40836  658 
(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

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

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

662 

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

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

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

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

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

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

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

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

670 

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

671 

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

672 

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

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

674 

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

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

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

677 
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

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

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

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

682 
(case Symreltab.lookup (coes_of ctxt) (a, b) of 
55301  683 
NONE => raise COERCION_GEN_ERROR (err +@> 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

684 
[Pretty.quote (Syntax.pretty_typ ctxt T1), Pretty.brk 1, 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

685 
Pretty.str "is not a subtype of", Pretty.brk 1, 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

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

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

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

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

692 
(*immediate error  cannot fix complex coercion with the global algorithm*) 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

693 
NONE => error (eval_err (err ++> Pretty.strs 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

694 
["No coercion known for type constructors:", quote a, "and", quote b])) 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

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

698 
val coT = range_type (fastype_of co_before); 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

699 
val insts = inst_collect tye 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

700 
(err ++> Pretty.str "Could not insert complex coercion") 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

703 
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

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

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

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

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

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

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

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

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

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

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

715 
 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

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

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

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

719 
if Type.could_unify (T1, T2) 
51335  720 
then mk_identity T1 
45102
7bb89635eb51
correct coercion generation in case of unknown map functions
traytel
parents:
45060
diff
changeset

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

722 
(err ++> Pretty.strs ["No map function for", quote a, "known"]) 
51335  723 
 SOME (tmap, variances) => 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

727 
>> map_filter I 

728 
> map_filter I; 

729 
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

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

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

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

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

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

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

737 
if Type.could_unify (T, U) 
51335  738 
then mk_identity T 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

739 
else raise COERCION_GEN_ERROR (err +@> 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

740 
[Pretty.str "Cannot generate coercion from", Pretty.brk 1, 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

741 
Pretty.quote (Syntax.pretty_typ ctxt T), Pretty.brk 1, Pretty.str "to", Pretty.brk 1, 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

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

745 
end; 
40836  746 

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

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

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

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

750 
(case Symreltab.lookup (coes_of ctxt) (C, "fun") of 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

751 
NONE => error (eval_err (err ++> Pretty.strs 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

752 
["No complex coercion from", quote C, "to fun"])) 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

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

755 
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

756 
val coT = range_type (fastype_of co_before); 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

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

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

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

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

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

764 
 T' => error (eval_err (err +@> [Pretty.str "No complex coercion from", Pretty.brk 1, 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

765 
Pretty.quote (Syntax.pretty_typ ctxt T'), Pretty.brk 1, Pretty.str "to fun"]))); 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

766 

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

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

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

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

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

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

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

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

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

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

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

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

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

782 
in 
40836  783 
if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U') 
784 
then (t' $ u', T) 

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

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

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

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

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

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

790 

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

791 

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

792 

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

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

794 

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

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

797 
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

798 

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

799 
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

800 
 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

801 
 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

802 
 inf _ bs (t as (Bound i)) tye_idx = 
43278  803 
(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

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

805 
let val (t', U, tye_idx') = inf coerce ((x, T) :: bs) t tye_idx 
40836  806 
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

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

809 
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

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

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

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

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

816 
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

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

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

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

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

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

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

823 
Pretty.str "Local coercion insertion on the operator failed:\n"; 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

825 
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

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

827 
(t'', strong_unify ctxt (W > V, T'') tye_idx'' 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

829 
error (eval_err (err' ++> Pretty.str msg))) 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

831 
val err' = err ++> Pretty.str 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

832 
((if t' aconv t'' then "" 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

833 
else "Successfully coerced the operator to a function of type:\n" ^ 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

835 
(the_single (snd (prep_output ctxt tye' bs [] [W > V]))) ^ "\n") ^ 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

836 
(if coerce' then "Local coercion insertion on the operand failed:\n" 
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

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

841 
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

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

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

844 
(t'' $ u'', strong_unify ctxt (U', W) tye_idx' 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

846 
raise COERCION_GEN_ERROR (err' ++> Pretty.str msg)) 
45060
9c2568c0a504
local coercion insertion algorithm to support complex coercions
traytel
parents:
45059
diff
changeset

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

849 

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

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

851 
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

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

853 

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

854 
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

855 
handle COERCION_GEN_ERROR err => 
40836  856 
let 
857 
fun gen_single t (tye_idx, constraints) = 

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

858 
let val (_, tye_idx', constraints') = 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

859 
generate_constraints ctxt (err ++> Pretty.str "\n") t tye_idx 
40836  860 
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

861 

40836  862 
val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []); 
54584
2bbcbf8cf47e
possibility to fold coercion inference error messages; tuned;
traytel
parents:
54470
diff
changeset

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

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

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

867 

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

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

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

870 

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

871 

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

872 

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

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

874 

40283  875 
(* term check *) 
876 

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

877 
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

878 

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

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

882 

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

883 

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

885 

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

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

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

888 
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

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

890 

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

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

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

896 

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

897 
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

898 
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

899 

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

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

902 
if U = U' then 
51335  903 
if null (Term.add_tvarsT U []) then INVARIANT_TO U :: gen_arg_var (Ts, Us) 
904 
else if Term.is_TVar U then INVARIANT :: gen_arg_var (Ts, Us) 

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

906 
else 

907 
(case Ts of 

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

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

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

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

912 
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

913 

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

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

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

916 
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

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

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

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

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

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

922 
 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

923 

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

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

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

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

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

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

929 

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

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

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

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

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

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

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

937 
end; 
45059  938 
val path = hd (Graph.irreducible_paths G (a, b)); 
939 
val path' = fst (split_last path) ~~ tl path; 

940 
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

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

943 
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

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

945 
(trans_co, ((Ts, Us), coercions)) 
45059  946 
end; 
947 

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

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

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

950 
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

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

952 

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

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

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

956 

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

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

959 

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

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

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

962 

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

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

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

965 

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

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

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

968 
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

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

971 
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

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

974 
val new_edges = 
49560  975 
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

976 
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

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

978 

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

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

981 
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

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

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

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

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

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

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

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

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

990 

45059  991 
fun delete_coercion raw_t context = 
992 
let 

993 
val ctxt = Context.proof_of context; 

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

995 

996 
fun err_coercion the = error ("Not" ^ 

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

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

999 
Syntax.string_of_typ ctxt (fastype_of t)); 

1000 

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

1002 
handle TYPE _ => err_coercion false; 

1003 

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

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

1005 
handle TYPE _ => err_coercion false; 
45059  1006 

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

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

1008 
handle TYPE _ => err_coercion false; 
45059  1009 

1010 
fun delete_and_insert tab G = 

1011 
let 

1012 
val pairs = 

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

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

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

49564  1017 
fun reinsert pair (G, xs) = 
1018 
(case Graph.irreducible_paths G pair of 

1019 
[] => (G, xs) 

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

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

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

1023 
(fold Symreltab.update ins tab', G'', restrict_graph G'') 
45059  1024 
end 
1025 

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

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

1028 

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

1029 
fun coercion_data_update (tab, G, _) = 
45059  1030 
(case Symreltab.lookup tab (a, b) of 
1031 
NONE => err_coercion false 

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

1032 
 SOME (t', (_, [])) => if t aconv t' 
45059  1033 
then delete_and_insert tab G 
1034 
else err_coercion true 

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

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

1038 
Syntax.string_of_typ ctxt (fastype_of t) ^ 

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

1040 
(map show_term ts)) ^ 

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

1042 
else err_coercion true); 

1043 
in 

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

1044 
map_coes_and_graphs coercion_data_update context 
45059  1045 
end; 
1046 

1047 
fun print_coercions ctxt = 

1048 
let 

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

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

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

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

1053 
(Symreltab.dest (coes_of ctxt)); 
52432  1054 
fun show_coercion ((a, b), (t, ((Ts, Us), _))) = 
1055 
Pretty.item [Pretty.block 

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

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

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

1059 
Pretty.block 

1060 
[Pretty.keyword "using", Pretty.brk 1, 

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

1062 

1063 
val type_space = Proof_Context.type_space ctxt; 

1064 
val tmaps = 

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

1066 
(Symtab.dest (tmaps_of ctxt)); 

53539  1067 
fun show_map (c, (t, _)) = 
52432  1068 
Pretty.block 
53539  1069 
[Name_Space.pretty ctxt type_space c, Pretty.str ":", 
52432  1070 
Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt t)]; 
45059  1071 
in 
52432  1072 
[Pretty.big_list "coercions between base types:" (map show_coercion simple), 
1073 
Pretty.big_list "other coercions:" (map show_coercion complex), 

1074 
Pretty.big_list "coercion maps:" (map show_map tmaps)] 

1075 
end > Pretty.chunks > Pretty.writeln; 

45059  1076 

1077 

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

1078 
(* theory setup *) 
40283  1079 

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

1080 
val parse_coerce_args = 
51327  1081 
Args.$$$ "+" >> K PERMIT  Args.$$$ "" >> K FORBID  Args.$$$ "0" >> K LEAVE 
40283  1082 

1083 
val setup = 

1084 
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

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

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

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

1090 
"deletion of coercions" #> 

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

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

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

1094 
Attrib.setup @{binding coercion_args} 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

1095 
(Args.const false  Scan.lift (Scan.repeat1 parse_coerce_args) >> 
4a92178011e7
constants with coercioninvariant arguments (possibility to disable/reenable
traytel
parents:
51248
diff
changeset

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

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

1098 

45059  1099 

1100 
(* outer syntax commands *) 

1101 

1102 
val _ = 

52432  1103 
Outer_Syntax.improper_command @{command_spec "print_coercions"} 
1104 
"print information about coercions" 

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

45059  1106 

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

1107 
end; 