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