[m-dev.] for review: assertions in the interface
Peter Ross
petdr at cs.mu.OZ.AU
Thu Sep 2 18:03:36 AEST 1999
Hi,
Fergus here is a completely revised diff.
Since I now do function resolving in post_typecheck, a relative diff
wouldn't be that helpful.
===================================================================
Estimated hours taken: 56
Extend the assertion system by
* handling assertions in the interface of a module differently to
those in the implementation.
* testing an assertion for the commutivity property.
compiler/polymorphism.m:
Remove the resolving of function calls and data constructors, do it
in post_typecheck instead so that assertions are fully resolved.
compiler/post_typecheck.m:
Add the resolving of function calls and data constructors.
Also call assertion__in_interface_check, if an assertion is in the
interface.
compiler/purity.m:
post_typecheck__finish_assertion can now print error messages so
pass the io__states.
compiler/hlds_data.m:
Add assertion_table_pred_ids, so that intermod knows which pred_ids
are assertions.
compiler/hlds_out.m:
Add predicate hlds_out__write_assertion, which is used by intermod
to write assertions to .opt files.
Change the behaviour of outputing a call, so that if the call is a
function it gets written out in functional syntax. This is
necessary because the resolving of function symbols now occurs in
post_typecheck (pre writing .opt files) rather than in polymorphism
(post writing .opt files).
compiler/intermod.m:
Change intermod so that it writes out any assertion in the
interface to the .opt file.
compiler/modules.m:
Ensure that assertions in the interface are not written to the
.int files. Assertions should only appear in .opt files.
compiler/dead_proc_elim.m:
When intermodule optimization is turned on dead_proc_elim gets run
before typechecking and the assertion predicates are removed. This
change makes dead_proc_elim keep assertions.
compiler/make_hlds.m:
The head variables for an assertion are already known, so initialise
the clause_info structure to those variables rather then creating
Arity fresh variables.
Also don't insert unifications with the head of the assertion, since
we already know that only variables are in the head.
compiler/goal_util.m:
Add mode `goal_calls_pred_id(in, out) is nondet' for use by
assertion__record_preds_used_in.
compiler/assertion.m:
Add a predicate assertion__is_comutativity_assertion, which given
an assertion_id determines whether or not that assertion declares
the commutivity of a pred/func.
Add a predicate assertion__in_interface_check, which checks that an
assertion doesn't refer to any constructors, functions and
predicates defined in the implementation of that module.
Rewrite assertion__record_preds_used_in to use the nondet mode of
goal_calls_pred_id.
compiler/accumulator.m:
Remove the facts which declare '+' and '*' to be commutative, and
instead use the new assertion__is_commutivity_assertion predicate.
Also remove the bool from assoc_fact which is the commutivity of the
predicate, since only associative predicates reside in the table
now.
library/int.m:
Add commutivity declarations for '+' and '*', now that they have
been removed from the assoc_fact table. This allows me to test that
all of these changes actually work!
compiler/hlds_goal.m:
Clear up the documentation (I hope) for the type call_unify_context,
so that it is clear that the unification may also have been a
function application.
doc/reference_manual.texi:
doc/transition_guide.texi:
Document assertions.
Index: compiler/accumulator.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/accumulator.m,v
retrieving revision 1.6
diff -u -r1.6 accumulator.m
--- accumulator.m 1999/07/14 04:17:10 1.6
+++ accumulator.m 1999/09/02 07:38:56
@@ -95,7 +95,8 @@
:- implementation.
-:- import_module goal_util, globals, hlds_data, hlds_goal, hlds_out.
+:- import_module (assertion), goal_util, globals.
+:- import_module hlds_data, hlds_goal, hlds_out.
:- import_module inst_match, instmap, mode_util, options, prog_data, prog_util.
:- import_module assoc_list, bool, list, map, multi_map.
@@ -1637,15 +1638,82 @@
Args0, Args, PossibleStaticVars, Commutative):-
module_info_pred_proc_info(ModuleInfo, PredId, ProcId,
PredInfo, ProcInfo),
- pred_info_module(PredInfo, ModuleName),
- pred_info_name(PredInfo, PredName),
- pred_info_arity(PredInfo, Arity),
+
proc_info_argmodes(ProcInfo, Modes),
- assoc_fact(ModuleName, PredName, Arity, Modes, ModuleInfo, Args0, Args,
- PossibleStaticVars, Reordered),
- bool__not(Reordered, Commutative).
+ pred_info_get_assertions(PredInfo, Assertions),
+
+ (
+ commutativity_assertion(set__to_sorted_list(Assertions),
+ ModuleInfo, Args0, PossibleStaticVars0)
+ ->
+ check_modes(Args0, PossibleStaticVars0, Modes, ModuleInfo),
+ Args = Args0,
+ PossibleStaticVars = PossibleStaticVars0,
+ Commutative = yes
+ ;
+
+ % Check if it is associative
+ pred_info_module(PredInfo, ModuleName),
+ pred_info_name(PredInfo, PredName),
+ pred_info_arity(PredInfo, Arity),
+
+ assoc_fact(ModuleName, PredName, Arity, Modes,
+ ModuleInfo, Args0, Args, PossibleStaticVars),
+ Commutative = no
+ ).
%
+ % commutativity_assertion
+ %
+ % Does there exist one (and only one) commutativity assertion for the
+ % current predicate.
+ % The 'and only one condition' is required because we currently
+ % don't handle the case of predicates which have individual
+ % parts which are commutative, because then we don't know which
+ % variable is descended from which.
+ %
+:- pred commutativity_assertion(list(assert_id)::in, module_info::in,
+ prog_vars::in, set(prog_var)::out) is semidet.
+
+commutativity_assertion([AssertId | AssertIds], ModuleInfo, Args0,
+ PossibleStaticVars) :-
+ (
+ assertion__is_commutativity_assertion(AssertId, ModuleInfo,
+ Args0, StaticVarA - StaticVarB)
+ ->
+ \+ commutativity_assertion(AssertIds, ModuleInfo, Args0, _),
+ PossibleStaticVars = set__list_to_set([StaticVarA, StaticVarB])
+ ;
+ commutativity_assertion(AssertIds, ModuleInfo, Args0,
+ PossibleStaticVars)
+ ).
+
+
+ %
+ % check_modes(Vs, CVs, Ms, MI)
+ %
+ % Given a list of variables, Vs, and associated modes, Ms, make
+ % sure that each variable whose order can be rearranged (member of CVs)
+ % has a mode where the instantiatedness of the the variable
+ % doesn't change (ie an in mode).
+ %
+:- pred check_modes(prog_vars::in, set(prog_var)::in,
+ list(mode)::in, module_info::in) is semidet.
+
+check_modes([], _, _, _).
+check_modes([V | Vs], PossibleStaticVars, [M | Ms], ModuleInfo) :-
+ (
+ set__member(V, PossibleStaticVars)
+ ->
+ mode_get_insts(ModuleInfo, M, InitialInst, FinalInst),
+ inst_matches_final(InitialInst, FinalInst, ModuleInfo)
+ ;
+ true
+ ),
+ check_modes(Vs, PossibleStaticVars, Ms, ModuleInfo).
+
+
+ %
% XXX this fact table is only a temporary solution to whether or
% not a particular procedure is associative. In the long term
% the user should be able to annotate their code to indicate
@@ -1658,23 +1726,11 @@
%
:- pred assoc_fact(module_name::in, string::in, arity::in,
list(mode)::in, module_info::in, prog_vars::in,
- prog_vars::out, set(prog_var)::out, bool::out) is semidet.
-
-assoc_fact(unqualified("int"), "+", 3, [In, In, Out], ModuleInfo,
- [A, B, C], [A, B, C], PossibleStaticVars, no) :-
- set__list_to_set([A, B], PossibleStaticVars),
- mode_is_input(ModuleInfo, In),
- mode_is_output(ModuleInfo, Out).
-
-assoc_fact(unqualified("int"), "*", 3, [In, In, Out], ModuleInfo,
- [A, B, C], [A, B, C], PossibleStaticVars, no) :-
- set__list_to_set([A, B], PossibleStaticVars),
- mode_is_input(ModuleInfo, In),
- mode_is_output(ModuleInfo, Out).
+ prog_vars::out, set(prog_var)::out) is semidet.
assoc_fact(unqualified("list"), "append", 3, [TypeInfoIn, In, In, Out],
ModuleInfo, [TypeInfo, A, B, C],
- [TypeInfo, B, A, C], PossibleStaticVars, yes) :-
+ [TypeInfo, B, A, C], PossibleStaticVars) :-
set__list_to_set([A, B], PossibleStaticVars),
mode_is_input(ModuleInfo, TypeInfoIn),
mode_is_input(ModuleInfo, In),
Index: compiler/assertion.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/assertion.m,v
retrieving revision 1.1
diff -u -r1.1 assertion.m
--- assertion.m 1999/07/14 04:17:11 1.1
+++ assertion.m 1999/09/02 07:56:48
@@ -18,7 +18,8 @@
:- interface.
-:- import_module hlds_data, hlds_goal, hlds_module.
+:- import_module hlds_data, hlds_goal, hlds_module, prog_data.
+:- import_module io, std_util.
%
% assertion__goal
@@ -36,14 +37,95 @@
:- pred assertion__record_preds_used_in(hlds_goal::in, assert_id::in,
module_info::in, module_info::out) is det.
+ %
+ % assertion__is_commutativity_assertion(Id, MI, Vs, CVs)
+ %
+ % Does the assertion represented by the assertion id, Id,
+ % state the commutativity of a pred/func?
+ % We extend the usual definition of commutativity to apply to
+ % predicates or functions with more than two arguments as
+ % follows by allowing extra arguments which must be invariant.
+ % If so, this predicate returns (in CVs) the two variables which
+ % can be swapped in order if it was a call to Vs.
+ %
+ % The assertion must be in a form similar to this
+ % all [Is,A,B,C] ( p(Is,A,B,C) <=> p(Is,B,A,C) )
+ % for the predicate to return true (note that the invariant
+ % arguments, Is, can be any where providing they are in
+ % identical locations on both sides of the equivalence).
+ %
+:- pred assertion__is_commutativity_assertion(assert_id::in, module_info::in,
+ prog_vars::in, pair(prog_var)::out) is semidet.
+
+ %
+ % assertion__in_interface_check
+ %
+ % Ensure that an assertion which is defined in an interface
+ % doesn't refer to any constructors, functions and predicates
+ % defined in the implementation of that module.
+ %
+:- pred assertion__in_interface_check(hlds_goal::in, module_info::in,
+ io__state::di, io__state::uo) is det.
+
%-----------------------------------------------------------------------------%
:- implementation.
+
+:- import_module globals, goal_util, hlds_out, hlds_pred, options, prog_out.
+:- import_module bool, list, map, require, set, std_util.
+
+:- type subst == map(prog_var, prog_var).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
-:- import_module hlds_pred.
-:- import_module list, require, set, std_util.
+assertion__is_commutativity_assertion(AssertId, Module, CallVars,
+ CommutativeVars) :-
+ assertion__goal(AssertId, Module, Goal),
+ equivalent(Goal, P, Q),
+ P = call(PredId, _, VarsP, _, _, _) - _,
+ Q = call(PredId, _, VarsQ, _, _, _) - _,
+ commutative_var_ordering(VarsP, VarsQ, CallVars, CommutativeVars).
+
+ %
+ % commutative_var_ordering(Ps, Qs, Vs, CommutativeVs)
+ %
+ % Check that the two list of variables are identical except that
+ % the position of two variables has been swapped.
+ % e.g [A,B,C] and [B,A,C] is true.
+ % It also takes a list of variables, Vs, to a call and returns
+ % the two variables in that list that can be swapped, ie [A,B].
+ %
+:- pred commutative_var_ordering(prog_vars::in, prog_vars::in,
+ prog_vars::in, pair(prog_var)::out) is semidet.
+
+commutative_var_ordering([P|Ps], [Q|Qs], [V|Vs], CommutativeVars) :-
+ (
+ P = Q
+ ->
+ commutative_var_ordering(Ps, Qs, Vs, CommutativeVars)
+ ;
+ commutative_var_ordering_2(P, Q, Ps, Qs, Vs, CallVarB),
+ CommutativeVars = V - CallVarB
+ ).
+
+:- pred commutative_var_ordering_2(prog_var::in, prog_var::in, prog_vars::in,
+ prog_vars::in, prog_vars::in, prog_var::out) is semidet.
+
+commutative_var_ordering_2(VarP, VarQ, [P|Ps], [Q|Qs], [V|Vs], CallVarB) :-
+ (
+ P = Q
+ ->
+ commutative_var_ordering_2(VarP, VarQ, Ps, Qs, Vs, CallVarB)
+ ;
+ CallVarB = V,
+ P = VarQ,
+ Q = VarP,
+ Ps = Qs
+ ).
%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
assertion__goal(AssertId, Module, Goal) :-
module_info_assertion_table(Module, AssertTable),
@@ -54,88 +136,422 @@
(
Clauses = [clause(_ProcIds, Goal0, _Context)]
->
- Goal = Goal0
+ assertion__normalise_goal(Goal0, Goal)
;
error("assertion__goal: not an assertion")
).
%-----------------------------------------------------------------------------%
-
-assertion__record_preds_used_in(call(PredId, _, _, _, _, _) - _, AssertId,
- Module0, Module) :-
- update_pred_info(PredId, AssertId, Module0, Module).
-assertion__record_preds_used_in(generic_call(_, _, _, _) - _, _AssertId,
- Module, Module).
-assertion__record_preds_used_in(conj(Goals) - _, AssertId, Module0, Module) :-
- assertion__record_preds_used_in_goal_list(Goals, AssertId,
- Module0, Module).
-assertion__record_preds_used_in(switch(_, _, Cases, _) - _, AssertId,
- Module0, Module) :-
- assertion__record_preds_used_in_cases(Cases, AssertId, Module0, Module).
-assertion__record_preds_used_in(unify(_, _, _, _, _) - _,
- _AssertId, Module, Module).
-assertion__record_preds_used_in(disj(Goals, _) - _, AssertId,
- Module0, Module) :-
- assertion__record_preds_used_in_goal_list(Goals, AssertId,
- Module0, Module).
-assertion__record_preds_used_in(not(Goal) - _, AssertId, Module0, Module) :-
- assertion__record_preds_used_in(Goal, AssertId, Module0, Module).
-assertion__record_preds_used_in(some(_, _, Goal) - _, AssertId,
- Module0, Module) :-
- assertion__record_preds_used_in(Goal, AssertId, Module0, Module).
-assertion__record_preds_used_in(if_then_else(_, If, Then, Else, _) - _,
- AssertId, Module0, Module) :-
- assertion__record_preds_used_in(If, AssertId, Module0, Module1),
- assertion__record_preds_used_in(Then, AssertId, Module1, Module2),
- assertion__record_preds_used_in(Else, AssertId, Module2, Module).
-assertion__record_preds_used_in(pragma_c_code(_, _, _, _, _, _, _) - _,
- _AssertId, Module, Module).
-assertion__record_preds_used_in(par_conj(Goals, _) - _, AssertId,
- Module0, Module) :-
- assertion__record_preds_used_in_goal_list(Goals, AssertId,
- Module0, Module).
-
%-----------------------------------------------------------------------------%
-:- pred assertion__record_preds_used_in_goal_list(list(hlds_goal)::in,
- assert_id::in, module_info::in, module_info::out) is det.
+:- pred implies(hlds_goal::in, hlds_goal::out, hlds_goal::out) is semidet.
-assertion__record_preds_used_in_goal_list([], _, Module, Module).
-assertion__record_preds_used_in_goal_list([Goal | Goals], AssertId,
- Module0, Module) :-
- assertion__record_preds_used_in(Goal, AssertId, Module0, Module1),
- assertion__record_preds_used_in_goal_list(Goals, AssertId,
- Module1, Module).
+implies(Goal, P, Q) :-
+ % Goal = (P => Q)
+ Goal = not(conj([P, NotQ]) - _) - _,
+ NotQ = not(Q) - _.
+
+:- pred equivalent(hlds_goal::in, hlds_goal::out, hlds_goal::out) is semidet.
+
+equivalent(Goal, P, Q) :-
+ % Goal = P <=> Q
+ Goal = conj([A, B]) - _GoalInfo,
+ map__init(Subst),
+ implies(A, PA, QA),
+ implies(B, QB, PB),
+ equal_goals(PA, PB, Subst, _),
+ equal_goals(QA, QB, Subst, _),
+ P = PA,
+ Q = QA.
%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
-:- pred assertion__record_preds_used_in_cases(list(case)::in, assert_id::in,
- module_info::in, module_info::out) is det.
+ %
+ % equal_goals(GA, GB)
+ %
+ % Do these two goals represent the same hlds_goal modulo
+ % renaming.
+ %
+:- pred equal_goals(hlds_goal::in, hlds_goal::in,
+ subst::in, subst::out) is semidet.
+
+equal_goals(conj(GoalAs) - _, conj(GoalBs) - _, Subst0, Subst) :-
+ equal_goals_list(GoalAs, GoalBs, Subst0, Subst).
+equal_goals(call(PredId, _, VarsA, _, _, _) - _,
+ call(PredId, _, VarsB, _, _, _) - _, Subst0, Subst) :-
+ equal_vars(VarsA, VarsB, Subst0, Subst).
+equal_goals(generic_call(Type, VarsA, _, _) - _,
+ generic_call(Type, VarsB, _, _) - _, Subst0, Subst) :-
+ equal_vars(VarsA, VarsB, Subst0, Subst).
+equal_goals(switch(Var, CanFail, CasesA, _) - _,
+ switch(Var, CanFail, CasesB, _) - _, Subst0, Subst) :-
+ equal_goals_cases(CasesA, CasesB, Subst0, Subst).
+equal_goals(unify(VarA, RHSA, _, _, _) - _, unify(VarB, RHSB, _, _, _) - _,
+ Subst0, Subst) :-
+ equal_vars([VarA], [VarB], Subst0, Subst1),
+ equal_unification(RHSA, RHSB, Subst1, Subst).
+equal_goals(disj(GoalAs, _) - _, disj(GoalBs, _) - _, Subst0, Subst) :-
+ equal_goals_list(GoalAs, GoalBs, Subst0, Subst).
+equal_goals(not(GoalA) - _, not(GoalB) - _, Subst0, Subst) :-
+ equal_goals(GoalA, GoalB, Subst0, Subst).
+equal_goals(some(VarsA, _, GoalA) - _, some(VarsB, _, GoalB) - _,
+ Subst0, Subst) :-
+ equal_vars(VarsA, VarsB, Subst0, Subst1),
+ equal_goals(GoalA, GoalB, Subst1, Subst).
+equal_goals(if_then_else(VarsA, IfA, ThenA, ElseA, _) - _,
+ if_then_else(VarsB, IfB, ThenB, ElseB, _) - _, Subst0, Subst) :-
+ equal_vars(VarsA, VarsB, Subst0, Subst1),
+ equal_goals(IfA, IfB, Subst1, Subst2),
+ equal_goals(ThenA, ThenB, Subst2, Subst3),
+ equal_goals(ElseA, ElseB, Subst3, Subst).
+equal_goals(pragma_c_code(Attribs, PredId, _, VarsA, _, _, _) - _,
+ pragma_c_code(Attribs, PredId, _, VarsB, _, _, _) - _,
+ Subst0, Subst) :-
+ equal_vars(VarsA, VarsB, Subst0, Subst).
+equal_goals(par_conj(GoalAs, _) - _, par_conj(GoalBs, _) - _, Subst0, Subst) :-
+ equal_goals_list(GoalAs, GoalBs, Subst0, Subst).
+
+:- pred equal_vars(prog_vars::in, prog_vars::in, subst::in,
+ subst::out) is semidet.
+
+equal_vars([], [], Subst, Subst).
+equal_vars([VA | VAs], [VB | VBs], Subst0, Subst) :-
+ (
+ map__search(Subst0, VA, SubstVA)
+ ->
+ SubstVA = VB,
+ equal_vars(VAs, VBs, Subst0, Subst)
+ ;
+ map__insert(Subst0, VA, VB, Subst1),
+ equal_vars(VAs, VBs, Subst1, Subst)
+ ).
-assertion__record_preds_used_in_cases([], _, Module, Module).
-assertion__record_preds_used_in_cases([Case | Cases], AssertId,
- Module0, Module) :-
- Case = case(_, Goal),
- assertion__record_preds_used_in(Goal, AssertId, Module0, Module1),
- assertion__record_preds_used_in_cases(Cases, AssertId, Module1, Module).
+:- pred equal_unification(unify_rhs::in, unify_rhs::in, subst::in,
+ subst::out) is semidet.
+equal_unification(var(A), var(B), Subst0, Subst) :-
+ equal_vars([A], [B], Subst0, Subst).
+equal_unification(functor(ConsId, VarsA), functor(ConsId, VarsB),
+ Subst0, Subst) :-
+ equal_vars(VarsA, VarsB, Subst0, Subst).
+equal_unification(lambda_goal(PredOrFunc, EvalMethod, FixModes, NLVarsA, LVarsA,
+ Modes, Det, GoalA),
+ lambda_goal(PredOrFunc, EvalMethod, FixModes, NLVarsB, LVarsB,
+ Modes, Det, GoalB),
+ Subst0, Subst) :-
+ equal_vars(NLVarsA, NLVarsB, Subst0, Subst1),
+ equal_vars(LVarsA, LVarsB, Subst1, Subst2),
+ equal_goals(GoalA, GoalB, Subst2, Subst).
+
+
+:- pred equal_goals_list(hlds_goals::in, hlds_goals::in, subst::in,
+ subst::out) is semidet.
+
+equal_goals_list([], [], Subst, Subst).
+equal_goals_list([GoalA | GoalAs], [GoalB | GoalBs], Subst0, Subst) :-
+ equal_goals(GoalA, GoalB, Subst0, Subst1),
+ equal_goals_list(GoalAs, GoalBs, Subst1, Subst).
+
+:- pred equal_goals_cases(list(case)::in, list(case)::in, subst::in,
+ subst::out) is semidet.
+
+equal_goals_cases([], [], Subst, Subst).
+equal_goals_cases([CaseA | CaseAs], [CaseB | CaseBs], Subst0, Subst) :-
+ CaseA = case(ConsId, GoalA),
+ CaseB = case(ConsId, GoalB),
+ equal_goals(GoalA, GoalB, Subst0, Subst1),
+ equal_goals_cases(CaseAs, CaseBs, Subst1, Subst).
+
+%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
+assertion__record_preds_used_in(Goal, AssertId, Module0, Module) :-
+ % Explicit lambda expression needed since
+ % goal_calls_pred_id has multiple modes.
+ P = (pred(PredId::out) is nondet :- goal_calls_pred_id(Goal, PredId)),
+ solutions(P, PredIds),
+ list__foldl(update_pred_info(AssertId), PredIds, Module0, Module).
+
+%-----------------------------------------------------------------------------%
+
%
% update_pred_info(Id, A, M0, M)
%
% Record in the pred_info pointed to by Id that that predicate
% is used in the assertion pointed to by A.
%
-:- pred update_pred_info(pred_id::in, assert_id::in, module_info::in,
+:- pred update_pred_info(assert_id::in, pred_id::in, module_info::in,
module_info::out) is det.
-update_pred_info(PredId, AssertId, Module0, Module) :-
+update_pred_info(AssertId, PredId, Module0, Module) :-
module_info_pred_info(Module0, PredId, PredInfo0),
pred_info_get_assertions(PredInfo0, Assertions0),
set__insert(Assertions0, AssertId, Assertions),
pred_info_set_assertions(PredInfo0, Assertions, PredInfo),
module_info_set_pred_info(Module0, PredId, PredInfo, Module).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+ %
+ % assertion__normalise_goal
+ %
+ % Place a hlds_goal into a standard form. Currently all the
+ % code does is replace conj([G]) with G.
+ %
+:- pred assertion__normalise_goal(hlds_goal::in, hlds_goal::out) is det.
+
+assertion__normalise_goal(call(A,B,C,D,E,F) - GI, call(A,B,C,D,E,F) - GI).
+assertion__normalise_goal(generic_call(A,B,C,D) - GI, generic_call(A,B,C,D)-GI).
+assertion__normalise_goal(unify(A,B,C,D,E) - GI, unify(A,B,C,D,E) - GI).
+assertion__normalise_goal(pragma_c_code(A,B,C,D,E,F,G) - GI,
+ pragma_c_code(A,B,C,D,E,F,G) - GI).
+assertion__normalise_goal(conj(Goals0) - GI, conj(Goals) - GI) :-
+ assertion__normalise_conj(Goals0, Goals).
+assertion__normalise_goal(switch(A,B,Case0s,D) - GI, switch(A,B,Cases,D)-GI) :-
+ assertion__normalise_cases(Case0s, Cases).
+assertion__normalise_goal(disj(Goal0s,B) - GI, disj(Goals,B) - GI) :-
+ assertion__normalise_goals(Goal0s, Goals).
+assertion__normalise_goal(not(Goal0) - GI, not(Goal) - GI) :-
+ assertion__normalise_goal(Goal0, Goal).
+assertion__normalise_goal(some(A,B,Goal0) - GI, some(A,B,Goal) - GI) :-
+ assertion__normalise_goal(Goal0, Goal).
+assertion__normalise_goal(if_then_else(A, If0, Then0, Else0, E) - GI,
+ if_then_else(A, If, Then, Else, E) - GI) :-
+ assertion__normalise_goal(If0, If),
+ assertion__normalise_goal(Then0, Then),
+ assertion__normalise_goal(Else0, Else).
+assertion__normalise_goal(par_conj(Goal0s,B) - GI, par_conj(Goals,B) - GI) :-
+ assertion__normalise_goals(Goal0s, Goals).
+
+%-----------------------------------------------------------------------------%
+
+:- pred assertion__normalise_conj(hlds_goals::in, hlds_goals::out) is det.
+
+assertion__normalise_conj([], []).
+assertion__normalise_conj([Goal0 | Goal0s], Goals) :-
+ goal_to_conj_list(Goal0, ConjGoals),
+ assertion__normalise_conj(Goal0s, Goal1s),
+ list__append(ConjGoals, Goal1s, Goals).
+
+:- pred assertion__normalise_cases(list(case)::in, list(case)::out) is det.
+
+assertion__normalise_cases([], []).
+assertion__normalise_cases([Case0 | Case0s], [Case | Cases]) :-
+ Case0 = case(ConsId, Goal0),
+ assertion__normalise_goal(Goal0, Goal),
+ Case = case(ConsId, Goal),
+ assertion__normalise_cases(Case0s, Cases).
+
+:- pred assertion__normalise_goals(hlds_goals::in, hlds_goals::out) is det.
+
+assertion__normalise_goals([], []).
+assertion__normalise_goals([Goal0 | Goal0s], [Goal | Goals]) :-
+ assertion__normalise_goal(Goal0, Goal),
+ assertion__normalise_goals(Goal0s, Goals).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+assertion__in_interface_check(call(PredId,_,_,_,_,SymName) - GoalInfo,
+ ModuleInfo) -->
+ { module_info_pred_info(ModuleInfo, PredId, PredInfo) },
+ (
+ { pred_info_import_status(PredInfo, ImportStatus) },
+ { \+ is_defined_in_implementation_section(ImportStatus) }
+ ->
+ []
+ ;
+ { goal_info_get_context(GoalInfo, Context) },
+ { pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
+ { pred_info_arity(PredInfo, Arity) },
+ write_assertion_interface_error(Context,
+ call(PredOrFunc, SymName, Arity), ModuleInfo)
+ ).
+assertion__in_interface_check(generic_call(_,_,_,_) - _, _) --> [].
+assertion__in_interface_check(unify(_,RHS,_,_,_) - GoalInfo,
+ ModuleInfo) -->
+ { goal_info_get_context(GoalInfo, Context) },
+ assertion__in_interface_check_unify_rhs(RHS, Context, ModuleInfo).
+assertion__in_interface_check(pragma_c_code(_,PredId,_,_,_,_,_) - GoalInfo,
+ ModuleInfo) -->
+ { module_info_pred_info(ModuleInfo, PredId, PredInfo) },
+ (
+ { pred_info_import_status(PredInfo, ImportStatus) },
+ { \+ is_defined_in_implementation_section(ImportStatus) }
+ ->
+ []
+ ;
+ { goal_info_get_context(GoalInfo, Context) },
+ { pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
+ { pred_info_name(PredInfo, Name) },
+ { SymName = unqualified(Name) },
+ { pred_info_arity(PredInfo, Arity) },
+ write_assertion_interface_error(Context,
+ call(PredOrFunc, SymName, Arity), ModuleInfo)
+ ).
+assertion__in_interface_check(conj(Goals) - _, ModuleInfo) -->
+ assertion__in_interface_check_list(Goals, ModuleInfo).
+assertion__in_interface_check(switch(_,_,_,_) - _, _) -->
+ { error("assertion__in_interface_check: assertion contains switch.") }.
+assertion__in_interface_check(disj(Goals,_) - _, ModuleInfo) -->
+ assertion__in_interface_check_list(Goals, ModuleInfo).
+assertion__in_interface_check(not(Goal) - _, ModuleInfo) -->
+ assertion__in_interface_check(Goal, ModuleInfo).
+assertion__in_interface_check(some(_,_,Goal) - _, ModuleInfo) -->
+ assertion__in_interface_check(Goal, ModuleInfo).
+assertion__in_interface_check(if_then_else(_, If, Then, Else, _) - _,
+ ModuleInfo) -->
+ assertion__in_interface_check(If, ModuleInfo),
+ assertion__in_interface_check(Then, ModuleInfo),
+ assertion__in_interface_check(Else, ModuleInfo).
+assertion__in_interface_check(par_conj(Goals,_) - _, ModuleInfo) -->
+ assertion__in_interface_check_list(Goals, ModuleInfo).
+
+%-----------------------------------------------------------------------------%
+
+:- pred assertion__in_interface_check_unify_rhs(unify_rhs::in, prog_context::in,
+ module_info::in, io__state::di, io__state::uo) is det.
+
+assertion__in_interface_check_unify_rhs(var(_), _, _) --> [].
+assertion__in_interface_check_unify_rhs(functor(ConsId, _), Context,
+ ModuleInfo) -->
+ { module_info_ctors(ModuleInfo, ConsTable) },
+ { map__lookup(ConsTable, ConsId, Defns) },
+ (
+ { Defns = [hlds_cons_defn(_, _, _, TypeId, _)] }
+ ->
+
+ (
+ { module_info_types(ModuleInfo, Types) },
+ { map__lookup(Types, TypeId, TypeDefn) },
+ { hlds_data__get_type_defn_status(TypeDefn,
+ TypeStatus) },
+ { \+ is_defined_in_implementation_section(TypeStatus) }
+ ->
+ []
+ ;
+ write_assertion_interface_error(Context,
+ cons(ConsId), ModuleInfo)
+ )
+ ;
+ prog_out__write_context(Context),
+ io__write_string("In assertion:\n"),
+
+ prog_out__write_context(Context),
+ io__write_string(" ambiguity error: constructor `"),
+ hlds_out__write_cons_id(ConsId),
+ io__write_string("' appears in multiple types.\n"),
+
+ prog_out__write_context(Context),
+ io__write_string(" Possible matches occur in types\n"),
+
+ prog_out__write_context(Context),
+ io__write_string(" "),
+
+ { Map = (pred(Defn::in, TypeId::out) is det :-
+ Defn = hlds_cons_defn(_, _, _, TypeId, _)) },
+ { Print = (pred(TypeId::in, IO0::di, IO::uo) is det :-
+ TypeId = SymName - Arity,
+ prog_out__write_sym_name_and_arity(
+ SymName / Arity, IO0, IO)) },
+
+ { list__map(Map, Defns, Types) },
+ io__write_list(Types, ",", Print),
+ io__nl,
+
+ globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
+ (
+ { VerboseErrors = yes }
+ ->
+ prog_out__write_context(Context),
+ io__write_string(" Module qualifying the constructor"),
+ io__write_string(" will resolve the ambiguity\n"),
+
+ prog_out__write_context(Context),
+ io__write_string(" providing the types reside in"),
+ io__write_string(" different modules,\n"),
+
+ prog_out__write_context(Context),
+ io__write_string(" otherwise one constructor must"),
+ io__write_string(" be renamed.\n")
+ ;
+ []
+ )
+ ).
+assertion__in_interface_check_unify_rhs(lambda_goal(_,_,_,_,_,_,_,Goal),
+ _Context, ModuleInfo) -->
+ assertion__in_interface_check(Goal, ModuleInfo).
+
+%-----------------------------------------------------------------------------%
+
+:- pred assertion__in_interface_check_list(hlds_goals::in, module_info::in,
+ io__state::di, io__state::uo)is det.
+
+assertion__in_interface_check_list([], _) --> [].
+assertion__in_interface_check_list([Goal0 | Goal0s], ModuleInfo) -->
+ assertion__in_interface_check(Goal0, ModuleInfo),
+ assertion__in_interface_check_list(Goal0s, ModuleInfo).
+
+%-----------------------------------------------------------------------------%
+
+:- pred is_defined_in_implementation_section(import_status::in) is semidet.
+
+is_defined_in_implementation_section(abstract_exported).
+is_defined_in_implementation_section(exported_to_submodules).
+is_defined_in_implementation_section(local).
+
+%-----------------------------------------------------------------------------%
+
+:- type call_or_consid
+ ---> call(pred_or_func, sym_name, arity)
+ ; cons(cons_id).
+
+:- pred write_assertion_interface_error(prog_context::in,
+ call_or_consid::in, module_info::in,
+ io__state::di, io__state::uo) is det.
+
+write_assertion_interface_error(Context, Type, ModuleInfo) -->
+ { module_info_name(ModuleInfo, ModuleName) },
+ prog_out__write_context(Context),
+ io__write_string("In interface for module `"),
+ prog_out__write_sym_name(ModuleName),
+ io__write_string("':\n"),
+
+ prog_out__write_context(Context),
+ io__write_string(" error: exported assertion refers to "),
+ (
+ { Type = call(PredOrFunc, SymName, Arity) },
+ hlds_out__write_simple_call_id(PredOrFunc, SymName, Arity),
+ io__nl
+ ;
+ { Type = cons(ConsId) },
+ io__write_string("constructor `"),
+ hlds_out__write_cons_id(ConsId),
+ io__write_string("'\n")
+ ),
+
+ prog_out__write_context(Context),
+ io__write_string(" which is defined in the implementation "),
+ io__write_string("of module `"),
+ prog_out__write_sym_name(ModuleName),
+ io__write_string("'.\n"),
+
+ globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
+ (
+ { VerboseErrors = yes }
+ ->
+ prog_out__write_context(Context),
+ io__write_string(" Either move the assertion into the "),
+ io__write_string("implementation\n"),
+
+ prog_out__write_context(Context),
+ io__write_string(" or the definition into the interface.\n")
+ ;
+ []
+ ).
+
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
Index: compiler/dead_proc_elim.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/dead_proc_elim.m,v
retrieving revision 1.48
diff -u -r1.48 dead_proc_elim.m
--- dead_proc_elim.m 1999/07/13 08:52:46 1.48
+++ dead_proc_elim.m 1999/08/27 09:13:57
@@ -759,6 +759,9 @@
% variables from inst `free' to inst `any'.
string__remove_suffix(PredName, "_init_any", _),
PredArity = 1
+ ;
+ % Don't eliminate the clauses for assertions.
+ pred_info_get_goal_type(PredInfo, assertion)
)
->
set__insert(NeededNames0, qualified(PredModule, PredName),
Index: compiler/goal_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/goal_util.m,v
retrieving revision 1.54
diff -u -r1.54 goal_util.m
--- goal_util.m 1999/08/04 02:45:31 1.54
+++ goal_util.m 1999/08/17 05:54:03
@@ -124,6 +124,7 @@
% have not been determined.
:- pred goal_calls_pred_id(hlds_goal, pred_id).
:- mode goal_calls_pred_id(in, in) is semidet.
+:- mode goal_calls_pred_id(in, out) is nondet.
% Convert a switch back into a disjunction. This is needed
% for the magic set transformation.
@@ -752,6 +753,7 @@
:- pred goals_calls_pred_id(list(hlds_goal), pred_id).
:- mode goals_calls_pred_id(in, in) is semidet.
+:- mode goals_calls_pred_id(in, out) is nondet.
goals_calls_pred_id([Goal | Goals], PredId) :-
(
@@ -762,6 +764,7 @@
:- pred cases_calls_pred_id(list(case), pred_id).
:- mode cases_calls_pred_id(in, in) is semidet.
+:- mode cases_calls_pred_id(in, out) is nondet.
cases_calls_pred_id([case(_, Goal) | Cases], PredId) :-
(
@@ -772,6 +775,7 @@
:- pred goal_expr_calls_pred_id(hlds_goal_expr, pred_id).
:- mode goal_expr_calls_pred_id(in, in) is semidet.
+:- mode goal_expr_calls_pred_id(in, out) is nondet.
goal_expr_calls_pred_id(conj(Goals), PredId) :-
goals_calls_pred_id(Goals, PredId).
Index: compiler/hlds_data.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_data.m,v
retrieving revision 1.38
diff -u -r1.38 hlds_data.m
--- hlds_data.m 1999/07/14 04:17:11 1.38
+++ hlds_data.m 1999/08/26 08:20:44
@@ -833,6 +833,9 @@
:- pred assertion_table_lookup(assertion_table::in, assert_id::in,
pred_id::out) is det.
+:- pred assertion_table_pred_ids(assertion_table::in,
+ list(pred_id)::out) is det.
+
:- implementation.
:- import_module int.
@@ -852,6 +855,9 @@
assertion_table_lookup(AssertionTable, Id, Assertion) :-
AssertionTable = assertion_table(_MaxId, AssertionMap),
map__lookup(AssertionMap, Id, Assertion).
+
+assertion_table_pred_ids(assertion_table(_, AssertionMap), PredIds) :-
+ map__values(AssertionMap, PredIds).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
Index: compiler/hlds_goal.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_goal.m,v
retrieving revision 1.62
diff -u -r1.62 hlds_goal.m
--- hlds_goal.m 1999/07/13 08:52:57 1.62
+++ hlds_goal.m 1999/09/01 04:57:48
@@ -512,9 +512,10 @@
:- type unify_sub_contexts == list(unify_sub_context).
% A call_unify_context is used for unifications that get
- % turned into calls to out-of-line unification predicates.
- % It records which part of the original source code
- % the unification occurred in.
+ % turned into calls to out-of-line unification predicates,
+ % and functions. It records which part of the original source
+ % code the unification (which may be a function application)
+ % occurred in.
:- type call_unify_context
---> call_unify_context(
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_out.m,v
retrieving revision 1.224
diff -u -r1.224 hlds_out.m
--- hlds_out.m 1999/08/13 01:43:00 1.224
+++ hlds_out.m 1999/09/01 06:08:47
@@ -142,6 +142,12 @@
:- mode hlds_out__write_clauses(in, in, in, in, in, in, in, in, in, di, uo)
is det.
+:- pred hlds_out__write_assertion(int, module_info, pred_id, prog_varset, bool,
+ list(prog_var), pred_or_func, clause, vartypes,
+ io__state, io__state).
+:- mode hlds_out__write_assertion(in, in, in, in, in, in, in, in, in, di, uo)
+ is det.
+
% Print out an HLDS goal. The module_info and prog_varset give
% the context of the goal. The boolean says whether variables should
% have their numbers appended to them. The integer gives the level
@@ -815,6 +821,25 @@
{ hlds_out__marker_name(Marker, Name) },
io__write_string(Name).
+hlds_out__write_assertion(Indent, ModuleInfo, _PredId, VarSet, AppendVarnums,
+ HeadVars, _PredOrFunc, Clause, TypeQual) -->
+
+ % curry the varset for term_io__write_variable/4
+ { PrintVar = lambda([VarName::in, IO0::di, IO::uo] is det,
+ term_io__write_variable(VarName, VarSet, IO0, IO)
+ ) },
+
+ hlds_out__write_indent(Indent),
+ io__write_string(":- assertion all["),
+ io__write_list(HeadVars, ", ", PrintVar),
+ io__write_string("] (\n"),
+
+ { Clause = clause(_Modes, Goal, _Context) },
+ hlds_out__write_goal_a(Goal, ModuleInfo, VarSet, AppendVarnums,
+ Indent+1, ").\n", TypeQual).
+
+
+
hlds_out__write_clauses(Indent, ModuleInfo, PredId, VarSet, AppendVarnums,
HeadVars, PredOrFunc, Clauses0, TypeQual) -->
(
@@ -1369,14 +1394,34 @@
),
hlds_out__write_indent(Indent),
( { invalid_pred_id(PredId) } ->
- []
+ % If we don't know then the call must be treated
+ % as a predicate.
+ { PredOrFunc = predicate }
;
{ module_info_pred_info(ModuleInfo, PredId, PredInfo) },
{ pred_info_get_purity(PredInfo, Purity) },
+ { pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
write_purity_prefix(Purity)
),
- hlds_out__write_sym_name_and_args(PredName,
- ArgVars, VarSet, AppendVarnums),
+ (
+ { PredOrFunc = predicate },
+ { NewArgVars = ArgVars }
+ ;
+ { PredOrFunc = function },
+ (
+ { MaybeUnifyContext = yes(UnifyContext) },
+ { UnifyContext = call_unify_context(A, UnifyRHS, _) },
+ { UnifyRHS = functor(_ConsId, NewArgVars0) }
+ ->
+ { NewArgVars = NewArgVars0 },
+ mercury_output_var(A, VarSet, AppendVarnums),
+ io__write_string(" = ")
+ ;
+ { error("hlds_out: function without unify context") }
+ )
+ ),
+ hlds_out__write_sym_name_and_args(PredName, NewArgVars, VarSet,
+ AppendVarnums),
io__write_string(Follow),
( { string__contains_char(Verbose, 'l') } ->
{ pred_id_to_int(PredId, PredNum) },
Index: compiler/intermod.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/intermod.m,v
retrieving revision 1.68
diff -u -r1.68 intermod.m
--- intermod.m 1999/08/26 03:11:49 1.68
+++ intermod.m 1999/09/01 07:07:40
@@ -91,7 +91,10 @@
{ ModuleInfo = ModuleInfo0 }
;
{ Result2 = ok },
- { module_info_predids(ModuleInfo0, PredIds) },
+ { module_info_predids(ModuleInfo0, RealPredIds) },
+ { module_info_assertion_table(ModuleInfo0, AssertionTable) },
+ { assertion_table_pred_ids(AssertionTable, AssertPredIds) },
+ { list__append(AssertPredIds, RealPredIds, PredIds) },
{ init_intermod_info(ModuleInfo0, IntermodInfo0) },
globals__io_lookup_int_option(
intermod_inline_simple_threshold, Threshold),
@@ -170,50 +173,9 @@
{ module_info_type_spec_info(ModuleInfo0, TypeSpecInfo) },
{ TypeSpecInfo = type_spec_info(_, TypeSpecForcePreds, _, _) },
(
- %
- % note: we can't include exported_to_submodules predicates
- % in the `.opt' file, for reasons explained in
- % the comments for intermod_info_add_proc
- %
- { pred_info_is_exported(PredInfo0) },
- { pred_info_procids(PredInfo0, [ProcId | _ProcIds]) },
- { pred_info_procedures(PredInfo0, Procs) },
- { map__lookup(Procs, ProcId, ProcInfo) },
- { proc_info_goal(ProcInfo, Goal) },
- (
- % Don't export builtins since they will be
- % recreated in the importing module anyway.
- { \+ code_util__compiler_generated(PredInfo0) },
- { \+ code_util__predinfo_is_builtin(PredInfo0) },
-
- % These will be recreated in the importing module.
- { \+ set__member(PredId, TypeSpecForcePreds) },
- (
- { inlining__is_simple_goal(Goal,
- InlineThreshold) },
- { pred_info_get_markers(PredInfo0, Markers) },
- { \+ check_marker(Markers, no_inline) },
- { proc_info_eval_method(ProcInfo,
- eval_normal) }
- ;
- { pred_info_requested_inlining(PredInfo0) }
- ;
- { has_ho_input(ModuleInfo0, ProcInfo) }
- ;
- { Deforestation = yes },
- % Double the inline-threshold since
- % goals we want to deforest will have
- % at least two disjuncts. This allows
- % one simple goal in each disjunct.
- % The disjunction adds one to the goal
- % size, hence the `+1'.
- { DeforestThreshold is
- InlineThreshold * 2 + 1},
- { inlining__is_simple_goal(Goal,
- DeforestThreshold) },
- { goal_is_deforestable(PredId, Goal) }
- )
- )
+ { intermod__should_be_processed(PredId, PredInfo0,
+ TypeSpecForcePreds, InlineThreshold,
+ Deforestation, ModuleInfo0) }
->
=(IntermodInfo0),
{ pred_info_clauses_info(PredInfo0, ClausesInfo0) },
@@ -262,6 +224,61 @@
intermod__gather_preds(PredIds, CollectTypes,
InlineThreshold, Deforestation).
+
+:- pred intermod__should_be_processed(pred_id::in, pred_info::in,
+ set(pred_id)::in, int::in, bool::in,
+ module_info::in) is semidet.
+
+intermod__should_be_processed(PredId, PredInfo, TypeSpecForcePreds,
+ InlineThreshold, Deforestation, ModuleInfo) :-
+ %
+ % note: we can't include exported_to_submodules predicates in
+ % the `.opt' file, for reasons explained in the comments for
+ % intermod_info_add_proc
+ %
+ pred_info_is_exported(PredInfo),
+ (
+ pred_info_procids(PredInfo, [ProcId | _ProcIds]),
+ pred_info_procedures(PredInfo, Procs),
+ map__lookup(Procs, ProcId, ProcInfo),
+ proc_info_goal(ProcInfo, Goal),
+ (
+ % Don't export builtins since they will be
+ % recreated in the importing module anyway.
+ \+ code_util__compiler_generated(PredInfo),
+ \+ code_util__predinfo_is_builtin(PredInfo),
+
+ % These will be recreated in the importing module.
+ \+ set__member(PredId, TypeSpecForcePreds),
+ (
+ inlining__is_simple_goal(Goal, InlineThreshold),
+ pred_info_get_markers(PredInfo, Markers),
+ \+ check_marker(Markers, no_inline),
+ proc_info_eval_method(ProcInfo, eval_normal)
+ ;
+ pred_info_requested_inlining(PredInfo)
+ ;
+ has_ho_input(ModuleInfo, ProcInfo)
+ ;
+ Deforestation = yes,
+ % Double the inline-threshold since
+ % goals we want to deforest will have at
+ % least two disjuncts. This allows one
+ % simple goal in each disjunct. The
+ % disjunction adds one to the goal size,
+ % hence the `+1'.
+ DeforestThreshold is InlineThreshold * 2 + 1,
+ inlining__is_simple_goal(Goal,
+ DeforestThreshold),
+ goal_is_deforestable(PredId, Goal)
+ )
+ )
+ ;
+ % assertions that are in the interface should always get
+ % included in the .opt file.
+ pred_info_get_goal_type(PredInfo, assertion)
+ ).
+
:- pred dcg_set(T::in, T::unused, T::out) is det.
dcg_set(T, _, T).
@@ -1127,6 +1144,18 @@
{ pred_info_procedures(PredInfo, Procs) },
intermod__write_c_code(SymName, PredOrFunc, HeadVars, VarSet,
Clauses, Procs)
+ ;
+ { pred_info_get_goal_type(PredInfo, assertion) }
+ ->
+ (
+ { Clauses = [Clause] }
+ ->
+ hlds_out__write_assertion(0, ModuleInfo, PredId,
+ VarSet, no, HeadVars, PredOrFunc,
+ Clause, no)
+ ;
+ { error("intermod__write_preds: assertion not a single clause.") }
+ )
;
% { pred_info_typevarset(PredInfo, TVarSet) },
hlds_out__write_clauses(1, ModuleInfo, PredId, VarSet, no,
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/make_hlds.m,v
retrieving revision 1.301
diff -u -r1.301 make_hlds.m
--- make_hlds.m 1999/08/31 05:25:33 1.301
+++ make_hlds.m 1999/09/01 06:38:48
@@ -2748,11 +2748,40 @@
preds_add_implicit(ModuleInfo, PredicateTable0, ModuleName, PredName, Arity,
Status, Context, PredOrFunc, PredId, PredicateTable) :-
+ clauses_info_init(Arity, ClausesInfo),
+ preds_add_implicit_2(ClausesInfo, ModuleInfo, PredicateTable0,
+ ModuleName, PredName, Arity, Status, Context,
+ PredOrFunc, PredId, PredicateTable).
+
+:- pred preds_add_implicit_for_assertion(prog_vars, module_info,
+ predicate_table, module_name, sym_name, arity,
+ import_status, prog_context, pred_or_func,
+ pred_id, predicate_table).
+:- mode preds_add_implicit_for_assertion(in, in, in,
+ in, in, in, in, in, in, out, out) is det.
+
+preds_add_implicit_for_assertion(HeadVars,
+ ModuleInfo, PredicateTable0, ModuleName,
+ PredName, Arity, Status, Context,
+ PredOrFunc, PredId, PredicateTable) :-
+ clauses_info_init_for_assertion(HeadVars, ClausesInfo),
+ preds_add_implicit_2(ClausesInfo, ModuleInfo, PredicateTable0,
+ ModuleName, PredName, Arity, Status, Context,
+ PredOrFunc, PredId, PredicateTable).
+
+:- pred preds_add_implicit_2(clauses_info, module_info, predicate_table,
+ module_name, sym_name, arity, import_status, prog_context,
+ pred_or_func, pred_id, predicate_table).
+:- mode preds_add_implicit_2(in, in, in,
+ in, in, in, in, in, in, out, out) is det.
+
+preds_add_implicit_2(ClausesInfo, ModuleInfo, PredicateTable0, ModuleName,
+ PredName, Arity, Status, Context,
+ PredOrFunc, PredId, PredicateTable) :-
varset__init(TVarSet0),
make_n_fresh_vars("T", Arity, TVarSet0, TypeVars, TVarSet),
term__var_list_to_term_list(TypeVars, Types),
Cond = true,
- clauses_info_init(Arity, ClausesInfo),
map__init(Proofs),
% The class context is empty since this is an implicit
% definition. Inference will fill it in.
@@ -2898,16 +2927,22 @@
(
% An assertion will not have a
% corresponding pred declaration.
- { IsAssertion = yes }
+ { IsAssertion = yes },
+ { term__term_list_to_var_list(Args, HeadVars) },
+ { preds_add_implicit_for_assertion(HeadVars,
+ ModuleInfo0, PredicateTable0,
+ ModuleName, PredName, Arity, Status,
+ Context, PredOrFunc,
+ PredId, PredicateTable1) }
;
{ IsAssertion = no },
maybe_undefined_pred_error(PredName, Arity, PredOrFunc,
- Context, "clause")
- ),
- { preds_add_implicit(ModuleInfo0, PredicateTable0,
- ModuleName, PredName, Arity, Status, Context,
- PredOrFunc,
- PredId, PredicateTable1) }
+ Context, "clause"),
+ { preds_add_implicit(ModuleInfo0, PredicateTable0,
+ ModuleName, PredName, Arity, Status,
+ Context, PredOrFunc,
+ PredId, PredicateTable1) }
+ )
),
% Lookup the pred_info for this pred,
% add the clause to the clauses_info in the pred_info,
@@ -4341,6 +4376,17 @@
%-----------------------------------------------------------------------------
+:- pred clauses_info_init_for_assertion(prog_vars::in,
+ clauses_info::out) is det.
+
+clauses_info_init_for_assertion(HeadVars, ClausesInfo) :-
+ map__init(VarTypes),
+ varset__init(VarSet),
+ map__init(TI_VarMap),
+ map__init(TCI_VarMap),
+ ClausesInfo = clauses_info(VarSet, VarTypes, VarTypes, HeadVars, [],
+ TI_VarMap, TCI_VarMap).
+
clauses_info_init(Arity, ClausesInfo) :-
map__init(VarTypes),
varset__init(VarSet0),
@@ -4461,8 +4507,6 @@
Goal, VarSet, Warnings, Module0, Module, Info0, Info) -->
transform_goal(Body, VarSet0, Subst, Goal1, VarSet1, Info0, Info1),
{ term__apply_substitution_to_list(Args0, Subst, Args) },
- insert_arg_unifications(HeadVars, Args, Context, head, no,
- Goal1, VarSet1, Goal2, VarSet2, Info1, Info),
{ map__init(Empty) },
%
@@ -4470,15 +4514,21 @@
% explicitly quantified, as it has not been determined
% what the correct implicit quantification should be for
% assertions.
+ % Also the head variables of an assertion will always be
+ % variables, so it is unecessary to insert unifications.
%
(
{ IsAssertion = yes }
->
- % Use Goal1, since HeadVar__* not yet introduced.
- report_implicit_quant_errs(Goal1, Args, VarSet0,
- Context, Module0, Module)
+ report_implicit_quant_errs(Goal1, Args, VarSet1,
+ Context, Module0, Module),
+ { VarSet2 = VarSet1 },
+ { Goal2 = Goal1 },
+ { Info = Info0 }
;
- { Module = Module0 }
+ { Module = Module0 },
+ insert_arg_unifications(HeadVars, Args, Context, head, no,
+ Goal1, VarSet1, Goal2, VarSet2, Info1, Info)
),
{ implicitly_quantify_clause_body(HeadVars, Goal2, VarSet2, Empty,
Goal, VarSet, _, Warnings) }.
Index: compiler/modules.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/modules.m,v
retrieving revision 1.107
diff -u -r1.107 modules.m
--- modules.m 1999/08/18 06:26:04 1.107
+++ modules.m 1999/08/31 08:58:21
@@ -738,13 +738,16 @@
;
%
% Strip out the imported interfaces,
+ % assertions are also striped since they should
+ % only be written to .opt files,
% check for some warnings, and then
% write out the `.int' and `int2' files
% and touch the `.date' file.
%
{ strip_imported_items(InterfaceItems2, [],
InterfaceItems3) },
- check_for_clauses_in_interface(InterfaceItems3,
+ { strip_assertions(InterfaceItems3, InterfaceItems4) },
+ check_for_clauses_in_interface(InterfaceItems4,
InterfaceItems),
check_int_for_no_exports(InterfaceItems, ModuleName),
write_interface_file(ModuleName, ".int",
@@ -761,7 +764,10 @@
% information in the current module and writes out the .int3 file.
make_short_interface(ModuleName, Items0) -->
{ get_interface(Items0, no, InterfaceItems0) },
- check_for_clauses_in_interface(InterfaceItems0, InterfaceItems),
+ % assertions are also striped since they should
+ % only be written to .opt files,
+ { strip_assertions(InterfaceItems0, InterfaceItems1) },
+ check_for_clauses_in_interface(InterfaceItems1, InterfaceItems),
{ get_short_interface(InterfaceItems, ShortInterfaceItems0) },
module_qual__module_qualify_items(ShortInterfaceItems0,
ShortInterfaceItems, ModuleName, no, _, _, _, _),
@@ -782,6 +788,20 @@
list__reverse(Items0, Items)
;
strip_imported_items(Rest, [Item - Context | Items0], Items)
+ ).
+
+:- pred strip_assertions(item_list::in, item_list::out) is det.
+
+strip_assertions([], []).
+strip_assertions([Item - Context | Rest], Items) :-
+ (
+ Item = assertion(_, _)
+ ->
+ strip_assertions(Rest, Items)
+ ;
+ strip_assertions(Rest, Items0),
+ Items = [Item - Context | Items0]
+
).
:- pred check_for_clauses_in_interface(item_list, item_list,
Index: compiler/polymorphism.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/polymorphism.m,v
retrieving revision 1.169
diff -u -r1.169 polymorphism.m
--- polymorphism.m 1999/08/26 07:17:37 1.169
+++ polymorphism.m 1999/09/01 06:17:50
@@ -1256,102 +1256,6 @@
map__lookup(VarTypes0, X0, TypeOfX),
list__length(ArgVars0, Arity),
(
- %
- % is the function symbol apply/N or ''/N,
- % representing a higher-order function call?
- %
- ConsId0 = cons(unqualified(ApplyName), _),
- ( ApplyName = "apply" ; ApplyName = "" ),
- Arity >= 1,
- ArgVars0 = [FuncVar | FuncArgVars]
- ->
- %
- % Convert the higher-order function call (apply/N)
- % into a higher-order predicate call
- % (i.e., replace `X = apply(F, A, B, C)'
- % with `call(F, A, B, C, X)')
- %
- list__append(FuncArgVars, [X0], ArgVars),
- Modes = [],
- Det = erroneous,
- adjust_func_arity(function, Arity, FullArity),
- HOCall = generic_call(
- higher_order(FuncVar, function, FullArity),
- ArgVars, Modes, Det),
-
- /*******
- %
- % Currently we don't support higher-order polymorphism;
- % all closures are monomorphic (any type_infos needed are
- % supplied when the closure is created, not when it is called).
- % Therefore we don't need to bother recursively processing
- % the higher-order function call. If we were to ever add
- % support for higher-order polymorphism, then we would need
- % to uncomment this code.
- %
- polymorphism__process_goal_expr(HOCall, GoalInfo0, Goal,
- PolyInfo0, PolyInfo)
- ********/
- Goal = HOCall - GoalInfo0,
- PolyInfo = PolyInfo0
- ;
- %
- % is the function symbol a user-defined function, rather
- % than a functor which represents a data constructor?
- %
-
- % Find the set of candidate predicates which have the
- % specified name and arity (and module, if module-qualified)
- ConsId0 = cons(PredName, _),
-
- %
- % We don't do this for compiler-generated predicates;
- % they are assumed to have been generated with all
- % functions already expanded.
- % If we did this check for compiler-generated
- % predicates, it would cause the wrong behaviour
- % in the case where there is a user-defined function
- % whose type is exactly the same as the type of
- % a constructor. (Normally that would cause
- % a type ambiguity error, but compiler-generated
- % predicates are not type-checked.)
- %
- poly_info_get_pred_info(PolyInfo0, PredInfo),
- \+ code_util__compiler_generated(PredInfo),
-
- module_info_get_predicate_table(ModuleInfo0, PredTable),
- predicate_table_search_func_sym_arity(PredTable,
- PredName, Arity, PredIds),
-
- % Check if any of the candidate functions have
- % argument/return types which subsume the actual
- % argument/return types of this function call
-
- poly_info_get_typevarset(PolyInfo0, TVarSet),
- map__apply_to_list(ArgVars0, VarTypes0, ArgTypes0),
- list__append(ArgTypes0, [TypeOfX], ArgTypes),
- typecheck__find_matching_pred_id(PredIds, ModuleInfo0,
- TVarSet, ArgTypes, PredId, QualifiedFuncName)
- ->
- %
- % Convert function calls into predicate calls:
- % replace `X = f(A, B, C)'
- % with `f(A, B, C, X)'
- %
- invalid_proc_id(ProcId),
- list__append(ArgVars0, [X0], ArgVars),
- FuncCallUnifyContext = call_unify_context(X0,
- functor(ConsId0, ArgVars0), UnifyContext),
- FuncCall = call(PredId, ProcId, ArgVars, not_builtin,
- yes(FuncCallUnifyContext), QualifiedFuncName),
-
- %
- % now process it
- %
- polymorphism__process_goal_expr(FuncCall, GoalInfo0, Goal,
- PolyInfo0, PolyInfo)
- ;
-
%
% We replace any unifications with higher-order pred constants
% by lambda expressions. For example, we replace
Index: compiler/post_typecheck.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/post_typecheck.m,v
retrieving revision 1.13
diff -u -r1.13 post_typecheck.m
--- post_typecheck.m 1999/08/31 05:25:36 1.13
+++ post_typecheck.m 1999/09/02 00:58:58
@@ -11,11 +11,7 @@
% This module does the final parts of type analysis:
%
% - it resolves predicate overloading
-% (perhaps it ought to also resolve function overloading,
-% converting unifications that are function calls into
-% HLDS call instructions, but currently that is done
-% in polymorphism.m)
-%
+% - it resolves function overloading
% - it checks for unbound type variables and if there are any,
% it reports an error (or a warning, binding them to the type `void').
%
@@ -100,14 +96,14 @@
% remove it from further processing and store it in the
% assertion_table.
:- pred post_typecheck__finish_assertion(module_info, pred_id,
- module_info) is det.
-:- mode post_typecheck__finish_assertion(in, in, out) is det.
+ module_info, io__state, io__state) is det.
+:- mode post_typecheck__finish_assertion(in, in, out, di, uo) is det.
%-----------------------------------------------------------------------------%
:- implementation.
-:- import_module (assertion), typecheck, clause_to_proc.
+:- import_module (assertion), code_util, typecheck, clause_to_proc.
:- import_module mode_util, inst_match, (inst).
:- import_module mercury_to_mercury, prog_out, hlds_data, hlds_out, type_util.
:- import_module globals, options.
@@ -572,7 +568,9 @@
%
post_typecheck__finish_pred(ModuleInfo, PredId, PredInfo0, PredInfo) -->
post_typecheck__propagate_types_into_modes(ModuleInfo, PredId,
- PredInfo0, PredInfo).
+ PredInfo0, PredInfo1),
+ { post_typecheck__resolve_func_overloading(PredInfo1, ModuleInfo,
+ PredInfo) }.
%
% For ill-typed preds, we just need to set the modes up correctly
@@ -594,24 +592,41 @@
PredInfo0, PredInfo).
%
- % Remove the assertion from the list of pred ids to be processed
- % in the future and place the pred_info associated with the
+ % Now that the assertion has finished being typechecked,
+ % and has had all of its pred_ids identified,
+ % remove the assertion from the list of pred ids to be processed
+ % in the future and place the pred_id associated with the
% assertion into the assertion table.
- % Also records for each predicate that is used in an assertion
+ % For each assertion that is in the interface, you need to check
+ % that it doesn't refer to any symbols which are local to that
+ % module.
+ % Also record for each predicate that is used in an assertion
% which assertion it is used in.
%
-post_typecheck__finish_assertion(Module0, PredId, Module) :-
+post_typecheck__finish_assertion(Module0, PredId, Module) -->
% store into assertion table.
- module_info_assertion_table(Module0, AssertTable0),
- assertion_table_add_assertion(PredId, AssertTable0, Id, AssertTable),
- module_info_set_assertion_table(Module0, AssertTable, Module1),
+ { module_info_assertion_table(Module0, AssertTable0) },
+ { assertion_table_add_assertion(PredId,
+ AssertTable0, AssertionId, AssertTable) },
+ { module_info_set_assertion_table(Module0, AssertTable, Module1) },
% Remove from further processing.
- module_info_remove_predid(Module1, PredId, Module2),
+ { module_info_remove_predid(Module1, PredId, Module2) },
+ % If the assertion is in the interface, then ensure that
+ % it doesn't refer to any local symbols.
+ { module_info_pred_info(Module2, PredId, PredInfo) },
+ { assertion__goal(AssertionId, Module2, Goal) },
+ (
+ { pred_info_is_exported(PredInfo) }
+ ->
+ assertion__in_interface_check(Goal, Module2)
+ ;
+ []
+ ),
+
% record which predicates are used in assertions
- assertion__goal(Id, Module2, Goal),
- assertion__record_preds_used_in(Goal, Id, Module2, Module).
+ { assertion__record_preds_used_in(Goal, AssertionId, Module2, Module) }.
%
@@ -716,4 +731,240 @@
prog_out__write_context(Context),
io__write_string(" with multiple `aditi:state' arguments.\n").
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+ %
+ % post_typecheck__resolve_func_overloading
+ %
+ % Convert unifications that are function calls into HLDS call
+ % instructions.
+ %
+:- pred post_typecheck__resolve_func_overloading(pred_info::in,
+ module_info::in, pred_info::out) is det.
+
+post_typecheck__resolve_func_overloading(PredInfo0, ModuleInfo, PredInfo) :-
+
+ pred_info_clauses_info(PredInfo0, ClausesInfo0),
+ clauses_info_clauses(ClausesInfo0, Clauses0),
+
+ list__map(post_typecheck__resolve_func_overloading_clauses(PredInfo0,
+ ModuleInfo),
+ Clauses0, Clauses),
+
+ clauses_info_set_clauses(ClausesInfo0, Clauses, ClausesInfo),
+ pred_info_set_clauses_info(PredInfo0, ClausesInfo, PredInfo).
+
+:- pred post_typecheck__resolve_func_overloading_clauses(pred_info::in,
+ module_info::in, clause::in, clause::out) is det.
+
+post_typecheck__resolve_func_overloading_clauses(PredInfo, ModuleInfo,
+ Clause0, Clause) :-
+ Clause0 = clause(ProcIds, Goal0, Context),
+ post_typecheck__resolve_data_cons_and_funcs(Goal0, ModuleInfo,
+ PredInfo, Goal),
+ Clause = clause(ProcIds, Goal, Context).
+
+%-----------------------------------------------------------------------------%
+
+ %
+ % post_typecheck__resolve_data_cons_and_funcs
+ %
+ % Traverse the hlds_goal structure transforming the unifications
+ % that are function application into the correct calls.
+ %
+:- pred post_typecheck__resolve_data_cons_and_funcs(hlds_goal::in,
+ module_info::in, pred_info::in,
+ hlds_goal::out) is det.
+
+post_typecheck__resolve_data_cons_and_funcs(
+ unify(XVar, Y, Mode, Unification, UnifyContext) - GoalInfo,
+ ModuleInfo, PredInfo, Goal) :-
+ (
+ Y = functor(ConsId, Args),
+ post_typecheck__resolve_unify_functor(XVar, ConsId,
+ Args, Mode, Unification, UnifyContext,
+ GoalInfo, ModuleInfo, PredInfo, Goal)
+ ;
+ Y = lambda_goal(A, B, C, D, E, F, G, LambdaGoal0),
+ post_typecheck__resolve_data_cons_and_funcs(LambdaGoal0,
+ ModuleInfo, PredInfo, LambdaGoal),
+ NewY = lambda_goal(A, B, C, D, E, F, G, LambdaGoal),
+ Goal = unify(XVar, NewY, Mode, Unification, UnifyContext)
+ - GoalInfo
+ ;
+ Y = var(_),
+ Goal = unify(XVar, Y, Mode, Unification, UnifyContext)
+ - GoalInfo
+ ).
+
+ % Goals which simply traverse the hlds_goal structure.
+post_typecheck__resolve_data_cons_and_funcs(call(A,B,C,D,E,F) - GoalInfo,
+ _, _, call(A,B,C,D,E,F) - GoalInfo).
+post_typecheck__resolve_data_cons_and_funcs(generic_call(A,B,C,D) - GoalInfo,
+ _, _, generic_call(A,B,C,D) - GoalInfo).
+post_typecheck__resolve_data_cons_and_funcs(pragma_c_code(A,B,C,D,E,F,G) -
+ GoalInfo, _, _, pragma_c_code(A,B,C,D,E,F,G) - GoalInfo).
+post_typecheck__resolve_data_cons_and_funcs(conj(Goals0) - GoalInfo,
+ ModuleInfo, PredInfo, conj(Goals) - GoalInfo) :-
+ post_typecheck__resolve_data_cons_and_funcs_list(Goals0,
+ ModuleInfo, PredInfo, Goals).
+post_typecheck__resolve_data_cons_and_funcs(switch(A,B,Cases0,D) - GoalInfo,
+ ModuleInfo, PredInfo,
+ switch(A,B,Cases,D) - GoalInfo) :-
+ post_typecheck__resolve_data_cons_and_funcs_cases(Cases0,
+ ModuleInfo, PredInfo, Cases).
+post_typecheck__resolve_data_cons_and_funcs(disj(Goals0,B) - GoalInfo,
+ ModuleInfo, PredInfo, disj(Goals,B) - GoalInfo) :-
+ post_typecheck__resolve_data_cons_and_funcs_list(Goals0,
+ ModuleInfo, PredInfo, Goals).
+post_typecheck__resolve_data_cons_and_funcs(not(Goal0) - GoalInfo,
+ ModuleInfo, PredInfo, not(Goal) - GoalInfo) :-
+ post_typecheck__resolve_data_cons_and_funcs(Goal0,
+ ModuleInfo, PredInfo, Goal).
+post_typecheck__resolve_data_cons_and_funcs(some(A,B,Goal0) - GoalInfo,
+ ModuleInfo, PredInfo, some(A,B,Goal) - GoalInfo) :-
+ post_typecheck__resolve_data_cons_and_funcs(Goal0,
+ ModuleInfo, PredInfo, Goal).
+post_typecheck__resolve_data_cons_and_funcs(par_conj(Goals0,B) - GoalInfo,
+ ModuleInfo, PredInfo, par_conj(Goals,B) - GoalInfo) :-
+ post_typecheck__resolve_data_cons_and_funcs_list(Goals0,
+ ModuleInfo, PredInfo, Goals).
+post_typecheck__resolve_data_cons_and_funcs(if_then_else(A,If0,Then0,Else0,E)
+ - GoalInfo, ModuleInfo, PredInfo,
+ if_then_else(A,If,Then,Else,E) - GoalInfo) :-
+ post_typecheck__resolve_data_cons_and_funcs(If0,
+ ModuleInfo, PredInfo, If),
+ post_typecheck__resolve_data_cons_and_funcs(Then0,
+ ModuleInfo, PredInfo, Then),
+ post_typecheck__resolve_data_cons_and_funcs(Else0,
+ ModuleInfo, PredInfo, Else).
+
+:- pred post_typecheck__resolve_data_cons_and_funcs_list(list(hlds_goal)::in,
+ module_info::in, pred_info::in, list(hlds_goal)::out) is det.
+
+post_typecheck__resolve_data_cons_and_funcs_list([], _, _, []).
+post_typecheck__resolve_data_cons_and_funcs_list([Goal0 | Goal0s],
+ ModuleInfo, PredInfo, [Goal | Goals]) :-
+ post_typecheck__resolve_data_cons_and_funcs(Goal0,
+ ModuleInfo, PredInfo, Goal),
+ post_typecheck__resolve_data_cons_and_funcs_list(Goal0s,
+ ModuleInfo, PredInfo, Goals).
+
+:- pred post_typecheck__resolve_data_cons_and_funcs_cases(list(case)::in,
+ module_info::in, pred_info::in, list(case)::out) is det.
+
+post_typecheck__resolve_data_cons_and_funcs_cases([], _, _, []).
+post_typecheck__resolve_data_cons_and_funcs_cases([Case0 | Case0s],
+ ModuleInfo, PredInfo, [Case | Cases]) :-
+ Case0 = case(ConsId, Goal0),
+ post_typecheck__resolve_data_cons_and_funcs(Goal0,
+ ModuleInfo, PredInfo, Goal),
+ Case = case(ConsId, Goal),
+ post_typecheck__resolve_data_cons_and_funcs_cases(Case0s,
+ ModuleInfo, PredInfo, Cases).
+
+%-----------------------------------------------------------------------------%
+
+:- pred post_typecheck__resolve_unify_functor(prog_var, cons_id, list(prog_var),
+ unify_mode, unification, unify_context, hlds_goal_info,
+ module_info, pred_info, hlds_goal).
+:- mode post_typecheck__resolve_unify_functor(in, in, in, in, in, in,
+ in, in, in, out) is det.
+
+post_typecheck__resolve_unify_functor(X0, ConsId0, ArgVars0, Mode0,
+ Unification0, UnifyContext, GoalInfo0,
+ ModuleInfo0, PredInfo, Goal) :-
+
+ pred_info_clauses_info(PredInfo, ClausesInfo),
+ clauses_info_vartypes(ClausesInfo, VarTypes0),
+
+ map__lookup(VarTypes0, X0, TypeOfX),
+ list__length(ArgVars0, Arity),
+ (
+ %
+ % is the function symbol apply/N or ''/N,
+ % representing a higher-order function call?
+ %
+ ConsId0 = cons(unqualified(ApplyName), _),
+ ( ApplyName = "apply" ; ApplyName = "" ),
+ Arity >= 1,
+ ArgVars0 = [FuncVar | FuncArgVars]
+ ->
+ %
+ % Convert the higher-order function call (apply/N)
+ % into a higher-order predicate call
+ % (i.e., replace `X = apply(F, A, B, C)'
+ % with `call(F, A, B, C, X)')
+ %
+ list__append(FuncArgVars, [X0], ArgVars),
+ Modes = [],
+ Det = erroneous,
+ adjust_func_arity(function, Arity, FullArity),
+ HOCall = generic_call(
+ higher_order(FuncVar, function, FullArity),
+ ArgVars, Modes, Det),
+
+ Goal = HOCall - GoalInfo0
+ ;
+ %
+ % is the function symbol a user-defined function, rather
+ % than a functor which represents a data constructor?
+ %
+
+ % Find the set of candidate predicates which have the
+ % specified name and arity (and module, if module-qualified)
+ ConsId0 = cons(PredName, _),
+
+ %
+ % We don't do this for compiler-generated predicates;
+ % they are assumed to have been generated with all
+ % functions already expanded.
+ % If we did this check for compiler-generated
+ % predicates, it would cause the wrong behaviour
+ % in the case where there is a user-defined function
+ % whose type is exactly the same as the type of
+ % a constructor. (Normally that would cause
+ % a type ambiguity error, but compiler-generated
+ % predicates are not type-checked.)
+ %
+ \+ code_util__compiler_generated(PredInfo),
+
+ module_info_get_predicate_table(ModuleInfo0, PredTable),
+ predicate_table_search_func_sym_arity(PredTable,
+ PredName, Arity, PredIds),
+
+ % Check if any of the candidate functions have
+ % argument/return types which subsume the actual
+ % argument/return types of this function call
+
+ pred_info_typevarset(PredInfo, TVarSet),
+ map__apply_to_list(ArgVars0, VarTypes0, ArgTypes0),
+ list__append(ArgTypes0, [TypeOfX], ArgTypes),
+ typecheck__find_matching_pred_id(PredIds, ModuleInfo0,
+ TVarSet, ArgTypes, PredId, QualifiedFuncName)
+ ->
+ %
+ % Convert function calls into predicate calls:
+ % replace `X = f(A, B, C)'
+ % with `f(A, B, C, X)'
+ %
+ invalid_proc_id(ProcId),
+ list__append(ArgVars0, [X0], ArgVars),
+ FuncCallUnifyContext = call_unify_context(X0,
+ functor(ConsId0, ArgVars0), UnifyContext),
+ FuncCall = call(PredId, ProcId, ArgVars, not_builtin,
+ yes(FuncCallUnifyContext), QualifiedFuncName),
+
+ Goal = FuncCall - GoalInfo0
+ ;
+ %
+ % ordinary construction/deconstruction unifications
+ % we leave alone
+ %
+ Goal = unify(X0, functor(ConsId0, ArgVars0), Mode0,
+ Unification0, UnifyContext) - GoalInfo0
+ ).
+
+%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
Index: compiler/purity.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/purity.m,v
retrieving revision 1.18
diff -u -r1.18 purity.m
--- purity.m 1999/07/29 07:51:47 1.18
+++ purity.m 1999/09/01 06:36:37
@@ -294,8 +294,8 @@
(
{ pred_info_get_goal_type(PredInfo0, assertion) }
->
- { post_typecheck__finish_assertion(ModuleInfo1,
- PredId, ModuleInfo2) }
+ post_typecheck__finish_assertion(ModuleInfo1,
+ PredId, ModuleInfo2)
;
{ ModuleInfo2 = ModuleInfo1 }
),
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/reference_manual.texi,v
retrieving revision 1.151
diff -u -r1.151 reference_manual.texi
--- reference_manual.texi 1999/08/31 05:01:33 1.151
+++ reference_manual.texi 1999/09/02 07:58:14
@@ -49,6 +49,7 @@
@author Peter Schachte
@author Simon Taylor
@author Chris Speirs
+ at author Peter Ross
@page
@vskip 0pt plus 1filll
Copyright @copyright{} 1995-1999 The University of Melbourne.
@@ -82,6 +83,8 @@
safely use destructive update to modify that value.
* Determinism:: Determinism declarations let you specify that a predicate
should never fail or should never succeed more than once.
+* Assertions:: Assertion declarations allow you to declare laws
+ that hold.
* Equality preds:: User-defined types can have user-defined equality
predicates.
* Higher-order:: Mercury supports higher-order predicates and functions,
@@ -366,6 +369,7 @@
:- typeclass
:- instance
:- pragma
+:- assertion
:- module
:- interface
:- implementation
@@ -2157,6 +2161,46 @@
And there are a variety of other applications.
@c XXX fix semantics for I/O + committed choice + mode inference
+
+ at node Assertions
+ at chapter Assertions
+
+Mercury supports the declaration of laws that hold for predicates and
+functions.
+These laws are only checked for type-correctness,
+it is the responsibility of the programmer to ensure overall correctness.
+The behaviour of programs with incorrect laws is undefined.
+
+A new law is introduced with the @samp{:- assertion} declaration.
+
+Here are some examples of @samp{:- assertion} declarations.
+The following example declares the function @samp{+} to be commutative.
+
+ at example
+:- assertion
+ all [A,B,R] (
+ R = A + B
+ <=>
+ R = B + A
+ ).
+ at end example
+
+Note that each variable in the declaration was explicitly quantified.
+The current Mercury compiler requires that each assertion begins with
+an @samp{all} quantification, and that every variable is explicitly
+quantified.
+
+Here is a more complicated declaration. It declares that @samp{append} is
+associative.
+
+ at example
+:- assertion
+ all [A,B,C,ABC] (
+ (some [AB] (append(A, B, AB), append(AB, C, ABC)))
+ <=>
+ (some [BC] (append(B, C, BC), append(A, BC, ABC)))
+ ).
+ at end example
@node Equality preds
@chapter User-defined equality predicates
Index: doc/transition_guide.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/transition_guide.texi,v
retrieving revision 1.29
diff -u -r1.29 transition_guide.texi
--- transition_guide.texi 1999/08/04 06:19:46 1.29
+++ transition_guide.texi 1999/08/17 05:54:33
@@ -149,6 +149,7 @@
aditi_top_down fx 500
all fxy 950
and xfy 720
+assertion fx 1199
div yfx 400
else xfy 1170
end_module fx 1199
Index: library/int.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/library/int.m,v
retrieving revision 1.57
diff -u -r1.57 int.m
--- int.m 1999/07/07 15:19:38 1.57
+++ int.m 1999/07/30 01:49:57
@@ -72,6 +72,9 @@
:- mode uo + in = in is det.
:- mode in + uo = in is det.
+ % commutativity of +
+:- assertion all [A,B,C] ( C = B + A <=> C = A + B ).
+
% multiplication
:- func int * int = int.
:- mode in * in = uo is det.
@@ -82,6 +85,8 @@
:- mode uo * in = in is semidet.
:- mode in * uo = in is semidet.
*/
+ % commutativity of *
+:- assertion all [A,B,C] ( C = B * A <=> C = A * B ).
% subtraction
:- func int - int = int.
cvs [diff aborted]: there is no version here; do 'cvs checkout' first
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to: mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions: mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------
More information about the developers
mailing list