symantic-lib/Language/Symantic/Lib/Either.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
   4 -- | Symantic for 'Either'.
   5 module Language.Symantic.Lib.Either where
   6
   7 import Control.Monad (liftM, liftM3)
   8 import qualified Data.Either as Either
   9 import Data.Proxy
  10 import Data.Type.Equality ((:~:)(Refl))
  11 import Prelude hiding (either)
  12
  13 import Language.Symantic.Parsing
  14 import Language.Symantic.Typing
  15 import Language.Symantic.Compiling
  16 import Language.Symantic.Interpreting
  17 import Language.Symantic.Transforming
  18 import Language.Symantic.Lib.Lambda
  19
  20 -- * Class 'Sym_Tuple'
  21 class Sym_Either term where
  22         _Left  :: term l -> term (Either l r)
  23         _Right :: term r -> term (Either l r)
  24         either :: term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
  25         default _Left  :: Trans t term => t term l -> t term (Either l r)
  26         default _Right :: Trans t term => t term r -> t term (Either l r)
  27         default either :: Trans t term => t term (l -> a) -> t term (r -> a) -> t term (Either l r) -> t term a
  28         _Left  = trans_map1 _Left
  29         _Right = trans_map1 _Right
  30         either = trans_map3 either
  31
  32 type instance Sym_of_Iface (Proxy Either) = Sym_Either
  33 type instance TyConsts_of_Iface (Proxy Either) = Proxy Either ': TyConsts_imported_by Either
  34 type instance TyConsts_imported_by Either =
  35  [ Proxy (->)
  36  , Proxy Applicative
  37  , Proxy Eq
  38  , Proxy Foldable
  39  , Proxy Functor
  40  , Proxy Monad
  41  , Proxy Ord
  42  , Proxy Show
  43  , Proxy Traversable
  44  ]
  45
  46 instance Sym_Either HostI where
  47         _Right = liftM Right
  48         _Left  = liftM Left
  49         either = liftM3 Either.either
  50 instance Sym_Either TextI where
  51         _Right = textI1 "Right"
  52         _Left  = textI1 "Left"
  53         either = textI3 "either"
  54 instance (Sym_Either r1, Sym_Either r2) => Sym_Either (DupI r1 r2) where
  55         _Left  = dupI1 @Sym_Either _Left
  56         _Right = dupI1 @Sym_Either _Right
  57         either = dupI3 @Sym_Either either
  58
  59 instance
  60  ( Read_TyNameR TyName cs rs
  61  , Inj_TyConst cs Either
  62  ) => Read_TyNameR TyName cs (Proxy Either ': rs) where
  63         read_TyNameR _cs (TyName "Either") k = k (ty @Either)
  64         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  65 instance Show_TyConst cs => Show_TyConst (Proxy Either ': cs) where
  66         show_TyConst TyConstZ{} = "Either"
  67         show_TyConst (TyConstS c) = show_TyConst c
  68 instance -- Proj_TyConC
  69  ( Proj_TyConst cs Either
  70  , Proj_TyConsts cs (TyConsts_imported_by Either)
  71  , Proj_TyCon cs
  72  ) => Proj_TyConC cs (Proxy Either) where
  73         proj_TyConC _ (TyConst q :$ (TyConst c :$ _l))
  74          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  75          , Just Refl <- proj_TyConst c (Proxy @Either)
  76          = case () of
  77                  _ | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
  78                    | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
  79                    | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
  80                    | Just Refl <- proj_TyConst q (Proxy @Foldable)    -> Just TyCon
  81                    | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
  82                  _ -> Nothing
  83         proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ l :$ r))
  84          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  85          , Just Refl <- proj_TyConst c (Proxy @Either)
  86          = case () of
  87                  _ | Just Refl <- proj_TyConst q (Proxy @Eq)
  88                    , Just TyCon  <- proj_TyCon (t :$ l)
  89                    , Just TyCon  <- proj_TyCon (t :$ r) -> Just TyCon
  90                    | Just Refl <- proj_TyConst q (Proxy @Ord)
  91                    , Just TyCon  <- proj_TyCon (t :$ l)
  92                    , Just TyCon  <- proj_TyCon (t :$ r) -> Just TyCon
  93                    | Just Refl <- proj_TyConst q (Proxy @Show)
  94                    , Just TyCon  <- proj_TyCon (t :$ l)
  95                    , Just TyCon  <- proj_TyCon (t :$ r) -> Just TyCon
  96                  _ -> Nothing
  97         proj_TyConC _c _q = Nothing
  98 data instance TokenT meta (ts::[*]) (Proxy Either)
  99  = Token_Term_Either_Left   (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 100  | Token_Term_Either_Right  (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 101  | Token_Term_Either_either (EToken meta ts) (EToken meta ts)
 102 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Either))
 103 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Either))
 104 instance -- CompileI
 105  ( Read_TyName TyName cs
 106  , Inj_TyConst        cs Either
 107  , Inj_TyConst        cs (->)
 108  -- , Proj_Token is Token_Type
 109  , Compile cs is
 110  ) => CompileI cs is (Proxy Either) where
 111         compileI tok ctx k =
 112                 case tok of
 113                  Token_Term_Either_Left tok_ty_r tok_l ->
 114                         -- Left :: l -> Either l r
 115                         compile_Type tok_ty_r $ \(ty_r::Type cs r) ->
 116                         check_Kind
 117                          (At Nothing SKiType)
 118                          (At (Just tok_ty_r) $ kind_of ty_r) $ \Refl ->
 119                         compileO tok_l ctx $ \ty_l (TermO l) ->
 120                         k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
 121                          \c -> _Left (l c)
 122                  Token_Term_Either_Right tok_ty_l tok_r ->
 123                         -- Right :: r -> Either l r
 124                         compile_Type tok_ty_l $ \(ty_l::Type cs l) ->
 125                         check_Kind
 126                          (At Nothing SKiType)
 127                          (At (Just tok_ty_l) $ kind_of ty_l) $ \Refl ->
 128                         compileO tok_r ctx $ \ty_r (TermO r) ->
 129                         k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
 130                          \c -> _Right (r c)
 131                  Token_Term_Either_either tok_l2a tok_r2a ->
 132                         -- either :: (l -> a) -> (r -> a) -> Either l r -> a
 133                         compileO tok_l2a ctx $ \ty_l2a (TermO l2a) ->
 134                         compileO tok_r2a ctx $ \ty_r2a (TermO r2a) ->
 135                         check_TyEq2 (ty @(->)) (At (Just tok_l2a) ty_l2a) $ \Refl ty_l2a_l ty_l2a_a ->
 136                         check_TyEq2 (ty @(->)) (At (Just tok_r2a) ty_r2a) $ \Refl ty_r2a_r ty_r2a_a ->
 137                         check_TyEq (At (Just tok_l2a) ty_l2a_a) (At (Just tok_r2a) ty_r2a_a) $ \Refl ->
 138                         k ((ty @Either :$ ty_l2a_l) :$ ty_r2a_r ~> ty_l2a_a) $ TermO $
 139                          \c -> lam $ either (l2a c) (r2a c)
 140 instance -- TokenizeT
 141  Inj_Token meta ts Either =>
 142  TokenizeT meta ts (Proxy Either) where
 143         tokenizeT _t = mempty
 144          { tokenizers_infix = tokenizeTMod []
 145                  [ (Term_Name "Left",) Term_ProTok
 146                          { term_protok = \meta -> ProTokLam $ \l -> ProTokPi $ \r ->
 147                                 ProTok $ inj_EToken meta $ Token_Term_Either_Left r l
 148                          , term_fixity = infixN5 }
 149                  , (Term_Name "Right",) Term_ProTok
 150                          { term_protok = \meta -> ProTokPi $ \l -> ProTokLam $ \r ->
 151                                 ProTok $ inj_EToken meta $ Token_Term_Either_Right l r
 152                          , term_fixity = infixN5 }
 153                  , tokenize2 "either" infixN5 Token_Term_Either_either
 154                  ]
 155          }
 156 instance Gram_Term_AtomsT meta ts (Proxy Either) g