src/Tools/subtyping.ML
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 53539 51157ee7f5ba
child 54470 0a7341e3948c
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
    12
  val print_coercions: Proof.context -> unit
40283
805ce1d64af0 proper signature constraint for ML structure;
wenzelm
parents: 40282
diff changeset
    13
  val setup: theory -> theory
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    14
end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    15
40283
805ce1d64af0 proper signature constraint for ML structure;
wenzelm
parents: 40282
diff changeset
    16
structure Subtyping: SUBTYPING =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    17
struct
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    18
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    19
(** coercions data **)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    20
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
    21
datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ;
51327
62c033d7f3d8 tuned (extend datatype to inline option)
traytel
parents: 51319
diff changeset
    22
datatype coerce_arg = PERMIT | FORBID | LEAVE
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    23
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    24
datatype data = Data of
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
    25
  {coes: (term * ((typ list * typ list) * term list)) Symreltab.table,  (*coercions table*)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
    26
   (*full coercions graph - only used at coercion declaration/deletion*)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
    27
   full_graph: int Graph.T,
52432
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
    28
   (*coercions graph restricted to base types - for efficiency reasons stored in the context*)
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
    29
   coes_graph: int Graph.T,
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    30
   tmaps: (term * variance list) Symtab.table,  (*map functions*)
51327
62c033d7f3d8 tuned (extend datatype to inline option)
traytel
parents: 51319
diff changeset
    31
   coerce_args: coerce_arg list Symtab.table  (*special constants with non-coercible arguments*)};
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    32
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    33
fun make_data (coes, full_graph, coes_graph, tmaps, coerce_args) =
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    34
  Data {coes = coes, full_graph = full_graph, coes_graph = coes_graph,
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    35
    tmaps = tmaps, coerce_args = coerce_args};
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    36
45935
32f769f94ea4 meaningful error message on failing merges of coercion tables
traytel
parents: 45429
diff changeset
    37
fun merge_error_coes (a, b) =
32f769f94ea4 meaningful error message on failing merges of coercion tables
traytel
parents: 45429
diff changeset
    38
  error ("Cannot merge coercion tables.\nConflicting declarations for coercions from " ^
32f769f94ea4 meaningful error message on failing merges of coercion tables
traytel
parents: 45429
diff changeset
    39
    quote a ^ " to " ^ quote b ^ ".");
32f769f94ea4 meaningful error message on failing merges of coercion tables
traytel
parents: 45429
diff changeset
    40
32f769f94ea4 meaningful error message on failing merges of coercion tables
traytel
parents: 45429
diff changeset
    41
fun merge_error_tmaps C =
32f769f94ea4 meaningful error message on failing merges of coercion tables
traytel
parents: 45429
diff changeset
    42
  error ("Cannot merge coercion map tables.\nConflicting declarations for the constructor " ^
32f769f94ea4 meaningful error message on failing merges of coercion tables
traytel
parents: 45429
diff changeset
    43
    quote C ^ ".");
32f769f94ea4 meaningful error message on failing merges of coercion tables
traytel
parents: 45429
diff changeset
    44
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    45
fun merge_error_coerce_args C =
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    46
  error ("Cannot merge tables for constants with coercion-invariant arguments.\n"
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    47
    ^ "Conflicting declarations for the constant " ^ quote C ^ ".");
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    48
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    49
structure Data = Generic_Data
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
  type T = data;
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    52
  val empty = make_data (Symreltab.empty, Graph.empty, Graph.empty, Symtab.empty, Symtab.empty);
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    53
  val extend = I;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    54
  fun merge
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    55
    (Data {coes = coes1, full_graph = full_graph1, coes_graph = coes_graph1,
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    56
      tmaps = tmaps1, coerce_args = coerce_args1},
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    57
      Data {coes = coes2, full_graph = full_graph2, coes_graph = coes_graph2,
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    58
        tmaps = tmaps2, coerce_args = coerce_args2}) =
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
    59
    make_data (Symreltab.merge (eq_pair (op aconv)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
    60
        (eq_pair (eq_pair (eq_list (op =)) (eq_list (op =))) (eq_list (op aconv))))
45935
32f769f94ea4 meaningful error message on failing merges of coercion tables
traytel
parents: 45429
diff changeset
    61
        (coes1, coes2) handle Symreltab.DUP key => merge_error_coes key,
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
    62
      Graph.merge (op =) (full_graph1, full_graph2),
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    63
      Graph.merge (op =) (coes_graph1, coes_graph2),
45935
32f769f94ea4 meaningful error message on failing merges of coercion tables
traytel
parents: 45429
diff changeset
    64
      Symtab.merge (eq_pair (op aconv) (op =)) (tmaps1, tmaps2)
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    65
        handle Symtab.DUP key => merge_error_tmaps key,
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    66
      Symtab.merge (eq_list (op =)) (coerce_args1, coerce_args2)
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    67
        handle Symtab.DUP key => merge_error_coerce_args key);
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    68
);
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
fun map_data f =
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    71
  Data.map (fn Data {coes, full_graph, coes_graph, tmaps, coerce_args} =>
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    72
    make_data (f (coes, full_graph, coes_graph, tmaps, coerce_args)));
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (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 map_coes f =
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    75
  map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    76
    (f coes, full_graph, coes_graph, tmaps, coerce_args));
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    77
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    78
fun map_coes_graph f =
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    79
  map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    80
    (coes, full_graph, f coes_graph, tmaps, coerce_args));
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    81
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
    82
fun map_coes_and_graphs f =
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    83
  map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
    84
    let val (coes', full_graph', coes_graph') = f (coes, full_graph, coes_graph);
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    85
    in (coes', full_graph', coes_graph', tmaps, coerce_args) end);
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    86
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    87
fun map_tmaps f =
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    88
  map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    89
    (coes, full_graph, coes_graph, f tmaps, coerce_args));
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    90
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    91
fun map_coerce_args f =
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    92
  map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
    93
    (coes, full_graph, coes_graph, tmaps, f coerce_args));
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    94
40285
80136c4240cc simplified data lookup;
wenzelm
parents: 40284
diff changeset
    95
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
    96
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    97
val coes_of = #coes o rep_data;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    98
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
    99
