Compare: Comparison Operations

      $func? Eq (e.Exp1)(e.Exp2) = ;
      $func? Ne (e.Exp1)(e.Exp2) = ;
      $func? Ge (e.Exp1)(e.Exp2) = ;
      $func? Gt (e.Exp1)(e.Exp2) = ;
      $func? Le (e.Exp1)(e.Exp2) = ;
      $func? Lt (e.Exp1)(e.Exp2) = ;

These functions compare two expressions e.Exp1 and e.Exp2 to determine whether the corresponding relation between the arguments holds. The correspondence between the functions and the relations is as follows. Eq corresponds to "equal to", Ne to "not equal to", Ge to "greater than or equal to", Gt to "greater than", Le to "less than or equal to", Lt to "less than".

If the condition is satisfied, the value returned by the functions is an empty ground expression, otherwise $fail(0).

      $func Compare (e.Exp1)(e.Exp2)  = s.Res;   /* '<', '>', '=' */

Compare compares two expressions e.Exp1 and e.Exp2, and returns either '<', if e.Exp1 is less than e.Exp2, '>' , if e.Exp1 is greater than e.Exp2, or '=', if e.Exp1 is equal to e.Exp2.

Ground expressions are compared according to the following linear ordering relation <.

For any ground expressions Ge' and Ge'', there holds either Ge' < Ge'', Ge' = Ge'', or Ge'' < Ge'.

Two expressions Ge' = Gt'1 ... Gt'm and Ge'' = Gt''1 ... Gt''n are compared lexicographically, which means that their top level terms are compared pairwise from left to right, until a pair is found of two unequal terms Gt'k and Gt''k. Then, if Gtk' < Gtk'', it is assumed that Ge' < Ge''.

If Ge' turns out to be shorter than Ge'', and all top level terms in Ge' are equal to the corresponding terms in Ge'', it is assumed that Ge' < Ge''.

Formally speaking, for all ground expressions Ge, Ge', Ge'' and for all ground terms Gt, Gt', Gt'' the following holds:

where [] denotes an empty ground expression.

The ordering of the ground terms is defined as follows.

Symbols are assumed to be less than the terms of the form (Ge). In other words, for all symbols Gs and ground expressions Ge,
Comparing the terms of the form (Ge) is reduced to comparing their contents according to the rule:
Each symbol belongs to one and only one of the following sets of symbols:

These sets will be referred to as symbol classes. We consider the set of symbol classes as equipped with a linear ordering, the ordering being given by the above list of symbol classes. Thus the set of character symbols precedes the set of word symbols, etc.

If two symbols Gs' and Gs'' belong to two different classes Class' and Class'', and Class' < Class'', then it is assumed that Gs' < Gs''.

If two symbols belong to the same class, they are compared according to the following rules.