author | wenzelm |
Wed, 08 Jun 2011 15:56:57 +0200 | |
changeset 43278 | 1fbdcebb364b |
parent 42616 | 92715b528e78 |
child 43591 | d4cbd6feffdf |
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 |
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset
|
9 |
val coercion_enabled: bool Config.T |
40284
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
10 |
val add_type_map: term -> Context.generic -> Context.generic |
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
11 |
val add_coercion: term -> Context.generic -> Context.generic |
40283 | 12 |
val setup: theory -> theory |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
13 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
14 |
|
40283 | 15 |
structure Subtyping: SUBTYPING = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
16 |
struct |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
17 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
18 |
(** coercions data **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
19 |
|
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
20 |
datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (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 data = Data of |
40282 | 23 |
{coes: term Symreltab.table, (*coercions table*) |
24 |
coes_graph: unit Graph.T, (*coercions graph*) |
|
25 |
tmaps: (term * variance list) Symtab.table}; (*map functions*) |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
26 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
27 |
fun make_data (coes, coes_graph, tmaps) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
28 |
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
|
29 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
30 |
structure Data = Generic_Data |
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 |
type T = data; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
33 |
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
|
34 |
val extend = I; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
35 |
fun merge |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
36 |
(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
|
37 |
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
|
38 |
make_data (Symreltab.merge (op aconv) (coes1, coes2), |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
39 |
Graph.merge (op =) (coes_graph1, coes_graph2), |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
40 |
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
|
41 |
); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
42 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
43 |
fun map_data f = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
44 |
Data.map (fn Data {coes, coes_graph, tmaps} => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
45 |
make_data (f (coes, coes_graph, tmaps))); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
46 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
47 |
fun map_coes f = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
48 |
map_data (fn (coes, coes_graph, tmaps) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
49 |
(f coes, coes_graph, tmaps)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
50 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
51 |
fun map_coes_graph f = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
52 |
map_data (fn (coes, coes_graph, tmaps) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
53 |
(coes, f coes_graph, tmaps)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
54 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
55 |
fun map_coes_and_graph f = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
56 |
map_data (fn (coes, coes_graph, tmaps) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
57 |
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
|
58 |
in (coes', coes_graph', tmaps) end); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
59 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
60 |
fun map_tmaps f = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
61 |
map_data (fn (coes, coes_graph, tmaps) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
62 |
(coes, coes_graph, f tmaps)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
63 |
|
40285 | 64 |
val rep_data = (fn Data args => args) o Data.get o Context.Proof; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
65 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
66 |
val coes_of = #coes o rep_data; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
67 |
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
|
68 |
val tmaps_of = #tmaps o rep_data; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
69 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
70 |
|
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 |
(** utils **) |
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 |
fun nameT (Type (s, [])) = s; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
75 |
fun t_of s = Type (s, []); |
40286 | 76 |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
77 |
fun sort_of (TFree (_, S)) = SOME S |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
78 |
| sort_of (TVar (_, S)) = SOME S |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
79 |
| sort_of _ = NONE; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
80 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
81 |
val is_typeT = fn (Type _) => true | _ => false; |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
82 |
val is_stypeT = fn (Type (_, [])) => true | _ => false; |
40282 | 83 |
val is_compT = fn (Type (_, _ :: _)) => true | _ => false; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
84 |
val is_freeT = fn (TFree _) => true | _ => false; |
40286 | 85 |
val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false; |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
86 |
val is_funtype = fn (Type ("fun", [_, _])) => true | _ => false; |
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 |
|
40836 | 89 |
(* unification *) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
90 |
|
40836 | 91 |
exception TYPE_INFERENCE_ERROR of unit -> string; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
92 |
exception NO_UNIFIER of string * typ Vartab.table; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
93 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
94 |
fun unify weak ctxt = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
95 |
let |
42361 | 96 |
val thy = Proof_Context.theory_of ctxt; |
42386 | 97 |
val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy); |
40281
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 |
|
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
188 |
fun gen_msg err msg = |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
189 |
err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^ |
40836 | 190 |
(if msg = "" then "" else ": " ^ msg) ^ "\n"; |
191 |
||
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
192 |
fun prep_output ctxt tye bs ts Ts = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
193 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
194 |
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
|
195 |
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
196 |
fun prep t = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
197 |
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) |
42284 | 198 |
in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
199 |
in (map prep ts', Ts') end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
200 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
201 |
fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
202 |
|
40836 | 203 |
fun unif_failed msg = |
204 |
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n"; |
|
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
205 |
|
40836 | 206 |
fun err_appl_msg ctxt msg tye bs t T u U () = |
207 |
let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U] |
|
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
208 |
in unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n" end; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
209 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
210 |
fun err_list ctxt msg tye Ts = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
211 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
212 |
val (_, Ts') = prep_output ctxt tye [] [] Ts; |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
213 |
val text = |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
214 |
msg ^ "\n" ^ "Cannot unify a list of types that should be the same:" ^ "\n" ^ |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
215 |
Pretty.string_of (Pretty.list "[" "]" (map (Syntax.pretty_typ ctxt) Ts')); |
40281
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 (ts, Ts) = fold |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
223 |
(fn (bs, t $ u, U, _, U') => fn (ts, Ts) => |
40836 | 224 |
let val (t', T') = prep_output ctxt tye bs [t, u] [U', U] |
40282 | 225 |
in (t' :: ts, T' :: Ts) end) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
226 |
packs ([], []); |
40836 | 227 |
val text = cat_lines ([msg, "Cannot fulfil subtype constraints:"] @ |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
228 |
(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
|
229 |
Pretty.block [ |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
230 |
Syntax.pretty_typ ctxt T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
231 |
Syntax.pretty_typ ctxt U, Pretty.brk 3, |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
232 |
Pretty.str "from function application", Pretty.brk 2, |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
233 |
Pretty.block [Syntax.pretty_term ctxt (t $ u)]])) |
40281
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 |
|
40836 | 243 |
fun generate_constraints ctxt err = |
40281
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 = |
43278 | 249 |
(snd (nth bs i handle General.Subscript => err_loose i), tye_idx, cs) |
40281
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) |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
260 |
handle NO_UNIFIER (msg, _) => error (gen_msg err msg); |
40281
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 |
|
40836 | 273 |
fun process_constraints ctxt err cs tye_idx = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
274 |
let |
42388 | 275 |
val thy = Proof_Context.theory_of ctxt; |
276 |
||
40285 | 277 |
val coes_graph = coes_graph_of ctxt; |
278 |
val tmaps = tmaps_of ctxt; |
|
42388 | 279 |
val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
280 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
281 |
fun split_cs _ [] = ([], []) |
40282 | 282 |
| split_cs f (c :: cs) = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
283 |
(case pairself f (fst c) of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
284 |
(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
|
285 |
| _ => apfst (cons c) (split_cs f cs)); |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
286 |
|
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
287 |
fun unify_list (T :: Ts) tye_idx = |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
288 |
fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
289 |
|
40282 | 290 |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
291 |
(* check whether constraint simplification will terminate using weak unification *) |
40282 | 292 |
|
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
293 |
val _ = fold (fn (TU, _) => fn tye_idx => |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
294 |
weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, _) => |
40836 | 295 |
error (gen_msg err ("weak unification of subtype constraints fails\n" ^ msg))) cs tye_idx; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (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 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
298 |
(* simplify constraints *) |
40282 | 299 |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
300 |
fun simplify_constraints cs tye_idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
301 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
302 |
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
|
303 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
304 |
val arg_var = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
305 |
(case Symtab.lookup tmaps a of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
306 |
(*everything is invariant for unknown constructors*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
307 |
NONE => replicate (length Ts) INVARIANT |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
308 |
| SOME av => snd av); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
309 |
fun new_constraints (variance, constraint) (cs, tye_idx) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
310 |
(case variance of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
311 |
COVARIANT => (constraint :: cs, tye_idx) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
312 |
| CONTRAVARIANT => (swap constraint :: cs, tye_idx) |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
313 |
| INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
314 |
handle NO_UNIFIER (msg, _) => |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
315 |
err_list ctxt (gen_msg err |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
316 |
"failed to unify invariant arguments w.r.t. to the known map function") |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
317 |
(fst tye_idx) Ts) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
318 |
| INVARIANT => (cs, strong_unify ctxt constraint tye_idx |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
319 |
handle NO_UNIFIER (msg, _) => |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
320 |
error (gen_msg err ("failed to unify invariant arguments" ^ msg)))); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
321 |
val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack)) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
322 |
(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
|
323 |
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
|
324 |
val (ch, done') = |
40286 | 325 |
if not (null new) then ([], done) |
326 |
else split_cs (test_update o Type_Infer.deref tye') done; |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
327 |
val todo' = ch @ todo; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
328 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
329 |
simplify done' (new @ todo') (tye', idx') |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
330 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
331 |
(*xi is definitely a parameter*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
332 |
and expand varleq xi S a Ts error_pack done todo tye idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
333 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
334 |
val n = length Ts; |
40286 | 335 |
val args = map2 Type_Infer.mk_param (idx upto idx + n - 1) (arity_sorts a S); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
336 |
val tye' = Vartab.update_new (xi, Type(a, args)) tye; |
40286 | 337 |
val (ch, done') = split_cs (is_compT o Type_Infer.deref tye') done; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
338 |
val todo' = ch @ todo; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
339 |
val new = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
340 |
if varleq then (Type(a, args), Type (a, Ts)) |
40286 | 341 |
else (Type (a, Ts), Type (a, args)); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
342 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
343 |
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
|
344 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
345 |
(*TU is a pair of a parameter and a free/fixed variable*) |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
346 |
and eliminate TU done todo tye idx = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
347 |
let |
40286 | 348 |
val [TVar (xi, S)] = filter Type_Infer.is_paramT TU; |
349 |
val [T] = filter_out Type_Infer.is_paramT TU; |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
350 |
val SOME S' = sort_of T; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
351 |
val test_update = if is_freeT T then is_freeT else is_fixedvarT; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
352 |
val tye' = Vartab.update_new (xi, T) tye; |
40286 | 353 |
val (ch, done') = split_cs (test_update o Type_Infer.deref tye') done; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
354 |
val todo' = ch @ todo; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
355 |
in |
42388 | 356 |
if Sign.subsort thy (S', S) (*TODO check this*) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
357 |
then simplify done' todo' (tye', idx) |
40836 | 358 |
else error (gen_msg err "sort mismatch") |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
359 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
360 |
and simplify done [] tye_idx = (done, tye_idx) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
361 |
| simplify done (((T, U), error_pack) :: todo) (tye_idx as (tye, idx)) = |
40286 | 362 |
(case (Type_Infer.deref tye T, Type_Infer.deref tye U) of |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
363 |
(Type (a, []), Type (b, [])) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
364 |
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
|
365 |
else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx |
40836 | 366 |
else error (gen_msg err (a ^ " is not a subtype of " ^ b)) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
367 |
| (Type (a, Ts), Type (b, Us)) => |
40836 | 368 |
if a <> b then error (gen_msg err "different constructors") |
369 |
(fst tye_idx) error_pack |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
370 |
else contract a Ts Us error_pack done todo tye idx |
40282 | 371 |
| (TVar (xi, S), Type (a, Ts as (_ :: _))) => |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
372 |
expand true xi S a Ts error_pack done todo tye idx |
40282 | 373 |
| (Type (a, Ts as (_ :: _)), TVar (xi, S)) => |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
374 |
expand false xi S a Ts error_pack done todo tye idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
375 |
| (T, U) => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
376 |
if T = U then simplify done todo tye_idx |
40282 | 377 |
else if exists (is_freeT orf is_fixedvarT) [T, U] andalso |
40286 | 378 |
exists Type_Infer.is_paramT [T, U] |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
379 |
then eliminate [T, U] done todo tye idx |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
380 |
else if exists (is_freeT orf is_fixedvarT) [T, U] |
40836 | 381 |
then error (gen_msg err "not eliminated free/fixed variables") |
40282 | 382 |
else simplify (((T, U), error_pack) :: done) todo tye_idx); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
383 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
384 |
simplify [] cs tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
385 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
386 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
387 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
388 |
(* do simplification *) |
40282 | 389 |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
390 |
val (cs', tye_idx') = simplify_constraints cs tye_idx; |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
391 |
|
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
392 |
fun find_error_pack lower T' = map_filter |
40836 | 393 |
(fn ((T, U), pack) => if if lower then T' = U else T' = T then SOME pack else NONE) cs'; |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
394 |
|
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
395 |
fun find_cycle_packs nodes = |
40836 | 396 |
let |
397 |
val (but_last, last) = split_last nodes |
|
398 |
val pairs = (last, hd nodes) :: (but_last ~~ tl nodes); |
|
399 |
in |
|
400 |
map_filter |
|
40838 | 401 |
(fn (TU, pack) => if member (op =) pairs TU then SOME pack else NONE) |
40836 | 402 |
cs' |
403 |
end; |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
404 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
405 |
(*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
|
406 |
in terms of the subtype-relation (excluding T itself)*) |
40282 | 407 |
fun styps super T = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
408 |
(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
|
409 |
handle Graph.UNDEF _ => []; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
410 |
|
40282 | 411 |
fun minmax sup (T :: Ts) = |
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 sup then (T, U) else (U, T); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
414 |
fun extract T [] = T |
40282 | 415 |
| extract T (U :: Us) = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
416 |
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
|
417 |
else if Graph.is_edge coes_graph (adjust U T) then extract U Us |
40836 | 418 |
else raise BOUND_ERROR "uncomparable types in type list"; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
419 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
420 |
t_of (extract T Ts) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
421 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
422 |
|
40282 | 423 |
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
|
424 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
425 |
fun adjust T U = if super then (T, U) else (U, T); |
40282 | 426 |
fun styp_test U Ts = forall |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
427 |
(fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts; |
42388 | 428 |
fun fitting Ts S U = Sign.of_sort thy (t_of U, S) andalso styp_test U Ts |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
429 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
430 |
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
|
431 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
432 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
433 |
(* 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
|
434 |
e.g. in the supremum case (sup = true): |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
435 |
------- 'a::S--- |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
436 |
/ / \ \ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
437 |
/ / \ \ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
438 |
'b::C1 'c::C2 ... T1 T2 ... |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
439 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
440 |
sorts - list of sorts [C1, C2, ...] |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
441 |
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
|
442 |
*) |
40282 | 443 |
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
|
444 |
let |
42388 | 445 |
fun restriction T = Sign.of_sort thy (t_of T, S) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
446 |
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
|
447 |
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
|
448 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
449 |
(case fold candidates Ts (filter restriction (T :: styps sup T)) of |
40836 | 450 |
[] => raise BOUND_ERROR ("no " ^ (if sup then "supremum" else "infimum")) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
451 |
| [T] => t_of T |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
452 |
| Ts => minmax sup Ts) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
453 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
454 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
455 |
fun build_graph G [] tye_idx = (G, tye_idx) |
40282 | 456 |
| 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
|
457 |
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
|
458 |
else |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
459 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
460 |
val G' = maybe_new_typnodes [T, U] G; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
461 |
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
|
462 |
handle Typ_Graph.CYCLES cycles => |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
463 |
let |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
464 |
val (tye, idx) = |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
465 |
fold |
40836 | 466 |
(fn cycle => fn tye_idx' => (unify_list cycle tye_idx' |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
467 |
handle NO_UNIFIER (msg, _) => |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
468 |
err_bound ctxt |
40836 | 469 |
(gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx) |
470 |
(find_cycle_packs cycle))) |
|
471 |
cycles tye_idx |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
472 |
in |
40836 | 473 |
collapse (tye, idx) cycles G |
474 |
end |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
475 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
476 |
build_graph G'' cs tye_idx' |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
477 |
end |
40836 | 478 |
and collapse (tye, idx) cycles G = (*nodes non-empty list*) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
479 |
let |
40836 | 480 |
(*all cycles collapse to one node, |
481 |
because all of them share at least the nodes x and y*) |
|
482 |
val nodes = (distinct (op =) (flat cycles)); |
|
483 |
val T = Type_Infer.deref tye (hd nodes); |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
484 |
val P = new_imm_preds G nodes; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
485 |
val S = new_imm_succs G nodes; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
486 |
val G' = Typ_Graph.del_nodes (tl nodes) G; |
40836 | 487 |
fun check_and_gen super T' = |
488 |
let val U = Type_Infer.deref tye T'; |
|
489 |
in |
|
490 |
if not (is_typeT T) orelse not (is_typeT U) orelse T = U |
|
491 |
then if super then (hd nodes, T') else (T', hd nodes) |
|
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
492 |
else |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
493 |
if super andalso |
40836 | 494 |
Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T') |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
495 |
else if not super andalso |
40836 | 496 |
Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes) |
497 |
else err_bound ctxt (gen_msg err "cycle elimination produces inconsistent graph") |
|
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
498 |
(fst tye_idx) |
40836 | 499 |
(maps find_cycle_packs cycles @ find_error_pack super T') |
500 |
end; |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
501 |
in |
40836 | 502 |
build_graph G' (map (check_and_gen false) P @ map (check_and_gen true) S) (tye, idx) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
503 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
504 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
505 |
fun assign_bound lower G key (tye_idx as (tye, _)) = |
40286 | 506 |
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
|
507 |
let |
40286 | 508 |
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
|
509 |
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
|
510 |
val raw_bound = get_bound G key; |
40286 | 511 |
val bound = map (Type_Infer.deref tye) raw_bound; |
512 |
val not_params = filter_out Type_Infer.is_paramT bound; |
|
40282 | 513 |
fun to_fulfil T = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
514 |
(case sort_of T of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
515 |
NONE => NONE |
40282 | 516 |
| SOME S => |
40286 | 517 |
SOME |
518 |
(map nameT |
|
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42402
diff
changeset
|
519 |
(filter_out Type_Infer.is_paramT |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42402
diff
changeset
|
520 |
(map (Type_Infer.deref tye) (get_bound G T))), S)); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
521 |
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
|
522 |
val assignment = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
523 |
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
|
524 |
else SOME (tightest lower S styps_and_sorts (map nameT not_params) |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
525 |
handle BOUND_ERROR msg => |
40836 | 526 |
err_bound ctxt (gen_msg err msg) tye (find_error_pack lower key)) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
527 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
528 |
(case assignment of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
529 |
NONE => tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
530 |
| SOME T => |
40286 | 531 |
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
|
532 |
else if lower then (*upper bound check*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
533 |
let |
40286 | 534 |
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
|
535 |
val s = nameT T; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
536 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
537 |
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
|
538 |
then apfst (Vartab.update (xi, T)) tye_idx |
40836 | 539 |
else err_bound ctxt (gen_msg err ("assigned simple type " ^ s ^ |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
540 |
" clashes with the upper bound of variable " ^ |
40836 | 541 |
Syntax.string_of_typ ctxt (TVar(xi, S)))) tye (find_error_pack (not lower) key) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
542 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
543 |
else apfst (Vartab.update (xi, T)) tye_idx) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
544 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
545 |
else tye_idx; |
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 |
val assign_lb = assign_bound true; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
548 |
val assign_ub = assign_bound false; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
549 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
550 |
fun assign_alternating ts' ts G tye_idx = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
551 |
if ts' = ts then tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
552 |
else |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
553 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
554 |
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
|
555 |
|> fold (assign_ub G) ts; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
556 |
in |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
557 |
assign_alternating ts |
40836 | 558 |
(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
|
559 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
560 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
561 |
(*Unify all weakly connected components of the constraint forest, |
40282 | 562 |
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
|
563 |
params anyway.*) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
564 |
fun unify_params G (tye_idx as (tye, _)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
565 |
let |
40286 | 566 |
val max_params = |
567 |
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
|
568 |
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
|
569 |
in |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
570 |
fold |
40836 | 571 |
(fn Ts => fn tye_idx' => unify_list Ts tye_idx' |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
572 |
handle NO_UNIFIER (msg, _) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts) |
40836 | 573 |
to_unify tye_idx |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
574 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
575 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
576 |
fun solve_constraints G tye_idx = tye_idx |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
577 |
|> assign_alternating [] (Typ_Graph.keys G) G |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
578 |
|> unify_params G; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
579 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
580 |
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
|
581 |
|-> solve_constraints |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
582 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
583 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
584 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
585 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
586 |
(** coercion insertion **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
587 |
|
40836 | 588 |
fun gen_coercion ctxt tye (T1, T2) = |
589 |
(case pairself (Type_Infer.deref tye) (T1, T2) of |
|
590 |
((Type (a, [])), (Type (b, []))) => |
|
591 |
if a = b |
|
592 |
then Abs (Name.uu, Type (a, []), Bound 0) |
|
593 |
else |
|
594 |
(case Symreltab.lookup (coes_of ctxt) (a, b) of |
|
595 |
NONE => raise Fail (a ^ " is not a subtype of " ^ b) |
|
596 |
| SOME co => co) |
|
597 |
| ((Type (a, Ts)), (Type (b, Us))) => |
|
598 |
if a <> b |
|
599 |
then raise Fail ("Different constructors: " ^ a ^ " and " ^ b) |
|
600 |
else |
|
601 |
let |
|
602 |
fun inst t Ts = |
|
603 |
Term.subst_vars |
|
604 |
(((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t; |
|
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
605 |
fun sub_co (COVARIANT, TU) = SOME (gen_coercion ctxt tye TU) |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
606 |
| sub_co (CONTRAVARIANT, TU) = SOME (gen_coercion ctxt tye (swap TU)) |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
607 |
| sub_co (INVARIANT_TO T, _) = NONE; |
40836 | 608 |
fun ts_of [] = [] |
609 |
| ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs); |
|
610 |
in |
|
611 |
(case Symtab.lookup (tmaps_of ctxt) a of |
|
612 |
NONE => raise Fail ("No map function for " ^ a ^ " known") |
|
613 |
| SOME tmap => |
|
614 |
let |
|
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
615 |
val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us)); |
40836 | 616 |
in |
617 |
Term.list_comb |
|
618 |
(inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes) |
|
619 |
end) |
|
620 |
end |
|
621 |
| (T, U) => |
|
622 |
if Type.could_unify (T, U) |
|
623 |
then Abs (Name.uu, T, Bound 0) |
|
624 |
else raise Fail ("Cannot generate coercion from " |
|
625 |
^ Syntax.string_of_typ ctxt T ^ " to " ^ Syntax.string_of_typ ctxt U)); |
|
626 |
||
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
627 |
fun insert_coercions ctxt tye ts = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
628 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
629 |
fun insert _ (Const (c, T)) = |
40836 | 630 |
let val T' = T; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
631 |
in (Const (c, T'), T') end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
632 |
| insert _ (Free (x, T)) = |
40836 | 633 |
let val T' = T; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
634 |
in (Free (x, T'), T') end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
635 |
| insert _ (Var (xi, T)) = |
40836 | 636 |
let val T' = T; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
637 |
in (Var (xi, T'), T') end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
638 |
| insert bs (Bound i) = |
43278 | 639 |
let val T = nth bs i handle General.Subscript => err_loose i; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
640 |
in (Bound i, T) end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
641 |
| insert bs (Abs (x, T, t)) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
642 |
let |
40836 | 643 |
val T' = T; |
40282 | 644 |
val (t', T'') = insert (T' :: bs) t; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
645 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
646 |
(Abs (x, T', t'), T' --> T'') |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
647 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
648 |
| insert bs (t $ u) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
649 |
let |
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42402
diff
changeset
|
650 |
val (t', Type ("fun", [U, T])) = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42402
diff
changeset
|
651 |
apsnd (Type_Infer.deref tye) (insert bs t); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
652 |
val (u', U') = insert bs u; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
653 |
in |
40836 | 654 |
if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U') |
655 |
then (t' $ u', T) |
|
656 |
else (t' $ (gen_coercion ctxt tye (U', U) $ u'), T) |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
657 |
end |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
658 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
659 |
map (fst o insert []) ts |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
660 |
end; |
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 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
663 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
664 |
(** assembling the pipeline **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
665 |
|
42398 | 666 |
fun coercion_infer_types ctxt raw_ts = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
667 |
let |
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42402
diff
changeset
|
668 |
val (idx, ts) = Type_Infer_Context.prepare ctxt raw_ts; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
669 |
|
40836 | 670 |
fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx) |
671 |
| inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx) |
|
672 |
| inf _ (t as (Var (_, T))) tye_idx = (t, T, tye_idx) |
|
673 |
| inf bs (t as (Bound i)) tye_idx = |
|
43278 | 674 |
(t, snd (nth bs i handle General.Subscript => err_loose i), tye_idx) |
40836 | 675 |
| inf bs (Abs (x, T, t)) tye_idx = |
676 |
let val (t', U, tye_idx') = inf ((x, T) :: bs) t tye_idx |
|
677 |
in (Abs (x, T, t'), T --> U, tye_idx') end |
|
678 |
| inf bs (t $ u) tye_idx = |
|
679 |
let |
|
680 |
val (t', T, tye_idx') = inf bs t tye_idx; |
|
681 |
val (u', U, (tye, idx)) = inf bs u tye_idx'; |
|
682 |
val V = Type_Infer.mk_param idx []; |
|
683 |
val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U --> V, T) (tye, idx + 1)) |
|
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
684 |
handle NO_UNIFIER (msg, tye') => |
40836 | 685 |
raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U); |
686 |
in (tu, V, tye_idx'') end; |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
687 |
|
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
688 |
fun infer_single t tye_idx = |
40836 | 689 |
let val (t, _, tye_idx') = inf [] t tye_idx; |
40938
e258f6817add
use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
traytel
parents:
40840
diff
changeset
|
690 |
in (t, tye_idx') end; |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
691 |
|
40938
e258f6817add
use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
traytel
parents:
40840
diff
changeset
|
692 |
val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx) |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
693 |
handle TYPE_INFERENCE_ERROR err => |
40836 | 694 |
let |
695 |
fun gen_single t (tye_idx, constraints) = |
|
696 |
let val (_, tye_idx', constraints') = generate_constraints ctxt err t tye_idx |
|
697 |
in (tye_idx', constraints' @ constraints) end; |
|
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
698 |
|
40836 | 699 |
val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []); |
700 |
val (tye, idx) = process_constraints ctxt err constraints tye_idx; |
|
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
701 |
in |
40836 | 702 |
(insert_coercions ctxt tye ts, (tye, idx)) |
703 |
end); |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
704 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
705 |
val (_, ts'') = Type_Infer.finish ctxt tye ([], ts'); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
706 |
in ts'' end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
707 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
708 |
|
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 |
(** installation **) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
711 |
|
40283 | 712 |
(* term check *) |
713 |
||
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42405
diff
changeset
|
714 |
val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false); |
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40938
diff
changeset
|
715 |
|
40283 | 716 |
val add_term_check = |
717 |
Syntax.add_term_check ~100 "coercions" |
|
42402
c7139609b67d
simplified check/uncheck interfaces: result comparison is hardwired by default;
wenzelm
parents:
42398
diff
changeset
|
718 |
(fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
719 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
720 |
|
40283 | 721 |
(* declarations *) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
722 |
|
40284
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
723 |
fun add_type_map raw_t context = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
724 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
725 |
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
|
726 |
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
|
727 |
|
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
728 |
fun err_str t = "\n\nThe provided function has the type\n" ^ |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
729 |
Syntax.string_of_typ ctxt (fastype_of t) ^ |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
730 |
"\n\nThe general type signature of a map function is" ^ |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
731 |
"\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^ |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
732 |
"\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)"; |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
733 |
|
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
734 |
val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t)) |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
735 |
handle Empty => error ("Not a proper map function:" ^ err_str t); |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
736 |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
737 |
fun gen_arg_var ([], []) = [] |
40282 | 738 |
| gen_arg_var ((T, T') :: Ts, (U, U') :: Us) = |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
739 |
if U = U' then |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
740 |
if is_stypeT U then INVARIANT_TO U :: gen_arg_var ((T, T') :: Ts, Us) |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
741 |
else error ("Invariant xi and yi should be base types:" ^ err_str t) |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
742 |
else if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us) |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
743 |
else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us) |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
744 |
else error ("Functions do not apply to arguments correctly:" ^ err_str t) |
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
745 |
| gen_arg_var (_, Ts) = |
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42361
diff
changeset
|
746 |
if forall (op = andf is_stypeT o fst) Ts |
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
747 |
then map (INVARIANT_TO o fst) Ts |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
748 |
else error ("Different numbers of functions and variant arguments\n" ^ err_str t); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
749 |
|
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
750 |
(*retry flag needed to adjust the type lists, when given a map over type constructor fun*) |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
751 |
fun check_map_fun fis (Type (C1, Ts)) (Type (C2, Us)) retry = |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
752 |
if C1 = C2 andalso not (null fis) andalso forall is_funtype fis |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
753 |
then ((map dest_funT fis, Ts ~~ Us), C1) |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
754 |
else error ("Not a proper map function:" ^ err_str t) |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
755 |
| check_map_fun fis T1 T2 true = |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
756 |
let val (fis', T') = split_last fis |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
757 |
in check_map_fun fis' T' (T1 --> T2) false end |
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
758 |
| check_map_fun _ _ _ _ = error ("Not a proper map function:" ^ err_str t); |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
759 |
|
41353
684003dbda54
Enabled non fully polymorphic map functions in subtyping
traytel
parents:
40939
diff
changeset
|
760 |
val res = check_map_fun fis T1 T2 true; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
761 |
val res_av = gen_arg_var (fst res); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
762 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
763 |
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
|
764 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
765 |
|
40284
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
766 |
fun add_coercion raw_t context = |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
767 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
768 |
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
|
769 |
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
|
770 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
771 |
fun err_coercion () = error ("Bad type for coercion " ^ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
772 |
Syntax.string_of_term ctxt t ^ ":\n" ^ |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
773 |
Syntax.string_of_typ ctxt (fastype_of t)); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
774 |
|
40840 | 775 |
val (T1, T2) = Term.dest_funT (fastype_of t) |
776 |
handle TYPE _ => err_coercion (); |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
777 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
778 |
val a = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
779 |
(case T1 of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
780 |
Type (x, []) => x |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
781 |
| _ => err_coercion ()); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
782 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
783 |
val b = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
784 |
(case T2 of |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
785 |
Type (x, []) => x |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
786 |
| _ => err_coercion ()); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
787 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
788 |
fun coercion_data_update (tab, G) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
789 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
790 |
val G' = maybe_new_nodes [a, b] G |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
791 |
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
|
792 |
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
|
793 |
"!\n\nCannot add coercion of type: " ^ a ^ " => " ^ b); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
794 |
val new_edges = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
795 |
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
|
796 |
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
|
797 |
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
|
798 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
799 |
fun complex_coercion tab G (a, b) = |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
800 |
let |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
801 |
val path = hd (Graph.irreducible_paths G (a, b)) |
40836 | 802 |
val path' = fst (split_last path) ~~ tl path |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
803 |
in Abs (Name.uu, Type (a, []), |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
804 |
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
|
805 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
806 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
807 |
val tab' = fold |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
808 |
(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
|
809 |
(filter (fn pair => pair <> (a, b)) new_edges) |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
810 |
(Symreltab.update ((a, b), t) tab); |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
811 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
812 |
(tab', G'') |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
813 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
814 |
in |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
815 |
map_coes_and_graph coercion_data_update context |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
816 |
end; |
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
817 |
|
40283 | 818 |
|
819 |
(* theory setup *) |
|
820 |
||
821 |
val setup = |
|
822 |
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
|
823 |
Attrib.setup @{binding coercion} |
c9acf88447e6
export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents:
40283
diff
changeset
|
824 |
(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
|
825 |
"declaration of new coercions" #> |
40297 | 826 |
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
|
827 |
(Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t)))) |
40283 | 828 |
"declaration of new map functions"; |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
829 |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff
changeset
|
830 |
end; |