[m-rev.] diff: attempt at sequence quantification (2)
Adrian Pellas-Rice
apell at students.cs.mu.oz.au
Tue Apr 10 03:33:58 AEST 2001
Index: mercury/library/ops.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/ops.m,v
retrieving revision 1.32
diff -u -d -r1.32 ops.m
--- mercury/library/ops.m 2000/09/19 04:46:50 1.32
+++ mercury/library/ops.m 2001/04/08 13:34:36
@@ -231,6 +231,9 @@
ops__op_table("where", after, xfx, 1175). % NU-Prolog extension (*)
ops__op_table("~", before, fy, 900). % Goedel (*)
ops__op_table("~=", after, xfx, 700). % NU-Prolog (*)
+ops__op_table("forall", before, fy, 999). % XXX sequence quantification
+ops__op_table("fin", after, xfx, 800). % XXX sequence quantification
+ops__op_table("as", after, xfx, 850). % XXX sequence quantification
% (*) means that the operator is not useful in Mercury
% and is provided only for compatibility.
Index: mercury/compiler/add_trail_ops.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/add_trail_ops.m,v
retrieving revision 1.3
diff -u -d -r1.3 add_trail_ops.m
--- mercury/compiler/add_trail_ops.m 2001/04/07 14:04:30 1.3
+++ mercury/compiler/add_trail_ops.m 2001/04/08 03:52:02
@@ -275,6 +275,8 @@
% these should have been expanded out by now
{ error("goal_expr_add_trail_ops: unexpected shorthand") }.
+
+
:- pred conj_add_trail_ops(hlds_goals::in, hlds_goals::out,
trail_ops_info::in, trail_ops_info::out) is det.
conj_add_trail_ops(Goals0, Goals) -->
Index: mercury/compiler/assertion.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/assertion.m,v
retrieving revision 1.13
diff -u -d -r1.13 assertion.m
--- mercury/compiler/assertion.m 2001/04/07 14:04:31 1.13
+++ mercury/compiler/assertion.m 2001/04/08 04:39:16
@@ -569,6 +569,18 @@
equal_goals(LeftGoalA, LeftGoalB, Subst0, Subst1),
equal_goals(RightGoalA, RightGoalB, Subst1, Subst).
+ % XXX ? sequence quantification code
+equal_goals_shorthand(forall(X) - GI, forall(X) - GI, Subst, Subst) :-
+ X = sequence_pre_patch(_,_,_,_,_,_,_),
+ error("assertion.m: equal_shorthand_goals should not be called on untransformed quantified sequences.").
+
+
+equal_goals_shorthand(forall(X) - GI, forall(X) - GI, Subst, Subst) :-
+ X = sequence_mid_patch(_,_,_,_,_,_),
+ error("assertion.m: equal_shorthand_goals should not be called on partly transformed quantified sequences.").
+
+
+
:- pred equal_vars(prog_vars::in, prog_vars::in, subst::in,
subst::out) is semidet.
@@ -699,7 +711,16 @@
bi_implication(LHS, RHS) - GI) :-
assertion__normalise_goal(LHS0, LHS),
assertion__normalise_goal(RHS0, RHS).
+assertion__normalise_goal_shorthand(forall(
+ sequence_pre_patch(ImplemCall0,A,B,ImplemGoal0,D,E,F)) - GI,
+ forall(sequence_pre_patch(ImplemCall,A,B,ImplemGoal,D,E,F))
+ - GI) :-
+ assertion__normalise_goal(ImplemCall0, ImplemCall),
+ assertion__normalise_goal(ImplemGoal0, ImplemGoal).
+assertion__normalise_goal_shorthand(forall(X) - GI, forall(X) - GI) :-
+ X = sequence_mid_patch(_,_,_,_,_,_),
+ error("assertion.m: Should not assert about partially transformed quantified sequences.").
%-----------------------------------------------------------------------------%
@@ -802,6 +823,13 @@
Module0, Module) -->
assertion__in_interface_check(LHS, PredInfo, Module0, Module1),
assertion__in_interface_check(RHS, PredInfo, Module1, Module).
+
+ % XXX sequence quantification
+assertion__in_interface_check_shorthand(forall(_), _, _, _) -->
+ {error("Assertions not yet implemented for sequence quantification.")}.
+
+
+
%-----------------------------------------------------------------------------%
Index: mercury/compiler/code_info.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/code_info.m,v
retrieving revision 1.263
diff -u -d -r1.263 code_info.m
--- mercury/compiler/code_info.m 2001/03/06 05:51:21 1.263
+++ mercury/compiler/code_info.m 2001/04/08 12:13:09
@@ -3575,13 +3575,14 @@
;
{ VarInfo0 = var_locn_info(VarLocnInfo0) },
{ code_info__var_arg_info_to_lval(InArgInfos, InArgLocs) },
+%% XXX BUG AFTER HERE:
{ list__append(StackVarLocs, InArgLocs, AllLocs) },
{ var_locn__place_vars(AllLocs, Code,
VarLocnInfo0, VarLocnInfo) },
code_info__set_var_locns_info(var_locn_info(VarLocnInfo)),
{ assoc_list__values(AllLocs, LiveLocList) },
{ set__list_to_set(LiveLocList, LiveLocs) }
-
+%% XXX AND VERY PROBABLY BEFORE HERE (in fact, certainly):
% { assoc_list__keys(InArgLocs, InArgVars) },
% { set__init(DeadVars0) },
% code_info__which_variables_are_forward_live(InArgVars,
Index: mercury/compiler/code_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/code_util.m,v
retrieving revision 1.131
diff -u -d -r1.131 code_util.m
--- mercury/compiler/code_util.m 2001/04/07 14:04:32 1.131
+++ mercury/compiler/code_util.m 2001/04/08 05:02:57
@@ -512,6 +512,11 @@
;
code_util__goal_may_allocate_heap(G2, May)
).
+ % XXX This is a conservative assumption; whether forall(...) goals can
+ % ever _not_ allocate heap has not yet been explored, so we just assume
+ % they always can.
+code_util__goal_may_allocate_heap_2_shorthand(forall(_), yes).
+
@@ -597,6 +602,11 @@
;
code_util__goal_may_alloc_temp_frame(G2, May)
).
+ % XXX Another conservative assumption: We have not yet worked out if a
+ % forall(...) goal can ever _not_ allocate a temp frame, so we just
+ % assume that it always may.
+code_util__goal_may_alloc_temp_frame_2_shorthand(forall(_), yes).
+
:- pred code_util__goal_list_may_alloc_temp_frame(list(hlds_goal)::in,
@@ -858,8 +868,7 @@
CTMax is CMax + TMax,
int__min(CTMin, EMin, Min),
int__max(CTMax, EMax, Max).
-code_util__count_recursive_calls_2(shorthand(_),
- _, _, _, _) :-
+code_util__count_recursive_calls_2(shorthand(_), _, _, _, _) :-
% these should have been expanded out by now
error("code_util__count_recursive_calls_2: unexpected shorthand").
Index: mercury/compiler/dead_proc_elim.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/dead_proc_elim.m,v
retrieving revision 1.65
diff -u -d -r1.65 dead_proc_elim.m
--- mercury/compiler/dead_proc_elim.m 2001/04/07 14:04:33 1.65
+++ mercury/compiler/dead_proc_elim.m 2001/04/08 03:52:07
@@ -889,6 +889,7 @@
% these should have been expanded out by now
{ error("pre_modecheck_examine_goal: unexpected shorthand") }.
+
:- pred pre_modecheck_examine_unify_rhs(unify_rhs::in,
dead_pred_info::in, dead_pred_info::out) is det.
Index: mercury/compiler/dependency_graph.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/dependency_graph.m,v
retrieving revision 1.53
diff -u -d -r1.53 dependency_graph.m
--- mercury/compiler/dependency_graph.m 2001/04/07 14:04:34 1.53
+++ mercury/compiler/dependency_graph.m 2001/04/08 05:44:02
@@ -365,6 +365,16 @@
Caller, DepGraph0, DepGraph) :-
dependency_graph__add_arcs_in_list([LHS, RHS], Caller,
DepGraph0, DepGraph).
+ % XXX Hmmm... I could be wrong but I suspect that if a
+ % dependency graph is being constructed from a hlds that still
+ % has quantified sequences in it, serious ill is afoot. Should
+ % this not be the case, then we should make sure that after the
+ % shorthand representation of a quantified sequence is expanded
+ % away in `quantification.m' any lingering dependency graphs
+ % are marked as invalid.
+dependency_graph__add_arcs_in_goal_2_shorthand(forall(_), _, DepGraph,
+ DepGraph) :-
+ error("dependency_graph__add_arcs_in_goal_2: sequence quantification not yet handled.").
%-----------------------------------------------------------------------------%
Index: mercury/compiler/dnf.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/dnf.m,v
retrieving revision 1.44
diff -u -d -r1.44 dnf.m
--- mercury/compiler/dnf.m 2001/04/07 14:04:36 1.44
+++ mercury/compiler/dnf.m 2001/04/08 05:46:27
@@ -480,10 +480,12 @@
ShorthandGoal, IsAtomic).
+
:- pred dnf__is_atomic_expr_shorthand(maybe(set(pred_proc_id))::in, bool::in,
bool::in, shorthand_goal_expr::in, bool::out) is det.
dnf__is_atomic_expr_shorthand(_, _, _, bi_implication(_,_), no).
+dnf__is_atomic_expr_shorthand(_, _, _, forall(_), no).
:- pred dnf__free_of_nonatomic(hlds_goal::in,
Index: mercury/compiler/goal_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/goal_util.m,v
retrieving revision 1.69
diff -u -d -r1.69 goal_util.m
--- mercury/compiler/goal_util.m 2001/04/07 14:04:37 1.69
+++ mercury/compiler/goal_util.m 2001/04/08 04:15:56
@@ -392,6 +392,26 @@
goal_util__rename_vars_in_goal(LHS0, Must, Subn, LHS),
goal_util__rename_vars_in_goal(RHS0, Must, Subn, RHS).
+ % XXX Observe that SuffixArgs should be renamed apart precisely when
+ % ImplemGoal is renamed apart, because SuffixArgs will eventually be
+ % used in ImplemGoal.
+goal_util__name_apart_2_shorthand(forall(sequence_mid_patch(ImplemCall0,
+ SuffixArgs0, ImplemGoal0, HeadVars, VarSet, Context)),
+ Must, Subn, forall(sequence_mid_patch(ImplemCall,
+ SuffixArgs, ImplemGoal, HeadVars, VarSet, Context))) :-
+ goal_util__rename_vars_in_goal(ImplemCall0, Must, Subn, ImplemCall),
+ goal_util__rename_vars_in_goal(ImplemGoal0, Must, Subn, ImplemGoal),
+ goal_util__rename_var_list(SuffixArgs0, Must, Subn, SuffixArgs).
+
+ % Attempting to rename apart un-expanded quantified sequences is
+ % likely to require changes elsewhere:
+goal_util__name_apart_2_shorthand(forall(X), _Must, _Subn,
+ forall(X)) :-
+ X = sequence_pre_patch(_,_,_,_,_,_,_),
+ error("goal_util.m: Cannot rename apart fully unexpanded sequence quantifications.").
+
+
+
%-----------------------------------------------------------------------------%
:- pred goal_util__name_apart_list(list(hlds_goal), bool,
@@ -637,8 +657,25 @@
goal_util__goal_vars_2(LHS, Set0, Set1),
goal_util__goal_vars_2(RHS, Set1, Set).
+ % As usual with sequence quantification, it's a little contentious
+ % whether or not we should return the variables that appear in the
+ % implementation goal. As also usual, we just do what works(?) (which
+ % at present is assumed to be including the implementation goal).
+goal_util__goal_vars_2_shorthand(forall(sequence_pre_patch(_ImplemCall,
+ ElemTerms, SourceTerms, ImplemGoalExpr - _, _HeadVars,
+ _VarSet,_Context)),Set0,Set) :-
+ term__vars_list(ElemTerms, ElemVars),
+ set__insert_list(Set0, ElemVars, Set1),
+ term__vars_list(SourceTerms, SourceVars),
+ set__insert_list(Set1, SourceVars, Set2),
+ goal_util__goal_vars_2(ImplemGoalExpr, Set2, Set).
+goal_util__goal_vars_2_shorthand(forall(X), Set, Set) :-
+ X = sequence_mid_patch(_,_,_,_,_,_),
+ error("goal_util.m: Should not extract vars from partially transformed quantified sequence.").
+
+
goal_util__goals_goal_vars([], Set, Set).
goal_util__goals_goal_vars([Goal - _ | Goals], Set0, Set) :-
goal_util__goal_vars_2(Goal, Set0, Set1),
@@ -786,6 +823,12 @@
goal_size(LHS, Size1),
goal_size(RHS, Size2),
Size is Size1 + Size2 + 1.
+
+ % TODO XXX The handling of the forall case may wind up with a very
+ % arbitrary decision about the `size' of a sequence. Tom should be
+ % consulted prior to final commit.
+goal_expr_size_shorthand(forall(_),1) :-
+ error("goal_util.m: goal_expr_size_shorthand is not yet implemented.").
%-----------------------------------------------------------------------------%
%
Index: mercury/compiler/hlds_goal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_goal.m,v
retrieving revision 1.87
diff -u -d -r1.87 hlds_goal.m
--- mercury/compiler/hlds_goal.m 2001/04/07 14:04:39 1.87
+++ mercury/compiler/hlds_goal.m 2001/04/08 06:00:57
@@ -216,10 +216,53 @@
% of bi-implications is done before implicit quantification,
% then the quantification would be wrong
---> bi_implication(hlds_goal, hlds_goal)
- .
-
+ % quantified sequences (forall X in DS ...)
+ ;
+ forall(hlds_sequence).
+
+
+:- type hlds_sequence
+ ---> sequence_pre_patch(
+ hlds_goal,
+ % the unrepaired call to the implementation
+ % predicate
+ list(prog_term),
+ % elemental terms
+ list(prog_term),
+ % source terms
+ hlds_goal,
+ % the unrepaired implementation predicate's body
+ list(prog_var),
+ % the head vars in the implementation goal
+ prog_varset,
+ % the varset for the implementation goal
+ prog_context
+ % the context (ie. filename/line number) of the
+ % quantified sequence
+ )
+ ; sequence_mid_patch(
+ hlds_goal,
+ % the unrepaired call to the implementation
+ % predicate
+ list(prog_var),
+ % the arguments suffixed to the makeshift list
+ % of arguments in order to make it complete
+ hlds_goal,
+ % the unrepaired implementation predicate's body
+ list(prog_var),
+ % the head vars in the implementation goal
+ prog_varset,
+ % the varset for the implementation goal
+ prog_context
+ % the context (ie. filename/line number) of the
+ % quantified sequence
+
+ ).
+
+
+
%-----------------------------------------------------------------------------%
%
% Information for generic_calls
@@ -560,8 +603,6 @@
% Each pair represents the insts
% of the LHS and the RHS respectively
-
-
%-----------------------------------------------------------------------------%
%
% Information for all kinds of goals
@@ -1544,6 +1585,7 @@
).
+
% Return yes if the shorthand goal contains any foreign code
:- func goal_has_foreign_shorthand(shorthand_goal_expr) = bool.
:- mode goal_has_foreign_shorthand(in) = out is det.
@@ -1557,6 +1599,8 @@
; no
).
+goal_has_foreign_shorthand(forall(_)) = no :-
+ error("hlds_goal: not implemented.").
goal_list_has_foreign([]) = no.
@@ -1683,7 +1727,20 @@
bi_implication(LHS, RHS)) :-
set_goal_contexts(Context, LHS0, LHS),
set_goal_contexts(Context, RHS0, RHS).
-
+set_goal_contexts_2_shorthand(Context,
+ forall(sequence_pre_patch(A0, B, C, D0, E, F, G)),
+ forall(sequence_pre_patch(A, B, C, D, E, F, G))) :-
+ % XXX there is no guarantee this works as desired.
+ set_goal_contexts(Context, A0, A),
+ set_goal_contexts(Context, D0, D).
+set_goal_contexts_2_shorthand(_Context, forall(X), forall(X)) :-
+ X = sequence_mid_patch(_,_,_,_,_,_),
+ error("hlds_goal.m: set_goal_contexts_2_shorthand is not implemented for use during transformation.").
+ % I can't see any reason why it couldn't be, but my gut instinct is
+ % that it's best to discourage people from messing around with the hlds
+ % too much between quantification and the purging of sequence
+ % quantification, and this is a discouragement.
+
%-----------------------------------------------------------------------------%
create_atomic_unification(A, B, Context, UnifyMainContext, UnifySubContext,
Index: mercury/compiler/hlds_module.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_module.m,v
retrieving revision 1.65
diff -u -d -r1.65 hlds_module.m
--- mercury/compiler/hlds_module.m 2001/02/27 21:42:55 1.65
+++ mercury/compiler/hlds_module.m 2001/04/08 12:20:18
@@ -1194,6 +1194,16 @@
module_info, pred_id).
:- mode get_pred_id(in, in, in, in, in, out) is semidet.
+ % XXX this predicate may allow the violation of invariants
+ % that are supposed to hold for the predicate table &/ pred ids.
+ % (Esp. invariants of the undocumented variety.)
+
+:- pred predicate_table_next_pred_id(predicate_table, pred_id).
+:- mode predicate_table_next_pred_id(in, out) is det.
+
+
+
+
%-----------------------------------------------------------------------------%
:- implementation.
@@ -1827,3 +1837,5 @@
pred_info_arity(PredInfo, Arity).
%-----------------------------------------------------------------------------%
+
+predicate_table_next_pred_id(predicate_table(_,NextID,_,_,_,_,_,_,_), NextID).
Index: mercury/compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.258
diff -u -d -r1.258 hlds_out.m
--- mercury/compiler/hlds_out.m 2001/04/07 14:04:40 1.258
+++ mercury/compiler/hlds_out.m 2001/04/08 04:36:00
@@ -846,12 +846,14 @@
% Never write the clauses out verbosely -
% disable the dump_hlds_options option before writing
% them, and restore its initial value afterwards
- globals__io_set_option(dump_hlds_options, string("")),
+ % XXX that's wrong -- we need to write the clauses out
+ % verbosely, especially for passes before mode analysis
+ % globals__io_set_option(dump_hlds_options, string("")),
hlds_out__write_clauses(Indent, ModuleInfo, PredId,
VarSet, AppendVarnums, HeadVars, PredOrFunc,
- Clauses, no),
- globals__io_set_option(dump_hlds_options,
- string(Verbose))
+ Clauses, no)
+ % globals__io_set_option(dump_hlds_options,
+ % string(Verbose))
;
[]
)
@@ -1646,6 +1648,63 @@
hlds_out__write_indent(Indent),
io__write_string(")"),
io__write_string(Follow).
+
+ % XXX This predicate doesn't output valid mercury syntax.
+hlds_out__write_goal_2_shorthand(forall(
+ sequence_pre_patch(ImplemCall, ElemTerms, SourceTerms,
+ ImplemGoal, _HeadVars, ImplemGoalVarSet, _Context)),
+ ModuleInfo, VarSet, AppendVarnums, Indent, Follow,
+ _TypeQual) -->
+ hlds_out__write_indent(Indent),
+ io__write_string("% quantified sequence\n"),
+
+ globals__io_lookup_string_option(dump_hlds_options, Verbose),
+ ( { string__contains_char(Verbose, 'l') } ->
+ io__write_string("% pred id is not available for quantified sequence prior to expansion"),
+ io__write_string("\n")
+ ;
+ []
+ ),
+
+ % XXX This is not valid Mercury syntax as output
+
+ hlds_out__write_indent(Indent),
+ io__write_string("% elem vars:\n"),
+ io__write_list(ElemTerms, ", ", (pred(ElemTerm::in, di, uo) is det -->
+ mercury_output_term(ElemTerm, VarSet, AppendVarnums))),
+ io__nl,
+
+ io__write_string("% source terms:\n"),
+ io__write_list(SourceTerms, ", ", (pred(SourceTerm::in, di, uo)
+ is det -->
+ mercury_output_term(SourceTerm, VarSet, AppendVarnums))
+ ),
+ io__nl,
+
+ hlds_out__write_indent(Indent),
+ io__write_string("% implementation call:\n"),
+ io__write_string("(\n"),
+ { Indent1 is Indent + 1 },
+ hlds_out__write_goal(ImplemCall, ModuleInfo, VarSet, AppendVarnums,
+ Indent1, "\n"),
+ hlds_out__write_indent(Indent),
+ io__write_string(")"),
+
+ hlds_out__write_indent(Indent),
+ io__write_string("% implementation goal's body:\n"),
+ io__write_string("(\n"),
+ hlds_out__write_goal(ImplemGoal, ModuleInfo, ImplemGoalVarSet,
+ AppendVarnums, Indent1, "\n"),
+ hlds_out__write_indent(Indent),
+ io__write_string(")"),
+
+ io__write_string(Follow).
+
+% Obviously this limitation needs to changed XXX
+hlds_out__write_goal_2_shorthand(forall(X), _ModuleInfo, _VarSet,
+ _AppendVarnums, _Indent, _Follow, _TypeQual) -->
+ { X = sequence_mid_patch(_,_,_,_,_,_) },
+ { error("Should not try to output partially patched hlds goal.\n") }.
Index: mercury/compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.368
diff -u -d -r1.368 make_hlds.m
--- mercury/compiler/make_hlds.m 2001/04/07 14:04:45 1.368
+++ mercury/compiler/make_hlds.m 2001/04/08 12:47:16
@@ -132,6 +132,7 @@
% efficiency, so we return it to the correct order here.
{ module_info_reverse_predids(Module5, Module) }.
+
%-----------------------------------------------------------------------------%
% When adding an item to the HLDS we need to know both its
@@ -160,10 +161,9 @@
% Add the type definitions and pragmas one by one to the module,
% and add default modes for functions with no mode declaration.
%
- % Adding type definitions needs to come after we have added the
- % pred declarations,
- % since we need to have the pred_id for `index/2' and `compare/3'
- % when we add compiler-generated clauses for `compare/3'.
+ % Adding type definitions needs to come after we have added the pred
+ % declarations, since we need to have the pred_id for `index/2' and
+ % `compare/3' when we add compiler-generated clauses for `compare/3'.
% (And similarly for other compiler-generated predicates like that.)
%
% Adding pragmas needs to come after we have added the
@@ -3639,8 +3639,10 @@
;
PredInfo = PredInfo6
),
- map__det_update(Preds0, PredId, PredInfo, Preds),
- predicate_table_set_preds(PredicateTable2, Preds,
+ module_info_get_predicate_table(ModuleInfo2, PredicateTable3),
+ predicate_table_get_preds(PredicateTable3, Preds3),
+ map__det_update(Preds3, PredId, PredInfo, Preds),
+ predicate_table_set_preds(PredicateTable3, Preds,
PredicateTable),
module_info_set_predicate_table(ModuleInfo2, PredicateTable,
ModuleInfo)
@@ -4590,8 +4592,21 @@
QuantVars, VarSet, PredCallId, MI) -->
warn_singletons_in_goal_list([LHS, RHS], QuantVars, VarSet,
PredCallId, MI).
-
+ % XXX this won't work in practice, but it's a close enough
+ % approximation for the time being.
+warn_singletons_in_goal_2_shorthand(forall(
+ sequence_pre_patch(ImplemCall,_,_,ImplemGoal,_,_,_)),
+ _GoalInfo, QuantVars, VarSet, PredCallId, MI) -->
+ warn_singletons_in_goal(ImplemCall, QuantVars, VarSet, PredCallId, MI),
+ warn_singletons_in_goal(ImplemGoal, QuantVars, VarSet, PredCallId, MI).
+
+warn_singletons_in_goal_2_shorthand(forall(X), _,_,_,_,_) -->
+ { X = sequence_mid_patch(_,_,_,_,_,_) },
+ { error("make_hlds.m: Attempt to warn about singletons in a partially transformed goal.") }.
+
+
+
:- pred warn_singletons_in_goal_list(list(hlds_goal), set(prog_var),
prog_varset, simple_call_id, module_info,
io__state, io__state).
@@ -5209,15 +5224,16 @@
->
{ VarSet2 = VarSet1 },
{ Goal2 = Goal1 },
- { Info = Info0 }
+ { Info2 = Info1 }
;
{ ArgContext = head(PredOrFunc, Arity) },
insert_arg_unifications(HeadVars, Args, Context, ArgContext,
- no, Goal1, VarSet1, Goal2, VarSet2, Info1, Info)
+ no, Goal1, VarSet1, Goal2, VarSet2, Info1, Info2)
),
{ map__init(EmptyVarTypes) },
{ implicitly_quantify_clause_body(HeadVars,
- Goal2, VarSet2, EmptyVarTypes, Goal, VarSet, _, Warnings) }.
+ Goal2, VarSet2, EmptyVarTypes, Goal3, VarSet, _, Warnings) },
+ purge_sequence_from_goal(Goal3, Goal, Info2, Info).
%-----------------------------------------------------------------------------%
@@ -5433,8 +5449,239 @@
{ term__apply_substitution(B0, Subst, B) },
unravel_unification(A, B, Context, explicit, [],
VarSet0, Purity, Goal, VarSet, Info0, Info).
+
+
+ % The transformation of quantified sequences is unintuitive and often
+ % has an irregular order.
+
+ % The lists of elemental and source terms stored in the forall(...)
+ % construct are used in later stages of the expansion. They need to
+ % have had Subst applied to them. However the equivalent terms used
+ % to construct goals in this should not have had this Subst applied to
+ % them. (The substitution will be applied later.)
+
+transform_goal_2(forall(Sequence, UserGoalPS0), Context, VarSet0, Subst,
+ shorthand(forall(sequence_pre_patch(InitialCall, ElemTerms,
+ SourceTerms, ImplemGoal, HeadVars, VarSet, Context))) -
+ GoalInfo, VarSet, Info0, Info) -->
+
+ % Get the various source and elemental terms we need from the forall
+ % item.
+ { parse_tree_sequence_get_source_terms(Sequence, UnSubstSourceTerms) },
+
+ { apply_subst_to_sequence(Sequence, Subst, SubstSequence) },
+ { parse_tree_sequence_get_source_terms(SubstSequence, SourceTerms) },
+ { parse_tree_sequence_get_elem_terms(SubstSequence, ElemTerms) },
+
+ % Construct a makeshift initial call to the implementation predicate.
+ % Everything except the part of the call(...) except the `pure' is
+ % spurious. (On 2nd thoughts, the pure may well be spurious too...)
+ % XXX beautifully hardwired predicate name
+ { ItemicInitialCall =
+ call(unqualified("sq__dummy"), UnSubstSourceTerms, pure) },
+
+ % There is no entry in the predicate table for "sq__dummy", so this
+ % transform_goal predicate ought not assume there is.
+ transform_goal(ItemicInitialCall - Context, VarSet0, Subst,
+ InitialCall, VarSet1, Info0, Info1),
+ { InitialCall = _InitialCallGoalExpr - GoalInfo },
+
+ % Create the new implementation predicate's body. Note the
+ % dummy predicate name. (As with the implementation call,
+ % the use of unqualified("bleck") and ImplemNextTerms in the call(...)
+ % is speculative and will be changed after quantification.
+ { itemic_sequence_to_unifications(SubstSequence, Context, VarSet1,
+ VarSet2, NextUnifications, EndUnifications, HeadVars,
+ NextVars) },
+ { term__var_list_to_term_list(NextVars, ImplemNextTerms) },
+ { ItemicImplemGoal
+ = (
+ (
+ (NextUnifications , UserGoalPS0)
+ - Context ,
+ call(unqualified("bleck"),
+ % XXX embedded constant
+ ImplemNextTerms,
+ pure)
+ - Context
+ )
+ - Context
+ ;
+ EndUnifications
+ )
+ - Context
+ },
+
+ % A blind leap of faith, frankly.
+ transform_goal(ItemicImplemGoal, VarSet2, Subst, ImplemGoal, VarSet,
+ Info1, Info).
+
+
+:- pred apply_subst_to_goal(goal::in, prog_substitution::in, goal::out) is det.
+
+apply_subst_to_goal(Goal0 - Context, Subst, Goal - Context) :-
+ apply_subst_to_goal_expr(Goal0, Subst, Goal).
+
+
+:- pred apply_subst_to_goal_expr(goal_expr, prog_substitution,
+ goal_expr).
+:- mode apply_subst_to_goal_expr(in, in, out) is det.
+
+apply_subst_to_goal_expr((GoalA0, GoalB0), Subst,
+ (GoalA, GoalB)) :-
+ apply_subst_to_goal(GoalA0, Subst, GoalA),
+ apply_subst_to_goal(GoalB0, Subst, GoalB).
+apply_subst_to_goal_expr((GoalA0 & GoalB0), Subst,
+ (GoalA & GoalB)) :-
+ apply_subst_to_goal(GoalA0, Subst, GoalA),
+ apply_subst_to_goal(GoalB0, Subst, GoalB).
+apply_subst_to_goal_expr(true, _, true).
+apply_subst_to_goal_expr(forall(Sequence0,Goal0), Subst,
+ forall(Sequence, Goal)) :-
+ apply_subst_to_sequence(Sequence0, Subst, Sequence),
+ apply_subst_to_goal(Goal0, Subst, Goal).
+apply_subst_to_goal_expr((GoalA0; GoalB0), Subst,
+ (GoalA; GoalB)) :-
+ apply_subst_to_goal(GoalA0, Subst, GoalA),
+ apply_subst_to_goal(GoalB0, Subst, GoalB).
+apply_subst_to_goal_expr(fail, _Subst, fail).
+apply_subst_to_goal_expr(not(Goal0), Subst, not(Goal)) :-
+ apply_subst_to_goal(Goal0, Subst, Goal).
+apply_subst_to_goal_expr(some(Vars0, Goal0), Subst,
+ some(Vars, Goal)) :-
+ term__var_list_to_term_list(Vars0, VarTerms0),
+ term__apply_substitution_to_list(VarTerms0, Subst, VarTerms),
+ term__term_list_to_var_list(VarTerms, Vars),
+ apply_subst_to_goal(Goal0, Subst, Goal).
+apply_subst_to_goal_expr(all(Vars0, Goal0), Subst,
+ all(Vars, Goal)) :-
+ term__var_list_to_term_list(Vars0, VarTerms0),
+ term__apply_substitution_to_list(VarTerms0, Subst, VarTerms),
+ term__term_list_to_var_list(VarTerms, Vars),
+ apply_subst_to_goal(Goal0, Subst, Goal).
+apply_subst_to_goal_expr(implies(GoalA0, GoalB0), Subst,
+ implies(GoalA, GoalB)) :-
+ apply_subst_to_goal(GoalA0, Subst, GoalA),
+ apply_subst_to_goal(GoalB0, Subst, GoalB).
+apply_subst_to_goal_expr(equivalent(GoalA0, GoalB0), Subst,
+ equivalent(GoalA, GoalB)) :-
+ apply_subst_to_goal(GoalA0, Subst, GoalA),
+ apply_subst_to_goal(GoalB0, Subst, GoalB).
+apply_subst_to_goal_expr(if_then(Vars0, Cond0, Then0), Subst,
+ if_then(Vars, Cond, Then)) :-
+ term__var_list_to_term_list(Vars0, VarTerms0),
+ term__apply_substitution_to_list(VarTerms0, Subst, VarTerms),
+ term__term_list_to_var_list(VarTerms, Vars),
+ apply_subst_to_goal(Cond0, Subst, Cond),
+ apply_subst_to_goal(Then0, Subst, Then).
+apply_subst_to_goal_expr(if_then_else(Vars0, Cond0, Then0, Else0),
+ Subst, if_then_else(Vars, Cond, Then, Else)) :-
+ term__var_list_to_term_list(Vars0, VarTerms0),
+ term__apply_substitution_to_list(VarTerms0, Subst, VarTerms),
+ term__term_list_to_var_list(VarTerms, Vars),
+ apply_subst_to_goal(Cond0, Subst, Cond),
+ apply_subst_to_goal(Then0, Subst, Then),
+ apply_subst_to_goal(Else0, Subst, Else).
+apply_subst_to_goal_expr(call(SymName, Terms0, Purity), Subst,
+ call(SymName, Terms, Purity)) :-
+ term__apply_substitution_to_list(Terms0, Subst, Terms).
+apply_subst_to_goal_expr(unify(TermA0, TermB0, Purity), Subst,
+ unify(TermA, TermB, Purity)) :-
+ term__apply_substitution(TermA0, Subst, TermA),
+ term__apply_substitution(TermB0, Subst, TermB).
+
+
+ % Apply a given substitution to a quantified sequence.
+:- pred apply_subst_to_sequence(quantified_sequence::in, prog_substitution::in,
+ quantified_sequence::out) is det.
+
+apply_subst_to_sequence(zipped_sequence(LeftSeq0, RightSeq0), Subst,
+ zipped_sequence(LeftSeq, RightSeq)) :-
+ apply_subst_to_sequence(LeftSeq0, Subst, LeftSeq),
+ apply_subst_to_sequence(RightSeq0, Subst, RightSeq).
+
+apply_subst_to_sequence(term_in_seq(TermV0, Term0), Subst,
+ term_in_seq(TermV, Term)) :-
+ term__apply_substitution(TermV0, Subst, TermV),
+ term__apply_substitution(Term0, Subst, Term).
+
+
+
+
+ % Extract the elemental terms from a quantified sequence.
+:- pred parse_tree_sequence_get_elem_terms(quantified_sequence::in,
+ list(prog_term)::out) is det.
+
+parse_tree_sequence_get_elem_terms(term_in_seq(ElemTerm,_SourceTerm),
+ [ElemTerm]).
+
+parse_tree_sequence_get_elem_terms(zipped_sequence(QSL, QSR), ElemTerms) :-
+ parse_tree_sequence_get_elem_terms(QSL, LeftTerms),
+ parse_tree_sequence_get_elem_terms(QSR, RightTerms),
+ append(LeftTerms, RightTerms, ElemTerms).
+
+
+ % Extract the source terms from a quantified sequence.
+:- pred parse_tree_sequence_get_source_terms(quantified_sequence::in,
+ list(prog_term)::out) is det.
+
+parse_tree_sequence_get_source_terms(term_in_seq(_ElemVar,SourceTerm),
+ [SourceTerm]).
+
+parse_tree_sequence_get_source_terms(zipped_sequence(QSL, QSR), SourceTerms) :-
+ parse_tree_sequence_get_source_terms(QSL, LeftVars),
+ parse_tree_sequence_get_source_terms(QSR, RightVars),
+ append(LeftVars, RightVars, SourceTerms).
+
+ % itemic_sequence_to_unifications(Sequence, Context, VarSet1,
+ % VarSet2, NextUnifications, EndUnifications, SourceVars,
+ % NextSourceVars)
+ % Using the parse-tree representation of a quantified sequence
+ % "Sequence", produce:
+ % * NextUnifications, the parse-tree representation of the
+ % conjunction of unifications that allow us to extract the next
+ % elements from the sequences. These unifications are of the
+ % form Source = [Elem|NextSource], and will be used in the
+ % implementation predicate.
+ % * EndUnifications, the parse-tree representation of the
+ % conjunction of unifications that allow us to terminate the
+ % sequences. These unifications are of the form Source = [],
+ % and will be used in the implementation predicate.
+ % * SourceVars is a list of all the variables appearing in the
+ % position of the variable Source in the above example.
+ % * NextSourceVars is a list of all the variables appearing in
+ % the position of the variable NextSource in the above example.
+
+:- pred itemic_sequence_to_unifications(quantified_sequence::in,
+ prog_context::in, prog_varset::in, prog_varset::out, goal::out,
+ goal::out, list(prog_var)::out, list(prog_var)::out)
+ is det.
+
+itemic_sequence_to_unifications(term_in_seq(X,_), Context, VarSet0, VarSet,
+ unify(term__variable(NewSource),
+ term__functor(term__atom("."), [X, term__variable(NewNext)],
+ Context), pure)-Context, unify(term__variable(NewSource),
+ term__functor(term__atom("[]"), [], Context), pure)-Context,
+ [NewSource], [NewNext]) :-
+ varset__new_var(VarSet0, NewSource, VarSet1),
+ varset__new_var(VarSet1, NewNext, VarSet).
+
+itemic_sequence_to_unifications(zipped_sequence(SeqA, SeqB), Context, VarSet0,
+ VarSet, GenerationGoal, SequenceEndGoal, Sources,
+ Nexts) :-
+ itemic_sequence_to_unifications(SeqA, Context, VarSet0, VarSet1,
+ GenGoalA, EndGoalA, SourcesA, NextsA),
+ itemic_sequence_to_unifications(SeqB, Context, VarSet1, VarSet,
+ GenGoalB, EndGoalB, SourcesB, NextsB),
+ GenerationGoal = (GenGoalA , GenGoalB) - Context,
+ SequenceEndGoal = (EndGoalA, EndGoalB) - Context,
+ append(SourcesA, SourcesB, Sources),
+ append(NextsA, NextsB, Nexts).
+
+
+
:- inst dcg_record_syntax_op = bound("=^"; ":=").
:- pred transform_dcg_record_syntax(string, list(prog_term), prog_context,
@@ -7794,3 +8041,277 @@
).
%-----------------------------------------------------------------------------%
+
+
+ % purge_sequence_from_goal(Goal0, Goal, ...) completes the expansion
+ % into non-shorthand hlds of any quantified sequences contained in
+ % Goal0, binding the result with Goal.
+:- pred purge_sequence_from_goal(hlds_goal::in, hlds_goal::out,
+ transform_info::in, transform_info::out, io__state::di,
+ io__state::uo) is det.
+
+:- pred purge_sequence_from_goal_shorthand(shorthand_goal_expr::in,
+ hlds_goal_expr::out, transform_info::in,
+ transform_info::out, io__state::di, io__state::uo) is det.
+
+purge_sequence_from_goal(conj(Goals0) - GoalInfo, conj(Goals) - GoalInfo,
+ TransInfo0, TransInfo) -->
+ purge_sequence_from_goal_list(Goals0, Goals, TransInfo0,
+ TransInfo).
+purge_sequence_from_goal(call(A,B,C,D,E,F) - GoalInfo, call(A,B,C,D,E,F) -
+ GoalInfo, TransInfo, TransInfo, I, I).
+purge_sequence_from_goal(generic_call(A,B,C,D) - GoalInfo,
+ generic_call(A,B,C,D) - GoalInfo, TransInfo, TransInfo, I, I).
+purge_sequence_from_goal(switch(A,B,C,D) - GoalInfo, switch(A,B,C,D) -
+ GoalInfo, TransInfo, TransInfo, I, I).
+purge_sequence_from_goal(unify(A,B,C,D,E) - GoalInfo, unify(A,B,C,D,E) -
+ GoalInfo, TransInfo, TransInfo, I, I).
+purge_sequence_from_goal(disj(Goals0, StoreMap) - GoalInfo,
+ disj(Goals, StoreMap) - GoalInfo, TransInfo0, TransInfo) -->
+ purge_sequence_from_goal_list(Goals0, Goals, TransInfo0,
+ TransInfo).
+purge_sequence_from_goal(not(Goal0) - GoalInfo, not(Goal) - GoalInfo,
+ TransInfo0, TransInfo) -->
+ purge_sequence_from_goal(Goal0, Goal, TransInfo0, TransInfo).
+purge_sequence_from_goal(some(Vars, CanRemove, Goal0) - GoalInfo,
+ some(Vars, CanRemove, Goal) - GoalInfo, TransInfo0,
+ TransInfo) -->
+ purge_sequence_from_goal(Goal0, Goal, TransInfo0, TransInfo).
+purge_sequence_from_goal(
+ if_then_else(LocalVars, CondGoal0, ThenGoal0, ElseGoal0,
+ StoreMap) - GoalInfo,
+ if_then_else(LocalVars, CondGoal, ThenGoal, ElseGoal,
+ StoreMap) - GoalInfo,
+ TransInfo0, TransInfo) -->
+ purge_sequence_from_goal(CondGoal0, CondGoal, TransInfo0,
+ TransInfo1),
+ purge_sequence_from_goal(ThenGoal0, ThenGoal, TransInfo1,
+ TransInfo2),
+ purge_sequence_from_goal(ElseGoal0, ElseGoal, TransInfo2,
+ TransInfo).
+purge_sequence_from_goal(foreign_proc(A,B,C,D,E,F,G) - GoalInfo,
+ foreign_proc(A,B,C,D,E,F,G) - GoalInfo, TransInfo,
+ TransInfo, I, I).
+purge_sequence_from_goal(par_conj(Goals0, StoreMap) - GoalInfo,
+ par_conj(Goals, StoreMap) - GoalInfo, TransInfo0,
+ TransInfo) -->
+ purge_sequence_from_goal_list(Goals0, Goals, TransInfo0,
+ TransInfo).
+purge_sequence_from_goal(shorthand(ShorthandGoal0) - GoalInfo,
+ Goal - GoalInfo, TransInfo0, TransInfo) -->
+ purge_sequence_from_goal_shorthand(ShorthandGoal0, Goal, TransInfo0,
+ TransInfo).
+
+
+ % Applies purge_sequence_from_goal to a list of goals, producing a
+ % list of purged goals as its result.
+:- pred purge_sequence_from_goal_list(list(hlds_goal)::in,
+ list(hlds_goal)::out, transform_info::in, transform_info::out,
+ io__state::di, io__state::uo) is det.
+
+purge_sequence_from_goal_list([], [], TI, TI, IOS, IOS).
+purge_sequence_from_goal_list([Goal0|G0s], [Goal|Gs], TI0, TI) -->
+ purge_sequence_from_goal(Goal0, Goal, TI0, TI1),
+ purge_sequence_from_goal_list(G0s, Gs, TI1, TI).
+
+
+ % purge_sequence_from_goal_shorthand(ShorthandGoal,
+ % NonShorthandGoal, ...) completes the expansion
+ % into non-shorthand hlds of any quantified sequences contained in or
+ % constituting ShorthandGoal, binding the result with
+ % NonShorthandGoal.
+purge_sequence_from_goal_shorthand(bi_implication(X,Y),
+ shorthand(bi_implication(X,Y)), TransInfo, TransInfo) -->
+ { error("make_hlds.m: unexpected bi-implication.\n") }.
+
+purge_sequence_from_goal_shorthand(forall(X), shorthand(forall(X)),
+ Info, Info) -->
+ { X = sequence_pre_patch(_,_,_,_,_,_,_) },
+ { error("make_hlds.m: Purge called on a sequence quantification that has not been partially transformed.") }.
+
+ % This case of purge_sequence_from_goal_shorthand concludes the
+ % transformation into non-shorthand hlds of the quantified sequence.
+ %
+ % When this predicate is called, we know which variables belong in the
+ % head of the implementation predicate. We do not know the predid of
+ % the implementation predicate as it is not yet in the precdicate
+ % table.
+ %
+ % To complete the transformation, we have three main tasks
+ % * enter the implementation predicate into the predicate table
+ % * take apart the implementation goal and implementation call
+ % to correct the information they contain about the
+ % implementation goal
+ % * correct the information in the predicate table
+purge_sequence_from_goal_shorthand(forall(
+ sequence_mid_patch(ImplemCall0, SuffixArgs, ImplemGoal0,
+ HeadArgs, VarSet, Context)), ImplemCall, Info0, Info) -->
+
+ purge_sequence_from_goal(ImplemGoal0, ImplemGoal1, Info0, Info1),
+
+ % determine the arity of the implementation predicate
+ { length(SuffixArgs, SuffixArity) },
+ { length(HeadArgs, PrefixArity) },
+ { Arity = SuffixArity + PrefixArity },
+
+ % Enter the implementation predicate in the predicate table.
+
+ { module_info_get_predicate_table(Info1 ^ module_info,
+ PredicateTable0) },
+ { module_info_name(Info1 ^ module_info, ModuleName) },
+
+ { predicate_table_next_pred_id(PredicateTable0, NextID) },
+ { gen_forall_pred_name(NextID, ImplemPredName) },
+
+ { preds_add_implicit( Info1 ^ module_info, PredicateTable0,
+ ModuleName, unqualified(ImplemPredName),
+ Arity, local, Context, predicate,
+ ImplemPredID, PredicateTable1) },
+
+ % assert(NextID = ImplemPredID) -- if not we may well be shot
+
+ % We interrupt the completion of the predicate table entry since we now
+ % have enough information to complete the calls to the implementation
+ % predicate that reside in ImplemPredCall and ImplemPredGoal.
+ % Particularly, the complete ImplemPredGoal needs to go into the
+ % predicate table soon.
+
+ {
+ ( ImplemCall0 = conj(N_CallConj0) - _
+ ->
+ CallConj0 = N_CallConj0
+ ;
+ ImplemCall0 = call(_,_,_,_,_,_) - _
+ ->
+ CallConj0 = [ImplemCall0]
+ ;
+ error("make_hlds.m: Compiler internal error: ImplemPredCall0 must be a conjunction, but it is not.")
+ ),
+ ( length(CallConj0, L_CC0),
+ list__split_list(L_CC0 - 1, CallConj0,
+ N_ArgUnifications,
+ [call(_,N_CallInvalidProcID,N_CallPrefixArgs,
+ N_CallBuiltinState,
+ N_CallMaybeCallUnifyContext,_)
+ - N_CGI])
+ ->
+ N_ArgUnifications = ArgUnifications,
+ N_CallInvalidProcID = CallInvalidProcID,
+ N_CallPrefixArgs = CallArgs,
+ N_CallBuiltinState = CallBuiltinState,
+ N_CallMaybeCallUnifyContext
+ = CallMaybeCallUnifyContext,
+ N_CGI = CGI
+ ;
+ error("make_hlds.m: Compiler internal error: Appendage failure with CallConj0.")
+ ),
+ append(ArgUnifications, [call(ImplemPredID,CallInvalidProcID,
+ CallArgs, CallBuiltinState, CallMaybeCallUnifyContext,
+ unqualified(ImplemPredName)) - CGI], CallConj),
+ (
+ CallConj = [SingleCall - _]
+ ->
+ ImplemCall = SingleCall
+ ;
+ ImplemCall = conj(CallConj)
+ ),
+
+ ( ImplemGoal1 = disj([N_Generate0, N_End], N_X) - N_DXI
+ ->
+ N_Generate0 = Generate0,
+ N_End = End,
+ N_X = X,
+ N_DXI = DXI
+ ;
+ error("make_hlds.m: Compiler internal error: ImplemPredGoal0 must be a disjunction of two disjuncts, but it is not.")
+ ),
+ ( Generate0 = conj(N_GenConj0) - N_KXI
+ ->
+ GenConj0 = N_GenConj0,
+ KXI = N_KXI
+ ;
+ error("make_hlds.m: Compiler internal error: Generate0 not a conjunction.")
+ ),
+ ( length(GenConj0, L_GC0),
+ list__split_list(L_GC0 - 1, GenConj0, N_GenConjPrefix,
+ [call(_,N_RecurseInvalidProcID,
+ N_RecursePrefixArgs,N_RecurseBuiltinState,
+ N_RecurseMaybeCallUnifyContext,_) - N_RGI])
+ ->
+ GenConjPrefix = N_GenConjPrefix,
+ RecurseInvalidProcID = N_RecurseInvalidProcID,
+ RecursePrefixArgs = N_RecursePrefixArgs,
+ RecurseBuiltinState = N_RecurseBuiltinState,
+ RecurseMaybeCallUnifyContext
+ = N_RecurseMaybeCallUnifyContext,
+ RGI = N_RGI
+ ;
+ error("make_hlds.m: Compiler internal error: Appendage failure with GenConj0.")
+ ),
+ append(RecursePrefixArgs, SuffixArgs, RecurseArgs) ,
+ append(GenConjPrefix,
+ [call(ImplemPredID,RecurseInvalidProcID,RecurseArgs,
+ RecurseBuiltinState,RecurseMaybeCallUnifyContext,
+ unqualified(ImplemPredName)) - RGI], GenConj),
+ Generate = conj(GenConj) - KXI ,
+ ImplemGoal = disj([Generate, End], X) - DXI
+ },
+
+ % Correct certain fields in the predicate info
+ { predicate_table_get_preds(PredicateTable1, ActualTable0) },
+ { map__lookup(ActualTable0, ImplemPredID, ImplemPredInfo0) },
+
+ { pred_info_get_markers(ImplemPredInfo0, ImplemPredMarkers0) },
+ { add_marker(ImplemPredMarkers0, infer_modes, ImplemPredMarkers1) },
+ { add_marker(ImplemPredMarkers1, infer_type, ImplemPredMarkers) },
+ { pred_info_set_markers(ImplemPredInfo0, ImplemPredMarkers,
+ ImplemPredInfo1) },
+ % correctness of this action unknown:
+ { pred_info_set_goal_type(ImplemPredInfo1, clauses,
+ ImplemPredInfo2) },
+ { pred_info_set_import_status(ImplemPredInfo2, local,
+ ImplemPredInfo3) },
+ { pred_info_set_goal_type(ImplemPredInfo3, clauses,
+ ImplemPredInfo4) },
+ % Correct the fields in the clauses' info, which effects the connection
+ % between the predicate table entry for the implementation predicate
+ % and its body, ImplemPredGoal, which has already been constructed.
+ { pred_info_clauses_info(ImplemPredInfo4, ImplemClausesInfo0) },
+ { clauses_info_set_varset(ImplemClausesInfo0, VarSet,
+ ImplemClausesInfo1) },
+ % XXX suspect next line may be wrong. Why would it be the
+ % args it's called with? Surely you need to get the headvars
+ % introduced earlier, append the Suffix args and put the
+ % result in here?
+ { append(HeadArgs, SuffixArgs, TotalHeadArgs) },
+ { clauses_info_set_headvars(ImplemClausesInfo1, TotalHeadArgs,
+ ImplemClausesInfo2) },
+ { clauses_info_set_clauses(ImplemClausesInfo2,
+ [clause([],ImplemGoal,Context)], ImplemClausesInfo3) },
+
+ % Tie it all back up.
+ { pred_info_set_clauses_info(ImplemPredInfo4, ImplemClausesInfo3,
+ ImplemPredInfo) },
+ { map__set(ActualTable0, ImplemPredID, ImplemPredInfo, ActualTable) },
+ { predicate_table_set_preds(PredicateTable1, ActualTable,
+ PredicateTable) },
+ { module_info_set_predicate_table(Info0 ^ module_info, PredicateTable,
+ ModuleInfo1) },
+ { Info = Info1 ^ module_info := ModuleInfo1 }.
+
+
+
+ % Generate a unique name for a predicate used to implement a
+ % forall (quantified sequence) goal.
+:- pred gen_forall_pred_name(pred_id::in, string::out) is det.
+ % This requires that the integers >= 1 and pred IDs have a one to one
+ % mapping. This was known to be the case in Jan 2000, however it is
+ % not a documented property of the `pred_id_to_int' that this
+ % relationship holds. In all liklihood, it should be documented.
+gen_forall_pred_name(PredID, PredName) :-
+ pred_id_to_int(PredID, PredIDInt),
+ string__int_to_string(PredIDInt, PredIDIntString),
+ % XXX embedded constant "forall[" "]"
+ string__append_list(["forall[", PredIDIntString, "]"], PredName).
+
+
Index: mercury/compiler/mercury_to_goedel.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_goedel.m,v
retrieving revision 1.71
diff -u -d -r1.71 mercury_to_goedel.m
--- mercury/compiler/mercury_to_goedel.m 2000/11/01 05:12:02 1.71
+++ mercury/compiler/mercury_to_goedel.m 2001/03/31 14:13:37
@@ -557,13 +557,18 @@
goedel_output_goal_2(true, _, _) -->
io__write_string("True").
- % Implication and equivalence should have been transformed out
- % by now
+
+
+ % Implication, equivalence and quantified sequences should have been
+ % transformed out by now.
goedel_output_goal_2(implies(_G1,_G2), _VarSet, _Indent) -->
{ error("mercury_to_goedel: implies/2 in goedel_output_goal")}.
goedel_output_goal_2(equivalent(_G1,_G2), _VarSet, _Indent) -->
{ error("mercury_to_goedel: equivalent/2 in goedel_output_goal")}.
+
+goedel_output_goal_2(forall(_,_), _, _) -->
+ { error("mercury_to_goedel: forall/2 in goedel_output_goal")}.
goedel_output_goal_2(some(Vars, Goal), VarSet, Indent) -->
( { Vars = [] } ->
Index: mercury/compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.184
diff -u -d -r1.184 mercury_to_mercury.m
--- mercury/compiler/mercury_to_mercury.m 2001/04/03 03:19:57 1.184
+++ mercury/compiler/mercury_to_mercury.m 2001/04/08 12:48:21
@@ -1870,6 +1870,16 @@
mercury_output_goal_2(true, _, _) -->
io__write_string("true").
+ % XXX predicted workingness 70%
+mercury_output_goal_2(forall(Sequence,Goal), VarSet, Indent) -->
+ io__write_string("forall "),
+ mercury_output_sequence_goal(Sequence, VarSet),
+ io__write_string(" :: "),
+ mercury_output_goal(Goal, VarSet, Indent),
+ mercury_output_newline(Indent).
+
+
+
mercury_output_goal_2(implies(G1,G2), VarSet, Indent) -->
{ Indent1 is Indent + 1 },
io__write_string("("),
@@ -1996,6 +2006,22 @@
mercury_output_term(B, VarSet, no, next_to_graphic_token).
+ % XXX some minor niggles inside
+:- pred mercury_output_sequence_goal(quantified_sequence::in, prog_varset::in,
+ io__state::di, io__state::uo) is det.
+
+mercury_output_sequence_goal(term_in_seq(Elem,Source), VarSet) -->
+ mercury_output_term(Elem, VarSet, no),
+ io__write_string(" fin "),
+ % XXX would like to use `in', but that conflicts with mode `in'
+ mercury_output_term(Source, VarSet, no).
+
+mercury_output_sequence_goal(zipped_sequence(SeqA, SeqB), VarSet) -->
+ mercury_output_sequence_goal(SeqA, VarSet),
+ io__write_string(" as "),
+ mercury_output_sequence_goal(SeqB, VarSet).
+
+
:- pred mercury_output_call(sym_name, list(prog_term), prog_varset, int,
io__state, io__state).
:- mode mercury_output_call(in, in, in, in, di, uo) is det.
@@ -2957,6 +2983,9 @@
mercury_infix_op("mod").
mercury_infix_op("rem").
mercury_infix_op("^").
+mercury_infix_op("fin").
+mercury_infix_op("as").
+
:- pred mercury_unary_prefix_op(string).
:- mode mercury_unary_prefix_op(in) is semidet.
@@ -3004,6 +3033,7 @@
mercury_unary_prefix_op("wait").
mercury_unary_prefix_op("~").
mercury_unary_prefix_op("^").
+mercury_unary_prefix_op("forall").
:- pred mercury_unary_postfix_op(string).
:- mode mercury_unary_postfix_op(in) is semidet.
Index: mercury/compiler/module_qual.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.65
diff -u -d -r1.65 module_qual.m
--- mercury/compiler/module_qual.m 2001/04/03 03:20:06 1.65
+++ mercury/compiler/module_qual.m 2001/04/08 03:52:26
@@ -416,6 +416,12 @@
list__append(Symbols0, SymbolsC, Symbols),
bool__and(SuccessA, SuccessB, Success0),
bool__and(Success0, SuccessC, Success).
+
+ % For each term in the sequence list call term_qualified_symbols &/or
+ % term__coerce as appropriate.
+process_assert(forall(_,_) - _, [], yes) :-
+ error("process_assert not implemented for sequence quantification.").
+
process_assert(call(SymName, Args0, _Purity) - _, Symbols, Success) :-
(
SymName = qualified(_, _)
Index: mercury/compiler/prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.65
diff -u -d -r1.65 prog_data.m
--- mercury/compiler/prog_data.m 2001/04/03 03:20:15 1.65
+++ mercury/compiler/prog_data.m 2001/04/08 12:49:44
@@ -623,7 +623,10 @@
% atomic goals
; call(sym_name, list(prog_term), purity)
- ; unify(prog_term, prog_term, purity).
+ ; unify(prog_term, prog_term, purity)
+
+ % quantified sequence
+ ; forall(quantified_sequence, goal).
:- type goals == list(goal).
@@ -660,6 +663,21 @@
; (aditi_top_down)
; (aditi_bottom_up)
.
+
+ % A zipped sequence is a sequence with an a pair of sequence 'as'ed
+ % together.
+:- type quantified_sequence
+ ---> term_in_seq(
+ prog_term, % term containing universally
+ % quantified variables
+ prog_term % the source term
+ )
+ ; zipped_sequence( % Sequence as Sequence
+ quantified_sequence,
+ quantified_sequence
+ )
+ .
+
%-----------------------------------------------------------------------------%
%
Index: mercury/compiler/prog_io_goal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_goal.m,v
retrieving revision 1.19
diff -u -d -r1.19 prog_io_goal.m
--- mercury/compiler/prog_io_goal.m 2000/04/22 07:12:00 1.19
+++ mercury/compiler/prog_io_goal.m 2001/04/08 12:56:05
@@ -98,6 +98,8 @@
:- import_module mode_util, purity, prog_io, prog_io_util, term_util.
:- import_module term.
:- import_module int, map, string, std_util.
+%XXX kick out the require module when it is no longer needed for error/2
+:- import_module require.
% Parse a goal.
%
@@ -234,6 +236,28 @@
parse_goal_with_purity(A0, V0, (impure), A, V).
parse_goal_2("semipure", [A0], V0, A, V) :-
parse_goal_with_purity(A0, V0, (semipure), A, V).
+parse_goal_2("::", [A0, B0], V0, forall(Y, B), V) :-
+ A0 = term__functor(term__atom("forall"), [Y0], _),
+ parse_seq_quan_goal(Y0, V0, Y, V1),
+ parse_goal(B0, V1, B, V).
+
+:- pred parse_seq_quan_goal(term, prog_varset, quantified_sequence,
+ prog_varset).
+:- mode parse_seq_quan_goal(in, in, out, out) is semidet.
+
+parse_seq_quan_goal(QS0, V0, QSGE, V) :-
+ QS0 = term__functor(term__atom("as"), [QSL0, QSR0], _),
+ parse_seq_quan_goal(QSL0, V0, QSL, V1),
+ parse_seq_quan_goal(QSR0, V1, QSR, V),
+ QSGE = zipped_sequence(QSL, QSR)
+ ;
+ QS0 = term__functor(term__atom("fin"), [Lterm0, Rterm0], _),
+ term__coerce(Lterm0, Lterm),
+ term__coerce(Rterm0, Rterm),
+ QSGE = term_in_seq(Lterm, Rterm),
+ V0 = V.
+
+
:- pred parse_goal_with_purity(term, prog_varset, purity, goal_expr,
Index: mercury/compiler/prog_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_util.m,v
retrieving revision 1.51
diff -u -d -r1.51 prog_util.m
--- mercury/compiler/prog_util.m 2000/09/21 00:21:06 1.51
+++ mercury/compiler/prog_util.m 2001/04/08 12:54:13
@@ -319,6 +319,32 @@
term__substitute(TermB0, OldVar, term__variable(NewVar),
TermB).
+prog_util__rename_in_goal_expr(forall(Sequence0,GoalExpr0 - GI), OldVar,
+ NewVar, forall(Sequence, GoalExpr - GI)) :-
+ prog_util__rename_in_sequence(Sequence0, OldVar, NewVar, Sequence),
+ prog_util__rename_in_goal_expr(GoalExpr0, OldVar, NewVar, GoalExpr).
+
+
+
+:- pred prog_util__rename_in_sequence(quantified_sequence::in, prog_var::in, prog_var::in, quantified_sequence::out) is det.
+
+ % This will needs the sequence_to_terms predicate to be
+ % pillaged from another one of the source files. Note that the
+ % determinism of the predicate will need to be checked, and
+ % possibly a second predicate written.
+prog_util__rename_in_sequence(zipped_sequence(SeqA0, SeqB0), OldVar, NewVar,
+ zipped_sequence(SeqA, SeqB)) :-
+ prog_util__rename_in_sequence(SeqA0, OldVar, NewVar, SeqA),
+ prog_util__rename_in_sequence(SeqB0, OldVar, NewVar, SeqB).
+
+prog_util__rename_in_sequence(term_in_seq(ElemTerm0, SourceTerm0), OldVar,
+ NewVar, term_in_seq(ElemTerm, SourceTerm)) :-
+ term__substitute(ElemTerm0, OldVar, term__variable(NewVar), ElemTerm),
+ term__substitute(SourceTerm0, OldVar, term__variable(NewVar),
+ SourceTerm).
+
+
+
:- pred prog_util__rename_in_vars(list(prog_var), prog_var, prog_var,
list(prog_var)).
:- mode prog_util__rename_in_vars(in, in, in, out) is det.
Index: mercury/compiler/quantification.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/quantification.m,v
retrieving revision 1.80
diff -u -d -r1.80 quantification.m
--- mercury/compiler/quantification.m 2001/04/07 14:04:56 1.80
+++ mercury/compiler/quantification.m 2001/04/08 13:01:52
@@ -123,7 +123,7 @@
:- import_module instmap, goal_util.
:- import_module map, term, varset.
-:- import_module std_util, bool, require.
+:- import_module std_util, bool, int, require.
:- import_module enum, sparse_bitset.
% The `outside vars', `lambda outside vars', and `quant vars'
@@ -327,6 +327,8 @@
Goal0, Goal1),
{ goal_util__rename_var_list(Vars0, no, RenameMap, Vars) }
),
+ % XXX here call update_seen_vars with the original variables,
+ % rather than the renamed apart ones. Is that right?
quantification__update_seen_vars(QVars),
{ insert_list(QuantVars, Vars, QuantVars1) },
quantification__set_quant_vars(QuantVars1),
@@ -581,8 +583,229 @@
{ Goal = conj([ForwardsImplication, ReverseImplication]) }.
+implicitly_quantify_goal_2_shorthand(forall(X), _Context,
+ shorthand(forall(X))) -->
+ { X = sequence_mid_patch(_,_,_,_,_,_) },
+ { error("quantification.m: implicitly quantifiy called on partially transformed sequence quantification. This should never happen.") }.
+
-:- pred implicitly_quantify_atomic_goal(list(prog_var), quant_info, quant_info).
+implicitly_quantify_goal_2_shorthand(forall(sequence_pre_patch(ImplemCall0,
+ ElemTerms, SourceTerms, ImplemGoal0, IGHeadVars,
+ IGVarSet, SQContext)),
+ Context,
+ shorthand(forall(sequence_mid_patch(ImplemCall, SuffixArgs,
+ ImplemGoal, IGHeadVars, IGVarSet, SQContext)))) -->
+
+
+ % Understanding how the sequential quantification of variables affects
+ % their ordinary quantification is best understood by understanding how
+ % a quantified sequence is expanded into traditional mercury code.
+ % The second best way to think about it is just to realise that `forall
+ % X in Xs' has the effect of universally quantifying X. (And
+ % therefore, any K that varies with X.)
+
+ % Quantified variables cannot be pushed inside a negation, and a
+ % sequence quantification is the same as a universal quantification
+ % which is equivalent to a negation (all X G == not some X not G), so
+ % we treat sequence quantifications the same. 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).
+
+
+ % We start out by working out:
+ % * the variables that are strictly local to the sequence
+ % quantification and do not appear in the enclosing scope. These
+ % variables must be universally quantified with respect to the
+ % enclosing scope.
+ % * the variables that do not feature in the sequence
+ % quantification but do feature in the enclosing scope.
+ % * the variables that feature in both the sequence
+ % quantification and the enclosing scope. These are
+ % existentially quantified w.r.t. the sequence quantification and
+ % will be ground->ground (or similarly) moded after mode
+ % analysis. They must feature in the argument list of the
+ % sequence quantification.
+
+ % XXX the reason I'm using sets and have calls to glap() is to make
+ % tracing easier.
+
+ { term__vars_list(ElemTerms, ElemVars) },
+ { ElemVarsSet = set__list_to_set(ElemVars) },
+ { term__vars_list(SourceTerms, SourceVars) },
+ { SourceVarsSet = set__list_to_set(SourceVars) },
+
+ quantification__get_outside(OutsideVarsBitset),
+ { OutsideVars = bitset_to_set(OutsideVarsBitset) },
+ { glap(_) },
+ % POSSIBLY this next computation is being made using the wrong varset!!
+ { quantification__goal_vars(ordinary_nonlocals, ImplemGoal0,
+ InsideOrdinaryVarsBitset, InsideLambdaVarsBitset) },
+ { InsideOrdinaryVars = bitset_to_set(InsideOrdinaryVarsBitset) },
+ { InsideLambdaVars = bitset_to_set(InsideLambdaVarsBitset) },
+
+ { glap(_) },
+ { set__union(InsideOrdinaryVars, InsideLambdaVars, InsideVars) },
+ { set__union(OutsideVars, SourceVarsSet) = RealOutsideVars },
+ { set__union(InsideVars, ElemVarsSet) = RealInsideVars },
+ { glap(_) },
+ { set__intersect(RealOutsideVars, RealInsideVars)
+ = RealIntersectVars },
+ { set__difference(RealInsideVars, RealOutsideVars)
+ = ExclusivelyInsideVars0 },
+ { glap(_) },
+ { set__difference(RealIntersectVars, SourceVarsSet)
+ = IntersectVars },
+
+ { set__to_sorted_list(IntersectVars, SuffixArgs) },
+ { glap(_) },
+
+ % Fix up ImplemCall ... we could know the name and arity of the
+ % predicate at this point, but why bother when we don't know the PredID
+ % (aside from the fact that it could make future debugging easier, lead
+ % to better error messages ...)
+ %
+ % I violate the mercury if-then-else Var0/Var convention here
+ % because many of the variables are already suffixed with a zero
+ % for the (different) "before and after" purpose.
+
+ {
+ ( ImplemCall0 = conj(N_CallConj0) - NGI
+ ->
+ CallConj0 = N_CallConj0,
+ GI = NGI
+ ;
+ ImplemCall0 = call(_,_,_,_,_,_) - NGI
+ ->
+ CallConj0 = [ImplemCall0],
+ GI = NGI
+ ;
+ error("quantifiction.m: Compiler internal error: ImplemPredCall0 must be a conjunction, but it is not.")
+ ),
+ (
+ list__split_list(list__length(CallConj0) - 1,
+ CallConj0, ArgUnifications, [Call]),
+ Call = call(InvalidPredID,
+ CallInvalidProcID,
+ CallPrefixArgs,
+ CallBuiltinState,
+ CallMaybeCallUnifyContext,
+ DummyName) - CGI
+ ->
+ append(CallPrefixArgs, SuffixArgs, CallArgs),
+ append(ArgUnifications, [call(InvalidPredID,
+ CallInvalidProcID, CallArgs, CallBuiltinState,
+ CallMaybeCallUnifyContext, DummyName) - CGI],
+ CallConj)
+ ;
+ error("quantification.m: Compiler internal error: Appendage failure with CallConj0.")
+ ),
+ (
+ CallConj = [SingleCall - _]
+ ->
+ ImplemCall1 = SingleCall - GI
+ ;
+
+ ImplemCall1 = conj(CallConj) - GI
+
+ )
+ } ,
+
+ % (this could be done earlier) quantify the body of the implementation
+ % predicate. XXX Those warnings should be packed into with the
+ % warnings bit of the quant info.
+ { append(IGHeadVars, SuffixArgs, RealHeadVars) } ,
+ { map__init(EmptyVarTypes) } ,
+ quantification__get_varset(VarSet0),
+ { implicitly_quantify_clause_body(RealHeadVars,
+ ImplemGoal0, VarSet0, EmptyVarTypes, ImplemGoal, VarSet, _,
+ _Warnings) } ,
+ quantification__set_varset(VarSet),
+
+ % Any variables that are within the scope of another quantification are
+ % outside the scope of the seqence quantification, hence, we set up the
+ % new QuantVars1 and a new OutsideVars1, where OutsideVars1 is the
+ % union of the old OutsideVars and QuantVars, and QuantVars1 is empty.
+
+ quantification__get_quant_vars(QuantVars),
+ { union(OutsideVarsBitset, QuantVars, OutsideVars1) },
+ { init(QuantVars1) },
+ quantification__set_quant_vars(QuantVars1),
+ quantification__set_outside(OutsideVars1),
+
+ quantification__get_lambda_outside(LambdaOutsideVars),
+ % Rename apart all the quantified
+ % variables that occur outside this goal.
+ { set__intersect(bitset_to_set(OutsideVars1), ExclusivelyInsideVars0,
+ RenameVars1) },
+ { set__intersect(bitset_to_set(LambdaOutsideVars),
+ ExclusivelyInsideVars0, RenameVars2) },
+ { union(set_to_bitset(RenameVars1), set_to_bitset(RenameVars2),
+ RenameVars) },
+ (
+ { empty(RenameVars) }
+ ->
+ { ImplemCall2 = ImplemCall1 },
+ { ExclusivelyInsideVars
+ = set__to_sorted_list(ExclusivelyInsideVars0) }
+ ;
+ quantification__warn_overlapping_scope(RenameVars, Context),
+ quantification__rename_apart(RenameVars, RenameMap,
+ ImplemCall1, ImplemCall2),
+ { goal_util__rename_var_list(
+ set__to_sorted_list(ExclusivelyInsideVars0), no,
+ RenameMap, ExclusivelyInsideVars) }
+ ),
+
+ % XXX here call update_seen_vars with the original variables,
+ % rather than the renamed apart ones. Is that right? (This is
+ % a question posed by Fergus to himself.)
+ quantification__update_seen_vars(set_to_bitset(ExclusivelyInsideVars0)),
+
+
+ % Now we move on to handling the variables that should be existentially
+ % quantified in the enclosing scope.
+
+ % "see" the existentially quantified variables
+ %{ term__vars_list(SourceTerms, SourceVars) },
+ { RealIntersectVarsBSet = set_to_bitset(RealIntersectVars) },
+ quantification__update_seen_vars(RealIntersectVarsBSet),
+
+ % set up new QuantVars for quantifying the call to the implmentation
+ % predicate. We don't need to set up a new OutsideVars, the current
+ % one still holds true.
+ { insert_list(QuantVars1, ExclusivelyInsideVars, QuantVars2) },
+ quantification__set_quant_vars(QuantVars2),
+
+
+ % This is more than a little precarious
+ implicitly_quantify_goal(ImplemCall2, ImplemCall),
+
+ % We adjust the NonLocal field to rip out the ElemVars, which will have
+ % been recognised as non-local because they _don't_ appear in the
+ % ImpemPredCall. XXX Dubious about this comment.
+ quantification__get_nonlocals(NonLocals0),
+ { intersect(NonLocals0, OutsideVarsBitset, NonLocals1) },
+ { intersect(NonLocals0, LambdaOutsideVars, NonLocals2) },
+ { union(NonLocals1, NonLocals2, NonLocals3) },
+ { NonLocals = delete_list(NonLocals3, ExclusivelyInsideVars) },
+ quantification__set_nonlocals(NonLocals),
+
+ % restore the original OutsideVars and QuantVars
+ quantification__set_outside(OutsideVarsBitset),
+ quantification__set_quant_vars(QuantVars).
+
+
+% XXX For debugging purposes
+
+:- pred glap(int::out) is det.
+
+glap(1).
+
+
+
+
+:- pred implicitly_quantify_atomic_goal(list(prog_var), quant_info,
+ quant_info).
:- mode implicitly_quantify_atomic_goal(in, in, out) is det.
implicitly_quantify_atomic_goal(HeadVars) -->
@@ -1018,6 +1241,29 @@
LambdaSet) :-
goal_list_vars_2(NonLocalsToRecompute, [LHS, RHS],
Set0, LambdaSet0, Set, LambdaSet).
+
+
+ % Notice that this gets the variables from inside the implementation
+ % goal.
+quantification__goal_vars_2_shorthand(NonLocalsToRecompute,
+ forall(sequence_pre_patch(_ImplemCall,ElemTerms, SourceTerms,
+ ImplemGoalExpr - _,_HeadVars,_VarSet,_Contet)),
+ Set0, LambdaSet0, Set, LambdaSet) :-
+ term__vars_list(SourceTerms, SourceVars),
+ term__vars_list(ElemTerms, ElemVars),
+ insert_list(Set0, SourceVars, Set1),
+ delete_list(Set1, ElemVars, Set2),
+ delete_list(LambdaSet0, ElemVars, LambdaSet1),
+ union(Set0, Set2, Set3),
+ union(LambdaSet0, LambdaSet1, LambdaSet2),
+ quantification__goal_vars_2(NonLocalsToRecompute, ImplemGoalExpr,
+ Set3, LambdaSet2, Set, LambdaSet).
+
+
+quantification__goal_vars_2_shorthand(_NonLocalsToRecompute, forall(X),
+ Set, LambdaSet, Set, LambdaSet) :-
+ X = sequence_mid_patch(_,_,_,_,_,_),
+ error("quantification.m: May not get variables from partially transformed sequence.").
:- pred quantification__unify_rhs_vars(nonlocals_to_recompute,
Index: mercury/compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.300
diff -u -d -r1.300 typecheck.m
--- mercury/compiler/typecheck.m 2001/04/07 14:04:59 1.300
+++ mercury/compiler/typecheck.m 2001/04/08 03:52:38
@@ -1102,6 +1102,24 @@
typecheck_goal(LHS0, LHS),
typecheck_goal(RHS0, RHS).
+ % This handling seems quite half baked to me. Frankly, it could be an
+ % excellent way to get the variable lists and sets out of synch.
+ % However, experimentation reveals that the compiler seg faults before
+ % reaching this code on some occasions.
+typecheck_goal_2_shorthand(forall(sequence_pre_patch(ImplemCall0, ElemTerms,
+ SourceTerms, ImplemGoal0,HeadVars, VarSet, Context)),
+ forall(sequence_pre_patch(ImplemCall,ElemTerms, SourceTerms,
+ ImplemGoal, HeadVars, VarSet, Context))) -->
+ checkpoint("quantified sequence"),
+ typecheck_goal(ImplemCall0, ImplemCall),
+ typecheck_info_set_context(Context),
+ % I think there should aslo be typecheck_info_set_varset(VarSet0
+ typecheck_goal(ImplemGoal0, ImplemGoal).
+
+typecheck_goal_2_shorthand(forall(X), forall(X)) -->
+ { X = sequence_mid_patch(_,_,_,_,_,_) },
+ { error("typecheck.m: cannot transform quantified sequence in the middle of transformation.") }.
+
%-----------------------------------------------------------------------------%
:- pred typecheck_goal_list(list(hlds_goal), list(hlds_goal),
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list