Language/Symantic/Expr/Integral.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE OverloadedStrings #-}
   4 {-# LANGUAGE ScopedTypeVariables #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# LANGUAGE TypeOperators #-}
   7 -- | Expression for 'Integral'.
   8 module Language.Symantic.Expr.Integral where
   9
  10 import Control.Monad
  11 import Data.Proxy (Proxy(..))
  12 import Data.Type.Equality ((:~:)(Refl))
  13 import Prelude hiding (Integral(..))
  14 import Prelude (Integral)
  15 import qualified Prelude
  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_Integral'
  25 -- | Symantic.
  26 class Sym_Integral repr where
  27         quot      :: Integral i => repr i -> repr i -> repr i
  28         rem       :: Integral i => repr i -> repr i -> repr i
  29         div       :: Integral i => repr i -> repr i -> repr i
  30         mod       :: Integral i => repr i -> repr i -> repr i
  31         quotRem   :: Integral i => repr i -> repr i -> repr (i, i)
  32         divMod    :: Integral i => repr i -> repr i -> repr (i, i)
  33         toInteger :: Integral i => repr i -> repr Integer
  34
  35         default quot      :: (Trans t repr, Integral i) => t repr i -> t repr i -> t repr i
  36         default rem       :: (Trans t repr, Integral i) => t repr i -> t repr i -> t repr i
  37         default div       :: (Trans t repr, Integral i) => t repr i -> t repr i -> t repr i
  38         default mod       :: (Trans t repr, Integral i) => t repr i -> t repr i -> t repr i
  39         default quotRem   :: (Trans t repr, Integral i) => t repr i -> t repr i -> t repr (i, i)
  40         default divMod    :: (Trans t repr, Integral i) => t repr i -> t repr i -> t repr (i, i)
  41         default toInteger :: (Trans t repr, Integral i) => t repr i -> t repr Integer
  42
  43         quot      = trans_map2 quot
  44         rem       = trans_map2 rem
  45         div       = trans_map2 div
  46         mod       = trans_map2 mod
  47         quotRem   = trans_map2 quotRem
  48         divMod    = trans_map2 divMod
  49         toInteger = trans_map1 toInteger
  50
  51 infixl 7 `quot`
  52 infixl 7 `rem`
  53 infixl 7 `div`
  54 infixl 7 `mod`
  55
  56 instance Sym_Integral Repr_Host where
  57         quot      = liftM2 Prelude.quot
  58         rem       = liftM2 Prelude.rem
  59         div       = liftM2 Prelude.div
  60         mod       = liftM2 Prelude.mod
  61         quotRem   = liftM2 Prelude.quotRem
  62         divMod    = liftM2 Prelude.divMod
  63         toInteger = liftM  Prelude.toInteger
  64 instance Sym_Integral Repr_Text where
  65         quot      = repr_text_infix "`quot`" (Precedence 7)
  66         div       = repr_text_infix "`div`"  (Precedence 7)
  67         rem       = repr_text_infix "`rem`"  (Precedence 7)
  68         mod       = repr_text_infix "`mod`"  (Precedence 7)
  69         quotRem   = repr_text_app2 "quotRem"
  70         divMod    = repr_text_app2 "divMod"
  71         toInteger = repr_text_app1 "toInteger"
  72 instance
  73  ( Sym_Integral r1
  74  , Sym_Integral r2
  75  ) => Sym_Integral (Dup r1 r2) where
  76         quot      (x1 `Dup` x2) (y1 `Dup` y2) = quot      x1 y1 `Dup` quot      x2 y2
  77         div       (x1 `Dup` x2) (y1 `Dup` y2) = div       x1 y1 `Dup` div       x2 y2
  78         rem       (x1 `Dup` x2) (y1 `Dup` y2) = rem       x1 y1 `Dup` rem       x2 y2
  79         mod       (x1 `Dup` x2) (y1 `Dup` y2) = mod       x1 y1 `Dup` mod       x2 y2
  80         quotRem   (x1 `Dup` x2) (y1 `Dup` y2) = quotRem   x1 y1 `Dup` quotRem   x2 y2
  81         divMod    (x1 `Dup` x2) (y1 `Dup` y2) = divMod    x1 y1 `Dup` divMod    x2 y2
  82         toInteger (x1 `Dup` x2)               = toInteger x1    `Dup` toInteger x2
  83
  84 precedence_Integral :: Precedence
  85 precedence_Integral  = Precedence 7
  86
  87 -- * Type 'Expr_Integral'
  88 -- | Expression.
  89 data Expr_Integral (root:: *)
  90 type instance Root_of_Expr      (Expr_Integral root)      = root
  91 type instance Type_of_Expr      (Expr_Integral root)      = No_Type
  92 type instance Sym_of_Expr       (Expr_Integral root) repr = Sym_Integral repr
  93 type instance Error_of_Expr ast (Expr_Integral root)      = No_Error_Expr
  94
  95 -- | Parse 'quotRem'.
  96 quotRem_from
  97  :: forall root ty ast hs ret.
  98  ( ty ~ Type_Root_of_Expr (Expr_Integral root)
  99  , Type0_Eq ty
 100  , Expr_From ast root
 101  , Type0_Lift Type_Tuple2 (Type_of_Expr root)
 102  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 103                    (Error_of_Expr ast root)
 104  , Root_of_Expr root ~ root
 105  , Type0_Constraint Integral ty
 106  ) => ast -> ast
 107  -> ExprFrom ast (Expr_Integral root) hs ret
 108 quotRem_from ast_x ast_y ex ast ctx k =
 109  -- quotRem :: a -> a -> (a, a)
 110         expr_from (Proxy::Proxy root) ast_x ctx $
 111          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 112         expr_from (Proxy::Proxy root) ast_y ctx $
 113          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
 114         check_type0_eq ex ast ty_x ty_y $ \Refl ->
 115         check_type0_constraint ex (Proxy::Proxy Integral) ast ty_x $ \Dict ->
 116         k (type_tuple2 ty_x ty_x) $ Forall_Repr_with_Context $
 117          \c -> quotRem (x c) (y c)
 118
 119 -- | Parse 'divMod'.
 120 divMod_from
 121  :: forall root ty ast hs ret.
 122  ( ty ~ Type_Root_of_Expr (Expr_Integral root)
 123  , Type0_Eq ty
 124  , Expr_From ast root
 125  , Type0_Lift Type_Tuple2 (Type_of_Expr root)
 126  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 127                    (Error_of_Expr ast root)
 128  , Root_of_Expr root ~ root
 129  , Type0_Constraint Integral ty
 130  ) => ast -> ast
 131  -> ExprFrom ast (Expr_Integral root) hs ret
 132 divMod_from ast_x ast_y ex ast ctx k =
 133  -- divMod :: a -> a -> (a, a)
 134         expr_from (Proxy::Proxy root) ast_x ctx $
 135          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 136         expr_from (Proxy::Proxy root) ast_y ctx $
 137          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
 138         check_type0_eq ex ast ty_x ty_y $ \Refl ->
 139         check_type0_constraint ex (Proxy::Proxy Integral) ast ty_x $ \Dict ->
 140         k (type_tuple2 ty_x ty_x) $ Forall_Repr_with_Context $
 141          \c -> divMod (x c) (y c)