Language/Symantic/Type/Type2.hs

   1 {-# LANGUAGE FlexibleInstances #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE ScopedTypeVariables #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7 module Language.Symantic.Type.Type2 where
   8
   9 import Data.Maybe (isJust)
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12
  13 import Language.Symantic.Lib.Data.Peano
  14 -- import Language.Symantic.Lib.Data.Bool
  15 import Language.Symantic.Type.Root
  16 -- import Language.Symantic.Type.Alt
  17 import Language.Symantic.Type.Error
  18 import Language.Symantic.Type.Type0
  19 -- import Language.Symantic.Type.Type1
  20
  21 -- * Type 'Type_Type2'
  22 data Type_Type2 px (root:: * -> *) h where
  23         Type_Type2
  24          :: px -> root a -> root b
  25          -> Type_Type2 px root ((Host2_of px) a b)
  26
  27 type instance Root_of_Type      (Type_Type2 px root) = root
  28 type instance Error_of_Type ast (Type_Type2 px root) = No_Error_Type
  29
  30 instance -- Eq_Type
  31  Eq_Type root =>
  32  Eq_Type (Type_Type2 (Proxy h2) root) where
  33         eq_type
  34          (Type_Type2 _ arg1 res1)
  35          (Type_Type2 _ arg2 res2)
  36          | Just Refl <- arg1 `eq_type` arg2
  37          , Just Refl <- res1 `eq_type` res2
  38          = Just Refl
  39         eq_type _ _ = Nothing
  40 instance -- Eq_Type
  41  Eq_Type root =>
  42  Eq_Type (Type_Type2 EPeano root) where
  43         eq_type (Type_Type2 p1 arg1 res1)
  44                 (Type_Type2 p2 arg2 res2)
  45          | p1 == p2
  46          , Just Refl <- arg1 `eq_type` arg2
  47          , Just Refl <- res1 `eq_type` res2
  48          = Just Refl
  49         eq_type _ _ = Nothing
  50 instance -- Eq
  51  Eq_Type root =>
  52  Eq (Type_Type2 (Proxy h2) root h) where
  53         x == y = isJust $ x `eq_type` y
  54 instance -- Eq
  55  Eq_Type root =>
  56  Eq (Type_Type2 EPeano root h) where
  57         x == y = isJust $ x `eq_type` y
  58 instance -- Show
  59  ( String_from_Type root
  60  , String_from_Type (Type_Type2 px root)
  61  ) => Show (Type_Type2 px root h) where
  62         show = string_from_type
  63
  64 -- ** Type 'Host2_of'
  65 type family Host2_of px :: * -> * -> *
  66 type instance Host2_of (Proxy h2) = h2