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