[m-dev.] for review: fix quantification of "<=>" [1/2]
Peter Ross
petdr at cs.mu.OZ.AU
Mon Oct 25 11:56:28 AEST 1999
This change looks fine.
Pete
On 25-Oct-1999, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> Estimated hours taken: 10
>
> Handle quantification analysis of bi-implication (`<=>') goals correctly.
> Previously we used to expand bi-implications before doing quantification
> analysis, which stuffed up the results of quantification analysis for
> those goals. We need to do quantification analysis first, and only
> then can we expand bi-implications. In addition, elimination of double
> negation needs to come after expansion of bi-implication, so I moved
> that from make_hlds.m to purity.m.
>
> compiler/hlds_goal.m:
> Add a new alternative to the HLDS goal type for bi-implications.
> Also add a new predicate negate_goal, for use by purity.m.
>
> compiler/make_hlds.m:
> Don't expand bi-implication here, instead just use the new
> bi_implication/2 HLDS goal type.
> Don't eliminated double negation here.
>
> compiler/quantification.m:
> Handle quantification for bi-implications.
> Expand bi-implications.
>
> compiler/purity.m:
> Eliminate double negation.
>
> compiler/hlds_out.m:
> Add code to print out bi-implication goals.
>
> compiler/*.m:
> Trivial changes to handle the new bi_implication/2
> alternative in the HLDS goal type.
>
> compiler/notes/compiler_design.html:
> Document the above changes.
>
> tests/hard_coded/Mmakefile:
> tests/hard_coded/quantifier2.m:
> tests/hard_coded/quantifier2.exp:
> A regression test for the above change.
>
> Workspace: /d-drive/home/hg/fjh/mercury
> Index: compiler/assertion.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/assertion.m,v
> retrieving revision 1.2
> diff -u -d -r1.2 assertion.m
> --- compiler/assertion.m 1999/09/12 04:26:37 1.2
> +++ compiler/assertion.m 1999/10/21 13:48:32
> @@ -211,6 +211,10 @@
> equal_vars(VarsA, VarsB, Subst0, Subst).
> equal_goals(par_conj(GoalAs, _) - _, par_conj(GoalBs, _) - _, Subst0, Subst) :-
> equal_goals_list(GoalAs, GoalBs, Subst0, Subst).
> +equal_goals(bi_implication(LeftGoalA, RightGoalA) - _,
> + bi_implication(LeftGoalB, RightGoalB) - _, Subst0, Subst) :-
> + equal_goals(LeftGoalA, LeftGoalB, Subst0, Subst1),
> + equal_goals(RightGoalA, RightGoalB, Subst1, Subst).
>
> :- pred equal_vars(prog_vars::in, prog_vars::in, subst::in,
> subst::out) is semidet.
> @@ -324,6 +328,10 @@
> assertion__normalise_goal(Else0, Else).
> assertion__normalise_goal(par_conj(Goal0s,B) - GI, par_conj(Goals,B) - GI) :-
> assertion__normalise_goals(Goal0s, Goals).
> +assertion__normalise_goal(bi_implication(LHS0, RHS0) - GI,
> + bi_implication(LHS, RHS) - GI) :-
> + assertion__normalise_goal(LHS0, LHS),
> + assertion__normalise_goal(RHS0, RHS).
>
> %-----------------------------------------------------------------------------%
>
> @@ -409,6 +417,10 @@
> assertion__in_interface_check(Else, PredInfo, ModuleInfo).
> assertion__in_interface_check(par_conj(Goals,_) - _, PredInfo, ModuleInfo) -->
> assertion__in_interface_check_list(Goals, PredInfo, ModuleInfo).
> +assertion__in_interface_check(bi_implication(LHS, RHS) - _, PredInfo,
> + ModuleInfo) -->
> + assertion__in_interface_check(LHS, PredInfo, ModuleInfo),
> + assertion__in_interface_check(RHS, PredInfo, ModuleInfo).
>
> %-----------------------------------------------------------------------------%
>
> Index: compiler/dependency_graph.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/dependency_graph.m,v
> retrieving revision 1.43
> diff -u -d -r1.43 dependency_graph.m
> --- compiler/dependency_graph.m 1999/07/13 08:52:47 1.43
> +++ compiler/dependency_graph.m 1999/10/21 11:08:20
> @@ -275,6 +275,11 @@
> dependency_graph__add_arcs_in_goal_2(pragma_c_code(_, _, _, _, _, _, _), _,
> DepGraph, DepGraph).
>
> +dependency_graph__add_arcs_in_goal_2(bi_implication(LHS, RHS), Caller,
> + DepGraph0, DepGraph) :-
> + dependency_graph__add_arcs_in_list([LHS, RHS], Caller,
> + DepGraph0, DepGraph).
> +
> %-----------------------------------------------------------------------------%
>
> :- pred dependency_graph__add_arcs_in_list(list(hlds_goal), relation_key,
> @@ -688,6 +693,9 @@
> Map, Map) --> [].
> process_aditi_goal(_IsNeg, pragma_c_code(_, _, _, _, _, _, _) - _,
> Map, Map) --> [].
> +process_aditi_goal(_, bi_implication(_, _) - _, _, _) -->
> + % these should have been expanded out by now
> + { error("process_aditi_goal: unexpected bi_implication") }.
>
> %-----------------------------------------------------------------------------%
>
> Index: compiler/dnf.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/dnf.m,v
> retrieving revision 1.37
> diff -u -d -r1.37 dnf.m
> --- compiler/dnf.m 1999/07/13 08:52:50 1.37
> +++ compiler/dnf.m 1999/10/21 16:33:06
> @@ -240,6 +240,10 @@
> ModuleInfo = ModuleInfo0,
> NewPredIds = NewPredIds0,
> Goal = Goal0
> + ;
> + GoalExpr0 = bi_implication(_, _),
> + % these should have been expanded out by now
> + error("dnf__transform_goal: unexpected bi_implication")
> ).
>
> %-----------------------------------------------------------------------------%
> @@ -468,6 +472,7 @@
> ).
> dnf__is_atomic_expr(_, _, _, if_then_else(_, _, _, _, _), no).
> dnf__is_atomic_expr(_, _, _, pragma_c_code(_, _, _, _, _, _, _), yes).
> +dnf__is_atomic_expr(_, _, _, bi_implication(_, _), no).
>
> :- pred dnf__free_of_nonatomic(hlds_goal::in,
> set(pred_proc_id)::in) is semidet.
> Index: compiler/goal_util.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/goal_util.m,v
> retrieving revision 1.58
> diff -u -d -r1.58 goal_util.m
> --- compiler/goal_util.m 1999/10/15 03:44:44 1.58
> +++ compiler/goal_util.m 1999/10/21 14:53:56
> @@ -368,6 +368,11 @@
> pragma_c_code(A,B,C,Vars,E,F,G)) :-
> goal_util__rename_var_list(Vars0, Must, Subn, Vars).
>
> +goal_util__name_apart_2(bi_implication(LHS0, RHS0), Must, Subn,
> + bi_implication(LHS, RHS)) :-
> + goal_util__rename_vars_in_goal(LHS0, Must, Subn, LHS),
> + goal_util__rename_vars_in_goal(RHS0, Must, Subn, RHS).
> +
> %-----------------------------------------------------------------------------%
>
> :- pred goal_util__name_apart_list(list(hlds_goal), bool,
> @@ -591,6 +596,10 @@
> Set0, Set) :-
> set__insert_list(Set0, ArgVars, Set).
>
> +goal_util__goal_vars_2(bi_implication(LHS - _, RHS - _), Set0, Set) :-
> + goal_util__goal_vars_2(LHS, Set0, Set1),
> + goal_util__goal_vars_2(RHS, Set1, Set).
> +
> goal_util__goals_goal_vars([], Set, Set).
> goal_util__goals_goal_vars([Goal - _ | Goals], Set0, Set) :-
> goal_util__goal_vars_2(Goal, Set0, Set1),
> @@ -728,6 +737,10 @@
> goal_expr_size(generic_call(_, _, _, _), 1).
> goal_expr_size(unify(_, _, _, _, _), 1).
> goal_expr_size(pragma_c_code(_, _, _, _, _, _, _), 1).
> +goal_expr_size(bi_implication(LHS, RHS), Size) :-
> + goal_size(LHS, Size1),
> + goal_size(RHS, Size2),
> + Size is Size1 + Size2 + 1.
>
> %-----------------------------------------------------------------------------%
> %
> Index: compiler/hlds_goal.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/hlds_goal.m,v
> retrieving revision 1.63
> diff -u -d -r1.63 hlds_goal.m
> --- compiler/hlds_goal.m 1999/09/12 04:26:41 1.63
> +++ compiler/hlds_goal.m 1999/10/21 14:55:52
> @@ -29,7 +29,7 @@
> ---> conj(hlds_goals)
>
> % A predicate call.
> - % Initially only the sym_name and arguments
> + % Initially only the sym_name, arguments, and context
> % are filled in. Type analysis fills in the
> % pred_id. Mode analysis fills in the
> % proc_id and the builtin_state field.
> @@ -179,12 +179,28 @@
> % pragma_c_codes; none for others.
> )
>
> + % parallel conjunction
> ; par_conj(hlds_goals, store_map)
> - % parallel conjunction
> % The store_map specifies the locations
> % in which live variables should be
> % stored at the start of the parallel
> % conjunction.
> +
> + % bi-implication (A <=> B)
> + %
> + % These get eliminated by quantification.m,
> + % so most passes of the compiler will just call error/1
> + % if they occur.
> + %
> + % Note that ordinary implications (A => B)
> + % and reverse implications (A <= B) are expanded
> + % out before we construct the HLDS. But we can't
> + % do that for bi-implications, because if expansion
> + % of bi-implications is done before implicit quantification,
> + % then the quantification would be wrong.
> +
> + ; bi_implication(hlds_goal, hlds_goal)
> +
> .
>
> :- type generic_call
> @@ -880,6 +896,11 @@
> :- pred conjoin_goals(hlds_goal, hlds_goal, hlds_goal).
> :- mode conjoin_goals(in, in, out) is det.
>
> + % Negate a goal, eliminating double negations as we go.
> + %
> +:- pred negate_goal(hlds_goal, hlds_goal_info, hlds_goal).
> +:- mode negate_goal(in, in, out) is det.
> +
> % A goal is atomic iff it doesn't contain any sub-goals
> % (except possibly goals inside lambda expressions --
> % but lambda expressions will get transformed into separate
> @@ -1242,6 +1263,37 @@
> ),
> conjoin_goal_and_goal_list(Goal1, GoalList, Goal).
>
> + % Negate a goal, eliminating double negations as we go.
> +
> +negate_goal(Goal, GoalInfo, NegatedGoal) :-
> + (
> + % eliminate double negations
> + Goal = not(Goal1) - _
> + ->
> + NegatedGoal = Goal1
> + ;
> + % convert negated conjunctions of negations
> + % into disjunctions
> + Goal = conj(NegatedGoals) - _,
> + all_negated(NegatedGoals, UnnegatedGoals)
> + ->
> + map__init(StoreMap),
> + NegatedGoal = disj(UnnegatedGoals, StoreMap) - GoalInfo
> + ;
> + NegatedGoal = not(Goal) - GoalInfo
> + ).
> +
> +:- pred all_negated(list(hlds_goal), list(hlds_goal)).
> +:- mode all_negated(in, out) is semidet.
> +
> +all_negated([], []).
> +all_negated([not(Goal) - _ | NegatedGoals], [Goal | Goals]) :-
> + all_negated(NegatedGoals, Goals).
> +all_negated([conj(NegatedConj) - _GoalInfo | NegatedGoals], Goals) :-
> + all_negated(NegatedConj, Goals1),
> + all_negated(NegatedGoals, Goals2),
> + list__append(Goals1, Goals2, Goals).
> +
> %-----------------------------------------------------------------------------%
>
> goal_is_atomic(conj([])).
> @@ -1345,6 +1397,10 @@
> Goal = unify(_, _, _, _, _).
> set_goal_contexts_2(_, Goal, Goal) :-
> Goal = pragma_c_code(_, _, _, _, _, _, _).
> +set_goal_contexts_2(Context, bi_implication(LHS0, RHS0),
> + bi_implication(LHS, RHS)) :-
> + set_goal_contexts(Context, LHS0, LHS),
> + set_goal_contexts(Context, RHS0, RHS).
>
> %-----------------------------------------------------------------------------%
>
> Index: compiler/hlds_out.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
> retrieving revision 1.227
> diff -u -d -r1.227 hlds_out.m
> --- compiler/hlds_out.m 1999/10/15 03:44:46 1.227
> +++ compiler/hlds_out.m 1999/10/21 11:25:52
> @@ -1539,6 +1539,21 @@
> io__write_string(")"),
> io__write_string(Follow).
>
> +hlds_out__write_goal_2(bi_implication(LHS, RHS), ModuleInfo, VarSet,
> + AppendVarnums, Indent, Follow, TypeQual) -->
> + hlds_out__write_indent(Indent),
> + io__write_string("( % bi-implication\n"),
> + { Indent1 is Indent + 1 },
> + hlds_out__write_goal_a(LHS, ModuleInfo, VarSet, AppendVarnums,
> + Indent1, "\n", TypeQual),
> + hlds_out__write_indent(Indent),
> + io__write_string("<=>\n"),
> + hlds_out__write_goal_a(RHS, ModuleInfo, VarSet, AppendVarnums,
> + Indent1, "\n", TypeQual),
> + hlds_out__write_indent(Indent),
> + io__write_string(")"),
> + io__write_string(Follow).
> +
> :- pred hlds_out__write_varnum_list(list(prog_var), io__state, io__state).
> :- mode hlds_out__write_varnum_list(in, di, uo) is det.
>
> Index: compiler/make_hlds.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
> retrieving revision 1.310
> diff -u -d -r1.310 make_hlds.m
> --- compiler/make_hlds.m 1999/10/14 04:27:52 1.310
> +++ compiler/make_hlds.m 1999/10/21 16:47:36
> @@ -4014,6 +4014,12 @@
> warn_singletons_in_pragma_c_code(PragmaImpl, ArgInfo, Context,
> PredCallId, MI).
>
> +warn_singletons_in_goal_2(bi_implication(LHS, RHS), _GoalInfo, QuantVars,
> + VarSet, PredCallId, MI) -->
> + warn_singletons_in_goal_list([LHS, RHS], QuantVars, VarSet,
> + PredCallId, MI).
> +
> +
> :- pred warn_singletons_in_goal_list(list(hlds_goal), set(prog_var),
> prog_varset, simple_call_id, module_info,
> io__state, io__state).
> @@ -4661,24 +4667,8 @@
>
> transform_goal_2(not(A0), _, VarSet0, Subst, Goal, VarSet, Info0, Info) -->
> transform_goal(A0, VarSet0, Subst, A, VarSet, Info0, Info),
> - {
> - % eliminate double negations
> - A = not(Goal1) - _
> - ->
> - Goal = Goal1
> - ;
> - % convert negated conjunctions of negations
> - % into disjunctions
> - A = conj(NegatedGoals) - _,
> - all_negated(NegatedGoals, UnnegatedGoals)
> - ->
> - goal_info_init(GoalInfo),
> - map__init(StoreMap),
> - Goal = disj(UnnegatedGoals, StoreMap) - GoalInfo
> - ;
> - goal_info_init(GoalInfo),
> - Goal = not(A) - GoalInfo
> - }.
> + { goal_info_init(GoalInfo) },
> + { Goal = not(A) - GoalInfo }.
>
> transform_goal_2((A0,B0), _, VarSet0, Subst, Goal, VarSet, Info0, Info) -->
> get_conj(B0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1),
> @@ -4705,13 +4695,19 @@
> transform_goal_2(TransformedGoal, Context, VarSet0, Subst,
> Goal, VarSet, Info0, Info).
>
> -transform_goal_2(equivalent(P, Q), Context, VarSet0, Subst, Goal, VarSet,
> +transform_goal_2(equivalent(P0, Q0), _Context, VarSet0, Subst, Goal, VarSet,
> Info0, Info) -->
> - % `P <=> Q' is defined as `(P => Q), (Q => P)'
> - { TransformedGoal = (implies(P, Q) - Context,
> - implies(Q, P) - Context) },
> - transform_goal_2(TransformedGoal, Context, VarSet0, Subst,
> - Goal, VarSet, Info0, Info).
> + %
> + % `P <=> Q' is defined as `(P => Q), (Q => P)',
> + % but that transformation must not be done until
> + % after quantification analysis, lest the duplication of
> + % the goals concerned affect the implicit quantification
> + % of the variables inside them.
> + %
> + { goal_info_init(GoalInfo) },
> + transform_goal(P0, VarSet0, Subst, P, VarSet1, Info0, Info1),
> + transform_goal(Q0, VarSet1, Subst, Q, VarSet, Info1, Info),
> + { Goal = bi_implication(P, Q) - GoalInfo }.
>
> transform_goal_2(call(Name, Args0, Purity), Context, VarSet0, Subst, Goal,
> VarSet, Info0, Info) -->
> @@ -4801,18 +4797,6 @@
> { term__apply_substitution(B0, Subst, B) },
> unravel_unification(A, B, Context, explicit, [],
> VarSet0, Goal, VarSet, Info0, Info).
> -
> -:- pred all_negated(list(hlds_goal), list(hlds_goal)).
> -:- mode all_negated(in, out) is semidet.
> -
> -all_negated([], []).
> -all_negated([not(Goal) - _ | NegatedGoals], [Goal | Goals]) :-
> - all_negated(NegatedGoals, Goals).
> -% nested conjunctions shouldn't occur here anyway, but just in case...
> -all_negated([conj(NegatedConj) - _GoalInfo | NegatedGoals], Goals) :-
> - all_negated(NegatedConj, Goals1),
> - all_negated(NegatedGoals, Goals2),
> - list__append(Goals1, Goals2, Goals).
>
> :- inst aditi_update_str =
> bound( "aditi_insert"
> Index: compiler/purity.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/purity.m,v
> retrieving revision 1.19
> diff -u -d -r1.19 purity.m
> --- compiler/purity.m 1999/09/12 04:26:51 1.19
> +++ compiler/purity.m 1999/10/21 17:12:08
> @@ -25,7 +25,11 @@
> % so they need to be a separate "post-typecheck pass"; they are done
> % here in combination with the purity-analysis pass for efficiency reasons.
> %
> +% We also do elimination of double-negation in this pass.
> +% It needs to be done somewhere after quantification analysis and
> +% before mode analysis, and this is convenient place to do it.
> %
> +%
> % The aim of Mercury's purity system is to allow one to declare certain parts
> % of one's program to be impure, thereby forbidding the compiler from making
> % certain optimizations to that part of the code. Since one can often
> @@ -508,10 +512,21 @@
> ModuleInfo, InClosure, Purity, NumErrors0, NumErrors) -->
> compute_goals_purity(Goals0, Goals, PredInfo, ModuleInfo,
> InClosure, pure, Purity, NumErrors0, NumErrors).
> -compute_expr_purity(not(Goal0), not(Goal), _, PredInfo, ModuleInfo,
> +compute_expr_purity(not(Goal0), NotGoal, GoalInfo0, PredInfo, ModuleInfo,
> InClosure, Purity, NumErrors0, NumErrors) -->
> - compute_goal_purity(Goal0, Goal, PredInfo, ModuleInfo,
> - InClosure, Purity, NumErrors0, NumErrors).
> + %
> + % eliminate double negation
> + %
> + { negate_goal(Goal0, GoalInfo0, NotGoal0) },
> + ( { NotGoal0 = not(Goal1) - _GoalInfo1 } ->
> + compute_goal_purity(Goal1, Goal, PredInfo, ModuleInfo,
> + InClosure, Purity, NumErrors0, NumErrors),
> + { NotGoal = not(Goal) }
> + ;
> + compute_goal_purity(NotGoal0, NotGoal1, PredInfo, ModuleInfo,
> + InClosure, Purity, NumErrors0, NumErrors),
> + { NotGoal1 = NotGoal - _ }
> + ).
> compute_expr_purity(some(Vars, CanRemove, Goal0), some(Vars, CanRemove, Goal),
> _, PredInfo, ModuleInfo, InClosure, Purity,
> NumErrors0, NumErrors) -->
> @@ -534,6 +549,9 @@
> { module_info_preds(ModuleInfo, Preds) },
> { map__lookup(Preds, PredId, PredInfo) },
> { pred_info_get_purity(PredInfo, Purity) }.
> +compute_expr_purity(bi_implication(_, _), _, _, _, _, _, _, _, _) -->
> + % these should have been expanded out by now
> + { error("compute_expr_purity: unexpected bi_implication") }.
>
> :- pred compute_goal_purity(hlds_goal, hlds_goal, pred_info,
> module_info, bool, purity, int, int, io__state, io__state).
> Index: compiler/quantification.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/quantification.m,v
> retrieving revision 1.68
> diff -u -d -r1.68 quantification.m
> --- compiler/quantification.m 1999/07/13 08:53:26 1.68
> +++ compiler/quantification.m 1999/10/24 15:32:11
> @@ -12,6 +12,10 @@
> % For the rules on implicit quantification, see the
> % Mercury language reference manual.
> %
> + % This pass also expands out bi-implications (that has to be
> + % done after quantification, and preferably as soon as possible,
> + % so we do it here).
> + %
> % Rather than making implicit quantification explicit by
> % inserting additional existential quantifiers in the form of
> % `some/2' goals, we instead record existential quantification
> @@ -353,6 +357,82 @@
> pragma_c_code(A,B,C,Vars,E,F,G)) -->
> implicitly_quantify_atomic_goal(Vars).
>
> +implicitly_quantify_goal_2(bi_implication(LHS0, RHS0), Context, Goal) -->
> + % get the initial values of various settings
> + quantification__get_quant_vars(QuantVars0),
> + quantification__get_outside(OutsideVars0),
> + quantification__get_lambda_outside(LambdaOutsideVars0),
> +
> + % quantified variables cannot be pushed inside a negation,
> + % so we insert the quantified vars into the outside vars set,
> + % and initialize the new quantified vars set to be empty
> + % (the lambda outside vars remain unchanged)
> + { set__union(OutsideVars0, QuantVars0, OutsideVars1) },
> + { set__init(QuantVars1) },
> + { LambdaOutsideVars1 = LambdaOutsideVars0 },
> + quantification__set_quant_vars(QuantVars1),
> +
> + % prepare for quantifying the LHS:
> + % add variables from the RHS to the outside vars
> + % and the outside lambda vars sets.
> + { quantification__goal_vars(RHS0, RHS_Vars, RHS_LambdaVars) },
> + { set__union(OutsideVars1, RHS_Vars, LHS_OutsideVars) },
> + { set__union(LambdaOutsideVars1, RHS_LambdaVars,
> + LHS_LambdaOutsideVars) },
> +
> + % quantify the LHS
> + quantification__set_outside(LHS_OutsideVars),
> + quantification__set_lambda_outside(LHS_LambdaOutsideVars),
> + implicitly_quantify_goal(LHS0, LHS),
> + quantification__get_nonlocals(LHS_NonLocalVars),
> +
> + % prepare for quantifying the RHS:
> + % add nonlocals from the LHS to the outside vars.
> + % (We use the nonlocals rather than the more symmetric
> + % approach of calling quantification__goal_vars on the
> + % LHS goal because it is more efficient.)
> + { set__union(OutsideVars1, LHS_NonLocalVars, RHS_OutsideVars) },
> + { RHS_LambdaOutsideVars = LambdaOutsideVars1 },
> +
> + % quantify the RHS
> + quantification__set_outside(RHS_OutsideVars),
> + quantification__set_lambda_outside(RHS_LambdaOutsideVars),
> + implicitly_quantify_goal(RHS0, RHS),
> + quantification__get_nonlocals(RHS_NonLocalVars),
> +
> + % compute the nonlocals for this goal
> + { set__union(LHS_NonLocalVars, RHS_NonLocalVars, AllNonLocalVars) },
> + { set__intersect(AllNonLocalVars, OutsideVars0, NonLocalVarsO) },
> + { set__intersect(AllNonLocalVars, LambdaOutsideVars0, NonLocalVarsL) },
> + { set__union(NonLocalVarsO, NonLocalVarsL, NonLocalVars) },
> + quantification__set_nonlocals(NonLocalVars),
> +
> + % restore the original values of various settings
> + quantification__set_outside(OutsideVars0),
> + quantification__set_lambda_outside(LambdaOutsideVars0),
> + quantification__set_quant_vars(QuantVars0),
> +
> + %
> + % We've figured out the quantification.
> + % Now expand the bi-implication according to the usual
> + % rules:
> + % LHS <=> RHS
> + % ===>
> + % (LHS => RHS), (RHS => LHS)
> + % ===>
> + % (not (LHS, not RHS)), (not (RHS, not LHS))
> + %
> + { goal_info_init(GoalInfo0) },
> + { goal_info_set_context(GoalInfo0, Context, GoalInfo1) },
> + { goal_info_set_nonlocals(GoalInfo1, LHS_NonLocalVars, LHS_GI) },
> + { goal_info_set_nonlocals(GoalInfo1, RHS_NonLocalVars, RHS_GI) },
> + { goal_info_set_nonlocals(GoalInfo1, NonLocalVars, GI) },
> + { NotLHS = not(LHS) - LHS_GI },
> + { NotRHS = not(RHS) - RHS_GI },
> + { ForwardsImplication = not(conj([LHS, NotRHS]) - GI) - GI },
> + { ReverseImplication = not(conj([RHS, NotLHS]) - GI) - GI },
> + { Goal = conj([ForwardsImplication, ReverseImplication]) }.
> +
> :- pred implicitly_quantify_atomic_goal(list(prog_var), quant_info, quant_info).
> :- mode implicitly_quantify_atomic_goal(in, in, out) is det.
>
> @@ -715,6 +795,10 @@
> quantification__goal_vars_2(pragma_c_code(_, _, _, ArgVars, _, _, _),
> Set0, LambdaSet, Set, LambdaSet) :-
> set__insert_list(Set0, ArgVars, Set).
> +
> +quantification__goal_vars_2(bi_implication(LHS, RHS), Set0, LambdaSet0, Set,
> + LambdaSet) :-
> + goal_list_vars_2([LHS, RHS], Set0, LambdaSet0, Set, LambdaSet).
>
> :- pred quantification__unify_rhs_vars(unify_rhs, set(prog_var), set(prog_var),
> set(prog_var), set(prog_var)).
> Index: compiler/typecheck.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
> retrieving revision 1.265
> diff -u -d -r1.265 typecheck.m
> --- compiler/typecheck.m 1999/07/22 17:14:39 1.265
> +++ compiler/typecheck.m 1999/10/21 16:22:40
> @@ -978,6 +978,10 @@
> OrigTypeAssignSet) },
> typecheck_call_pred_id(PredId, Args),
> perform_context_reduction(OrigTypeAssignSet).
> +typecheck_goal_2(bi_implication(LHS0, RHS0), bi_implication(LHS, RHS)) -->
> + checkpoint("<=>"),
> + typecheck_goal(LHS0, LHS),
> + typecheck_goal(RHS0, RHS).
>
> %-----------------------------------------------------------------------------%
>
> Index: compiler/notes/compiler_design.html
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/notes/compiler_design.html,v
> retrieving revision 1.39
> diff -u -d -r1.39 compiler_design.html
> --- compiler/notes/compiler_design.html 1999/10/14 05:27:35 1.39
> +++ compiler/notes/compiler_design.html 1999/10/21 16:01:22
> @@ -206,6 +206,9 @@
>
> make_hlds.m transforms the code into superhomogeneous form,
> and at the same time converts the parse tree into the HLDS.
> + It expands away universal quantification
> + (using `all [Vs] G' ===> `not (some [Vs] (not G))')
> + and implication (using `A => B' ===> `not(A, not B)').
> It converts `pragma import', `pragma c_code' and `pragma fact_table'
> declarations into clauses with HLDS `pragma_c_code'
> instructions for bodies.
> @@ -258,7 +261,10 @@
> <dd>
> quantification.m handles implicit quantification and computes
> the set of non-local variables for each sub-goal.
> - This is done in transform in make_hlds.m
> + It also expands away bi-implication (unlike the expansion
> + of implication and universal quantification, this expansion
> + cannot be done until after quantification).
> + This pass is called from the `transform' predicate in make_hlds.m.
>
> <dt> checking typeclass instances (check_typeclass.m)
> <dd>
> @@ -324,6 +330,8 @@
> complete the handling of predicate
> overloading for cases which typecheck.m is unable to handle,
> and to check for unbound type variables.
> + Elimination of double negation is also done here; that needs to
> + be done after quantification analysis and before mode analysis.
>
> <dt> polymorphism transformation
>
> Index: tests/hard_coded/Mmakefile
> ===================================================================
> RCS file: /home/mercury1/repository/tests/hard_coded/Mmakefile,v
> retrieving revision 1.67
> diff -u -d -r1.67 Mmakefile
> --- tests/hard_coded/Mmakefile 1999/10/19 04:11:43 1.67
> +++ tests/hard_coded/Mmakefile 1999/10/24 15:30:26
> @@ -80,6 +80,7 @@
> qual_basic_test \
> qual_is_test \
> quantifier \
> + quantifier2 \
> quoting_bug_test \
> rational_test \
> relation_test \
> cvs diff: tests/hard_coded/quantifier2.exp is a new entry, no comparison available
> cvs diff: tests/hard_coded/quantifier2.m is a new entry, no comparison available
> ====================
> tests/hard_coded/quantifier2.exp
> ====================
> yes
> ====================
> tests/hard_coded/quantifier2.m
> ====================
> :- module quantifier2.
>
> :- interface.
>
> :- import_module io.
>
> :- pred main(io__state::di,io__state::uo) is det.
>
> :- implementation.
>
> :- import_module list, int.
>
> :- pred testsum(list(int),int,int).
> :- mode testsum(in,in,out) is semidet.
>
> testsum([],I,0) :- I > 0.
> testsum([X|L],I,X + N1) :- testsum(L,I,N1).
>
>
> :- pred foo(pred(int, int)).
> :- mode foo(free->pred(in, out) is semidet) is det.
>
> foo(testsum([1,2,3])).
>
>
> main -->
> (
> { P = lambda([I :: in, X :: out] is semidet, (I > 0, X = 6)),
> foo(Q),
> J = 1,
> (call(P,J,_X) <=> call(Q,J,_Y)) }
> ->
> print("yes"), nl
> ;
> print("no"), nl
> ).
>
> ====================
>
> [continued in part 2]
>
> --
> Fergus Henderson <fjh at cs.mu.oz.au> | "I have always known that the pursuit
> WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
> PGP: finger fjh at 128.250.37.3 | -- the last words of T. S. Garp.
> --------------------------------------------------------------------------
> 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
> --------------------------------------------------------------------------
----
+----------------------------------------------------------------------+
| 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