]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Real.hs
Update to lastest symantic-document
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Real.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Real'.
4 module Language.Symantic.Lib.Real where
5
6 import Prelude (Real)
7 import Prelude hiding (Real(..))
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.Ratio (tyRatio)
14
15 -- * Class 'Sym_Real'
16 type instance Sym Real = Sym_Real
17 class Sym_Real term where
18 toRational :: Real a => term a -> term Rational
19 default toRational :: Sym_Real (UnT term) => Trans term => Real a => term a -> term Rational
20 toRational = trans1 toRational
21
22 -- Interpreting
23 instance Sym_Real Eval where
24 toRational = eval1 Prelude.toRational
25 instance Sym_Real View where
26 toRational = view1 "toRational"
27 instance (Sym_Real r1, Sym_Real r2) => Sym_Real (Dup r1 r2) where
28 toRational = dup1 @Sym_Real toRational
29
30 -- Transforming
31 instance (Sym_Real term, Sym_Lambda term) => Sym_Real (BetaT term)
32
33 -- Typing
34 instance NameTyOf Real where
35 nameTyOf _c = ["Real"] `Mod` "Real"
36 instance FixityOf Real
37 instance ClassInstancesFor Real
38 instance TypeInstancesFor Real
39
40 -- Compiling
41 instance Gram_Term_AtomsFor src ss g Real
42 instance (Source src, SymInj ss Real) => ModuleFor src ss Real where
43 moduleFor = ["Real"] `moduleWhere`
44 [ "toRational" := teReal_toRational
45 ]
46
47 -- ** 'Type's
48 tyReal :: Source src => Type src vs a -> Type src vs (Real a)
49 tyReal a = tyConstLen @(K Real) @Real (lenVars a) `tyApp` a
50
51 tyRational :: Source src => LenInj vs => Type src vs Rational
52 tyRational = tyRatio tyInteger
53
54 -- ** 'Term's
55 teReal_toRational :: TermDef Real '[Proxy a] (Real a #> (a -> Rational))
56 teReal_toRational = Term (tyReal a0) (a0 ~> tyRational) $ teSym @Real $ lam1 toRational