symantic-lib/Language/Symantic/Lib/Integer.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Integer'.
   4 module Language.Symantic.Lib.Integer where
   5
   6 import Data.Eq (Eq)
   7 import Data.Function (($), (.))
   8 import Data.Functor ((<$>))
   9 import Data.Maybe (Maybe(..))
  10 import Data.Ord (Ord)
  11 import Prelude (Enum, Integer, Integral, Num, Real)
  12 import Text.Show (Show(..))
  13 import Text.Read (read)
  14 import qualified Data.Text as Text
  15
  16 import Language.Symantic
  17 import Language.Symantic.Grammar
  18
  19 -- * Class 'Sym_Integer'
  20 type instance Sym Integer = Sym_Integer
  21 class Sym_Integer term where
  22         integer :: Integer -> term Integer
  23         default integer :: Sym_Integer (UnT term) => Trans term => Integer -> term Integer
  24         integer = trans . integer
  25
  26 -- Interpreting
  27 instance Sym_Integer Eval where
  28         integer = Eval
  29 instance Sym_Integer View where
  30         integer a = View $ \_p _v ->
  31                 Text.pack (show a)
  32 instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (Dup r1 r2) where
  33         integer x = integer x `Dup` integer x
  34
  35 -- Transforming
  36 instance (Sym_Integer term, Sym_Lambda term) => Sym_Integer (BetaT term)
  37
  38 -- Typing
  39 instance NameTyOf Integer where
  40         nameTyOf _c = ["Integer"] `Mod` "Integer"
  41 instance ClassInstancesFor Integer where
  42         proveConstraintFor _ (TyConst _ _ q :$ z)
  43          | Just HRefl <- proj_ConstKiTy @_ @Integer z
  44          = case () of
  45                  _ | Just Refl <- proj_Const @Enum     q -> Just Dict
  46                    | Just Refl <- proj_Const @Eq       q -> Just Dict
  47                    | Just Refl <- proj_Const @Integral q -> Just Dict
  48                    | Just Refl <- proj_Const @Num      q -> Just Dict
  49                    | Just Refl <- proj_Const @Ord      q -> Just Dict
  50                    | Just Refl <- proj_Const @Real     q -> Just Dict
  51                    | Just Refl <- proj_Const @Show     q -> Just Dict
  52                  _ -> Nothing
  53         proveConstraintFor _c _q = Nothing
  54 instance TypeInstancesFor Integer
  55
  56 -- Compiling
  57 instance
  58  ( Gram_Source src g
  59  , Gram_Alt g
  60  , Gram_AltApp g
  61  , Gram_Rule g
  62  , Gram_Comment g
  63  , SymInj ss Integer
  64  ) => Gram_Term_AtomsFor src ss g Integer where
  65         g_term_atomsFor =
  66          [ rule "teinteger" $
  67                 lexeme $ source $
  68                 (\i src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teInteger $ read i)
  69                  <$> some (choice $ char <$> ['0'..'9'])
  70          ]
  71 instance ModuleFor src ss Integer
  72
  73 -- ** 'Term's
  74 tyInteger :: Source src => LenInj vs => Type src vs Integer
  75 tyInteger = tyConst @(K Integer) @Integer
  76
  77 teInteger :: Source src => SymInj ss Integer => Integer -> Term src ss ts '[] (() #> Integer)
  78 teInteger i = Term noConstraint tyInteger $ teSym @Integer $ integer i