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 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 NameTyOf Integer where
  32         nameTyOf _c = ["Integer"] `Mod` "Integer"
  33 instance ClassInstancesFor Integer where
  34         proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
  35          | Just HRefl <- proj_ConstKiTy @_ @Integer z
  36          = case () of
  37                  _ | Just Refl <- proj_Const @Enum     q -> Just Dict
  38                    | Just Refl <- proj_Const @Eq       q -> Just Dict
  39                    | Just Refl <- proj_Const @Integral q -> Just Dict
  40                    | Just Refl <- proj_Const @Num      q -> Just Dict
  41                    | Just Refl <- proj_Const @Ord      q -> Just Dict
  42                    | Just Refl <- proj_Const @Real     q -> Just Dict
  43                    | Just Refl <- proj_Const @Show     q -> Just Dict
  44                  _ -> Nothing
  45         proveConstraintFor _c _q = Nothing
  46 instance TypeInstancesFor Integer
  47
  48 -- Compiling
  49 instance
  50  ( Gram_Source src g
  51  , Gram_Alt g
  52  , Gram_AltApp g
  53  , Gram_Rule g
  54  , Gram_Comment g
  55  , SymInj ss Integer
  56  ) => Gram_Term_AtomsFor src ss g Integer where
  57         g_term_atomsFor =
  58          [ rule "teinteger" $
  59                 lexeme $ source $
  60                 (\i src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teInteger $ read i)
  61                  <$> some (choice $ char <$> ['0'..'9'])
  62          ]
  63 instance ModuleFor src ss Integer
  64
  65 -- ** 'Term's
  66 tyInteger :: Source src => LenInj vs => Type src vs Integer
  67 tyInteger = tyConst @(K Integer) @Integer
  68
  69 teInteger :: Source src => SymInj ss Integer => Integer -> Term src ss ts '[] (() #> Integer)
  70 teInteger i = Term noConstraint tyInteger $ teSym @Integer $ integer i