{-# 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_If in paren p p' $ "if " <> cond p' v <> " then " <> ok p' v <> " else " <> ko p' v precedence_If :: Precedence precedence_If = Precedence 2 instance ( Sym_If r1 , Sym_If r2 ) => Sym_If (Dup r1 r2) where if_ (c1 `Dup` c2) (ok1 `Dup` ok2) (ko1 `Dup` ko2) = if_ c1 ok1 ko1 `Dup` if_ c2 ok2 ko2 -- * 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_If in paren p p' $ "when " <> cond p' v <> " " <> ok p' v instance ( Sym_When r1 , Sym_When r2 ) => Sym_When (Dup r1 r2) where when (c1 `Dup` c2) (ok1 `Dup` ok2) = when c1 ok1 `Dup` when c2 ok2 -- * 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)