symantic-lib/Language/Symantic/Lib/Ratio.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
   4 -- | Symantic for 'Ratio'.
   5 module Language.Symantic.Lib.Ratio where
   6
   7 import Control.Monad (liftM, liftM2)
   8 import Data.Proxy
   9 import Data.Ratio (Ratio)
  10 import qualified Data.Ratio as Ratio
  11 import Data.Type.Equality ((:~:)(Refl))
  12
  13 import Language.Symantic.Parsing
  14 import Language.Symantic.Typing
  15 import Language.Symantic.Compiling
  16 import Language.Symantic.Interpreting
  17 import Language.Symantic.Transforming
  18
  19 -- * Class 'Sym_Ratio'
  20 class Sym_Ratio term where
  21         ratio :: Integral a => term a -> term a -> term (Ratio a)
  22         numerator   :: term (Ratio a) -> term a
  23         denominator :: term (Ratio a) -> term a
  24
  25         default ratio :: (Trans t term, Integral a) => t term a -> t term a -> t term (Ratio a)
  26         default numerator   :: Trans t term => t term (Ratio a) -> t term a
  27         default denominator :: Trans t term => t term (Ratio a) -> t term a
  28
  29         ratio       = trans_map2 ratio
  30         numerator   = trans_map1 numerator
  31         denominator = trans_map1 denominator
  32
  33 type instance Sym_of_Iface (Proxy Ratio) = Sym_Ratio
  34 type instance TyConsts_of_Iface (Proxy Ratio) = Proxy Ratio ': TyConsts_imported_by Ratio
  35 type instance TyConsts_imported_by Ratio =
  36  [ Proxy Enum
  37  , Proxy Eq
  38  -- , Proxy Fractional
  39  , Proxy Integral
  40  , Proxy Num
  41  , Proxy Ord
  42  , Proxy Real
  43  -- , Proxy RealFrac
  44  , Proxy Show
  45  ]
  46
  47 instance Sym_Ratio HostI where
  48         ratio       = liftM2 (Ratio.%)
  49         numerator   = liftM  Ratio.numerator
  50         denominator = liftM  Ratio.denominator
  51 instance Sym_Ratio TextI where
  52         ratio       = textI_infix "ratio" (infixL 7)
  53         numerator   = textI1 "numerator"
  54         denominator = textI1 "denominator"
  55 instance (Sym_Ratio r1, Sym_Ratio r2) => Sym_Ratio (DupI r1 r2) where
  56         ratio       = dupI2 @Sym_Ratio ratio
  57         numerator   = dupI1 @Sym_Ratio numerator
  58         denominator = dupI1 @Sym_Ratio denominator
  59
  60 instance
  61  ( Read_TyNameR TyName cs rs
  62  , Inj_TyConst cs Ratio
  63  ) => Read_TyNameR TyName cs (Proxy Ratio ': rs) where
  64         read_TyNameR _cs (TyName "Ratio") k = k (ty @Ratio)
  65         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  66 instance Show_TyConst cs => Show_TyConst (Proxy Ratio ': cs) where
  67         show_TyConst TyConstZ{} = "Ratio"
  68         show_TyConst (TyConstS c) = show_TyConst c
  69
  70 instance -- Proj_TyConC
  71  ( Proj_TyConst cs Ratio
  72  , Proj_TyConsts cs (TyConsts_imported_by Ratio)
  73  , Proj_TyCon cs
  74  , Inj_TyConst cs Integral
  75  ) => Proj_TyConC cs (Proxy Ratio) where
  76         proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
  77          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
  78          , Just Refl <- proj_TyConst c (Proxy @Ratio)
  79          = case () of
  80                  _ | Just Refl  <- proj_TyConst q (Proxy @Eq)
  81                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
  82                    | Just Refl  <- proj_TyConst q (Proxy @Show)
  83                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
  84                    | Just Refl  <- proj_TyConst q (Proxy @Real)
  85                    , Just TyCon  <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
  86                    | Just Refl  <- proj_TyConst q (Proxy @Ord)
  87                    {-
  88                    , Just TyCon  <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
  89                    | Just Refl  <- proj_TyConst q (Proxy @Fractional)
  90                    -}
  91                    , Just TyCon  <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
  92                    | Just Refl  <- proj_TyConst q (Proxy @Num)
  93                    , Just TyCon  <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
  94                    {-
  95                    | Just Refl  <- proj_TyConst q (Proxy @RealFrac)
  96                    , Just TyCon  <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
  97                    -}
  98                  _ -> Nothing
  99         proj_TyConC _c _q = Nothing
 100
 101 data instance TokenT meta (ts::[*]) (Proxy Ratio)
 102  = Token_Term_Ratio             (EToken meta ts) (EToken meta ts)
 103  | Token_Term_Ratio_numerator   (EToken meta ts)
 104  | Token_Term_Ratio_denominator (EToken meta ts)
 105 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ratio))
 106 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ratio))
 107 instance -- CompileI
 108  ( Inj_TyConst cs Ratio
 109  , Inj_TyConst cs Integral
 110  , Proj_TyCon  cs
 111  , Compile cs is
 112  ) => CompileI cs is (Proxy Ratio) where
 113         compileI tok ctx k =
 114                 case tok of
 115                  Token_Term_Ratio tok_n tok_d ->
 116                         -- (%) :: a -> a -> (a, a)
 117                         compileO tok_n ctx $ \ty_n (TermO n) ->
 118                         compileO tok_d ctx $ \ty_d (TermO d) ->
 119                         check_TyEq
 120                          (At (Just tok_n) ty_n)
 121                          (At (Just tok_d) ty_d) $ \Refl ->
 122                         check_TyCon (At (Just tok_n) (ty @Integral :$ ty_n)) $ \TyCon ->
 123                         k (ty @Ratio :$ ty_n) $ TermO $
 124                          \c -> ratio (n c) (d c)
 125                  Token_Term_Ratio_numerator tok_r ->
 126                         -- numerator :: Ratio a -> a
 127                         compileO tok_r ctx $ \ty_r (TermO r) ->
 128                         check_TyEq1 (ty @Ratio) (At (Just tok_r) ty_r) $ \Refl ty_a ->
 129                         k ty_a $ TermO $
 130                          \c -> numerator (r c)
 131                  Token_Term_Ratio_denominator tok_r ->
 132                         -- denominator :: Ratio a -> a
 133                         compileO tok_r ctx $ \ty_r (TermO r) ->
 134                         check_TyEq1 (ty @Ratio) (At (Just tok_r) ty_r) $ \Refl ty_a ->
 135                         k ty_a $ TermO $
 136                          \c -> denominator (r c)
 137 instance -- TokenizeT
 138  -- Inj_Token meta ts Ratio =>
 139  TokenizeT meta ts (Proxy Ratio)
 140 instance Gram_Term_AtomsT meta ts (Proxy Ratio) g