Language/Symantic/Expr/If.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE ScopedTypeVariables #-}
   4 {-# LANGUAGE TypeFamilies #-}
   5 {-# LANGUAGE TypeOperators #-}
   6 -- | Expression for @if@.
   7 module Language.Symantic.Expr.If where
   8
   9 import Data.Proxy (Proxy(..))
  10 import Data.Type.Equality ((:~:)(Refl))
  11 import Language.Symantic.Expr.Common
  12 import Language.Symantic.Repr.Dup
  13 import Language.Symantic.Trans.Common
  14 import Language.Symantic.Type
  15
  16 -- * Class 'Sym_If'
  17 -- | Symantic.
  18 class Sym_If repr where
  19         if_  :: repr Bool -> repr a -> repr a -> repr a
  20         default if_ :: Trans t repr => t repr Bool -> t repr a -> t repr a -> t repr a
  21         if_  = trans_map3 if_
  22 -- | Symantic.
  23 class Sym_When repr where
  24         when :: repr Bool -> repr () -> repr ()
  25         default when :: Trans t repr => t repr Bool -> t repr () -> t repr ()
  26         when = trans_map2 when
  27
  28 instance -- Sym_If Dup
  29  ( Sym_If r1
  30  , Sym_If r2
  31  ) => Sym_If (Dup r1 r2) where
  32         if_ (c1 `Dup` c2) (ok1 `Dup` ok2) (ko1 `Dup` ko2) =
  33                 if_ c1 ok1 ko1 `Dup`
  34                 if_ c2 ok2 ko2
  35 instance -- Sym_When Dup
  36  ( Sym_When r1
  37  , Sym_When r2
  38  ) => Sym_When (Dup r1 r2) where
  39         when (c1 `Dup` c2) (ok1 `Dup` ok2) =
  40                 when c1 ok1 `Dup`
  41                 when c2 ok2
  42
  43 -- * Type 'Expr_If'
  44 -- | Expression.
  45 data Expr_If (root:: *)
  46 type instance Root_of_Expr      (Expr_If root)      = root
  47 type instance Type_of_Expr      (Expr_If root)      = No_Type
  48 type instance Sym_of_Expr       (Expr_If root) repr = (Sym_If repr)
  49 type instance Error_of_Expr ast (Expr_If root)      = No_Error_Expr
  50
  51 if_from
  52  :: forall root ty ast hs ret.
  53  ( ty ~ Type_Root_of_Expr (Expr_If root)
  54  , Type_Eq ty
  55  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
  56  , Expr_from ast root
  57  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  58                    (Error_of_Expr ast root)
  59  , Root_of_Expr root ~ root
  60  ) => ast -> ast -> ast
  61  -> Expr_From ast (Expr_If root) hs ret
  62 if_from ast_cond ast_ok ast_ko ex ast ctx k =
  63         expr_from (Proxy::Proxy root) ast_cond ctx $
  64          \(ty_cond::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context cond) ->
  65         expr_from (Proxy::Proxy root) ast_ok ctx $
  66          \(ty_ok::Type_Root_of_Expr root h_ok) (Forall_Repr_with_Context ok) ->
  67         expr_from (Proxy::Proxy root) ast_ko ctx $
  68          \(ty_ko::Type_Root_of_Expr root h_ko) (Forall_Repr_with_Context ko) ->
  69         check_type_eq ex ast type_bool ty_cond $ \Refl ->
  70         check_type_eq ex ast ty_ok ty_ko $ \Refl ->
  71                 k ty_ok $ Forall_Repr_with_Context $
  72                  \c -> if_ (cond c) (ok c) (ko c)
  73
  74 -- * Type 'Expr_When'
  75 -- | Expression.
  76 data Expr_When (root:: *)
  77 type instance Root_of_Expr      (Expr_When root)      = root
  78 type instance Type_of_Expr      (Expr_When root)      = No_Type
  79 type instance Sym_of_Expr       (Expr_When root) repr = (Sym_When repr)
  80 type instance Error_of_Expr ast (Expr_When root)      = No_Error_Expr
  81
  82 when_from
  83  :: forall root ty ast hs ret.
  84  ( ty ~ Type_Root_of_Expr (Expr_When root)
  85  , Type_Eq ty
  86  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
  87  , Type_Root_Lift Type_Unit (Type_Root_of_Expr root)
  88  , Expr_from ast root
  89  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  90                    (Error_of_Expr ast root)
  91  , Root_of_Expr root ~ root
  92  ) => ast -> ast
  93  -> Expr_From ast (Expr_When root) hs ret
  94 when_from ast_cond ast_ok ex ast ctx k =
  95         expr_from (Proxy::Proxy root) ast_cond ctx $
  96          \(ty_cond::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context cond) ->
  97         expr_from (Proxy::Proxy root) ast_ok ctx $
  98          \(ty_ok::Type_Root_of_Expr root h_ok) (Forall_Repr_with_Context ok) ->
  99         check_type_eq ex ast type_bool ty_cond $ \Refl ->
 100         check_type_eq ex ast type_unit ty_ok $ \Refl ->
 101                 k ty_ok $ Forall_Repr_with_Context $
 102                  \c -> when (cond c) (ok c)