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