Language/Symantic/Compiling/Integral.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fno-warn-orphans #-}
  13 {-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
  14 -- | Symantic for 'Integral'.
  15 module Language.Symantic.Compiling.Integral where
  16
  17 import Control.Monad (liftM, liftM2)
  18 import Data.Proxy
  19 import Data.String (IsString)
  20 import Data.Text (Text)
  21 import qualified Prelude
  22 import Prelude hiding (Integral(..))
  23 import Prelude (Integral)
  24
  25 import Language.Symantic.Typing
  26 import Language.Symantic.Compiling.Term
  27 import Language.Symantic.Compiling.Tuple2 (tyTuple2)
  28 import Language.Symantic.Interpreting
  29 import Language.Symantic.Transforming.Trans
  30
  31 -- * Class 'Sym_Integral'
  32 class Sym_Integral term where
  33         quot      :: Integral i => term i -> term i -> term i
  34         rem       :: Integral i => term i -> term i -> term i
  35         div       :: Integral i => term i -> term i -> term i
  36         mod       :: Integral i => term i -> term i -> term i
  37         quotRem   :: Integral i => term i -> term i -> term (i, i)
  38         divMod    :: Integral i => term i -> term i -> term (i, i)
  39         toInteger :: Integral i => term i -> term Integer
  40
  41         default quot      :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  42         default rem       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  43         default div       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  44         default mod       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  45         default quotRem   :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i)
  46         default divMod    :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i)
  47         default toInteger :: (Trans t term, Integral i) => t term i -> t term Integer
  48
  49         quot      = trans_map2 quot
  50         rem       = trans_map2 rem
  51         div       = trans_map2 div
  52         mod       = trans_map2 mod
  53         quotRem   = trans_map2 quotRem
  54         divMod    = trans_map2 divMod
  55         toInteger = trans_map1 toInteger
  56
  57 infixl 7 `quot`
  58 infixl 7 `rem`
  59 infixl 7 `div`
  60 infixl 7 `mod`
  61
  62 type instance Sym_of_Iface (Proxy Integral) = Sym_Integral
  63 type instance Consts_of_Iface (Proxy Integral) = Proxy Integral ': Consts_imported_by Integral
  64 type instance Consts_imported_by Integral =
  65  '[ Proxy (,)
  66  ]
  67
  68 instance Sym_Integral HostI where
  69         quot      = liftM2 Prelude.quot
  70         rem       = liftM2 Prelude.rem
  71         div       = liftM2 Prelude.div
  72         mod       = liftM2 Prelude.mod
  73         quotRem   = liftM2 Prelude.quotRem
  74         divMod    = liftM2 Prelude.divMod
  75         toInteger = liftM  Prelude.toInteger
  76 instance Sym_Integral TextI where
  77         quot      = textI_infix "`quot`" (Precedence 7)
  78         div       = textI_infix "`div`"  (Precedence 7)
  79         rem       = textI_infix "`rem`"  (Precedence 7)
  80         mod       = textI_infix "`mod`"  (Precedence 7)
  81         quotRem   = textI_app2 "quotRem"
  82         divMod    = textI_app2 "divMod"
  83         toInteger = textI_app1 "toInteger"
  84 instance (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (DupI r1 r2) where
  85         quot      = dupI2 sym_Integral quot
  86         rem       = dupI2 sym_Integral rem
  87         div       = dupI2 sym_Integral div
  88         mod       = dupI2 sym_Integral mod
  89         quotRem   = dupI2 sym_Integral quotRem
  90         divMod    = dupI2 sym_Integral divMod
  91         toInteger = dupI1 sym_Integral toInteger
  92
  93 instance Const_from Text cs => Const_from Text (Proxy Integral ': cs) where
  94         const_from "Integral" k = k (ConstZ kind)
  95         const_from s k = const_from s $ k . ConstS
  96 instance Show_Const cs => Show_Const (Proxy Integral ': cs) where
  97         show_const ConstZ{} = "Integral"
  98         show_const (ConstS c) = show_const c
  99
 100 instance -- Proj_ConC
 101  Proj_ConC cs (Proxy Integral)
 102 instance -- Term_fromI
 103  ( AST ast
 104  , Lexem ast ~ LamVarName
 105  , Inj_Const (Consts_of_Ifaces is) Integral
 106  , Inj_Const (Consts_of_Ifaces is) (->)
 107  , Inj_Const (Consts_of_Ifaces is) (,)
 108  , Proj_Con  (Consts_of_Ifaces is)
 109  , Term_from is ast
 110  ) => Term_fromI is (Proxy Integral) ast where
 111         term_fromI ast ctx k =
 112                 case ast_lexem ast of
 113                  "quot"    -> integral_op2_from quot
 114                  "rem"     -> integral_op2_from rem
 115                  "div"     -> integral_op2_from div
 116                  "mod"     -> integral_op2_from mod
 117                  "quotRem" -> integral_op2t2_from quotRem
 118                  "divMod"  -> integral_op2t2_from divMod
 119                  _ -> Left $ Error_Term_unsupported
 120                 where
 121                 integral_op2_from
 122                  (op::forall term a. (Sym_Integral term, Integral a)
 123                          => term a -> term a -> term a) =
 124                  -- quot :: Integral i => i -> i -> i
 125                  -- rem  :: Integral i => i -> i -> i
 126                  -- div  :: Integral i => i -> i -> i
 127                  -- mod  :: Integral i => i -> i -> i
 128                         from_ast1 ast $ \ast_a as ->
 129                         term_from ast_a ctx $ \ty_a (TermLC x) ->
 130                         check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
 131                         k as (ty_a ~> ty_a) $ TermLC $
 132                          \c -> lam $ \y -> op (x c) y
 133                 integral_op2t2_from
 134                  (op::forall term a. (Sym_Integral term, Integral a)
 135                          => term a -> term a -> term (a, a)) =
 136                  -- quotRem :: Integral i => i -> i -> (i, i)
 137                  -- divMod  :: Integral i => i -> i -> (i, i)
 138                         from_ast1 ast $ \ast_a as ->
 139                         term_from ast_a ctx $ \ty_a (TermLC x) ->
 140                         check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
 141                         k as (ty_a ~> (tyTuple2 :$ ty_a) :$ ty_a) $ TermLC $
 142                          \c -> lam $ \y -> op (x c) y
 143
 144 -- | The 'Integral' 'Type'
 145 tyIntegral :: Inj_Const cs Integral => Type cs Integral
 146 tyIntegral = TyConst inj_const
 147
 148 sym_Integral :: Proxy Sym_Integral
 149 sym_Integral = Proxy
 150
 151 syIntegral :: IsString a => [Syntax a] -> Syntax a
 152 syIntegral = Syntax "Integral"