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

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