{-# 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