{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
-- | Expression for @if@.
module Language.Symantic.Expr.If where

import qualified Control.Monad as Monad
import Data.Monoid
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))

import Language.Symantic.Type
import Language.Symantic.Repr
import Language.Symantic.Expr.Root
import Language.Symantic.Expr.Error
import Language.Symantic.Expr.From
import Language.Symantic.Trans.Common

-- * Class 'Sym_If'
-- | Symantic.
class Sym_If repr where
	if_  :: repr Bool -> repr a -> repr a -> repr a
	default if_ :: Trans t repr => t repr Bool -> t repr a -> t repr a -> t repr a
	if_  = trans_map3 if_
instance Sym_If Repr_Host where
	if_ (Repr_Host b) ok ko = if b then ok else ko
instance Sym_If Repr_Text where
	if_ (Repr_Text cond) (Repr_Text ok) (Repr_Text ko) =
		Repr_Text $ \p v ->
			let p' = Precedence 2 in
			paren p p' $
			"if " <> cond p' v <>
			" then " <> ok p' v <>
			" else " <> ko p' v

instance (Sym_If r1, Sym_If r2) => Sym_If (Repr_Dup r1 r2) where
	if_ = repr_dup3 sym_If if_

sym_If :: Proxy Sym_If
sym_If = Proxy

-- * Class 'Sym_When'
-- | Symantic.
class Sym_When repr where
	when :: repr Bool -> repr () -> repr ()
	default when :: Trans t repr => t repr Bool -> t repr () -> t repr ()
	when = trans_map2 when
instance Sym_When Repr_Host where
	when (Repr_Host b) = Monad.when b
instance Sym_When Repr_Text where
	when (Repr_Text cond) (Repr_Text ok) =
		Repr_Text $ \p v ->
			let p' = Precedence 2 in
			paren p p' $
			"when " <> cond p' v <>
			" " <> ok p' v
instance (Sym_When r1, Sym_When r2) => Sym_When (Repr_Dup r1 r2) where
	when = repr_dup2 sym_When when

sym_When :: Proxy Sym_When
sym_When = Proxy

-- * Type 'Expr_If'
-- | Expression.
data Expr_If (root:: *)
type instance Root_of_Expr      (Expr_If root)      = root
type instance Type_of_Expr      (Expr_If root)      = No_Type
type instance Sym_of_Expr       (Expr_If root) repr = (Sym_If repr)
type instance Error_of_Expr ast (Expr_If root)      = No_Error_Expr

if_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_If root)
 , Type0_Eq ty
 , Type0_Lift Type_Bool (Type_of_Expr root)
 , Expr_From ast 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
 -> ExprFrom ast (Expr_If root) hs ret
if_from ast_cond ast_ok ast_ko ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_cond ctx $
	 \(ty_cond::ty h_n) (Forall_Repr_with_Context cond) ->
	expr_from (Proxy::Proxy root) ast_ok ctx $
	 \(ty_ok::ty h_ok) (Forall_Repr_with_Context ok) ->
	expr_from (Proxy::Proxy root) ast_ko ctx $
	 \(ty_ko::ty h_ko) (Forall_Repr_with_Context ko) ->
	check_type0_eq ex ast type_bool ty_cond $ \Refl ->
	check_type0_eq ex ast ty_ok ty_ko $ \Refl ->
	k ty_ok $ Forall_Repr_with_Context $
	 \c -> if_ (cond c) (ok c) (ko c)

-- * Type 'Expr_When'
-- | Expression.
data Expr_When (root:: *)
type instance Root_of_Expr      (Expr_When root)      = root
type instance Type_of_Expr      (Expr_When root)      = No_Type
type instance Sym_of_Expr       (Expr_When root) repr = (Sym_When repr)
type instance Error_of_Expr ast (Expr_When root)      = No_Error_Expr

when_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_When root)
 , Type0_Eq ty
 , Type0_Lift Type_Bool (Type_of_Expr root)
 , Type0_Lift Type_Unit (Type_of_Expr root)
 , Expr_From ast 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
 -> ExprFrom ast (Expr_When root) hs ret
when_from ast_cond ast_ok ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_cond ctx $
	 \(ty_cond::ty h_n) (Forall_Repr_with_Context cond) ->
	expr_from (Proxy::Proxy root) ast_ok ctx $
	 \(ty_ok::ty h_ok) (Forall_Repr_with_Context ok) ->
	check_type0_eq ex ast type_bool ty_cond $ \Refl ->
	check_type0_eq ex ast type_unit ty_ok $ \Refl ->
	k ty_ok $ Forall_Repr_with_Context $
	 \c -> when (cond c) (ok c)