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 =
  48                 Repr_Text $ \_p _v ->
  49                         "nothing"
  50         just  = repr_text_app1 "just"
  51         maybe = repr_text_app3 "maybe"
  52 instance
  53  ( Sym_Maybe r1
  54  , Sym_Maybe r2
  55  ) => Sym_Maybe (Dup r1 r2) where
  56         nothing = nothing `Dup` nothing
  57         just (a1 `Dup` a2) = just a1 `Dup` just a2
  58         maybe (m1 `Dup` m2) (n1 `Dup` n2) (j1 `Dup` j2) =
  59                 maybe m1 n1 j1 `Dup`
  60                 maybe m2 n2 j2
  61
  62 -- * Type 'Expr_Maybe'
  63 -- | Expression.
  64 data Expr_Maybe (root:: *)
  65 type instance Root_of_Expr      (Expr_Maybe root)      = root
  66 type instance Type_of_Expr      (Expr_Maybe root)      = Type_Maybe
  67 type instance Sym_of_Expr       (Expr_Maybe root) repr = (Sym_Maybe repr)
  68 type instance Error_of_Expr ast (Expr_Maybe root)      = No_Error_Expr
  69
  70 -- | Parsing utility to check that the given type is a 'Type_Maybe'
  71 -- or raise 'Error_Expr_Type_mismatch'.
  72 check_type_maybe
  73  :: forall ast ex root ty h ret.
  74  ( root ~ Root_of_Expr ex
  75  , ty ~ Type_Root_of_Expr ex
  76  , Lift_Type   Type_Maybe (Type_of_Expr root)
  77  , Unlift_Type Type_Maybe (Type_of_Expr root)
  78  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  79                    (Error_of_Expr ast root)
  80  )
  81  => Proxy ex -> ast -> ty h
  82  -> (Type_Maybe ty h -> Either (Error_of_Expr ast root) ret)
  83  -> Either (Error_of_Expr ast root) ret
  84 check_type_maybe ex ast ty k =
  85         case unlift_type $ unType_Root ty of
  86          Just ty_l -> k ty_l
  87          Nothing -> Left $
  88                 error_expr ex $
  89                 Error_Expr_Type_mismatch ast
  90                  (Exists_Type (type_maybe $ type_var0 SZero
  91                  :: ty (Maybe Var0)))
  92                  (Exists_Type ty)
  93
  94 -- | Parse 'maybe'.
  95 maybe_from
  96  :: forall root ty ast hs ret.
  97  ( ty ~ Type_Root_of_Expr (Expr_Maybe root)
  98  , Eq_Type ty
  99  , Expr_from ast root
 100  , Lift_Type   Type_Fun   (Type_of_Expr root)
 101  , Unlift_Type Type_Fun   (Type_of_Expr root)
 102  , Lift_Type   Type_Maybe (Type_of_Expr root)
 103  , Unlift_Type Type_Maybe (Type_of_Expr root)
 104  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 105                    (Error_of_Expr ast root)
 106  , Root_of_Expr root ~ root
 107  ) => ast -> ast -> ast
 108  -> Expr_From ast (Expr_Maybe root) hs ret
 109 maybe_from ast_n ast_j ast_m ex ast ctx k =
 110         expr_from (Proxy::Proxy root) ast_n ctx $
 111          \(ty_n::ty h_n) (Forall_Repr_with_Context n) ->
 112         expr_from (Proxy::Proxy root) ast_j ctx $
 113          \(ty_j::ty h_j) (Forall_Repr_with_Context j) ->
 114         expr_from (Proxy::Proxy root) ast_m ctx $
 115          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 116         check_type_fun ex ast ty_j $ \(Type_Type2 Proxy ty_j_a ty_j_b
 117          :: Type_Fun ty h_j) ->
 118         check_type_maybe ex ast ty_m $ \(Type_Type1 _ ty_m_a) ->
 119         check_eq_type ex ast ty_n   ty_j_b $ \Refl ->
 120         check_eq_type ex ast ty_m_a ty_j_a $ \Refl ->
 121                 k ty_n $ Forall_Repr_with_Context $
 122                  \c -> maybe (n c) (j c) (m c)
 123
 124 -- | Parse 'nothing'.
 125 nothing_from
 126  :: forall root ty ast hs ret.
 127  ( ty ~ Type_Root_of_Expr (Expr_Maybe root)
 128  , Type_from ast ty
 129  , Lift_Type Type_Maybe (Type_of_Expr root)
 130  , Lift_Error_Expr (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 root) hs ret
 135 nothing_from ast_ty_a ex ast _ctx k =
 136         case type_from (Proxy::Proxy ty)
 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                         Fun.const nothing
 142
 143 -- | Parse 'just'.
 144 just_from
 145  :: forall root ty ast hs ret.
 146  ( ty ~ Type_Root_of_Expr (Expr_Maybe root)
 147  , Expr_from ast root
 148  , Lift_Type Type_Maybe (Type_of_Expr root)
 149  , Root_of_Expr root ~ root
 150  ) => ast
 151  -> Expr_From ast (Expr_Maybe root) hs ret
 152 just_from ast_a _ex _ast ctx k =
 153         expr_from (Proxy::Proxy root) ast_a ctx $
 154          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 155         k (type_maybe ty_a) $ Forall_Repr_with_Context $
 156          \c -> just (a c)