{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Num'. module Language.Symantic.Compiling.Num where import Control.Monad (liftM, liftM2) import qualified Data.Function as Fun import Data.Proxy import Data.Text (Text) import Data.Type.Equality ((:~:)(Refl)) import qualified Prelude import Prelude hiding (Num(..)) import Prelude (Num) import Language.Symantic.Parsing import Language.Symantic.Typing import Language.Symantic.Compiling.Term import Language.Symantic.Interpreting import Language.Symantic.Transforming.Trans -- * Class '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 (-) :: Num n => term n -> term n -> term n (*) :: Num n => term n -> term n -> term n fromInteger :: Num n => term Integer -> term n default abs :: (Trans t term, Num n) => t term n -> t term n default negate :: (Trans t term, Num n) => t term n -> t term n default signum :: (Trans t term, Num n) => t term n -> t term n default (+) :: (Trans t term, Num n) => t term n -> t term n -> t term n default (-) :: (Trans t term, Num n) => t term n -> t term n -> t term n default (*) :: (Trans t term, Num n) => t term n -> t term n -> t term n default fromInteger :: (Trans t term, Num n) => t term Integer -> t term n abs = trans_map1 abs negate = trans_map1 negate signum = trans_map1 signum (+) = trans_map2 (+) (-) = trans_map2 (-) (*) = trans_map2 (*) fromInteger = trans_map1 fromInteger infixl 6 + infixl 6 - infixl 7 * type instance Sym_of_Iface (Proxy Num) = Sym_Num type instance Consts_of_Iface (Proxy Num) = Proxy Num ': Consts_imported_by Num type instance Consts_imported_by Num = '[ Proxy Integer ] instance Sym_Num HostI where abs = liftM Prelude.abs negate = liftM Prelude.negate signum = liftM Prelude.signum (+) = liftM2 (Prelude.+) (-) = liftM2 (Prelude.-) (*) = liftM2 (Prelude.*) fromInteger = liftM Prelude.fromInteger instance Sym_Num TextI where abs = textI_app1 "abs" negate = textI_app1 "negate" signum = textI_app1 "signum" (+) = textI_infix "+" (Precedence 6) (-) = textI_infix "-" (Precedence 6) (*) = textI_infix "-" (Precedence 7) fromInteger = textI_app1 "fromInteger" instance (Sym_Num r1, Sym_Num r2) => Sym_Num (DupI r1 r2) where abs = dupI1 (Proxy @Sym_Num) abs negate = dupI1 (Proxy @Sym_Num) negate signum = dupI1 (Proxy @Sym_Num) signum (+) = dupI2 (Proxy @Sym_Num) (+) (-) = dupI2 (Proxy @Sym_Num) (-) (*) = dupI2 (Proxy @Sym_Num) (*) fromInteger = dupI1 (Proxy @Sym_Num) fromInteger instance Const_from Text cs => Const_from Text (Proxy Num ': cs) where const_from "Num" k = k (ConstZ kind) const_from s k = const_from s $ k . ConstS instance Show_Const cs => Show_Const (Proxy Num ': cs) where show_const ConstZ{} = "Num" show_const (ConstS c) = show_const c instance Proj_ConC cs (Proxy Num) data instance TokenT meta (ts::[*]) (Proxy Num) = Token_Term_Num_abs (EToken meta ts) | Token_Term_Num_negate (EToken meta ts) | Token_Term_Num_signum (EToken meta ts) | Token_Term_Num_add (EToken meta ts) | Token_Term_Num_sub (EToken meta ts) | Token_Term_Num_mul (EToken meta ts) | Token_Term_Num_fromInteger (EToken meta '[Proxy Token_Type]) deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Num)) deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Num)) instance -- Term_fromI ( Const_from Name_LamVar (Consts_of_Ifaces is) , Inj_Const (Consts_of_Ifaces is) Num , Inj_Const (Consts_of_Ifaces is) (->) , Inj_Const (Consts_of_Ifaces is) Integer , Proj_Con (Consts_of_Ifaces is) , Term_from is ) => Term_fromI is (Proxy Num) where term_fromI tok ctx k = case tok of Token_Term_Num_abs tok_a -> op1_from tok_a abs Token_Term_Num_negate tok_a -> op1_from tok_a negate Token_Term_Num_signum tok_a -> op1_from tok_a signum Token_Term_Num_add tok_a -> op2_from tok_a (+) Token_Term_Num_sub tok_a -> op2_from tok_a (-) Token_Term_Num_mul tok_a -> op2_from tok_a (*) Token_Term_Num_fromInteger tok_ty_a -> -- fromInteger :: Num a => Integer -> a type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) -> check_kind (At Nothing SKiType) (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl -> check_con (At (Just tok_ty_a) (ty @Num :$ ty_a)) $ \Con -> k (ty @Integer ~> ty_a) $ TermLC $ Fun.const $ lam fromInteger where op1_from tok_a (op::forall term a. (Sym_Num term, Num a) => term a -> term a) = -- abs :: Num a => a -> a -- negate :: Num a => a -> a -- signum :: Num a => a -> a term_from tok_a ctx $ \ty_a (TermLC x) -> check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con -> k ty_a $ TermLC $ \c -> op (x c) op2_from tok_a (op::forall term a. (Sym_Num term, Num a) => term a -> term a -> term a) = -- (+) :: Num a => a -> a -> a -- (-) :: Num a => a -> a -> a -- (*) :: Num a => a -> a -> a term_from tok_a ctx $ \ty_a (TermLC x) -> check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con -> k (ty_a ~> ty_a) $ TermLC $ \c -> lam $ \y -> op (x c) y