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 qualified Control.Applicative as Alternative
   8 import Control.Monad (liftM2)
   9 import qualified Data.Function as Fun
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Prelude hiding (Functor(..), (<$>), id, const)
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Parsing.Grammar hiding (Alter(..))
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling
  18 import Language.Symantic.Lib.Lambda
  19 import Language.Symantic.Lib.Functor (Sym_Functor(..))
  20 import Language.Symantic.Interpreting
  21 import Language.Symantic.Transforming.Trans
  22
  23 -- * Class 'Sym_Alternative'
  24 class Sym_Functor term => Sym_Alternative term where
  25         empty :: Alternative f => term (f a)
  26         (<|>) :: Alternative f => term (f a) -> term (f a) -> term (f a)
  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 infixl 3 <|>
  36
  37 type instance Sym_of_Iface (Proxy Alternative) = Sym_Alternative
  38 type instance Consts_of_Iface (Proxy Alternative) = Proxy Alternative ': Consts_imported_by Alternative
  39 type instance Consts_imported_by Alternative = '[]
  40
  41 instance Sym_Alternative HostI where
  42         empty = HostI Alternative.empty
  43         (<|>) = liftM2 (Alternative.<|>)
  44 instance Sym_Alternative TextI where
  45         empty = textI0 "empty"
  46         (<|>) = textI_infix "<|>" (infixL 3)
  47 instance (Sym_Alternative r1, Sym_Alternative r2) => Sym_Alternative (DupI r1 r2) where
  48         empty = dupI0 (Proxy @Sym_Alternative) empty
  49         (<|>) = dupI2 (Proxy @Sym_Alternative) (<|>)
  50
  51 instance
  52  ( Read_TypeNameR Type_Name cs rs
  53  , Inj_Const cs Alternative
  54  ) => Read_TypeNameR Type_Name cs (Proxy Alternative ': rs) where
  55         read_typenameR _cs (Type_Name "Alternative") k = k (ty @Alternative)
  56         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  57 instance Show_Const cs => Show_Const (Proxy Alternative ': cs) where
  58         show_const ConstZ{} = "Alternative"
  59         show_const (ConstS c) = show_const c
  60
  61 instance Proj_ConC cs (Proxy Alternative)
  62 data instance TokenT meta (ts::[*]) (Proxy Alternative)
  63  = Token_Term_Alternative_empty (EToken meta '[Proxy Token_Type]) (EToken meta '[Proxy Token_Type])
  64  | Token_Term_Alternative_alt   (EToken meta ts)
  65 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Alternative))
  66 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Alternative))
  67 instance -- CompileI
  68  ( Read_TypeName Type_Name (Consts_of_Ifaces is)
  69  , Inj_Const  (Consts_of_Ifaces is) Alternative
  70  , Inj_Const  (Consts_of_Ifaces is) (->)
  71  , Proj_Con   (Consts_of_Ifaces is)
  72  , Compile is
  73  ) => CompileI is (Proxy Alternative) where
  74         compileI tok ctx k =
  75                 case tok of
  76                  Token_Term_Alternative_empty tok_ty_f tok_ty_a ->
  77                         -- empty :: Alternative f => f a
  78                         compile_type tok_ty_f $ \(ty_f::Type (Consts_of_Ifaces is) f) ->
  79                         compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
  80                         check_kind
  81                          (At Nothing $ SKiType `SKiArrow` SKiType)
  82                          (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
  83                         check_con (At (Just tok_ty_f) (ty @Alternative :$ ty_f)) $ \Con ->
  84                         check_kind
  85                          (At Nothing $ SKiType)
  86                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
  87                         k (ty_f :$ ty_a) $ TermO $
  88                          Fun.const empty
  89                  Token_Term_Alternative_alt tok_fl ->
  90                         -- (<|>) :: Alternative f => f a -> f a -> f a
  91                         compileO tok_fl ctx $ \ty_fa (TermO fl) ->
  92                         check_con1 (ty @Alternative)
  93                          (At (Just tok_fl) ty_fa) $ \Refl Con _ty_f _ty_a ->
  94                         k (ty_fa ~> ty_fa) $ TermO $
  95                          \c -> lam $ \fr -> (<|>) (fl c) fr
  96 instance -- TokenizeT
  97  Inj_Token meta ts Alternative =>
  98  TokenizeT meta ts (Proxy Alternative) where
  99         tokenizeT _t = mempty
 100          { tokenizers_infix = tokenizeTMod []
 101                  [ (Term_Name "empty",) Term_ProTok
 102                          { term_protok = \meta -> ProTokPi $ \f -> ProTokPi $ \a ->
 103                                 ProTok $ inj_etoken meta $ Token_Term_Alternative_empty f a
 104                          , term_fixity = infixN5
 105                          }
 106                  , tokenize1 "<|>" (infixL 3) Token_Term_Alternative_alt
 107                  ]
 108          }
 109 instance Gram_Term_AtomsT meta ts (Proxy Alternative) g