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

import Control.Monad
import qualified Data.Function as Fun
import qualified Data.Maybe as Maybe
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (maybe)

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

-- * 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 Maybe
type instance TyConsts_imported_by Maybe =
 [ Proxy Applicative
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , 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_TyConC
 ( Proj_TyConst cs Maybe
 , Proj_TyConsts cs (TyConsts_imported_by 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
		 _ -> 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) $ TermO $
				Fun.const _Nothing
		 Token_Term_Maybe_Just tok_a ->
			-- Just :: a -> Maybe a
			compileO tok_a ctx $ \ty_a (TermO a) ->
			k (ty @Maybe :$ ty_a) $ TermO $
			 \c -> _Just (a c)
		 Token_Term_Maybe_maybe tok_b tok_a2b ->
			-- maybe :: b -> (a -> b) -> Maybe a -> b
			compileO tok_b   ctx $ \ty_b   (TermO b) ->
			compileO tok_a2b ctx $ \ty_a2b (TermO 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) $ TermO $
			 \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 ->
				ProTok $ 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