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