{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Real'. 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) -- * Class 'Sym_Real' 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 -- Interpreting 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 -- Transforming instance (Sym_Real term, Sym_Lambda term) => Sym_Real (BetaT term) -- Typing instance FixityOf Real instance ClassInstancesFor Real instance TypeInstancesFor Real -- Compiling 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 ] -- ** 'Type's 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 -- ** 'Term's teReal_toRational :: TermDef Real '[Proxy a] (Real a #> (a -> Rational)) teReal_toRational = Term (tyReal a0) (a0 ~> tyRational) $ teSym @Real $ lam1 toRational