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 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 NameTyOf Num where
  72         nameTyOf _c = ["Num"] `Mod` "Num"
  73 instance FixityOf Num
  74 instance ClassInstancesFor Num
  75 instance TypeInstancesFor Num
  76
  77 -- Compiling
  78 instance Gram_Term_AtomsFor src ss g Num
  79 instance (Source src, SymInj ss Num) => ModuleFor src ss Num where
  80         moduleFor = ["Num"] `moduleWhere`
  81          [ "abs"    := teNum_abs
  82          , "negate" := teNum_negate
  83          , "signum" := teNum_signum
  84          , "+" `withInfixB` (SideL, 6) := teNum_add
  85          , "-" `withInfixL` 6          := teNum_sub
  86          , "-" `withPrefix` 10         := teNum_negate
  87          , "*" `withInfixB` (SideL, 7) := teNum_mul
  88          , "fromInteger" := teNum_fromInteger
  89          ]
  90
  91 -- ** 'Type's
  92 tyNum :: Source src => Type src vs a -> Type src vs (Num a)
  93 tyNum a = tyConstLen @(K Num) @Num (lenVars a) `tyApp` a
  94
  95 -- ** 'Term's
  96 teNum_fromInteger :: TermDef Num '[Proxy a] (Num a #> (Integer -> a))
  97 teNum_fromInteger = Term (tyNum a0) (tyInteger ~> a0) $ teSym @Num $ lam1 fromInteger
  98
  99 teNum_abs, teNum_negate, teNum_signum :: TermDef Num '[Proxy a] (Num a #> (a -> a))
 100 teNum_abs = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 abs
 101 teNum_negate = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 negate
 102 teNum_signum = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 signum
 103
 104 teNum_add, teNum_sub, teNum_mul :: TermDef Num '[Proxy a] (Num a #> (a -> a -> a))
 105 teNum_add = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (+)
 106 teNum_sub = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (-)
 107 teNum_mul = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (*)