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 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 NameTyOf Integral where
  73         nameTyOf _c = ["Integral"] `Mod` "Integral"
  74 instance FixityOf Integral
  75 instance ClassInstancesFor Integral
  76 instance TypeInstancesFor Integral
  77
  78 -- Compiling
  79 instance Gram_Term_AtomsFor src ss g Integral
  80 instance (Source src, SymInj ss Integral) => ModuleFor src ss Integral where
  81         moduleFor = ["Integral"] `moduleWhere`
  82          [ "quot" `withInfixL` 7 := teIntegral_quot
  83          , "rem"  `withInfixL` 7 := teIntegral_rem
  84          , "div"  `withInfixL` 7 := teIntegral_div
  85          , "mod"  `withInfixL` 7 := teIntegral_mod
  86          , "quotRem"   := teIntegral_quotRem
  87          , "divMod"    := teIntegral_divMod
  88          , "toInteger" := teIntegral_toInteger
  89          ]
  90
  91 -- ** 'Type's
  92 tyIntegral :: Source src => Type src vs a -> Type src vs (Integral a)
  93 tyIntegral a = tyConstLen @(K Integral) @Integral (lenVars a) `tyApp` a
  94
  95 -- ** 'Term's
  96 teIntegral_quot, teIntegral_rem, teIntegral_div, teIntegral_mod :: TermDef Integral '[Proxy a] (Integral a #> (a -> a -> a))
  97 teIntegral_quot = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 quot
  98 teIntegral_rem  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 rem
  99 teIntegral_div  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 div
 100 teIntegral_mod  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 mod
 101
 102 teIntegral_quotRem, teIntegral_divMod :: TermDef Integral '[Proxy a] (Integral a #> (a -> a -> (a, a)))
 103 teIntegral_quotRem = Term (tyIntegral a0) (a0 ~> a0 ~> tyTuple2 a0 a0) $ teSym @Integral $ lam2 quotRem
 104 teIntegral_divMod  = Term (tyIntegral a0) (a0 ~> a0 ~> tyTuple2 a0 a0) $ teSym @Integral $ lam2 divMod
 105
 106 teIntegral_toInteger :: TermDef Integral '[Proxy a] (Integral a #> (a -> Integer))
 107 teIntegral_toInteger = Term (tyIntegral a0) (a0 ~> tyInteger) $ teSym @Integral $ lam1 toInteger