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  '[ Proxy Integer
  66  ]
  67
  68 instance Sym_Num HostI where
  69         abs         = liftM Prelude.abs
  70         negate      = liftM Prelude.negate
  71         signum      = liftM Prelude.signum
  72         (+)         = liftM2 (Prelude.+)
  73         (-)         = liftM2 (Prelude.-)
  74         (*)         = liftM2 (Prelude.*)
  75         fromInteger = liftM Prelude.fromInteger
  76 instance Sym_Num TextI where
  77         abs         = textI_app1 "abs"
  78         negate      = textI_app1 "negate"
  79         signum      = textI_app1 "signum"
  80         (+)         = textI_infix "+" (Precedence 6)
  81         (-)         = textI_infix "-" (Precedence 6)
  82         (*)         = textI_infix "-" (Precedence 7)
  83         fromInteger = textI_app1 "fromInteger"
  84 instance (Sym_Num r1, Sym_Num r2) => Sym_Num (DupI r1 r2) where
  85         abs         = dupI1 sym_Num abs
  86         negate      = dupI1 sym_Num negate
  87         signum      = dupI1 sym_Num signum
  88         (+)         = dupI2 sym_Num (+)
  89         (-)         = dupI2 sym_Num (-)
  90         (*)         = dupI2 sym_Num (*)
  91         fromInteger = dupI1 sym_Num fromInteger
  92
  93 instance Const_from Text cs => Const_from Text (Proxy Num ': cs) where
  94         const_from "Num" k = k (ConstZ kind)
  95         const_from s k = const_from s $ k . ConstS
  96 instance Show_Const cs => Show_Const (Proxy Num ': cs) where
  97         show_const ConstZ{} = "Num"
  98         show_const (ConstS c) = show_const c
  99
 100 instance -- Proj_ConC
 101  Proj_ConC cs (Proxy Num)
 102 instance -- Term_fromI
 103  ( AST ast
 104  , Lexem ast ~ LamVarName
 105  , Const_from (Lexem ast) (Consts_of_Ifaces is)
 106  , Inj_Const (Consts_of_Ifaces is) Num
 107  , Inj_Const (Consts_of_Ifaces is) (->)
 108  , Inj_Const (Consts_of_Ifaces is) Integer
 109  , Proj_Con  (Consts_of_Ifaces is)
 110  , Term_from is ast
 111  ) => Term_fromI is (Proxy Num) ast where
 112         term_fromI ast ctx k =
 113                 case ast_lexem ast of
 114                  "abs"         -> num_op1_from abs
 115                  "negate"      -> num_op1_from negate
 116                  "signum"      -> num_op1_from signum
 117                  "+"           -> num_op2_from (+)
 118                  "-"           -> num_op2_from (-)
 119                  "*"           -> num_op2_from (*)
 120                  "fromInteger" -> fromInteger_from
 121                  _ -> Left $ Error_Term_unsupported
 122                 where
 123                 num_op1_from
 124                  (op::forall term a. (Sym_Num term, Num a)
 125                          => term a -> term a) =
 126                  -- abs    :: Num a => a -> a
 127                  -- negate :: Num a => a -> a
 128                  -- signum :: Num a => a -> a
 129                         from_ast1 ast $ \ast_a as ->
 130                         term_from ast_a ctx $ \ty_a (TermLC x) ->
 131                         check_constraint (At (Just ast_a) (tyNum :$ ty_a)) $ \Con ->
 132                         k as ty_a $ TermLC $
 133                          \c -> op (x c)
 134                 num_op2_from
 135                  (op::forall term a. (Sym_Num term, Num a)
 136                          => term a -> term a -> term a) =
 137                  -- (+) :: Num a => a -> a -> a
 138                  -- (-) :: Num a => a -> a -> a
 139                  -- (*) :: Num a => a -> a -> a
 140                         from_ast1 ast $ \ast_a as ->
 141                         term_from ast_a ctx $ \ty_a (TermLC x) ->
 142                         check_constraint (At (Just ast_a) (tyNum :$ ty_a)) $ \Con ->
 143                         k as (ty_a ~> ty_a) $ TermLC $
 144                          \c -> lam $ \y -> op (x c) y
 145                 fromInteger_from =
 146                  -- fromInteger :: Num a => Integer -> a
 147                         from_ast1 ast $ \ast_ty_a as ->
 148                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 149                         type_from ast_ty_a $ \ty_a -> Right $
 150                         check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
 151                         check_constraint (At (Just ast_ty_a) (tyNum :$ ty_a)) $ \Con ->
 152                         k as (tyInteger ~> ty_a) $ TermLC $
 153                         Fun.const $ lam fromInteger
 154
 155 -- | The 'Num' 'Type'
 156 tyNum :: Inj_Const cs Num => Type cs Num
 157 tyNum = TyConst inj_const
 158
 159 sym_Num :: Proxy Sym_Num
 160 sym_Num = Proxy
 161
 162 syNum :: IsString a => [Syntax a] -> Syntax a
 163 syNum = Syntax "Num"