3.4.3 Grade modifiers for trailing

In the absence of the .tr grade modifier, the Mercury compiler generates executables that do not support trailing.

Trailing is a technique that the implementations of logic programming languages use to support constraint solving. All Prolog implementations use it, because unification in standard Prolog is effectively a solver for constraints of the form “are these two terms unifiable?”. (Such constraints are usually called Herbrand constraints.) In Mercury, the mode system imposes a requirement that when two terms are unified, one of them must be ground, which means that such questions are always trivially answerable. In fact, the design of Mercury was driven in large part by the intention to avoid any requirement for constraint solving, because it makes programs harder to understand both by humans, and by the compiler. Unlike Prolog, Mercury thus has no constraint solver built into it. However, Mercury can be used to implement constraint solvers. While the act of posting a constraint in such a program is a declarative action, its implementation requires updating a constraint store. This in turn requires that when execution backtracks past the goal that posted the constraint, the update to the constraint store must be undone.

This is why in the right grades, Mercury can support a trail. (see Trailing in The Mercury language Reference Manual). The trail is a stack-like data structure that consists of a sequence of entries, each of which effectively describes how to undo an update to a data structure. This can be used to implement constraint solvers like this:

• When execution is about to enter a disjunction or an if-then-else, the implementation records the address of the top of the trail, effectively as a snapshot.
• When the program adds a new constraint to the constraint store, it must also push a new entry on top of the trail that describes how to undo the addition of this new constraint. (That entry will consist of the address of the undo function, and an argument for it that identifies the specific addition to undo.)
• Whenever execution backtracks, either to a later disjunct in a disjunction or to the else part of an if-then-else, the implementation walks the trail from the current top of the trail down to the snapshot address that was recorded on entry to the current disjunction or if-then-else, and executes the undo actions that they encode. (For example, a trail entry can contain the address of a C function to call, and an argument to invoke that function with.) This is usually called unwinding the trail.

.tr

Compiling programs in a grade that includes the .tr grade modifier generates executables that support trailing. This means that the compiler-generated code will create the snapshots and unwind the trail as needed. The addition of new constraints to the constraint store, and the addition of new entries to the trail to undo those additions, will be done by C code in foreign_proc pragmas written by the user. (Each trail entry consists of the address of a C function to call, and an argument to invoke that function with.)

This grade modifier is compatible only with base grades that target C.