# HG changeset patch # User traytel # Date 1385391383 -3600 # Node ID 2bbcbf8cf47e2622abf0ac77878dda6b27c530e7 # Parent 3936fb5803d683b31e229e81289f0318225ebf07 possibility to fold coercion inference error messages; tuned; diff -r 3936fb5803d6 -r 2bbcbf8cf47e src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Mon Nov 25 16:00:09 2013 +0000 +++ b/src/Tools/subtyping.ML Mon Nov 25 15:56:23 2013 +0100 @@ -125,14 +125,22 @@ fun instantiate t Ts = Term.subst_TVars ((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts) t; -exception COERCION_GEN_ERROR of unit -> string; +exception COERCION_GEN_ERROR of unit -> (string * Pretty.T list); + +infixr ++> +@> (* lazy error msg composition *) + +fun err ++> prt = err #> apsnd (cons prt); +val op +@> = Library.foldl op ++>; + +fun eval_err err = err () + |> (fn (str, errs) => str ^ Pretty.string_of (Pretty.text_fold (rev errs))); fun inst_collect tye err T U = (case (T, Type_Infer.deref tye U) of - (TVar (xi, S), U) => [(xi, U)] + (TVar (xi, _), U) => [(xi, U)] | (Type (a, Ts), Type (b, Us)) => - if a <> b then raise error (err ()) else inst_collects tye err Ts Us - | (_, U') => if T <> U' then error (err ()) else []) + 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 []) and inst_collects tye err Ts Us = fold2 (fn T => fn U => fn is => inst_collect tye err T U @ is) Ts Us []; @@ -234,13 +242,12 @@ (** error messages **) -infixr ++> (* lazy error msg composition *) - -fun err ++> str = err #> suffix str +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]; -fun gen_msg err msg = - 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 fun prep_output ctxt tye bs ts Ts = let @@ -258,34 +265,34 @@ 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" end; + in (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n\n", [Pretty.fbrk, Pretty.fbrk, + Pretty.str "Coercion Inference:"]) end; -fun err_list ctxt msg tye Ts = +fun err_list ctxt err tye Ts = let val (_, Ts') = prep_output ctxt tye [] [] Ts; - val text = - msg ^ "\nCannot unify a list of types that should be the same:\n" ^ - Pretty.string_of (Pretty.list "[" "]" (map (Syntax.pretty_typ ctxt) 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 end; -fun err_bound ctxt msg tye packs = +fun err_bound ctxt err tye packs = let val (ts, Ts) = fold (fn (bs, t $ u, U, _, U') => fn (ts, Ts) => let val (t', T') = prep_output ctxt tye bs [t, u] [U', U] in (t' :: ts, T' :: Ts) end) packs ([], []); - val text = msg ^ "\n" ^ Pretty.string_of ( - Pretty.big_list "Cannot fulfil subtype constraints:" + val text = eval_err (err +@> [Pretty.fbrk, 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)) + ts Ts)]) in error text end; @@ -385,8 +392,9 @@ | CONTRAVARIANT => (swap constraint :: cs, tye_idx) | INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx handle NO_UNIFIER (msg, _) => - err_list ctxt (gen_msg err - "failed to unify invariant arguments w.r.t. to the known map function\n" ^ msg) + err_list ctxt (gen_err err + ("failed to unify invariant arguments w.r.t. to the known map function\n" ^ + msg)) (fst tye_idx) (T :: Ts)) | INVARIANT => (cs, strong_unify ctxt constraint tye_idx handle NO_UNIFIER (msg, _) => @@ -541,7 +549,7 @@ (fn cycle => fn tye_idx' => (unify_list cycle tye_idx' handle NO_UNIFIER (msg, _) => err_bound ctxt - (gen_msg err ("constraint cycle not unifiable\n" ^ msg)) (fst tye_idx) + (gen_err err ("constraint cycle not unifiable\n" ^ msg)) (fst tye_idx) (find_cycle_packs cycle))) cycles tye_idx in @@ -569,7 +577,7 @@ 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_msg err "cycle elimination produces inconsistent graph") + 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; @@ -597,7 +605,7 @@ val assignment = 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_msg err msg) tye + handle BOUND_ERROR msg => err_bound ctxt (gen_err err msg) tye (maps (find_error_pack (not lower)) raw_bound)) in (case assignment of @@ -611,7 +619,7 @@ 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_msg err ("assigned base type " ^ + 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 @@ -646,7 +654,7 @@ in fold (fn Ts => fn tye_idx' => unify_list Ts tye_idx' - handle NO_UNIFIER (msg, _) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts) + handle NO_UNIFIER (msg, _) => err_list ctxt (gen_err err msg) (fst tye_idx) Ts) to_unify tye_idx end; @@ -670,21 +678,24 @@ then mk_identity T1 else (case Symreltab.lookup (coes_of ctxt) (a, b) of - NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^ - " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2)) + 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)]) | 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 (err () ^ "No coercion known for type constructors: " ^ - quote a ^ " and " ^ quote b) + NONE => error (eval_err (err ++> Pretty.strs + ["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 ++> "Could not insert complex coercion") + val insts = inst_collect tye + (err ++> Pretty.str "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); @@ -706,7 +717,7 @@ if Type.could_unify (T1, T2) then mk_identity T1 else raise COERCION_GEN_ERROR - (err ++> "No map function for " ^ quote a ^ " known") + (err ++> Pretty.strs ["No map function for", quote a, "known"]) | SOME (tmap, variances) => let val (used_coes, invarTs) = @@ -723,9 +734,10 @@ | (T, U) => if Type.could_unify (T, U) then mk_identity T - else raise COERCION_GEN_ERROR (err ++> "Cannot generate coercion from " ^ - quote (Syntax.string_of_typ ctxt T) ^ " to " ^ - quote (Syntax.string_of_typ ctxt U))); + 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)])); in gen TU end; @@ -734,20 +746,21 @@ (case Type_Infer.deref tye T of Type (C, Ts) => (case Symreltab.lookup (coes_of ctxt) (C, "fun") of - NONE => error (err () ^ "No complex coercion from " ^ quote C ^ " to fun") + NONE => error (eval_err (err ++> Pretty.strs + ["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 ++> "Could not insert complex coercion") + val insts = inst_collect tye (err ++> Pretty.str "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 (err () ^ "No complex coercion from " ^ - quote (Syntax.string_of_typ ctxt T') ^ " to fun")); + | 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"]))); fun insert_coercions ctxt (tye, idx) ts = let @@ -767,7 +780,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 ("", [])) tye (U', U) $ u'), T) end in map (fst o insert []) ts @@ -804,21 +817,22 @@ (t', strong_unify ctxt (W --> V, T) (tye, idx + 2)) handle NO_UNIFIER _ => let - val err' = - err ++> "\nLocal coercion insertion on the operator failed:\n"; + val err' = err ++> + Pretty.str "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 (err' () ^ msg)) + handle NO_UNIFIER (msg, _) => + error (eval_err (err' ++> Pretty.str msg))) end; - val err' = err ++> - (if t' aconv t'' then "" - else "\nSuccessfully coerced the operator to a function of type:\n" ^ + val err' = err ++> Pretty.str + ((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 "\nLocal coercion insertion on the operand failed:\n" - else "\nLocal coercion insertion on the operand disallowed:\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); @@ -826,7 +840,8 @@ else (u, U, (tye', idx')); in (t'' $ u'', strong_unify ctxt (U', W) tye_idx' - handle NO_UNIFIER (msg, _) => raise COERCION_GEN_ERROR (err' ++> msg)) + handle NO_UNIFIER (msg, _) => + raise COERCION_GEN_ERROR (err' ++> Pretty.str msg)) end; in (tu, V, tye_idx'') end; @@ -839,11 +854,11 @@ let fun gen_single t (tye_idx, constraints) = let val (_, tye_idx', constraints') = - generate_constraints ctxt (err ++> "\n") t tye_idx + generate_constraints ctxt (err ++> Pretty.str "\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 ++> "\n") constraints tye_idx; + val (tye, idx) = process_constraints ctxt (err ++> Pretty.str "\n") constraints tye_idx; in (insert_coercions ctxt (tye, idx) ts, (tye, idx)) end); @@ -984,10 +999,10 @@ val (T1, T2) = Term.dest_funT (fastype_of t) handle TYPE _ => err_coercion false; - val (a, Ts) = dest_Type T1 + val (a, _) = dest_Type T1 handle TYPE _ => err_coercion false; - val (b, Us) = dest_Type T2 + val (b, _) = dest_Type T2 handle TYPE _ => err_coercion false; fun delete_and_insert tab G =