Language/Symantic/Compiling/Num.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 -- | Symantic for 'Num'.
  14 module Language.Symantic.Compiling.Num where
  15
  16 import Control.Monad (liftM, liftM2)
  17 import qualified Data.Function as Fun
  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 (Num(..))
  24 import Prelude (Num)
  25
  26 import Language.Symantic.Typing
  27 import Language.Symantic.Compiling.Term
  28 import Language.Symantic.Compiling.Integer (tyInteger)
  29 import Language.Symantic.Interpreting
  30 import Language.Symantic.Transforming.Trans
  31
  32 -- * Class 'Sym_Num'
  33 class Sym_Num term where
  34         abs         :: Num n => term n -> term n
  35         negate      :: Num n => term n -> term n
  36         signum      :: Num n => term n -> term n
  37         (+)         :: Num n => term n -> term n -> term n
  38         (-)         :: Num n => term n -> term n -> term n
  39         (*)         :: Num n => term n -> term n -> term n
  40         fromInteger :: Num n => term Integer -> term n
  41
  42         default abs         :: (Trans t term, Num n) => t term n -> t term n
  43         default negate      :: (Trans t term, Num n) => t term n -> t term n
  44         default signum      :: (Trans t term, Num n) => t term n -> t term n
  45         default (+)         :: (Trans t term, Num n) => t term n -> t term n -> t term n
  46         default (-)         :: (Trans t term, Num n) => t term n -> t term n -> t term n
  47         default (*)         :: (Trans t term, Num n) => t term n -> t term n -> t term n
  48         default fromInteger :: (Trans t term, Num n) => t term Integer -> t term n
  49
  50         abs         = trans_map1 abs
  51         negate      = trans_map1 negate
  52         signum      = trans_map1 signum
  53         (+)         = trans_map2 (+)
  54         (-)         = trans_map2 (-)
  55         (*)         = trans_map2 (*)
  56         fromInteger = trans_map1 fromInteger
  57
  58 infixl 6 +
  59 infixl 6 -
  60 infixl 7 *
  61
  62 type instance Sym_of_Iface (Proxy Num) = Sym_Num
  63 type instance Consts_of_Iface (Proxy Num) = Proxy Num ': Consts_imported_by Num
  64 type instance Consts_imported_by Num = '[]
  65
  66 instance Sym_Num HostI where
  67         abs         = liftM Prelude.abs
  68         negate      = liftM Prelude.negate
  69         signum      = liftM Prelude.signum
  70         (+)         = liftM2 (Prelude.+)
  71         (-)         = liftM2 (Prelude.-)
  72         (*)         = liftM2 (Prelude.*)
  73         fromInteger = liftM Prelude.fromInteger
  74 instance Sym_Num TextI where
  75         abs         = textI_app1 "abs"
  76         negate      = textI_app1 "negate"
  77         signum      = textI_app1 "signum"
  78         (+)         = textI_infix "+" (Precedence 6)
  79         (-)         = textI_infix "-" (Precedence 6)
  80         (*)         = textI_infix "-" (Precedence 7)
  81         fromInteger = textI_app1 "fromInteger"
  82 instance (Sym_Num r1, Sym_Num r2) => Sym_Num (DupI r1 r2) where
  83         abs         = dupI1 sym_Num abs
  84         negate      = dupI1 sym_Num negate
  85         signum      = dupI1 sym_Num signum
  86         (+)         = dupI2 sym_Num (+)
  87         (-)         = dupI2 sym_Num (-)
  88         (*)         = dupI2 sym_Num (*)
  89         fromInteger = dupI1 sym_Num fromInteger
  90
  91 instance Const_from Text cs => Const_from Text (Proxy Num ': cs) where
  92         const_from "Num" k = k (ConstZ kind)
  93         const_from s k = const_from s $ k . ConstS
  94 instance Show_Const cs => Show_Const (Proxy Num ': cs) where
  95         show_const ConstZ{} = "Num"
  96         show_const (ConstS c) = show_const c
  97
  98 instance -- Proj_ConC
  99  Proj_ConC cs (Proxy Num)
 100 instance -- Term_fromI
 101  ( AST ast
 102  , Lexem ast ~ LamVarName
 103  , Const_from (Lexem ast) (Consts_of_Ifaces is)
 104  , Inj_Const (Consts_of_Ifaces is) Num
 105  , Inj_Const (Consts_of_Ifaces is) (->)
 106  , Inj_Const (Consts_of_Ifaces is) Integer
 107  , Proj_Con  (Consts_of_Ifaces is)
 108  , Term_from is ast
 109  ) => Term_fromI is (Proxy Num) ast where
 110         term_fromI ast ctx k =
 111                 case ast_lexem ast of
 112                  "abs"         -> num_op1_from abs
 113                  "negate"      -> num_op1_from negate
 114                  "signum"      -> num_op1_from signum
 115                  "+"           -> num_op2_from (+)
 116                  "-"           -> num_op2_from (-)
 117                  "*"           -> num_op2_from (*)
 118                  "fromInteger" -> fromInteger_from
 119                  _ -> Left $ Error_Term_unsupported
 120                 where
 121                 num_op1_from
 122                  (op::forall term a. (Sym_Num term, Num a)
 123                          => term a -> term a) =
 124                  -- abs    :: Num a => a -> a
 125                  -- negate :: Num a => a -> a
 126                  -- signum :: Num a => a -> a
 127                         from_ast1 ast $ \ast_a as ->
 128                         term_from ast_a ctx $ \ty_a (TermLC x) ->
 129                         check_constraint (At (Just ast_a) (tyNum :$ ty_a)) $ \Con ->
 130                         k as ty_a $ TermLC $
 131                          \c -> op (x c)
 132                 num_op2_from
 133                  (op::forall term a. (Sym_Num term, Num a)
 134                          => term a -> term a -> term a) =
 135                  -- (+) :: Num a => a -> a -> a
 136                  -- (-) :: Num a => a -> a -> a
 137                  -- (*) :: Num a => a -> a -> a
 138                         from_ast1 ast $ \ast_a as ->
 139                         term_from ast_a ctx $ \ty_a (TermLC x) ->
 140                         check_constraint (At (Just ast_a) (tyNum :$ ty_a)) $ \Con ->
 141                         k as (ty_a ~> ty_a) $ TermLC $
 142                          \c -> lam $ \y -> op (x c) y
 143                 fromInteger_from =
 144                  -- fromInteger :: Num a => Integer -> a
 145                         from_ast1 ast $ \ast_ty_a as ->
 146                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 147                         type_from ast_ty_a $ \ty_a -> Right $
 148                         check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
 149                         check_constraint (At (Just ast_ty_a) (tyNum :$ ty_a)) $ \Con ->
 150                         k as (tyInteger ~> ty_a) $ TermLC $
 151                         Fun.const $ lam fromInteger
 152
 153 -- | The 'Num' 'Type'
 154 tyNum :: Inj_Const cs Num => Type cs Num
 155 tyNum = TyConst inj_const
 156
 157 sym_Num :: Proxy Sym_Num
 158 sym_Num = Proxy
 159
 160 syNum :: IsString a => [Syntax a] -> Syntax a
 161 syNum = Syntax "Num"