author  blanchet 
Tue, 07 Dec 2010 11:56:01 +0100  
changeset 41051  2ed1b971fc20 
parent 40939  2c150063cd4d 
child 41353  684003dbda54 
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 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

9 
datatype variance = COVARIANT  CONTRAVARIANT  INVARIANT 
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset

10 
val coercion_enabled: bool Config.T 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

11 
val infer_types: Proof.context > (string > typ option) > (indexname > typ option) > 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

13 
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

14 
val add_coercion: term > Context.generic > Context.generic 
40836  15 
val gen_coercion: Proof.context > typ Vartab.table > (typ * typ) > term 
40283  16 
val setup: theory > theory 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

18 

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

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

23 

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

24 
datatype variance = COVARIANT  CONTRAVARIANT  INVARIANT 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

25 

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

26 
datatype data = Data of 
40282  27 
{coes: term Symreltab.table, (*coercions table*) 
28 
coes_graph: unit Graph.T, (*coercions graph*) 

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

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

30 

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

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

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

33 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

49 
make_data (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 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 
(f coes, 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_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 
(coes, f coes_graph, tmaps)); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

58 

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

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

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

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

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

63 

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

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

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

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

67 

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

69 

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

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

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

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

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

75 

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

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

77 

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

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

79 
fun t_of s = Type (s, []); 
40286  80 

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

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

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

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

84 

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

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

87 
val is_freeT = fn (TFree _) => true  _ => false; 
40286  88 
val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi)  _ => false; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

89 

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

90 

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

92 

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

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

95 

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

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

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

98 
val thy = ProofContext.theory_of ctxt; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

99 
val pp = Syntax.pp ctxt; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

100 
val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

101 

40282  102 

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

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

104 

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

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

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

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

108 

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

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

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

111 
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

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

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

114 
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

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

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

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

120 
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

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

123 
 meets _ tye_idx = tye_idx; 
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 
val weak_meet = if weak then fn _ => I else meet 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

126 

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

127 

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

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

129 

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

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

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

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

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

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

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

136 
 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

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

138 

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

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

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

141 
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

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

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

144 

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

147 

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

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

149 
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

150 

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

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

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

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

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

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

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

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

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

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

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

162 

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

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

164 

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

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

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

167 

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

168 

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

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

170 

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

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

172 
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

173 
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

174 
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

175 
fun maybe_new_typnodes Ts G = fold maybe_new_typnode Ts G; 
40282  176 
fun new_imm_preds 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_preds G) Ts)); 
40282  178 
fun new_imm_succs G Ts = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

179 
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

180 

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

183 

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

184 
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

185 
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

186 

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

187 

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

188 

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

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

190 

40836  191 
fun gen_msg err msg = 
192 
err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^ 

193 
(if msg = "" then "" else ": " ^ msg) ^ "\n"; 

194 

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

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

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

197 
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

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

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

200 
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

203 

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

204 
fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); 
40836  205 

206 
fun unif_failed msg = 

207 
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n"; 

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

208 

40836  209 
fun subtyping_err_appl_msg ctxt msg tye bs t T u U () = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

210 
let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U] 
40836  211 
in msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end; 
212 

213 
fun err_appl_msg ctxt msg tye bs t T u U () = 

214 
let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U] 

215 
in unif_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end; 

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

216 

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

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

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

219 
val (_, Ts') = prep_output ctxt tye [] [] Ts; 
40836  220 
val text = cat_lines ([msg, 
221 
"Cannot unify a list of types that should be the same:", 

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

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

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

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

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

226 

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

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

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

229 
val pp = Syntax.pp ctxt; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

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

238 
Pretty.typ pp T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, Pretty.typ pp U, 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

239 
Pretty.brk 3, Pretty.str "from function application", Pretty.brk 2, 
40836  240 
Pretty.block [Pretty.term pp (t $ u)]])) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

245 

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

246 

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

247 

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

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

249 

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

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

252 
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

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

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

255 
 gen cs bs (Bound i) tye_idx = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

258 
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

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

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

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

262 
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

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

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

266 
val tye_idx''= strong_unify ctxt (U > V, T) (tye, idx + 2) 
40836  267 
handle NO_UNIFIER (msg, tye') => error (gen_msg err msg); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

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

273 

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

274 

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

275 

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

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

277 

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

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

279 

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

281 
let 
40285  282 
val coes_graph = coes_graph_of ctxt; 
283 
val tmaps = tmaps_of ctxt; 

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

284 
val tsig = Sign.tsig_of (ProofContext.theory_of ctxt); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

285 
val pp = Syntax.pp ctxt; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

286 
val arity_sorts = Type.arity_sorts pp tsig; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

287 
val subsort = Type.subsort tsig; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

288 

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

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

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

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

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

294 

40282  295 

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

296 
(* check whether constraint simplification will terminate using weak unification *) 
40282  297 

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

298 
val _ = fold (fn (TU, error_pack) => fn tye_idx => 
40836  299 
weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, tye) => 
300 
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

301 

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

302 

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

303 
(* simplify constraints *) 
40282  304 

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

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

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

307 
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

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

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

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

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

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

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

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

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

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

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

318 
 INVARIANT => (cs, strong_unify ctxt constraint tye_idx 
40836  319 
handle NO_UNIFIER (msg, tye) => 
320 
error (gen_msg err ("failed to unify invariant arguments\n" ^ msg)))); 

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

