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 Prelude (Num)
   7 import Prelude hiding (Num(..))
   8 import qualified Prelude
   9
  10 import Language.Symantic
  11 import Language.Symantic.Lib.Function (a0)
  12 import Language.Symantic.Lib.Integer (tyInteger)
  13
  14 -- * Class 'Sym_Num'
  15 type instance Sym (Proxy Num) = Sym_Num
  16 class Sym_Num term where
  17         abs         :: Num n => term n -> term n
  18         negate      :: Num n => term n -> term n
  19         signum      :: Num n => term n -> term n
  20         (+)         :: Num n => term n -> term n -> term n; infixl 6 +
  21         (-)         :: Num n => term n -> term n -> term n; infixl 6 -
  22         (*)         :: Num n => term n -> term n -> term n; infixl 7 *
  23         fromInteger :: Num n => term Integer -> term n
  24
  25         default abs         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n
  26         default negate      :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n
  27         default signum      :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n
  28         default (+)         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n
  29         default (-)         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n
  30         default (*)         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n
  31         default fromInteger :: Sym_Num (UnT term) => Trans term => Num n => term Integer -> term n
  32
  33         abs         = trans1 abs
  34         negate      = trans1 negate
  35         signum      = trans1 signum
  36         (+)         = trans2 (+)
  37         (-)         = trans2 (-)
  38         (*)         = trans2 (*)
  39         fromInteger = trans1 fromInteger
  40
  41 -- Interpreting
  42 instance Sym_Num Eval where
  43         abs         = eval1 Prelude.abs
  44         negate      = eval1 Prelude.negate
  45         signum      = eval1 Prelude.signum
  46         (+)         = eval2 (Prelude.+)
  47         (-)         = eval2 (Prelude.-)
  48         (*)         = eval2 (Prelude.*)
  49         fromInteger = eval1 Prelude.fromInteger
  50 instance Sym_Num View where
  51         abs         = view1 "abs"
  52         negate      = view1 "negate"
  53         signum      = view1 "signum"
  54         (+)         = viewInfix "+" (infixB SideL 6)
  55         (-)         = viewInfix "-" (infixL 6)
  56         (*)         = viewInfix "*" (infixB SideL 7)
  57         fromInteger = view1 "fromInteger"
  58 instance (Sym_Num r1, Sym_Num r2) => Sym_Num (Dup r1 r2) where
  59         abs         = dup1 @Sym_Num abs
  60         negate      = dup1 @Sym_Num negate
  61         signum      = dup1 @Sym_Num signum
  62         (+)         = dup2 @Sym_Num (+)
  63         (-)         = dup2 @Sym_Num (-)
  64         (*)         = dup2 @Sym_Num (*)
  65         fromInteger = dup1 @Sym_Num fromInteger
  66
  67 -- Transforming
  68 instance (Sym_Num term, Sym_Lambda term) => Sym_Num (BetaT term)
  69
  70 -- Typing
  71 instance FixityOf Num
  72 instance ClassInstancesFor Num
  73 instance TypeInstancesFor Num
  74
  75 -- Compiling
  76 instance Gram_Term_AtomsFor src ss g Num
  77 instance (Source src, Inj_Sym ss Num) => Module src ss Num where
  78         module_ _s = [] `moduleWhere`
  79          [ "abs"    := teNum_abs
  80          , "negate" := teNum_negate
  81          , "signum" := teNum_signum
  82          , "+" `withInfixB` (SideL, 6) := teNum_add
  83          , "-" `withInfixL` 6          := teNum_sub
  84          , "-" `withPrefix` 10         := teNum_negate
  85          , "*" `withInfixB` (SideL, 7) := teNum_mul
  86          , "fromInteger" := teNum_fromInteger
  87          ]
  88
  89 -- ** 'Type's
  90 tyNum :: Source src => Type src vs a -> Type src vs (Num a)
  91 tyNum a = tyConstLen @(K Num) @Num (lenVars a) `tyApp` a
  92
  93 -- ** 'Term's
  94 teNum_fromInteger :: TermDef Num '[Proxy a] (Num a #> (Integer -> a))
  95 teNum_fromInteger = Term (tyNum a0) (tyInteger ~> a0) $ teSym @Num $ lam1 fromInteger
  96
  97 teNum_abs, teNum_negate, teNum_signum :: TermDef Num '[Proxy a] (Num a #> (a -> a))
  98 teNum_abs = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 abs
  99 teNum_negate = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 negate
 100 teNum_signum = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 signum
 101
 102 teNum_add, teNum_sub, teNum_mul :: TermDef Num '[Proxy a] (Num a #> (a -> a -> a))
 103 teNum_add = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (+)
 104 teNum_sub = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (-)
 105 teNum_mul = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (*)