# HG changeset patch # User wenzelm # Date 1391453438 -3600 # Node ID b1ca6ce9e1e0c8e1be07ac2a307f31801214ca87 # Parent 70e7ac6af16f70e010383390ac2d0bbfbfa1c667# Parent c3bb1cffce26cc718c16b736b7f01e6ee94fa686 merged; diff -r c3bb1cffce26 -r b1ca6ce9e1e0 src/HOL/Tools/Datatype/rep_datatype.ML --- a/src/HOL/Tools/Datatype/rep_datatype.ML Mon Feb 03 19:32:02 2014 +0100 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Mon Feb 03 19:50:38 2014 +0100 @@ -577,7 +577,7 @@ fun constr_of_term (Const (c, T)) = (c, T) | constr_of_term t = error ("Not a constant: " ^ Syntax.string_of_term ctxt t); fun no_constr (c, T) = - error ("Bad constructor: " ^ Proof_Context.extern_const ctxt c ^ "::" ^ + error ("Bad constructor: " ^ Proof_Context.markup_const ctxt c ^ "::" ^ Syntax.string_of_typ ctxt T); fun type_of_constr (cT as (_, T)) = let diff -r c3bb1cffce26 -r b1ca6ce9e1e0 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Mon Feb 03 19:32:02 2014 +0100 +++ b/src/Pure/Isar/class.ML Mon Feb 03 19:50:38 2014 +0100 @@ -528,7 +528,7 @@ fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); fun pr_param ((c, _), (v, ty)) = Pretty.block (Pretty.breaks - [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c), + [Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c, Pretty.str "::", Syntax.pretty_typ lthy ty]); in Pretty.command "instantiation" :: map pr_arity tycos @ map pr_param params end; @@ -538,7 +538,7 @@ val thy = Proof_Context.theory_of lthy; val _ = tycos |> List.app (fn tyco => if Sign.of_sort thy (Type (tyco, map TFree vs), sort) then () - else error ("Missing instance proof for type " ^ quote (Proof_Context.extern_type lthy tyco))); + else error ("Missing instance proof for type " ^ quote (Proof_Context.markup_type lthy tyco))); in lthy end; fun instantiation (tycos, vs, sort) thy = diff -r c3bb1cffce26 -r b1ca6ce9e1e0 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Mon Feb 03 19:32:02 2014 +0100 +++ b/src/Pure/Isar/locale.ML Mon Feb 03 19:50:38 2014 +0100 @@ -458,8 +458,8 @@ let val context = Context.Proof (Proof_Context.init_global thy); val marked = Idents.get context; - val (marked', context') = activate_all name thy Element.init - (Morphism.transfer_morphism o Context.theory_of) (empty_idents, context) + val (marked', context') = (empty_idents, context) + |> activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of); in context' |> Idents.put (merge_idents (marked, marked')) diff -r c3bb1cffce26 -r b1ca6ce9e1e0 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Mon Feb 03 19:32:02 2014 +0100 +++ b/src/Pure/Isar/overloading.ML Mon Feb 03 19:50:38 2014 +0100 @@ -171,7 +171,7 @@ val overloading = get_overloading lthy; fun pr_operation ((c, ty), (v, _)) = Pretty.block (Pretty.breaks - [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c), + [Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c, Pretty.str "::", Syntax.pretty_typ lthy ty]); in Pretty.command "overloading" :: map pr_operation overloading end; diff -r c3bb1cffce26 -r b1ca6ce9e1e0 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Feb 03 19:32:02 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Mon Feb 03 19:50:38 2014 +0100 @@ -42,8 +42,14 @@ val intern_type: Proof.context -> xstring -> string val intern_const: Proof.context -> xstring -> string val extern_class: Proof.context -> string -> xstring + val markup_class: Proof.context -> string -> string + val pretty_class: Proof.context -> string -> Pretty.T val extern_type: Proof.context -> string -> xstring + val markup_type: Proof.context -> string -> string + val pretty_type: Proof.context -> string -> Pretty.T val extern_const: Proof.context -> string -> xstring + val markup_const: Proof.context -> string -> string + val pretty_const: Proof.context -> string -> Pretty.T val transfer_syntax: theory -> Proof.context -> Proof.context val transfer: theory -> Proof.context -> Proof.context val background_theory: (theory -> theory) -> Proof.context -> Proof.context @@ -293,6 +299,14 @@ fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt); fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt); +fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |-> Markup.markup; +fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |-> Markup.markup; +fun markup_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |-> Markup.markup; + +fun pretty_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |> Pretty.mark_str; +fun pretty_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |> Pretty.mark_str; +fun pretty_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |> Pretty.mark_str; + (* theory transfer *) diff -r c3bb1cffce26 -r b1ca6ce9e1e0 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Mon Feb 03 19:32:02 2014 +0100 +++ b/src/Tools/Code/code_runtime.ML Mon Feb 03 19:50:38 2014 +0100 @@ -209,7 +209,7 @@ | SOME const' => (const, const')) consts consts' val tycos_map = map2 (fn tyco => fn NONE => - error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^ + error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^ "\nhas a user-defined serialization") | SOME tyco' => (tyco, tyco')) tycos tycos'; in (ml_code, (tycos_map, consts_map)) end; diff -r c3bb1cffce26 -r b1ca6ce9e1e0 src/Tools/Code/code_symbol.ML --- a/src/Tools/Code/code_symbol.ML Mon Feb 03 19:32:02 2014 +0100 +++ b/src/Tools/Code/code_symbol.ML Mon Feb 03 19:50:38 2014 +0100 @@ -125,13 +125,18 @@ fun is_value (Constant "") = true | is_value _ = false; -fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) - | quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco) - | quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class) +fun quote ctxt (Constant c) = + Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) + | quote ctxt (Type_Constructor tyco) = + "type " ^ Library.quote (Proof_Context.markup_type ctxt tyco) + | quote ctxt (Type_Class class) = + "class " ^ Library.quote (Proof_Context.markup_class ctxt class) | quote ctxt (Class_Relation (sub, super)) = - Library.quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ Library.quote (Proof_Context.extern_class ctxt super) + Library.quote (Proof_Context.markup_class ctxt sub) ^ " < " ^ + Library.quote (Proof_Context.markup_class ctxt super) | quote ctxt (Class_Instance (tyco, class)) = - Library.quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ Library.quote (Proof_Context.extern_class ctxt class); + Library.quote (Proof_Context.markup_type ctxt tyco) ^ " :: " ^ + Library.quote (Proof_Context.markup_class ctxt class); fun marker (Constant c) = "CONST " ^ c | marker (Type_Constructor tyco) = "TYPE " ^ tyco diff -r c3bb1cffce26 -r b1ca6ce9e1e0 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Mon Feb 03 19:32:02 2014 +0100 +++ b/src/Tools/Code/code_target.ML Mon Feb 03 19:50:38 2014 +0100 @@ -336,7 +336,7 @@ val _ = if null unimplemented then () else error ("No code equations for " ^ - commas (map (Proof_Context.extern_const ctxt) unimplemented)); + commas (map (Proof_Context.markup_const ctxt) unimplemented)); val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3; in (syms4, program4) end; diff -r c3bb1cffce26 -r b1ca6ce9e1e0 src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Mon Feb 03 19:32:02 2014 +0100 +++ b/src/Tools/subtyping.ML Mon Feb 03 19:50:38 2014 +0100 @@ -43,8 +43,8 @@ quote C ^ "."); fun merge_error_coerce_args C = - error ("Cannot merge tables for constants with coercion-invariant arguments.\n" - ^ "Conflicting declarations for the constant " ^ quote C ^ "."); + error ("Cannot merge tables for constants with coercion-invariant arguments.\n" ^ + "Conflicting declarations for the constant " ^ quote C ^ "."); structure Data = Generic_Data ( @@ -71,14 +71,6 @@ Data.map (fn Data {coes, full_graph, coes_graph, tmaps, coerce_args} => make_data (f (coes, full_graph, coes_graph, tmaps, coerce_args))); -fun map_coes f = - map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) => - (f coes, full_graph, coes_graph, tmaps, coerce_args)); - -fun map_coes_graph f = - map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) => - (coes, full_graph, f coes_graph, tmaps, coerce_args)); - fun map_coes_and_graphs f = map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) => let val (coes', full_graph', coes_graph') = f (coes, full_graph, coes_graph); @@ -113,7 +105,6 @@ | sort_of _ = NONE; val is_typeT = fn (Type _) => true | _ => false; -val is_stypeT = fn (Type (_, [])) => true | _ => false; val is_compT = fn (Type (_, _ :: _)) => true | _ => false; val is_freeT = fn (TFree _) => true | _ => false; val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false; @@ -125,23 +116,24 @@ fun instantiate t Ts = Term.subst_TVars ((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts) t; -exception COERCION_GEN_ERROR of unit -> (string * Pretty.T list); +exception COERCION_GEN_ERROR of unit -> string * Buffer.T; -infixr ++> +@> (* lazy error msg composition *) +infixr ++> (*composition with deferred error message*) +fun (err : unit -> string * Buffer.T) ++> s = + err #> apsnd (Buffer.add s); -fun (err : unit -> string * Pretty.T list) ++> (prt : Pretty.T) = - err #> apsnd (cons prt); -val op +@> = Library.foldl op ++>; +fun eval_err err = + let val (s, buf) = err () + in s ^ Markup.markup Markup.text_fold (Buffer.content buf) end; -fun eval_err err = err () - |> (fn (str, errs) => str ^ Pretty.string_of (Pretty.text_fold (rev errs))); +fun eval_error err = error (eval_err err); fun inst_collect tye err T U = (case (T, Type_Infer.deref tye U) of (TVar (xi, _), U) => [(xi, U)] | (Type (a, Ts), Type (b, Us)) => - if a <> b then raise error (eval_err err) else inst_collects tye err Ts Us - | (_, U') => if T <> U' then error (eval_err err) else []) + if a <> b then eval_error err else inst_collects tye err Ts Us + | (_, U') => if T <> U' then eval_error err else []) and inst_collects tye err Ts Us = fold2 (fn T => fn U => fn is => inst_collect tye err T U @ is) Ts Us []; @@ -178,7 +170,7 @@ meets (Ts, Ss) (meet (Type_Infer.deref tye T, S) tye_idx) | meets _ tye_idx = tye_idx; - val weak_meet = if weak then fn _ => I else meet + val weak_meet = if weak then fn _ => I else meet; (* occurs check and assignment *) @@ -236,17 +228,16 @@ (* Graph shortcuts *) -fun maybe_new_node s G = perhaps (try (Graph.new_node s)) G -fun maybe_new_nodes ss G = fold maybe_new_node ss G +fun maybe_new_node s G = perhaps (try (Graph.new_node s)) G; +fun maybe_new_nodes ss G = fold maybe_new_node ss G; (** error messages **) fun gen_err err msg = - err +@> [Pretty.fbrk, Pretty.str "Now trying to infer coercions globally.", Pretty.fbrk, - Pretty.fbrk, Pretty.str "Coercion inference failed", - Pretty.str (if msg = "" then "" else ":\n" ^ msg), Pretty.fbrk]; + err ++> ("\nNow trying to infer coercions globally.\n\nCoercion inference failed" ^ + (if msg = "" then "" else ":\n" ^ msg) ^ "\n"); val gen_msg = eval_err oo gen_err @@ -265,18 +256,16 @@ "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n"; fun err_appl_msg ctxt msg tye bs t T u U () = - let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U] - in (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n\n", [Pretty.fbrk, Pretty.fbrk, - Pretty.str "Coercion Inference:"]) end; + let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U] in + (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n\n", + Buffer.empty |> Buffer.add "Coercion Inference:\n\n") + end; fun err_list ctxt err tye Ts = - let - val (_, Ts') = prep_output ctxt tye [] [] Ts; - val text = eval_err (err +@> [Pretty.fbrk, - Pretty.str "Cannot unify a list of types that should be the same:", Pretty.fbrk, - Pretty.list "[" "]" (map (Syntax.pretty_typ ctxt) Ts')]); - in - error text + let val (_, Ts') = prep_output ctxt tye [] [] Ts in + eval_error (err ++> + ("\nCannot unify a list of types that should be the same:\n" ^ + Pretty.string_of (Pretty.list "[" "]" (map (Syntax.pretty_typ ctxt) Ts')))) end; fun err_bound ctxt err tye packs = @@ -286,17 +275,16 @@ let val (t', T') = prep_output ctxt tye bs [t, u] [U', U] in (t' :: ts, T' :: Ts) end) packs ([], []); - val text = eval_err (err +@> [Pretty.fbrk, Pretty.big_list "Cannot fulfil subtype constraints:" + val msg = + Pretty.string_of (Pretty.big_list "Cannot fulfil subtype constraints:" (map2 (fn [t, u] => fn [T, U] => Pretty.block [ Syntax.pretty_typ ctxt T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, Syntax.pretty_typ ctxt U, Pretty.brk 3, Pretty.str "from function application", Pretty.brk 2, Pretty.block [Syntax.pretty_term ctxt (t $ u)]]) - ts Ts)]) - in - error text - end; + ts Ts)); + in eval_error (err ++> ("\n" ^ msg)) end; @@ -446,11 +434,12 @@ (T1 as Type (a, []), T2 as Type (b, [])) => if a = b then simplify done todo tye_idx else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx - else error (gen_msg err (quote (Syntax.string_of_typ ctxt T1) ^ - " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2))) + else + error (gen_msg err (quote (Syntax.string_of_typ ctxt T1) ^ + " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2))) | (Type (a, Ts), Type (b, Us)) => - if a <> b then error (gen_msg err "different constructors") - (fst tye_idx) error_pack + if a <> b then + error (gen_msg err "different constructors") (fst tye_idx) error_pack else contract a Ts Us error_pack done todo tye idx | (TVar (xi, S), Type (a, Ts as (_ :: _))) => expand true xi S a Ts error_pack done todo tye idx @@ -509,7 +498,7 @@ fun adjust T U = if super then (T, U) else (U, T); fun styp_test U Ts = forall (fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts; - fun fitting Ts S U = Sign.of_sort thy (t_of U, S) andalso styp_test U Ts + fun fitting Ts S U = Sign.of_sort thy (t_of U, S) andalso styp_test U Ts; in forall (fn (Ts, S) => exists (fitting Ts S) (T :: styps super T)) styps_and_sorts end; @@ -578,9 +567,10 @@ Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T') else if not super andalso Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes) - else err_bound ctxt (gen_err err "cycle elimination produces inconsistent graph") - (fst tye_idx) - (maps find_cycle_packs cycles @ find_error_pack super T') + else + err_bound ctxt (gen_err err "cycle elimination produces inconsistent graph") + (fst tye_idx) + (maps find_cycle_packs cycles @ find_error_pack super T') end; in build_graph G' (map (check_and_gen false) P @ map (check_and_gen true) S) (tye, idx) @@ -607,7 +597,7 @@ if null bound orelse null not_params then NONE else SOME (tightest lower S styps_and_sorts (map nameT not_params) handle BOUND_ERROR msg => err_bound ctxt (gen_err err msg) tye - (maps (find_error_pack (not lower)) raw_bound)) + (maps (find_error_pack (not lower)) raw_bound)); in (case assignment of NONE => tye_idx @@ -620,11 +610,16 @@ in if subset (op = o apfst nameT) (filter is_typeT other_bound, s :: styps true s) then apfst (Vartab.update (xi, T)) tye_idx - else err_bound ctxt (gen_err err ("assigned base type " ^ - quote (Syntax.string_of_typ ctxt T) ^ - " clashes with the upper bound of variable " ^ - Syntax.string_of_typ ctxt (TVar(xi, S)))) tye - (maps (find_error_pack lower) other_bound) + else + err_bound ctxt + (gen_err err + (Pretty.string_of (Pretty.block + [Pretty.str "assigned base type", Pretty.brk 1, + Pretty.quote (Syntax.pretty_typ ctxt T), Pretty.brk 1, + Pretty.str "clashes with the upper bound of variable", Pretty.brk 1, + Syntax.pretty_typ ctxt (TVar (xi, S))]))) + tye + (maps (find_error_pack lower) other_bound) end else apfst (Vartab.update (xi, T)) tye_idx) end @@ -679,25 +674,30 @@ then mk_identity T1 else (case Symreltab.lookup (coes_of ctxt) (a, b) of - NONE => raise COERCION_GEN_ERROR (err +@> - [Pretty.quote (Syntax.pretty_typ ctxt T1), Pretty.brk 1, - Pretty.str "is not a subtype of", Pretty.brk 1, - Pretty.quote (Syntax.pretty_typ ctxt T2)]) + NONE => + raise COERCION_GEN_ERROR (err ++> + (Pretty.string_of o Pretty.block) + [Pretty.quote (Syntax.pretty_typ ctxt T1), Pretty.brk 1, + Pretty.str "is not a subtype of", Pretty.brk 1, + Pretty.quote (Syntax.pretty_typ ctxt T2)]) | SOME (co, _) => co) | (T1 as Type (a, Ts), T2 as Type (b, Us)) => if a <> b then (case Symreltab.lookup (coes_of ctxt) (a, b) of (*immediate error - cannot fix complex coercion with the global algorithm*) - NONE => error (eval_err (err ++> Pretty.strs - ["No coercion known for type constructors:", quote a, "and", quote b])) + NONE => + eval_error (err ++> + ("No coercion known for type constructors: " ^ + quote (Proof_Context.markup_type ctxt a) ^ " and " ^ + quote (Proof_Context.markup_type ctxt b))) | SOME (co, ((Ts', Us'), _)) => let val co_before = gen (T1, Type (a, Ts')); val coT = range_type (fastype_of co_before); - val insts = inst_collect tye - (err ++> Pretty.str "Could not insert complex coercion") - (domain_type (fastype_of co)) coT; + val insts = + inst_collect tye (err ++> "Could not insert complex coercion") + (domain_type (fastype_of co)) coT; val co' = Term.subst_TVars insts co; val co_after = gen (Type (b, (map (typ_subst_TVars insts) Us')), T2); in @@ -717,8 +717,11 @@ NONE => if Type.could_unify (T1, T2) then mk_identity T1 - else raise COERCION_GEN_ERROR - (err ++> Pretty.strs ["No map function for", quote a, "known"]) + else + raise COERCION_GEN_ERROR + (err ++> + ("No map function for " ^ quote (Proof_Context.markup_type ctxt a) + ^ " known")) | SOME (tmap, variances) => let val (used_coes, invarTs) = @@ -735,10 +738,12 @@ | (T, U) => if Type.could_unify (T, U) then mk_identity T - else raise COERCION_GEN_ERROR (err +@> - [Pretty.str "Cannot generate coercion from", Pretty.brk 1, - Pretty.quote (Syntax.pretty_typ ctxt T), Pretty.brk 1, Pretty.str "to", Pretty.brk 1, - Pretty.quote (Syntax.pretty_typ ctxt U)])); + else raise COERCION_GEN_ERROR (err ++> + (Pretty.string_of o Pretty.block) + [Pretty.str "Cannot generate coercion from", Pretty.brk 1, + Pretty.quote (Syntax.pretty_typ ctxt T), Pretty.brk 1, + Pretty.str "to", Pretty.brk 1, + Pretty.quote (Syntax.pretty_typ ctxt U)])); in gen TU end; @@ -747,21 +752,28 @@ (case Type_Infer.deref tye T of Type (C, Ts) => (case Symreltab.lookup (coes_of ctxt) (C, "fun") of - NONE => error (eval_err (err ++> Pretty.strs - ["No complex coercion from", quote C, "to fun"])) + NONE => + eval_error (err ++> ("No complex coercion from " ^ + quote (Proof_Context.markup_type ctxt C) ^ " to " ^ + quote (Proof_Context.markup_type ctxt "fun"))) | SOME (co, ((Ts', _), _)) => let val co_before = gen_coercion ctxt err tye (Type (C, Ts), Type (C, Ts')); val coT = range_type (fastype_of co_before); - val insts = inst_collect tye (err ++> Pretty.str "Could not insert complex coercion") - (domain_type (fastype_of co)) coT; + val insts = + inst_collect tye (err ++> "Could not insert complex coercion") + (domain_type (fastype_of co)) coT; val co' = Term.subst_TVars insts co; in Abs (Name.uu, Type (C, Ts), Library.foldr (op $) (filter (not o is_identity) [co', co_before], Bound 0)) end) - | T' => error (eval_err (err +@> [Pretty.str "No complex coercion from", Pretty.brk 1, - Pretty.quote (Syntax.pretty_typ ctxt T'), Pretty.brk 1, Pretty.str "to fun"]))); + | T' => + eval_error (err ++> + (Pretty.string_of o Pretty.block) + [Pretty.str "No complex coercion from", Pretty.brk 1, + Pretty.quote (Syntax.pretty_typ ctxt T'), Pretty.brk 1, + Pretty.str "to", Pretty.brk 1, Proof_Context.pretty_type ctxt "fun"])); fun insert_coercions ctxt (tye, idx) ts = let @@ -781,7 +793,7 @@ in if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U') then (t' $ u', T) - else (t' $ (gen_coercion ctxt (K ("", [])) tye (U', U) $ u'), T) + else (t' $ (gen_coercion ctxt (K ("", Buffer.empty)) tye (U', U) $ u'), T) end in map (fst o insert []) ts @@ -818,22 +830,20 @@ (t', strong_unify ctxt (W --> V, T) (tye, idx + 2)) handle NO_UNIFIER _ => let - val err' = err ++> - Pretty.str "Local coercion insertion on the operator failed:\n"; + val err' = err ++> "Local coercion insertion on the operator failed:\n"; val co = function_of ctxt err' tye T; val (t'', T'', tye_idx'') = inf coerce bs (co $ t') (tye, idx + 2); in (t'', strong_unify ctxt (W --> V, T'') tye_idx'' - handle NO_UNIFIER (msg, _) => - error (eval_err (err' ++> Pretty.str msg))) + handle NO_UNIFIER (msg, _) => eval_error (err' ++> msg)) end; - val err' = err ++> Pretty.str + val err' = err ++> ((if t' aconv t'' then "" - else "Successfully coerced the operator to a function of type:\n" ^ - Syntax.string_of_typ ctxt - (the_single (snd (prep_output ctxt tye' bs [] [W --> V]))) ^ "\n") ^ - (if coerce' then "Local coercion insertion on the operand failed:\n" - else "Local coercion insertion on the operand disallowed:\n")); + else "Successfully coerced the operator to a function of type:\n" ^ + Syntax.string_of_typ ctxt + (the_single (snd (prep_output ctxt tye' bs [] [W --> V]))) ^ "\n") ^ + (if coerce' then "Local coercion insertion on the operand failed:\n" + else "Local coercion insertion on the operand disallowed:\n")); val (u'', U', tye_idx') = if coerce' then let val co = gen_coercion ctxt err' tye' (U, W); @@ -841,8 +851,7 @@ else (u, U, (tye', idx')); in (t'' $ u'', strong_unify ctxt (U', W) tye_idx' - handle NO_UNIFIER (msg, _) => - raise COERCION_GEN_ERROR (err' ++> Pretty.str msg)) + handle NO_UNIFIER (msg, _) => raise COERCION_GEN_ERROR (err' ++> msg)) end; in (tu, V, tye_idx'') end; @@ -855,11 +864,11 @@ let fun gen_single t (tye_idx, constraints) = let val (_, tye_idx', constraints') = - generate_constraints ctxt (err ++> Pretty.str "\n") t tye_idx + generate_constraints ctxt (err ++> "\n") t tye_idx in (tye_idx', constraints' @ constraints) end; val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []); - val (tye, idx) = process_constraints ctxt (err ++> Pretty.str "\n") constraints tye_idx; + val (tye, idx) = process_constraints ctxt (err ++> "\n") constraints tye_idx; in (insert_coercions ctxt (tye, idx) ts, (tye, idx)) end); @@ -911,7 +920,7 @@ else error ("Functions do not apply to arguments correctly:" ^ err_str t)); (*retry flag needed to adjust the type lists, when given a map over type constructor fun*) - fun check_map_fun fis (Type (C1, Ts)) (Type (C2, Us)) retry = + fun check_map_fun fis (Type (C1, Ts)) (Type (C2, Us)) _ = if C1 = C2 andalso not (null fis) andalso forall is_funtype fis then ((map dest_funT fis, Ts ~~ Us), C1) else error ("Not a proper map function:" ^ err_str t) @@ -949,7 +958,8 @@ val ctxt = Context.proof_of context; val t = singleton (Variable.polymorphic ctxt) raw_t; - fun err_coercion () = error ("Bad type for a coercion:\n" ^ + fun err_coercion () = + error ("Bad type for a coercion:\n" ^ Syntax.string_of_term ctxt t ^ " :: " ^ Syntax.string_of_typ ctxt (fastype_of t)); @@ -992,7 +1002,8 @@ val ctxt = Context.proof_of context; val t = singleton (Variable.polymorphic ctxt) raw_t; - fun err_coercion the = error ("Not" ^ + fun err_coercion the = + error ("Not" ^ (if the then " the defined " else " a ") ^ "coercion:\n" ^ Syntax.string_of_term ctxt t ^ " :: " ^ Syntax.string_of_typ ctxt (fastype_of t)); @@ -1022,23 +1033,26 @@ (fold Symreltab.update ins tab', G'', restrict_graph G'') end - fun show_term t = Pretty.block [Syntax.pretty_term ctxt t, - Pretty.str " :: ", Syntax.pretty_typ ctxt (fastype_of t)] + fun show_term t = + Pretty.block [Syntax.pretty_term ctxt t, + Pretty.str " :: ", Syntax.pretty_typ ctxt (fastype_of t)]; fun coercion_data_update (tab, G, _) = - (case Symreltab.lookup tab (a, b) of - NONE => err_coercion false - | SOME (t', (_, [])) => if t aconv t' - then delete_and_insert tab G - else err_coercion true - | SOME (t', (_, ts)) => if t aconv t' - then error ("Cannot delete the automatically derived coercion:\n" ^ + (case Symreltab.lookup tab (a, b) of + NONE => err_coercion false + | SOME (t', (_, [])) => + if t aconv t' + then delete_and_insert tab G + else err_coercion true + | SOME (t', (_, ts)) => + if t aconv t' then + error ("Cannot delete the automatically derived coercion:\n" ^ Syntax.string_of_term ctxt t ^ " :: " ^ - Syntax.string_of_typ ctxt (fastype_of t) ^ - Pretty.string_of (Pretty.big_list "\n\nDeleting one of the coercions:" - (map show_term ts)) ^ + Syntax.string_of_typ ctxt (fastype_of t) ^ "\n\n" ^ + Pretty.string_of + (Pretty.big_list "Deleting one of the coercions:" (map show_term ts)) ^ "\nwill also remove the transitive coercion.") - else err_coercion true); + else err_coercion true); in map_coes_and_graphs coercion_data_update context end;