321 
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

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

323 
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

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

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

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

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

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

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

332 
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

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

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

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

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

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

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

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

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

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

345 
(*TU is a pair of a parameter and a free/fixed variable*) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

351 
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

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

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

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

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

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

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

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

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

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

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

365 
else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx 
40836  366 
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

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

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

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

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

374 
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

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

376 
if T = U then simplify done todo tye_idx 
40282  377 
else if exists (is_freeT orf is_fixedvarT) [T, U] andalso 
40286  378 
exists Type_Infer.is_paramT [T, U] 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

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

386 

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 
(* do simplification *) 
40282  389 

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

390 
val (cs', tye_idx') = simplify_constraints cs tye_idx; 
40836  391 

392 
fun find_error_pack lower T' = map_filter 

393 
(fn ((T, U), pack) => if if lower then T' = U else T' = T then SOME pack else NONE) cs'; 

394 

395 
fun find_cycle_packs nodes = 

396 
let 

397 
val (but_last, last) = split_last nodes 

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

399 
in 

400 
map_filter 

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

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

404 

40282  405 
fun unify_list (T :: Ts) tye_idx = 
40836  406 
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

407 

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

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

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

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

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

413 

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

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

416 
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

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

419 
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

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

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

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

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

425 

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

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

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

430 
(fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

431 
fun fitting Ts S U = Type.of_sort tsig (t_of U, S) andalso styp_test U Ts 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

433 
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

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

435 

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

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

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

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

439 
/ / \ \ 
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 
'b::C1 'c::C2 ... T1 T2 ... 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

442 

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

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

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

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

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

448 
fun restriction T = Type.of_sort tsig (t_of T, S) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

449 
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

450 
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

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

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

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

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

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

457 

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

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

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

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

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

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

464 
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

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

466 
let 
40836  467 
val (tye, idx) = 
468 
fold 

469 
(fn cycle => fn tye_idx' => (unify_list cycle tye_idx' 

470 
handle NO_UNIFIER (msg, tye) => 

471 
err_bound ctxt 

472 
(gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx) 

473 
(find_cycle_packs cycle))) 

474 
cycles tye_idx 

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

475 
in 
40836  476 
collapse (tye, idx) cycles G 
477 
end 

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

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

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

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

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

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

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

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

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

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

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

492 
in 

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

494 
then if super then (hd nodes, T') else (T', hd nodes) 

495 
else 

496 
if super andalso 

497 
Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T') 

498 
else if not super andalso 

499 
Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes) 

500 
else err_bound ctxt (gen_msg err "cycle elimination produces inconsistent graph") 

501 
(fst tye_idx) 

502 
(maps find_cycle_packs cycles @ find_error_pack super T') 

503 
end; 

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

504 
in 
40836  505 
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

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

507 

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

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

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

512 
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

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

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

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

518 
NONE => NONE 
40282  519 
 SOME S => 
40286  520 
SOME 
521 
(map nameT 

522 
(filter_out Type_Infer.is_paramT (map (Type_Infer.deref tye) (get_bound G T))), 

523 
S)); 

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

524 
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

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

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

527 
else SOME (tightest lower S styps_and_sorts (map nameT not_params) 
40836  528 
handle BOUND_ERROR msg => 
529 
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

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

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

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

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

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

536 
let 
40286  537 
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

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

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

540 
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

541 
then apfst (Vartab.update (xi, T)) tye_idx 
40836  542 
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

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

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

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

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

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

549 

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

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

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

552 

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

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

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

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

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

557 
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

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

559 
in 
40836  560 
assign_alternating ts 
561 
(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

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

563 

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

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

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

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

568 
let 
40286  569 
val max_params = 
570 
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

571 
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

572 
in 
40836  573 
fold 
574 
(fn Ts => fn tye_idx' => unify_list Ts tye_idx' 

575 
handle NO_UNIFIER (msg, tye) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts) 

576 
to_unify tye_idx 

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

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

578 

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

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

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

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

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

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

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

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

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

588 

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

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

590 

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

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

594 
if a = b 

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

596 
else 

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

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

599 
 SOME co => co) 

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

601 
if a <> b 

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

603 
else 

604 
let 

605 
fun inst t Ts = 

606 
Term.subst_vars 

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

608 
fun sub_co (COVARIANT, TU) = gen_coercion ctxt tye TU 

609 
 sub_co (CONTRAVARIANT, TU) = gen_coercion ctxt tye (swap TU); 

610 
fun ts_of [] = [] 

611 
 ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs); 

