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