Language/Symantic/Compiling/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.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 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 = textI_app1 "Right"
  52         _Left  = textI_app1 "Left"
  53         either = textI_app3 "either"
  54 instance (Sym_Either r1, Sym_Either r2) => Sym_Either (DupI r1 r2) where
  55         _Left  = dupI1 (Proxy @Sym_Either) _Left
  56         _Right = dupI1 (Proxy @Sym_Either) _Right
  57         either = dupI3 (Proxy @Sym_Either) either
  58
  59 instance Const_from Text cs => Const_from Text (Proxy Either ': cs) where
  60         const_from "Either" k = k (ConstZ kind)
  61         const_from s k = const_from s $ k . ConstS
  62 instance Show_Const cs => Show_Const (Proxy Either ': cs) where
  63         show_const ConstZ{} = "Either"
  64         show_const (ConstS c) = show_const c
  65 instance -- Proj_ConC
  66  ( Proj_Const cs Either
  67  , Proj_Consts cs (Consts_imported_by Either)
  68  , Proj_Con cs
  69  ) => Proj_ConC cs (Proxy Either) where
  70         proj_conC _ (TyConst q :$ (TyConst c :$ _l))
  71          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  72          , Just Refl <- proj_const c (Proxy::Proxy Either)
  73          = case () of
  74                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  75                    | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
  76                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
  77                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
  78                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
  79                  _ -> Nothing
  80         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ l :$ r))
  81          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  82          , Just Refl <- proj_const c (Proxy::Proxy Either)
  83          = case () of
  84                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
  85                    , Just Con  <- proj_con (t :$ l)
  86                    , Just Con  <- proj_con (t :$ r) -> Just Con
  87                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
  88                    , Just Con  <- proj_con (t :$ l)
  89                    , Just Con  <- proj_con (t :$ r) -> Just Con
  90                    | Just Refl <- proj_const q (Proxy::Proxy Show)
  91                    , Just Con  <- proj_con (t :$ l)
  92                    , Just Con  <- proj_con (t :$ r) -> Just Con
  93                  _ -> Nothing
  94         proj_conC _c _q = Nothing
  95 data instance TokenT meta (ts::[*]) (Proxy Either)
  96  = Token_Term_Either_Left   (EToken meta '[Proxy Token_Type]) (EToken meta ts)
  97  | Token_Term_Either_Right  (EToken meta '[Proxy Token_Type]) (EToken meta ts)
  98  | Token_Term_Either_either (EToken meta ts) (EToken meta ts)
  99 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Either))
 100 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Either))
 101 instance -- CompileI
 102  ( Const_from Name_LamVar (Consts_of_Ifaces is)
 103  , Inj_Const (Consts_of_Ifaces is) Either
 104  , Inj_Const (Consts_of_Ifaces is) (->)
 105  -- , Proj_Token is Token_Type
 106  , Compile is
 107  ) => CompileI is (Proxy Either) where
 108         compileI tok ctx k =
 109                 case tok of
 110                  Token_Term_Either_Left tok_ty_r tok_l ->
 111                         -- Left :: l -> Either l r
 112                         type_from tok_ty_r $ \(ty_r::Type (Consts_of_Ifaces is) r) ->
 113                         check_kind
 114                          (At Nothing SKiType)
 115                          (At (Just tok_ty_r) $ kind_of ty_r) $ \Refl ->
 116                         compileO tok_l ctx $ \ty_l (TermO l) ->
 117                         k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
 118                          \c -> _Left (l c)
 119                  Token_Term_Either_Right tok_ty_l tok_r ->
 120                         -- Right :: r -> Either l r
 121                         type_from tok_ty_l $ \(ty_l::Type (Consts_of_Ifaces is) l) ->
 122                         check_kind
 123                          (At Nothing SKiType)
 124                          (At (Just tok_ty_l) $ kind_of ty_l) $ \Refl ->
 125                         compileO tok_r ctx $ \ty_r (TermO r) ->
 126                         k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
 127                          \c -> _Right (r c)
 128                  Token_Term_Either_either tok_l2a tok_r2a ->
 129                         -- either :: (l -> a) -> (r -> a) -> Either l r -> a
 130                         compileO tok_l2a ctx $ \ty_l2a (TermO l2a) ->
 131                         compileO tok_r2a ctx $ \ty_r2a (TermO r2a) ->
 132                         check_type2 (ty @(->)) (At (Just tok_l2a) ty_l2a) $ \Refl ty_l2a_l ty_l2a_a ->
 133                         check_type2 (ty @(->)) (At (Just tok_r2a) ty_r2a) $ \Refl ty_r2a_r ty_r2a_a ->
 134                         check_type (At (Just tok_l2a) ty_l2a_a) (At (Just tok_r2a) ty_r2a_a) $ \Refl ->
 135                         k ((ty @Either :$ ty_l2a_l) :$ ty_r2a_r ~> ty_l2a_a) $ TermO $
 136                          \c -> lam $ either (l2a c) (r2a c)