{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Alternative'. module Language.Symantic.Lib.Alternative where import Control.Applicative (Alternative) import Control.Monad (liftM2) import Data.Proxy import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (Functor(..), (<$>), id, const) import qualified Control.Applicative as Alternative import qualified Data.Function as Fun import Language.Symantic.Parsing hiding (Alter(..)) import Language.Symantic.Typing import Language.Symantic.Compiling import Language.Symantic.Lib.Lambda import Language.Symantic.Lib.Functor (Sym_Functor(..)) import Language.Symantic.Interpreting import Language.Symantic.Transforming -- * Class 'Sym_Alternative' class Sym_Functor term => Sym_Alternative term where empty :: Alternative f => term (f a) (<|>) :: Alternative f => term (f a) -> term (f a) -> term (f a) infixl 3 <|> default empty :: (Trans t term, Alternative f) => t term (f a) default (<|>) :: (Trans t term, Alternative f) => t term (f a) -> t term (f a) -> t term (f a) empty = trans_lift empty (<|>) = trans_map2 (<|>) type instance Sym_of_Iface (Proxy Alternative) = Sym_Alternative type instance TyConsts_of_Iface (Proxy Alternative) = Proxy Alternative ': TyConsts_imported_by (Proxy Alternative) type instance TyConsts_imported_by (Proxy Alternative) = '[] instance Sym_Alternative HostI where empty = HostI Alternative.empty (<|>) = liftM2 (Alternative.<|>) instance Sym_Alternative TextI where empty = textI0 "empty" (<|>) = textI_infix "<|>" (infixL 3) instance (Sym_Alternative r1, Sym_Alternative r2) => Sym_Alternative (DupI r1 r2) where empty = dupI0 @Sym_Alternative empty (<|>) = dupI2 @Sym_Alternative (<|>) instance ( Read_TyNameR TyName cs rs , Inj_TyConst cs Alternative ) => Read_TyNameR TyName cs (Proxy Alternative ': rs) where read_TyNameR _cs (TyName "Alternative") k = k (ty @Alternative) read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k instance Show_TyConst cs => Show_TyConst (Proxy Alternative ': cs) where show_TyConst TyConstZ{} = "Alternative" show_TyConst (TyConstS c) = show_TyConst c instance Proj_TyConC cs (Proxy Alternative) data instance TokenT meta (ts::[*]) (Proxy Alternative) = Token_Term_Alternative_empty (EToken meta '[Proxy Token_Type]) (EToken meta '[Proxy Token_Type]) | Token_Term_Alternative_alt (EToken meta ts) deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Alternative)) deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Alternative)) instance -- CompileI ( Read_TyName TyName cs , Inj_TyConst cs Alternative , Inj_TyConst cs (->) , Proj_TyCon cs , Compile cs is ) => CompileI cs is (Proxy Alternative) where compileI tok ctx k = case tok of Token_Term_Alternative_empty tok_ty_f tok_ty_a -> -- empty :: Alternative f => f a compile_Type tok_ty_f $ \(ty_f::Type cs f) -> compile_Type tok_ty_a $ \(ty_a::Type cs a) -> check_Kind (At Nothing $ SKiType `SKiArrow` SKiType) (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl -> check_TyCon (At (Just tok_ty_f) (ty @Alternative :$ ty_f)) $ \TyCon -> check_Kind (At Nothing $ SKiType) (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl -> k (ty_f :$ ty_a) $ Term $ Fun.const empty Token_Term_Alternative_alt tok_fl -> -- (<|>) :: Alternative f => f a -> f a -> f a compile tok_fl ctx $ \ty_fa (Term fl) -> check_TyCon1 (ty @Alternative) (At (Just tok_fl) ty_fa) $ \Refl TyCon _ty_f _ty_a -> k (ty_fa ~> ty_fa) $ Term $ \c -> lam $ \fr -> (<|>) (fl c) fr instance -- TokenizeT Inj_Token meta ts Alternative => TokenizeT meta ts (Proxy Alternative) where tokenizeT _t = mempty { tokenizers_infix = tokenizeTMod [] [ (TeName "empty",) ProTok_Term { protok_term = \meta -> ProTokPi $ \f -> ProTokPi $ \a -> ProTok $ inj_EToken meta $ Token_Term_Alternative_empty f a , protok_fixity = infixN5 } , tokenize1 "<|>" (infixL 3) Token_Term_Alternative_alt ] } instance Gram_Term_AtomsT meta ts (Proxy Alternative) g