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

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

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * 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 Consts_of_Iface (Proxy Maybe) = Proxy Maybe ': Consts_imported_by Maybe
type instance Consts_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 = textI_app0 "Nothing"
	_Just    = textI_app1 "Just"
	maybe    = textI_app3 "maybe"
instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
	_Nothing = dupI0 (Proxy @Sym_Maybe) _Nothing
	_Just    = dupI1 (Proxy @Sym_Maybe) _Just
	maybe    = dupI3 (Proxy @Sym_Maybe) maybe

instance Const_from Text cs => Const_from Text (Proxy Maybe ': cs) where
	const_from "Maybe" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy Maybe ': cs) where
	show_const ConstZ{} = "Maybe"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 ( Proj_Const cs Maybe
 , Proj_Consts cs (Consts_imported_by Maybe)
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy Maybe) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy Maybe)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
		 _ -> Nothing
	proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy Maybe)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monoid)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Show)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		 _ -> Nothing
	proj_conC _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 -- Term_fromI
 ( Const_from Name_LamVar (Consts_of_Ifaces is)
 , Inj_Const  (Consts_of_Ifaces is) Maybe
 , Inj_Const  (Consts_of_Ifaces is) (->)
 , Term_from is
 ) => Term_fromI is (Proxy Maybe) where
	term_fromI tok ctx k =
		case tok of
		 Token_Term_Maybe_Nothing tok_ty_a ->
			-- Nothing :: Maybe a
			type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
			check_kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			k (ty @Maybe :$ ty_a) $ TermLC $
				Fun.const _Nothing
		 Token_Term_Maybe_Just tok_a ->
			-- Just :: a -> Maybe a
			term_from tok_a ctx $ \ty_a (TermLC a) ->
			k (ty @Maybe :$ ty_a) $ TermLC $
			 \c -> _Just (a c)
		 Token_Term_Maybe_maybe tok_b tok_a2b ->
			-- maybe :: b -> (a -> b) -> Maybe a -> b
			term_from tok_b   ctx $ \ty_b   (TermLC b) ->
			term_from tok_a2b ctx $ \ty_a2b (TermLC a2b) ->
			check_type2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
			check_type
			 (At (Just tok_a2b) ty_a2b_b)
			 (At (Just tok_b) ty_b) $ \Refl ->
			k (ty @Maybe :$ ty_a2b_a ~> ty_b) $ TermLC $
			 \c -> lam $ maybe (b c) (a2b c)