Language/LOL/Symantic/Type/Bool.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE OverloadedStrings #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7 module Language.LOL.Symantic.Type.Bool where
   8
   9 import Data.Maybe (isJust)
  10 import Data.Type.Equality ((:~:)(Refl))
  11
  12 import Language.LOL.Symantic.Raw
  13 import Language.LOL.Symantic.Type.Common
  14 import Language.LOL.Symantic.Type.Fun
  15
  16 -- * Type 'Type_Bool'
  17
  18 -- | The 'Bool' type.
  19 data Type_Bool (root:: * -> *) h where
  20         Type_Bool :: Type_Bool root Bool
  21 type instance Root_of_Type (Type_Bool root) = root
  22 type instance Error_of_Type raw (Type_Bool root) = Error_Type_Fun raw
  23
  24 -- | Convenient alias.
  25 type Type_Fun_Bool lam = Type_Root (Type_Cons (Type_Fun lam) Type_Bool)
  26
  27 -- | Convenient alias to include a 'Type_Bool' within a type.
  28 type_bool :: Type_Root_Lift Type_Bool root => root Bool
  29 type_bool = type_root_lift Type_Bool
  30
  31 {-
  32 r :: Type_Root_Lift curr root => curr root h -> root h
  33 r = type_root_lift
  34
  35 t0 :: Type_Root Type_Bool Bool
  36 t0 = Type_Root $ Type_Bool
  37
  38 t1 :: Type_Fun_Bool lam (lam Bool -> lam Bool)
  39 t1 = r $ Type_Fun (r Type_Bool) (r Type_Bool)
  40
  41 t2 :: Type_Fun_Bool lam (lam Bool -> lam (lam Bool -> lam Bool))
  42 t2 = r $ Type_Fun (r Type_Bool) (r $ Type_Fun (r Type_Bool) (r Type_Bool))
  43
  44 t3 :: Type_Fun_Bool lam (lam (lam Bool -> lam Bool) -> lam Bool)
  45 t3 = r $ Type_Fun (r $ Type_Fun (r Type_Bool) (r Type_Bool)) (r Type_Bool)
  46 -}
  47
  48 instance -- Type_Eq
  49  Type_Eq (Type_Bool root) where
  50         type_eq Type_Bool Type_Bool = Just Refl
  51 instance -- Eq
  52  Eq (Type_Bool root h) where
  53         x == y = isJust $ type_eq x y
  54 instance -- Type_from Raw
  55  ( Type_Root_Lift Type_Bool root
  56  , Error_Type_Lift (Error_Type_Fun Raw) (Error_of_Type Raw root)
  57    -- NOTE: require UndecidableInstances.
  58  ) => Type_from Raw (Type_Bool root) where
  59         type_from _px_ty raw@(Raw "Bool" raws) k =
  60                 case raws of
  61                  [] -> k $ type_root_lift Type_Bool
  62                  _ -> Left $ Just $ error_type_lift $
  63                         Error_Type_Fun_Wrong_number_of_arguments 0 raw
  64         type_from _px_ty _raw _k = Left Nothing
  65 instance -- String_from_Type
  66  String_from_Type (Type_Bool root) where
  67         string_from_type Type_Bool = "Bool"
  68 instance -- Show
  69  Show (Type_Bool root h) where
  70         show = string_from_type