diff --git a/compiler/assertion.m b/compiler/assertion.m index 0b7f36102..376329b9e 100644 --- a/compiler/assertion.m +++ b/compiler/assertion.m @@ -211,6 +211,10 @@ equal_goals(pragma_c_code(Attribs, PredId, _, VarsA, _, _, _) - _, 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(if_then_else(A, If0, Then0, Else0, E) - GI, 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(if_then_else(_, If, Then, Else, _) - _, 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). %-----------------------------------------------------------------------------% diff --git a/compiler/bytecode_gen.m b/compiler/bytecode_gen.m index 99188aa97..4e29d8393 100644 --- a/compiler/bytecode_gen.m +++ b/compiler/bytecode_gen.m @@ -252,6 +252,10 @@ bytecode_gen__goal_expr(GoalExpr, GoalInfo, ByteInfo0, ByteInfo, Code) :- GoalExpr = pragma_c_code(_, _, _, _, _, _, _), Code = node([not_supported]), ByteInfo = ByteInfo0 + ; + GoalExpr = bi_implication(_, _), + % these should have been expanded out by now + error("bytecode_gen__goal_expr: unexpected bi_implication") ). %---------------------------------------------------------------------------% diff --git a/compiler/code_gen.m b/compiler/code_gen.m index 18b61d377..16787645b 100644 --- a/compiler/code_gen.m +++ b/compiler/code_gen.m @@ -890,6 +890,9 @@ code_gen__generate_goal_2(pragma_c_code(Attributes, pragma_c_gen__generate_pragma_c_code(CodeModel, Attributes, PredId, ModeId, Args, ArgNames, OrigArgTypes, GoalInfo, PragmaCode, Instr). +code_gen__generate_goal_2(bi_implication(_, _), _, _, _) --> + % these should have been expanded out by now + { error("code_gen__generate_goal_2: unexpected bi_implication") }. %---------------------------------------------------------------------------% diff --git a/compiler/code_util.m b/compiler/code_util.m index a1da26a76..a07f7f53e 100644 --- a/compiler/code_util.m +++ b/compiler/code_util.m @@ -864,6 +864,10 @@ code_util__count_recursive_calls_2(if_then_else(_, Cond, Then, Else, _), CTMax is CMax + TMax, int__min(CTMin, EMin, Min), int__max(CTMax, EMax, Max). +code_util__count_recursive_calls_2(bi_implication(_, _), + _, _, _, _) :- + % these should have been expanded out by now + error("code_util__count_recursive_calls_2: unexpected bi_implication"). :- pred code_util__count_recursive_calls_conj(list(hlds_goal), pred_id, proc_id, int, int, int, int). diff --git a/compiler/cse_detection.m b/compiler/cse_detection.m index ce2f29c52..5bff96570 100644 --- a/compiler/cse_detection.m +++ b/compiler/cse_detection.m @@ -274,6 +274,10 @@ detect_cse_in_goal_2(if_then_else(Vars, Cond0, Then0, Else0, SM), GoalInfo, detect_cse_in_ite(NonLocalsList, Vars, Cond0, Then0, Else0, GoalInfo, SM, InstMap, CseInfo0, CseInfo, Redo, Goal). +detect_cse_in_goal_2(bi_implication(_, _), _, _, _, _, _, _) :- + % these should have been expanded out by now + error("detect_cse_in_goal_2: unexpected bi_implication"). + %-----------------------------------------------------------------------------% :- pred detect_cse_in_conj(list(hlds_goal), instmap, cse_info, cse_info, diff --git a/compiler/dead_proc_elim.m b/compiler/dead_proc_elim.m index fea8327ad..0212e65a7 100644 --- a/compiler/dead_proc_elim.m +++ b/compiler/dead_proc_elim.m @@ -485,6 +485,9 @@ dead_proc_elim__examine_expr(unify(_,_,_, Uni, _), _CurrProc, Queue0, Queue, Queue = Queue0, Needed = Needed0 ). +dead_proc_elim__examine_expr(bi_implication(_,_), _, _, _, _, _) :- + % these should have been expanded out by now + error("detect_cse_in_goal_2: unexpected bi_implication"). %-----------------------------------------------------------------------------% @@ -831,6 +834,9 @@ pre_modecheck_examine_goal(call(_, _, _, _, _, PredName) - _) --> pre_modecheck_examine_goal(pragma_c_code(_, _, _, _, _, _, _) - _) --> []. pre_modecheck_examine_goal(unify(_, Rhs, _, _, _) - _) --> pre_modecheck_examine_unify_rhs(Rhs). +pre_modecheck_examine_goal(bi_implication(_, _) - _) --> + % these should have been expanded out by now + { error("pre_modecheck_examine_goal: unexpected bi_implication") }. :- pred pre_modecheck_examine_unify_rhs(unify_rhs::in, dead_pred_info::in, dead_pred_info::out) is det. diff --git a/compiler/deforest.m b/compiler/deforest.m index 864a06fad..e30f9d703 100644 --- a/compiler/deforest.m +++ b/compiler/deforest.m @@ -219,6 +219,10 @@ deforest__goal(Goal0, Goal) --> deforest__goal(Goal, Goal) --> { Goal = unify(_, _, _, _, _) - _ }. +deforest__goal(bi_implication(_, _) - _, _) --> + % these should have been expanded out by now + { error("deforest__goal: unexpected bi_implication") }. + %-----------------------------------------------------------------------------% :- pred deforest__disj(list(hlds_goal)::in, list(hlds_goal)::out, diff --git a/compiler/dependency_graph.m b/compiler/dependency_graph.m index f3dda38ff..0ebffe8ef 100644 --- a/compiler/dependency_graph.m +++ b/compiler/dependency_graph.m @@ -275,6 +275,11 @@ dependency_graph__add_arcs_in_goal_2(unify(_,_,_,Unify,_), Caller, 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 @@ process_aditi_goal(_IsNeg, generic_call(_, _, _, _) - _, 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") }. %-----------------------------------------------------------------------------% diff --git a/compiler/det_analysis.m b/compiler/det_analysis.m index 83e0aa2d6..dde0858de 100644 --- a/compiler/det_analysis.m +++ b/compiler/det_analysis.m @@ -676,6 +676,10 @@ det_infer_goal_2(pragma_c_code(IsRecursive, PredId, ProcId, Args, Detism = erroneous ). +det_infer_goal_2(bi_implication(_, _), _, _, _, _, _, _, _, _, _) :- + % these should have been expanded out by now + error("det_infer_goal_2: unexpected bi_implication"). + %-----------------------------------------------------------------------------% :- pred det_infer_conj(list(hlds_goal), instmap, soln_context, det_info, diff --git a/compiler/det_report.m b/compiler/det_report.m index ba58bec32..2b68d4b7d 100644 --- a/compiler/det_report.m +++ b/compiler/det_report.m @@ -621,6 +621,10 @@ det_diagnose_goal_2(pragma_c_code(_, _, _, _, _, _, _), GoalInfo, Desired, % prog_out__write_context(Context), % io__write_string(" for modes which don't succeed more than once.\n"). +det_diagnose_goal_2(bi_implication(_, _), _, _, _, _, _, _) --> + % these should have been expanded out by now + { error("det_diagnose_goal_2: unexpected bi_implication") }. + %-----------------------------------------------------------------------------% :- pred report_generic_call_context(prog_context::in, diff --git a/compiler/dnf.m b/compiler/dnf.m index 142aeed7b..6e3e21657 100644 --- a/compiler/dnf.m +++ b/compiler/dnf.m @@ -240,6 +240,10 @@ dnf__transform_goal(Goal0, InstMap0, MaybeNonAtomic, ModuleInfo0, ModuleInfo, 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(MaybeNonAtomic, InNeg, InSome, ). 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. diff --git a/compiler/excess.m b/compiler/excess.m index 83cff6ee7..9391b637b 100644 --- a/compiler/excess.m +++ b/compiler/excess.m @@ -43,7 +43,7 @@ :- implementation. :- import_module hlds_goal, goal_util, prog_data, varset, term. -:- import_module list, bool, map, set, std_util. +:- import_module list, bool, map, set, std_util, require. %-----------------------------------------------------------------------------% @@ -137,6 +137,10 @@ excess_assignments_in_goal(GoalExpr0 - GoalInfo0, ElimVars0, Goal, ElimVars) :- GoalExpr0 = pragma_c_code(_, _, _, _, _, _, _), Goal = GoalExpr0 - GoalInfo0, ElimVars = ElimVars0 + ; + GoalExpr0 = bi_implication(_, _), + % these should have been expanded out by now + error("detect_cse_in_goal_2: unexpected bi_implication") ), !. diff --git a/compiler/follow_code.m b/compiler/follow_code.m index 6bb163a7f..5a75f55b9 100644 --- a/compiler/follow_code.m +++ b/compiler/follow_code.m @@ -125,6 +125,10 @@ move_follow_code_in_goal_2(unify(A,B,C,D,E), unify(A,B,C,D,E), _, R, R). move_follow_code_in_goal_2(pragma_c_code(A,B,C,D,E,F,G), pragma_c_code(A,B,C,D,E,F,G), _, R, R). +move_follow_code_in_goal_2(bi_implication(_, _), _, _, _, _) :- + % these should have been expanded out by now + error("move_follow_code_in_goal_2: unexpected bi_implication"). + %-----------------------------------------------------------------------------% % move_follow_code_in_disj is used both for disjunction and diff --git a/compiler/follow_vars.m b/compiler/follow_vars.m index a1a04623c..10fa2dc3a 100644 --- a/compiler/follow_vars.m +++ b/compiler/follow_vars.m @@ -202,6 +202,10 @@ find_follow_vars_in_goal_2(pragma_c_code(A,B,C,D,E,F,G), _, _ModuleInfo, FollowVars, pragma_c_code(A,B,C,D,E,F,G), FollowVars). +find_follow_vars_in_goal_2(bi_implication(_,_), _, _, _, _, _) :- + % these should have been expanded out by now + error("find_follow_vars_in_goal_2: unexpected bi_implication"). + %-----------------------------------------------------------------------------% :- pred find_follow_vars_in_call(pred_id, proc_id, list(prog_var), module_info, diff --git a/compiler/goal_path.m b/compiler/goal_path.m index 0bcbd4191..d78e8737d 100644 --- a/compiler/goal_path.m +++ b/compiler/goal_path.m @@ -21,7 +21,7 @@ :- implementation. :- import_module hlds_goal. -:- import_module int, list, std_util. +:- import_module int, list, std_util, require. goal_path__fill_slots(Proc0, _ModuleInfo, Proc) :- % The ModuleInfo argument is there just for passes_aux @@ -60,6 +60,9 @@ fill_expr_slots(generic_call(A,B,C,D), _Path0, generic_call(A,B,C,D)). fill_expr_slots(unify(A,B,C,D,E), _Path0, unify(A,B,C,D,E)). fill_expr_slots(pragma_c_code(A,B,C,D,E,F,G), _Path0, pragma_c_code(A,B,C,D,E,F,G)). +fill_expr_slots(bi_implication(_, _), _, _) :- + % these should have been expanded out by now + error("fill_expr_slots: unexpected bi_implication"). :- pred fill_conj_slots(list(hlds_goal)::in, goal_path::in, int::in, list(hlds_goal)::out) is det. diff --git a/compiler/goal_util.m b/compiler/goal_util.m index 48144da35..87aae377f 100644 --- a/compiler/goal_util.m +++ b/compiler/goal_util.m @@ -368,6 +368,11 @@ goal_util__name_apart_2(pragma_c_code(A,B,C,Vars0,E,F,G), Must, Subn, 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 @@ goal_util__goal_vars_2(pragma_c_code(_, _, _, ArgVars, _, _, _), 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(call(_, _, _, _, _, _), 1). 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. %-----------------------------------------------------------------------------% % diff --git a/compiler/higher_order.m b/compiler/higher_order.m index a5cd8fc84..b9d9cc7bc 100644 --- a/compiler/higher_order.m +++ b/compiler/higher_order.m @@ -478,6 +478,10 @@ traverse_goal_2(Goal, Goal) --> { Goal = unify(_, _, _, Unify, _) - _ }, check_unify(Unify). +traverse_goal_2(bi_implication(_, _) - _, _) --> + % these should have been expanded out by now + { error("traverse_goal_2: unexpected bi_implication") }. + % To process a disjunction, we process each disjunct with the % specialization information before the goal, then merge the % results to give the specialization information after the diff --git a/compiler/hlds_goal.m b/compiler/hlds_goal.m index 5e69b284c..21d37573e 100644 --- a/compiler/hlds_goal.m +++ b/compiler/hlds_goal.m @@ -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 @@ hlds_goal__generic_call_id(aditi_builtin(Builtin, Name), :- 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_goals(Goal1, Goal2, Goal) :- ), 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 @@ set_goal_contexts_2(_, Goal, Goal) :- 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). %-----------------------------------------------------------------------------% diff --git a/compiler/hlds_out.m b/compiler/hlds_out.m index fd731c541..f4c50fb0d 100644 --- a/compiler/hlds_out.m +++ b/compiler/hlds_out.m @@ -1539,6 +1539,21 @@ hlds_out__write_goal_2(pragma_c_code(_, _, _, ArgVars, ArgNames, _, 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. diff --git a/compiler/inlining.m b/compiler/inlining.m index 0342c6fcc..c5630907b 100644 --- a/compiler/inlining.m +++ b/compiler/inlining.m @@ -544,6 +544,10 @@ inlining__inlining_in_goal(unify(A, B, C, D, E) - GoalInfo, inlining__inlining_in_goal(pragma_c_code(A, B, C, D, E, F, G) - GoalInfo, pragma_c_code(A, B, C, D, E, F, G) - GoalInfo) --> []. +inlining__inlining_in_goal(bi_implication(_, _) - _, _) --> + % these should have been expanded out by now + { error("inlining__inlining_in_goal: unexpected bi_implication") }. + %-----------------------------------------------------------------------------% inlining__do_inline_call(HeadTypeParams, ArgVars, PredInfo, ProcInfo, diff --git a/compiler/intermod.m b/compiler/intermod.m index c15ae2452..3a624f99e 100644 --- a/compiler/intermod.m +++ b/compiler/intermod.m @@ -515,6 +515,11 @@ intermod__traverse_goal(if_then_else(Vars, Cond0, Then0, Else0, SM) - Info, intermod__traverse_goal(pragma_c_code(A,B,C,D,E,F,G) - Info, pragma_c_code(A,B,C,D,E,F,G) - Info, yes) --> []. +intermod__traverse_goal(bi_implication(_, _) - _, _, _) --> + % these should have been expanded out by now + { error("intermod__traverse_goal: unexpected bi_implication") }. + + :- pred intermod__traverse_list_of_goals(hlds_goals::in, hlds_goals::out, bool::out, intermod_info::in, intermod_info::out) is det. diff --git a/compiler/lambda.m b/compiler/lambda.m index fc028de72..3023a7d86 100644 --- a/compiler/lambda.m +++ b/compiler/lambda.m @@ -255,6 +255,9 @@ lambda__process_goal_2(call(A,B,C,D,E,F), GoalInfo, lambda__process_goal_2(pragma_c_code(A,B,C,D,E,F,G), GoalInfo, pragma_c_code(A,B,C,D,E,F,G) - GoalInfo) --> []. +lambda__process_goal_2(bi_implication(_, _), _, _) --> + % these should have been expanded out by now + { error("lambda__process_goal_2: unexpected bi_implication") }. :- pred lambda__process_goal_list(list(hlds_goal), list(hlds_goal), lambda_info, lambda_info). diff --git a/compiler/lco.m b/compiler/lco.m index 558648cdf..d8e89d303 100644 --- a/compiler/lco.m +++ b/compiler/lco.m @@ -94,6 +94,10 @@ lco_in_goal_2(unify(A,B,C,D,E), _ModuleInfo, unify(A,B,C,D,E)). lco_in_goal_2(pragma_c_code(A,B,C,D,E,F,G), _, pragma_c_code(A,B,C,D,E,F,G)). +lco_in_goal_2(bi_implication(_, _), _, _) :- + % these should have been expanded out by now + error("lco_in_goal_2: unexpected bi_implication"). + %-----------------------------------------------------------------------------% :- pred lco_in_disj(list(hlds_goal), module_info, list(hlds_goal)). diff --git a/compiler/live_vars.m b/compiler/live_vars.m index 6745bdcb2..7d15d1f71 100644 --- a/compiler/live_vars.m +++ b/compiler/live_vars.m @@ -397,6 +397,11 @@ build_live_sets_in_goal_2(pragma_c_code(Attributes, PredId, ProcId, ) ). +build_live_sets_in_goal_2(bi_implication(_, _), _, _, _, _, _, _, _, _, _, _) + :- + % these should have been expanded out by now + error("build_live_sets_in_goal_2: unexpected bi_implication"). + %-----------------------------------------------------------------------------% :- pred build_live_sets_in_conj(list(hlds_goal), set(prog_var), set(prog_var), diff --git a/compiler/liveness.m b/compiler/liveness.m index f386903cb..ec798647d 100644 --- a/compiler/liveness.m +++ b/compiler/liveness.m @@ -325,6 +325,9 @@ detect_liveness_in_goal_2(unify(_,_,_,_,_), _, _, _, _, _) :- detect_liveness_in_goal_2(pragma_c_code(_,_,_,_,_,_,_), _, _, _, _, _) :- error("pragma_c_code in detect_liveness_in_goal_2"). +detect_liveness_in_goal_2(bi_implication(_, _), _, _, _, _, _) :- + error("bi_implication in detect_liveness_in_goal_2"). + %-----------------------------------------------------------------------------% :- pred detect_liveness_in_conj(list(hlds_goal), set(prog_var), live_info, @@ -528,6 +531,9 @@ detect_deadness_in_goal_2(unify(_,_,_,_,_), _, _, _, _, _) :- detect_deadness_in_goal_2(pragma_c_code(_,_,_,_,_,_,_), _, _, _, _, _) :- error("pragma_c_code in detect_deadness_in_goal_2"). +detect_deadness_in_goal_2(bi_implication(_, _), _, _, _, _, _) :- + error("bi_implication in detect_deadness_in_goal_2"). + %-----------------------------------------------------------------------------% :- pred detect_deadness_in_conj(list(hlds_goal), set(prog_var), live_info, @@ -749,6 +755,10 @@ detect_resume_points_in_goal_2(pragma_c_code(A,B,C,D,E,F,G), _, Liveness, _, _, pragma_c_code(A,B,C,D,E,F,G), Liveness). +detect_resume_points_in_goal_2(bi_implication(_, _), _, _, _, _, _, _) :- + % these should have been expanded out by now + error("detect_resume_points_in_goal_2: unexpected bi_implication"). + :- pred detect_resume_points_in_conj(list(hlds_goal), set(prog_var), live_info, set(prog_var), list(hlds_goal), set(prog_var)). :- mode detect_resume_points_in_conj(in, in, in, in, out, out) is det. diff --git a/compiler/magic.m b/compiler/magic.m index 661ea8d5b..edce994d0 100644 --- a/compiler/magic.m +++ b/compiler/magic.m @@ -1546,6 +1546,10 @@ magic__preprocess_goal_2(Goal0, Goals, HOMap0, HOMap) --> { HOMap = HOMap0 } ). +magic__preprocess_goal_2(bi_implication(_, _) - _, _, _, _) --> + % these should have been expanded out by now + { error("magic__preprocess_goal_2: unexpected bi_implication") }. + % Introduce new variables and assignments to them for any % duplicates in the list. :- pred magic__preprocess_call_args(list(prog_var)::in, list(prog_var)::out, diff --git a/compiler/make_hlds.m b/compiler/make_hlds.m index b3549ed03..323fb0253 100644 --- a/compiler/make_hlds.m +++ b/compiler/make_hlds.m @@ -4014,6 +4014,12 @@ warn_singletons_in_goal_2(pragma_c_code(_, _, _, _, ArgInfo, _, PragmaImpl), 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(if_then(Vars0, A0, B0), Context, Subst, VarSet0, 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(implies(P, Q), Context, VarSet0, Subst, Goal, VarSet, 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) --> @@ -4802,18 +4798,6 @@ transform_goal_2(unify(A0, B0), Context, VarSet0, Subst, Goal, VarSet, 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" ; "aditi_delete" diff --git a/compiler/ml_code_gen.m b/compiler/ml_code_gen.m index 5ac5df789..8926bdc0a 100644 --- a/compiler/ml_code_gen.m +++ b/compiler/ml_code_gen.m @@ -1055,6 +1055,10 @@ ml_gen_goal_expr(pragma_c_code(_, _, _, _, _ArgNames, _, _PragmaCode), _, _, _, _) --> { sorry("C interface") }. +ml_gen_goal_expr(bi_implication(_, _), _, _, _, _) --> + % these should have been expanded out by now + { error("ml_gen_goal_expr: unexpected bi_implication") }. + %-----------------------------------------------------------------------------% % % Code for procedure calls diff --git a/compiler/mode_util.m b/compiler/mode_util.m index e375f485a..f1da7a42b 100644 --- a/compiler/mode_util.m +++ b/compiler/mode_util.m @@ -1211,6 +1211,10 @@ recompute_instmap_delta_2(_, pragma_c_code(A, PredId, ProcId, Args, E, F, recompute_instmap_delta_call(PredId, ProcId, Args, InstMap, InstMapDelta). +recompute_instmap_delta_2(_, bi_implication(_, _), _, _, _, _, _) --> + % these should have been expanded out by now + { error("recompute_instmap_delta_2: unexpected bi_implication") }. + %-----------------------------------------------------------------------------% :- pred recompute_instmap_delta_conj(bool, list(hlds_goal), list(hlds_goal), diff --git a/compiler/modes.m b/compiler/modes.m index 5d997f9a9..43f62546b 100644 --- a/compiler/modes.m +++ b/compiler/modes.m @@ -1184,6 +1184,10 @@ modecheck_goal_expr(pragma_c_code(IsRecursive, PredId, ProcId0, Args0, mode_info_unset_call_context, mode_checkpoint(exit, "pragma_c_code"). +modecheck_goal_expr(bi_implication(_, _), _, _) --> + % these should have been expanded out by now + { error("modecheck_goal_expr: unexpected bi_implication") }. + % given the right-hand-side of a unification, return a list of % the potentially non-local variables of that unification. diff --git a/compiler/notes/compiler_design.html b/compiler/notes/compiler_design.html index 92b59b425..ab5e905f6 100644 --- a/compiler/notes/compiler_design.html +++ b/compiler/notes/compiler_design.html @@ -206,6 +206,9 @@ stored in the io__state, using the type globals defined in globals.m. 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 @@ so that the compiler does the right thing for options such as
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.
checking typeclass instances (check_typeclass.m)
@@ -324,6 +330,8 @@ so that the compiler does the right thing for options such as 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.
polymorphism transformation @@ -1069,6 +1077,6 @@ Some of them are obsolete; other are work-in-progress.
-Last update was $Date: 1999-10-14 05:27:35 $ by $Author: conway $@cs.mu.oz.au.
+Last update was $Date: 1999-10-25 03:53:07 $ by $Author: fjh $@cs.mu.oz.au.
diff --git a/compiler/pd_cost.m b/compiler/pd_cost.m index 3da812e14..4acf62adf 100644 --- a/compiler/pd_cost.m +++ b/compiler/pd_cost.m @@ -36,7 +36,7 @@ :- implementation. :- import_module hlds_data, prog_data. -:- import_module int, list, set, std_util. +:- import_module int, list, set, std_util, require. %-----------------------------------------------------------------------------% @@ -103,6 +103,10 @@ pd_cost__goal(pragma_c_code(Attributes, _, _, Args, _, _, _) - _, Cost) :- pd_cost__reg_assign(AssignCost), Cost is Cost1 + Cost2 + AssignCost * InputArgs. +pd_cost__goal(bi_implication(_, _) - _, _) :- + % these should have been expanded out by now + error("pd_cost__goal: unexpected bi_implication"). + :- pred pd_cost__unify(set(prog_var)::in, unification::in, int::out) is det. pd_cost__unify(_, assign(_, _), 0). diff --git a/compiler/polymorphism.m b/compiler/polymorphism.m index 845cf18db..bf7989dab 100644 --- a/compiler/polymorphism.m +++ b/compiler/polymorphism.m @@ -1109,6 +1109,9 @@ polymorphism__process_goal_expr(if_then_else(Vars, A0, B0, C0, SM), GoalInfo, polymorphism__process_goal(A0, A), polymorphism__process_goal(B0, B), polymorphism__process_goal(C0, C). +polymorphism__process_goal_expr(bi_implication(_, _), _, _) --> + % these should have been expanded out by now + { error("polymorphism__process_goal_expr: unexpected bi_implication") }. :- pred polymorphism__process_unify(prog_var, unify_rhs, unify_mode, unification, unify_context, hlds_goal_info, diff --git a/compiler/post_typecheck.m b/compiler/post_typecheck.m index 8f500d4d9..31663b367 100644 --- a/compiler/post_typecheck.m +++ b/compiler/post_typecheck.m @@ -854,6 +854,9 @@ post_typecheck__resolve_data_cons_and_funcs(if_then_else(A,If0,Then0,Else0,E) ModuleInfo, PredInfo, Then), post_typecheck__resolve_data_cons_and_funcs(Else0, ModuleInfo, PredInfo, Else). +post_typecheck__resolve_data_cons_and_funcs(bi_implication(_, _) - _, _, _, _) :- + % these should have been expanded out by now + error("post_typecheck__resolve_data_cons_and_funcs: unexpected bi_implication"). :- 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. diff --git a/compiler/purity.m b/compiler/purity.m index 705ce0563..b96394a55 100644 --- a/compiler/purity.m +++ b/compiler/purity.m @@ -25,6 +25,10 @@ % 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 @@ -508,10 +512,21 @@ compute_expr_purity(disj(Goals0,Store), disj(Goals,Store), _, PredInfo, 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 @@ compute_expr_purity(Ccode, Ccode, _, _, ModuleInfo, _, Purity, { 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). diff --git a/compiler/quantification.m b/compiler/quantification.m index a96fe51fd..0cc102990 100644 --- a/compiler/quantification.m +++ b/compiler/quantification.m @@ -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 @@ implicitly_quantify_goal_2(pragma_c_code(A,B,C,Vars,E,F,G), _, 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. @@ -716,6 +796,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)). :- mode quantification__unify_rhs_vars(in, in, in, out, out) is det. diff --git a/compiler/rl_exprn.m b/compiler/rl_exprn.m index c4a8ec781..a5331dd93 100644 --- a/compiler/rl_exprn.m +++ b/compiler/rl_exprn.m @@ -668,6 +668,9 @@ rl_exprn__goal(pragma_c_code(_, _, _, _, _, _, _) - _, _, _) --> { error("rl_exprn__goal: pragma_c_code not yet implemented") }. rl_exprn__goal(some(_, _, Goal) - _, Fail, Code) --> rl_exprn__goal(Goal, Fail, Code). +rl_exprn__goal(bi_implication(_, _) - _, _, _) --> + % these should have been expanded out by now + { error("rl_exprn__goal: unexpected bi_implication") }. :- pred rl_exprn__cases(prog_var::in, list(case)::in, byte_tree::in, byte_tree::in, byte_tree::out, diff --git a/compiler/saved_vars.m b/compiler/saved_vars.m index db2d92259..bebef990b 100644 --- a/compiler/saved_vars.m +++ b/compiler/saved_vars.m @@ -42,7 +42,7 @@ :- import_module hlds_goal, hlds_out, goal_util, quantification, passes_aux. :- import_module mode_util, prog_data, term, varset. -:- import_module bool, list, set, map, std_util. +:- import_module bool, list, set, map, std_util, require. %-----------------------------------------------------------------------------% @@ -137,6 +137,10 @@ saved_vars_in_goal(GoalExpr0 - GoalInfo0, SlotInfo0, Goal, SlotInfo) :- GoalExpr0 = pragma_c_code(_, _, _, _, _, _, _), Goal = GoalExpr0 - GoalInfo0, SlotInfo = SlotInfo0 + ; + GoalExpr0 = bi_implication(_, _), + % these should have been expanded out by now + error("saved_vars_in_goal: unexpected bi_implication") ), !. @@ -373,6 +377,10 @@ saved_vars_delay_goal([Goal0 | Goals0], Construct, Var, IsNonLocal, SlotInfo0, saved_vars_delay_goal(Goals0, Construct, Var, IsNonLocal, SlotInfo3, Goals1, SlotInfo), Goals = [Goal1 | Goals1] + ; + Goal0Expr = bi_implication(_, _), + % these should have been expanded out by now + error("saved_vars_delay_goal: unexpected bi_implication") ) ; saved_vars_delay_goal(Goals0, Construct, Var, IsNonLocal, diff --git a/compiler/simplify.m b/compiler/simplify.m index ca838e86a..dc19eb54b 100644 --- a/compiler/simplify.m +++ b/compiler/simplify.m @@ -1059,6 +1059,10 @@ simplify__goal_2(Goal0, GoalInfo, Goal, GoalInfo, Info0, Info) :- Goal = Goal0 ). +simplify__goal_2(bi_implication(_, _), _, _, _, _, _) :- + % these should have been expanded out by now + error("simplify__goal_2: unexpected bi_implication"). + %-----------------------------------------------------------------------------% :- pred simplify__process_compl_unify(prog_var, prog_var, diff --git a/compiler/store_alloc.m b/compiler/store_alloc.m index 4e5a682a0..f942e5d00 100644 --- a/compiler/store_alloc.m +++ b/compiler/store_alloc.m @@ -206,6 +206,10 @@ store_alloc_in_goal_2(unify(A,B,C,D,E), Liveness, _, _, store_alloc_in_goal_2(pragma_c_code(A, B, C, D, E, F, G), Liveness, _, _, _, pragma_c_code(A, B, C, D, E, F, G), Liveness). +store_alloc_in_goal_2(bi_implication(_, _), _, _, _, _, _, _) :- + % these should have been expanded out by now + error("store_alloc_in_goal_2: unexpected bi_implication"). + %-----------------------------------------------------------------------------% :- pred store_alloc_in_conj(list(hlds_goal), liveness_info, set(prog_var), diff --git a/compiler/stratify.m b/compiler/stratify.m index 87891faa3..e39dbfd31 100644 --- a/compiler/stratify.m +++ b/compiler/stratify.m @@ -212,6 +212,9 @@ first_order_check_goal(call(CPred, CProc, _Args, _BuiltinState, _Contex, _Sym), first_order_check_goal(generic_call(_Var, _Vars, _Modes, _Det), _GInfo, _Negated, _WholeScc, _ThisPredProcId, _Error, Module, Module) --> []. +first_order_check_goal(bi_implication(_, _), _, _, _, _, _, _, _) --> + % these should have been expanded out by now + { error("first_order_check_goal: unexpected bi_implication") }. :- pred first_order_check_goal_list(list(hlds_goal), bool, list(pred_proc_id), pred_proc_id, bool, module_info, @@ -377,6 +380,9 @@ higher_order_check_goal(generic_call(GenericCall, _Vars, _Modes, _Det), ; { Module = Module0 } ). +higher_order_check_goal(bi_implication(_, _), _, _, _, _, _, _, _, _) --> + % these should have been expanded out by now + { error("higher_order_check_goal: unexpected bi_implication") }. :- pred higher_order_check_goal_list(list(hlds_goal), bool, set(pred_proc_id), pred_proc_id, bool, bool, module_info, module_info, @@ -817,6 +823,10 @@ check_goal1(not(Goal - _GoalInfo), Calls0, Calls, HasAT0, HasAT, CallsHO0, check_goal1(pragma_c_code(_IsRec, _CPred, _CProc, _, _, _, _), Calls, Calls, HasAT, HasAT, CallsHO, CallsHO). + +check_goal1(bi_implication(_, _), _, _, _, _, _, _) :- + % these should have been expanded out by now + error("check_goal1: unexpected bi_implication"). :- pred check_goal_list(list(hlds_goal), set(pred_proc_id), set(pred_proc_id), set(pred_proc_id), set(pred_proc_id), bool, bool). @@ -904,6 +914,9 @@ get_called_procs(not(Goal - _GoalInfo), Calls0, Calls) :- get_called_procs(Goal, Calls0, Calls). get_called_procs(pragma_c_code(_IsRec, _CPred, _CProc, _, _, _, _), Calls, Calls). +get_called_procs(bi_implication(_, _), _, _) :- + % these should have been expanded out by now + error("get_called_procs: unexpected bi_implication"). :- pred check_goal_list(list(hlds_goal), list(pred_proc_id), list(pred_proc_id)). diff --git a/compiler/switch_detection.m b/compiler/switch_detection.m index 0bb92b844..4477705a5 100644 --- a/compiler/switch_detection.m +++ b/compiler/switch_detection.m @@ -218,6 +218,9 @@ detect_switches_in_goal_2(switch(Var, CanFail, Cases0, SM), _, InstMap, detect_switches_in_goal_2(pragma_c_code(A,B,C,D,E,F,G), _, _, _, _, pragma_c_code(A,B,C,D,E,F,G)). +detect_switches_in_goal_2(bi_implication(_, _), _, _, _, _, _) :- + % these should have been expanded out by now + error("detect_switches_in_goal_2: unexpected bi_implication"). %-----------------------------------------------------------------------------% diff --git a/compiler/term_traversal.m b/compiler/term_traversal.m index 759955713..3503cdde9 100644 --- a/compiler/term_traversal.m +++ b/compiler/term_traversal.m @@ -288,6 +288,10 @@ traverse_goal_2(call(CallPredId, CallProcId, Args, _, _, _), Info = Info3 ). +traverse_goal_2(bi_implication(_, _), _, _, _, _) :- + % these should have been expanded out by now + error("traverse_goal_2traverse_goal_2: unexpected bi_implication"). + %-----------------------------------------------------------------------------% % Traverse_conj should be invoked with a reversed list of goals. diff --git a/compiler/typecheck.m b/compiler/typecheck.m index 41f12b426..d6b70f8db 100644 --- a/compiler/typecheck.m +++ b/compiler/typecheck.m @@ -978,6 +978,10 @@ typecheck_goal_2(pragma_c_code(A, PredId, C, Args, E, F, G), 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). %-----------------------------------------------------------------------------% diff --git a/compiler/unique_modes.m b/compiler/unique_modes.m index e251c2bd8..5995fec1c 100644 --- a/compiler/unique_modes.m +++ b/compiler/unique_modes.m @@ -499,6 +499,10 @@ unique_modes__check_goal_2(pragma_c_code(IsRecursive, PredId, ProcId0, mode_info_unset_call_context, mode_checkpoint(exit, "pragma_c_code"). +unique_modes__check_goal_2(bi_implication(_, _), _, _) --> + % these should have been expanded out by now + { error("unique_modes__check_goal_2: unexpected bi_implication") }. + :- pred unique_modes__check_call(pred_id, proc_id, list(prog_var), proc_id, mode_info, mode_info). :- mode unique_modes__check_call(in, in, in, out, diff --git a/compiler/unused_args.m b/compiler/unused_args.m index 7d309b2e1..db58bdd33 100644 --- a/compiler/unused_args.m +++ b/compiler/unused_args.m @@ -523,6 +523,10 @@ traverse_goal(_, unify(Var, Rhs, _, complicated_unify(_, _, _), _), error("complicated unifications should only be var-var") ). +traverse_goal(_, bi_implication(_, _), _, _) :- + % these should have been expanded out by now + error("traverse_goal: unexpected bi_implication"). + % add PredProc - HeadVar as an alias for the same element of Args. :- pred add_pred_call_arg_dep(pred_proc_id::in, list(prog_var)::in, list(prog_var)::in, var_dep::in, var_dep::out) is det. @@ -1287,6 +1291,10 @@ fixup_goal_expr(_ModuleInfo, _UnusedVars, _ProcCallInfo, no, GoalExpr - GoalInfo, GoalExpr - GoalInfo) :- GoalExpr = pragma_c_code(_, _, _, _, _, _, _). +fixup_goal_expr(_, _, _, _, bi_implication(_, _) - _, _) :- + % these should have been expanded out by now + error("fixup_goal_expr: unexpected bi_implication"). + % Remove useless unifications from a list of conjuncts. :- pred fixup_conjuncts(module_info::in, list(prog_var)::in, proc_call_info::in, bool::in, bool::out, hlds_goals::in, hlds_goals::out) is det. diff --git a/tests/hard_coded/Mmakefile b/tests/hard_coded/Mmakefile index 17eff01f3..f1509c954 100644 --- a/tests/hard_coded/Mmakefile +++ b/tests/hard_coded/Mmakefile @@ -80,6 +80,7 @@ PROGS= \ qual_basic_test \ qual_is_test \ quantifier \ + quantifier2 \ quoting_bug_test \ rational_test \ relation_test \ diff --git a/tests/hard_coded/quantifier2.exp b/tests/hard_coded/quantifier2.exp new file mode 100644 index 000000000..7cfab5b05 --- /dev/null +++ b/tests/hard_coded/quantifier2.exp @@ -0,0 +1 @@ +yes diff --git a/tests/hard_coded/quantifier2.m b/tests/hard_coded/quantifier2.m new file mode 100644 index 000000000..9fe2626d3 --- /dev/null +++ b/tests/hard_coded/quantifier2.m @@ -0,0 +1,37 @@ +:- 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 + ). +