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

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Num'.
   4 module Language.Symantic.Lib.Num where
   5
   6 import Control.Monad (liftM, liftM2)
   7 import qualified Data.Function as Fun
   8 import Data.Proxy
   9 import Data.Type.Equality ((:~:)(Refl))
  10 import qualified Prelude
  11 import Prelude hiding (Num(..))
  12 import Prelude (Num)
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming
  19 import Language.Symantic.Lib.Lambda
  20
  21 -- * Class 'Sym_Num'
  22 class Sym_Num term where
  23         abs         :: Num n => term n -> term n
  24         negate      :: Num n => term n -> term n
  25         signum      :: Num n => term n -> term n
  26         (+)         :: Num n => term n -> term n -> term n; infixl 6 +
  27         (-)         :: Num n => term n -> term n -> term n; infixl 6 -
  28         (*)         :: Num n => term n -> term n -> term n; infixl 7 *
  29         fromInteger :: Num n => term Integer -> term n
  30
  31         default abs         :: (Trans t term, Num n) => t term n -> t term n
  32         default negate      :: (Trans t term, Num n) => t term n -> t term n
  33         default signum      :: (Trans t term, Num n) => t term n -> t term n
  34         default (+)         :: (Trans t term, Num n) => t term n -> t term n -> t term n
  35         default (-)         :: (Trans t term, Num n) => t term n -> t term n -> t term n
  36         default (*)         :: (Trans t term, Num n) => t term n -> t term n -> t term n
  37         default fromInteger :: (Trans t term, Num n) => t term Integer -> t term n
  38
  39         abs         = trans_map1 abs
  40         negate      = trans_map1 negate
  41         signum      = trans_map1 signum
  42         (+)         = trans_map2 (+)
  43         (-)         = trans_map2 (-)
  44         (*)         = trans_map2 (*)
  45         fromInteger = trans_map1 fromInteger
  46
  47 type instance Sym_of_Iface (Proxy Num) = Sym_Num
  48 type instance TyConsts_of_Iface (Proxy Num) = Proxy Num ': TyConsts_imported_by Num
  49 type instance TyConsts_imported_by Num =
  50  '[ Proxy Integer
  51  ]
  52
  53 instance Sym_Num HostI where
  54         abs         = liftM Prelude.abs
  55         negate      = liftM Prelude.negate
  56         signum      = liftM Prelude.signum
  57         (+)         = liftM2 (Prelude.+)
  58         (-)         = liftM2 (Prelude.-)
  59         (*)         = liftM2 (Prelude.*)
  60         fromInteger = liftM Prelude.fromInteger
  61 instance Sym_Num TextI where
  62         abs         = textI1 "abs"
  63         negate      = textI1 "negate"
  64         signum      = textI1 "signum"
  65         (+)         = textI_infix "+" (infixB L 6)
  66         (-)         = textI_infix "-" (infixL 6)
  67         (*)         = textI_infix "*" (infixB L 7)
  68         fromInteger = textI1 "fromInteger"
  69 instance (Sym_Num r1, Sym_Num r2) => Sym_Num (DupI r1 r2) where
  70         abs         = dupI1 @Sym_Num abs
  71         negate      = dupI1 @Sym_Num negate
  72         signum      = dupI1 @Sym_Num signum
  73         (+)         = dupI2 @Sym_Num (+)
  74         (-)         = dupI2 @Sym_Num (-)
  75         (*)         = dupI2 @Sym_Num (*)
  76         fromInteger = dupI1 @Sym_Num fromInteger
  77
  78 instance
  79  ( Read_TyNameR TyName cs rs
  80  , Inj_TyConst cs Num
  81  ) => Read_TyNameR TyName cs (Proxy Num ': rs) where
  82         read_TyNameR _cs (TyName "Num") k = k (ty @Num)
  83         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  84 instance Show_TyConst cs => Show_TyConst (Proxy Num ': cs) where
  85         show_TyConst TyConstZ{} = "Num"
  86         show_TyConst (TyConstS c) = show_TyConst c
  87
  88 instance Proj_TyConC cs (Proxy Num)
  89 data instance TokenT meta (ts::[*]) (Proxy Num)
  90  = Token_Term_Num_abs         (EToken meta ts)
  91  | Token_Term_Num_negate      (EToken meta ts)
  92  | Token_Term_Num_signum      (EToken meta ts)
  93  | Token_Term_Num_add         (EToken meta ts)
  94  | Token_Term_Num_sub         (EToken meta ts)
  95  | Token_Term_Num_mul         (EToken meta ts)
  96  | Token_Term_Num_fromInteger (EToken meta '[Proxy Token_Type])
  97 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Num))
  98 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Num))
  99 instance -- CompileI
 100  ( Read_TyName TyName cs
 101  , Inj_TyConst        cs Num
 102  , Inj_TyConst        cs (->)
 103  , Inj_TyConst        cs Integer
 104  , Proj_TyCon         cs
 105  , Compile cs is
 106  ) => CompileI cs is (Proxy Num) where
 107         compileI tok ctx k =
 108                 case tok of
 109                  Token_Term_Num_abs    tok_a -> op1_from tok_a abs
 110                  Token_Term_Num_negate tok_a -> op1_from tok_a negate
 111                  Token_Term_Num_signum tok_a -> op1_from tok_a signum
 112                  Token_Term_Num_add    tok_a -> op2_from tok_a (+)
 113                  Token_Term_Num_sub    tok_a -> op2_from tok_a (-)
 114                  Token_Term_Num_mul    tok_a -> op2_from tok_a (*)
 115                  Token_Term_Num_fromInteger tok_ty_a ->
 116                         -- fromInteger :: Num a => Integer -> a
 117                         compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
 118                         check_Kind
 119                          (At Nothing SKiType)
 120                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 121                         check_TyCon (At (Just tok_ty_a) (ty @Num :$ ty_a)) $ \TyCon ->
 122                         k (ty @Integer ~> ty_a) $ TermO $
 123                                 Fun.const $ lam fromInteger
 124                 where
 125                 op1_from tok_a
 126                  (op::forall term a. (Sym_Num term, Num a)
 127                          => term a -> term a) =
 128                  -- abs    :: Num a => a -> a
 129                  -- negate :: Num a => a -> a
 130                  -- signum :: Num a => a -> a
 131                         compileO tok_a ctx $ \ty_a (TermO x) ->
 132                         check_TyCon (At (Just tok_a) (ty @Num :$ ty_a)) $ \TyCon ->
 133                         k ty_a $ TermO $
 134                          \c -> op (x c)
 135                 op2_from tok_a
 136                  (op::forall term a. (Sym_Num term, Num a)
 137                          => term a -> term a -> term a) =
 138                  -- (+) :: Num a => a -> a -> a
 139                  -- (-) :: Num a => a -> a -> a
 140                  -- (*) :: Num a => a -> a -> a
 141                         compileO tok_a ctx $ \ty_a (TermO x) ->
 142                         check_TyCon (At (Just tok_a) (ty @Num :$ ty_a)) $ \TyCon ->
 143                         k (ty_a ~> ty_a) $ TermO $
 144                          \c -> lam $ \y -> op (x c) y
 145 instance -- TokenizeT
 146  Inj_Token meta ts Num =>
 147  TokenizeT meta ts (Proxy Num) where
 148         tokenizeT _t = mempty
 149          { tokenizers_infix = tokenizeTMod []
 150                  [ tokenize1 "abs"    infixN5 Token_Term_Num_abs
 151                  , tokenize1 "negate" infixN5 Token_Term_Num_negate
 152                  , tokenize1 "signum" infixN5 Token_Term_Num_signum
 153                  , tokenize1 "+" (infixB L 6) Token_Term_Num_add
 154                  , tokenize1 "-" (infixL 6) Token_Term_Num_sub
 155                  , tokenize1 "*" (infixB L 7) Token_Term_Num_mul
 156                  , (TeName "fromInteger",) ProTok_Term
 157                          { protok_term = \meta -> ProTokPi $ \a ->
 158                                 ProTok $ inj_EToken meta $ Token_Term_Num_fromInteger a
 159                          , protok_fixity = infixN5
 160                          }
 161                  ]
 162          , tokenizers_prefix = tokenizeTMod []
 163                  [ tokenize1 "-"   (Prefix 10) Token_Term_Num_negate
 164                  ]
 165          }
 166 instance Gram_Term_AtomsT meta ts (Proxy Num) g