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.Parsing.Grammar
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  20 import Language.Symantic.Lib.Lambda
  21
  22 -- * Class 'Sym_Num'
  23 class Sym_Num term where
  24         abs         :: Num n => term n -> term n
  25         negate      :: Num n => term n -> term n
  26         signum      :: Num n => term n -> term n
  27         (+)         :: Num n => term n -> term n -> term n
  28         (-)         :: Num n => term n -> term n -> term n
  29         (*)         :: Num n => term n -> term n -> term n
  30         fromInteger :: Num n => term Integer -> term n
  31
  32         default abs         :: (Trans t term, Num n) => t term n -> t term n
  33         default negate      :: (Trans t term, Num n) => t term n -> t term n
  34         default signum      :: (Trans t term, Num 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 (*)         :: (Trans t term, Num n) => t term n -> t term n -> t term n
  38         default fromInteger :: (Trans t term, Num n) => t term Integer -> t term n
  39
  40         abs         = trans_map1 abs
  41         negate      = trans_map1 negate
  42         signum      = trans_map1 signum
  43         (+)         = trans_map2 (+)
  44         (-)         = trans_map2 (-)
  45         (*)         = trans_map2 (*)
  46         fromInteger = trans_map1 fromInteger
  47
  48 infixl 6 +
  49 infixl 6 -
  50 infixl 7 *
  51
  52 type instance Sym_of_Iface (Proxy Num) = Sym_Num
  53 type instance Consts_of_Iface (Proxy Num) = Proxy Num ': Consts_imported_by Num
  54 type instance Consts_imported_by Num =
  55  '[ Proxy Integer
  56  ]
  57
  58 instance Sym_Num HostI where
  59         abs         = liftM Prelude.abs
  60         negate      = liftM Prelude.negate
  61         signum      = liftM Prelude.signum
  62         (+)         = liftM2 (Prelude.+)
  63         (-)         = liftM2 (Prelude.-)
  64         (*)         = liftM2 (Prelude.*)
  65         fromInteger = liftM Prelude.fromInteger
  66 instance Sym_Num TextI where
  67         abs         = textI1 "abs"
  68         negate      = textI1 "negate"
  69         signum      = textI1 "signum"
  70         (+)         = textI_infix "+" (infixB L 6)
  71         (-)         = textI_infix "-" (infixL 6)
  72         (*)         = textI_infix "*" (infixB L 7)
  73         fromInteger = textI1 "fromInteger"
  74 instance (Sym_Num r1, Sym_Num r2) => Sym_Num (DupI r1 r2) where
  75         abs         = dupI1 (Proxy @Sym_Num) abs
  76         negate      = dupI1 (Proxy @Sym_Num) negate
  77         signum      = dupI1 (Proxy @Sym_Num) signum
  78         (+)         = dupI2 (Proxy @Sym_Num) (+)
  79         (-)         = dupI2 (Proxy @Sym_Num) (-)
  80         (*)         = dupI2 (Proxy @Sym_Num) (*)
  81         fromInteger = dupI1 (Proxy @Sym_Num) fromInteger
  82
  83 instance
  84  ( Read_TypeNameR Type_Name cs rs
  85  , Inj_Const cs Num
  86  ) => Read_TypeNameR Type_Name cs (Proxy Num ': rs) where
  87         read_typenameR _cs (Type_Name "Num") k = k (ty @Num)
  88         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  89 instance Show_Const cs => Show_Const (Proxy Num ': cs) where
  90         show_const ConstZ{} = "Num"
  91         show_const (ConstS c) = show_const c
  92
  93 instance Proj_ConC cs (Proxy Num)
  94 data instance TokenT meta (ts::[*]) (Proxy Num)
  95  = Token_Term_Num_abs         (EToken meta ts)
  96  | Token_Term_Num_negate      (EToken meta ts)
  97  | Token_Term_Num_signum      (EToken meta ts)
  98  | Token_Term_Num_add         (EToken meta ts)
  99  | Token_Term_Num_sub         (EToken meta ts)
 100  | Token_Term_Num_mul         (EToken meta ts)
 101  | Token_Term_Num_fromInteger (EToken meta '[Proxy Token_Type])
 102 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Num))
 103 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Num))
 104 instance -- CompileI
 105  ( Read_TypeName Type_Name (Consts_of_Ifaces is)
 106  , Inj_Const (Consts_of_Ifaces is) Num
 107  , Inj_Const (Consts_of_Ifaces is) (->)
 108  , Inj_Const (Consts_of_Ifaces is) Integer
 109  , Proj_Con  (Consts_of_Ifaces is)
 110  , Compile is
 111  ) => CompileI is (Proxy Num) where
 112         compileI tok ctx k =
 113                 case tok of
 114                  Token_Term_Num_abs    tok_a -> op1_from tok_a abs
 115                  Token_Term_Num_negate tok_a -> op1_from tok_a negate
 116                  Token_Term_Num_signum tok_a -> op1_from tok_a signum
 117                  Token_Term_Num_add    tok_a -> op2_from tok_a (+)
 118                  Token_Term_Num_sub    tok_a -> op2_from tok_a (-)
 119                  Token_Term_Num_mul    tok_a -> op2_from tok_a (*)
 120                  Token_Term_Num_fromInteger tok_ty_a ->
 121                         -- fromInteger :: Num a => Integer -> a
 122                         compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 123                         check_kind
 124                          (At Nothing SKiType)
 125                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 126                         check_con (At (Just tok_ty_a) (ty @Num :$ ty_a)) $ \Con ->
 127                         k (ty @Integer ~> ty_a) $ TermO $
 128                                 Fun.const $ lam fromInteger
 129                 where
 130                 op1_from tok_a
 131                  (op::forall term a. (Sym_Num term, Num a)
 132                          => term a -> term a) =
 133                  -- abs    :: Num a => a -> a
 134                  -- negate :: Num a => a -> a
 135                  -- signum :: Num a => a -> a
 136                         compileO tok_a ctx $ \ty_a (TermO x) ->
 137                         check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con ->
 138                         k ty_a $ TermO $
 139                          \c -> op (x c)
 140                 op2_from tok_a
 141                  (op::forall term a. (Sym_Num term, Num a)
 142                          => term a -> term a -> term a) =
 143                  -- (+) :: Num a => a -> a -> a
 144                  -- (-) :: Num a => a -> a -> a
 145                  -- (*) :: Num a => a -> a -> a
 146                         compileO tok_a ctx $ \ty_a (TermO x) ->
 147                         check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con ->
 148                         k (ty_a ~> ty_a) $ TermO $
 149                          \c -> lam $ \y -> op (x c) y
 150 instance -- TokenizeT
 151  Inj_Token meta ts Num =>
 152  TokenizeT meta ts (Proxy Num) where
 153         tokenizeT _t = mempty
 154          { tokenizers_infix = tokenizeTMod []
 155                  [ tokenize1 "abs"    infixN5 Token_Term_Num_abs
 156                  , tokenize1 "negate" infixN5 Token_Term_Num_negate
 157                  , tokenize1 "signum" infixN5 Token_Term_Num_signum
 158                  , tokenize1 "+" (infixB L 6) Token_Term_Num_add
 159                  , tokenize1 "-" (infixL 6) Token_Term_Num_sub
 160                  , tokenize1 "*" (infixB L 7) Token_Term_Num_mul
 161                  , (Term_Name "fromInteger",) Term_ProTok
 162                          { term_protok = \meta -> ProTokPi $ \a ->
 163                                 ProTok $ inj_etoken meta $ Token_Term_Num_fromInteger a
 164                          , term_fixity = infixN5
 165                          }
 166                  ]
 167          , tokenizers_prefix = tokenizeTMod []
 168                  [ tokenize1 "-"   (Prefix 10) Token_Term_Num_negate
 169                  ]
 170          }
 171 instance Gram_Term_AtomsT meta ts (Proxy Num) g