Language/Symantic/Expr/Maybe.hs

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