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 NameTyOf Int where
  31         nameTyOf _c = ["Int"] `Mod` "Int"
  32 instance ClassInstancesFor Int where
  33         proveConstraintFor _c (TyApp _ (TyConst _ _ q) z)
  34          | Just HRefl <- proj_ConstKiTy @_ @Int z
  35          = case () of
  36                  _ | Just Refl <- proj_Const @Bounded  q -> Just Dict
  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 Int
  47
  48 -- Compiling
  49 instance Gram_Term_AtomsFor src ss g Int
  50 instance ModuleFor src ss Int
  51
  52 -- ** 'Type's
  53 tyInt :: Source src => LenInj vs => Type src vs Int
  54 tyInt = tyConst @(K Int) @Int
  55
  56 -- ** 'Term's
  57 teInt :: Source src => SymInj ss Int => Int -> Term src ss ts '[] (() #> Int)
  58 teInt i = Term noConstraint tyInt $ teSym @Int $ int i