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

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Int'.
   4 module Language.Symantic.Lib.Int where
   5
   6 import qualified Data.Text as Text
   7
   8 import Language.Symantic
   9
  10 -- * Class 'Sym_Int'
  11 type instance Sym Int = Sym_Int
  12 class Sym_Int term where
  13         int :: Int -> term Int
  14         default int :: Sym_Int (UnT term) => Trans term => Int -> term Int
  15         int = trans . int
  16
  17 -- Interpreting
  18 instance Sym_Int Eval where
  19         int = Eval
  20 instance Sym_Int View where
  21         int a = View $ \_p _v ->
  22                 Text.pack (show a)
  23 instance (Sym_Int r1, Sym_Int r2) => Sym_Int (Dup r1 r2) where
  24         int x = int x `Dup` int x
  25
  26 -- Transforming
  27 instance (Sym_Int term, Sym_Lambda term) => Sym_Int (BetaT term)
  28
  29 -- Typing
  30 instance ClassInstancesFor Int where
  31         proveConstraintFor _c (TyApp _ (TyConst _ _ q) z)
  32          | Just HRefl <- proj_ConstKiTy @_ @Int z
  33          = case () of
  34                  _ | Just Refl <- proj_Const @Bounded  q -> Just Dict
  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 Int
  45
  46 -- Compiling
  47 instance Gram_Term_AtomsFor src ss g Int
  48 instance ModuleFor src ss Int
  49
  50 -- ** 'Type's
  51 tyInt :: Source src => LenInj vs => Type src vs Int
  52 tyInt = tyConst @(K Int) @Int
  53
  54 -- ** 'Term's
  55 teInt :: Source src => SymInj ss Int => Int -> Term src ss ts '[] (() #> Int)
  56 teInt i = Term noConstraint tyInt $ teSym @Int $ int i