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 Data.Type.Equality ((:~:)(Refl))
  22 import qualified Prelude
  23 import Prelude hiding (Integral(..))
  24 import Prelude (Integral)
  25
  26 import Language.Symantic.Typing
  27 import Language.Symantic.Compiling.Term
  28 import Language.Symantic.Compiling.Tuple2 (tyTuple2)
  29 import Language.Symantic.Interpreting
  30 import Language.Symantic.Transforming.Trans
  31
  32 -- * Class 'Sym_Integral'
  33 class Sym_Integral term where
  34         quot      :: Integral i => term i -> term i -> term i
  35         rem       :: Integral i => term i -> term i -> term i
  36         div       :: Integral i => term i -> term i -> term i
  37         mod       :: Integral i => term i -> term i -> term i
  38         quotRem   :: Integral i => term i -> term i -> term (i, i)
  39         divMod    :: Integral i => term i -> term i -> term (i, i)
  40         toInteger :: Integral i => term i -> term Integer
  41
  42         default quot      :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  43         default rem       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  44         default div       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  45         default mod       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  46         default quotRem   :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i)
  47         default divMod    :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i)
  48         default toInteger :: (Trans t term, Integral i) => t term i -> t term Integer
  49
  50         quot      = trans_map2 quot
  51         rem       = trans_map2 rem
  52         div       = trans_map2 div
  53         mod       = trans_map2 mod
  54         quotRem   = trans_map2 quotRem
  55         divMod    = trans_map2 divMod
  56         toInteger = trans_map1 toInteger
  57
  58 infixl 7 `quot`
  59 infixl 7 `rem`
  60 infixl 7 `div`
  61 infixl 7 `mod`
  62
  63 type instance Sym_of_Iface (Proxy Integral) = Sym_Integral
  64 type instance Consts_of_Iface (Proxy Integral) = Proxy Integral ': Consts_imported_by Integral
  65 type instance Consts_imported_by Integral =
  66  '[ Proxy (,)
  67  ]
  68
  69 instance Sym_Integral HostI where
  70         quot      = liftM2 Prelude.quot
  71         rem       = liftM2 Prelude.rem
  72         div       = liftM2 Prelude.div
  73         mod       = liftM2 Prelude.mod
  74         quotRem   = liftM2 Prelude.quotRem
  75         divMod    = liftM2 Prelude.divMod
  76         toInteger = liftM  Prelude.toInteger
  77 instance Sym_Integral TextI where
  78         quot      = textI_infix "`quot`" (Precedence 7)
  79         div       = textI_infix "`div`"  (Precedence 7)
  80         rem       = textI_infix "`rem`"  (Precedence 7)
  81         mod       = textI_infix "`mod`"  (Precedence 7)
  82         quotRem   = textI_app2 "quotRem"
  83         divMod    = textI_app2 "divMod"
  84         toInteger = textI_app1 "toInteger"
  85 instance (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (DupI r1 r2) where
  86         quot      = dupI2 sym_Integral quot
  87         rem       = dupI2 sym_Integral rem
  88         div       = dupI2 sym_Integral div
  89         mod       = dupI2 sym_Integral mod
  90         quotRem   = dupI2 sym_Integral quotRem
  91         divMod    = dupI2 sym_Integral divMod
  92         toInteger = dupI1 sym_Integral toInteger
  93
  94 instance Const_from Text cs => Const_from Text (Proxy Integral ': cs) where
  95         const_from "Integral" k = k (ConstZ kind)
  96         const_from s k = const_from s $ k . ConstS
  97 instance Show_Const cs => Show_Const (Proxy Integral ': cs) where
  98         show_const ConstZ{} = "Integral"
  99         show_const (ConstS c) = show_const c
 100
 101 instance -- Proj_ConC
 102  Proj_ConC cs (Proxy Integral)
 103 instance -- Term_fromI
 104  ( AST ast
 105  , Lexem ast ~ LamVarName
 106  , Inj_Const (Consts_of_Ifaces is) Integral
 107  , Inj_Const (Consts_of_Ifaces is) (->)
 108  , Inj_Const (Consts_of_Ifaces is) (,)
 109  , Proj_Con  (Consts_of_Ifaces is)
 110  , Term_from is ast
 111  ) => Term_fromI is (Proxy Integral) ast where
 112         term_fromI ast ctx k =
 113                 case ast_lexem ast of
 114                  "quot"    -> integral_op2_from quot
 115                  "rem"     -> integral_op2_from rem
 116                  "div"     -> integral_op2_from div
 117                  "mod"     -> integral_op2_from mod
 118                  "quotRem" -> integral_op2t2_from quotRem
 119                  "divMod"  -> integral_op2t2_from divMod
 120                  _ -> Left $ Error_Term_unsupported
 121                 where
 122                 integral_op2_from
 123                  (op::forall term a. (Sym_Integral term, Integral a)
 124                          => term a -> term a -> term a) =
 125                  -- quot :: Integral i => i -> i -> i
 126                  -- rem  :: Integral i => i -> i -> i
 127                  -- div  :: Integral i => i -> i -> i
 128                  -- mod  :: Integral i => i -> i -> i
 129                         case ast_nodes ast of
 130                          [] -> Left $ Error_Term_Syntax $
 131                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 132                          [ast_a] ->
 133                                 term_from ast_a ctx $ \ty_a (TermLC x) ->
 134                                 check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
 135                                 k (ty_a ~> ty_a) $ TermLC $
 136                                  \c -> lam $ \y -> op (x c) y
 137                          [ast_a, ast_y] ->
 138                                 term_from ast_a ctx $ \ty_a (TermLC x) ->
 139                                 term_from ast_y ctx $ \ty_y (TermLC y) ->
 140                                 check_type (At (Just ast_a) ty_a) (At (Just ast_y) ty_y) $ \Refl ->
 141                                 check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
 142                                 k ty_a $ TermLC $
 143                                  \c -> op (x c) (y c)
 144                          _ -> Left $ Error_Term_Syntax $
 145                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 146                 integral_op2t2_from
 147                  (op::forall term a. (Sym_Integral term, Integral a)
 148                          => term a -> term a -> term (a, a)) =
 149                  -- quotRem :: Integral i => i -> i -> (i, i)
 150                  -- divMod  :: Integral i => i -> i -> (i, i)
 151                         case ast_nodes ast of
 152                          [] -> Left $ Error_Term_Syntax $
 153                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 154                          [ast_a] ->
 155                                 term_from ast_a ctx $ \ty_a (TermLC x) ->
 156                                 check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
 157                                 k (ty_a ~> (tyTuple2 :$ ty_a) :$ ty_a) $ TermLC $
 158                                  \c -> lam $ \y -> op (x c) y
 159                          [ast_a, ast_y] ->
 160                                 term_from ast_a ctx $ \ty_a (TermLC x) ->
 161                                 term_from ast_y ctx $ \ty_y (TermLC y) ->
 162                                 check_type (At (Just ast_a) ty_a) (At (Just ast_y) ty_y) $ \Refl ->
 163                                 check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
 164                                 k ((tyTuple2 :$ ty_a) :$ ty_a) $ TermLC $
 165                                  \c -> op (x c) (y c)
 166                          _ -> Left $ Error_Term_Syntax $
 167                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 168
 169 -- | The 'Integral' 'Type'
 170 tyIntegral :: Inj_Const cs Integral => Type cs Integral
 171 tyIntegral = TyConst inj_const
 172
 173 sym_Integral :: Proxy Sym_Integral
 174 sym_Integral = Proxy
 175
 176 syIntegral :: IsString a => [Syntax a] -> Syntax a
 177 syIntegral = Syntax "Integral"