author  wenzelm 
Sat, 09 Jul 2011 21:53:27 +0200  
changeset 43721  fad8634cee62 
parent 43591  d4cbd6feffdf 
child 44338  700008399ee5 
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 
40283  12 
val setup: theory > theory 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

14 

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

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

17 

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

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

19 

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

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

21 

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

22 
datatype data = Data of 
40282  23 
{coes: term Symreltab.table, (*coercions table*) 
24 
coes_graph: unit Graph.T, (*coercions graph*) 

25 
tmaps: (term * variance list) Symtab.table}; (*map functions*) 

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

26 

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

27 
fun make_data (coes, coes_graph, tmaps) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

29 

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

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

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

32 
type T = data; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

36 
(Data {coes = coes1, coes_graph = coes_graph1, tmaps = tmaps1}, 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

37 
Data {coes = coes2, coes_graph = coes_graph2, tmaps = tmaps2}) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

38 
make_data (Symreltab.merge (op aconv) (coes1, coes2), 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

42 

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

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

44 
Data.map (fn Data {coes, coes_graph, tmaps} => 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

46 

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

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

48 
map_data (fn (coes, coes_graph, tmaps) => 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

50 

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

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

52 
map_data (fn (coes, coes_graph, tmaps) => 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

54 

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

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

56 
map_data (fn (coes, coes_graph, tmaps) => 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

57 
let val (coes', coes_graph') = f (coes, coes_graph); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

59 

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

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

61 
map_data (fn (coes, coes_graph, tmaps) => 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

63 

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

65 

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

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

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

68 
val tmaps_of = #tmaps o rep_data; 
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 

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

71 

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

72 
(** utils **) 
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 nameT (Type (s, [])) = s; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

75 
fun t_of s = Type (s, []); 
40286  76 

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

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

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

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

80 

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

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

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

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

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

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

88 

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

89 

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

91 

40836  92 
exception TYPE_INFERENCE_ERROR of unit > string; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

94 

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

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

96 
let 
42361  97 
val thy = Proof_Context.theory_of ctxt; 
42386  98 
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

99 

40282  100 

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

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

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

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

106 

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

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

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

109 
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

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

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

112 
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

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

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

115 
else if Type_Infer.is_param xi then 
40286  116 
(Vartab.update_new 
117 
(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

118 
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

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

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

122 

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

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

124 

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

125 

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

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

127 

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

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

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

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

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

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

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

134 
 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

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

136 

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

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

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

139 
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

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

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

142 

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

143 

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

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

145 

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

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

147 
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

148 

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

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

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

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

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

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

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

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

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

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

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

160 

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

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

162 

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

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

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

165 

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

166 

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

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

168 

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

169 
val add_edge = Typ_Graph.add_edge_acyclic; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

170 
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

171 
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

172 
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

173 
fun maybe_new_typnodes Ts G = fold maybe_new_typnode Ts G; 
40282  174 
fun new_imm_preds G Ts = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

175 
subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.imm_preds G) Ts)); 
40282  176 
fun new_imm_succs G Ts = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

178 

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

179 

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

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

181 

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

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

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

184 

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 

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

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

188 

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

189 
fun gen_msg err msg = 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

190 
err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^ 
40836  191 
(if msg = "" then "" else ": " ^ msg) ^ "\n"; 
192 

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

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

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

195 
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

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

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

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

200 
in (map prep ts', Ts') end; 
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 
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

203 

40836  204 
fun unif_failed msg = 
205 
"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

206 

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

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

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

210 

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

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

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

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

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

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

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

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

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

219 
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 
fun err_bound ctxt msg tye packs = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

227 
packs ([], []); 
40836  228 
val text = cat_lines ([msg, "Cannot fulfil subtype constraints:"] @ 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

231 
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

232 
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

233 
Pretty.str "from function application", Pretty.brk 2, 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

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

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

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

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

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

239 

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

240 

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

243 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

260 
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

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

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

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

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

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

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

267 

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

268 

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

269 

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

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

271 

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

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

273 

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

275 
let 
42388  276 
val thy = Proof_Context.theory_of ctxt; 
277 

40285  278 
val coes_graph = coes_graph_of ctxt; 
279 
val tmaps = tmaps_of ctxt; 

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

281 

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

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

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

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

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

287 

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

288 
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

289 
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

290 

40282  291 

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

292 
(* check whether constraint simplification will terminate using weak unification *) 
40282  293 

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

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

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

297 

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

298 

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

299 
(* simplify constraints *) 
40282  300 

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

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

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

303 
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

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

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

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

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

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

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

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

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

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

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

314 
 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

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

316 
err_list ctxt (gen_msg err 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

317 
"failed to unify invariant arguments w.r.t. to the known map function") 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

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

319 
 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

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

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

322 
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

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

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

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

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

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

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

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

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

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

333 
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

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

335 
val n = length Ts; 
40286  336 
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

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

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

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

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

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

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

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

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

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

348 
let 
40286  349 
val [TVar (xi, S)] = filter Type_Infer.is_paramT TU; 
350 
val [T] = filter_out Type_Infer.is_paramT TU; 

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

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

352 
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

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

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

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

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

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

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

362 
 simplify done (((T, U), error_pack) :: todo) (tye_idx as (tye, idx)) = 
40286  363 
(case (Type_Infer.deref tye T, Type_Infer.deref tye U) of 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

366 
else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx 
40836  367 
else error (gen_msg err (a ^ " is not a subtype of " ^ b)) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

368 
 (Type (a, Ts), Type (b, Us)) => 
40836  369 
if a <> b then error (gen_msg err "different constructors") 
370 
(fst tye_idx) error_pack 

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

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

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

375 
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

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

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

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

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

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

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

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

387 

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

388 

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

389 
(* do simplification *) 
40282  390 

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

391 
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

392 

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

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

395 

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

396 
fun find_cycle_packs nodes = 
40836  397 
let 
398 
val (but_last, last) = split_last nodes 

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

400 
in 

401 
map_filter 

40838  402 
(fn (TU, pack) => if member (op =) pairs TU then SOME pack else NONE) 
40836  403 
cs' 
404 
end; 

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

405 

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

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

407 
in terms of the subtyperelation (excluding T itself)*) 
40282  408 
fun styps super T = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

411 

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

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

414 
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

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

417 
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

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

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

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

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

423 

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

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

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

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

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

431 
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

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

433 

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

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

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

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

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

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

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

440 

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

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

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

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

445 
let 
42388  446 
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

447 
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

448 
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

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

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

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

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

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

455 

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

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

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

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

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

461 
val G' = maybe_new_typnodes [T, U] G; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

462 
val (G'', tye_idx') = (add_edge (T, U) G', tye_idx) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

466 
fold 
40836  467 
(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

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

469 
err_bound ctxt 
40836  470 
(gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx) 
471 
(find_cycle_packs cycle))) 

472 
cycles tye_idx 

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

473 
in 
40836  474 
collapse (tye, idx) cycles G 
475 
end 

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

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

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

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

480 
let 
40836  481 
(*all cycles collapse to one node, 
482 
because all of them share at least the nodes x and y*) 

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

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

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

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

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

487 
val G' = Typ_Graph.del_nodes (tl nodes) G; 
40836  488 
fun check_and_gen super T' = 
489 
let val U = Type_Infer.deref tye T'; 

490 
in 

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

492 
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

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

494 
if super andalso 
40836  495 
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

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

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

499 
(fst tye_idx) 
40836  500 
(maps find_cycle_packs cycles @ find_error_pack super T') 
501 
end; 

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

502 
in 
40836  503 
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

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

505 

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

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

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

510 
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

511 
val raw_bound = get_bound G key; 
40286  512 
val bound = map (Type_Infer.deref tye) raw_bound; 
513 
val not_params = filter_out Type_Infer.is_paramT bound; 

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

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

516 
NONE => NONE 
40282  517 
 SOME S => 
40286  518 
SOME 
519 
(map nameT 

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

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

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

522 
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

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

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

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

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

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

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

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

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

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

534 
let 
40286  535 
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

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

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

538 
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

539 
then apfst (Vartab.update (xi, T)) tye_idx 
40836  540 
else err_bound ctxt (gen_msg err ("assigned simple type " ^ s ^ 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

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

547 

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

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

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

550 

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

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

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

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

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

555 
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

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

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

558 
assign_alternating ts 
40836  559 
(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

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

561 

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

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

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

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

566 
let 
40286  567 
val max_params = 
568 
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

569 
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

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

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

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

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

576 

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

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

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

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

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

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

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

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

584 

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

585 

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

586 

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

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

588 

40836  589 
fun gen_coercion ctxt tye (T1, T2) = 
590 
(case pairself (Type_Infer.deref tye) (T1, T2) of 

591 
((Type (a, [])), (Type (b, []))) => 

592 
if a = b 

593 
then Abs (Name.uu, Type (a, []), Bound 0) 

594 
else 

595 
(case Symreltab.lookup (coes_of ctxt) (a, b) of 

596 
NONE => raise Fail (a ^ " is not a subtype of " ^ b) 

597 
 SOME co => co) 

598 
 ((Type (a, Ts)), (Type (b, Us))) => 

599 
if a <> b 

600 
then raise Fail ("Different constructors: " ^ a ^ " and " ^ b) 

601 
else 

602 
let 

603 
fun inst t Ts = 

604 
Term.subst_vars 

605 
(((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t; 

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

606 
fun sub_co (COVARIANT, TU) = SOME (gen_coercion ctxt tye TU) 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

607 
 sub_co (CONTRAVARIANT, TU) = SOME (gen_coercion ctxt tye (swap TU)) 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

608 
 sub_co (INVARIANT_TO T, _) = NONE; 
40836  609 
fun ts_of [] = [] 
610 
 ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs); 

611 
in 

612 
(case Symtab.lookup (tmaps_of ctxt) a of 

613 
NONE => raise Fail ("No map function for " ^ a ^ " known") 

614 
 SOME tmap => 

615 
let 

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

616 
val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us)); 
40836  617 
in 
43591
d4cbd6feffdf
collapse map functions with identity subcoercions to identities;
traytel
parents:
43278
diff
changeset

618 
if null (filter (not o is_identity) used_coes) 
d4cbd6feffdf
collapse map functions with identity subcoercions to identities;
traytel
parents:
43278
diff
changeset

619 
then Abs (Name.uu, Type (a, Ts), Bound 0) 
d4cbd6feffdf
collapse map functions with identity subcoercions to identities;
traytel
parents:
43278
diff
changeset

620 
else Term.list_comb 
40836  621 
(inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes) 
622 
end) 

623 
end 

624 
 (T, U) => 

625 
if Type.could_unify (T, U) 

626 
then Abs (Name.uu, T, Bound 0) 

627 
else raise Fail ("Cannot generate coercion from " 

628 
^ Syntax.string_of_typ ctxt T ^ " to " ^ Syntax.string_of_typ ctxt U)); 

629 

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

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

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

632 
fun insert _ (Const (c, T)) = 
40836  633 
let val T' = T; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

634 
in (Const (c, T'), T') end 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

635 
 insert _ (Free (x, T)) = 
40836  636 
let val T' = T; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

637 
in (Free (x, T'), T') end 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

638 
 insert _ (Var (xi, T)) = 
40836  639 
let val T' = T; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

640 
in (Var (xi, T'), T') end 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

645 
let 
40836  646 
val T' = T; 
40282  647 
val (t', T'') = insert (T' :: bs) t; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

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

653 
val (t', Type ("fun", [U, T])) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42402
diff
changeset

654 
apsnd (Type_Infer.deref tye) (insert bs t); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

656 
in 
40836  657 
if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U') 
658 
then (t' $ u', T) 

659 
else (t' $ (gen_coercion ctxt tye (U', U) $ u'), T) 

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

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

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

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

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

664 

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

665 

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

666 

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

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

668 

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

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

671 
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

672 

40836  673 
fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx) 
674 
 inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx) 

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

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

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

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

681 
 inf bs (t $ u) tye_idx = 

682 
let 

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

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

685 
val V = Type_Infer.mk_param idx []; 

686 
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

687 
handle NO_UNIFIER (msg, tye') => 
40836  688 
raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U); 
689 
in (tu, V, tye_idx'') end; 

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

690 

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

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

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

694 

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

695 
val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx) 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset

696 
handle TYPE_INFERENCE_ERROR err => 
40836  697 
let 
698 
fun gen_single t (tye_idx, constraints) = 

699 
let val (_, tye_idx', constraints') = generate_constraints ctxt err t tye_idx 

700 
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

701 

40836  702 
val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []); 
703 
val (tye, idx) = process_constraints ctxt err constraints tye_idx; 

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

704 
in 
40836  705 
(insert_coercions ctxt tye ts, (tye, idx)) 
706 
end); 

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

707 

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

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

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

710 

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

711 

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

712 

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

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

714 

40283  715 
(* term check *) 
716 

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

717 
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

718 

40283  719 
val add_term_check = 
720 
Syntax.add_term_check ~100 "coercions" 

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

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

722 

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

723 

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

725 

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

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

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

728 
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

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

730 

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

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

732 
Syntax.string_of_typ ctxt (fastype_of t) ^ 
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

733 
"\n\nThe general type signature of a map function is" ^ 
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset

734 
"\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^ 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

735 
"\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

736 

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

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

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

739 

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

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

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

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

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

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

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

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

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

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

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

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

752 

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

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

754 
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

755 
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

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

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

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

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

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

761 
 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

762 

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

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

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

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

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

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

768 

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

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

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

771 
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

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

773 

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

774 
fun err_coercion () = error ("Bad type for coercion " ^ 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

775 
Syntax.string_of_term ctxt t ^ ":\n" ^ 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

777 

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

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

780 

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

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

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

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

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

785 

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

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

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

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

789 
 _ => err_coercion ()); 
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 
fun coercion_data_update (tab, G) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

795 
handle Graph.CYCLES _ => error (a ^ " is already a subtype of " ^ b ^ 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

796 
"!\n\nCannot add coercion of type: " ^ a ^ " => " ^ b); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

799 
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

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

801 

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

802 
fun complex_coercion tab G (a, b) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

804 
val path = hd (Graph.irreducible_paths G (a, b)) 
40836  805 
val path' = fst (split_last path) ~~ tl path 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

806 
in Abs (Name.uu, Type (a, []), 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

807 
fold (fn t => fn u => t $ u) (map (the o Symreltab.lookup tab) path') (Bound 0)) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

809 

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

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

811 
(fn pair => fn tab => Symreltab.update (pair, complex_coercion tab G_and_new pair) tab) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

812 
(filter (fn pair => pair <> (a, b)) new_edges) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

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

820 

40283  821 

822 
(* theory setup *) 

823 

824 
val setup = 

825 
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

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

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

828 
"declaration of new coercions" #> 
40297  829 
Attrib.setup @{binding coercion_map} 
40284
c9acf88447e6
export declarations by default, to allow other ML packages bypass concrete syntax;
wenzelm
parents:
40283
diff
changeset

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

832 

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

833 
end; 