Language/Symantic/Expr/Maybe.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeFamilies #-}
   8 {-# LANGUAGE TypeOperators #-}
   9 {-# OPTIONS_GHC -fno-warn-orphans #-}
  10 -- | Expression for 'Maybe'.
  11 module Language.Symantic.Expr.Maybe where
  12
  13 import Control.Monad
  14 import qualified Data.Maybe as Maybe
  15 import qualified Data.Function as Fun
  16 import Data.Proxy (Proxy(..))
  17 import Data.Type.Equality ((:~:)(Refl))
  18 import Prelude hiding (maybe)
  19
  20 import Language.Symantic.Type
  21 import Language.Symantic.Repr
  22 import Language.Symantic.Expr.Root
  23 import Language.Symantic.Expr.Error
  24 import Language.Symantic.Expr.From
  25 import Language.Symantic.Expr.Lambda
  26 import Language.Symantic.Trans.Common
  27
  28 -- * Class 'Sym_Maybe_Lam'
  29 -- | Symantic.
  30 class Sym_Maybe repr where
  31         nothing :: repr (Maybe a)
  32         just    :: repr a -> repr (Maybe a)
  33         maybe   :: repr b -> repr ((->) a b) -> repr (Maybe a) -> 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   :: Trans t repr => t repr b -> t repr ((->) a b) -> t repr (Maybe a) -> t repr b
  38
  39         nothing = trans_lift nothing
  40         just    = trans_map1 just
  41         maybe   = trans_map3 maybe
  42 instance Sym_Maybe Repr_Host where
  43         nothing = Repr_Host Nothing
  44         just    = liftM Just
  45         maybe   = liftM3 Maybe.maybe
  46 instance Sym_Maybe Repr_Text where
  47         nothing = repr_text_app0 "nothing"
  48         just    = repr_text_app1 "just"
  49         maybe   = repr_text_app3 "maybe"
  50 instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (Repr_Dup r1 r2) where
  51         nothing = repr_dup0 sym_Maybe nothing
  52         just    = repr_dup1 sym_Maybe just
  53         maybe   = repr_dup3 sym_Maybe maybe
  54
  55 sym_Maybe :: Proxy Sym_Maybe
  56 sym_Maybe = Proxy
  57
  58 -- * Type 'Expr_Maybe'
  59 -- | Expression.
  60 data Expr_Maybe (root:: *)
  61 type instance Root_of_Expr      (Expr_Maybe root)      = root
  62 type instance Type_of_Expr      (Expr_Maybe root)      = Type_Maybe
  63 type instance Sym_of_Expr       (Expr_Maybe root) repr = Sym_Maybe repr
  64 type instance Error_of_Expr ast (Expr_Maybe root)      = No_Error_Expr
  65
  66 -- | Parsing utility to check that the given type is a 'Type_Maybe'
  67 -- or raise 'Error_Expr_Type_mismatch'.
  68 check_type_maybe
  69  :: forall ast ex root ty h ret.
  70  ( root ~ Root_of_Expr ex
  71  , ty ~ Type_Root_of_Expr ex
  72  , Type0_Lift   Type_Maybe (Type_of_Expr root)
  73  , Type0_Unlift Type_Maybe (Type_of_Expr root)
  74  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  75                    (Error_of_Expr ast root)
  76  )
  77  => Proxy ex -> ast -> ty h
  78  -> (Type_Maybe ty h -> Either (Error_of_Expr ast root) ret)
  79  -> Either (Error_of_Expr ast root) ret
  80 check_type_maybe ex ast ty k =
  81         case type0_unlift $ unType_Root ty of
  82          Just ty_l -> k ty_l
  83          Nothing -> Left $
  84                 error_expr ex $
  85                 Error_Expr_Type_mismatch ast
  86                  (Exists_Type0 (type_maybe $ type_var0 SZero
  87                  :: ty (Maybe Var0)))
  88                  (Exists_Type0 ty)
  89
  90 -- | Parse 'maybe'.
  91 maybe_from
  92  :: forall root ty ast hs ret.
  93  ( ty ~ Type_Root_of_Expr (Expr_Maybe root)
  94  , Type0_Eq ty
  95  , Expr_From ast root
  96  , Type0_Lift   Type_Fun   (Type_of_Expr root)
  97  , Type0_Unlift Type_Fun   (Type_of_Expr root)
  98  , Type0_Lift   Type_Maybe (Type_of_Expr root)
  99  , Type0_Unlift Type_Maybe (Type_of_Expr root)
 100  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 101                    (Error_of_Expr ast root)
 102  , Root_of_Expr root ~ root
 103  ) => ast -> ast -> ast
 104  -> ExprFrom ast (Expr_Maybe root) hs ret
 105 maybe_from ast_n ast_j ast_m ex ast ctx k =
 106         expr_from (Proxy::Proxy root) ast_n ctx $
 107          \(ty_n::ty h_n) (Forall_Repr_with_Context n) ->
 108         expr_from (Proxy::Proxy root) ast_j ctx $
 109          \(ty_j::ty h_j) (Forall_Repr_with_Context j) ->
 110         expr_from (Proxy::Proxy root) ast_m ctx $
 111          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 112         check_type_fun ex ast ty_j $ \(Type2 Proxy ty_j_a ty_j_b) ->
 113         check_type_maybe ex ast ty_m $ \(Type1 _ ty_m_a) ->
 114         check_type0_eq ex ast ty_n   ty_j_b $ \Refl ->
 115         check_type0_eq ex ast ty_m_a ty_j_a $ \Refl ->
 116                 k ty_n $ Forall_Repr_with_Context $
 117                  \c -> maybe (n c) (j c) (m c)
 118
 119 -- | Parse 'nothing'.
 120 nothing_from
 121  :: forall root ty ast hs ret.
 122  ( ty ~ Type_Root_of_Expr (Expr_Maybe root)
 123  , Type0_From ast ty
 124  , Type0_Lift Type_Maybe (Type_of_Expr root)
 125  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 126                    (Error_of_Expr ast root)
 127  , Root_of_Expr root ~ root
 128  ) => ast
 129  -> ExprFrom ast (Expr_Maybe root) hs ret
 130 nothing_from ast_ty_a ex ast _ctx k =
 131         case type0_from (Proxy::Proxy ty)
 132          ast_ty_a (Right . Exists_Type0) of
 133          Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
 134          Right (Exists_Type0 ty_a) ->
 135                 k (type_maybe ty_a) $ Forall_Repr_with_Context $
 136                         Fun.const nothing
 137
 138 -- | Parse 'just'.
 139 just_from
 140  :: forall root ty ast hs ret.
 141  ( ty ~ Type_Root_of_Expr (Expr_Maybe root)
 142  , Expr_From ast root
 143  , Type0_Lift Type_Maybe (Type_of_Expr root)
 144  , Root_of_Expr root ~ root
 145  ) => ast
 146  -> ExprFrom ast (Expr_Maybe root) hs ret
 147 just_from ast_a _ex _ast ctx k =
 148         expr_from (Proxy::Proxy root) ast_a ctx $
 149          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 150         k (type_maybe ty_a) $ Forall_Repr_with_Context $
 151          \c -> just (a c)