]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Integral.hs
Massive rewrite to better support rank-1 polymorphic types.
[haskell/symantic.git] / 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