Language/Symantic/Expr/Maybe.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 -- | Expression for 'Maybe'.
   8 module Language.Symantic.Expr.Maybe where
   9
  10 import Data.Proxy (Proxy(..))
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Prelude hiding (maybe)
  13 import Language.Symantic.Type
  14 import Language.Symantic.Repr.Dup
  15 import Language.Symantic.Trans.Common
  16 import Language.Symantic.Expr.Common
  17 import Language.Symantic.Expr.Lambda
  18 import Language.Symantic.Expr.Bool
  19
  20 -- * Class 'Sym_Maybe'
  21 -- | Symantic.
  22 class Sym_Maybe lam repr where
  23         maybe
  24          :: repr b
  25          -> repr (Lambda lam a b)
  26          -> repr (Maybe a)
  27          -> repr b
  28
  29         default maybe
  30          :: Trans t repr
  31          => t repr b
  32          -> t repr (Lambda lam a b)
  33          -> t repr (Maybe a)
  34          -> t repr b
  35         maybe = trans_map3 maybe
  36 -- | Symantic.
  37 class Sym_Maybe_Cons repr where
  38         nothing :: repr (Maybe a)
  39         just    :: repr a -> repr (Maybe a)
  40
  41         default nothing :: Trans t repr => t repr (Maybe a)
  42         default just    :: Trans t repr => t repr a -> t repr (Maybe a)
  43         nothing = trans_lift nothing
  44         just    = trans_map1 just
  45
  46 instance -- Sym_Maybe Dup
  47  ( Sym_Maybe lam r1
  48  , Sym_Maybe lam r2
  49  ) => Sym_Maybe lam (Dup r1 r2) where
  50         maybe (m1 `Dup` m2) (n1 `Dup` n2) (j1 `Dup` j2) =
  51                 maybe m1 n1 j1 `Dup` maybe m2 n2 j2
  52 instance -- Sym_Maybe_Cons Dup
  53  ( Sym_Maybe_Cons r1
  54  , Sym_Maybe_Cons r2
  55  ) => Sym_Maybe_Cons (Dup r1 r2) where
  56         nothing = nothing `Dup` nothing
  57         just (a1 `Dup` a2) = just a1 `Dup` just a2
  58
  59 -- * Type 'Expr_Maybe'
  60 -- | Expression.
  61 data Expr_Maybe (lam:: * -> *) (root:: *)
  62 type instance Root_of_Expr      (Expr_Maybe lam root)      = root
  63 type instance Type_of_Expr      (Expr_Maybe lam root)      = Type_Maybe
  64 type instance Sym_of_Expr       (Expr_Maybe lam root) repr = (Sym_Maybe lam repr, Sym_Maybe_Cons repr)
  65 type instance Error_of_Expr ast (Expr_Maybe lam root)      = No_Error_Expr
  66
  67 maybe_from
  68  :: forall root lam ty ast hs ret.
  69  ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
  70  , Type_Eq (Type_Root_of_Expr root)
  71  , Expr_from ast root
  72  , Type_Root_Lift (Type_Fun lam) (Type_Root_of_Expr root)
  73  , Type_Root_Lift Type_Maybe (Type_Root_of_Expr root)
  74  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  75                    (Error_of_Expr ast root)
  76  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
  77  , Type_Unlift Type_Maybe     (Type_of_Expr root)
  78  , Root_of_Expr root ~ root
  79  ) => ast -> ast -> ast
  80  -> Expr_From ast (Expr_Maybe lam root) hs ret
  81 maybe_from ast_n ast_j ast_m ex ast ctx k =
  82         expr_from (Proxy::Proxy root) ast_n ctx $
  83          \(ty_n::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context n) ->
  84         expr_from (Proxy::Proxy root) ast_j ctx $
  85          \(ty_j::Type_Root_of_Expr root h_j) (Forall_Repr_with_Context j) ->
  86         expr_from (Proxy::Proxy root) ast_m ctx $
  87          \(ty_m::Type_Root_of_Expr root h_m) (Forall_Repr_with_Context m) ->
  88                 case type_unlift $ unType_Root ty_j of
  89                  Nothing -> Left $
  90                         error_expr ex $
  91                         Error_Expr_Type_mismatch ast
  92                          (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
  93                          :: Type_Root_of_Expr (Expr_Maybe lam root) (lam Zero -> lam (Succ Zero))))
  94                          (Exists_Type ty_m)
  95                  Just (ty_j_a `Type_Fun` ty_j_b
  96                   :: Type_Fun lam (Type_Root_of_Expr root) h_j) ->
  97                         case type_unlift $ unType_Root ty_m of
  98                          Nothing -> Left $
  99                                 error_expr ex $
 100                                 Error_Expr_Type_mismatch ast
 101                                  (Exists_Type (type_maybe $ type_var SZero
 102                                  :: Type_Root_of_Expr (Expr_Maybe lam root) (Maybe Zero)))
 103                                  (Exists_Type ty_m)
 104                          Just (Type_Maybe ty_m_a
 105                                 :: Type_Maybe (Type_Root_of_Expr root) h_m) ->
 106                                 when_type_eq ex ast
 107                                  ty_n ty_j_b $ \Refl ->
 108                                         when_type_eq ex ast
 109                                          ty_m_a ty_j_a $ \Refl ->
 110                                                 k ty_n $ Forall_Repr_with_Context $
 111                                                  \c -> maybe (n c) (j c) (m c)
 112
 113 nothing_from
 114  :: forall root lam ty ast hs ret.
 115  ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
 116  , Type_from ast (Type_Root_of_Expr root)
 117  , Type_Root_Lift Type_Maybe (Type_Root_of_Expr root)
 118  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 119                    (Error_of_Expr ast root)
 120  , Root_of_Expr root ~ root
 121  ) => ast
 122  -> Expr_From ast (Expr_Maybe lam root) hs ret
 123 nothing_from ast_ty_a ex ast _ctx k =
 124         case type_from
 125          (Proxy::Proxy (Type_Root_of_Expr root))
 126          ast_ty_a (Right . Exists_Type) of
 127          Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
 128          Right (Exists_Type (ty_a::Type_Root_of_Expr root h_a)) ->
 129                         k (type_maybe ty_a) $ Forall_Repr_with_Context $
 130                                 const nothing
 131
 132 just_from
 133  :: forall root lam ty ast hs ret.
 134  ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
 135  , Expr_from ast root
 136  , Type_Root_Lift Type_Maybe (Type_Root_of_Expr root)
 137  , Root_of_Expr root ~ root
 138  ) => ast
 139  -> Expr_From ast (Expr_Maybe lam root) hs ret
 140 just_from ast_a _ex _ast ctx k =
 141         expr_from (Proxy::Proxy root) ast_a ctx $
 142          \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
 143                 k (type_maybe ty_a) $ Forall_Repr_with_Context $
 144                         \c -> just (a c)
 145
 146 -- ** Type 'Expr_Lambda_Maybe_Bool'
 147 -- | Convenient alias.
 148 type Expr_Lambda_Maybe_Bool lam
 149  =   Expr_Root (Expr_Alt (Expr_Lambda lam)
 150                          (Expr_Alt (Expr_Maybe lam)
 151                                     Expr_Bool))
 152
 153 -- | Convenient alias around 'expr_from'.
 154 expr_lambda_maybe_bool_from
 155  :: forall lam ast root.
 156  ( Expr_from ast (Expr_Lambda_Maybe_Bool lam)
 157  , root ~ Expr_Lambda_Maybe_Bool lam
 158  ) => Proxy lam
 159  -> ast
 160  -> Either (Error_of_Expr ast root)
 161            (Exists_Type_and_Repr (Type_Root_of_Expr root)
 162                                  (Forall_Repr root))
 163 expr_lambda_maybe_bool_from _lam ast =
 164         expr_from (Proxy::Proxy root) ast
 165          Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
 166                 Right $ Exists_Type_and_Repr ty $
 167                         Forall_Repr $ repr Context_Empty