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