TFHOE/Type/Bool.hs

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