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