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                         case ast_nodes ast of
 128                          [] -> Left $ Error_Term_Syntax $
 129                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 130                          [ast_a] ->
 131                                 term_from ast_a ctx $ \ty_a (TermLC x) ->
 132                                 check_constraint (At (Just ast_a) (tyNum :$ ty_a)) $ \Con ->
 133                                 k ty_a $ TermLC $
 134                                  \c -> op (x c)
 135                          _ -> Left $ Error_Term_Syntax $
 136                                 Error_Syntax_too_many_arguments $ At (Just ast) 1
 137                 num_op2_from
 138                  (op::forall term a. (Sym_Num term, Num a)
 139                          => term a -> term a -> term a) =
 140                  -- (+) :: Num a => a -> a -> a
 141                  -- (-) :: Num a => a -> a -> a
 142                  -- (*) :: Num a => a -> a -> a
 143                         case ast_nodes ast of
 144                          [] -> Left $ Error_Term_Syntax $
 145                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 146                          [ast_a] ->
 147                                 term_from ast_a ctx $ \ty_a (TermLC x) ->
 148                                 check_constraint (At (Just ast_a) (tyNum :$ ty_a)) $ \Con ->
 149                                 k (ty_a ~> ty_a) $ TermLC $
 150                                  \c -> lam $ \y -> op (x c) y
 151                          [ast_a, ast_y] ->
 152                                 term_from ast_a ctx $ \ty_a (TermLC x) ->
 153                                 term_from ast_y ctx $ \ty_y (TermLC y) ->
 154                                 check_type (At (Just ast_a) ty_a) (At (Just ast_y) ty_y) $ \Refl ->
 155                                 check_constraint (At (Just ast_a) (tyNum :$ ty_a)) $ \Con ->
 156                                 k ty_a $ TermLC $
 157                                  \c -> op (x c) (y c)
 158                          _ -> Left $ Error_Term_Syntax $
 159                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 160                 fromInteger_from =
 161                  -- fromInteger :: Num a => Integer -> a
 162                         case ast_nodes ast of
 163                          [] -> Left $ Error_Term_Syntax $
 164                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 165                          [ast_ty_a] ->
 166                                 either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 167                                 type_from ast_ty_a $ \ty_a -> Right $
 168                                 check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
 169                                 check_constraint (At (Just ast_ty_a) (tyNum :$ ty_a)) $ \Con ->
 170                                 k (tyInteger ~> ty_a) $ TermLC $
 171                                 Fun.const $ lam fromInteger
 172                          [ast_ty_a, ast_i] ->
 173                                 either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 174                                 type_from ast_ty_a $ \ty_a -> Right $
 175                                 term_from ast_i ctx $ \ty_i (TermLC i) ->
 176                                 check_type (At Nothing tyInteger) (At (Just ast_i) ty_i) $ \Refl ->
 177                                 check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
 178                                 check_constraint (At (Just ast_ty_a) (tyNum :$ ty_a)) $ \Con ->
 179                                 k ty_a $ TermLC $
 180                                 fromInteger . i
 181                          _ -> Left $ Error_Term_Syntax $
 182                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 183
 184 -- | The 'Num' 'Type'
 185 tyNum :: Inj_Const cs Num => Type cs Num
 186 tyNum = TyConst inj_const
 187
 188 sym_Num :: Proxy Sym_Num
 189 sym_Num = Proxy
 190
 191 syNum :: IsString a => [Syntax a] -> Syntax a
 192 syNum = Syntax "Num"