{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
-- | Expression for 'Maybe'.
module Language.LOL.Symantic.Expr.Maybe where

import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (maybe)
import Language.LOL.Symantic.Type
import Language.LOL.Symantic.Repr.Dup
import Language.LOL.Symantic.Trans.Common
import Language.LOL.Symantic.Expr.Common
import Language.LOL.Symantic.Expr.Lambda
import Language.LOL.Symantic.Expr.Bool

-- * Class 'Sym_Maybe'

class Sym_Maybe lam repr where
	maybe
	 :: repr b
	 -> repr (Lambda lam a b)
	 -> repr (Maybe a)
	 -> repr b
	
	default maybe
	 :: Trans t repr
	 => t repr b
	 -> t repr (Lambda lam a b)
	 -> t repr (Maybe a)
	 -> t repr b
	maybe = trans_map3 maybe
class Sym_Maybe_Cons repr where
	nothing :: repr (Maybe a)
	just    :: repr a -> repr (Maybe a)
	
	default nothing :: Trans t repr => t repr (Maybe a)
	default just    :: Trans t repr => t repr a -> t repr (Maybe a)
	nothing = trans_lift nothing
	just    = trans_map1 just

instance -- Sym_Maybe Dup
 ( Sym_Maybe lam r1
 , Sym_Maybe lam r2
 ) => Sym_Maybe lam (Dup r1 r2) where
	maybe (m1 `Dup` m2) (n1 `Dup` n2) (j1 `Dup` j2) =
		maybe m1 n1 j1 `Dup` maybe m2 n2 j2
instance -- Sym_Maybe_Cons Dup
 ( Sym_Maybe_Cons r1
 , Sym_Maybe_Cons r2
 ) => Sym_Maybe_Cons (Dup r1 r2) where
	nothing = nothing `Dup` nothing
	just (a1 `Dup` a2) = just a1 `Dup` just a2

-- * Type 'Expr_Maybe'
-- | Expression.
data Expr_Maybe (lam:: * -> *) (root:: *)
type instance Root_of_Expr      (Expr_Maybe lam root)      = root
type instance Type_of_Expr      (Expr_Maybe lam root)      = Type_Maybe
type instance Sym_of_Expr       (Expr_Maybe lam root) repr = (Sym_Maybe lam repr, Sym_Maybe_Cons repr)
type instance Error_of_Expr ast (Expr_Maybe lam root)      = No_Error_Expr

maybe_from
 :: forall root lam ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
 , Type_Eq (Type_Root_of_Expr root)
 , Expr_from ast root
 , Type_Root_Lift (Type_Fun lam) (Type_Root_of_Expr root)
 , Type_Root_Lift Type_Maybe (Type_Root_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
 , Type_Unlift Type_Maybe     (Type_of_Expr root)
 , Root_of_Expr root ~ root
 ) => ast -> ast -> ast
 -> Expr_From ast (Expr_Maybe lam root) hs ret
maybe_from ast_n ast_j ast_m px_ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_n ctx $
	 \(ty_n::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context n) ->
	expr_from (Proxy::Proxy root) ast_j ctx $
	 \(ty_j::Type_Root_of_Expr root h_j) (Forall_Repr_with_Context j) ->
	expr_from (Proxy::Proxy root) ast_m ctx $
	 \(ty_m::Type_Root_of_Expr root h_m) (Forall_Repr_with_Context m) ->
		case type_unlift $ unType_Root ty_j of
		 Nothing -> Left $
			error_expr px_ex $
			Error_Expr_Type_mismatch ast
			 (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
			 :: Type_Root_of_Expr (Expr_Maybe lam root) (lam Zero -> lam (Succ Zero))))
			 (Exists_Type ty_m)
		 Just (ty_j_a `Type_Fun` ty_j_b
		  :: Type_Fun lam (Type_Root_of_Expr root) h_j) ->
			case type_unlift $ unType_Root ty_m of
			 Nothing -> Left $
				error_expr px_ex $
				Error_Expr_Type_mismatch ast
				 (Exists_Type (type_maybe $ type_var SZero
				 :: Type_Root_of_Expr (Expr_Maybe lam root) (Maybe Zero)))
				 (Exists_Type ty_m)
			 Just (Type_Maybe ty_m_a
				:: Type_Maybe (Type_Root_of_Expr root) h_m) ->
				when_type_eq px_ex ast
				 ty_n ty_j_b $ \Refl ->
					when_type_eq px_ex ast
					 ty_m_a ty_j_a $ \Refl ->
						k ty_n $ Forall_Repr_with_Context $
						 \c -> maybe (n c) (j c) (m c)

nothing_from
 :: forall root lam ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
 , Type_from ast (Type_Root_of_Expr root)
 , Type_Root_Lift Type_Maybe (Type_Root_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> Expr_From ast (Expr_Maybe lam root) hs ret
nothing_from ast_ty_a px_ex ast _ctx k =
	case type_from
	 (Proxy::Proxy (Type_Root_of_Expr root))
	 ast_ty_a (Right . Exists_Type) of
	 Left err -> Left $ error_expr px_ex $ Error_Expr_Type err ast
	 Right (Exists_Type (ty_a::Type_Root_of_Expr root h_a)) ->
			k (type_maybe ty_a) $ Forall_Repr_with_Context $
				const nothing

just_from
 :: forall root lam ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
 , Expr_from ast root
 , Type_Root_Lift Type_Maybe (Type_Root_of_Expr root)
 , Root_of_Expr root ~ root
 ) => ast
 -> Expr_From ast (Expr_Maybe lam root) hs ret
just_from ast_a _px_ex _ast ctx k =
	expr_from (Proxy::Proxy root) ast_a ctx $
	 \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
		k (type_maybe ty_a) $ Forall_Repr_with_Context $
			\c -> just (a c)

-- ** Type 'Expr_Lambda_Maybe_Bool'
-- | Convenient alias.
type Expr_Lambda_Maybe_Bool lam
 =   Expr_Root (Expr_Alt (Expr_Lambda lam)
                         (Expr_Alt (Expr_Maybe lam)
                                    Expr_Bool))

-- | Convenient alias around 'expr_from'.
expr_lambda_maybe_bool_from
 :: forall lam ast root.
 ( Expr_from ast (Expr_Lambda_Maybe_Bool lam)
 , root ~ Expr_Lambda_Maybe_Bool lam
 ) => Proxy lam
 -> ast
 -> Either (Error_of_Expr ast root)
           (Exists_Type_and_Repr (Type_Root_of_Expr root)
                                 (Forall_Repr root))
expr_lambda_maybe_bool_from _px_lam ast =
	expr_from (Proxy::Proxy root) ast
	 Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
		Right $ Exists_Type_and_Repr ty $
			Forall_Repr $ repr Context_Empty