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