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