Matching Clauses

A matching clause is a form of a clause in which the determinacy and input/output unifications are explicitly denoted. The compiler translates matching clauses into matching trees, and generates indices for all of the input arguments. The compilation of matching clauses is much simpler than that of normal Prolog clauses, because no complex program analysis or specialization is necessary, and because the generated code tends to be faster and more compact.

A determinate matching clause takes the following form:

      H, G  => B
where H is an atomic formula, and G and B are two sequences of atomic formulas. H is called the head, G is called the guard, and B is called the body of the clause. Calls in G cannot bind variables in H, and all calls in G must be in-line tests. In other words, the guard must be flat.

For a call C, matching is used instead of unification in order to select a matching clause in its predicate. The matching clause H, G => B is applicable to C if C matches H (i.e., C and H become identical after a substitution is applied to H) and G succeeds. When applying the matching clause to C, the system rewrites C determininately into B. In other words, when execution backtracks to C, no alternative clauses will be tried.

A non-determinate matching clause takes the following form:

      H, G  ?=> B
It differs from the determinate matching clause H, G => B, in that the rewriting from H into B is non-determinate. In other words, the alternative clause will be tried upon backtracking.

The following types of predicates can occur in G:



Subsections
Neng-Fa Zhou 2013-01-25