$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''.
If Ge' < Ge'' , then Gt Ge' < Gt Ge'' .
If Gt' < Gt'' , then Gt' Ge' < Gt'' Ge'' .
[] < Gt Ge .
where [] denotes an empty ground expression.
The ordering of the ground terms is defined as follows.
Gs < (Ge)
If Ge' < Ge'' , then (Ge') < (Ge'') .
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''.