{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Expression for 'Maybe'.
module Language.Symantic.Expr.Maybe where

import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (maybe)

import Language.Symantic.Type
import Language.Symantic.Repr.Dup
import Language.Symantic.Trans.Common
import Language.Symantic.Expr.Common
import Language.Symantic.Expr.Lambda
import Language.Symantic.Expr.Functor
import Language.Symantic.Expr.Applicative

-- * Class 'Sym_Maybe_Lam'
-- | Symantic.
class Sym_Maybe 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
-- | Symantic requiring a 'Lambda'.
class Sym_Maybe_Lam 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

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

-- * 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 repr, Sym_Maybe_Lam lam repr)
type instance Error_of_Expr ast (Expr_Maybe lam root)      = No_Error_Expr

instance Constraint1_Type Functor_with_Lambda (Type_Type1 Maybe root) where
	constraint1_type _c (Type_Type1 _ _) = Just Dict
instance Constraint1_Type Applicative_with_Lambda (Type_Type1 Maybe root) where
	constraint1_type _c (Type_Type1 _ _) = Just Dict

-- | Parsing utility to check that the given type is a 'Type_Maybe'
-- or raise 'Error_Expr_Type_mismatch'.
check_type_maybe
 :: forall ast ex root ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Type_Lift   Type_Maybe (Type_of_Expr root)
 , Type_Unlift Type_Maybe (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy ex -> ast -> ty h
 -> (Type_Maybe ty h -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type_maybe ex ast ty k =
	case type_unlift $ unType_Root ty of
	 Just ty_l -> k ty_l
	 Nothing -> Left $
		error_expr ex $
		Error_Expr_Type_mismatch ast
		 (Exists_Type (type_maybe $ type_var SZero
		 :: Type_Root_of_Expr ex (Maybe Zero)))
		 (Exists_Type ty)

-- | Parse 'maybe'.
maybe_from
 :: forall root lam ty ty_root ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
 , ty_root ~ Type_of_Expr root
 , Eq_Type ty
 , Expr_from ast root
 , Type_Lift   (Type_Fun lam) ty_root
 , Type_Unlift (Type_Fun lam) ty_root
 , Type_Lift   Type_Maybe     ty_root
 , Type_Unlift Type_Maybe     ty_root
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast 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 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) ->
	check_type_fun ex ast ty_j $ \(ty_j_a `Type_Fun` ty_j_b
	 :: Type_Fun lam (Type_Root_of_Expr root) h_j) ->
	check_type_maybe ex ast ty_m $ \(Type_Type1 _ ty_m_a) ->
	check_eq_type ex ast ty_n   ty_j_b $ \Refl ->
	check_eq_type ex ast ty_m_a ty_j_a $ \Refl ->
		k ty_n $ Forall_Repr_with_Context $
		 \c -> maybe (n c) (j c) (m c)

-- | Parse 'nothing'.
nothing_from
 :: forall root lam ty ty_root ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
 , ty_root ~ Type_Root_of_Expr root
 , Type_from ast ty_root
 , Type_Root_Lift Type_Maybe ty_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 ex ast _ctx k =
	case type_from (Proxy::Proxy ty_root)
	 ast_ty_a (Right . Exists_Type) of
	 Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
	 Right (Exists_Type ty_a) ->
		k (type_maybe ty_a) $ Forall_Repr_with_Context $
			const nothing

-- | Parse 'just'.
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 _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)