Language/Symantic/Expr/Num.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE OverloadedStrings #-}
   4 {-# LANGUAGE ScopedTypeVariables #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# LANGUAGE TypeOperators #-}
   7 -- | Expression for 'Num'.
   8 module Language.Symantic.Expr.Num where
   9
  10 import Control.Monad
  11 import Prelude hiding (Num(..))
  12 import Prelude (Num)
  13 import qualified Prelude
  14 import Data.Proxy (Proxy(..))
  15 import Data.Type.Equality ((:~:)(Refl))
  16
  17 import Language.Symantic.Type
  18 import Language.Symantic.Repr
  19 import Language.Symantic.Expr.Root
  20 import Language.Symantic.Expr.Error
  21 import Language.Symantic.Expr.From
  22 import Language.Symantic.Trans.Common
  23
  24 -- * Class 'Sym_Num'
  25 -- | Symantic.
  26 class Sym_Num repr where
  27         abs         :: Num n => repr n -> repr n
  28         negate      :: Num n => repr n -> repr n
  29         signum      :: Num n => repr n -> repr n
  30         (+)         :: Num n => repr n -> repr n -> repr n
  31         (-)         :: Num n => repr n -> repr n -> repr n
  32         (*)         :: Num n => repr n -> repr n -> repr n
  33         fromInteger :: Num n => repr Integer -> repr n
  34
  35         default abs         :: (Trans t repr, Num n) => t repr n -> t repr n
  36         default negate      :: (Trans t repr, Num n) => t repr n -> t repr n
  37         default signum      :: (Trans t repr, Num n) => t repr n -> t repr n
  38         default (+)         :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
  39         default (-)         :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
  40         default (*)         :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
  41         default fromInteger :: (Trans t repr, Num n) => t repr Integer -> t repr n
  42
  43         abs         = trans_map1 abs
  44         negate      = trans_map1 negate
  45         signum      = trans_map1 signum
  46         (+)         = trans_map2 (+)
  47         (-)         = trans_map2 (-)
  48         (*)         = trans_map2 (*)
  49         fromInteger = trans_map1 fromInteger
  50
  51 infixl 6 +
  52 infixl 6 -
  53 infixl 7 *
  54
  55 instance Sym_Num Repr_Host where
  56         abs         = liftM Prelude.abs
  57         negate      = liftM Prelude.negate
  58         signum      = liftM Prelude.signum
  59         (+)         = liftM2 (Prelude.+)
  60         (-)         = liftM2 (Prelude.-)
  61         (*)         = liftM2 (Prelude.*)
  62         fromInteger = liftM Prelude.fromInteger
  63 instance Sym_Num Repr_Text where
  64         abs         = repr_text_app1 "abs"
  65         negate      = repr_text_app1 "negate"
  66         signum      = repr_text_app1 "signum"
  67         (+)         = repr_text_infix "+" (Precedence 6)
  68         (-)         = repr_text_infix "-" (Precedence 6)
  69         (*)         = repr_text_infix "-" (Precedence 7)
  70         fromInteger = repr_text_app1 "fromInteger"
  71 instance (Sym_Num r1, Sym_Num r2) => Sym_Num (Repr_Dup r1 r2) where
  72         abs    (x1 `Repr_Dup` x2)                    = abs x1    `Repr_Dup` abs x2
  73         negate (x1 `Repr_Dup` x2)                    = negate x1 `Repr_Dup` negate x2
  74         signum (x1 `Repr_Dup` x2)                    = signum x1 `Repr_Dup` signum x2
  75         (+)    (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) = (+) x1 y1 `Repr_Dup` (+) x2 y2
  76         (-)    (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) = (-) x1 y1 `Repr_Dup` (-) x2 y2
  77         (*)    (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) = (*) x1 y1 `Repr_Dup` (*) x2 y2
  78         fromInteger (x1 `Repr_Dup` x2) = fromInteger x1 `Repr_Dup` fromInteger x2
  79
  80 -- * Type 'Expr_Num'
  81 -- | Expression.
  82 data Expr_Num (root:: *)
  83 type instance Root_of_Expr      (Expr_Num root)      = root
  84 type instance Type_of_Expr      (Expr_Num root)      = No_Type
  85 type instance Sym_of_Expr       (Expr_Num root) repr = Sym_Num repr
  86 type instance Error_of_Expr ast (Expr_Num root)      = No_Error_Expr
  87
  88 -- | Parse 'fst'.
  89 fromInteger_from
  90  :: forall root ty ast hs ret.
  91  ( ty ~ Type_Root_of_Expr (Expr_Num root)
  92  , Type0_Eq ty
  93  , Expr_From ast root
  94  , Type0_Lift   Type_Integer (Type_of_Expr root)
  95  , Type0_Unlift Type_Integer (Type_of_Expr root)
  96  , Type0_Constraint Num ty
  97  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  98                    (Error_of_Expr ast root)
  99  , Root_of_Expr root ~ root
 100  ) => ast
 101  -> ExprFrom ast (Expr_Num root) hs ret
 102 fromInteger_from ast_i ex ast ctx k =
 103  -- fromInteger :: Num a => Integer -> a
 104         expr_from (Proxy::Proxy root) ast_i ctx $
 105          \(ty_i::ty h_i) (Forall_Repr_with_Context i) ->
 106         check_type0_eq ex ast type_integer ty_i $ \Refl ->
 107         k ty_i $ Forall_Repr_with_Context $
 108          \c -> fromInteger (i c)