-- |

module Language.REST where

import Language.REST.OCAlgebra (OCAlgebra)
import Language.REST.OCToAbstract
import Language.REST.WQOConstraints.ADT (ConstraintsADT, adtOC)
import Language.REST.RPO
import Language.REST.RuntimeTerm
import Language.REST.Op
import System.IO (Handle)


-- | 'adtRPO' Is an ordering constraint algebra derived from the recursive
-- path ordering; it is a useful general-purpose OCA.
adtRPO :: (Handle, Handle) -> OCAlgebra (ConstraintsADT Op) RuntimeTerm IO
adtRPO :: (Handle, Handle) -> OCAlgebra (ConstraintsADT Op) RuntimeTerm IO
adtRPO (Handle, Handle)
z3 = forall (impl :: * -> *) base lifted (m :: * -> *).
(ToSMTVar base Int, Ord base, Eq base, Hashable base, Show lifted,
 Show base, Show (impl base)) =>
WQOConstraints impl m
-> ConstraintGen impl base lifted Identity
-> OCAlgebra (impl base) lifted m
lift ((Handle, Handle) -> WQOConstraints ConstraintsADT IO
adtOC (Handle, Handle)
z3) forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm Identity
rpo