Language.REST.RPO

This module contains the implementation of the Recursive Path Quasi-Ordering, defined in section 4.2.1 of the REST paper

Documentation

rpo :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity

The constraint generator for RPQO. That is, given terms t, u, rpo generates the constraints on n RPQO ≥ᵣ such that t ≥ᵣ u.

rpoGTE :: (?impl :: WQOConstraints oc m, Hashable (oc Op), Eq (oc Op), Show (oc Op)) => RuntimeTerm -> RuntimeTerm -> oc Op

rpoGTE impl t u generates the constraints a WQO over Op (via impl) that ensures that t ≥ᵣ u in the result RPQO ≥ᵣ.

synGTE :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool

Performs the (concrete) RPQO calculation. synGTE o t u returns true iff t ≥ᵣ u using an RPQO with precedence o.