module Data.Comp.MultiParam.Ordering
(
POrd(..),
OrdHD(..)
) where
import Data.Comp.MultiParam.Term
import Data.Comp.MultiParam.Sum
import Data.Comp.MultiParam.Ops
import Data.Comp.MultiParam.HDifunctor
import Data.Comp.MultiParam.FreshM
import Data.Comp.MultiParam.Equality
class PEq a => POrd a where
pcompare :: a i -> a j -> FreshM Ordering
instance Ord a => POrd (K a) where
pcompare (K x) (K y) = return $ compare x y
class EqHD f => OrdHD f where
compareHD :: POrd a => f Var a i -> f Var a j -> FreshM Ordering
instance (OrdHD f, OrdHD g) => OrdHD (f :+: g) where
compareHD (Inl x) (Inl y) = compareHD x y
compareHD (Inl _) (Inr _) = return LT
compareHD (Inr x) (Inr y) = compareHD x y
compareHD (Inr _) (Inl _) = return GT
instance OrdHD f => OrdHD (Cxt h f) where
compareHD (Term e1) (Term e2) = compareHD e1 e2
compareHD (Hole h1) (Hole h2) = pcompare h1 h2
compareHD (Place p1) (Place p2) = pcompare p1 p2
compareHD (Term _) _ = return LT
compareHD (Hole _) (Term _) = return GT
compareHD (Hole _) (Place _) = return LT
compareHD (Place _) _ = return GT
instance POrd Var where
pcompare x y = return $ varCompare x y
instance (OrdHD f, POrd a) => POrd (Cxt h f Var a) where
pcompare = compareHD
instance (HDifunctor f, OrdHD f) => Ord (Term f i) where
compare x y = evalFreshM $ compareHD (coerceCxt x) (coerceCxt y)