{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Lib.Real where
import Prelude (Real)
import Prelude hiding (Real(..))
import qualified Prelude
import Language.Symantic
import Language.Symantic.Lib.Function (a0)
import Language.Symantic.Lib.Integer (tyInteger)
import Language.Symantic.Lib.Ratio (tyRatio)
type instance Sym Real = Sym_Real
class Sym_Real term where
toRational :: Real a => term a -> term Rational
default toRational :: Sym_Real (UnT term) => Trans term => Real a => term a -> term Rational
toRational = trans1 toRational
instance Sym_Real Eval where
toRational = eval1 Prelude.toRational
instance Sym_Real View where
toRational = view1 "toRational"
instance (Sym_Real r1, Sym_Real r2) => Sym_Real (Dup r1 r2) where
toRational = dup1 @Sym_Real toRational
instance (Sym_Real term, Sym_Lambda term) => Sym_Real (BetaT term)
instance NameTyOf Real where
nameTyOf _c = ["Real"] `Mod` "Real"
instance FixityOf Real
instance ClassInstancesFor Real
instance TypeInstancesFor Real
instance Gram_Term_AtomsFor src ss g Real
instance (Source src, SymInj ss Real) => ModuleFor src ss Real where
moduleFor = ["Real"] `moduleWhere`
[ "toRational" := teReal_toRational
]
tyReal :: Source src => Type src vs a -> Type src vs (Real a)
tyReal a = tyConstLen @(K Real) @Real (lenVars a) `tyApp` a
tyRational :: Source src => LenInj vs => Type src vs Rational
tyRational = tyRatio tyInteger
teReal_toRational :: TermDef Real '[Proxy a] (Real a #> (a -> Rational))
teReal_toRational = Term (tyReal a0) (a0 ~> tyRational) $ teSym @Real $ lam1 toRational