-- | 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
+import Language.Symantic.Lib.Bool (tyBool)
+import Language.Symantic.Lib.Function (a0)
import Language.Symantic.Lib.Eq (Sym_Eq)
-import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement)
+
+-- * Class 'Sym_Ordering'
+type instance Sym Ordering = Sym_Ordering
+class Sym_Eq term => Sym_Ordering term where
+ ordering :: Ordering -> term Ordering
+ default ordering :: Sym_Ordering (UnT term) => Trans term => Ordering -> term Ordering
+ ordering = trans . ordering
+
+-- Interpreting
+instance Sym_Ordering Eval where
+ ordering = Eval
+instance Sym_Ordering View where
+ ordering o = View $ \_p _v ->
+ Text.pack (show o)
+instance (Sym_Ordering r1, Sym_Ordering r2) => Sym_Ordering (Dup r1 r2) where
+ ordering o = ordering o `Dup` ordering o
+
+-- Transforming
+instance (Sym_Ordering term, Sym_Lambda term) => Sym_Ordering (BetaT term)
+
+-- Typing
+instance NameTyOf Ordering where
+ nameTyOf _c = ["Ord"] `Mod` "Ordering"
+instance ClassInstancesFor Ordering
+instance TypeInstancesFor Ordering
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Ordering
+instance (Source src, SymInj ss Ordering) => ModuleFor src ss Ordering where
+ moduleFor = [] `moduleWhere`
+ [ "LT" := teOrdering LT
+ , "EQ" := teOrdering EQ
+ , "GT" := teOrdering GT
+ ]
+
+-- ** 'Type's
+tyOrdering :: Source src => LenInj vs => Type src vs Ordering
+tyOrdering = tyConst @(K Ordering) @Ordering
+
+-- ** 'Term's
+teOrdering :: Source src => SymInj ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering)
+teOrdering o = Term noConstraint tyOrdering $ teSym @Ordering $ ordering o
-- * Class 'Sym_Ord'
+type instance Sym Ord = 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 <
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
+ default compare :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Ordering
+ default (<) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
+ default (<=) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
+ default (>) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
+ default (>=) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
+ default max :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
+ default min :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
- compare = trans_map2 compare
- (<) = trans_map2 (<)
- (<=) = trans_map2 (<=)
- (>) = trans_map2 (>)
- (>=) = trans_map2 (>=)
- min = trans_map2 min
- max = trans_map2 max
+ compare = trans2 compare
+ (<) = trans2 (<)
+ (<=) = trans2 (<=)
+ (>) = trans2 (>)
+ (>=) = trans2 (>=)
+ min = trans2 min
+ max = trans2 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) =
- [ Proxy Bool
- , Proxy Ordering
- ]
-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)
+-- Interpreting
+instance Sym_Ord Eval where
+ compare = eval2 Ord.compare
+ (<) = eval2 (Ord.<)
+ (<=) = eval2 (Ord.<=)
+ (>) = eval2 (Ord.>)
+ (>=) = eval2 (Ord.>=)
+ min = eval2 Ord.min
+ max = eval2 Ord.max
+instance Sym_Ord View where
+ compare = view2 "compare"
+ (<) = viewInfix "<" (infixN 4)
+ (<=) = viewInfix "<=" (infixN 4)
+ (>) = viewInfix ">" (infixN 4)
+ (>=) = viewInfix ">=" (infixN 4)
+ min = view2 "min"
+ max = view2 "max"
+instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (Dup r1 r2) where
+ compare = dup2 @Sym_Ord compare
+ (<) = dup2 @Sym_Ord (<)
+ (<=) = dup2 @Sym_Ord (<=)
+ (>) = dup2 @Sym_Ord (>)
+ (>=) = dup2 @Sym_Ord (>=)
+ min = dup2 @Sym_Ord min
+ max = dup2 @Sym_Ord max
+
+-- Transforming
+instance (Sym_Ord term, Sym_Lambda term) => Sym_Ord (BetaT term)
+
+-- Typing
+instance NameTyOf Ord where
+ nameTyOf _c = ["Ord"] `Mod` "Ord"
+instance FixityOf Ord
+instance ClassInstancesFor Ord where
+ proveConstraintFor _ (TyConst _ _ q :$ z)
+ | Just HRefl <- proj_ConstKiTy @_ @Ordering z
= 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
+ _ | Just Refl <- proj_Const @Bounded q -> Just Dict
+ | Just Refl <- proj_Const @Enum q -> Just Dict
+ | Just Refl <- proj_Const @Eq q -> Just Dict
+ | Just Refl <- proj_Const @Ord q -> Just Dict
+ | Just Refl <- proj_Const @Show q -> Just Dict
_ -> 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)
- -> Compiler 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
- compile tok_a ctx $ \ty_a (Term x) ->
- check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
- k (ty_a ~> ty_res) $ Term $
- \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
- compile tok_a ctx $ \ty_a (Term x) ->
- check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
- k (ty_a ~> ty_a) $ Term $
- \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) $ Term $ \_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
+ proveConstraintFor _c _q = Nothing
+instance TypeInstancesFor Ord
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Ord
+instance (Source src, SymInj ss Ord) => ModuleFor src ss Ord where
+ moduleFor = ["Ord"] `moduleWhere`
+ [ "compare" := teOrd_compare
+ , "<" `withInfixN` 4 := teOrd_lt
+ , "<=" `withInfixN` 4 := teOrd_le
+ , ">" `withInfixN` 4 := teOrd_gt
+ , ">=" `withInfixN` 4 := teOrd_ge
+ ]
+
+-- ** 'Type's
+tyOrd :: Source src => Type src vs a -> Type src vs (Ord a)
+tyOrd a = tyConstLen @(K Ord) @Ord (lenVars a) `tyApp` a
+
+-- ** 'Term's
+teOrd_compare :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Ordering))
+teOrd_compare = Term (tyOrd a0) (a0 ~> a0 ~> tyOrdering) $ teSym @Ord $ lam2 compare
+
+teOrd_le, teOrd_lt, teOrd_ge, teOrd_gt :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Bool))
+teOrd_le = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<=)
+teOrd_lt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<)
+teOrd_ge = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>=)
+teOrd_gt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>)
+
+teOrd_min, teOrd_max :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> a))
+teOrd_min = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 min
+teOrd_max = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 max
sourcephile / git / haskell / symantic.git / blobdiff