Language/Symantic/Expr/If.hs

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