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         = repr_dup1 sym_Num abs
  73         negate      = repr_dup1 sym_Num negate
  74         signum      = repr_dup1 sym_Num signum
  75         (+)         = repr_dup2 sym_Num (+)
  76         (-)         = repr_dup2 sym_Num (-)
  77         (*)         = repr_dup2 sym_Num (*)
  78         fromInteger = repr_dup1 sym_Num fromInteger
  79
  80 sym_Num :: Proxy Sym_Num
  81 sym_Num = Proxy
  82
  83 -- * Type 'Expr_Num'
  84 -- | Expression.
  85 data Expr_Num (root:: *)
  86 type instance Root_of_Expr      (Expr_Num root)      = root
  87 type instance Type_of_Expr      (Expr_Num root)      = No_Type
  88 type instance Sym_of_Expr       (Expr_Num root) repr = Sym_Num repr
  89 type instance Error_of_Expr ast (Expr_Num root)      = No_Error_Expr
  90
  91 -- | Parse 'fst'.
  92 fromInteger_from
  93  :: forall root ty ast hs ret.
  94  ( ty ~ Type_Root_of_Expr (Expr_Num root)
  95  , Type0_Eq ty
  96  , Expr_From ast root
  97  , Type0_Lift   Type_Integer (Type_of_Expr root)
  98  , Type0_Unlift Type_Integer (Type_of_Expr root)
  99  , Type0_Constraint Num ty
 100  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 101                    (Error_of_Expr ast root)
 102  , Root_of_Expr root ~ root
 103  ) => ast
 104  -> ExprFrom ast (Expr_Num root) hs ret
 105 fromInteger_from ast_i ex ast ctx k =
 106  -- fromInteger :: Num a => Integer -> a
 107         expr_from (Proxy::Proxy root) ast_i ctx $
 108          \(ty_i::ty h_i) (Forall_Repr_with_Context i) ->
 109         check_type0_eq ex ast type_integer ty_i $ \Refl ->
 110         k ty_i $ Forall_Repr_with_Context $
 111          \c -> fromInteger (i c)