{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Integral'. module Language.Symantic.Lib.Integral where import Prelude (Integral) import Prelude hiding (Integral(..)) import qualified Prelude import Language.Symantic import Language.Symantic.Lib.Function (a0) import Language.Symantic.Lib.Integer (tyInteger) import Language.Symantic.Lib.Tuple2 (tyTuple2) -- * Class 'Sym_Integral' type instance Sym Integral = Sym_Integral class Sym_Integral term where quot :: Integral i => term i -> term i -> term i; infixl 7 `quot` rem :: Integral i => term i -> term i -> term i; infixl 7 `rem` div :: Integral i => term i -> term i -> term i; infixl 7 `div` mod :: Integral i => term i -> term i -> term i; infixl 7 `mod` quotRem :: Integral i => term i -> term i -> term (i, i) divMod :: Integral i => term i -> term i -> term (i, i) toInteger :: Integral i => term i -> term Integer default quot :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i default rem :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i default div :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i default mod :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i default quotRem :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term (i, i) default divMod :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term (i, i) default toInteger :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term Integer quot = trans2 quot rem = trans2 rem div = trans2 div mod = trans2 mod quotRem = trans2 quotRem divMod = trans2 divMod toInteger = trans1 toInteger -- Interpreting instance Sym_Integral Eval where quot = eval2 Prelude.quot rem = eval2 Prelude.rem div = eval2 Prelude.div mod = eval2 Prelude.mod quotRem = eval2 Prelude.quotRem divMod = eval2 Prelude.divMod toInteger = eval1 Prelude.toInteger instance Sym_Integral View where quot = viewInfix "`quot`" (infixL 7) div = viewInfix "`div`" (infixL 7) rem = viewInfix "`rem`" (infixL 7) mod = viewInfix "`mod`" (infixL 7) quotRem = view2 "quotRem" divMod = view2 "divMod" toInteger = view1 "toInteger" instance (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (Dup r1 r2) where quot = dup2 @Sym_Integral quot rem = dup2 @Sym_Integral rem div = dup2 @Sym_Integral div mod = dup2 @Sym_Integral mod quotRem = dup2 @Sym_Integral quotRem divMod = dup2 @Sym_Integral divMod toInteger = dup1 @Sym_Integral toInteger -- Transforming instance (Sym_Integral term, Sym_Lambda term) => Sym_Integral (BetaT term) -- Typing instance FixityOf Integral instance ClassInstancesFor Integral instance TypeInstancesFor Integral -- Compiling instance Gram_Term_AtomsFor src ss g Integral instance (Source src, Inj_Sym ss Integral) => ModuleFor src ss Integral where moduleFor = ["Integral"] `moduleWhere` [ "quot" `withInfixL` 7 := teIntegral_quot , "rem" `withInfixL` 7 := teIntegral_rem , "div" `withInfixL` 7 := teIntegral_div , "mod" `withInfixL` 7 := teIntegral_mod , "quotRem" := teIntegral_quotRem , "divMod" := teIntegral_divMod , "toInteger" := teIntegral_toInteger ] -- ** 'Type's tyIntegral :: Source src => Type src vs a -> Type src vs (Integral a) tyIntegral a = tyConstLen @(K Integral) @Integral (lenVars a) `tyApp` a -- ** 'Term's teIntegral_quot, teIntegral_rem, teIntegral_div, teIntegral_mod :: TermDef Integral '[Proxy a] (Integral a #> (a -> a -> a)) teIntegral_quot = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 quot teIntegral_rem = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 rem teIntegral_div = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 div teIntegral_mod = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 mod teIntegral_quotRem, teIntegral_divMod :: TermDef Integral '[Proxy a] (Integral a #> (a -> a -> (a, a))) teIntegral_quotRem = Term (tyIntegral a0) (a0 ~> a0 ~> tyTuple2 a0 a0) $ teSym @Integral $ lam2 quotRem teIntegral_divMod = Term (tyIntegral a0) (a0 ~> a0 ~> tyTuple2 a0 a0) $ teSym @Integral $ lam2 divMod teIntegral_toInteger :: TermDef Integral '[Proxy a] (Integral a #> (a -> Integer)) teIntegral_toInteger = Term (tyIntegral a0) (a0 ~> tyInteger) $ teSym @Integral $ lam1 toInteger