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 {-# OPTIONS_GHC -fno-warn-orphans #-}
   9 -- | Expression for 'Maybe'.
  10 module Language.Symantic.Expr.Maybe where
  11
  12 import qualified Data.Function as Fun
  13 import Data.Proxy (Proxy(..))
  14 import Data.Type.Equality ((:~:)(Refl))
  15 import Prelude hiding (maybe)
  16
  17 import Language.Symantic.Type
  18 import Language.Symantic.Trans.Common
  19 import Language.Symantic.Expr.Root
  20 import Language.Symantic.Expr.Error
  21 import Language.Symantic.Expr.From
  22 import Language.Symantic.Expr.Lambda
  23
  24 -- * Class 'Sym_Maybe_Lam'
  25 -- | Symantic.
  26 class Sym_Maybe repr where
  27         nothing :: repr (Maybe a)
  28         just    :: repr a -> repr (Maybe a)
  29         maybe
  30          :: repr b
  31          -> repr ((->) a b)
  32          -> repr (Maybe a)
  33          -> repr b
  34
  35         default nothing :: Trans t repr => t repr (Maybe a)
  36         default just    :: Trans t repr => t repr a -> t repr (Maybe a)
  37         default maybe
  38          :: Trans t repr
  39          => t repr b
  40          -> t repr ((->) a b)
  41          -> t repr (Maybe a)
  42          -> t repr b
  43
  44         nothing = trans_lift nothing
  45         just    = trans_map1 just
  46         maybe   = trans_map3 maybe
  47
  48 -- * Type 'Expr_Maybe'
  49 -- | Expression.
  50 data Expr_Maybe (root:: *)
  51 type instance Root_of_Expr      (Expr_Maybe root)      = root
  52 type instance Type_of_Expr      (Expr_Maybe root)      = Type_Maybe
  53 type instance Sym_of_Expr       (Expr_Maybe root) repr = (Sym_Maybe repr)
  54 type instance Error_of_Expr ast (Expr_Maybe root)      = No_Error_Expr
  55
  56 -- | Parsing utility to check that the given type is a 'Type_Maybe'
  57 -- or raise 'Error_Expr_Type_mismatch'.
  58 check_type_maybe
  59  :: forall ast ex root ty h ret.
  60  ( root ~ Root_of_Expr ex
  61  , ty ~ Type_Root_of_Expr ex
  62  , Lift_Type   Type_Maybe (Type_of_Expr root)
  63  , Unlift_Type Type_Maybe (Type_of_Expr root)
  64  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  65                    (Error_of_Expr ast root)
  66  )
  67  => Proxy ex -> ast -> ty h
  68  -> (Type_Maybe ty h -> Either (Error_of_Expr ast root) ret)
  69  -> Either (Error_of_Expr ast root) ret
  70 check_type_maybe ex ast ty k =
  71         case unlift_type $ unType_Root ty of
  72          Just ty_l -> k ty_l
  73          Nothing -> Left $
  74                 error_expr ex $
  75                 Error_Expr_Type_mismatch ast
  76                  (Exists_Type (type_maybe $ type_var0 SZero
  77                  :: ty (Maybe Var0)))
  78                  (Exists_Type ty)
  79
  80 -- | Parse 'maybe'.
  81 maybe_from
  82  :: forall root ty ast hs ret.
  83  ( ty ~ Type_Root_of_Expr (Expr_Maybe root)
  84  , Eq_Type ty
  85  , Expr_from ast root
  86  , Lift_Type   Type_Fun   (Type_of_Expr root)
  87  , Unlift_Type Type_Fun   (Type_of_Expr root)
  88  , Lift_Type   Type_Maybe (Type_of_Expr root)
  89  , Unlift_Type Type_Maybe (Type_of_Expr root)
  90  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  91                    (Error_of_Expr ast root)
  92  , Root_of_Expr root ~ root
  93  ) => ast -> ast -> ast
  94  -> Expr_From ast (Expr_Maybe root) hs ret
  95 maybe_from ast_n ast_j ast_m ex ast ctx k =
  96         expr_from (Proxy::Proxy root) ast_n ctx $
  97          \(ty_n::ty h_n) (Forall_Repr_with_Context n) ->
  98         expr_from (Proxy::Proxy root) ast_j ctx $
  99          \(ty_j::ty h_j) (Forall_Repr_with_Context j) ->
 100         expr_from (Proxy::Proxy root) ast_m ctx $
 101          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 102         check_type_fun ex ast ty_j $ \(Type_Type2 Proxy ty_j_a ty_j_b
 103          :: Type_Fun ty h_j) ->
 104         check_type_maybe ex ast ty_m $ \(Type_Type1 _ ty_m_a) ->
 105         check_eq_type ex ast ty_n   ty_j_b $ \Refl ->
 106         check_eq_type ex ast ty_m_a ty_j_a $ \Refl ->
 107                 k ty_n $ Forall_Repr_with_Context $
 108                  \c -> maybe (n c) (j c) (m c)
 109
 110 -- | Parse 'nothing'.
 111 nothing_from
 112  :: forall root ty ast hs ret.
 113  ( ty ~ Type_Root_of_Expr (Expr_Maybe root)
 114  , Type_from ast ty
 115  , Lift_Type Type_Maybe (Type_of_Expr root)
 116  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 117                    (Error_of_Expr ast root)
 118  , Root_of_Expr root ~ root
 119  ) => ast
 120  -> Expr_From ast (Expr_Maybe root) hs ret
 121 nothing_from ast_ty_a ex ast _ctx k =
 122         case type_from (Proxy::Proxy ty)
 123          ast_ty_a (Right . Exists_Type) of
 124          Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
 125          Right (Exists_Type ty_a) ->
 126                 k (type_maybe ty_a) $ Forall_Repr_with_Context $
 127                         Fun.const nothing
 128
 129 -- | Parse 'just'.
 130 just_from
 131  :: forall root ty ast hs ret.
 132  ( ty ~ Type_Root_of_Expr (Expr_Maybe root)
 133  , Expr_from ast root
 134  , Lift_Type Type_Maybe (Type_of_Expr root)
 135  , Root_of_Expr root ~ root
 136  ) => ast
 137  -> Expr_From ast (Expr_Maybe root) hs ret
 138 just_from ast_a _ex _ast ctx k =
 139         expr_from (Proxy::Proxy root) ast_a ctx $
 140          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 141         k (type_maybe ty_a) $ Forall_Repr_with_Context $
 142          \c -> just (a c)