-- | Symantic for 'Num'.
module Language.Symantic.Lib.Num where
-import Control.Monad (liftM, liftM2)
-import qualified Data.Function as Fun
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
-import qualified Prelude
-import Prelude hiding (Num(..))
import Prelude (Num)
+import Prelude hiding (Num(..))
+import qualified Prelude
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
+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
(*) :: Num n => term n -> term n -> term n; infixl 7 *
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
+ 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 = trans_map1 abs
- negate = trans_map1 negate
- signum = trans_map1 signum
- (+) = trans_map2 (+)
- (-) = trans_map2 (-)
- (*) = trans_map2 (*)
- fromInteger = trans_map1 fromInteger
+ 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 NameTyOf Num where
+ nameTyOf _c = ["Num"] `Mod` "Num"
+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 instance Sym_of_Iface (Proxy Num) = Sym_Num
-type instance TyConsts_of_Iface (Proxy Num) = Proxy Num ': TyConsts_imported_by Num
-type instance TyConsts_imported_by Num =
- '[ Proxy Integer
- ]
+-- ** 'Type's
+tyNum :: Source src => Type src vs a -> Type src vs (Num a)
+tyNum a = tyConstLen @(K Num) @Num (lenVars a) `tyApp` a
-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 = textI1 "abs"
- negate = textI1 "negate"
- signum = textI1 "signum"
- (+) = textI_infix "+" (infixB L 6)
- (-) = textI_infix "-" (infixL 6)
- (*) = textI_infix "*" (infixB L 7)
- fromInteger = textI1 "fromInteger"
-instance (Sym_Num r1, Sym_Num r2) => Sym_Num (DupI r1 r2) where
- abs = dupI1 @Sym_Num abs
- negate = dupI1 @Sym_Num negate
- signum = dupI1 @Sym_Num signum
- (+) = dupI2 @Sym_Num (+)
- (-) = dupI2 @Sym_Num (-)
- (*) = dupI2 @Sym_Num (*)
- fromInteger = dupI1 @Sym_Num fromInteger
+-- ** 'Term's
+teNum_fromInteger :: TermDef Num '[Proxy a] (Num a #> (Integer -> a))
+teNum_fromInteger = Term (tyNum a0) (tyInteger ~> a0) $ teSym @Num $ lam1 fromInteger
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Num
- ) => Read_TyNameR TyName cs (Proxy Num ': rs) where
- read_TyNameR _cs (TyName "Num") k = k (ty @Num)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Num ': cs) where
- show_TyConst TyConstZ{} = "Num"
- show_TyConst (TyConstS c) = show_TyConst c
+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
-instance Proj_TyConC 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 -- CompileI
- ( Read_TyName TyName cs
- , Inj_TyConst cs Num
- , Inj_TyConst cs (->)
- , Inj_TyConst cs Integer
- , Proj_TyCon cs
- , Compile cs is
- ) => CompileI cs is (Proxy Num) where
- compileI 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
- compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
- check_Kind
- (At Nothing SKiType)
- (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
- check_TyCon (At (Just tok_ty_a) (ty @Num :$ ty_a)) $ \TyCon ->
- k (ty @Integer ~> ty_a) $ TermO $
- 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
- compileO tok_a ctx $ \ty_a (TermO x) ->
- check_TyCon (At (Just tok_a) (ty @Num :$ ty_a)) $ \TyCon ->
- k ty_a $ TermO $
- \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
- compileO tok_a ctx $ \ty_a (TermO x) ->
- check_TyCon (At (Just tok_a) (ty @Num :$ ty_a)) $ \TyCon ->
- k (ty_a ~> ty_a) $ TermO $
- \c -> lam $ \y -> op (x c) y
-instance -- TokenizeT
- Inj_Token meta ts Num =>
- TokenizeT meta ts (Proxy Num) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize1 "abs" infixN5 Token_Term_Num_abs
- , tokenize1 "negate" infixN5 Token_Term_Num_negate
- , tokenize1 "signum" infixN5 Token_Term_Num_signum
- , tokenize1 "+" (infixB L 6) Token_Term_Num_add
- , tokenize1 "-" (infixL 6) Token_Term_Num_sub
- , tokenize1 "*" (infixB L 7) Token_Term_Num_mul
- , (Term_Name "fromInteger",) Term_ProTok
- { term_protok = \meta -> ProTokPi $ \a ->
- ProTok $ inj_EToken meta $ Token_Term_Num_fromInteger a
- , term_fixity = infixN5
- }
- ]
- , tokenizers_prefix = tokenizeTMod []
- [ tokenize1 "-" (Prefix 10) Token_Term_Num_negate
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Num) g
+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 (*)
sourcephile / git / haskell / symantic.git / blobdiff