Mercury Bugs - mercury
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000540mercuryFeature Requestpublic2021-11-08 17:292021-11-08 17:29
Reporterzs 
Assigned To 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusnewResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0000540: making up for not updating insts
DescriptionWhen mode analysis processes a conjunction such as A = f(B, C), B = g(D),
it updates the insts of only the variables of the primitive operation it is
looking at at each point in time. This means that when we process B = g(D),
we update the inst of B to say that it is bound to g, but we do NOT update
the insts of the variables whose terms include B. Therefore if a later part
of that conjunction passes A to a predicate whose in an argument position
that requires the inst of the argument to be f(g(ground), ground), we get
an error, because while mode analysis knows that A's inst is f(ground, ground),
it does not know that the first ground is now known to be g(ground).

Alias tracking turned out to be a bad idea when done all the time, but we could
maybe get around this by doing it "on demand". It would apply only when
all the mode errors for a procedure have the form "var A is expected to have
inst InstSpec, but its actual inst is InstGen", where InstSpec is an
instance of InstGen that differs from it by requiring a ground inst of
a specific shape (such as "g(ground)") for some part of InstGen
that is simply "ground". In such cases, we would redo the mode analysis
after making a trial modification of the procedure body for each such error.
If these modifications fix all the errors, we keep the modified body;
otherwise, we revert to the original procedure body and report the errors.

The trial modification needs as input the identity of the variable in the error,
its required inst, and the goal path of the goal with the error. (We can keep
this info in the mode_error structure.) The modification would traverse the
procedure body while keeping a set of variable it is on the lookout for.
Initially, this set would contain only the variable in the error. When we find
either a construction or deconstruction unification with a lookout variable
on the left hand side, we would (a) record in a map the right hand corresponding
to this left hand side, and (b) we would add all the variables in the right hand
side to the lookout set. This way, we could enable the reconstruction of *all*
the constructed and/or deconstructred parts of the original variable, even when
some of those unifications don't directly reference it.

The above works in the absence of branched goals. In their presence, we would
need to (a) start processing each branch with the same initial binding map,
(b) process each branch independently, and (b) take the intersection of the
final binding maps of the branches as the final map of the branched control
structure itself. This intersection operation throws away information,
and this may prevent being able to reconstruct the binding of the original
variable at the error site.

However, if we *can* reconstruct that binding, then we can add a new goal
before the error site that rebuilds the same term as the original variable,
as e.g. A' = f(B, C), and replaces all references to A with references to A'
in all the places where that reconstruction is valid. (This means all goals
for which the value of A is supplied by the unifications that we used to
construct A'; references to A outside any of their scopes must NOT be replaced.)
Given the unification sequence B = g(D), A' = f(B, C), mode analysis *will*
record the inst of A' as f(g(ground), ground), which should fix the original
mode error. This extra unification will be deleted, long after mode analysis,
by common structure elimination.

With the right housekeeping, it should be possible to (try to) fix all mode errors
of this form in a procedure body at the same time.

Of course, this is rather a lot of machinery for a relatively rare problem.
Simply adding a verbose-only component to the original error message reminding
the programmer that manually adding this redundant unification may fix
the mode error (and why) may get most of the benefit at much lower cost.
TagsNo tags attached.
Relationships
Attached Files

There are no notes attached to this issue.

Issue History
Date ModifiedUsernameFieldChange
2021-11-08 17:29zsNew Issue