Language/Symantic/Compiling/Integer.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=5 #-}
  14 -- | Symantic for 'Integer'.
  15 module Language.Symantic.Compiling.Integer where
  16
  17 import qualified Data.Function as Fun
  18 import Data.Proxy
  19 import Data.String (IsString)
  20 import Data.Text (Text)
  21 import qualified Data.Text as Text
  22 import Data.Type.Equality ((:~:)(Refl))
  23
  24 import Language.Symantic.Typing
  25 import Language.Symantic.Compiling.Term
  26 import Language.Symantic.Interpreting
  27 import Language.Symantic.Transforming.Trans
  28
  29 -- * Class 'Sym_Integer'
  30 class Sym_Integer term where
  31         integer :: Integer -> term Integer
  32         default integer :: Trans t term => Integer -> t term Integer
  33         integer = trans_lift . integer
  34
  35 type instance Sym_of_Iface (Proxy Integer) = Sym_Integer
  36 type instance Consts_of_Iface (Proxy Integer) = Proxy Integer ': Consts_imported_by Integer
  37 type instance Consts_imported_by Integer =
  38  [ Proxy Enum
  39  , Proxy Eq
  40  , Proxy Integral
  41  , Proxy Num
  42  , Proxy Ord
  43  , Proxy Real
  44  ]
  45
  46 instance Sym_Integer HostI where
  47         integer = HostI
  48 instance Sym_Integer TextI where
  49         integer a = TextI $ \_p _v ->
  50                 Text.pack (show a)
  51 instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (DupI r1 r2) where
  52         integer x = integer x `DupI` integer x
  53
  54 instance Const_from Text cs => Const_from Text (Proxy Integer ': cs) where
  55         const_from "Integer" k = k (ConstZ kind)
  56         const_from s k = const_from s $ k . ConstS
  57 instance Show_Const cs => Show_Const (Proxy Integer ': cs) where
  58         show_const ConstZ{} = "Integer"
  59         show_const (ConstS c) = show_const c
  60
  61 instance -- Proj_ConC
  62  ( Proj_Const cs Integer
  63  , Proj_Consts cs (Consts_imported_by Integer)
  64  ) => Proj_ConC cs (Proxy Integer) where
  65         proj_conC _ (TyConst q :$ TyConst c)
  66          | Just Refl <- eq_skind (kind_of_const c) SKiType
  67          , Just Refl <- proj_const c (Proxy::Proxy Integer)
  68          = Just $ case () of
  69                  _ | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
  70                    | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
  71                    | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Con
  72                    | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Con
  73                    | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
  74                    | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Con
  75                  _ -> Nothing
  76         proj_conC _c _q = Nothing
  77 instance -- Term_fromI
  78  ( AST ast
  79  , Lexem ast ~ LamVarName
  80  , Inj_Const (Consts_of_Ifaces is) Integer
  81  , Show_Const (Consts_of_Ifaces is)
  82  ) => Term_fromI is (Proxy Integer) ast where
  83         term_fromI ast _ctx k =
  84                 case ast_lexem ast of
  85                  "integer" -> integer_from
  86                  _ -> Left $ Error_Term_unsupported
  87                 where
  88                 integer_from =
  89                         let ty = tyInteger in
  90                         from_lex (Text.pack $ show_type ty) ast $ \(i::Integer) ->
  91                         k ty $ TermLC $ Fun.const $ integer i
  92
  93 -- | The 'Integer' 'Type'
  94 tyInteger :: Inj_Const cs Integer => Type cs Integer
  95 tyInteger = TyConst inj_const
  96
  97 sym_Integer :: Proxy Sym_Integer
  98 sym_Integer = Proxy
  99
 100 syInteger :: IsString a => Syntax a
 101 syInteger = Syntax "Integer" []