{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
-- | Symantic for 'Either'.
module Language.Symantic.Lib.Either where
-import Control.Monad (liftM, liftM3)
-import qualified Data.Either as Either
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (either)
+import qualified Data.Either as Either
+import qualified Data.MonoTraversable as MT
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
+import Language.Symantic
+import Language.Symantic.Lib.MonoFunctor (Element)
+import Language.Symantic.Lib.Function (a0, b1, c2)
--- * Class 'Sym_Tuple'
+-- * Class 'Sym_Either'
+type instance Sym Either = Sym_Either
class Sym_Either term where
_Left :: term l -> term (Either l r)
_Right :: term r -> term (Either l r)
either :: term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
- default _Left :: Trans t term => t term l -> t term (Either l r)
- default _Right :: Trans t term => t term r -> t term (Either l r)
- default either :: Trans t term => t term (l -> a) -> t term (r -> a) -> t term (Either l r) -> t term a
- _Left = trans_map1 _Left
- _Right = trans_map1 _Right
- either = trans_map3 either
+
+ default _Left :: Sym_Either (UnT term) => Trans term => term l -> term (Either l r)
+ default _Right :: Sym_Either (UnT term) => Trans term => term r -> term (Either l r)
+ default either :: Sym_Either (UnT term) => Trans term => term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
+
+ _Left = trans1 _Left
+ _Right = trans1 _Right
+ either = trans3 either
-type instance Sym_of_Iface (Proxy Either) = Sym_Either
-type instance TyConsts_of_Iface (Proxy Either) = Proxy Either ': TyConsts_imported_by Either
-type instance TyConsts_imported_by Either =
- [ Proxy (->)
- , Proxy Applicative
- , Proxy Eq
- , Proxy Foldable
- , Proxy Functor
- , Proxy Monad
- , Proxy Ord
- , Proxy Show
- , Proxy Traversable
- ]
+-- Interpreting
+instance Sym_Either Eval where
+ _Right = eval1 Right
+ _Left = eval1 Left
+ either = eval3 Either.either
+instance Sym_Either View where
+ _Right = view1 "Right"
+ _Left = view1 "Left"
+ either = view3 "either"
+instance (Sym_Either r1, Sym_Either r2) => Sym_Either (Dup r1 r2) where
+ _Left = dup1 @Sym_Either _Left
+ _Right = dup1 @Sym_Either _Right
+ either = dup3 @Sym_Either either
-instance Sym_Either HostI where
- _Right = liftM Right
- _Left = liftM Left
- either = liftM3 Either.either
-instance Sym_Either TextI where
- _Right = textI1 "Right"
- _Left = textI1 "Left"
- either = textI3 "either"
-instance (Sym_Either r1, Sym_Either r2) => Sym_Either (DupI r1 r2) where
- _Left = dupI1 (Proxy @Sym_Either) _Left
- _Right = dupI1 (Proxy @Sym_Either) _Right
- either = dupI3 (Proxy @Sym_Either) either
+-- Transforming
+instance (Sym_Either term, Sym_Lambda term) => Sym_Either (BetaT term)
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Either
- ) => Read_TyNameR TyName cs (Proxy Either ': rs) where
- read_TyNameR _cs (TyName "Either") k = k (ty @Either)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Either ': cs) where
- show_TyConst TyConstZ{} = "Either"
- show_TyConst (TyConstS c) = show_TyConst c
-instance -- Proj_TyConC
- ( Proj_TyConst cs Either
- , Proj_TyConsts cs (TyConsts_imported_by Either)
- , Proj_TyCon cs
- ) => Proj_TyConC cs (Proxy Either) where
- proj_TyConC _ (TyConst q :$ (TyConst c :$ _l))
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @Either)
+-- Typing
+instance NameTyOf Either where
+ nameTyOf _c = ["Either"] `Mod` "Either"
+instance FixityOf Either
+instance ClassInstancesFor Either where
+ proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _l))
+ | Just HRefl <- proj_ConstKiTy @_ @Either c
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Monad) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
+ _ | Just Refl <- proj_Const @Functor q -> Just Dict
+ | Just Refl <- proj_Const @Applicative q -> Just Dict
+ | Just Refl <- proj_Const @Monad q -> Just Dict
+ | Just Refl <- proj_Const @Foldable q -> Just Dict
+ | Just Refl <- proj_Const @Traversable q -> Just Dict
_ -> Nothing
- proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ l :$ r))
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @Either)
+ proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c l) r))
+ | Just HRefl <- proj_ConstKiTy @_ @Either c
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Eq)
- , Just TyCon <- proj_TyCon (t :$ l)
- , Just TyCon <- proj_TyCon (t :$ r) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Ord)
- , Just TyCon <- proj_TyCon (t :$ l)
- , Just TyCon <- proj_TyCon (t :$ r) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Show)
- , Just TyCon <- proj_TyCon (t :$ l)
- , Just TyCon <- proj_TyCon (t :$ r) -> Just TyCon
+ _ | Just Refl <- proj_Const @Eq q
+ , Just Dict <- proveConstraint (tq `tyApp` l)
+ , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
+ | Just Refl <- proj_Const @Ord q
+ , Just Dict <- proveConstraint (tq `tyApp` l)
+ , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
+ | Just Refl <- proj_Const @Show q
+ , Just Dict <- proveConstraint (tq `tyApp` l)
+ , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
+ | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
+ | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
_ -> Nothing
- proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy Either)
- = Token_Term_Either_Left (EToken meta '[Proxy Token_Type]) (EToken meta ts)
- | Token_Term_Either_Right (EToken meta '[Proxy Token_Type]) (EToken meta ts)
- | Token_Term_Either_either (EToken meta ts) (EToken meta ts)
-deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Either))
-deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Either))
-instance -- CompileI
- ( Read_TyName TyName (TyConsts_of_Ifaces is)
- , Inj_TyConst (TyConsts_of_Ifaces is) Either
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- -- , Proj_Token is Token_Type
- , Compile is
- ) => CompileI is (Proxy Either) where
- compileI tok ctx k =
- case tok of
- Token_Term_Either_Left tok_ty_r tok_l ->
- -- Left :: l -> Either l r
- compile_Type tok_ty_r $ \(ty_r::Type (TyConsts_of_Ifaces is) r) ->
- check_Kind
- (At Nothing SKiType)
- (At (Just tok_ty_r) $ kind_of ty_r) $ \Refl ->
- compileO tok_l ctx $ \ty_l (TermO l) ->
- k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
- \c -> _Left (l c)
- Token_Term_Either_Right tok_ty_l tok_r ->
- -- Right :: r -> Either l r
- compile_Type tok_ty_l $ \(ty_l::Type (TyConsts_of_Ifaces is) l) ->
- check_Kind
- (At Nothing SKiType)
- (At (Just tok_ty_l) $ kind_of ty_l) $ \Refl ->
- compileO tok_r ctx $ \ty_r (TermO r) ->
- k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
- \c -> _Right (r c)
- Token_Term_Either_either tok_l2a tok_r2a ->
- -- either :: (l -> a) -> (r -> a) -> Either l r -> a
- compileO tok_l2a ctx $ \ty_l2a (TermO l2a) ->
- compileO tok_r2a ctx $ \ty_r2a (TermO r2a) ->
- check_TyEq2 (ty @(->)) (At (Just tok_l2a) ty_l2a) $ \Refl ty_l2a_l ty_l2a_a ->
- check_TyEq2 (ty @(->)) (At (Just tok_r2a) ty_r2a) $ \Refl ty_r2a_r ty_r2a_a ->
- check_TyEq (At (Just tok_l2a) ty_l2a_a) (At (Just tok_r2a) ty_r2a_a) $ \Refl ->
- k ((ty @Either :$ ty_l2a_l) :$ ty_r2a_r ~> ty_l2a_a) $ TermO $
- \c -> lam $ either (l2a c) (r2a c)
-instance -- TokenizeT
- Inj_Token meta ts Either =>
- TokenizeT meta ts (Proxy Either) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ (Term_Name "Left",) Term_ProTok
- { term_protok = \meta -> ProTokLam $ \l -> ProTokPi $ \r ->
- ProTok $ inj_EToken meta $ Token_Term_Either_Left r l
- , term_fixity = infixN5 }
- , (Term_Name "Right",) Term_ProTok
- { term_protok = \meta -> ProTokPi $ \l -> ProTokLam $ \r ->
- ProTok $ inj_EToken meta $ Token_Term_Either_Right l r
- , term_fixity = infixN5 }
- , tokenize2 "either" infixN5 Token_Term_Either_either
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Either) g
+ proveConstraintFor _c _q = Nothing
+instance TypeInstancesFor Either where
+ expandFamFor _c _len f (TyApp _ (TyApp _ c _ty_l) r `TypesS` TypesZ)
+ | Just HRefl <- proj_ConstKi @_ @Element f
+ , Just HRefl <- proj_ConstKiTy @_ @Either c
+ = Just r
+ expandFamFor _c _len _fam _as = Nothing
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Either
+instance (Source src, SymInj ss Either) => ModuleFor src ss Either where
+ moduleFor = ["Either"] `moduleWhere`
+ [ "Left" := teEither_Left
+ , "Right" := teEither_Right
+ , "either" := teEither_either
+ ]
+
+-- ** 'Type's
+tyEither :: Source src => Type src vs l -> Type src vs r -> Type src vs (Either l r)
+tyEither l r = tyConstLen @(K Either) @Either (lenVars l) `tyApp` l `tyApp` r
+
+-- ** 'Term's
+teEither_Left :: TermDef Either '[Proxy a, Proxy b] (() #> (a -> Either a b))
+teEither_Left = Term noConstraint (a0 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Left
+teEither_Right :: TermDef Either '[Proxy a, Proxy b] (() #> (b -> Either a b))
+teEither_Right = Term noConstraint (b1 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Right
+teEither_either :: TermDef Either '[Proxy a, Proxy b, Proxy c] (() #> ((a -> c) -> (b -> c) -> Either a b -> c))
+teEither_either = Term noConstraint ((a0 ~> c2) ~> (b1 ~> c2) ~> tyEither a0 b1 ~> c2) $ teSym @Either $ lam3 either
sourcephile / git / haskell / symantic.git / blobdiff