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 Data.Eq (Eq)
   7 import Data.Function (($), (.))
   8 import Data.Int (Int)
   9 import Data.Maybe (Maybe(..))
  10 import Data.Ord (Ord)
  11 import Prelude (Bounded, Enum, Integral, Num, Real)
  12 import Text.Show (Show(..))
  13 import qualified Data.Text as Text
  14
  15 import Language.Symantic
  16
  17 -- * Class 'Sym_Int'
  18 type instance Sym Int = Sym_Int
  19 class Sym_Int term where
  20         int :: Int -> term Int
  21         default int :: Sym_Int (UnT term) => Trans term => Int -> term Int
  22         int = trans . int
  23
  24 -- Interpreting
  25 instance Sym_Int Eval where
  26         int = Eval
  27 instance Sym_Int View where
  28         int a = View $ \_p _v ->
  29                 Text.pack (show a)
  30 instance (Sym_Int r1, Sym_Int r2) => Sym_Int (Dup r1 r2) where
  31         int x = int x `Dup` int x
  32
  33 -- Transforming
  34 instance (Sym_Int term, Sym_Lambda term) => Sym_Int (BetaT term)
  35
  36 -- Typing
  37 instance NameTyOf Int where
  38         nameTyOf _c = ["Int"] `Mod` "Int"
  39 instance ClassInstancesFor Int where
  40         proveConstraintFor _c (TyConst _ _ q :$ z)
  41          | Just HRefl <- proj_ConstKiTy @_ @Int z
  42          = case () of
  43                  _ | Just Refl <- proj_Const @Bounded  q -> Just Dict
  44                    | Just Refl <- proj_Const @Enum     q -> Just Dict
  45                    | Just Refl <- proj_Const @Eq       q -> Just Dict
  46                    | Just Refl <- proj_Const @Integral q -> Just Dict
  47                    | Just Refl <- proj_Const @Num      q -> Just Dict
  48                    | Just Refl <- proj_Const @Ord      q -> Just Dict
  49                    | Just Refl <- proj_Const @Real     q -> Just Dict
  50                    | Just Refl <- proj_Const @Show     q -> Just Dict
  51                  _ -> Nothing
  52         proveConstraintFor _c _q = Nothing
  53 instance TypeInstancesFor Int
  54
  55 -- Compiling
  56 instance Gram_Term_AtomsFor src ss g Int
  57 instance ModuleFor src ss Int
  58
  59 -- ** 'Type's
  60 tyInt :: Source src => LenInj vs => Type src vs Int
  61 tyInt = tyConst @(K Int) @Int
  62
  63 -- ** 'Term's
  64 teInt :: Source src => SymInj ss Int => Int -> Term src ss ts '[] (() #> Int)
  65 teInt i = Term noConstraint tyInt $ teSym @Int $ int i