612 
in 

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

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

615 
 SOME tmap => 

616 
let 

617 
val used_coes = map sub_co ((snd tmap) ~~ (Ts ~~ Us)); 

618 
in 

619 
Term.list_comb 

620 
(inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes) 

621 
end) 

622 
end 

623 
 (T, U) => 

624 
if Type.could_unify (T, U) 

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

626 
else raise Fail ("Cannot generate coercion from " 

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

628 

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

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

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

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

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

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

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

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

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

640 
 insert bs (Bound i) = 
40836  641 
let val T = nth bs i handle Subscript => err_loose i; 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

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

651 
let 
40836  652 
val (t', Type ("fun", [U, T])) = apsnd (Type_Infer.deref tye) (insert bs t); 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

657 
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

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

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

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

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

662 

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

663 

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 
(** assembling the pipeline **) 
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 
fun infer_types ctxt const_type var_type raw_ts = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

669 
val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

670 

40836  671 
fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx) 
672 
 inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx) 

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

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

675 
(t, snd (nth bs i handle Subscript => err_loose i), tye_idx) 

676 
 inf bs (Abs (x, T, t)) tye_idx = 

677 
let val (t', U, tye_idx') = inf ((x, T) :: bs) t tye_idx 

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

679 
 inf bs (t $ u) tye_idx = 

680 
let 

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

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

683 
val V = Type_Infer.mk_param idx []; 

684 
val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U > V, T) (tye, idx + 1)) 

685 
handle NO_UNIFIER (msg, tye') => 

686 
raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U); 

687 
in (tu, V, tye_idx'') end; 

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

688 

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

689 
fun infer_single t tye_idx = 
40836  690 
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

691 
in (t, tye_idx') end; 
40836  692 

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

693 
val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx) 
40836  694 
handle TYPE_INFERENCE_ERROR err => 
695 
let 

696 
fun gen_single t (tye_idx, constraints) = 

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

698 
in (tye_idx', constraints' @ constraints) end; 

699 

700 
val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []); 

701 
val (tye, idx) = process_constraints ctxt err constraints tye_idx; 

702 
in 

703 
(insert_coercions ctxt tye ts, (tye, idx)) 

704 
end); 

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

705 

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

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

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

708 

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

709 

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

712 

40283  713 
(* term check *) 
714 

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

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

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

717 
(try (Consts.the_constraint (ProofContext.consts_of ctxt))) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

719 

40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset

720 
val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false); 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset

721 

40283  722 
val add_term_check = 
723 
Syntax.add_term_check ~100 "coercions" 

724 
(fn xs => fn ctxt => 

40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset

725 
if Config.get ctxt coercion_enabled then 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset

726 
let val xs' = coercion_infer_types ctxt xs 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset

727 
in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset

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

729 

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

730 

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

732 

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

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

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

735 
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

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

737 

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

738 
fun err_str () = "\n\nthe general type signature for a map function is" ^ 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

740 
"\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)"; 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

741 

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

742 
fun gen_arg_var ([], []) = [] 
40282  743 
 gen_arg_var ((T, T') :: Ts, (U, U') :: Us) = 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

746 
else error ("Functions do not apply to arguments correctly:" ^ err_str ()) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

749 

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

750 
(* TODO: This function is only needed to introde the fun type map 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

751 
function: "% f g h . g o h o f". There must be a better solution. *) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

752 
fun balanced (Type (_, [])) (Type (_, [])) = true 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

754 
a = b andalso forall I (map2 balanced Ts Us) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

755 
 balanced (TFree _) (TFree _) = true 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

756 
 balanced (TVar _) (TVar _) = true 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

758 

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

759 
fun check_map_fun (pairs, []) (Type ("fun", [T as Type (C, Ts), U as Type (_, Us)])) = 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

760 
if balanced T U 
40282  761 
then ((pairs, Ts ~~ Us), C) 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

762 
else if C = "fun" 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

763 
then check_map_fun (pairs @ [(hd Ts, hd (tl Ts))], []) U 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

764 
else error ("Not a proper map function:" ^ err_str ()) 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

765 
 check_map_fun _ _ = error ("Not a proper map function:" ^ err_str ()); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

766 

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

767 
val res = check_map_fun ([], []) (fastype_of t); 
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
diff
changeset

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

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

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

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

772 

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

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

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

775 
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

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

777 

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

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

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

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

781 

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

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

784 

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

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

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

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

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

789 

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

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

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

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

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

794 

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

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

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

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

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

799 
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

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

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

802 
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

803 
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

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

805 

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

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

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

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

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

811 
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

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

813 

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

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

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

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

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

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

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

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

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

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

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

824 

40283  825 

826 
(* theory setup *) 

827 

828 
val setup = 

40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset

829 
coercion_enabled_setup #> 
40283  830 
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

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

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

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

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

837 

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

838 
end; 