{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances, UndecidableInstances, IncoherentInstances, GADTs #-} -------------------------------------------------------------------------------- -- | -- Module : Data.Comp.MultiParam.Ordering -- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved -- License : BSD3 -- Maintainer : Tom Hvitved -- Stability : experimental -- Portability : non-portable (GHC Extensions) -- -- This module defines ordering of signatures, which lifts to ordering of -- terms and contexts. -- -------------------------------------------------------------------------------- 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 -- |Ordering of parametric values. 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 {-| Signature ordering. An instance @OrdHD f@ gives rise to an instance @Ord (Term f)@. -} class EqHD f => OrdHD f where compareHD :: POrd a => f Var a i -> f Var a j -> FreshM Ordering {-| 'OrdHD' is propagated through sums. -} 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 {-| From an 'OrdHD' difunctor an 'Ord' instance of the corresponding term type can be derived. -} 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 {-| Ordering of terms. -} instance (HDifunctor f, OrdHD f) => Ord (Term f i) where compare x y = evalFreshM $ compareHD (coerceCxt x) (coerceCxt y)