{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Ord'. module Language.Symantic.Lib.Ord where import Control.Monad import Data.Ord (Ord) import Data.Proxy (Proxy(..)) import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (Ord(..)) import qualified Data.Kind as Kind import qualified Data.Ord as Ord import qualified Data.Text as Text import Language.Symantic.Parsing import Language.Symantic.Typing import Language.Symantic.Compiling import Language.Symantic.Interpreting import Language.Symantic.Transforming import Language.Symantic.Lib.Lambda import Language.Symantic.Lib.Eq (Sym_Eq) import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement) -- * Class 'Sym_Ord' class Sym_Eq term => Sym_Ord term where compare :: Ord a => term a -> term a -> term Ordering (<) :: Ord a => term a -> term a -> term Bool; infix 4 < (<=) :: Ord a => term a -> term a -> term Bool; infix 4 <= (>) :: Ord a => term a -> term a -> term Bool; infix 4 > (>=) :: Ord a => term a -> term a -> term Bool; infix 4 >= max :: Ord a => term a -> term a -> term a min :: Ord a => term a -> term a -> term a default compare :: (Trans t term, Ord a) => t term a -> t term a -> t term Ordering default (<) :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool default (<=) :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool default (>) :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool default (>=) :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool default max :: (Trans t term, Ord a) => t term a -> t term a -> t term a default min :: (Trans t term, Ord a) => t term a -> t term a -> t term a compare = trans_map2 compare (<) = trans_map2 (<) (<=) = trans_map2 (<=) (>) = trans_map2 (>) (>=) = trans_map2 (>=) min = trans_map2 min max = trans_map2 max -- * Class 'Sym_Ordering' class Sym_Eq term => Sym_Ordering term where ordering :: Ordering -> term Ordering default ordering :: Trans t term => Ordering -> t term Ordering ordering = trans_lift . ordering type instance Sym_of_Iface (Proxy Ord) = Sym_Ord type instance Sym_of_Iface (Proxy Ordering) = Sym_Ordering type instance TyConsts_of_Iface (Proxy Ord) = Proxy Ord ': TyConsts_imported_by (Proxy Ord) type instance TyConsts_of_Iface (Proxy Ordering) = Proxy Ordering ': TyConsts_imported_by (Proxy Ordering) type instance TyConsts_imported_by (Proxy Ord) = '[] type instance TyConsts_imported_by (Proxy Ordering) = [ Proxy Bounded , Proxy Enum , Proxy Eq , Proxy Ord , Proxy Show ] instance Sym_Ord HostI where compare = liftM2 Ord.compare (<) = liftM2 (Ord.<) (<=) = liftM2 (Ord.<=) (>) = liftM2 (Ord.>) (>=) = liftM2 (Ord.>=) min = liftM2 Ord.min max = liftM2 Ord.max instance Sym_Ordering HostI where ordering = HostI instance Sym_Ord TextI where compare = textI2 "compare" (<) = textI_infix "<" (infixN 4) (<=) = textI_infix "<=" (infixN 4) (>) = textI_infix ">" (infixN 4) (>=) = textI_infix ">=" (infixN 4) min = textI2 "min" max = textI2 "max" instance Sym_Ordering TextI where ordering o = TextI $ \_p _v -> Text.pack (show o) instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where compare = dupI2 @Sym_Ord compare (<) = dupI2 @Sym_Ord (<) (<=) = dupI2 @Sym_Ord (<=) (>) = dupI2 @Sym_Ord (>) (>=) = dupI2 @Sym_Ord (>=) min = dupI2 @Sym_Ord min max = dupI2 @Sym_Ord max instance (Sym_Ordering r1, Sym_Ordering r2) => Sym_Ordering (DupI r1 r2) where ordering o = ordering o `DupI` ordering o instance ( Read_TyNameR TyName cs rs , Inj_TyConst cs Ord ) => Read_TyNameR TyName cs (Proxy Ord ': rs) where read_TyNameR _cs (TyName "Ord") k = k (ty @Ord) read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k instance ( Read_TyNameR TyName cs rs , Inj_TyConst cs Ordering ) => Read_TyNameR TyName cs (Proxy Ordering ': rs) where read_TyNameR _cs (TyName "Ordering") k = k (ty @Ordering) read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k instance Show_TyConst cs => Show_TyConst (Proxy Ord ': cs) where show_TyConst TyConstZ{} = "Ord" show_TyConst (TyConstS c) = show_TyConst c instance Show_TyConst cs => Show_TyConst (Proxy Ordering ': cs) where show_TyConst TyConstZ{} = "Ordering" show_TyConst (TyConstS c) = show_TyConst c instance Proj_TyFamC cs TyFam_MonoElement Ordering instance Proj_TyConC cs (Proxy Ord) instance -- Proj_TyConC ( Proj_TyConst cs Ordering , Proj_TyConsts cs (TyConsts_imported_by (Proxy Ordering)) ) => Proj_TyConC cs (Proxy Ordering) where proj_TyConC _ (TyConst q :$ TyConst c) | Just Refl <- eq_skind (kind_of_TyConst c) SKiType , Just Refl <- proj_TyConst c (Proxy @Ordering) = case () of _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon _ -> Nothing proj_TyConC _c _q = Nothing data instance TokenT meta (ts::[*]) (Proxy Ord) = Token_Term_Ord_compare (EToken meta ts) | Token_Term_Ord_le (EToken meta ts) | Token_Term_Ord_lt (EToken meta ts) | Token_Term_Ord_ge (EToken meta ts) | Token_Term_Ord_gt (EToken meta ts) | Token_Term_Ord_min (EToken meta ts) | Token_Term_Ord_max (EToken meta ts) data instance TokenT meta (ts::[*]) (Proxy Ordering) = Token_Term_Ordering Ordering deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ord)) deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ordering)) deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ord)) deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ordering)) instance -- CompileI ( Inj_TyConst cs Bool , Inj_TyConst cs (->) , Inj_TyConst cs Ord , Inj_TyConst cs Ordering , Proj_TyCon cs , Compile cs is ) => CompileI cs is (Proxy Ord) where compileI :: forall meta ctx ret ls rs. TokenT meta is (Proxy Ord) -> CompileT meta ctx ret cs is ls (Proxy Ord ': rs) compileI tok ctx k = case tok of Token_Term_Ord_compare tok_a -> compare_from tok_a (ty @Ordering) compare Token_Term_Ord_le tok_a -> compare_from tok_a (ty @Bool) (<=) Token_Term_Ord_lt tok_a -> compare_from tok_a (ty @Bool) (<) Token_Term_Ord_ge tok_a -> compare_from tok_a (ty @Bool) (>=) Token_Term_Ord_gt tok_a -> compare_from tok_a (ty @Bool) (>) Token_Term_Ord_min tok_a -> op2_from tok_a min Token_Term_Ord_max tok_a -> op2_from tok_a max where compare_from :: EToken meta is -> Type cs (res::Kind.Type) -> (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term res) -> Either (Error_Term meta cs is) ret compare_from tok_a ty_res op = -- compare :: Ord a => a -> a -> Ordering -- (<=) :: Ord a => a -> a -> Bool -- (<) :: Ord a => a -> a -> Bool -- (>=) :: Ord a => a -> a -> Bool -- (>) :: Ord a => a -> a -> Bool compileO tok_a ctx $ \ty_a (TermO x) -> check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon -> k (ty_a ~> ty_res) $ TermO $ \c -> lam $ op (x c) op2_from tok_a (op::forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term a) = -- min :: Ord a => a -> a -> a -- max :: Ord a => a -> a -> a compileO tok_a ctx $ \ty_a (TermO x) -> check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon -> k (ty_a ~> ty_a) $ TermO $ \c -> lam $ \y -> op (x c) y instance -- CompileI ( Inj_TyConst cs Ordering ) => CompileI cs is (Proxy Ordering) where compileI tok _ctx k = case tok of Token_Term_Ordering o -> k (ty @Ordering) $ TermO $ \_c -> ordering o instance -- TokenizeT Inj_Token meta ts Ord => TokenizeT meta ts (Proxy Ord) where tokenizeT _t = mempty { tokenizers_infix = tokenizeTMod [] [ tokenize1 "compare" infixN5 Token_Term_Ord_compare , tokenize1 "<" (infixN 4) Token_Term_Ord_lt , tokenize1 "<=" (infixN 4) Token_Term_Ord_le , tokenize1 ">" (infixN 4) Token_Term_Ord_gt , tokenize1 ">=" (infixN 4) Token_Term_Ord_ge ] } instance -- TokenizeT Inj_Token meta ts Ordering => TokenizeT meta ts (Proxy Ordering) where tokenizeT _t = mempty { tokenizers_infix = tokenizeTMod [] [ tokenize0 "LT" infixN5 $ Token_Term_Ordering LT , tokenize0 "EQ" infixN5 $ Token_Term_Ordering EQ , tokenize0 "GT" infixN5 $ Token_Term_Ordering GT ] } instance Gram_Term_AtomsT meta ts (Proxy Ordering) g instance Gram_Term_AtomsT meta ts (Proxy Ord) g