val tmaps_of = #tmaps o rep_data;
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   100
val coerce_args_of = #coerce_args o rep_data;
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (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
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   103
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   104
(** utils **)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   105
46614
165886a4fe64 clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents: 45935
diff changeset
   106
fun restrict_graph G = Graph.restrict (fn x => Graph.get_node G x = 0) G;
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   107
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   108
fun nameT (Type (s, [])) = s;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   109
fun t_of s = Type (s, []);
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   110
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   111
fun sort_of (TFree (_, S)) = SOME S
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   112
  | sort_of (TVar (_, S)) = SOME S
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   113
  | sort_of _ = NONE;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   114
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   115
val is_typeT = fn (Type _) => true | _ => false;
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   116
val is_stypeT = fn (Type (_, [])) => true | _ => false;
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   117
val is_compT = fn (Type (_, _ :: _)) => true | _ => false;
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   118
val is_freeT = fn (TFree _) => true | _ => false;
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   119
val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false;
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   120
val is_funtype = fn (Type ("fun", [_, _])) => true | _ => false;
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   121
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   122
fun mk_identity T = Abs (Name.uu, T, Bound 0);
43591
d4cbd6feffdf collapse map functions with identity subcoercions to identities;
traytel
parents: 43278
diff changeset
   123
val is_identity = fn (Abs (_, _, Bound 0)) => true | _ => false;
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   124
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   125
fun instantiate t Ts = Term.subst_TVars
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   126
  ((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts) t;
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   127
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   128
exception COERCION_GEN_ERROR of unit -> string;
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   129
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   130
fun inst_collect tye err T U =
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   131
  (case (T, Type_Infer.deref tye U) of
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   132
    (TVar (xi, S), U) => [(xi, U)]
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   133
  | (Type (a, Ts), Type (b, Us)) =>
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   134
      if a <> b then raise error (err ()) else inst_collects tye err Ts Us
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   135
  | (_, U') => if T <> U' then error (err ()) else [])
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   136
and inst_collects tye err Ts Us =
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   137
  fold2 (fn T => fn U => fn is => inst_collect tye err T U @ is) Ts Us [];
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   138
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   139
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   140
(* unification *)
40281
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
exception NO_UNIFIER of string * typ Vartab.table;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   143
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   144
fun unify weak ctxt =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   145
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42284
diff changeset
   146
    val thy = Proof_Context.theory_of ctxt;
42386
wenzelm
parents: 42383
diff changeset
   147
    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
   148
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   149
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   150
    (* adjust sorts of parameters *)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   151
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   152
    fun not_of_sort x S' S =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   153
      "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
   154
        Syntax.string_of_sort ctxt S;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   155
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   156
    fun meet (_, []) tye_idx = tye_idx
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   157
      | 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
   158
          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
   159
      | 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
   160
          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
   161
          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
   162
      | 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
   163
          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
   164
          else if Type_Infer.is_param xi then
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   165
            (Vartab.update_new
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   166
              (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
   167
          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
   168
    and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   169
          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
   170
      | meets _ tye_idx = tye_idx;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   171
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   172
    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
   173
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   174
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   175
    (* occurs check and assignment *)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   176
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   177
    fun occurs_check tye xi (TVar (xi', _)) =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   178
          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
   179
          else
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   180
            (case Vartab.lookup tye xi' of
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   181
              NONE => ()
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   182
            | SOME T => occurs_check tye xi T)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   183
      | 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
   184
      | occurs_check _ _ _ = ();
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
    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
   187
          if xi = xi' then env
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   188
          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
   189
      | assign xi T S (env as (tye, _)) =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   190
          (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
   191
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   192
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   193
    (* unification *)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   194
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   195
    fun show_tycon (a, Ts) =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   196
      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
   197
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   198
    fun unif (T1, T2) (env as (tye, _)) =
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   199
      (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
   200
        ((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
   201
      | ((_, 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
   202
      | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   203
          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
   204
          else if a <> b then
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   205
            raise NO_UNIFIER
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   206
              ("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
   207
          else fold unif (Ts ~~ Us) env
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   208
      | ((_, 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
   209
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   210
  in unif end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   211
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   212
val weak_unify = unify true;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   213
val strong_unify = unify false;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   214
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   215
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   216
(* Typ_Graph shortcuts *)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   217
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   218
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
   219
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
   220
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
   221
fun maybe_new_typnodes Ts G = fold maybe_new_typnode Ts G;
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 43591
diff changeset
   222
fun new_imm_preds G Ts =  (* FIXME inefficient *)
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 43591
diff changeset
   223
  subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_preds G) Ts));
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 43591
diff changeset
   224
fun new_imm_succs G Ts =  (* FIXME inefficient *)
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 43591
diff changeset
   225
  subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_succs G) Ts));
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   226
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   227
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   228
(* Graph shortcuts *)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   229
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   230
fun maybe_new_node s G = perhaps (try (Graph.new_node s)) G
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   231
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
   232
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   233
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   234
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   235
(** error messages **)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   236
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   237
infixr ++> (* lazy error msg composition *)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   238
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   239
fun err ++> str = err #> suffix str
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   240
42383
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   241
fun gen_msg err msg =
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   242
  err () ^ "\nNow trying to infer coercions globally.\n\nCoercion inference failed" ^
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   243
  (if msg = "" then "" else ":\n" ^ msg) ^ "\n";
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   244
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   245
fun prep_output ctxt tye bs ts Ts =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   246
  let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   247
    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
   248
    val (Ts', Ts'') = chop (length Ts) Ts_bTs';
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   249
    fun prep t =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   250
      let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
49660
de49d9b4d7bc more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents: 49564
diff changeset
   251
      in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   252
  in (map prep ts', Ts') end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   253
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   254
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
   255
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   256
fun unif_failed msg =
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   257
  "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
   258
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   259
fun err_appl_msg ctxt msg tye bs t T u U () =
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   260
  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
   261
  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
   262
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   263
fun err_list ctxt msg tye Ts =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   264
  let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   265
    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
   266
    val text =
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   267
      msg ^ "\nCannot unify a list of types that should be the same:\n" ^
42383
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   268
        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
   269
  in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   270
    error text
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   271
  end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   272
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   273
fun err_bound ctxt msg tye packs =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   274
  let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   275
    val (ts, Ts) = fold
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   276
      (fn (bs, t $ u, U, _, U') => fn (ts, Ts) =>
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   277
        let val (t', T') = prep_output ctxt tye bs [t, u] [U', U]
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   278
        in (t' :: ts, T' :: Ts) end)
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   279
      packs ([], []);
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   280
    val text = msg ^ "\n" ^ Pretty.string_of (
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   281
        Pretty.big_list "Cannot fulfil subtype constraints:"
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   282
        (map2 (fn [t, u] => fn [T, U] =>
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   283
          Pretty.block [
42383
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   284
            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
   285
            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
   286
            Pretty.str "from function application", Pretty.brk 2,
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   287
            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
   288
        ts Ts))
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   289
  in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   290
    error text
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   291
  end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   292
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   293
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   294
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   295
(** constraint generation **)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   296
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   297
fun update_coerce_arg ctxt old t =
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   298
  let
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   299
    val mk_coerce_args = the_default [] o Symtab.lookup (coerce_args_of ctxt);
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   300
    fun update _ [] = old
51327
62c033d7f3d8 tuned (extend datatype to inline option)
traytel
parents: 51319
diff changeset
   301
      | update 0 (coerce :: _) = (case coerce of LEAVE => old | PERMIT => true | FORBID => false)
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   302
      | update n (_ :: cs) = update (n - 1) cs;
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   303
    val (f, n) = Term.strip_comb (Type.strip_constraints t) ||> length;
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   304
  in
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   305
    update n (case f of Const (name, _) => mk_coerce_args name | _ => [])
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   306
  end;
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   307
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   308
fun generate_constraints ctxt err =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   309
  let
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   310
    fun gen _ cs _ (Const (_, T)) tye_idx = (T, tye_idx, cs)
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   311
      | gen _ cs _ (Free (_, T)) tye_idx = (T, tye_idx, cs)
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   312
      | gen _ cs _ (Var (_, T)) tye_idx = (T, tye_idx, cs)
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   313
      | gen _ cs bs (Bound i) tye_idx =
43278
1fbdcebb364b more robust exception pattern General.Subscript;
wenzelm
parents: 42616
diff changeset
   314
          (snd (nth bs i handle General.Subscript => err_loose i), tye_idx, cs)
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   315
      | gen coerce cs bs (Abs (x, T, t)) tye_idx =
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   316
          let val (U, tye_idx', cs') = gen coerce cs ((x, T) :: bs) t tye_idx
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   317
          in (T --> U, tye_idx', cs') end
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   318
      | gen coerce cs bs (t $ u) tye_idx =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   319
          let
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   320
            val (T, tye_idx', cs') = gen coerce cs bs t tye_idx;
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   321
            val coerce' = update_coerce_arg ctxt coerce t;
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   322
            val (U', (tye, idx), cs'') = gen coerce' cs' bs u tye_idx';
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   323
            val U = Type_Infer.mk_param idx [];
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   324
            val V = Type_Infer.mk_param (idx + 1) [];
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   325
            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
   326
              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
   327
            val error_pack = (bs, t $ u, U, V, U');
52432
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
   328
          in
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   329
            if coerce'
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   330
            then (V, tye_idx'', ((U', U), error_pack) :: cs'')
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   331
            else (V,
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   332
              strong_unify ctxt (U, U') tye_idx''
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   333
                handle NO_UNIFIER (msg, _) => error (gen_msg err msg),
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   334
              cs'')
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   335
          end;
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   336
  in
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   337
    gen true [] []
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   338
  end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   339
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   340
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   341
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   342
(** constraint resolution **)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   343
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   344
exception BOUND_ERROR of string;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   345
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   346
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
   347
  let
42388
a44b0fdaa6c2 standardized aliases of operations on tsig;
wenzelm
parents: 42386
diff changeset
   348
    val thy = Proof_Context.theory_of ctxt;
a44b0fdaa6c2 standardized aliases of operations on tsig;
wenzelm
parents: 42386
diff changeset
   349
40285
80136c4240cc simplified data lookup;
wenzelm
parents: 40284
diff changeset
   350
    val coes_graph = coes_graph_of ctxt;
80136c4240cc simplified data lookup;
wenzelm
parents: 40284
diff changeset
   351
    val tmaps = tmaps_of ctxt;
42388
a44b0fdaa6c2 standardized aliases of operations on tsig;
wenzelm
parents: 42386
diff changeset
   352
    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
   353
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   354
    fun split_cs _ [] = ([], [])
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   355
      | split_cs f (c :: cs) =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   356
          (case pairself f (fst c) of
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   357
            (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
   358
          | _ => 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
   359
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   360
    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
   361
      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
   362
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   363
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   364
    (* check whether constraint simplification will terminate using weak unification *)
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   365
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   366
    val _ = fold (fn (TU, _) => fn tye_idx =>
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   367
      weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, _) =>
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   368
        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
   369
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   370
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   371
    (* simplify constraints *)
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   372
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   373
    fun simplify_constraints cs tye_idx =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   374
      let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   375
        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
   376
          let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   377
            val arg_var =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   378
              (case Symtab.lookup tmaps a of
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   379
                (*everything is invariant for unknown constructors*)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   380
                NONE => replicate (length Ts) INVARIANT
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   381
              | SOME av => snd av);
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   382
            fun new_constraints (variance, constraint) (cs, tye_idx) =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   383
              (case variance of
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   384
                COVARIANT => (constraint :: cs, tye_idx)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   385
              | CONTRAVARIANT => (swap constraint :: cs, tye_idx)
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   386
              | 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
   387
                  handle NO_UNIFIER (msg, _) =>
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   388
                    err_list ctxt (gen_msg err
51248
029de23bb5e8 tuned error messages
traytel
parents: 51246
diff changeset
   389
                      "failed to unify invariant arguments w.r.t. to the known map function\n" ^ msg)
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   390
                      (fst tye_idx) (T :: Ts))
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   391
              | 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
   392
                  handle NO_UNIFIER (msg, _) =>
51248
029de23bb5e8 tuned error messages
traytel
parents: 51246
diff changeset
   393
                    error (gen_msg err ("failed to unify invariant arguments\n" ^ msg))));
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   394
            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
   395
              (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
49142
0f81eca1e473 more conservative rechecking of processed constraints in subtyping constraint simplification
traytel
parents: 47060
diff changeset
   396
            val test_update = is_typeT orf is_freeT orf is_fixedvarT;
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   397
            val (ch, done') =
51246
755562fd2d9d apply unifying substitution before building the constraint graph
traytel
parents: 49660
diff changeset
   398
              done
755562fd2d9d apply unifying substitution before building the constraint graph
traytel
parents: 49660
diff changeset
   399
              |> map (apfst (pairself (Type_Infer.deref tye')))
755562fd2d9d apply unifying substitution before building the constraint graph
traytel
parents: 49660
diff changeset
   400
              |> (if not (null new) then rpair []  else split_cs test_update);
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   401
            val todo' = ch @ todo;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   402
          in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   403
            simplify done' (new @ todo') (tye', idx')
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   404
          end
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   405
        (*xi is definitely a parameter*)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   406
        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
   407
          let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   408
            val n = length Ts;
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   409
            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
   410
            val tye' = Vartab.update_new (xi, Type(a, args)) tye;
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   411
            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
   412
            val todo' = ch @ todo;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   413
            val new =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   414
              if varleq then (Type(a, args), Type (a, Ts))
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   415
              else (Type (a, Ts), Type (a, args));
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   416
          in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   417
            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
   418
          end
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   419
        (*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
   420
        and eliminate TU done todo tye idx =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   421
          let
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   422
            val [TVar (xi, S)] = filter Type_Infer.is_paramT TU;
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   423
            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
   424
            val SOME S' = sort_of T;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   425
            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
   426
            val tye' = Vartab.update_new (xi, T) tye;
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   427
            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
   428
            val todo' = ch @ todo;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   429
          in
42388
a44b0fdaa6c2 standardized aliases of operations on tsig;
wenzelm
parents: 42386
diff changeset
   430
            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
   431
            then simplify done' todo' (tye', idx)
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   432
            else error (gen_msg err "sort mismatch")
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   433
          end
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   434
        and simplify done [] tye_idx = (done, tye_idx)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   435
          | simplify done (((T, U), error_pack) :: todo) (tye_idx as (tye, idx)) =
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   436
              (case (Type_Infer.deref tye T, Type_Infer.deref tye U) of
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   437
                (T1 as Type (a, []), T2 as Type (b, [])) =>
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   438
                  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
   439
                  else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   440
                  else error (gen_msg err (quote (Syntax.string_of_typ ctxt T1) ^
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   441
                    " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2)))
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   442
              | (Type (a, Ts), Type (b, Us)) =>
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   443
                  if a <> b then error (gen_msg err "different constructors")
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   444
                    (fst tye_idx) error_pack
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   445
                  else contract a Ts Us error_pack done todo tye idx
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   446
              | (TVar (xi, S), Type (a, Ts as (_ :: _))) =>
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   447
                  expand true xi S a Ts error_pack done todo tye idx
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   448
              | (Type (a, Ts as (_ :: _)), TVar (xi, S)) =>
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   449
                  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
   450
              | (T, U) =>
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   451
                  if T = U then simplify done todo tye_idx
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   452
                  else if exists (is_freeT orf is_fixedvarT) [T, U] andalso
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   453
                    exists Type_Infer.is_paramT [T, U]
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   454
                  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
   455
                  else if exists (is_freeT orf is_fixedvarT) [T, U]
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   456
                  then error (gen_msg err "not eliminated free/fixed variables")
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   457
                  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
   458
      in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   459
        simplify [] cs tye_idx
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   460
      end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   461
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   462
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   463
    (* do simplification *)
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   464
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   465
    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
   466
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   467
    fun find_error_pack lower T' = map_filter
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   468
      (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
   469
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   470
    fun find_cycle_packs nodes =
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   471
      let
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   472
        val (but_last, last) = split_last nodes
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   473
        val pairs = (last, hd nodes) :: (but_last ~~ tl nodes);
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   474
      in
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   475
        map_filter
40838
d9bd6df700a8 simplified equality on pairs of types;
wenzelm
parents: 40836
diff changeset
   476
          (fn (TU, pack) => if member (op =) pairs TU then SOME pack else NONE)
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   477
          cs'
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   478
      end;
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   479
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   480
    (*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
   481
      in terms of the subtype-relation (excluding T itself)*)
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   482
    fun styps super T =
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 43591
diff changeset
   483
      (if super then Graph.immediate_succs else Graph.immediate_preds) coes_graph T
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   484
        handle Graph.UNDEF _ => [];
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   485
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   486
    fun minmax sup (T :: Ts) =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   487
      let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   488
        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
   489
        fun extract T [] = T
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   490
          | extract T (U :: Us) =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   491
              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
   492
              else if Graph.is_edge coes_graph (adjust U T) then extract U Us
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   493
              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
   494
      in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   495
        t_of (extract T Ts)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   496
      end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   497
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   498
    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
   499
      let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   500
        fun adjust T U = if super then (T, U) else (U, T);
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   501
        fun styp_test U Ts = forall
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   502
          (fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts;
42388
a44b0fdaa6c2 standardized aliases of operations on tsig;
wenzelm
parents: 42386
diff changeset
   503
        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
   504
      in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   505
        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
   506
      end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   507
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   508
    (* 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
   509
       e.g. in the supremum case (sup = true):
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   510
               ------- 'a::S---
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   511
              /        /    \  \
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   512
             /        /      \  \
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   513
        'b::C1   'c::C2 ...  T1 T2 ...
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   514
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   515
       sorts - list of sorts [C1, C2, ...]
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   516
       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
   517
    *)
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   518
    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
   519
      let
42388
a44b0fdaa6c2 standardized aliases of operations on tsig;
wenzelm
parents: 42386
diff changeset
   520
        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
   521
          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
   522
        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
   523
      in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   524
        (case fold candidates Ts (filter restriction (T :: styps sup T)) of
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   525
          [] => 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
   526
        | [T] => t_of T
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   527
        | Ts => minmax sup Ts)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   528
      end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   529
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   530
    fun build_graph G [] tye_idx = (G, tye_idx)
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   531
      | 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
   532
        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
   533
        else
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   534
          let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   535
            val G' = maybe_new_typnodes [T, U] G;
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   536
            val (G'', tye_idx') = (Typ_Graph.add_edge_acyclic (T, U) G', tye_idx)
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   537
              handle Typ_Graph.CYCLES cycles =>
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   538
                let
42383
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   539
                  val (tye, idx) =
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   540
                    fold
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   541
                      (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
   542
                        handle NO_UNIFIER (msg, _) =>
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   543
                          err_bound ctxt
51248
029de23bb5e8 tuned error messages
traytel
parents: 51246
diff changeset
   544
                            (gen_msg err ("constraint cycle not unifiable\n" ^ msg)) (fst tye_idx)
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   545
                            (find_cycle_packs cycle)))
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   546
                      cycles tye_idx
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   547
                in
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   548
                  collapse (tye, idx) cycles G
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   549
                end
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   550
          in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   551
            build_graph G'' cs tye_idx'
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   552
          end
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   553
    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
   554
      let
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   555
        (*all cycles collapse to one node,
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   556
          because all of them share at least the nodes x and y*)
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   557
        val nodes = (distinct (op =) (flat cycles));
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   558
        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
   559
        val P = new_imm_preds G nodes;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   560
        val S = new_imm_succs G nodes;
46665
919dfcdf6d8a discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
wenzelm
parents: 46614
diff changeset
   561
        val G' = fold Typ_Graph.del_node (tl nodes) G;
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   562
        fun check_and_gen super T' =
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   563
          let val U = Type_Infer.deref tye T';
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   564
          in
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   565
            if not (is_typeT T) orelse not (is_typeT U) orelse T = U
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   566
            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
   567
            else
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   568
              if super andalso
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   569
                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
   570
              else if not super andalso
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   571
                Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes)
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   572
              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
   573
                    (fst tye_idx)
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   574
                    (maps find_cycle_packs cycles @ find_error_pack super T')
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   575
          end;
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   576
      in
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   577
        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
   578
      end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   579
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   580
    fun assign_bound lower G key (tye_idx as (tye, _)) =
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   581
      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
   582
        let
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   583
          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
   584
          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
   585
          val raw_bound = get_bound G key;
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   586
          val bound = map (Type_Infer.deref tye) raw_bound;
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   587
          val not_params = filter_out Type_Infer.is_paramT bound;
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   588
          fun to_fulfil T =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   589
            (case sort_of T of
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   590
              NONE => NONE
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   591
            | SOME S =>
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   592
                SOME
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   593
                  (map nameT
42405
13ecdb3057d8 split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents: 42402
diff changeset
   594
                    (filter_out Type_Infer.is_paramT
13ecdb3057d8 split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents: 42402
diff changeset
   595
                      (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
   596
          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
   597
          val assignment =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   598
            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
   599
            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
   600
                handle BOUND_ERROR msg =>
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   601
                  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
   602
        in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   603
          (case assignment of
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   604
            NONE => tye_idx
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   605
          | SOME T =>
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   606
              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
   607
              else if lower then (*upper bound check*)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   608
                let
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   609
                  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
   610
                  val s = nameT T;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   611
                in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   612
                  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
   613
                  then apfst (Vartab.update (xi, T)) tye_idx
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   614
                  else err_bound ctxt (gen_msg err ("assigned base type " ^
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   615
                    quote (Syntax.string_of_typ ctxt T) ^
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   616
                    " clashes with the upper bound of variable " ^
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   617
                    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
   618
                end
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   619
              else apfst (Vartab.update (xi, T)) tye_idx)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   620
        end
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   621
      else tye_idx;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   622
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   623
    val assign_lb = assign_bound true;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   624
    val assign_ub = assign_bound false;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   625
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   626
    fun assign_alternating ts' ts G tye_idx =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   627
      if ts' = ts then tye_idx
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   628
      else
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   629
        let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   630
          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
   631
            |> fold (assign_ub G) ts;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   632
        in
42383
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   633
          assign_alternating ts
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   634
            (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
   635
        end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   636
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   637
    (*Unify all weakly connected components of the constraint forest,
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   638
      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
   639
      params anyway.*)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   640
    fun unify_params G (tye_idx as (tye, _)) =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   641
      let
40286
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   642
        val max_params =
b928e3960446 more sharing of operations, without aliases;
wenzelm
parents: 40285
diff changeset
   643
          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
   644
        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
   645
      in
42383
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   646
        fold
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   647
          (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
   648
            handle NO_UNIFIER (msg, _) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts)
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   649
          to_unify tye_idx
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   650
      end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   651
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   652
    fun solve_constraints G tye_idx = tye_idx
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   653
      |> assign_alternating [] (Typ_Graph.keys G) G
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   654
      |> unify_params G;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   655
  in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   656
    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
   657
      |-> solve_constraints
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   658
  end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   659
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   660
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
(** coercion insertion **)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   663
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   664
fun gen_coercion ctxt err tye TU =
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   665
  let
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   666
    fun gen (T1, T2) = (case pairself (Type_Infer.deref tye) (T1, T2) of
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   667
        (T1 as (Type (a, [])), T2 as (Type (b, []))) =>
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   668
            if a = b
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   669
            then mk_identity T1
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   670
            else
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   671
              (case Symreltab.lookup (coes_of ctxt) (a, b) of
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   672
                NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   673
                  " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2))
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   674
              | SOME (co, _) => co)
45102
7bb89635eb51 correct coercion generation in case of unknown map functions
traytel
parents: 45060
diff changeset
   675
      | (T1 as Type (a, Ts), T2 as Type (b, Us)) =>
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   676
            if a <> b
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   677
            then
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   678
              (case Symreltab.lookup (coes_of ctxt) (a, b) of
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   679
                (*immediate error - cannot fix complex coercion with the global algorithm*)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   680
                NONE => error (err () ^ "No coercion known for type constructors: " ^
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   681
                  quote a ^ " and " ^ quote b)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   682
              | SOME (co, ((Ts', Us'), _)) =>
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   683
                  let
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   684
                    val co_before = gen (T1, Type (a, Ts'));
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   685
                    val coT = range_type (fastype_of co_before);
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   686
                    val insts = inst_collect tye (err ++> "Could not insert complex coercion")
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   687
                      (domain_type (fastype_of co)) coT;
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   688
                    val co' = Term.subst_TVars insts co;
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   689
                    val co_after = gen (Type (b, (map (typ_subst_TVars insts) Us')), T2);
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   690
                  in
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   691
                    Abs (Name.uu, T1, Library.foldr (op $)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   692
                      (filter (not o is_identity) [co_after, co', co_before], Bound 0))
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   693
                  end)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   694
            else
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   695
              let
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   696
                fun sub_co (COVARIANT, TU) = (SOME (gen TU), NONE)
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   697
                  | sub_co (CONTRAVARIANT, TU) = (SOME (gen (swap TU)), NONE)
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   698
                  | sub_co (INVARIANT, (T, _)) = (NONE, SOME T)
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   699
                  | sub_co (INVARIANT_TO T, _) = (NONE, NONE);
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   700
                fun ts_of [] = []
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   701
                  | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   702
              in
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   703
                (case Symtab.lookup (tmaps_of ctxt) a of
45102
7bb89635eb51 correct coercion generation in case of unknown map functions
traytel
parents: 45060
diff changeset
   704
                  NONE =>
7bb89635eb51 correct coercion generation in case of unknown map functions
traytel
parents: 45060
diff changeset
   705
                    if Type.could_unify (T1, T2)
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   706
                    then mk_identity T1
45102
7bb89635eb51 correct coercion generation in case of unknown map functions
traytel
parents: 45060
diff changeset
   707
                    else raise COERCION_GEN_ERROR
7bb89635eb51 correct coercion generation in case of unknown map functions
traytel
parents: 45060
diff changeset
   708
                      (err ++> "No map function for " ^ quote a ^ " known")
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   709
                | SOME (tmap, variances) =>
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   710
                    let
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   711
                      val (used_coes, invarTs) =
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   712
                        map_split sub_co (variances ~~ (Ts ~~ Us))
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   713
                        |>> map_filter I
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   714
                        ||> map_filter I;
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   715
                      val Tinsts = ts_of (map fastype_of used_coes) @ invarTs;
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   716
                    in
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   717
                      if null (filter (not o is_identity) used_coes)
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   718
                      then mk_identity (Type (a, Ts))
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   719
                      else Term.list_comb (instantiate tmap Tinsts, used_coes)
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   720
                    end)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   721
              end
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   722
      | (T, U) =>
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   723
            if Type.could_unify (T, U)
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   724
            then mk_identity T
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   725
            else raise COERCION_GEN_ERROR (err ++> "Cannot generate coercion from " ^
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   726
              quote (Syntax.string_of_typ ctxt T) ^ " to " ^
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   727
              quote (Syntax.string_of_typ ctxt U)));
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   728
  in
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   729
    gen TU
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   730
  end;
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   731
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   732
fun function_of ctxt err tye T =
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   733
  (case Type_Infer.deref tye T of
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   734
    Type (C, Ts) =>
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   735
      (case Symreltab.lookup (coes_of ctxt) (C, "fun") of
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   736
        NONE => error (err () ^ "No complex coercion from " ^ quote C ^ " to fun")
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   737
      | SOME (co, ((Ts', _), _)) =>
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   738
        let
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   739
          val co_before = gen_coercion ctxt err tye (Type (C, Ts), Type (C, Ts'));
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   740
          val coT = range_type (fastype_of co_before);
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   741
          val insts = inst_collect tye (err ++> "Could not insert complex coercion")
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   742
            (domain_type (fastype_of co)) coT;
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   743
          val co' = Term.subst_TVars insts co;
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   744
        in
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   745
          Abs (Name.uu, Type (C, Ts), Library.foldr (op $)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   746
            (filter (not o is_identity) [co', co_before], Bound 0))
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   747
        end)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   748
  | T' => error (err () ^ "No complex coercion from " ^
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   749
      quote (Syntax.string_of_typ ctxt T') ^ " to fun"));
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   750
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   751
fun insert_coercions ctxt (tye, idx) ts =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   752
  let
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   753
    fun insert _ (Const (c, T)) = (Const (c, T), T)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   754
      | insert _ (Free (x, T)) = (Free (x, T), T)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   755
      | insert _ (Var (xi, T)) = (Var (xi, T), T)
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   756
      | insert bs (Bound i) =
43278
1fbdcebb364b more robust exception pattern General.Subscript;
wenzelm
parents: 42616
diff changeset
   757
          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
   758
          in (Bound i, T) end
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   759
      | insert bs (Abs (x, T, t)) =
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   760
          let val (t', T') = insert (T :: bs) t;
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   761
          in (Abs (x, T, t'), T --> T') end
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   762
      | insert bs (t $ u) =
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   763
          let
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   764
            val (t', Type ("fun", [U, T])) = 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
   765
            val (u', U') = insert bs u;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   766
          in
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   767
            if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U')
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   768
            then (t' $ u', T)
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   769
            else (t' $ (gen_coercion ctxt (K "") tye (U', U) $ u'), T)
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   770
          end
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   771
  in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   772
    map (fst o insert []) ts
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   773
  end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   774
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   775
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   776
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   777
(** assembling the pipeline **)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   778
42398
919e17c0358e tuned signature;
wenzelm
parents: 42388
diff changeset
   779
fun coercion_infer_types ctxt raw_ts =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   780
  let
42405
13ecdb3057d8 split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents: 42402
diff changeset
   781
    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
   782
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   783
    fun inf _ _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx)
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   784
      | inf _ _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   785
      | inf _ _ (t as (Var (_, T))) tye_idx = (t, T, tye_idx)
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   786
      | inf _ bs (t as (Bound i)) tye_idx =
43278
1fbdcebb364b more robust exception pattern General.Subscript;
wenzelm
parents: 42616
diff changeset
   787
          (t, snd (nth bs i handle General.Subscript => err_loose i), tye_idx)
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   788
      | inf coerce bs (Abs (x, T, t)) tye_idx =
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   789
          let val (t', U, tye_idx') = inf coerce ((x, T) :: bs) t tye_idx
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   790
          in (Abs (x, T, t'), T --> U, tye_idx') end
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   791
      | inf coerce bs (t $ u) tye_idx =
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   792
          let
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   793
            val (t', T, tye_idx') = inf coerce bs t tye_idx;
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   794
            val coerce' = update_coerce_arg ctxt coerce t;
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   795
            val (u', U, (tye, idx)) = inf coerce' bs u tye_idx';
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   796
            val V = Type_Infer.mk_param idx [];
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   797
            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
   798
              handle NO_UNIFIER (msg, tye') =>
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   799
                let
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   800
                  val err = err_appl_msg ctxt msg tye' bs t T u U;
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   801
                  val W = Type_Infer.mk_param (idx + 1) [];
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   802
                  val (t'', (tye', idx')) =
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   803
                    (t', strong_unify ctxt (W --> V, T) (tye, idx + 2))
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   804
                      handle NO_UNIFIER _ =>
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   805
                        let
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   806
                          val err' =
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   807
                            err ++> "\nLocal coercion insertion on the operator failed:\n";
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   808
                          val co = function_of ctxt err' tye T;
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   809
                          val (t'', T'', tye_idx'') = inf coerce bs (co $ t') (tye, idx + 2);
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   810
                        in
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   811
                          (t'', strong_unify ctxt (W --> V, T'') tye_idx''
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   812
                             handle NO_UNIFIER (msg, _) => error (err' () ^ msg))
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   813
                        end;
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   814
                  val err' = err ++>
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   815
                    (if t' aconv t'' then ""
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   816
                    else "\nSuccessfully coerced the operator to a function of type:\n" ^
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   817
                      Syntax.string_of_typ ctxt
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   818
                        (the_single (snd (prep_output ctxt tye' bs [] [W --> V]))) ^ "\n") ^
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   819
                    (if coerce' then "\nLocal coercion insertion on the operand failed:\n"
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   820
                    else "\nLocal coercion insertion on the operand disallowed:\n");
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   821
                  val (u'', U', tye_idx') =
52432
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
   822
                    if coerce' then
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   823
                      let val co = gen_coercion ctxt err' tye' (U, W);
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   824
                      in inf coerce' bs (if is_identity co then u else co $ u) (tye', idx') end
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   825
                    else (u, U, (tye', idx'));
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   826
                in
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   827
                  (t'' $ u'', strong_unify ctxt (U', W) tye_idx'
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   828
                    handle NO_UNIFIER (msg, _) => raise COERCION_GEN_ERROR (err' ++> msg))
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   829
                end;
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   830
          in (tu, V, tye_idx'') end;
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   831
42383
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   832
    fun infer_single t tye_idx =
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
   833
      let val (t, _, tye_idx') = inf true [] t tye_idx
40938
e258f6817add use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
traytel
parents: 40840
diff changeset
   834
      in (t, tye_idx') end;
42383
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   835
40938
e258f6817add use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
traytel
parents: 40840
diff changeset
   836
    val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx)
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   837
      handle COERCION_GEN_ERROR err =>
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   838
        let
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   839
          fun gen_single t (tye_idx, constraints) =
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   840
            let val (_, tye_idx', constraints') =
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   841
              generate_constraints ctxt (err ++> "\n") t tye_idx
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   842
            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
   843
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   844
          val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []);
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   845
          val (tye, idx) = process_constraints ctxt (err ++> "\n") constraints tye_idx;
42383
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   846
        in
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   847
          (insert_coercions ctxt (tye, idx) ts, (tye, idx))
40836
a81d66d72e70 two-staged architecture for subtyping;
traytel
parents: 40297
diff changeset
   848
        end);
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   849
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   850
    val (_, ts'') = Type_Infer.finish ctxt tye ([], ts');
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   851
  in ts'' end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   852
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   853
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   854
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   855
(** installation **)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   856
40283
805ce1d64af0 proper signature constraint for ML structure;
wenzelm
parents: 40282
diff changeset
   857
(* term check *)
805ce1d64af0 proper signature constraint for ML structure;
wenzelm
parents: 40282
diff changeset
   858
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42405
diff changeset
   859
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
   860
40283
805ce1d64af0 proper signature constraint for ML structure;
wenzelm
parents: 40282
diff changeset
   861
val add_term_check =
45429
fd58cbf8cae3 tuned signature;
wenzelm
parents: 45102
diff changeset
   862
  Syntax_Phases.term_check ~100 "coercions"
42402
c7139609b67d simplified check/uncheck interfaces: result comparison is hardwired by default;
wenzelm
parents: 42398
diff changeset
   863
    (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
   864
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   865
40283
805ce1d64af0 proper signature constraint for ML structure;
wenzelm
parents: 40282
diff changeset
   866
(* declarations *)
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   867
40284
c9acf88447e6 export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents: 40283
diff changeset
   868
fun add_type_map raw_t context =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   869
  let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   870
    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
   871
    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
   872
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   873
    fun err_str t = "\n\nThe provided function has the type:\n" ^
42383
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   874
      Syntax.string_of_typ ctxt (fastype_of t) ^
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   875
      "\n\nThe general type signature of a map function is:" ^
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   876
      "\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   877
      "\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
   878
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   879
    val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t))
47060
e2741ec9ae36 prefer explicitly qualified exception List.Empty;
wenzelm
parents: 46961
diff changeset
   880
      handle List.Empty => error ("Not a proper map function:" ^ err_str t);
42383
0ae4ad40d7b5 simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents: 42361
diff changeset
   881
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   882
    fun gen_arg_var ([], []) = []
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   883
      | gen_arg_var (Ts, (U, U') :: Us) =
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   884
          if U = U' then
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   885
            if null (Term.add_tvarsT U []) then INVARIANT_TO U :: gen_arg_var (Ts, Us)
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   886
            else if Term.is_TVar U then INVARIANT :: gen_arg_var (Ts, Us)
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   887
            else error ("Invariant xi and yi should be variables or variable-free:" ^ err_str t)
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   888
          else
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   889
            (case Ts of
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   890
              [] => error ("Different numbers of functions and variant arguments\n" ^ err_str t)
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   891
            | (T, T') :: Ts =>
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   892
              if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us)
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   893
              else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us)
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   894
              else error ("Functions do not apply to arguments correctly:" ^ err_str t));
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   895
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   896
    (*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
   897
    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
   898
          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
   899
          then ((map dest_funT fis, Ts ~~ Us), C1)
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   900
          else error ("Not a proper map function:" ^ err_str t)
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   901
      | check_map_fun fis T1 T2 true =
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   902
          let val (fis', T') = split_last fis
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   903
          in check_map_fun fis' T' (T1 --> T2) false end
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   904
      | 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
   905
41353
684003dbda54 Enabled non fully polymorphic map functions in subtyping
traytel
parents: 40939
diff changeset
   906
    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
   907
    val res_av = gen_arg_var (fst res);
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   908
  in
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   909
    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
   910
  end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   911
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   912
fun transitive_coercion ctxt tab G (a, b) =
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   913
  let
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   914
    fun safe_app t (Abs (x, T', u)) =
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   915
      let
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   916
        val t' = map_types Type_Infer.paramify_vars t;
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   917
      in
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   918
        singleton (coercion_infer_types ctxt) (Abs(x, T', (t' $ u)))
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   919
      end;
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   920
    val path = hd (Graph.irreducible_paths G (a, b));
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   921
    val path' = fst (split_last path) ~~ tl path;
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   922
    val coercions = map (fst o the o Symreltab.lookup tab) path';
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   923
    val trans_co = singleton (Variable.polymorphic ctxt)
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51327
diff changeset
   924
      (fold safe_app coercions (mk_identity dummyT));
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   925
    val (Ts, Us) = pairself (snd o Term.dest_Type) (Term.dest_funT (type_of trans_co))
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   926
  in
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   927
    (trans_co, ((Ts, Us), coercions))
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   928
  end;
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   929
40284
c9acf88447e6 export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents: 40283
diff changeset
   930
fun add_coercion raw_t context =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   931
  let
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   932
    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
   933
    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
   934
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   935
    fun err_coercion () = error ("Bad type for a coercion:\n" ^
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   936
        Syntax.string_of_term ctxt t ^ " :: " ^
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   937
        Syntax.string_of_typ ctxt (fastype_of t));
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   938
40840
2f97215e79bf just one Term.dest_funT;
wenzelm
parents: 40838
diff changeset
   939
    val (T1, T2) = Term.dest_funT (fastype_of t)
2f97215e79bf just one Term.dest_funT;
wenzelm
parents: 40838
diff changeset
   940
      handle TYPE _ => err_coercion ();
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   941
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   942
    val (a, Ts) = Term.dest_Type T1
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   943
      handle TYPE _ => err_coercion ();
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   944
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   945
    val (b, Us) = Term.dest_Type T2
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   946
      handle TYPE _ => err_coercion ();
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   947
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   948
    fun coercion_data_update (tab, G, _) =
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   949
      let
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   950
        val G' = maybe_new_nodes [(a, length Ts), (b, length Us)] G
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   951
        val G'' = Graph.add_edge_trans_acyclic (a, b) G'
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   952
          handle Graph.CYCLES _ => error (
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   953
            Syntax.string_of_typ ctxt T2 ^ " is already a subtype of " ^
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   954
            Syntax.string_of_typ ctxt T1 ^ "!\n\nCannot add coercion of type: " ^
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   955
            Syntax.string_of_typ ctxt (T1 --> T2));
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   956
        val new_edges =
49560
11430dd89e35 added graph encode/decode operations;
wenzelm
parents: 49142
diff changeset
   957
          flat (Graph.dest G'' |> map (fn ((x, _), ys) => ys |> map_filter (fn y =>
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   958
            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
   959
        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
   960
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   961
        val tab' = fold
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   962
          (fn pair => fn tab =>
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   963
            Symreltab.update (pair, transitive_coercion ctxt tab G_and_new pair) tab)
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   964
          (filter (fn pair => pair <> (a, b)) new_edges)
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   965
          (Symreltab.update ((a, b), (t, ((Ts, Us), []))) tab);
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   966
      in
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   967
        (tab', G'', restrict_graph G'')
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   968
      end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   969
  in
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   970
    map_coes_and_graphs coercion_data_update context
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   971
  end;
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   972
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   973
fun delete_coercion raw_t context =
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   974
  let
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   975
    val ctxt = Context.proof_of context;
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   976
    val t = singleton (Variable.polymorphic ctxt) raw_t;
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   977
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   978
    fun err_coercion the = error ("Not" ^
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   979
        (if the then " the defined " else  " a ") ^ "coercion:\n" ^
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   980
        Syntax.string_of_term ctxt t ^ " :: " ^
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   981
        Syntax.string_of_typ ctxt (fastype_of t));
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   982
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   983
    val (T1, T2) = Term.dest_funT (fastype_of t)
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   984
      handle TYPE _ => err_coercion false;
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   985
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   986
    val (a, Ts) = dest_Type T1
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   987
      handle TYPE _ => err_coercion false;
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   988
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   989
    val (b, Us) = dest_Type T2
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   990
      handle TYPE _ => err_coercion false;
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   991
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   992
    fun delete_and_insert tab G =
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   993
      let
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   994
        val pairs =
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
   995
          Symreltab.fold (fn ((a, b), (_, (_, ts))) => fn pairs =>
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   996
            if member (op aconv) ts t then (a, b) :: pairs else pairs) tab [(a, b)];
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   997
        fun delete pair (G, tab) = (Graph.del_edge pair G, Symreltab.delete_safe pair tab);
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
   998
        val (G', tab') = fold delete pairs (G, tab);
49564
wenzelm
parents: 49560
diff changeset
   999
        fun reinsert pair (G, xs) =
wenzelm
parents: 49560
diff changeset
  1000
          (case Graph.irreducible_paths G pair of
wenzelm
parents: 49560
diff changeset
  1001
            [] => (G, xs)
wenzelm
parents: 49560
diff changeset
  1002
          | _ => (Graph.add_edge pair G, (pair, transitive_coercion ctxt tab' G' pair) :: xs));
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1003
        val (G'', ins) = fold reinsert pairs (G', []);
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1004
      in
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
  1005
        (fold Symreltab.update ins tab', G'', restrict_graph G'')
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1006
      end
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1007
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1008
    fun show_term t = Pretty.block [Syntax.pretty_term ctxt t,
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1009
      Pretty.str " :: ", Syntax.pretty_typ ctxt (fastype_of t)]
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1010
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
  1011
    fun coercion_data_update (tab, G, _) =
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1012
        (case Symreltab.lookup tab (a, b) of
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1013
          NONE => err_coercion false
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
  1014
        | SOME (t', (_, [])) => if t aconv t'
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1015
            then delete_and_insert tab G
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1016
            else err_coercion true
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
  1017
        | SOME (t', (_, ts)) => if t aconv t'
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1018
            then error ("Cannot delete the automatically derived coercion:\n" ^
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1019
              Syntax.string_of_term ctxt t ^ " :: " ^
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1020
              Syntax.string_of_typ ctxt (fastype_of t) ^
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1021
              Pretty.string_of (Pretty.big_list "\n\nDeleting one of the coercions:"
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1022
                (map show_term ts)) ^
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1023
              "\nwill also remove the transitive coercion.")
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1024
            else err_coercion true);
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1025
  in
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
  1026
    map_coes_and_graphs coercion_data_update context
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1027
  end;
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1028
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1029
fun print_coercions ctxt =
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1030
  let
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
  1031
    fun separate _ [] = ([], [])
52432
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1032
      | separate P (x :: xs) = (if P x then apfst else apsnd) (cons x) (separate P xs);
45060
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
  1033
    val (simple, complex) =
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
  1034
      separate (fn (_, (_, ((Ts, Us), _))) => null Ts andalso null Us)
9c2568c0a504 local coercion insertion algorithm to support complex coercions
traytel
parents: 45059
diff changeset
  1035
        (Symreltab.dest (coes_of ctxt));
52432
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1036
    fun show_coercion ((a, b), (t, ((Ts, Us), _))) =
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1037
      Pretty.item [Pretty.block
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1038
       [Syntax.pretty_typ ctxt (Type (a, Ts)), Pretty.brk 1,
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1039
        Pretty.str "<:", Pretty.brk 1,
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1040
        Syntax.pretty_typ ctxt (Type (b, Us)), Pretty.brk 3,
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1041
        Pretty.block
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1042
         [Pretty.keyword "using", Pretty.brk 1,
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1043
          Pretty.quote (Syntax.pretty_term ctxt t)]]];
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1044
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1045
    val type_space = Proof_Context.type_space ctxt;
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1046
    val tmaps =
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1047
      sort (Name_Space.extern_ord ctxt type_space o pairself #1)
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1048
        (Symtab.dest (tmaps_of ctxt));
53539
51157ee7f5ba tuned signature;
wenzelm
parents: 52432
diff changeset
  1049
    fun show_map (c, (t, _)) =
52432
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1050
      Pretty.block
53539
51157ee7f5ba tuned signature;
wenzelm
parents: 52432
diff changeset
  1051
       [Name_Space.pretty ctxt type_space c, Pretty.str ":",
52432
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1052
        Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt t)];
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1053
  in
52432
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1054
   [Pretty.big_list "coercions between base types:" (map show_coercion simple),
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1055
    Pretty.big_list "other coercions:" (map show_coercion complex),
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1056
    Pretty.big_list "coercion maps:" (map show_map tmaps)]
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1057
  end |> Pretty.chunks |> Pretty.writeln;
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1058
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1059
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
  1060
(* theory setup *)
40283
805ce1d64af0 proper signature constraint for ML structure;
wenzelm
parents: 40282
diff changeset
  1061
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
  1062
val parse_coerce_args =
51327
62c033d7f3d8 tuned (extend datatype to inline option)
traytel
parents: 51319
diff changeset
  1063
  Args.$$$ "+" >> K PERMIT || Args.$$$ "-" >> K FORBID || Args.$$$ "0" >> K LEAVE
40283
805ce1d64af0 proper signature constraint for ML structure;
wenzelm
parents: 40282
diff changeset
  1064
805ce1d64af0 proper signature constraint for ML structure;
wenzelm
parents: 40282
diff changeset
  1065
val setup =
805ce1d64af0 proper signature constraint for ML structure;
wenzelm
parents: 40282
diff changeset
  1066
  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
  1067
  Attrib.setup @{binding coercion}
c9acf88447e6 export declarations by default, to allow other ML packages by-pass concrete syntax;
wenzelm
parents: 40283
diff changeset
  1068
    (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
  1069
    "declaration of new coercions" #>
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1070
  Attrib.setup @{binding coercion_delete}
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1071
    (Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t))))
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1072
    "deletion of coercions" #>
40297
c753e3f8b4d6 Attribute map_function -> coercion_map;
traytel
parents: 40286
diff changeset
  1073
  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
  1074
    (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
51319
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
  1075
    "declaration of new map functions" #>
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
  1076
  Attrib.setup @{binding coercion_args}
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
  1077
    (Args.const false -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
  1078
      (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
4a92178011e7 constants with coercion-invariant arguments (possibility to disable/reenable
traytel
parents: 51248
diff changeset
  1079
    "declaration of new constants with coercion-invariant arguments";
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
  1080
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1081
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1082
(* outer syntax commands *)
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1083
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1084
val _ =
52432
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1085
  Outer_Syntax.improper_command @{command_spec "print_coercions"}
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1086
    "print information about coercions"
c03090937c3b tuned message -- more markup;
wenzelm
parents: 51335
diff changeset
  1087
    (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)));
45059
28d3e387f22e printing and deleting of coercions
traytel
parents: 44338
diff changeset
  1088
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
  1089
end;