symantic-lib/Language/Symantic/Lib/Integral.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Integral'.
   4 module Language.Symantic.Lib.Integral where
   5
   6 import Prelude (Integral)
   7 import Prelude hiding (Integral(..))
   8 import qualified Prelude
   9
  10 import Language.Symantic
  11 import Language.Symantic.Lib.Function (a0)
  12 import Language.Symantic.Lib.Integer (tyInteger)
  13 import Language.Symantic.Lib.Tuple2 (tyTuple2)
  14
  15 -- * Class 'Sym_Integral'
  16 type instance Sym (Proxy Integral) = Sym_Integral
  17 class Sym_Integral term where
  18         quot      :: Integral i => term i -> term i -> term i; infixl 7 `quot`
  19         rem       :: Integral i => term i -> term i -> term i; infixl 7 `rem`
  20         div       :: Integral i => term i -> term i -> term i; infixl 7 `div`
  21         mod       :: Integral i => term i -> term i -> term i; infixl 7 `mod`
  22         quotRem   :: Integral i => term i -> term i -> term (i, i)
  23         divMod    :: Integral i => term i -> term i -> term (i, i)
  24         toInteger :: Integral i => term i -> term Integer
  25
  26         default quot      :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i
  27         default rem       :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i
  28         default div       :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i
  29         default mod       :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i
  30         default quotRem   :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term (i, i)
  31         default divMod    :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term (i, i)
  32         default toInteger :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term Integer
  33
  34         quot      = trans2 quot
  35         rem       = trans2 rem
  36         div       = trans2 div
  37         mod       = trans2 mod
  38         quotRem   = trans2 quotRem
  39         divMod    = trans2 divMod
  40         toInteger = trans1 toInteger
  41
  42 -- Interpreting
  43 instance Sym_Integral Eval where
  44         quot      = eval2 Prelude.quot
  45         rem       = eval2 Prelude.rem
  46         div       = eval2 Prelude.div
  47         mod       = eval2 Prelude.mod
  48         quotRem   = eval2 Prelude.quotRem
  49         divMod    = eval2 Prelude.divMod
  50         toInteger = eval1 Prelude.toInteger
  51 instance Sym_Integral View where
  52         quot      = viewInfix "`quot`" (infixL 7)
  53         div       = viewInfix "`div`"  (infixL 7)
  54         rem       = viewInfix "`rem`"  (infixL 7)
  55         mod       = viewInfix "`mod`"  (infixL 7)
  56         quotRem   = view2 "quotRem"
  57         divMod    = view2 "divMod"
  58         toInteger = view1 "toInteger"
  59 instance (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (Dup r1 r2) where
  60         quot      = dup2 @Sym_Integral quot
  61         rem       = dup2 @Sym_Integral rem
  62         div       = dup2 @Sym_Integral div
  63         mod       = dup2 @Sym_Integral mod
  64         quotRem   = dup2 @Sym_Integral quotRem
  65         divMod    = dup2 @Sym_Integral divMod
  66         toInteger = dup1 @Sym_Integral toInteger
  67
  68 -- Transforming
  69 instance (Sym_Integral term, Sym_Lambda term) => Sym_Integral (BetaT term)
  70
  71 -- Typing
  72 instance FixityOf Integral
  73 instance ClassInstancesFor Integral
  74 instance TypeInstancesFor Integral
  75
  76 -- Compiling
  77 instance Gram_Term_AtomsFor src ss g Integral
  78 instance (Source src, Inj_Sym ss Integral) => Module src ss Integral where
  79         module_ _s = [] `moduleWhere`
  80          [ "quot" `withInfixL` 7 := teIntegral_quot
  81          , "rem"  `withInfixL` 7 := teIntegral_rem
  82          , "div"  `withInfixL` 7 := teIntegral_div
  83          , "mod"  `withInfixL` 7 := teIntegral_mod
  84          , "quotRem"   := teIntegral_quotRem
  85          , "divMod"    := teIntegral_divMod
  86          , "toInteger" := teIntegral_toInteger
  87          ]
  88
  89 -- ** 'Type's
  90 tyIntegral :: Source src => Type src vs a -> Type src vs (Integral a)
  91 tyIntegral a = tyConstLen @(K Integral) @Integral (lenVars a) `tyApp` a
  92
  93 -- ** 'Term's
  94 teIntegral_quot, teIntegral_rem, teIntegral_div, teIntegral_mod :: TermDef Integral '[Proxy a] (Integral a #> (a -> a -> a))
  95 teIntegral_quot = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 quot
  96 teIntegral_rem  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 rem
  97 teIntegral_div  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 div
  98 teIntegral_mod  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 mod
  99
 100 teIntegral_quotRem, teIntegral_divMod :: TermDef Integral '[Proxy a] (Integral a #> (a -> a -> (a, a)))
 101 teIntegral_quotRem = Term (tyIntegral a0) (a0 ~> a0 ~> tyTuple2 a0 a0) $ teSym @Integral $ lam2 quotRem
 102 teIntegral_divMod  = Term (tyIntegral a0) (a0 ~> a0 ~> tyTuple2 a0 a0) $ teSym @Integral $ lam2 divMod
 103
 104 teIntegral_toInteger :: TermDef Integral '[Proxy a] (Integral a #> (a -> Integer))
 105 teIntegral_toInteger = Term (tyIntegral a0) (a0 ~> tyInteger) $ teSym @Integral $ lam1 toInteger