Language/Symantic/Compiling/Either.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
   4 -- | Symantic for 'Either'.
   5 module Language.Symantic.Compiling.Either where
   6
   7 import Control.Monad (liftM, liftM3)
   8 import qualified Data.Either as Either
   9 import Data.Proxy
  10 import Data.Text (Text)
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Prelude hiding (either)
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling.Term
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming.Trans
  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 Consts_of_Iface (Proxy Either) = Proxy Either ': Consts_imported_by Either
  34 type instance Consts_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 Traversable
  43  ]
  44
  45 instance Sym_Either HostI where
  46         _Right = liftM Right
  47         _Left  = liftM Left
  48         either = liftM3 Either.either
  49 instance Sym_Either TextI where
  50         _Right = textI_app1 "Right"
  51         _Left  = textI_app1 "Left"
  52         either = textI_app3 "either"
  53 instance (Sym_Either r1, Sym_Either r2) => Sym_Either (DupI r1 r2) where
  54         _Left  = dupI1 (Proxy @Sym_Either) _Left
  55         _Right = dupI1 (Proxy @Sym_Either) _Right
  56         either = dupI3 (Proxy @Sym_Either) either
  57
  58 instance Const_from Text cs => Const_from Text (Proxy Either ': cs) where
  59         const_from "Either" k = k (ConstZ kind)
  60         const_from s k = const_from s $ k . ConstS
  61 instance Show_Const cs => Show_Const (Proxy Either ': cs) where
  62         show_const ConstZ{} = "Either"
  63         show_const (ConstS c) = show_const c
  64 instance -- Proj_ConC
  65  ( Proj_Const cs Either
  66  , Proj_Consts cs (Consts_imported_by Either)
  67  , Proj_Con cs
  68  ) => Proj_ConC cs (Proxy Either) where
  69         proj_conC _ (TyConst q :$ (TyConst c :$ _l))
  70          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  71          , Just Refl <- proj_const c (Proxy::Proxy Either)
  72          = case () of
  73                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  74                    | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
  75                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
  76                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
  77                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
  78                  _ -> Nothing
  79         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ l :$ r))
  80          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  81          , Just Refl <- proj_const c (Proxy::Proxy Either)
  82          = case () of
  83                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
  84                    , Just Con  <- proj_con (t :$ l)
  85                    , Just Con  <- proj_con (t :$ r) -> Just Con
  86                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
  87                    , Just Con  <- proj_con (t :$ l)
  88                    , Just Con  <- proj_con (t :$ r) -> Just Con
  89                  _ -> Nothing
  90         proj_conC _c _q = Nothing
  91 data instance TokenT meta (ts::[*]) (Proxy Either)
  92  = Token_Term_Either_Left   (EToken meta '[Proxy Token_Type]) (EToken meta ts)
  93  | Token_Term_Either_Right  (EToken meta '[Proxy Token_Type]) (EToken meta ts)
  94  | Token_Term_Either_either (EToken meta ts) (EToken meta ts)
  95 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Either))
  96 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Either))
  97 instance -- Term_fromI
  98  ( Const_from Name_LamVar (Consts_of_Ifaces is)
  99  , Inj_Const (Consts_of_Ifaces is) Either
 100  , Inj_Const (Consts_of_Ifaces is) (->)
 101  -- , Proj_Token is Token_Type
 102  , Term_from is
 103  ) => Term_fromI is (Proxy Either) where
 104         term_fromI tok ctx k =
 105                 case tok of
 106                  Token_Term_Either_Left tok_ty_r tok_l ->
 107                         -- Left :: l -> Either l r
 108                         type_from tok_ty_r $ \(ty_r::Type (Consts_of_Ifaces is) r) ->
 109                         check_kind
 110                          (At Nothing SKiType)
 111                          (At (Just tok_ty_r) $ kind_of ty_r) $ \Refl ->
 112                         term_from tok_l ctx $ \ty_l (TermLC l) ->
 113                         k ((ty @Either :$ ty_l) :$ ty_r) $ TermLC $
 114                          \c -> _Left (l c)
 115                  Token_Term_Either_Right tok_ty_l tok_r ->
 116                         -- Right :: r -> Either l r
 117                         type_from tok_ty_l $ \(ty_l::Type (Consts_of_Ifaces is) l) ->
 118                         check_kind
 119                          (At Nothing SKiType)
 120                          (At (Just tok_ty_l) $ kind_of ty_l) $ \Refl ->
 121                         term_from tok_r ctx $ \ty_r (TermLC r) ->
 122                         k ((ty @Either :$ ty_l) :$ ty_r) $ TermLC $
 123                          \c -> _Right (r c)
 124                  Token_Term_Either_either tok_l2a tok_r2a ->
 125                         -- either :: (l -> a) -> (r -> a) -> Either l r -> a
 126                         term_from tok_l2a ctx $ \ty_l2a (TermLC l2a) ->
 127                         term_from tok_r2a ctx $ \ty_r2a (TermLC r2a) ->
 128                         check_type2 (ty @(->)) (At (Just tok_l2a) ty_l2a) $ \Refl ty_l2a_l ty_l2a_a ->
 129                         check_type2 (ty @(->)) (At (Just tok_r2a) ty_r2a) $ \Refl ty_r2a_r ty_r2a_a ->
 130                         check_type (At (Just tok_l2a) ty_l2a_a) (At (Just tok_r2a) ty_r2a_a) $ \Refl ->
 131                         k ((ty @Either :$ ty_l2a_l) :$ ty_r2a_r ~> ty_l2a_a) $ TermLC $
 132                          \c -> lam $ either (l2a c) (r2a c)