{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Num'. module Language.Symantic.Lib.Num where import Prelude (Num) import Prelude hiding (Num(..)) import qualified Prelude import Language.Symantic import Language.Symantic.Lib.Function (a0) import Language.Symantic.Lib.Integer (tyInteger) -- * Class 'Sym_Num' type instance Sym Num = Sym_Num class Sym_Num term where abs :: Num n => term n -> term n negate :: Num n => term n -> term n signum :: Num n => term n -> term n (+) :: Num n => term n -> term n -> term n; infixl 6 + (-) :: Num n => term n -> term n -> term n; infixl 6 - (*) :: Num n => term n -> term n -> term n; infixl 7 * fromInteger :: Num n => term Integer -> term n default abs :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n default negate :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n default signum :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n default (+) :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n default (-) :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n default (*) :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n default fromInteger :: Sym_Num (UnT term) => Trans term => Num n => term Integer -> term n abs = trans1 abs negate = trans1 negate signum = trans1 signum (+) = trans2 (+) (-) = trans2 (-) (*) = trans2 (*) fromInteger = trans1 fromInteger -- Interpreting instance Sym_Num Eval where abs = eval1 Prelude.abs negate = eval1 Prelude.negate signum = eval1 Prelude.signum (+) = eval2 (Prelude.+) (-) = eval2 (Prelude.-) (*) = eval2 (Prelude.*) fromInteger = eval1 Prelude.fromInteger instance Sym_Num View where abs = view1 "abs" negate = view1 "negate" signum = view1 "signum" (+) = viewInfix "+" (infixB SideL 6) (-) = viewInfix "-" (infixL 6) (*) = viewInfix "*" (infixB SideL 7) fromInteger = view1 "fromInteger" instance (Sym_Num r1, Sym_Num r2) => Sym_Num (Dup r1 r2) where abs = dup1 @Sym_Num abs negate = dup1 @Sym_Num negate signum = dup1 @Sym_Num signum (+) = dup2 @Sym_Num (+) (-) = dup2 @Sym_Num (-) (*) = dup2 @Sym_Num (*) fromInteger = dup1 @Sym_Num fromInteger -- Transforming instance (Sym_Num term, Sym_Lambda term) => Sym_Num (BetaT term) -- Typing instance FixityOf Num instance ClassInstancesFor Num instance TypeInstancesFor Num -- Compiling instance Gram_Term_AtomsFor src ss g Num instance (Source src, SymInj ss Num) => ModuleFor src ss Num where moduleFor = ["Num"] `moduleWhere` [ "abs" := teNum_abs , "negate" := teNum_negate , "signum" := teNum_signum , "+" `withInfixB` (SideL, 6) := teNum_add , "-" `withInfixL` 6 := teNum_sub , "-" `withPrefix` 10 := teNum_negate , "*" `withInfixB` (SideL, 7) := teNum_mul , "fromInteger" := teNum_fromInteger ] -- ** 'Type's tyNum :: Source src => Type src vs a -> Type src vs (Num a) tyNum a = tyConstLen @(K Num) @Num (lenVars a) `tyApp` a -- ** 'Term's teNum_fromInteger :: TermDef Num '[Proxy a] (Num a #> (Integer -> a)) teNum_fromInteger = Term (tyNum a0) (tyInteger ~> a0) $ teSym @Num $ lam1 fromInteger teNum_abs, teNum_negate, teNum_signum :: TermDef Num '[Proxy a] (Num a #> (a -> a)) teNum_abs = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 abs teNum_negate = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 negate teNum_signum = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 signum teNum_add, teNum_sub, teNum_mul :: TermDef Num '[Proxy a] (Num a #> (a -> a -> a)) teNum_add = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (+) teNum_sub = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (-) teNum_mul = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (*)