[m-rev.] for review: don't allow nondefault mode functions in terms
Mark Brown
mark at mercurylang.org
Sun Nov 22 21:19:06 AEDT 2015
On Mon, Nov 2, 2015 at 2:08 AM, Zoltan Somogyi
<zoltan.somogyi at runbox.com> wrote:
> However, if it was
> done correctly, it would guarantee that the information cannot
> get lost.
We need to be careful with our words, because the term information,
like the term ground, has come to mean two different things. You were
using the term in the sense of explicit information, I think, so that
`in(func(in) = out is semidet)' is more information than just `in'.
As is known, this meaning is "defaulty": more information in this
sense does not equate to more logical consequences. But for soundness,
the logical consequences ordering is the important one; in this
ordering, `func(in) = out is semidet' and `ground' are incomparable.
In contrast, the set of logical consequences of `func(in) = out(s) is
det' is greater than that of `func(in) = out is det', assuming `s'
expresses some subtype of the relevant type. That means going from the
former to the latter is sound, so it's okay to lose information in
this sense. The problem to avoid is not so much that information is
lost, but that new logical consequences arise.
The attached diff reverts the workaround for bug 264. I think I've
covered all the mode system issues related to the bug, but if anyone
is not convinced please say so. It also attempts to clarify the
reference manual, which is for review by anyone. The new test case
demonstrates the point from the previous paragraph.
Discussion of what you are proposing I shall leave for another thread.
Mark
-------------- next part --------------
commit 2e69e68a382bf2ff7a3a47a33bc200707299b601
Author: Mark Brown <mark at mercurylang.org>
Date: Sun Nov 22 20:01:05 2015 +1100
Revert the workaround from commit 3c255eea
Bug 264, which this workaround was for, has been fixed in other changes.
compiler/mode_errors.m:
Remove the temporary error.
compiler/modecheck_unify.m:
Don't check this error condition.
doc/reference_manual.texi:
Document the constraint that actually applies, namely that functions
that do not match the default mode do not match Mercury's 'ground'
inst.
Clarify that "no higher-order inst information" means no *explicit*
information. Given that there is a default, this is not the same as
saying there are no logical consequences.
tests/invalid/default_ho_inst.err_exp:
tests/invalid/default_ho_inst_2.err_exp:
Update expected output.
tests/valid/Mmakefile:
tests/valid/ho_func_call_2.m:
New test case. Function modes that are not the same as the default,
but that match it, can still safely be treated as ground.
diff --git a/compiler/mode_errors.m b/compiler/mode_errors.m
index 29c4ec8..cd1223d 100644
--- a/compiler/mode_errors.m
+++ b/compiler/mode_errors.m
@@ -142,13 +142,6 @@
% One of the head variables did not have the expected final inst
% on exit from the proc.
- ; mode_error_nondefault_mode_func(prog_var, cons_id,
- list(prog_var), one_or_more(prog_var))
- % mode_error_nondefault_mode_func(X, ConsId, Ys, BadYs):
- % In the unification X = ConsId(Ys), the BadYs are functions
- % that do NOT have the default mode and determinism, i.e.
- % they aren't functions of the form f(in, ..., in) = out is det.
-
; purity_error_should_be_in_promise_purity_scope(
negated_context_desc, prog_var)
% The condition of an if-then-else or the body of a negation
@@ -351,11 +344,6 @@ mode_error_to_spec(ModeInfo, ModeError) = Spec :-
Spec = mode_error_unify_var_functor_to_spec(ModeInfo, Var, Name,
Args, Inst, ArgInsts)
;
- ModeError = mode_error_nondefault_mode_func(Var, Name,
- AllArgVars, BadArgVars),
- Spec = mode_error_nondefault_mode_func_to_spec(ModeInfo, Var, Name,
- AllArgVars, BadArgVars)
- ;
ModeError = mode_error_conj(Errors, Culprit),
Spec = mode_error_conj_to_spec(ModeInfo, Errors, Culprit)
;
@@ -1130,44 +1118,6 @@ mode_error_unify_var_functor_to_spec(ModeInfo, X, ConsId, Args,
%-----------------------------------------------------------------------------%
-:- func mode_error_nondefault_mode_func_to_spec(mode_info, prog_var,
- cons_id, list(prog_var), one_or_more(prog_var)) = error_spec.
-
-mode_error_nondefault_mode_func_to_spec(ModeInfo, X, ConsId,
- AllArgVars, BadArgVars) = Spec :-
- Preamble = mode_info_context_preamble(ModeInfo),
- mode_info_get_context(ModeInfo, Context),
- mode_info_get_varset(ModeInfo, VarSet),
- mode_info_get_module_info(ModeInfo, ModuleInfo),
- FunctorConsIdStr = functor_cons_id_to_string(ModuleInfo, VarSet,
- print_name_only, ConsId, AllArgVars),
- BadArgVars = one_or_more(HeadBadArgVar, TailBadArgVars),
- (
- TailBadArgVars = [],
- ArgPieces = [words("Argument"),
- quote(mercury_var_to_name_only(VarSet, HeadBadArgVar)),
- words("is a function")]
- ;
- TailBadArgVars = [_ | _],
- ArgPieces = [words("Arguments"),
- quote(mercury_vars_to_name_only(VarSet,
- [HeadBadArgVar | TailBadArgVars])),
- words("are functions")]
- ),
- Pieces = [words("mode error in unification of"),
- quote(mercury_var_to_name_only(VarSet, X)),
- words("and"), words_quote(FunctorConsIdStr), suffix("."), nl] ++
- ArgPieces ++ [words("whose argument modes and/or determinism"),
- words("differ from the default function signature"),
- words("(f(in, ..., in) = out is det)."),
- words("This is not allowed, because taking such arguments"),
- words("out of the term being constructed"),
- words("would lose their mode and determinism information."), nl],
- Spec = error_spec(severity_error, phase_mode_check(report_in_any_mode),
- [simple_msg(Context, [always(Preamble ++ Pieces)])]).
-
-%-----------------------------------------------------------------------------%
-
:- func mode_warning_cannot_succeed_var_var(mode_info,
prog_var, prog_var, mer_inst, mer_inst) = error_spec.
diff --git a/compiler/modecheck_unify.m b/compiler/modecheck_unify.m
index b8dba39..a6c0e90 100644
--- a/compiler/modecheck_unify.m
+++ b/compiler/modecheck_unify.m
@@ -757,15 +757,6 @@ modecheck_unify_functor(X0, TypeOfX, ConsId0, IsExistConstruction, ArgVars0,
% Construct the final goal expression.
( if
- Unification = construct(_, _, ConstructArgVars, _, _, _, _),
- find_nondefault_mode_func_vars(!.ModeInfo, ConstructArgVars,
- BadArgVars),
- BadArgVars = [HeadBadArgVar | TailBadArgVars]
- then
- handle_nondefault_mode_func_error(X, InstConsId,
- ArgVars0, one_or_more(HeadBadArgVar, TailBadArgVars),
- GoalExpr, !ModeInfo)
- else if
Unification = construct(_, _, _, _, _, _, _),
LiveX = is_dead
then
@@ -902,104 +893,6 @@ all_arg_vars_are_non_free_or_solver_vars([ArgVar | ArgVars], [Inst | Insts],
VarTypes, ModuleInfo, ArgVarsToInit)
).
-:- pred find_nondefault_mode_func_vars(mode_info::in, list(prog_var)::in,
- list(prog_var)::out) is det.
-
-find_nondefault_mode_func_vars(_ModeInfo, [], []).
-find_nondefault_mode_func_vars(ModeInfo, [ArgVar | ArgVars], BadArgVars) :-
- find_nondefault_mode_func_vars(ModeInfo, ArgVars, BadArgVarsTail),
- mode_info_get_var_types(ModeInfo, VarTypes),
- lookup_var_type(VarTypes, ArgVar, ArgType),
- ( if
- type_is_higher_order(ArgType),
- mode_info_get_instmap(ModeInfo, InstMap),
- instmap_lookup_var(InstMap, ArgVar, ArgInst),
- ArgInst = ground(_Uniq, HoInstInfo),
- ho_inst_info_is_nondefault_mode_func(HoInstInfo, yes)
- then
- BadArgVars = [ArgVar | BadArgVarsTail]
- else
- BadArgVars = BadArgVarsTail
- ).
-
-:- pred ho_inst_info_is_nondefault_mode_func(ho_inst_info::in, bool::out)
- is det.
-
-ho_inst_info_is_nondefault_mode_func(HoInstInfo, IsBad) :-
- (
- HoInstInfo = none_or_default_func,
- % When you take a higher order value out of a term, we record
- % `none_or_default_func' as its ho_inst_info. It should be ok to put
- % such values back into another term.
- IsBad = no
- ;
- HoInstInfo = higher_order(PredInstInfo),
- PredInstInfo = pred_inst_info(PredOrFunc, ArgModes, _ArgRegInfo,
- Detism),
- (
- PredOrFunc = pf_predicate,
- IsBad = no
- ;
- PredOrFunc = pf_function,
- ( if Detism = detism_det then
- list.det_split_last(ArgModes,
- ShouldBeInputArgModes, ShouldBeOutputMode),
- ( if
- list.all_true(is_input_mode, ShouldBeInputArgModes),
- is_output_mode(ShouldBeOutputMode)
- then
- IsBad = no
- else
- IsBad = yes
- )
- else
- IsBad = yes
- )
- )
- ).
-
-:- pred is_input_mode(mer_mode::in) is semidet.
-
-is_input_mode(Mode) :-
- (
- % The structural version of the input mode.
- Mode = (ground_inst -> ground_inst)
- ;
- % The named version of the input mode.
- Mode = in_mode
- ).
-
-:- pred is_output_mode(mer_mode::in) is semidet.
-
-is_output_mode(Mode) :-
- (
- % The structural version of the output mode.
- Mode = (free -> ground_inst)
- ;
- % The named version of the output mode.
- Mode = out_mode
- ).
-
-:- pred handle_nondefault_mode_func_error(prog_var::in, cons_id::in,
- list(prog_var)::in, one_or_more(prog_var)::in, hlds_goal_expr::out,
- mode_info::in, mode_info::out) is det.
-
-handle_nondefault_mode_func_error(X, InstConsId, ArgVars0, BadArgVars,
- GoalExpr, !ModeInfo) :-
- set_of_var.init(NoWaitingVars),
- ModeError = mode_error_nondefault_mode_func(X, InstConsId,
- ArgVars0, BadArgVars),
- mode_info_error(NoWaitingVars, ModeError, !ModeInfo),
- % If we get an error, set the inst to not_reached to avoid cascading
- % errors. But don't call categorize_unification, because that could
- % cause an invalid call to `unify_proc.request_unify'.
- Inst = not_reached,
- modecheck_set_var_inst(X, Inst, no, !ModeInfo),
- NoArgInsts = list.duplicate(list.length(ArgVars0), no),
- bind_args(Inst, ArgVars0, NoArgInsts, !ModeInfo),
- % Return any old garbage.
- GoalExpr = disj([]).
-
:- pred handle_var_functor_mode_error(prog_var::in, cons_id::in,
list(prog_var)::in, mer_inst::in, list(mer_inst)::in,
list(prog_var)::in, hlds_goal_expr::out,
diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index f5c7e51..bbd02c0 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -4491,23 +4491,15 @@ extraction will typically be @code{out} and the higher-order inst information
will be lost.
To partially alleviate this problem, and to make higher-order functional
programming easier, if the term to be called has a function
-type, but no higher-order inst information, we assume that it has the default
-higher-order function inst
+type, but no higher-order inst information is explicitly provided,
+we assume that it has the default higher-order function inst
@samp{func(in, @dots{}, in) = out is det}.
-As a consequence of this, it is a mode error to pass a higher-order function
-term that does not match this standard mode to somewhere where its higher-order
-inst information may be lost, such as to a polymorphic predicate where the
-argument mode is @code{in}.
-
-The Melbourne Mercury implementation currently cannot track
-all the places where higher-order inst information could be lost
-if a function is put into a term.
-To preserve safety, it therefore requires that
-functions may be put into terms only if they have the default signature,
-i.e. all their arguments have mode @code{in},
-their result has mode @code{out},
-and they have determinism @code{det}.
+As a consequence of this,
+a higher-order function term that does not match this default mode
+cannot match the Mercury @code{ground} inst.
+If it did, the term might later be called with the default mode,
+which would be unsound.
Mercury also provides builtin @samp{inst} values for use with solver types:
diff --git a/tests/invalid/default_ho_inst.err_exp b/tests/invalid/default_ho_inst.err_exp
index 5bcce1b..e911d60 100644
--- a/tests/invalid/default_ho_inst.err_exp
+++ b/tests/invalid/default_ho_inst.err_exp
@@ -1,10 +1,8 @@
default_ho_inst.m:026: In clause for `main(di, uo)':
-default_ho_inst.m:026: mode error in unification of `V_7' and
-default_ho_inst.m:026: `default_ho_inst.foo(V_9)'.
-default_ho_inst.m:026: Argument `V_9' is a function whose argument modes
-default_ho_inst.m:026: and/or determinism differ from the default function
-default_ho_inst.m:026: signature (f(in, ..., in) = out is det). This is not
-default_ho_inst.m:026: allowed, because taking such arguments out of the term
-default_ho_inst.m:026: being constructed would lose their mode and
-default_ho_inst.m:026: determinism information.
+default_ho_inst.m:026: in argument 1 of call to predicate
+default_ho_inst.m:026: `default_ho_inst.callfoo'/3:
+default_ho_inst.m:026: mode error: variable `V_7' has instantiatedness
+default_ho_inst.m:026: `unique(default_ho_inst.foo(/* unique */(func((ground
+default_ho_inst.m:026: >> ground)) = (free >> ground) is semidet)))',
+default_ho_inst.m:026: expected instantiatedness was `ground'.
For more information, recompile with `-E'.
diff --git a/tests/invalid/default_ho_inst_2.err_exp b/tests/invalid/default_ho_inst_2.err_exp
index 1a77a2f..95b6c4f 100644
--- a/tests/invalid/default_ho_inst_2.err_exp
+++ b/tests/invalid/default_ho_inst_2.err_exp
@@ -1,10 +1,8 @@
-default_ho_inst_2.m:031: In clause for `main(di, uo)':
-default_ho_inst_2.m:031: mode error in unification of `F' and
-default_ho_inst_2.m:031: `default_ho_inst_2.foo(V_8)'.
-default_ho_inst_2.m:031: Argument `V_8' is a function whose argument modes
-default_ho_inst_2.m:031: and/or determinism differ from the default function
-default_ho_inst_2.m:031: signature (f(in, ..., in) = out is det). This is not
-default_ho_inst_2.m:031: allowed, because taking such arguments out of the
-default_ho_inst_2.m:031: term being constructed would lose their mode and
-default_ho_inst_2.m:031: determinism information.
+default_ho_inst_2.m:033: In clause for `main(di, uo)':
+default_ho_inst_2.m:033: mode mismatch in disjunction.
+default_ho_inst_2.m:033: The variable `F' has these instantiation states:
+default_ho_inst_2.m:033: line 31: unique(default_ho_inst_2.foo(/* unique
+default_ho_inst_2.m:033: */(func((ground >> ground)) = (free >> ground) is
+default_ho_inst_2.m:033: semidet)))
+default_ho_inst_2.m:033: line 33: ground
For more information, recompile with `-E'.
diff --git a/tests/valid/Mmakefile b/tests/valid/Mmakefile
index 7180d57..f4bd247 100644
--- a/tests/valid/Mmakefile
+++ b/tests/valid/Mmakefile
@@ -133,6 +133,7 @@ OTHER_PROGS = \
higher_order_implied_mode \
ho_and_type_spec_bug \
ho_and_type_spec_bug2 \
+ ho_func_call_2 \
ho_inst \
ho_unify \
id_type_bug \
diff --git a/tests/valid/ho_func_call_2.m b/tests/valid/ho_func_call_2.m
new file mode 100644
index 0000000..31b2d1b
--- /dev/null
+++ b/tests/valid/ho_func_call_2.m
@@ -0,0 +1,29 @@
+:- module ho_func_call_2.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- type t ---> a ; b ; c.
+:- inst s ---> a ; b.
+
+:- type foo
+ ---> foo(func(t) = t).
+
+:- pred callfoo(foo::in, t::in, t::out) is det.
+
+callfoo(foo(F), X, F(X)).
+
+:- func subfoo(t::in) = (t::out(s)) is det.
+
+subfoo(_) = a.
+
+main(!IO) :-
+ callfoo(foo(subfoo), c, X),
+ io.write(X, !IO),
+ io.nl(!IO).
+
+% vim: ft=mercury ts=4 sts=4 sw=4 et
More information about the reviews
mailing list