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.Monoid
  12 import Data.Proxy (Proxy(..))
  13 import Data.Type.Equality ((:~:)(Refl))
  14 import Prelude hiding (quot, rem, div, mod, quotRem, divMod, toInteger)
  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 infixl 7 `quot`
  51 infixl 7 `rem`
  52 infixl 7 `div`
  53 infixl 7 `mod`
  54 instance Sym_Integral Repr_Host where
  55         quot      = liftM2 Prelude.quot
  56         rem       = liftM2 Prelude.rem
  57         div       = liftM2 Prelude.div
  58         mod       = liftM2 Prelude.mod
  59         quotRem   = liftM2 Prelude.quotRem
  60         divMod    = liftM2 Prelude.divMod
  61         toInteger = liftM  Prelude.toInteger
  62 instance Sym_Integral Repr_Text where
  63         quot (Repr_Text x) (Repr_Text y) =
  64                 Repr_Text $ \p v ->
  65                         let p' = precedence_Integral in
  66                         paren p p' $ x p' v <> " `quot` " <> y p' v
  67         rem (Repr_Text x) (Repr_Text y) =
  68                 Repr_Text $ \p v ->
  69                         let p' = precedence_Integral in
  70                         paren p p' $ x p' v <> " `rem` " <> y p' v
  71         div (Repr_Text x) (Repr_Text y) =
  72                 Repr_Text $ \p v ->
  73                         let p' = precedence_Integral in
  74                         paren p p' $ x p' v <> " `div` " <> y p' v
  75         mod (Repr_Text x) (Repr_Text y) =
  76                 Repr_Text $ \p v ->
  77                         let p' = precedence_Integral in
  78                         paren p p' $ x p' v <> " `mod` " <> y p' v
  79         quotRem   = repr_text_app2 "quotRem"
  80         divMod    = repr_text_app2 "divMod"
  81         toInteger = repr_text_app1 "toInteger"
  82 instance
  83  ( Sym_Integral r1
  84  , Sym_Integral r2
  85  ) => Sym_Integral (Dup r1 r2) where
  86         quot      (x1 `Dup` x2) (y1 `Dup` y2) = quot      x1 y1 `Dup` quot      x2 y2
  87         div       (x1 `Dup` x2) (y1 `Dup` y2) = div       x1 y1 `Dup` div       x2 y2
  88         rem       (x1 `Dup` x2) (y1 `Dup` y2) = rem       x1 y1 `Dup` rem       x2 y2
  89         mod       (x1 `Dup` x2) (y1 `Dup` y2) = mod       x1 y1 `Dup` mod       x2 y2
  90         quotRem   (x1 `Dup` x2) (y1 `Dup` y2) = quotRem   x1 y1 `Dup` quotRem   x2 y2
  91         divMod    (x1 `Dup` x2) (y1 `Dup` y2) = divMod    x1 y1 `Dup` divMod    x2 y2
  92         toInteger (x1 `Dup` x2)               = toInteger x1    `Dup` toInteger x2
  93
  94 -- * Type 'Expr_Integral'
  95 -- | Expression.
  96 data Expr_Integral (root:: *)
  97 type instance Root_of_Expr      (Expr_Integral root)      = root
  98 type instance Type_of_Expr      (Expr_Integral root)      = No_Type
  99 type instance Sym_of_Expr       (Expr_Integral root) repr = Sym_Integral repr
 100 type instance Error_of_Expr ast (Expr_Integral root)      = No_Error_Expr
 101
 102 -- | Parse 'quotRem'.
 103 quotRem_from
 104  :: forall root ty ast hs ret.
 105  ( ty ~ Type_Root_of_Expr (Expr_Integral root)
 106  , Eq_Type ty
 107  , Expr_from ast root
 108  , Lift_Type Type_Tuple2 (Type_of_Expr root)
 109  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 110                    (Error_of_Expr ast root)
 111  , Root_of_Expr root ~ root
 112  , Constraint_Type Integral ty
 113  ) => ast -> ast
 114  -> Expr_From ast (Expr_Integral root) hs ret
 115 quotRem_from ast_x ast_y ex ast ctx k =
 116  -- quotRem :: a -> a -> (a, a)
 117         expr_from (Proxy::Proxy root) ast_x ctx $
 118          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 119         expr_from (Proxy::Proxy root) ast_y ctx $
 120          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
 121         check_eq_type ex ast ty_x ty_y $ \Refl ->
 122         check_constraint_type ex (Proxy::Proxy Integral) ast ty_x $ \Dict ->
 123         k (type_tuple2 ty_x ty_x) $ Forall_Repr_with_Context $
 124          \c -> quotRem (x c) (y c)
 125
 126 -- | Parse 'divMod'.
 127 divMod_from
 128  :: forall root ty ast hs ret.
 129  ( ty ~ Type_Root_of_Expr (Expr_Integral root)
 130  , Eq_Type ty
 131  , Expr_from ast root
 132  , Lift_Type Type_Tuple2 (Type_of_Expr root)
 133  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 134                    (Error_of_Expr ast root)
 135  , Root_of_Expr root ~ root
 136  , Constraint_Type Integral ty
 137  ) => ast -> ast
 138  -> Expr_From ast (Expr_Integral root) hs ret
 139 divMod_from ast_x ast_y ex ast ctx k =
 140  -- divMod :: a -> a -> (a, a)
 141         expr_from (Proxy::Proxy root) ast_x ctx $
 142          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 143         expr_from (Proxy::Proxy root) ast_y ctx $
 144          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
 145         check_eq_type ex ast ty_x ty_y $ \Refl ->
 146         check_constraint_type ex (Proxy::Proxy Integral) ast ty_x $ \Dict ->
 147         k (type_tuple2 ty_x ty_x) $ Forall_Repr_with_Context $
 148          \c -> divMod (x c) (y c)