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