Language/Symantic/Expr/If.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE OverloadedStrings #-}
   4 {-# LANGUAGE ScopedTypeVariables #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# LANGUAGE TypeOperators #-}
   7 -- | Expression for @if@.
   8 module Language.Symantic.Expr.If where
   9
  10 import qualified Control.Monad as Monad
  11 import Data.Monoid
  12 import Data.Proxy (Proxy(..))
  13 import Data.Type.Equality ((:~:)(Refl))
  14
  15 import Language.Symantic.Type
  16 import Language.Symantic.Repr
  17 import Language.Symantic.Expr.Root
  18 import Language.Symantic.Expr.Error
  19 import Language.Symantic.Expr.From
  20 import Language.Symantic.Trans.Common
  21
  22 -- * Class 'Sym_If'
  23 -- | Symantic.
  24 class Sym_If repr where
  25         if_  :: repr Bool -> repr a -> repr a -> repr a
  26         default if_ :: Trans t repr => t repr Bool -> t repr a -> t repr a -> t repr a
  27         if_  = trans_map3 if_
  28 instance Sym_If Repr_Host where
  29         if_ (Repr_Host b) ok ko = if b then ok else ko
  30 instance Sym_If Repr_Text where
  31         if_ (Repr_Text cond) (Repr_Text ok) (Repr_Text ko) =
  32                 Repr_Text $ \p v ->
  33                         let p' = precedence_If in
  34                         paren p p' $
  35                         "if " <> cond p' v <>
  36                         " then " <> ok p' v <>
  37                         " else " <> ko p' v
  38
  39 precedence_If :: Precedence
  40 precedence_If  = Precedence 2
  41
  42 instance
  43  ( Sym_If r1
  44  , Sym_If r2
  45  ) => Sym_If (Dup r1 r2) where
  46         if_ (c1 `Dup` c2) (ok1 `Dup` ok2) (ko1 `Dup` ko2) =
  47                 if_ c1 ok1 ko1 `Dup` if_ c2 ok2 ko2
  48
  49 -- * Class 'Sym_When'
  50 -- | Symantic.
  51 class Sym_When repr where
  52         when :: repr Bool -> repr () -> repr ()
  53         default when :: Trans t repr => t repr Bool -> t repr () -> t repr ()
  54         when = trans_map2 when
  55 instance Sym_When Repr_Host where
  56         when (Repr_Host b) = Monad.when b
  57 instance Sym_When Repr_Text where
  58         when (Repr_Text cond) (Repr_Text ok) =
  59                 Repr_Text $ \p v ->
  60                         let p' = precedence_If in
  61                         paren p p' $
  62                         "when " <> cond p' v <>
  63                         " " <> ok p' v
  64 instance
  65  ( Sym_When r1
  66  , Sym_When r2
  67  ) => Sym_When (Dup r1 r2) where
  68         when (c1 `Dup` c2) (ok1 `Dup` ok2) =
  69                 when c1 ok1 `Dup` when c2 ok2
  70
  71 -- * Type 'Expr_If'
  72 -- | Expression.
  73 data Expr_If (root:: *)
  74 type instance Root_of_Expr      (Expr_If root)      = root
  75 type instance Type_of_Expr      (Expr_If root)      = No_Type
  76 type instance Sym_of_Expr       (Expr_If root) repr = (Sym_If repr)
  77 type instance Error_of_Expr ast (Expr_If root)      = No_Error_Expr
  78
  79 if_from
  80  :: forall root ty ast hs ret.
  81  ( ty ~ Type_Root_of_Expr (Expr_If root)
  82  , Type0_Eq ty
  83  , Type0_Lift Type_Bool (Type_of_Expr root)
  84  , Expr_From ast root
  85  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  86                    (Error_of_Expr ast root)
  87  , Root_of_Expr root ~ root
  88  ) => ast -> ast -> ast
  89  -> ExprFrom ast (Expr_If root) hs ret
  90 if_from ast_cond ast_ok ast_ko ex ast ctx k =
  91         expr_from (Proxy::Proxy root) ast_cond ctx $
  92          \(ty_cond::ty h_n) (Forall_Repr_with_Context cond) ->
  93         expr_from (Proxy::Proxy root) ast_ok ctx $
  94          \(ty_ok::ty h_ok) (Forall_Repr_with_Context ok) ->
  95         expr_from (Proxy::Proxy root) ast_ko ctx $
  96          \(ty_ko::ty h_ko) (Forall_Repr_with_Context ko) ->
  97         check_type0_eq ex ast type_bool ty_cond $ \Refl ->
  98         check_type0_eq ex ast ty_ok ty_ko $ \Refl ->
  99         k ty_ok $ Forall_Repr_with_Context $
 100          \c -> if_ (cond c) (ok c) (ko c)
 101
 102 -- * Type 'Expr_When'
 103 -- | Expression.
 104 data Expr_When (root:: *)
 105 type instance Root_of_Expr      (Expr_When root)      = root
 106 type instance Type_of_Expr      (Expr_When root)      = No_Type
 107 type instance Sym_of_Expr       (Expr_When root) repr = (Sym_When repr)
 108 type instance Error_of_Expr ast (Expr_When root)      = No_Error_Expr
 109
 110 when_from
 111  :: forall root ty ast hs ret.
 112  ( ty ~ Type_Root_of_Expr (Expr_When root)
 113  , Type0_Eq ty
 114  , Type0_Lift Type_Bool (Type_of_Expr root)
 115  , Type0_Lift Type_Unit (Type_of_Expr root)
 116  , Expr_From ast root
 117  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 118                    (Error_of_Expr ast root)
 119  , Root_of_Expr root ~ root
 120  ) => ast -> ast
 121  -> ExprFrom ast (Expr_When root) hs ret
 122 when_from ast_cond ast_ok ex ast ctx k =
 123         expr_from (Proxy::Proxy root) ast_cond ctx $
 124          \(ty_cond::ty h_n) (Forall_Repr_with_Context cond) ->
 125         expr_from (Proxy::Proxy root) ast_ok ctx $
 126          \(ty_ok::ty h_ok) (Forall_Repr_with_Context ok) ->
 127         check_type0_eq ex ast type_bool ty_cond $ \Refl ->
 128         check_type0_eq ex ast type_unit ty_ok $ \Refl ->
 129         k ty_ok $ Forall_Repr_with_Context $
 130          \c -> when (cond c) (ok c)