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.Root
  12 import Language.Symantic.Expr.Error
  13 import Language.Symantic.Expr.From
  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
  24 -- * Class 'Sym_When'
  25 -- | Symantic.
  26 class Sym_When repr where
  27         when :: repr Bool -> repr () -> repr ()
  28         default when :: Trans t repr => t repr Bool -> t repr () -> t repr ()
  29         when = trans_map2 when
  30
  31 -- * Type 'Expr_If'
  32 -- | Expression.
  33 data Expr_If (root:: *)
  34 type instance Root_of_Expr      (Expr_If root)      = root
  35 type instance Type_of_Expr      (Expr_If root)      = No_Type
  36 type instance Sym_of_Expr       (Expr_If root) repr = (Sym_If repr)
  37 type instance Error_of_Expr ast (Expr_If root)      = No_Error_Expr
  38
  39 if_from
  40  :: forall root ty ast hs ret.
  41  ( ty ~ Type_Root_of_Expr (Expr_If root)
  42  , Eq_Type ty
  43  , Lift_Type_Root Type_Bool (Type_Root_of_Expr root)
  44  , Expr_from ast root
  45  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  46                    (Error_of_Expr ast root)
  47  , Root_of_Expr root ~ root
  48  ) => ast -> ast -> ast
  49  -> Expr_From ast (Expr_If root) hs ret
  50 if_from ast_cond ast_ok ast_ko ex ast ctx k =
  51         expr_from (Proxy::Proxy root) ast_cond ctx $
  52          \(ty_cond::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context cond) ->
  53         expr_from (Proxy::Proxy root) ast_ok ctx $
  54          \(ty_ok::Type_Root_of_Expr root h_ok) (Forall_Repr_with_Context ok) ->
  55         expr_from (Proxy::Proxy root) ast_ko ctx $
  56          \(ty_ko::Type_Root_of_Expr root h_ko) (Forall_Repr_with_Context ko) ->
  57         check_eq_type ex ast type_bool ty_cond $ \Refl ->
  58         check_eq_type ex ast ty_ok ty_ko $ \Refl ->
  59         k ty_ok $ Forall_Repr_with_Context $
  60          \c -> if_ (cond c) (ok c) (ko c)
  61
  62 -- * Type 'Expr_When'
  63 -- | Expression.
  64 data Expr_When (root:: *)
  65 type instance Root_of_Expr      (Expr_When root)      = root
  66 type instance Type_of_Expr      (Expr_When root)      = No_Type
  67 type instance Sym_of_Expr       (Expr_When root) repr = (Sym_When repr)
  68 type instance Error_of_Expr ast (Expr_When root)      = No_Error_Expr
  69
  70 when_from
  71  :: forall root ty ast hs ret.
  72  ( ty ~ Type_Root_of_Expr (Expr_When root)
  73  , Eq_Type ty
  74  , Lift_Type_Root Type_Bool (Type_Root_of_Expr root)
  75  , Lift_Type_Root Type_Unit (Type_Root_of_Expr root)
  76  , Expr_from ast root
  77  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  78                    (Error_of_Expr ast root)
  79  , Root_of_Expr root ~ root
  80  ) => ast -> ast
  81  -> Expr_From ast (Expr_When root) hs ret
  82 when_from ast_cond ast_ok ex ast ctx k =
  83         expr_from (Proxy::Proxy root) ast_cond ctx $
  84          \(ty_cond::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context cond) ->
  85         expr_from (Proxy::Proxy root) ast_ok ctx $
  86          \(ty_ok::Type_Root_of_Expr root h_ok) (Forall_Repr_with_Context ok) ->
  87         check_eq_type ex ast type_bool ty_cond $ \Refl ->
  88         check_eq_type ex ast type_unit ty_ok $ \Refl ->
  89         k ty_ok $ Forall_Repr_with_Context $
  90          \c -> when (cond c) (ok c)