{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
-- | Symantic for 'Maybe'.
module Language.Symantic.Lib.Maybe where

import Control.Monad
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (maybe)
import qualified Data.Function as Fun
import qualified Data.Maybe as Maybe
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.Lib.MonoFunctor (TyFam_MonoElement(..))

-- * Class 'Sym_Maybe_Lam'
class Sym_Maybe term where
	_Nothing :: term (Maybe a)
	_Just    :: term a -> term (Maybe a)
	maybe    :: term b -> term (a -> b) -> term (Maybe a) -> term b
	
	default _Nothing :: Trans t term => t term (Maybe a)
	default _Just    :: Trans t term => t term a -> t term (Maybe a)
	default maybe    :: Trans t term => t term b -> t term (a -> b) -> t term (Maybe a) -> t term b
	
	_Nothing = trans_lift _Nothing
	_Just    = trans_map1 _Just
	maybe    = trans_map3 maybe

type instance Sym_of_Iface (Proxy Maybe) = Sym_Maybe
type instance TyConsts_of_Iface (Proxy Maybe) = Proxy Maybe ': TyConsts_imported_by (Proxy Maybe)
type instance TyConsts_imported_by (Proxy Maybe) =
 [ Proxy Applicative
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy MT.MonoFoldable
 , Proxy MT.MonoFunctor
 , Proxy Monoid
 , Proxy Show
 , Proxy Traversable
 ]

instance Sym_Maybe HostI where
	_Nothing = HostI Nothing
	_Just    = liftM Just
	maybe    = liftM3 Maybe.maybe
instance Sym_Maybe TextI where
	_Nothing = textI0 "Nothing"
	_Just    = textI1 "Just"
	maybe    = textI3 "maybe"
instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
	_Nothing = dupI0 @Sym_Maybe _Nothing
	_Just    = dupI1 @Sym_Maybe _Just
	maybe    = dupI3 @Sym_Maybe maybe

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Maybe
 ) => Read_TyNameR TyName cs (Proxy Maybe ': rs) where
	read_TyNameR _cs (TyName "Maybe") k = k (ty @Maybe)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Maybe ': cs) where
	show_TyConst TyConstZ{} = "Maybe"
	show_TyConst (TyConstS c) = show_TyConst c

instance -- Proj_TyFamC TyFam_MonoElement
 ( Proj_TyConst cs Maybe
 ) => Proj_TyFamC cs TyFam_MonoElement Maybe where
	proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Maybe)
	 = Just ty_a
	proj_TyFamC _c _fam _ty = Nothing

instance -- Proj_TyConC
 ( Proj_TyConst cs Maybe
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Maybe))
 , Proj_TyCon cs
 ) => Proj_TyConC cs (Proxy Maybe) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Maybe)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Foldable)    -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Maybe)
	 = case () of
		 _ | Just Refl  <- proj_TyConst q (Proxy @Eq)
		   , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monoid)
		   , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show)
		   , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor)  -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy Maybe)
 = Token_Term_Maybe_Nothing (EToken meta '[Proxy Token_Type])
 | Token_Term_Maybe_Just    (EToken meta ts)
 | Token_Term_Maybe_maybe   (EToken meta ts) (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Maybe))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Maybe))

instance -- CompileI
 ( Read_TyName TyName cs
 , Inj_TyConst        cs Maybe
 , Inj_TyConst        cs (->)
 , Compile cs is
 ) => CompileI cs is (Proxy Maybe) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Maybe_Nothing tok_ty_a ->
			-- Nothing :: Maybe a
			compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
			check_Kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			k (ty @Maybe :$ ty_a) $ Term $
				Fun.const _Nothing
		 Token_Term_Maybe_Just tok_a ->
			-- Just :: a -> Maybe a
			compile tok_a ctx $ \ty_a (Term a) ->
			k (ty @Maybe :$ ty_a) $ Term $
			 \c -> _Just (a c)
		 Token_Term_Maybe_maybe tok_b tok_a2b ->
			-- maybe :: b -> (a -> b) -> Maybe a -> b
			compile tok_b   ctx $ \ty_b   (Term b) ->
			compile tok_a2b ctx $ \ty_a2b (Term a2b) ->
			check_TyEq2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
			check_TyEq
			 (At (Just tok_a2b) ty_a2b_b)
			 (At (Just tok_b) ty_b) $ \Refl ->
			k (ty @Maybe :$ ty_a2b_a ~> ty_b) $ Term $
			 \c -> lam $ maybe (b c) (a2b c)
instance
 Inj_Token meta ts Maybe =>
 TokenizeT meta ts (Proxy Maybe) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ (TeName "Nothing",) ProTok_Term
			 { protok_term = \meta -> ProTokPi $ \a ->
				ProTokTe $ inj_EToken meta $ Token_Term_Maybe_Nothing a
			 , protok_fixity = infixN5
			 }
		 , tokenize1 "Just" infixN5 Token_Term_Maybe_Just
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Maybe) g