author | traytel |
Tue, 02 Nov 2010 12:37:12 +0100 | |
changeset 40297 | c753e3f8b4d6 |
parent 40286 | b928e3960446 |
child 40836 | a81d66d72e70 |
permissions | -rw-r--r-- |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Tools/subtyping.ML |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
3 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
4 |
Coercive subtyping via subtype constraints. |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
5 |
*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
6 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
7 |
signature SUBTYPING = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
8 |
sig |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
9 |
datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
10 |
val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) -> |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
11 |
term list -> term list |
40284
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
12 |
val add_type_map: term -> Context.generic -> Context.generic |
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
13 |
val add_coercion: term -> Context.generic -> Context.generic |
40283 | 14 |
val setup: theory -> theory |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
15 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
16 |
|
40283 | 17 |
structure Subtyping: SUBTYPING = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
18 |
struct |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
19 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
20 |
(** coercions data **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
21 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
22 |
datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
23 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
24 |
datatype data = Data of |
40282 | 25 |
{coes: term Symreltab.table, (*coercions table*) |
26 |
coes_graph: unit Graph.T, (*coercions graph*) |
|
27 |
tmaps: (term * variance list) Symtab.table}; (*map functions*) |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
28 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
29 |
fun make_data (coes, coes_graph, tmaps) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
30 |
Data {coes = coes, coes_graph = coes_graph, tmaps = tmaps}; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
31 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
32 |
structure Data = Generic_Data |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
33 |
( |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
34 |
type T = data; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
35 |
val empty = make_data (Symreltab.empty, Graph.empty, Symtab.empty); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
36 |
val extend = I; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
37 |
fun merge |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
38 |
(Data {coes = coes1, coes_graph = coes_graph1, tmaps = tmaps1}, |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
39 |
Data {coes = coes2, coes_graph = coes_graph2, tmaps = tmaps2}) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
40 |
make_data (Symreltab.merge (op aconv) (coes1, coes2), |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
41 |
Graph.merge (op =) (coes_graph1, coes_graph2), |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
42 |
Symtab.merge (eq_pair (op aconv) (op =)) (tmaps1, tmaps2)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
43 |
); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
44 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
45 |
fun map_data f = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
46 |
Data.map (fn Data {coes, coes_graph, tmaps} => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
47 |
make_data (f (coes, coes_graph, tmaps))); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
48 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
49 |
fun map_coes f = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
50 |
map_data (fn (coes, coes_graph, tmaps) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
51 |
(f coes, coes_graph, tmaps)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
52 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
53 |
fun map_coes_graph f = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
54 |
map_data (fn (coes, coes_graph, tmaps) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
55 |
(coes, f coes_graph, tmaps)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
56 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
57 |
fun map_coes_and_graph f = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
58 |
map_data (fn (coes, coes_graph, tmaps) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
59 |
let val (coes', coes_graph') = f (coes, coes_graph); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
60 |
in (coes', coes_graph', tmaps) end); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
61 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
62 |
fun map_tmaps f = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
63 |
map_data (fn (coes, coes_graph, tmaps) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
64 |
(coes, coes_graph, f tmaps)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
65 |
|
40285 | 66 |
val rep_data = (fn Data args => args) o Data.get o Context.Proof; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
67 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
68 |
val coes_of = #coes o rep_data; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
69 |
val coes_graph_of = #coes_graph o rep_data; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
70 |
val tmaps_of = #tmaps o rep_data; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
71 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
72 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
73 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
74 |
(** utils **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
75 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
76 |
fun nameT (Type (s, [])) = s; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
77 |
fun t_of s = Type (s, []); |
40286 | 78 |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
79 |
fun sort_of (TFree (_, S)) = SOME S |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
80 |
| sort_of (TVar (_, S)) = SOME S |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
81 |
| sort_of _ = NONE; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
82 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
83 |
val is_typeT = fn (Type _) => true | _ => false; |
40282 | 84 |
val is_compT = fn (Type (_, _ :: _)) => true | _ => false; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
85 |
val is_freeT = fn (TFree _) => true | _ => false; |
40286 | 86 |
val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
87 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
88 |
|
40282 | 89 |
(* unification *) (* TODO dup? needed for weak unification *) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
90 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
91 |
exception NO_UNIFIER of string * typ Vartab.table; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
92 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
93 |
fun unify weak ctxt = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
94 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
95 |
val thy = ProofContext.theory_of ctxt; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
96 |
val pp = Syntax.pp ctxt; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
97 |
val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
98 |
|
40282 | 99 |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
100 |
(* adjust sorts of parameters *) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
101 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
102 |
fun not_of_sort x S' S = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
103 |
"Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
104 |
Syntax.string_of_sort ctxt S; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
105 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
106 |
fun meet (_, []) tye_idx = tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
107 |
| meet (Type (a, Ts), S) (tye_idx as (tye, _)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
108 |
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 (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
109 |
| meet (TFree (x, S'), S) (tye_idx as (tye, _)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
110 |
if Sign.subsort thy (S', S) then tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
111 |
else raise NO_UNIFIER (not_of_sort x S' S, tye) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
112 |
| meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
113 |
if Sign.subsort thy (S', S) then tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
114 |
else if Type_Infer.is_param xi then |
40286 | 115 |
(Vartab.update_new |
116 |
(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 (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
117 |
else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
118 |
and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = |
40286 | 119 |
meets (Ts, Ss) (meet (Type_Infer.deref tye T, S) tye_idx) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
120 |
| meets _ tye_idx = tye_idx; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
121 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
122 |
val weak_meet = if weak then fn _ => I else meet |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
123 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
124 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
125 |
(* occurs check and assignment *) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
126 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
127 |
fun occurs_check tye xi (TVar (xi', _)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
128 |
if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
129 |
else |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
130 |
(case Vartab.lookup tye xi' of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
131 |
NONE => () |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
132 |
| SOME T => occurs_check tye xi T) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
133 |
| occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
134 |
| occurs_check _ _ _ = (); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
135 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
136 |
fun assign xi (T as TVar (xi', _)) S env = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
137 |
if xi = xi' then env |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
138 |
else env |> weak_meet (T, S) |>> Vartab.update_new (xi, T) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
139 |
| assign xi T S (env as (tye, _)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
140 |
(occurs_check tye xi T; env |> weak_meet (T, S) |>> Vartab.update_new (xi, T)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
141 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
142 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
143 |
(* unification *) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
144 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
145 |
fun show_tycon (a, Ts) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
146 |
quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
147 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
148 |
fun unif (T1, T2) (env as (tye, _)) = |
40286 | 149 |
(case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
150 |
((true, TVar (xi, S)), (_, T)) => assign xi T S env |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
151 |
| ((_, T), (true, TVar (xi, S))) => assign xi T S env |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
152 |
| ((_, Type (a, Ts)), (_, Type (b, Us))) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
153 |
if weak andalso null Ts andalso null Us then env |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
154 |
else if a <> b then |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
155 |
raise NO_UNIFIER |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
156 |
("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
157 |
else fold unif (Ts ~~ Us) env |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
158 |
| ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
159 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
160 |
in unif end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
161 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
162 |
val weak_unify = unify true; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
163 |
val strong_unify = unify false; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
164 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
165 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
166 |
(* Typ_Graph shortcuts *) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
167 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
168 |
val add_edge = Typ_Graph.add_edge_acyclic; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
169 |
fun get_preds G T = Typ_Graph.all_preds G [T]; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
170 |
fun get_succs G T = Typ_Graph.all_succs G [T]; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
171 |
fun maybe_new_typnode T G = perhaps (try (Typ_Graph.new_node (T, ()))) G; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
172 |
fun maybe_new_typnodes Ts G = fold maybe_new_typnode Ts G; |
40282 | 173 |
fun new_imm_preds G Ts = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
174 |
subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.imm_preds G) Ts)); |
40282 | 175 |
fun new_imm_succs G Ts = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
176 |
subtract op= Ts (distinct (op =) (maps (Typ_Graph.imm_succs G) Ts)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
177 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
178 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
179 |
(* Graph shortcuts *) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
180 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
181 |
fun maybe_new_node s G = perhaps (try (Graph.new_node (s, ()))) G |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
182 |
fun maybe_new_nodes ss G = fold maybe_new_node ss G |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
183 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
184 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
185 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
186 |
(** error messages **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
187 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
188 |
fun prep_output ctxt tye bs ts Ts = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
189 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
190 |
val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
191 |
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
192 |
fun prep t = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
193 |
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
194 |
in Term.subst_bounds (map Syntax.mark_boundT xs, t) end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
195 |
in (map prep ts', Ts') end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
196 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
197 |
fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
198 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
199 |
fun inf_failed msg = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
200 |
"Subtype inference failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n"; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
201 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
202 |
fun err_appl ctxt msg tye bs t T u U = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
203 |
let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U] |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
204 |
in error (inf_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n") end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
205 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
206 |
fun err_subtype ctxt msg tye (bs, t $ u, U, V, U') = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
207 |
err_appl ctxt msg tye bs t (U --> V) u U'; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
208 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
209 |
fun err_list ctxt msg tye Ts = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
210 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
211 |
val (_, Ts') = prep_output ctxt tye [] [] Ts; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
212 |
val text = cat_lines ([inf_failed msg, |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
213 |
"Cannot unify a list of types that should be the same,", |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
214 |
"according to suptype dependencies:", |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
215 |
(Pretty.string_of (Pretty.list "[" "]" (map (Pretty.typ (Syntax.pp ctxt)) Ts')))]); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
216 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
217 |
error text |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
218 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
219 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
220 |
fun err_bound ctxt msg tye packs = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
221 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
222 |
val pp = Syntax.pp ctxt; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
223 |
val (ts, Ts) = fold |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
224 |
(fn (bs, t $ u, U, _, U') => fn (ts, Ts) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
225 |
let val (t', T') = prep_output ctxt tye bs [t, u] [U, U'] |
40282 | 226 |
in (t' :: ts, T' :: Ts) end) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
227 |
packs ([], []); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
228 |
val text = cat_lines ([inf_failed msg, "Cannot fullfill subtype constraints:"] @ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
229 |
(map2 (fn [t, u] => fn [T, U] => Pretty.string_of ( |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
230 |
Pretty.block [ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
231 |
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 (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
232 |
Pretty.brk 3, Pretty.str "from function application", Pretty.brk 2, |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
233 |
Pretty.block [Pretty.term pp t, Pretty.brk 1, Pretty.term pp u]])) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
234 |
ts Ts)) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
235 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
236 |
error text |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
237 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
238 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
239 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
240 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
241 |
(** constraint generation **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
242 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
243 |
fun generate_constraints ctxt = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
244 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
245 |
fun gen cs _ (Const (_, T)) tye_idx = (T, tye_idx, cs) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
246 |
| gen cs _ (Free (_, T)) tye_idx = (T, tye_idx, cs) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
247 |
| gen cs _ (Var (_, T)) tye_idx = (T, tye_idx, cs) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
248 |
| gen cs bs (Bound i) tye_idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
249 |
(snd (nth bs i handle Subscript => err_loose i), tye_idx, cs) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
250 |
| gen cs bs (Abs (x, T, t)) tye_idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
251 |
let val (U, tye_idx', cs') = gen cs ((x, T) :: bs) t tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
252 |
in (T --> U, tye_idx', cs') end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
253 |
| gen cs bs (t $ u) tye_idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
254 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
255 |
val (T, tye_idx', cs') = gen cs bs t tye_idx; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
256 |
val (U', (tye, idx), cs'') = gen cs' bs u tye_idx'; |
40286 | 257 |
val U = Type_Infer.mk_param idx []; |
258 |
val V = Type_Infer.mk_param (idx + 1) []; |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
259 |
val tye_idx''= strong_unify ctxt (U --> V, T) (tye, idx + 2) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
260 |
handle NO_UNIFIER (msg, tye') => err_appl ctxt msg tye' bs t T u U; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
261 |
val error_pack = (bs, t $ u, U, V, U'); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
262 |
in (V, tye_idx'', ((U', U), error_pack) :: cs'') end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
263 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
264 |
gen [] [] |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
265 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
266 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
267 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
268 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
269 |
(** constraint resolution **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
270 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
271 |
exception BOUND_ERROR of string; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
272 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
273 |
fun process_constraints ctxt cs tye_idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
274 |
let |
40285 | 275 |
val coes_graph = coes_graph_of ctxt; |
276 |
val tmaps = tmaps_of ctxt; |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
277 |
val tsig = Sign.tsig_of (ProofContext.theory_of ctxt); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
278 |
val pp = Syntax.pp ctxt; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
279 |
val arity_sorts = Type.arity_sorts pp tsig; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
280 |
val subsort = Type.subsort tsig; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
281 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
282 |
fun split_cs _ [] = ([], []) |
40282 | 283 |
| split_cs f (c :: cs) = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
284 |
(case pairself f (fst c) of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
285 |
(false, false) => apsnd (cons c) (split_cs f cs) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
286 |
| _ => apfst (cons c) (split_cs f cs)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
287 |
|
40282 | 288 |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
289 |
(* check whether constraint simplification will terminate using weak unification *) |
40282 | 290 |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
291 |
val _ = fold (fn (TU, error_pack) => fn tye_idx => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
292 |
(weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, tye) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
293 |
err_subtype ctxt ("Weak unification of subtype constraints fails:\n" ^ msg) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
294 |
tye error_pack)) cs tye_idx; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
295 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
296 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
297 |
(* simplify constraints *) |
40282 | 298 |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
299 |
fun simplify_constraints cs tye_idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
300 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
301 |
fun contract a Ts Us error_pack done todo tye idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
302 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
303 |
val arg_var = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
304 |
(case Symtab.lookup tmaps a of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
305 |
(*everything is invariant for unknown constructors*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
306 |
NONE => replicate (length Ts) INVARIANT |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
307 |
| SOME av => snd av); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
308 |
fun new_constraints (variance, constraint) (cs, tye_idx) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
309 |
(case variance of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
310 |
COVARIANT => (constraint :: cs, tye_idx) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
311 |
| CONTRAVARIANT => (swap constraint :: cs, tye_idx) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
312 |
| INVARIANT => (cs, strong_unify ctxt constraint tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
313 |
handle NO_UNIFIER (msg, tye) => err_subtype ctxt msg tye error_pack)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
314 |
val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack)) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
315 |
(fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx))); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
316 |
val test_update = is_compT orf is_freeT orf is_fixedvarT; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
317 |
val (ch, done') = |
40286 | 318 |
if not (null new) then ([], done) |
319 |
else split_cs (test_update o Type_Infer.deref tye') done; |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
320 |
val todo' = ch @ todo; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
321 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
322 |
simplify done' (new @ todo') (tye', idx') |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
323 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
324 |
(*xi is definitely a parameter*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
325 |
and expand varleq xi S a Ts error_pack done todo tye idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
326 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
327 |
val n = length Ts; |
40286 | 328 |
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 (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
329 |
val tye' = Vartab.update_new (xi, Type(a, args)) tye; |
40286 | 330 |
val (ch, done') = split_cs (is_compT o Type_Infer.deref tye') done; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
331 |
val todo' = ch @ todo; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
332 |
val new = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
333 |
if varleq then (Type(a, args), Type (a, Ts)) |
40286 | 334 |
else (Type (a, Ts), Type (a, args)); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
335 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
336 |
simplify done' ((new, error_pack) :: todo') (tye', idx + n) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
337 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
338 |
(*TU is a pair of a parameter and a free/fixed variable*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
339 |
and eliminate TU error_pack done todo tye idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
340 |
let |
40286 | 341 |
val [TVar (xi, S)] = filter Type_Infer.is_paramT TU; |
342 |
val [T] = filter_out Type_Infer.is_paramT TU; |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
343 |
val SOME S' = sort_of T; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
344 |
val test_update = if is_freeT T then is_freeT else is_fixedvarT; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
345 |
val tye' = Vartab.update_new (xi, T) tye; |
40286 | 346 |
val (ch, done') = split_cs (test_update o Type_Infer.deref tye') done; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
347 |
val todo' = ch @ todo; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
348 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
349 |
if subsort (S', S) (*TODO check this*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
350 |
then simplify done' todo' (tye', idx) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
351 |
else err_subtype ctxt "Sort mismatch" tye error_pack |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
352 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
353 |
and simplify done [] tye_idx = (done, tye_idx) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
354 |
| simplify done (((T, U), error_pack) :: todo) (tye_idx as (tye, idx)) = |
40286 | 355 |
(case (Type_Infer.deref tye T, Type_Infer.deref tye U) of |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
356 |
(Type (a, []), Type (b, [])) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
357 |
if a = b then simplify done todo tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
358 |
else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx |
40286 | 359 |
else err_subtype ctxt (a ^ " is not a subtype of " ^ b) (fst tye_idx) error_pack |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
360 |
| (Type (a, Ts), Type (b, Us)) => |
40286 | 361 |
if a <> b then err_subtype ctxt "Different constructors" (fst tye_idx) error_pack |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
362 |
else contract a Ts Us error_pack done todo tye idx |
40282 | 363 |
| (TVar (xi, S), Type (a, Ts as (_ :: _))) => |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
364 |
expand true xi S a Ts error_pack done todo tye idx |
40282 | 365 |
| (Type (a, Ts as (_ :: _)), TVar (xi, S)) => |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
366 |
expand false xi S a Ts error_pack done todo tye idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
367 |
| (T, U) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
368 |
if T = U then simplify done todo tye_idx |
40282 | 369 |
else if exists (is_freeT orf is_fixedvarT) [T, U] andalso |
40286 | 370 |
exists Type_Infer.is_paramT [T, U] |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
371 |
then eliminate [T, U] error_pack done todo tye idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
372 |
else if exists (is_freeT orf is_fixedvarT) [T, U] |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
373 |
then err_subtype ctxt "Not eliminated free/fixed variables" |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
374 |
(fst tye_idx) error_pack |
40282 | 375 |
else simplify (((T, U), error_pack) :: done) todo tye_idx); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
376 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
377 |
simplify [] cs tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
378 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
379 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
380 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
381 |
(* do simplification *) |
40282 | 382 |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
383 |
val (cs', tye_idx') = simplify_constraints cs tye_idx; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
384 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
385 |
fun find_error_pack lower T' = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
386 |
map snd (filter (fn ((T, U), _) => if lower then T' = U else T' = T) cs'); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
387 |
|
40282 | 388 |
fun unify_list (T :: Ts) tye_idx = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
389 |
fold (fn U => fn tye_idx => strong_unify ctxt (T, U) tye_idx |
40282 | 390 |
handle NO_UNIFIER (msg, tye) => err_list ctxt msg tye (T :: Ts)) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
391 |
Ts tye_idx; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
392 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
393 |
(*styps stands either for supertypes or for subtypes of a type T |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
394 |
in terms of the subtype-relation (excluding T itself)*) |
40282 | 395 |
fun styps super T = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
396 |
(if super then Graph.imm_succs else Graph.imm_preds) coes_graph T |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
397 |
handle Graph.UNDEF _ => []; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
398 |
|
40282 | 399 |
fun minmax sup (T :: Ts) = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
400 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
401 |
fun adjust T U = if sup then (T, U) else (U, T); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
402 |
fun extract T [] = T |
40282 | 403 |
| extract T (U :: Us) = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
404 |
if Graph.is_edge coes_graph (adjust T U) then extract T Us |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
405 |
else if Graph.is_edge coes_graph (adjust U T) then extract U Us |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
406 |
else raise BOUND_ERROR "Uncomparable types in type list"; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
407 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
408 |
t_of (extract T Ts) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
409 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
410 |
|
40282 | 411 |
fun ex_styp_of_sort super T styps_and_sorts = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
412 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
413 |
fun adjust T U = if super then (T, U) else (U, T); |
40282 | 414 |
fun styp_test U Ts = forall |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
415 |
(fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
416 |
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 (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
417 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
418 |
forall (fn (Ts, S) => exists (fitting Ts S) (T :: styps super T)) styps_and_sorts |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
419 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
420 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
421 |
(* computes the tightest possible, correct assignment for 'a::S |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
422 |
e.g. in the supremum case (sup = true): |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
423 |
------- 'a::S--- |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
424 |
/ / \ \ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
425 |
/ / \ \ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
426 |
'b::C1 'c::C2 ... T1 T2 ... |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
427 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
428 |
sorts - list of sorts [C1, C2, ...] |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
429 |
T::Ts - non-empty list of base types [T1, T2, ...] |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
430 |
*) |
40282 | 431 |
fun tightest sup S styps_and_sorts (T :: Ts) = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
432 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
433 |
fun restriction T = Type.of_sort tsig (t_of T, S) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
434 |
andalso ex_styp_of_sort (not sup) T styps_and_sorts; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
435 |
fun candidates T = inter (op =) (filter restriction (T :: styps sup T)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
436 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
437 |
(case fold candidates Ts (filter restriction (T :: styps sup T)) of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
438 |
[] => raise BOUND_ERROR ("No " ^ (if sup then "supremum" else "infimum")) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
439 |
| [T] => t_of T |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
440 |
| Ts => minmax sup Ts) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
441 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
442 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
443 |
fun build_graph G [] tye_idx = (G, tye_idx) |
40282 | 444 |
| build_graph G ((T, U) :: cs) tye_idx = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
445 |
if T = U then build_graph G cs tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
446 |
else |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
447 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
448 |
val G' = maybe_new_typnodes [T, U] G; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
449 |
val (G'', tye_idx') = (add_edge (T, U) G', tye_idx) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
450 |
handle Typ_Graph.CYCLES cycles => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
451 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
452 |
val (tye, idx) = fold unify_list cycles tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
453 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
454 |
(*all cycles collapse to one node, |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
455 |
because all of them share at least the nodes x and y*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
456 |
collapse (tye, idx) (distinct (op =) (flat cycles)) G |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
457 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
458 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
459 |
build_graph G'' cs tye_idx' |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
460 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
461 |
and collapse (tye, idx) nodes G = (*nodes non-empty list*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
462 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
463 |
val T = hd nodes; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
464 |
val P = new_imm_preds G nodes; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
465 |
val S = new_imm_succs G nodes; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
466 |
val G' = Typ_Graph.del_nodes (tl nodes) G; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
467 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
468 |
build_graph G' (map (fn x => (x, T)) P @ map (fn x => (T, x)) S) (tye, idx) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
469 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
470 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
471 |
fun assign_bound lower G key (tye_idx as (tye, _)) = |
40286 | 472 |
if Type_Infer.is_paramT (Type_Infer.deref tye key) then |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
473 |
let |
40286 | 474 |
val TVar (xi, S) = Type_Infer.deref tye key; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
475 |
val get_bound = if lower then get_preds else get_succs; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
476 |
val raw_bound = get_bound G key; |
40286 | 477 |
val bound = map (Type_Infer.deref tye) raw_bound; |
478 |
val not_params = filter_out Type_Infer.is_paramT bound; |
|
40282 | 479 |
fun to_fulfil T = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
480 |
(case sort_of T of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
481 |
NONE => NONE |
40282 | 482 |
| SOME S => |
40286 | 483 |
SOME |
484 |
(map nameT |
|
485 |
(filter_out Type_Infer.is_paramT (map (Type_Infer.deref tye) (get_bound G T))), |
|
486 |
S)); |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
487 |
val styps_and_sorts = distinct (op =) (map_filter to_fulfil raw_bound); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
488 |
val assignment = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
489 |
if null bound orelse null not_params then NONE |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
490 |
else SOME (tightest lower S styps_and_sorts (map nameT not_params) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
491 |
handle BOUND_ERROR msg => err_bound ctxt msg tye (find_error_pack lower key)) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
492 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
493 |
(case assignment of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
494 |
NONE => tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
495 |
| SOME T => |
40286 | 496 |
if Type_Infer.is_paramT T then tye_idx |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
497 |
else if lower then (*upper bound check*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
498 |
let |
40286 | 499 |
val other_bound = map (Type_Infer.deref tye) (get_succs G key); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
500 |
val s = nameT T; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
501 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
502 |
if subset (op = o apfst nameT) (filter is_typeT other_bound, s :: styps true s) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
503 |
then apfst (Vartab.update (xi, T)) tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
504 |
else err_bound ctxt ("Assigned simple type " ^ s ^ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
505 |
" clashes with the upper bound of variable " ^ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
506 |
Syntax.string_of_typ ctxt (TVar(xi, S))) tye (find_error_pack (not lower) key) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
507 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
508 |
else apfst (Vartab.update (xi, T)) tye_idx) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
509 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
510 |
else tye_idx; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
511 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
512 |
val assign_lb = assign_bound true; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
513 |
val assign_ub = assign_bound false; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
514 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
515 |
fun assign_alternating ts' ts G tye_idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
516 |
if ts' = ts then tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
517 |
else |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
518 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
519 |
val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
520 |
|> fold (assign_ub G) ts; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
521 |
in |
40286 | 522 |
assign_alternating ts (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx' |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
523 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
524 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
525 |
(*Unify all weakly connected components of the constraint forest, |
40282 | 526 |
that contain only params. These are the only WCCs that contain |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
527 |
params anyway.*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
528 |
fun unify_params G (tye_idx as (tye, _)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
529 |
let |
40286 | 530 |
val max_params = |
531 |
filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G); |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
532 |
val to_unify = map (fn T => T :: get_preds G T) max_params; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
533 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
534 |
fold unify_list to_unify tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
535 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
536 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
537 |
fun solve_constraints G tye_idx = tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
538 |
|> assign_alternating [] (Typ_Graph.keys G) G |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
539 |
|> unify_params G; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
540 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
541 |
build_graph Typ_Graph.empty (map fst cs') tye_idx' |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
542 |
|-> solve_constraints |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
543 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
544 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
545 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
546 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
547 |
(** coercion insertion **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
548 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
549 |
fun insert_coercions ctxt tye ts = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
550 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
551 |
fun deep_deref T = |
40286 | 552 |
(case Type_Infer.deref tye T of |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
553 |
Type (a, Ts) => Type (a, map deep_deref Ts) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
554 |
| U => U); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
555 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
556 |
fun gen_coercion ((Type (a, [])), (Type (b, []))) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
557 |
if a = b |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
558 |
then Abs (Name.uu, Type (a, []), Bound 0) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
559 |
else |
40285 | 560 |
(case Symreltab.lookup (coes_of ctxt) (a, b) of |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
561 |
NONE => raise Fail (a ^ " is not a subtype of " ^ b) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
562 |
| SOME co => co) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
563 |
| gen_coercion ((Type (a, Ts)), (Type (b, Us))) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
564 |
if a <> b |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
565 |
then raise raise Fail ("Different constructors: " ^ a ^ " and " ^ b) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
566 |
else |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
567 |
let |
40282 | 568 |
fun inst t Ts = |
569 |
Term.subst_vars |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
570 |
(((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
571 |
fun sub_co (COVARIANT, TU) = gen_coercion TU |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
572 |
| sub_co (CONTRAVARIANT, TU) = gen_coercion (swap TU); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
573 |
fun ts_of [] = [] |
40282 | 574 |
| ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
575 |
in |
40285 | 576 |
(case Symtab.lookup (tmaps_of ctxt) a of |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
577 |
NONE => raise Fail ("No map function for " ^ a ^ " known") |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
578 |
| SOME tmap => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
579 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
580 |
val used_coes = map sub_co ((snd tmap) ~~ (Ts ~~ Us)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
581 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
582 |
Term.list_comb |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
583 |
(inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
584 |
end) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
585 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
586 |
| gen_coercion (T, U) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
587 |
if Type.could_unify (T, U) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
588 |
then Abs (Name.uu, T, Bound 0) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
589 |
else raise Fail ("Cannot generate coercion from " |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
590 |
^ Syntax.string_of_typ ctxt T ^ " to " ^ Syntax.string_of_typ ctxt U); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
591 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
592 |
fun insert _ (Const (c, T)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
593 |
let val T' = deep_deref T; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
594 |
in (Const (c, T'), T') end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
595 |
| insert _ (Free (x, T)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
596 |
let val T' = deep_deref T; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
597 |
in (Free (x, T'), T') end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
598 |
| insert _ (Var (xi, T)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
599 |
let val T' = deep_deref T; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
600 |
in (Var (xi, T'), T') end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
601 |
| insert bs (Bound i) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
602 |
let val T = nth bs i handle Subscript => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
603 |
raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
604 |
in (Bound i, T) end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
605 |
| insert bs (Abs (x, T, t)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
606 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
607 |
val T' = deep_deref T; |
40282 | 608 |
val (t', T'') = insert (T' :: bs) t; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
609 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
610 |
(Abs (x, T', t'), T' --> T'') |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
611 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
612 |
| insert bs (t $ u) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
613 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
614 |
val (t', Type ("fun", [U, T])) = insert bs t; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
615 |
val (u', U') = insert bs u; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
616 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
617 |
if U <> U' |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
618 |
then (t' $ (gen_coercion (U', U) $ u'), T) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
619 |
else (t' $ u', T) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
620 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
621 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
622 |
map (fst o insert []) ts |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
623 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
624 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
625 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
626 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
627 |
(** assembling the pipeline **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
628 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
629 |
fun infer_types ctxt const_type var_type raw_ts = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
630 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
631 |
val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
632 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
633 |
fun gen_all t (tye_idx, constraints) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
634 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
635 |
val (_, tye_idx', constraints') = generate_constraints ctxt t tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
636 |
in (tye_idx', constraints' @ constraints) end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
637 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
638 |
val (tye_idx, constraints) = fold gen_all ts ((Vartab.empty, idx), []); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
639 |
val (tye, _) = process_constraints ctxt constraints tye_idx; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
640 |
val ts' = insert_coercions ctxt tye ts; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
641 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
642 |
val (_, ts'') = Type_Infer.finish ctxt tye ([], ts'); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
643 |
in ts'' end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
644 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
645 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
646 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
647 |
(** installation **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
648 |
|
40283 | 649 |
(* term check *) |
650 |
||
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
651 |
fun coercion_infer_types ctxt = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
652 |
infer_types ctxt |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
653 |
(try (Consts.the_constraint (ProofContext.consts_of ctxt))) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
654 |
(ProofContext.def_type ctxt); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
655 |
|
40283 | 656 |
val add_term_check = |
657 |
Syntax.add_term_check ~100 "coercions" |
|
658 |
(fn xs => fn ctxt => |
|
659 |
let val xs' = coercion_infer_types ctxt xs |
|
660 |
in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end); |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
661 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
662 |
|
40283 | 663 |
(* declarations *) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
664 |
|
40284
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
665 |
fun add_type_map raw_t context = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
666 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
667 |
val ctxt = Context.proof_of context; |
40284
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
668 |
val t = singleton (Variable.polymorphic ctxt) raw_t; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
669 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
670 |
fun err_str () = "\n\nthe general type signature for a map function is" ^ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
671 |
"\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [x1, ..., xn]" ^ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
672 |
"\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)"; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
673 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
674 |
fun gen_arg_var ([], []) = [] |
40282 | 675 |
| gen_arg_var ((T, T') :: Ts, (U, U') :: Us) = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
676 |
if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
677 |
else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
678 |
else error ("Functions do not apply to arguments correctly:" ^ err_str ()) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
679 |
| gen_arg_var (_, _) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
680 |
error ("Different numbers of functions and arguments\n" ^ err_str ()); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
681 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
682 |
(* TODO: This function is only needed to introde the fun type map |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
683 |
function: "% f g h . g o h o f". There must be a better solution. *) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
684 |
fun balanced (Type (_, [])) (Type (_, [])) = true |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
685 |
| balanced (Type (a, Ts)) (Type (b, Us)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
686 |
a = b andalso forall I (map2 balanced Ts Us) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
687 |
| balanced (TFree _) (TFree _) = true |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
688 |
| balanced (TVar _) (TVar _) = true |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
689 |
| balanced _ _ = false; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
690 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
691 |
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 (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
692 |
if balanced T U |
40282 | 693 |
then ((pairs, Ts ~~ Us), C) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
694 |
else if C = "fun" |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
695 |
then check_map_fun (pairs @ [(hd Ts, hd (tl Ts))], []) U |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
696 |
else error ("Not a proper map function:" ^ err_str ()) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
697 |
| check_map_fun _ _ = error ("Not a proper map function:" ^ err_str ()); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
698 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
699 |
val res = check_map_fun ([], []) (fastype_of t); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
700 |
val res_av = gen_arg_var (fst res); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
701 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
702 |
map_tmaps (Symtab.update (snd res, (t, res_av))) context |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
703 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
704 |
|
40284
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
705 |
fun add_coercion raw_t context = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
706 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
707 |
val ctxt = Context.proof_of context; |
40284
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
708 |
val t = singleton (Variable.polymorphic ctxt) raw_t; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
709 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
710 |
fun err_coercion () = error ("Bad type for coercion " ^ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
711 |
Syntax.string_of_term ctxt t ^ ":\n" ^ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
712 |
Syntax.string_of_typ ctxt (fastype_of t)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
713 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
714 |
val (Type ("fun", [T1, T2])) = fastype_of t |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
715 |
handle Bind => err_coercion (); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
716 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
717 |
val a = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
718 |
(case T1 of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
719 |
Type (x, []) => x |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
720 |
| _ => err_coercion ()); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
721 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
722 |
val b = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
723 |
(case T2 of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
724 |
Type (x, []) => x |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
725 |
| _ => err_coercion ()); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
726 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
727 |
fun coercion_data_update (tab, G) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
728 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
729 |
val G' = maybe_new_nodes [a, b] G |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
730 |
val G'' = Graph.add_edge_trans_acyclic (a, b) G' |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
731 |
handle Graph.CYCLES _ => error (a ^ " is already a subtype of " ^ b ^ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
732 |
"!\n\nCannot add coercion of type: " ^ a ^ " => " ^ b); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
733 |
val new_edges = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
734 |
flat (Graph.dest G'' |> map (fn (x, ys) => ys |> map_filter (fn y => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
735 |
if Graph.is_edge G' (x, y) then NONE else SOME (x, y)))); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
736 |
val G_and_new = Graph.add_edge (a, b) G'; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
737 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
738 |
fun complex_coercion tab G (a, b) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
739 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
740 |
val path = hd (Graph.irreducible_paths G (a, b)) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
741 |
val path' = (fst (split_last path)) ~~ tl path |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
742 |
in Abs (Name.uu, Type (a, []), |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
743 |
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 (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
744 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
745 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
746 |
val tab' = fold |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
747 |
(fn pair => fn tab => Symreltab.update (pair, complex_coercion tab G_and_new pair) tab) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
748 |
(filter (fn pair => pair <> (a, b)) new_edges) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
749 |
(Symreltab.update ((a, b), t) tab); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
750 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
751 |
(tab', G'') |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
752 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
753 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
754 |
map_coes_and_graph coercion_data_update context |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
755 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
756 |
|
40283 | 757 |
|
758 |
(* theory setup *) |
|
759 |
||
760 |
val setup = |
|
761 |
Context.theory_map add_term_check #> |
|
40284
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
762 |
Attrib.setup @{binding coercion} |
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
763 |
(Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t)))) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
764 |
"declaration of new coercions" #> |
40297 | 765 |
Attrib.setup @{binding coercion_map} |
40284
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
766 |
(Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t)))) |
40283 | 767 |
"declaration of new map functions"; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
768 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
769 |
end; |