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 qualified Data.Text as Text
   7
   8 import Language.Symantic
   9 import Language.Symantic.Grammar
  10
  11 -- * Class 'Sym_Integer'
  12 type instance Sym (Proxy Integer) = Sym_Integer
  13 class Sym_Integer term where
  14         integer :: Integer -> term Integer
  15         default integer :: Sym_Integer (UnT term) => Trans term => Integer -> term Integer
  16         integer = trans . integer
  17
  18 -- Interpreting
  19 instance Sym_Integer Eval where
  20         integer = Eval
  21 instance Sym_Integer View where
  22         integer a = View $ \_p _v ->
  23                 Text.pack (show a)
  24 instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (Dup r1 r2) where
  25         integer x = integer x `Dup` integer x
  26
  27 -- Transforming
  28 instance (Sym_Integer term, Sym_Lambda term) => Sym_Integer (BetaT term)
  29
  30 -- Typing
  31 instance ClassInstancesFor Integer where
  32         proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
  33          | Just HRefl <- proj_ConstKiTy @_ @Integer z
  34          = case () of
  35                  _ | Just Refl <- proj_Const @Enum     q -> Just Dict
  36                    | Just Refl <- proj_Const @Eq       q -> Just Dict
  37                    | Just Refl <- proj_Const @Integral q -> Just Dict
  38                    | Just Refl <- proj_Const @Num      q -> Just Dict
  39                    | Just Refl <- proj_Const @Ord      q -> Just Dict
  40                    | Just Refl <- proj_Const @Real     q -> Just Dict
  41                    | Just Refl <- proj_Const @Show     q -> Just Dict
  42                  _ -> Nothing
  43         proveConstraintFor _c _q = Nothing
  44 instance TypeInstancesFor Integer
  45
  46 -- Compiling
  47 instance
  48  ( Gram_Source src g
  49  , Gram_Alt g
  50  , Gram_AltApp g
  51  , Gram_Rule g
  52  , Gram_Comment g
  53  , Inj_Sym ss Integer
  54  ) => Gram_Term_AtomsFor src ss g Integer where
  55         g_term_atomsFor =
  56          [ rule "teinteger" $
  57                 lexeme $ g_source $
  58                 (\i src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teInteger $ read i)
  59                  <$> some (choice $ char <$> ['0'..'9'])
  60          ]
  61 instance ModuleFor src ss Integer
  62
  63 -- ** 'Term's
  64 tyInteger :: Source src => Inj_Len vs => Type src vs Integer
  65 tyInteger = tyConst @(K Integer) @Integer
  66
  67 teInteger :: Source src => Inj_Sym ss Integer => Integer -> Term src ss ts '[] (() #> Integer)
  68 teInteger i = Term noConstraint tyInteger $ teSym @Integer $ integer i