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 (Proxy 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 FixityOf Real
  35 instance ClassInstancesFor Real
  36 instance TypeInstancesFor Real
  37
  38 -- Compiling
  39 instance Gram_Term_AtomsFor src ss g Real
  40 instance (Source src, Inj_Sym ss Real) => ModuleFor src ss Real where
  41         moduleFor _s = ["Real"] `moduleWhere`
  42          [ "toRational" := teReal_toRational
  43          ]
  44
  45 -- ** 'Type's
  46 tyReal :: Source src => Type src vs a -> Type src vs (Real a)
  47 tyReal a = tyConstLen @(K Real) @Real (lenVars a) `tyApp` a
  48
  49 tyRational :: Source src => Inj_Len vs => Type src vs Rational
  50 tyRational = tyRatio tyInteger
  51
  52 -- ** 'Term's
  53 teReal_toRational :: TermDef Real '[Proxy a] (Real a #> (a -> Rational))
  54 teReal_toRational = Term (tyReal a0) (a0 ~> tyRational) $ teSym @Real $ lam1 toRational