symantic-lib/Language/Symantic/Lib/Alternative.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Alternative'.
   4 module Language.Symantic.Lib.Alternative where
   5
   6 import Control.Applicative (Alternative)
   7 import Control.Monad (liftM2)
   8 import Data.Proxy
   9 import Data.Type.Equality ((:~:)(Refl))
  10 import Prelude hiding (Functor(..), (<$>), id, const)
  11 import qualified Control.Applicative as Alternative
  12 import qualified Data.Function as Fun
  13
  14 import Language.Symantic.Parsing hiding (Alter(..))
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling
  17 import Language.Symantic.Lib.Lambda
  18 import Language.Symantic.Lib.Functor (Sym_Functor(..))
  19 import Language.Symantic.Interpreting
  20 import Language.Symantic.Transforming
  21
  22 -- * Class 'Sym_Alternative'
  23 class Sym_Functor term => Sym_Alternative term where
  24         empty :: Alternative f => term (f a)
  25         (<|>) :: Alternative f => term (f a) -> term (f a) -> term (f a)
  26         infixl 3 <|>
  27
  28         default empty :: (Trans t term, Alternative f) => t term (f a)
  29         default (<|>) :: (Trans t term, Alternative f)
  30          => t term (f a) -> t term (f a) -> t term (f a)
  31
  32         empty = trans_lift empty
  33         (<|>) = trans_map2 (<|>)
  34
  35 type instance Sym_of_Iface (Proxy Alternative) = Sym_Alternative
  36 type instance TyConsts_of_Iface (Proxy Alternative) = Proxy Alternative ': TyConsts_imported_by (Proxy Alternative)
  37 type instance TyConsts_imported_by (Proxy Alternative) = '[]
  38
  39 instance Sym_Alternative HostI where
  40         empty = HostI Alternative.empty
  41         (<|>) = liftM2 (Alternative.<|>)
  42 instance Sym_Alternative TextI where
  43         empty = textI0 "empty"
  44         (<|>) = textI_infix "<|>" (infixL 3)
  45 instance (Sym_Alternative r1, Sym_Alternative r2) => Sym_Alternative (DupI r1 r2) where
  46         empty = dupI0 @Sym_Alternative empty
  47         (<|>) = dupI2 @Sym_Alternative (<|>)
  48
  49 instance
  50  ( Read_TyNameR TyName cs rs
  51  , Inj_TyConst cs Alternative
  52  ) => Read_TyNameR TyName cs (Proxy Alternative ': rs) where
  53         read_TyNameR _cs (TyName "Alternative") k = k (ty @Alternative)
  54         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  55 instance Show_TyConst cs => Show_TyConst (Proxy Alternative ': cs) where
  56         show_TyConst TyConstZ{} = "Alternative"
  57         show_TyConst (TyConstS c) = show_TyConst c
  58
  59 instance Proj_TyConC cs (Proxy Alternative)
  60 data instance TokenT meta (ts::[*]) (Proxy Alternative)
  61  = Token_Term_Alternative_empty (EToken meta '[Proxy Token_Type]) (EToken meta '[Proxy Token_Type])
  62  | Token_Term_Alternative_alt   (EToken meta ts)
  63 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Alternative))
  64 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Alternative))
  65
  66 instance -- CompileI
  67  ( Read_TyName TyName cs
  68  , Inj_TyConst        cs Alternative
  69  , Inj_TyConst        cs (->)
  70  , Proj_TyCon         cs
  71  , Compile cs is
  72  ) => CompileI cs is (Proxy Alternative) where
  73         compileI tok ctx k =
  74                 case tok of
  75                  Token_Term_Alternative_empty tok_ty_f tok_ty_a ->
  76                         -- empty :: Alternative f => f a
  77                         compile_Type tok_ty_f $ \(ty_f::Type cs f) ->
  78                         compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
  79                         check_Kind
  80                          (At Nothing $ SKiType `SKiArrow` SKiType)
  81                          (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
  82                         check_TyCon (At (Just tok_ty_f) (ty @Alternative :$ ty_f)) $ \TyCon ->
  83                         check_Kind
  84                          (At Nothing $ SKiType)
  85                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
  86                         k (ty_f :$ ty_a) $ Term $
  87                          Fun.const empty
  88                  Token_Term_Alternative_alt tok_fl ->
  89                         -- (<|>) :: Alternative f => f a -> f a -> f a
  90                         compile tok_fl ctx $ \ty_fa (Term fl) ->
  91                         check_TyCon1 (ty @Alternative)
  92                          (At (Just tok_fl) ty_fa) $ \Refl TyCon _ty_f _ty_a ->
  93                         k (ty_fa ~> ty_fa) $ Term $
  94                          \c -> lam $ \fr -> (<|>) (fl c) fr
  95 instance -- TokenizeT
  96  Inj_Token meta ts Alternative =>
  97  TokenizeT meta ts (Proxy Alternative) where
  98         tokenizeT _t = mempty
  99          { tokenizers_infix = tokenizeTMod []
 100                  [ (TeName "empty",) ProTok_Term
 101                          { protok_term = \meta -> ProTokPi $ \f -> ProTokPi $ \a ->
 102                                 ProTok $ inj_EToken meta $ Token_Term_Alternative_empty f a
 103                          , protok_fixity = infixN5
 104                          }
 105                  , tokenize1 "<|>" (infixL 3) Token_Term_Alternative_alt
 106                  ]
 107          }
 108 instance Gram_Term_AtomsT meta ts (Proxy Alternative) g