{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
-- | Symantic for 'Ratio'.
module Language.Symantic.Lib.Ratio where
-import Control.Monad (liftM, liftM2)
-import Data.Proxy
import Data.Ratio (Ratio)
import qualified Data.Ratio as Ratio
-import Data.Type.Equality ((:~:)(Refl))
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
+import Language.Symantic
+import Language.Symantic.Lib.Function (a0)
+import Language.Symantic.Lib.Integral (tyIntegral)
-- * Class 'Sym_Ratio'
+type instance Sym (Proxy Ratio) = Sym_Ratio
class Sym_Ratio term where
- ratio :: Integral a => term a -> term a -> term (Ratio a)
+ ratio :: Integral a => term a -> term a -> term (Ratio a)
numerator :: term (Ratio a) -> term a
denominator :: term (Ratio a) -> term a
- default ratio :: (Trans t term, Integral a) => t term a -> t term a -> t term (Ratio a)
- default numerator :: Trans t term => t term (Ratio a) -> t term a
- default denominator :: Trans t term => t term (Ratio a) -> t term a
+ default ratio :: Sym_Ratio (UnT term) => Trans term => Integral a => term a -> term a -> term (Ratio a)
+ default numerator :: Sym_Ratio (UnT term) => Trans term => term (Ratio a) -> term a
+ default denominator :: Sym_Ratio (UnT term) => Trans term => term (Ratio a) -> term a
- ratio = trans_map2 ratio
- numerator = trans_map1 numerator
- denominator = trans_map1 denominator
+ ratio = trans2 ratio
+ numerator = trans1 numerator
+ denominator = trans1 denominator
-type instance Sym_of_Iface (Proxy Ratio) = Sym_Ratio
-type instance TyConsts_of_Iface (Proxy Ratio) = Proxy Ratio ': TyConsts_imported_by Ratio
-type instance TyConsts_imported_by Ratio =
- [ Proxy Enum
- , Proxy Eq
- -- , Proxy Fractional
- , Proxy Integral
- , Proxy Num
- , Proxy Ord
- , Proxy Real
- -- , Proxy RealFrac
- , Proxy Show
- ]
+-- Interpreting
+instance Sym_Ratio Eval where
+ ratio = eval2 (Ratio.%)
+ numerator = eval1 Ratio.numerator
+ denominator = eval1 Ratio.denominator
+instance Sym_Ratio View where
+ ratio = viewInfix "ratio" (infixL 7)
+ numerator = view1 "numerator"
+ denominator = view1 "denominator"
+instance (Sym_Ratio r1, Sym_Ratio r2) => Sym_Ratio (Dup r1 r2) where
+ ratio = dup2 @Sym_Ratio ratio
+ numerator = dup1 @Sym_Ratio numerator
+ denominator = dup1 @Sym_Ratio denominator
-instance Sym_Ratio HostI where
- ratio = liftM2 (Ratio.%)
- numerator = liftM Ratio.numerator
- denominator = liftM Ratio.denominator
-instance Sym_Ratio TextI where
- ratio = textI_infix "ratio" (infixL 7)
- numerator = textI1 "numerator"
- denominator = textI1 "denominator"
-instance (Sym_Ratio r1, Sym_Ratio r2) => Sym_Ratio (DupI r1 r2) where
- ratio = dupI2 @Sym_Ratio ratio
- numerator = dupI1 @Sym_Ratio numerator
- denominator = dupI1 @Sym_Ratio denominator
+-- Transforming
+instance (Sym_Ratio term, Sym_Lambda term) => Sym_Ratio (BetaT term)
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Ratio
- ) => Read_TyNameR TyName cs (Proxy Ratio ': rs) where
- read_TyNameR _cs (TyName "Ratio") k = k (ty @Ratio)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Ratio ': cs) where
- show_TyConst TyConstZ{} = "Ratio"
- show_TyConst (TyConstS c) = show_TyConst c
-
-instance -- Proj_TyConC
- ( Proj_TyConst cs Ratio
- , Proj_TyConsts cs (TyConsts_imported_by Ratio)
- , Proj_TyCon cs
- , Inj_TyConst cs Integral
- ) => Proj_TyConC cs (Proxy Ratio) where
- proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @Ratio)
+-- Typing
+instance FixityOf Ratio
+instance ClassInstancesFor Ratio where
+ proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
+ | Just HRefl <- proj_ConstKiTy @_ @Ratio c
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Eq)
- , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Show)
- , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Real)
- , Just TyCon <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Ord)
- {-
- , Just TyCon <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Fractional)
- -}
- , Just TyCon <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Num)
- , Just TyCon <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
- {-
- | Just Refl <- proj_TyConst q (Proxy @RealFrac)
- , Just TyCon <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
- -}
+ _ | Just Refl <- proj_Const @Eq q
+ , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+ | Just Refl <- proj_Const @Show q
+ , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+ | Just Refl <- proj_Const @Real q
+ , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
+ | Just Refl <- proj_Const @Ord q
+ , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
+ | Just Refl <- proj_Const @Fractional q
+ , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
+ | Just Refl <- proj_Const @Num q
+ , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
+ | Just Refl <- proj_Const @RealFrac q
+ , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
_ -> Nothing
- proj_TyConC _c _q = Nothing
+ proveConstraintFor _c _q = Nothing
+instance TypeInstancesFor Ratio
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Ratio
+instance (Source src, Inj_Sym ss Ratio) => ModuleFor src ss Ratio where
+ moduleFor _s = ["Ratio"] `moduleWhere`
+ [ "ratio" := teRatio
+ , "numerator" := teRatio_numerator
+ , "denominator" := teRatio_denominator
+ ]
+
+-- ** 'Type's
+tyRatio :: Source src => Type src vs a -> Type src vs (Ratio a)
+tyRatio a = tyConstLen @(K Ratio) @Ratio (lenVars a) `tyApp` a
+
+-- ** 'Term's
+teRatio :: TermDef Ratio '[Proxy a] (Integral a #> (a -> a -> Ratio a))
+teRatio = Term (tyIntegral a0) (a0 ~> a0 ~> tyRatio a0) $ teSym @Ratio $ lam2 ratio
-data instance TokenT meta (ts::[*]) (Proxy Ratio)
- = Token_Term_Ratio (EToken meta ts) (EToken meta ts)
- | Token_Term_Ratio_numerator (EToken meta ts)
- | Token_Term_Ratio_denominator (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ratio))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ratio))
-instance -- CompileI
- ( Inj_TyConst cs Ratio
- , Inj_TyConst cs Integral
- , Proj_TyCon cs
- , Compile cs is
- ) => CompileI cs is (Proxy Ratio) where
- compileI tok ctx k =
- case tok of
- Token_Term_Ratio tok_n tok_d ->
- -- (%) :: a -> a -> (a, a)
- compileO tok_n ctx $ \ty_n (TermO n) ->
- compileO tok_d ctx $ \ty_d (TermO d) ->
- check_TyEq
- (At (Just tok_n) ty_n)
- (At (Just tok_d) ty_d) $ \Refl ->
- check_TyCon (At (Just tok_n) (ty @Integral :$ ty_n)) $ \TyCon ->
- k (ty @Ratio :$ ty_n) $ TermO $
- \c -> ratio (n c) (d c)
- Token_Term_Ratio_numerator tok_r ->
- -- numerator :: Ratio a -> a
- compileO tok_r ctx $ \ty_r (TermO r) ->
- check_TyEq1 (ty @Ratio) (At (Just tok_r) ty_r) $ \Refl ty_a ->
- k ty_a $ TermO $
- \c -> numerator (r c)
- Token_Term_Ratio_denominator tok_r ->
- -- denominator :: Ratio a -> a
- compileO tok_r ctx $ \ty_r (TermO r) ->
- check_TyEq1 (ty @Ratio) (At (Just tok_r) ty_r) $ \Refl ty_a ->
- k ty_a $ TermO $
- \c -> denominator (r c)
-instance -- TokenizeT
- -- Inj_Token meta ts Ratio =>
- TokenizeT meta ts (Proxy Ratio)
-instance Gram_Term_AtomsT meta ts (Proxy Ratio) g
+teRatio_numerator, teRatio_denominator :: TermDef Ratio '[Proxy a] (Ratio a -> a)
+teRatio_numerator = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 numerator
+teRatio_denominator = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 denominator
sourcephile / git / haskell / symantic.git / blobdiff