TFHOE/Type/Int.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 module TFHOE.Type.Int where
   7
   8 import Data.Maybe (isJust)
   9 import Data.Type.Equality ((:~:)(Refl))
  10
  11 import TFHOE.Raw
  12 import TFHOE.Type.Common
  13 import TFHOE.Type.Bool
  14
  15 -- * Type 'Type_Int'
  16
  17 -- | GADT for integer type:
  18 --
  19 -- * singleton (bijective mapping between Haskell type @h@ and the GADT's terms),
  20 -- * and extensible (through @next@).
  21 data Type_Int (next:: * -> *) h where
  22         Type_Int      :: Type_Int next Int -- Introduce an 'Int' type.
  23         Type_Int_Next :: next h -> Type_Int next h -- Introduce a type extension @next@.
  24
  25 type Type_Fun_Bool_Int repr next = Type_Fun_Bool repr (Type_Int next)
  26 type Type_Fun_Bool_Int_End repr  = Type_Fun_Bool_Int repr Type_End
  27
  28 instance -- Type_Eq
  29  Type_Eq next =>
  30  Type_Eq (Type_Int next) where
  31         type_eq Type_Int Type_Int = Just Refl
  32         type_eq (Type_Int_Next x) (Type_Int_Next y) = x `type_eq` y
  33         type_eq _ _ = Nothing
  34 instance -- Eq
  35  Type_Eq next =>
  36  Eq (Type_Int next h) where
  37         x == y = isJust $ type_eq x y
  38 instance -- Type_from Raw
  39  Type_from Raw next =>
  40  Type_from Raw (Type_Int next) where
  41         type_from (Raw "Int" []) k = k Type_Int
  42         type_from raw k = type_from raw $ k . Type_Int_Next
  43 instance -- String_from_Type
  44  String_from_Type next =>
  45  String_from_Type (Type_Int next) where
  46         string_from_type Type_Int = "Int"
  47         string_from_type (Type_Int_Next t) = string_from_type t
  48 instance -- Show
  49  String_from_Type next =>
  50  Show (Type_Int next h) where
  51         show = string_from_type