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 (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (Repr_Dup r1 r2) where
  73         quot      = repr_dup2 sym_Integral quot
  74         rem       = repr_dup2 sym_Integral rem
  75         div       = repr_dup2 sym_Integral div
  76         mod       = repr_dup2 sym_Integral mod
  77         quotRem   = repr_dup2 sym_Integral quotRem
  78         divMod    = repr_dup2 sym_Integral divMod
  79         toInteger = repr_dup1 sym_Integral toInteger
  80
  81 sym_Integral :: Proxy Sym_Integral
  82 sym_Integral = Proxy
  83
  84 -- * Type 'Expr_Integral'
  85 -- | Expression.
  86 data Expr_Integral (root:: *)
  87 type instance Root_of_Expr      (Expr_Integral root)      = root
  88 type instance Type_of_Expr      (Expr_Integral root)      = No_Type
  89 type instance Sym_of_Expr       (Expr_Integral root) repr = Sym_Integral repr
  90 type instance Error_of_Expr ast (Expr_Integral root)      = No_Error_Expr
  91
  92 -- | Parse 'quotRem'.
  93 quotRem_from
  94  :: forall root ty ast hs ret.
  95  ( ty ~ Type_Root_of_Expr (Expr_Integral root)
  96  , Type0_Eq ty
  97  , Expr_From ast root
  98  , Type0_Lift Type_Tuple2 (Type_of_Expr root)
  99  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 100                    (Error_of_Expr ast root)
 101  , Root_of_Expr root ~ root
 102  , Type0_Constraint Integral ty
 103  ) => ast -> ast
 104  -> ExprFrom ast (Expr_Integral root) hs ret
 105 quotRem_from ast_x ast_y ex ast ctx k =
 106  -- quotRem :: a -> a -> (a, a)
 107         expr_from (Proxy::Proxy root) ast_x ctx $
 108          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 109         expr_from (Proxy::Proxy root) ast_y ctx $
 110          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
 111         check_type0_eq ex ast ty_x ty_y $ \Refl ->
 112         check_type0_constraint ex (Proxy::Proxy Integral) ast ty_x $ \Dict ->
 113         k (type_tuple2 ty_x ty_x) $ Forall_Repr_with_Context $
 114          \c -> quotRem (x c) (y c)
 115
 116 -- | Parse 'quotRem', partially applied.
 117 quotRem_from1
 118  :: forall root ty ast hs ret.
 119  ( ty ~ Type_Root_of_Expr (Expr_Integral root)
 120  , Type0_Eq ty
 121  , Expr_From ast root
 122  , Type0_Lift Type_Fun    (Type_of_Expr root)
 123  , Type0_Lift Type_Tuple2 (Type_of_Expr root)
 124  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 125                    (Error_of_Expr ast root)
 126  , Root_of_Expr root ~ root
 127  , Type0_Constraint Integral ty
 128  ) => ast
 129  -> ExprFrom ast (Expr_Integral root) hs ret
 130 quotRem_from1 ast_x ex ast ctx k =
 131  -- quotRem :: a -> a -> (a, a)
 132         expr_from (Proxy::Proxy root) ast_x ctx $
 133          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 134         check_type0_constraint ex (Proxy::Proxy Integral) ast ty_x $ \Dict ->
 135         k (type_fun ty_x $ type_tuple2 ty_x ty_x) $ Forall_Repr_with_Context $
 136          \c -> lam $ quotRem (x c)
 137
 138 -- | Parse 'divMod'.
 139 divMod_from
 140  :: forall root ty ast hs ret.
 141  ( ty ~ Type_Root_of_Expr (Expr_Integral root)
 142  , Type0_Eq ty
 143  , Expr_From ast root
 144  , Type0_Lift Type_Tuple2 (Type_of_Expr root)
 145  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 146                    (Error_of_Expr ast root)
 147  , Root_of_Expr root ~ root
 148  , Type0_Constraint Integral ty
 149  ) => ast -> ast
 150  -> ExprFrom ast (Expr_Integral root) hs ret
 151 divMod_from ast_x ast_y ex ast ctx k =
 152  -- divMod :: a -> a -> (a, a)
 153         expr_from (Proxy::Proxy root) ast_x ctx $
 154          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 155         expr_from (Proxy::Proxy root) ast_y ctx $
 156          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
 157         check_type0_eq ex ast ty_x ty_y $ \Refl ->
 158         check_type0_constraint ex (Proxy::Proxy Integral) ast ty_x $ \Dict ->
 159         k (type_tuple2 ty_x ty_x) $ Forall_Repr_with_Context $
 160          \c -> divMod (x c) (y c)
 161
 162 -- | Parse 'divMod', partially applied.
 163 divMod_from1
 164  :: forall root ty ast hs ret.
 165  ( ty ~ Type_Root_of_Expr (Expr_Integral root)
 166  , Type0_Eq ty
 167  , Expr_From ast root
 168  , Type0_Lift Type_Fun    (Type_of_Expr root)
 169  , Type0_Lift Type_Tuple2 (Type_of_Expr root)
 170  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 171                    (Error_of_Expr ast root)
 172  , Root_of_Expr root ~ root
 173  , Type0_Constraint Integral ty
 174  ) => ast
 175  -> ExprFrom ast (Expr_Integral root) hs ret
 176 divMod_from1 ast_x ex ast ctx k =
 177  -- divMod :: a -> a -> (a, a)
 178         expr_from (Proxy::Proxy root) ast_x ctx $
 179          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 180         check_type0_constraint ex (Proxy::Proxy Integral) ast ty_x $ \Dict ->
 181         k (type_fun ty_x $ type_tuple2 ty_x ty_x) $ Forall_Repr_with_Context $
 182          \c -> lam $ divMod (x c)