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.Parsing.Grammar
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming.Trans
  19 import Language.Symantic.Lib.Lambda
  20
  21 -- * Class 'Sym_Tuple'
  22 class Sym_Either term where
  23         _Left  :: term l -> term (Either l r)
  24         _Right :: term r -> term (Either l r)
  25         either :: term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
  26         default _Left  :: Trans t term => t term l -> t term (Either l r)
  27         default _Right :: Trans t term => t term r -> t term (Either l r)
  28         default either :: Trans t term => t term (l -> a) -> t term (r -> a) -> t term (Either l r) -> t term a
  29         _Left  = trans_map1 _Left
  30         _Right = trans_map1 _Right
  31         either = trans_map3 either
  32
  33 type instance Sym_of_Iface (Proxy Either) = Sym_Either
  34 type instance Consts_of_Iface (Proxy Either) = Proxy Either ': Consts_imported_by Either
  35 type instance Consts_imported_by Either =
  36  [ Proxy (->)
  37  , Proxy Applicative
  38  , Proxy Eq
  39  , Proxy Foldable
  40  , Proxy Functor
  41  , Proxy Monad
  42  , Proxy Ord
  43  , Proxy Show
  44  , Proxy Traversable
  45  ]
  46
  47 instance Sym_Either HostI where
  48         _Right = liftM Right
  49         _Left  = liftM Left
  50         either = liftM3 Either.either
  51 instance Sym_Either TextI where
  52         _Right = textI1 "Right"
  53         _Left  = textI1 "Left"
  54         either = textI3 "either"
  55 instance (Sym_Either r1, Sym_Either r2) => Sym_Either (DupI r1 r2) where
  56         _Left  = dupI1 (Proxy @Sym_Either) _Left
  57         _Right = dupI1 (Proxy @Sym_Either) _Right
  58         either = dupI3 (Proxy @Sym_Either) either
  59
  60 instance
  61  ( Read_TypeNameR Type_Name cs rs
  62  , Inj_Const cs Either
  63  ) => Read_TypeNameR Type_Name cs (Proxy Either ': rs) where
  64         read_typenameR _cs (Type_Name "Either") k = k (ty @Either)
  65         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  66 instance Show_Const cs => Show_Const (Proxy Either ': cs) where
  67         show_const ConstZ{} = "Either"
  68         show_const (ConstS c) = show_const c
  69 instance -- Proj_ConC
  70  ( Proj_Const cs Either
  71  , Proj_Consts cs (Consts_imported_by Either)
  72  , Proj_Con cs
  73  ) => Proj_ConC cs (Proxy Either) where
  74         proj_conC _ (TyConst q :$ (TyConst c :$ _l))
  75          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  76          , Just Refl <- proj_const c (Proxy @Either)
  77          = case () of
  78                  _ | Just Refl <- proj_const q (Proxy @Functor)     -> Just Con
  79                    | Just Refl <- proj_const q (Proxy @Applicative) -> Just Con
  80                    | Just Refl <- proj_const q (Proxy @Monad)       -> Just Con
  81                    | Just Refl <- proj_const q (Proxy @Foldable)    -> Just Con
  82                    | Just Refl <- proj_const q (Proxy @Traversable) -> Just Con
  83                  _ -> Nothing
  84         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ l :$ r))
  85          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  86          , Just Refl <- proj_const c (Proxy @Either)
  87          = case () of
  88                  _ | Just Refl <- proj_const q (Proxy @Eq)
  89                    , Just Con  <- proj_con (t :$ l)
  90                    , Just Con  <- proj_con (t :$ r) -> Just Con
  91                    | Just Refl <- proj_const q (Proxy @Ord)
  92                    , Just Con  <- proj_con (t :$ l)
  93                    , Just Con  <- proj_con (t :$ r) -> Just Con
  94                    | Just Refl <- proj_const q (Proxy @Show)
  95                    , Just Con  <- proj_con (t :$ l)
  96                    , Just Con  <- proj_con (t :$ r) -> Just Con
  97                  _ -> Nothing
  98         proj_conC _c _q = Nothing
  99 data instance TokenT meta (ts::[*]) (Proxy Either)
 100  = Token_Term_Either_Left   (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 101  | Token_Term_Either_Right  (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 102  | Token_Term_Either_either (EToken meta ts) (EToken meta ts)
 103 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Either))
 104 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Either))
 105 instance -- CompileI
 106  ( Read_TypeName Type_Name (Consts_of_Ifaces is)
 107  , Inj_Const (Consts_of_Ifaces is) Either
 108  , Inj_Const (Consts_of_Ifaces is) (->)
 109  -- , Proj_Token is Token_Type
 110  , Compile is
 111  ) => CompileI is (Proxy Either) where
 112         compileI tok ctx k =
 113                 case tok of
 114                  Token_Term_Either_Left tok_ty_r tok_l ->
 115                         -- Left :: l -> Either l r
 116                         compile_type tok_ty_r $ \(ty_r::Type (Consts_of_Ifaces is) r) ->
 117                         check_kind
 118                          (At Nothing SKiType)
 119                          (At (Just tok_ty_r) $ kind_of ty_r) $ \Refl ->
 120                         compileO tok_l ctx $ \ty_l (TermO l) ->
 121                         k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
 122                          \c -> _Left (l c)
 123                  Token_Term_Either_Right tok_ty_l tok_r ->
 124                         -- Right :: r -> Either l r
 125                         compile_type tok_ty_l $ \(ty_l::Type (Consts_of_Ifaces is) l) ->
 126                         check_kind
 127                          (At Nothing SKiType)
 128                          (At (Just tok_ty_l) $ kind_of ty_l) $ \Refl ->
 129                         compileO tok_r ctx $ \ty_r (TermO r) ->
 130                         k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
 131                          \c -> _Right (r c)
 132                  Token_Term_Either_either tok_l2a tok_r2a ->
 133                         -- either :: (l -> a) -> (r -> a) -> Either l r -> a
 134                         compileO tok_l2a ctx $ \ty_l2a (TermO l2a) ->
 135                         compileO tok_r2a ctx $ \ty_r2a (TermO r2a) ->
 136                         check_type2 (ty @(->)) (At (Just tok_l2a) ty_l2a) $ \Refl ty_l2a_l ty_l2a_a ->
 137                         check_type2 (ty @(->)) (At (Just tok_r2a) ty_r2a) $ \Refl ty_r2a_r ty_r2a_a ->
 138                         check_type (At (Just tok_l2a) ty_l2a_a) (At (Just tok_r2a) ty_r2a_a) $ \Refl ->
 139                         k ((ty @Either :$ ty_l2a_l) :$ ty_r2a_r ~> ty_l2a_a) $ TermO $
 140                          \c -> lam $ either (l2a c) (r2a c)
 141 instance -- TokenizeT
 142  Inj_Token meta ts Either =>
 143  TokenizeT meta ts (Proxy Either) where
 144         tokenizeT _t = mempty
 145          { tokenizers_infix = tokenizeTMod []
 146                  [ (Term_Name "Left",) Term_ProTok
 147                          { term_protok = \meta -> ProTokLam $ \l -> ProTokPi $ \r ->
 148                                 ProTok $ inj_etoken meta $ Token_Term_Either_Left r l
 149                          , term_fixity = infixN5 }
 150                  , (Term_Name "Right",) Term_ProTok
 151                          { term_protok = \meta -> ProTokPi $ \l -> ProTokLam $ \r ->
 152                                 ProTok $ inj_etoken meta $ Token_Term_Either_Right l r
 153                          , term_fixity = infixN5 }
 154                  , tokenize2 "either" infixN5 Token_Term_Either_either
 155                  ]
 156          }
 157 instance Gram_Term_AtomsT meta ts (Proxy Either) g