{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Alternative'.
module Language.Symantic.Lib.Alternative where

import Control.Applicative (Alternative)
import qualified Control.Applicative as Alternative
import Control.Monad (liftM2)
import qualified Data.Function as Fun
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Functor(..), (<$>), id, const)

import Language.Symantic.Parsing
import Language.Symantic.Parsing.Grammar
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.Trans

-- * 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)
	
	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 (<|>)

infixl 3 <|>

type instance Sym_of_Iface (Proxy Alternative) = Sym_Alternative
type instance Consts_of_Iface (Proxy Alternative) = Proxy Alternative ': Consts_imported_by Alternative
type instance Consts_imported_by 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 (Proxy @Sym_Alternative) empty
	(<|>) = dupI2 (Proxy @Sym_Alternative) (<|>)

instance
 ( Read_TypeNameR Type_Name cs rs
 , Inj_Const cs Alternative
 ) => Read_TypeNameR Type_Name cs (Proxy Alternative ': rs) where
	read_typenameR _cs (Type_Name "Alternative") k = k (ty @Alternative)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Alternative ': cs) where
	show_const ConstZ{} = "Alternative"
	show_const (ConstS c) = show_const c

instance Proj_ConC 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_TypeName Type_Name (Consts_of_Ifaces is)
 , Inj_Const  (Consts_of_Ifaces is) Alternative
 , Inj_Const  (Consts_of_Ifaces is) (->)
 , Proj_Con   (Consts_of_Ifaces is)
 , Compile is
 ) => CompileI 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 (Consts_of_Ifaces is) f) ->
			compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
			check_kind
			 (At Nothing $ SKiType `SKiArrow` SKiType)
			 (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
			check_con (At (Just tok_ty_f) (ty @Alternative :$ ty_f)) $ \Con ->
			check_kind
			 (At Nothing $ SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			k (ty_f :$ ty_a) $ TermO $
			 Fun.const empty
		 Token_Term_Alternative_alt tok_fl ->
			-- (<|>) :: Alternative f => f a -> f a -> f a
			compileO tok_fl ctx $ \ty_fa (TermO fl) ->
			check_con1 (ty @Alternative)
			 (At (Just tok_fl) ty_fa) $ \Refl Con _ty_f _ty_a ->
			k (ty_fa ~> ty_fa) $ TermO $
			 \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 []
		 [ (Term_Name "empty",) Term_ProTok
			 { term_protok = \meta -> ProTokPi $ \f -> ProTokPi $ \a ->
				ProTok $ inj_etoken meta $ Token_Term_Alternative_empty f a
			 , term_fixity = infixN5
			 }
		 , tokenize1 "<|>" (infixL 3) Token_Term_Alternative_alt
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Alternative) g