--- a/src/Tools/subtyping.ML Mon Feb 03 15:31:47 2014 +0100
+++ b/src/Tools/subtyping.ML Mon Feb 03 15:44:46 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
(
@@ -125,23 +125,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 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 [];
@@ -244,9 +245,8 @@
(** 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
@@ -267,17 +267,14 @@
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:"])
+ 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 =
@@ -287,17 +284,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;
@@ -447,11 +443,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
@@ -579,9 +576,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)
@@ -621,11 +619,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
@@ -680,25 +683,28 @@
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 a ^ " and " ^ quote 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
@@ -718,8 +724,9 @@
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 a ^ " known"))
| SOME (tmap, variances) =>
let
val (used_coes, invarTs) =
@@ -736,10 +743,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;
@@ -748,21 +757,24 @@
(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 C ^ " to 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 fun"]));
fun insert_coercions ctxt (tye, idx) ts =
let
@@ -782,7 +794,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
@@ -819,22 +831,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);
@@ -842,8 +852,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;
@@ -856,11 +865,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);
@@ -950,7 +959,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));
@@ -993,7 +1003,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));
@@ -1023,23 +1034,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;