Language/Symantic/Compiling/Num.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Num'.
   4 module Language.Symantic.Compiling.Num where
   5
   6 import Control.Monad (liftM, liftM2)
   7 import qualified Data.Function as Fun
   8 import Data.Proxy
   9 import Data.Text (Text)
  10 import Data.Type.Equality ((:~:)(Refl))
  11 import qualified Prelude
  12 import Prelude hiding (Num(..))
  13 import Prelude (Num)
  14
  15 import Language.Symantic.Parsing
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling.Term
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  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
  27         (-)         :: Num n => term n -> term n -> term n
  28         (*)         :: Num n => term n -> term n -> term n
  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 infixl 6 +
  48 infixl 6 -
  49 infixl 7 *
  50
  51 type instance Sym_of_Iface (Proxy Num) = Sym_Num
  52 type instance Consts_of_Iface (Proxy Num) = Proxy Num ': Consts_imported_by Num
  53 type instance Consts_imported_by Num =
  54  '[ Proxy Integer
  55  ]
  56
  57 instance Sym_Num HostI where
  58         abs         = liftM Prelude.abs
  59         negate      = liftM Prelude.negate
  60         signum      = liftM Prelude.signum
  61         (+)         = liftM2 (Prelude.+)
  62         (-)         = liftM2 (Prelude.-)
  63         (*)         = liftM2 (Prelude.*)
  64         fromInteger = liftM Prelude.fromInteger
  65 instance Sym_Num TextI where
  66         abs         = textI1 "abs"
  67         negate      = textI1 "negate"
  68         signum      = textI1 "signum"
  69         (+)         = textI_infix "+" (Precedence 6)
  70         (-)         = textI_infix "-" (Precedence 6)
  71         (*)         = textI_infix "-" (Precedence 7)
  72         fromInteger = textI1 "fromInteger"
  73 instance (Sym_Num r1, Sym_Num r2) => Sym_Num (DupI r1 r2) where
  74         abs         = dupI1 (Proxy @Sym_Num) abs
  75         negate      = dupI1 (Proxy @Sym_Num) negate
  76         signum      = dupI1 (Proxy @Sym_Num) signum
  77         (+)         = dupI2 (Proxy @Sym_Num) (+)
  78         (-)         = dupI2 (Proxy @Sym_Num) (-)
  79         (*)         = dupI2 (Proxy @Sym_Num) (*)
  80         fromInteger = dupI1 (Proxy @Sym_Num) fromInteger
  81
  82 instance
  83  ( Read_TypeNameR Text cs rs
  84  , Inj_Const cs Num
  85  ) => Read_TypeNameR Text cs (Proxy Num ': rs) where
  86         read_typenameR _cs "Num" k = k (ty @Num)
  87         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  88 instance Show_Const cs => Show_Const (Proxy Num ': cs) where
  89         show_const ConstZ{} = "Num"
  90         show_const (ConstS c) = show_const c
  91
  92 instance Proj_ConC cs (Proxy Num)
  93 data instance TokenT meta (ts::[*]) (Proxy Num)
  94  = Token_Term_Num_abs         (EToken meta ts)
  95  | Token_Term_Num_negate      (EToken meta ts)
  96  | Token_Term_Num_signum      (EToken meta ts)
  97  | Token_Term_Num_add         (EToken meta ts)
  98  | Token_Term_Num_sub         (EToken meta ts)
  99  | Token_Term_Num_mul         (EToken meta ts)
 100  | Token_Term_Num_fromInteger (EToken meta '[Proxy Token_Type])
 101 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Num))
 102 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Num))
 103 instance -- CompileI
 104  ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
 105  , Inj_Const (Consts_of_Ifaces is) Num
 106  , Inj_Const (Consts_of_Ifaces is) (->)
 107  , Inj_Const (Consts_of_Ifaces is) Integer
 108  , Proj_Con  (Consts_of_Ifaces is)
 109  , Compile is
 110  ) => CompileI is (Proxy Num) where
 111         compileI tok ctx k =
 112                 case tok of
 113                  Token_Term_Num_abs    tok_a -> op1_from tok_a abs
 114                  Token_Term_Num_negate tok_a -> op1_from tok_a negate
 115                  Token_Term_Num_signum tok_a -> op1_from tok_a signum
 116                  Token_Term_Num_add    tok_a -> op2_from tok_a (+)
 117                  Token_Term_Num_sub    tok_a -> op2_from tok_a (-)
 118                  Token_Term_Num_mul    tok_a -> op2_from tok_a (*)
 119                  Token_Term_Num_fromInteger tok_ty_a ->
 120                         -- fromInteger :: Num a => Integer -> a
 121                         compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 122                         check_kind
 123                          (At Nothing SKiType)
 124                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 125                         check_con (At (Just tok_ty_a) (ty @Num :$ ty_a)) $ \Con ->
 126                         k (ty @Integer ~> ty_a) $ TermO $
 127                                 Fun.const $ lam fromInteger
 128                 where
 129                 op1_from tok_a
 130                  (op::forall term a. (Sym_Num term, Num a)
 131                          => term a -> term a) =
 132                  -- abs    :: Num a => a -> a
 133                  -- negate :: Num a => a -> a
 134                  -- signum :: Num a => a -> a
 135                         compileO tok_a ctx $ \ty_a (TermO x) ->
 136                         check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con ->
 137                         k ty_a $ TermO $
 138                          \c -> op (x c)
 139                 op2_from tok_a
 140                  (op::forall term a. (Sym_Num term, Num a)
 141                          => term a -> term a -> term a) =
 142                  -- (+) :: Num a => a -> a -> a
 143                  -- (-) :: Num a => a -> a -> a
 144                  -- (*) :: Num a => a -> a -> a
 145                         compileO tok_a ctx $ \ty_a (TermO x) ->
 146                         check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con ->
 147                         k (ty_a ~> ty_a) $ TermO $
 148                          \c -> lam $ \y -> op (x c) y