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         = textI_app1 "abs"
  67         negate      = textI_app1 "negate"
  68         signum      = textI_app1 "signum"
  69         (+)         = textI_infix "+" (Precedence 6)
  70         (-)         = textI_infix "-" (Precedence 6)
  71         (*)         = textI_infix "-" (Precedence 7)
  72         fromInteger = textI_app1 "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 Const_from Text cs => Const_from Text (Proxy Num ': cs) where
  83         const_from "Num" k = k (ConstZ kind)
  84         const_from s k = const_from s $ k . ConstS
  85 instance Show_Const cs => Show_Const (Proxy Num ': cs) where
  86         show_const ConstZ{} = "Num"
  87         show_const (ConstS c) = show_const c
  88
  89 instance Proj_ConC cs (Proxy Num)
  90 data instance TokenT meta (ts::[*]) (Proxy Num)
  91  = Token_Term_Num_abs         (EToken meta ts)
  92  | Token_Term_Num_negate      (EToken meta ts)
  93  | Token_Term_Num_signum      (EToken meta ts)
  94  | Token_Term_Num_add         (EToken meta ts)
  95  | Token_Term_Num_sub         (EToken meta ts)
  96  | Token_Term_Num_mul         (EToken meta ts)
  97  | Token_Term_Num_fromInteger (EToken meta '[Proxy Token_Type])
  98 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Num))
  99 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Num))
 100 instance -- CompileI
 101  ( Const_from Name_LamVar (Consts_of_Ifaces is)
 102  , Inj_Const (Consts_of_Ifaces is) Num
 103  , Inj_Const (Consts_of_Ifaces is) (->)
 104  , Inj_Const (Consts_of_Ifaces is) Integer
 105  , Proj_Con  (Consts_of_Ifaces is)
 106  , Compile is
 107  ) => CompileI is (Proxy Num) where
 108         compileI tok ctx k =
 109                 case tok of
 110                  Token_Term_Num_abs    tok_a -> op1_from tok_a abs
 111                  Token_Term_Num_negate tok_a -> op1_from tok_a negate
 112                  Token_Term_Num_signum tok_a -> op1_from tok_a signum
 113                  Token_Term_Num_add    tok_a -> op2_from tok_a (+)
 114                  Token_Term_Num_sub    tok_a -> op2_from tok_a (-)
 115                  Token_Term_Num_mul    tok_a -> op2_from tok_a (*)
 116                  Token_Term_Num_fromInteger tok_ty_a ->
 117                         -- fromInteger :: Num a => Integer -> a
 118                         type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 119                         check_kind
 120                          (At Nothing SKiType)
 121                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 122                         check_con (At (Just tok_ty_a) (ty @Num :$ ty_a)) $ \Con ->
 123                         k (ty @Integer ~> ty_a) $ TermO $
 124                                 Fun.const $ lam fromInteger
 125                 where
 126                 op1_from tok_a
 127                  (op::forall term a. (Sym_Num term, Num a)
 128                          => term a -> term a) =
 129                  -- abs    :: Num a => a -> a
 130                  -- negate :: Num a => a -> a
 131                  -- signum :: Num a => a -> a
 132                         compileO tok_a ctx $ \ty_a (TermO x) ->
 133                         check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con ->
 134                         k ty_a $ TermO $
 135                          \c -> op (x c)
 136                 op2_from tok_a
 137                  (op::forall term a. (Sym_Num term, Num a)
 138                          => term a -> term a -> term a) =
 139                  -- (+) :: Num a => a -> a -> a
 140                  -- (-) :: Num a => a -> a -> a
 141                  -- (*) :: Num a => a -> a -> a
 142                         compileO tok_a ctx $ \ty_a (TermO x) ->
 143                         check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con ->
 144                         k (ty_a ~> ty_a) $ TermO $
 145                          \c -> lam $ \y -> op (x c) y