[m-dev.] for review: more assertion integration
Peter Ross
petdr at cs.mu.OZ.AU
Mon Aug 30 14:37:20 AEST 1999
Hi,
This is for dmo to review.
Pete.
===================================================================
Estimated hours taken: 40
More integration of assertions with the compiler.
compiler/accumulator.m:
Use the new assertion__is_commutative predicate.
compiler/assertion.m:
Add assertion__is_commutative, which given an assertion_id returns
whether or not the assertion is commutative.
Rewrite assertion__record_preds_used_in so that it is more simple.
Add assertion__check_exported, which ensures that an assertion which
is defined in the interface only refers to constructors, functions
and predicates defined in that interface.
compiler/dead_proc_elim.m:
Don't eliminate the clauses for assertions.
compiler/goal_util.m:
Add the mode (in, out) to goal_calls_pred_id.
compiler/hlds_data.m:
Add assertion_table_pred_ids, which returns all the predids of every
assertion.
compiler/hlds_out.m:
Add hlds_out__write_assertion, which will write an assertion.
compiler/intermod.m:
Ensure that assertions defined in the interface, get written out to
the .opt file.
compiler/make_hlds.m:
When adding an assertion add an implicit pred declaration.
compiler/modules.m:
Discard assertions so that they are not written out in interface files.
compiler/polymorphism.m:
Remove assertions from futher processing after the polymorphism
pass.
compiler/post_typecheck.m:
compiler/purity.m:
Don't remove assertions after typechecking as polymorphism needs to
be run to allow the difference between functions and data
constructors to be resolved.
compiler/notes/compiler_design.html:
Move the documentation on assertions to after the documentation on
polymorphism.
Index: 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/07/29 10:11:10
@@ -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),
+
+ (
+ commutative_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
+ ).
%
+ % commutative_assertion
+ %
+ % Does there exist one (and only one) commutative 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 commutative_assertion(list(assert_id)::in, module_info::in,
+ prog_vars::in, set(prog_var)::out) is semidet.
+
+commutative_assertion([AssertId | AssertIds], ModuleInfo, Args0,
+ PossibleStaticVars) :-
+ (
+ assertion__is_commutative(AssertId, ModuleInfo, Args0,
+ PossibleStaticVars0)
+ ->
+ \+ commutative_assertion(AssertIds, ModuleInfo, Args0, _),
+ PossibleStaticVars = set__list_to_set(PossibleStaticVars0)
+ ;
+ commutative_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 that is commutative (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: 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/07/30 07:27:43
@@ -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.
%
% assertion__goal
@@ -36,15 +37,91 @@
:- pred assertion__record_preds_used_in(hlds_goal::in, assert_id::in,
module_info::in, module_info::out) is det.
+ %
+ % assertion__is_commutative(Id, MI, Vs, CVs)
+ %
+ % Does the assertion represented by the assertion id, Id,
+ % represent a commutative pred/func?
+ % If so, CVs, returns 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 [I,A,B,C] ( p(A,B,C) <=> p(B,A,C) )
+ % for the predicate to return true.
+ %
+:- pred assertion__is_commutative(assert_id::in, module_info::in,
+ prog_vars::in, prog_vars::out) is semidet.
+
+ %
+ % assertion__check_exported
+ %
+ % Ensure that an assertion which is defined in an interface only
+ % refers to constructors, functions and predicates defined in
+ % that interface.
+ % XXX at a later date this constraint should disappear.
+ %
+:- pred assertion__check_exported(hlds_goal::in, module_info::in,
+ module_specifier::in, io__state::di, io__state::uo) is det.
+
%-----------------------------------------------------------------------------%
:- implementation.
+
+:- import_module goal_util, hlds_out, hlds_pred, prog_out.
+:- import_module list, map, require, set, std_util.
-:- import_module hlds_pred.
-:- import_module list, require, set, std_util.
+:- type subst == map(prog_var, prog_var).
%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+assertion__is_commutative(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, prog_vars::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),
assertion_table_lookup(AssertTable, AssertId, PredId),
@@ -54,71 +131,134 @@
(
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).
+
+:- 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).
+
%-----------------------------------------------------------------------------%
%
@@ -127,15 +267,197 @@
% 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__check_exported(call(PredId,_,_,_,_,SymName) - GoalInfo,
+ ModuleInfo, ModSpec) -->
+ { module_info_pred_info(ModuleInfo, PredId, PredInfo) },
+ (
+ { pred_info_is_exported(PredInfo) }
+ ->
+ []
+ ;
+ { goal_info_get_context(GoalInfo, Context) },
+ { pred_info_arity(PredInfo, Arity) },
+ { pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
+ write_error_message(Context, PredOrFunc, SymName,
+ Arity, ModSpec)
+ ).
+assertion__check_exported(generic_call(_,_,_,_) - _, _, _) --> [].
+assertion__check_exported(unify(_,RHS,_,_,_) - GoalInfo,
+ ModuleInfo, ModSpec) -->
+ { goal_info_get_context(GoalInfo, Context) },
+ assertion__check_exported_unify_rhs(RHS, Context, ModuleInfo, ModSpec).
+assertion__check_exported(pragma_c_code(_,PredId,_,_,_,_,_) - GoalInfo,
+ ModuleInfo, ModSpec) -->
+ { module_info_pred_info(ModuleInfo, PredId, PredInfo) },
+ (
+ { pred_info_is_exported(PredInfo) }
+ ->
+ []
+ ;
+ { goal_info_get_context(GoalInfo, Context) },
+ { pred_info_name(PredInfo, Name) },
+ { SymName = unqualified(Name) },
+ { pred_info_arity(PredInfo, Arity) },
+ { pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
+ write_error_message(Context, PredOrFunc, SymName,
+ Arity, ModSpec)
+ ).
+assertion__check_exported(conj(Goals) - _, ModuleInfo, ModSpec) -->
+ assertion__check_exported_list(Goals, ModuleInfo, ModSpec).
+assertion__check_exported(switch(_,_,_,_) - _, _, _) -->
+ { error("assertion__check_exported: assertion contains switch.") }.
+assertion__check_exported(disj(Goals,_) - _, ModuleInfo, ModSpec) -->
+ assertion__check_exported_list(Goals, ModuleInfo, ModSpec).
+assertion__check_exported(not(Goal) - _, ModuleInfo, ModSpec) -->
+ assertion__check_exported(Goal, ModuleInfo, ModSpec).
+assertion__check_exported(some(_,_,Goal) - _, ModuleInfo, ModSpec) -->
+ assertion__check_exported(Goal, ModuleInfo, ModSpec).
+assertion__check_exported(if_then_else(_, If, Then, Else, _) - _,
+ ModuleInfo, ModSpec) -->
+ assertion__check_exported(If, ModuleInfo, ModSpec),
+ assertion__check_exported(Then, ModuleInfo, ModSpec),
+ assertion__check_exported(Else, ModuleInfo, ModSpec).
+assertion__check_exported(par_conj(Goals,_) - _, ModuleInfo, ModSpec) -->
+ assertion__check_exported_list(Goals, ModuleInfo, ModSpec).
+
+%-----------------------------------------------------------------------------%
+
+:- pred write_error_message(prog_context::in,
+ pred_or_func::in, sym_name::in, arity::in,
+ module_specifier::in, io__state::di, io__state::uo) is det.
+
+write_error_message(Context, PredOrFunc, SymName, Arity, ModSpec) -->
+ prog_out__write_context(Context),
+ io__write_string("Error: "),
+ hlds_out__write_simple_call_id(PredOrFunc, SymName, Arity),
+ io__write_string(" in an assertion which is in an interface\n"),
+ prog_out__write_context(Context),
+ io__write_string(" and not an exported "),
+ hlds_out__write_pred_or_func(PredOrFunc),
+ io__write_string(" of the module `"),
+ prog_out__write_sym_name(ModSpec),
+ io__write_string("'\n").
+
+%-----------------------------------------------------------------------------%
+
+:- pred assertion__check_exported_unify_rhs(unify_rhs::in, prog_context::in,
+ module_info::in, module_specifier::in,
+ io__state::di, io__state::uo) is det.
+
+assertion__check_exported_unify_rhs(var(_), _, _, _) --> [].
+assertion__check_exported_unify_rhs(functor(ConsId, _), Context,
+ _ModuleInfo, ModSpec) -->
+ (
+ { assertion__check_cons_id(ConsId, ModSpec) }
+ ->
+ []
+ ;
+ write_error_message(Context, ConsId, ModSpec)
+ ).
+assertion__check_exported_unify_rhs(lambda_goal(_,_,_,_,_,_,_,Goal), _Context,
+ ModuleInfo, ModSpec) -->
+ assertion__check_exported(Goal, ModuleInfo, ModSpec).
+
+:- pred assertion__check_cons_id(cons_id::in, module_specifier::in) is semidet.
+
+assertion__check_cons_id(ConsId, ModSpec) :-
+ ConsId = cons(SymName, _) => SymName = qualified(ModSpec, _).
+
+:- pred write_error_message(prog_context::in, cons_id::in,
+ module_specifier::in, io__state::di, io__state::uo) is det.
+
+write_error_message(Context, ConsId, ModSpec) -->
+ prog_out__write_context(Context),
+ io__write_string("Error: Constructor `"),
+ hlds_out__write_cons_id(ConsId),
+ io__write_string("' in an assertion in the interface section\n"),
+ prog_out__write_context(Context),
+ io__write_string(" which is not module qualified with `"),
+ prog_out__write_sym_name(ModSpec),
+ io__write_string("'\n").
+
+%-----------------------------------------------------------------------------%
+
+:- pred assertion__check_exported_list(hlds_goals::in, module_info::in,
+ module_specifier::in, io__state::di, io__state::uo)is det.
+
+assertion__check_exported_list([], _, _) --> [].
+assertion__check_exported_list([Goal0 | Goal0s], ModuleInfo, ModSpec) -->
+ assertion__check_exported(Goal0, ModuleInfo, ModSpec),
+ assertion__check_exported_list(Goal0s, ModuleInfo, ModSpec).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
Index: 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: 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: 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: 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/08/27 07:06:06
@@ -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) -->
(
@@ -846,6 +871,7 @@
},
globals__io_lookup_string_option(dump_hlds_options, Verbose),
( { string__contains_char(Verbose, 'm') } ->
+ hlds_out__write_indent(Indent),
hlds_out__write_indent(Indent),
io__write_string("% Modes for which this clause applies: "),
{ list__map(lambda([Mode :: in, ModeInt :: out] is det,
Index: 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/08/27 05:51:27
@@ -91,7 +91,11 @@
{ 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, PredIds0) },
+ { list__reverse(PredIds0, PredIds) },
{ init_intermod_info(ModuleInfo0, IntermodInfo0) },
globals__io_lookup_int_option(
intermod_inline_simple_threshold, Threshold),
@@ -170,50 +174,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 +225,60 @@
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)
+ )
+ )
+ ;
+ 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: make_hlds.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/make_hlds.m,v
retrieving revision 1.300
diff -u -r1.300 make_hlds.m
--- make_hlds.m 1999/07/14 14:56:11 1.300
+++ make_hlds.m 1999/08/27 07:39:38
@@ -695,9 +695,22 @@
{ Info = Info0 }
).
add_item_clause(assertion(Goal0, VarSet),
- Status, Status, Context, Module0, Module, Info0, Info) -->
+ Status0, Status, Context, Module0, Module, Info0, Info) -->
%
+ % If the assertion is imported, we need to change it to
+ % opt_imported so that type and purity checking, and
+ % polymorphism get run on it.
+ %
+ (
+ { Status0 = imported }
+ ->
+ { Status = opt_imported }
+ ;
+ { Status = Status0 }
+ ),
+
+ %
% If the outermost existentially quantified variables
% are placed in the head of the assertion, the
% typechecker will avoid warning about unbound
@@ -2696,11 +2709,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.
@@ -2825,16 +2867,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,
@@ -4268,6 +4316,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),
@@ -4388,8 +4447,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) },
%
@@ -4401,11 +4458,15 @@
(
{ 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: 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/25 07:27:57
@@ -807,6 +807,10 @@
report_warning("Warning: pragma in module interface.\n"),
check_for_clauses_in_interface(Items0, Items)
;
+ { Item0 = assertion(_, _) }
+ ->
+ check_for_clauses_in_interface(Items0, Items)
+ ;
{ Items = [ItemAndContext0 | Items1] },
check_for_clauses_in_interface(Items0, Items1)
).
@@ -844,6 +848,11 @@
; Item0 = pragma(Pragma),
pragma_allowed_in_interface(Pragma, no)
)
+ ->
+ split_clauses_and_decls(Items0, ClauseItems1, InterfaceItems),
+ ClauseItems = [ItemAndContext0 | ClauseItems1]
+ ;
+ Item0 = assertion(_, _)
->
split_clauses_and_decls(Items0, ClauseItems1, InterfaceItems),
ClauseItems = [ItemAndContext0 | ClauseItems1]
Index: 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/08/27 09:39:06
@@ -433,7 +433,7 @@
:- import_module type_util, mode_util, quantification, instmap, prog_out.
:- import_module code_util, unify_proc, prog_util, make_hlds.
:- import_module (inst), hlds_out, base_typeclass_info, goal_util, passes_aux.
-:- import_module clause_to_proc.
+:- import_module (assertion), clause_to_proc.
:- import_module bool, int, string, set, map.
:- import_module term, varset, std_util, require, assoc_list.
@@ -612,8 +612,17 @@
{ pred_info_set_procedures(PredInfo2, Procs, PredInfo) },
{ module_info_set_pred_info(ModuleInfo1, PredId, PredInfo,
- ModuleInfo) }.
+ ModuleInfo2) },
+ (
+ { pred_info_get_goal_type(PredInfo0, assertion) }
+ ->
+ polymorphism__finish_assertion(ModuleInfo2,
+ PredId, ModuleInfo)
+ ;
+ { ModuleInfo = ModuleInfo2 }
+ ).
+
:- pred polymorphism__process_clause_info(clauses_info, pred_info, module_info,
clauses_info, poly_info, list(mode)).
:- mode polymorphism__process_clause_info(in, in, in, out, out, out) is det.
@@ -978,6 +987,46 @@
term__context_init(Context),
create_atomic_unification(Var1, var(Var2), Context, explicit,
[], Goal).
+
+%-----------------------------------------------------------------------------%
+
+ %
+ % 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_info associated with the
+ % assertion into the assertion table.
+ % Also record for each predicate that is used in an assertion
+ % which assertion it is used in.
+ %
+:- pred polymorphism__finish_assertion(module_info, pred_id,
+ module_info, io__state, io__state).
+:- mode polymorphism__finish_assertion(in, in, out, di, uo) is det.
+
+polymorphism__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) },
+
+ % Remove from further processing.
+ { module_info_remove_predid(Module1, PredId, Module2) },
+
+ { module_info_pred_info(Module2, PredId, PredInfo) },
+ { assertion__goal(Id, Module2, Goal) },
+ (
+ { pred_info_is_exported(PredInfo) }
+ ->
+ { module_info_name(Module2, ModSpec) },
+ assertion__check_exported(Goal, Module2, ModSpec)
+ ;
+ []
+ ),
+
+ % record which predicates are used in assertions
+ { assertion__record_preds_used_in(Goal, Id, Module2, Module) }.
+
%-----------------------------------------------------------------------------%
Index: post_typecheck.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/post_typecheck.m,v
retrieving revision 1.12
diff -u -r1.12 post_typecheck.m
--- post_typecheck.m 1999/07/29 07:51:47 1.12
+++ post_typecheck.m 1999/07/29 10:21:32
@@ -96,18 +96,11 @@
pred_info, pred_info, io__state, io__state).
:- mode post_typecheck__finish_ill_typed_pred(in, in, in, out, di, uo) is det.
- % Now that the assertion has finished being typechecked,
- % 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.
-
%-----------------------------------------------------------------------------%
:- implementation.
-:- import_module (assertion), typecheck, clause_to_proc.
+:- import_module 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.
@@ -594,27 +587,6 @@
PredInfo0, PredInfo) -->
post_typecheck__propagate_types_into_modes(ModuleInfo, PredId,
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
- % assertion into the assertion table.
- % Also records for each predicate that is used in an assertion
- % which assertion it is used in.
- %
-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),
-
- % Remove from further processing.
- module_info_remove_predid(Module1, PredId, Module2),
-
- % record which predicates are used in assertions
- assertion__goal(Id, Module2, Goal),
- assertion__record_preds_used_in(Goal, Id, Module2, Module).
-
%
% Ensure that all constructors occurring in predicate mode
Index: 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/07/29 10:21:32
@@ -291,15 +291,7 @@
{ module_info_set_predicate_table(ModuleInfo0, PredTable,
ModuleInfo1) },
- (
- { pred_info_get_goal_type(PredInfo0, assertion) }
- ->
- { post_typecheck__finish_assertion(ModuleInfo1,
- PredId, ModuleInfo2) }
- ;
- { ModuleInfo2 = ModuleInfo1 }
- ),
- check_preds_purity_2(PredIds, FoundTypeError, ModuleInfo2, ModuleInfo,
+ check_preds_purity_2(PredIds, FoundTypeError, ModuleInfo1, ModuleInfo,
NumErrors1, NumErrors).
% Purity-check the code for single predicate, reporting any errors.
Index: notes/compiler_design.html
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/notes/compiler_design.html,v
retrieving revision 1.35
diff -u -r1.35 compiler_design.html
--- compiler_design.html 1999/08/05 11:57:42 1.35
+++ compiler_design.html 1999/08/17 06:01:18
@@ -100,7 +100,6 @@
This section describes the role of each module in the compiler.
For more information about the design of a particular module,
see the documentation at the start of that module's source code.
-
<p>
<hr>
<!---------------------------------------------------------------------------->
@@ -126,7 +125,6 @@
<h3> FRONT END </h3>
<h4> 1. Parsing </h4>
-
<p>
<ul>
@@ -307,15 +305,6 @@
It also removes assertions from further processing.
</ul>
-<dt> assertions
-
- <dd>
- assertion.m is the abstract interface to the assertion table.
- Currently all the compiler does is type check the assertions and
- record for each predicate that is used in an assertion, which
- assertion it is used in. The set up of the assertion table occurs
- in post_typecheck__finish_assertion.
-
<dt> purity analysis
<dd>
@@ -348,6 +337,15 @@
are used by other modules. These include some routines for generating
code to create type_infos, which are used by simplify.m and magic.m
when those modules introduce new calls to polymorphic procedures.
+
+<dt> assertions
+
+ <dd>
+ assertion.m is the abstract interface to the assertion table.
+ Currently all the compiler does is type check the assertions and
+ record for each predicate that is used in an assertion, which
+ assertion it is used in. The set up of the assertion table occurs
+ in polymorphism__finish_assertion.
<dt> mode analysis
----
+----------------------------------------------------------------------+
| Peter Ross M Sci/Eng Melbourne Uni |
| petdr at cs.mu.oz.au WWW: www.cs.mu.oz.au/~petdr/ ph: +61 3 9344 9158 |
+----------------------------------------------------------------------+
--------------------------------------------------------------------------
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