Language/LOL/Symantic/Expr/Maybe.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE UndecidableInstances #-}
  11 -- | Expression for 'Maybe'.
  12 module Language.LOL.Symantic.Expr.Maybe where
  13
  14 import Data.Proxy (Proxy(..))
  15 import Data.Type.Equality ((:~:)(Refl))
  16 import Prelude hiding (maybe)
  17 import Language.LOL.Symantic.AST
  18 import Language.LOL.Symantic.Type
  19 import Language.LOL.Symantic.Repr.Dup
  20 import Language.LOL.Symantic.Trans.Common
  21 import Language.LOL.Symantic.Expr.Common
  22 import Language.LOL.Symantic.Expr.Lambda
  23 import Language.LOL.Symantic.Expr.Bool
  24
  25 -- * Class 'Sym_Maybe'
  26
  27 class Sym_Maybe lam repr where
  28         maybe
  29          :: repr b
  30          -> repr (Lambda lam a b)
  31          -> repr (Maybe a)
  32          -> repr b
  33
  34         default maybe
  35          :: Trans t repr
  36          => t repr b
  37          -> t repr (Lambda lam a b)
  38          -> t repr (Maybe a)
  39          -> t repr b
  40         maybe = trans_map3 maybe
  41 class Sym_Maybe_Cons repr where
  42         nothing :: repr (Maybe a)
  43         just    :: repr a -> repr (Maybe a)
  44
  45         default nothing :: Trans t repr => t repr (Maybe a)
  46         default just    :: Trans t repr => t repr a -> t repr (Maybe a)
  47         nothing = trans_lift nothing
  48         just    = trans_map1 just
  49
  50 instance -- Sym_Maybe Dup
  51  ( Sym_Maybe lam r1
  52  , Sym_Maybe lam r2
  53  ) => Sym_Maybe lam (Dup r1 r2) where
  54         maybe (m1 `Dup` m2) (n1 `Dup` n2) (j1 `Dup` j2) =
  55                 maybe m1 n1 j1 `Dup` maybe m2 n2 j2
  56 instance -- Sym_Maybe_Cons Dup
  57  ( Sym_Maybe_Cons r1
  58  , Sym_Maybe_Cons r2
  59  ) => Sym_Maybe_Cons (Dup r1 r2) where
  60         nothing = nothing `Dup` nothing
  61         just (a1 `Dup` a2) = just a1 `Dup` just a2
  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 lam repr, Sym_Maybe_Cons repr)
  69 type instance Error_of_Expr ast (Expr_Maybe lam root)      = ()
  70
  71 instance -- Expr_from AST Expr_Maybe
  72  ( Type_from AST (Type_Root_of_Expr root)
  73  , Expr_from AST root
  74
  75  , Type_Root_Lift (Type_Fun lam) (Type_Root_of_Expr root)
  76  , Type_Root_Lift Type_Maybe (Type_Root_of_Expr root)
  77  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
  78                                (                   Type_Root_of_Expr root)
  79                                AST)
  80                    (Error_of_Expr AST root)
  81  , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
  82                                  (                   Type_Root_of_Expr root)
  83                                  AST)
  84                    (Error_of_Expr AST root)
  85
  86  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
  87  , Type_Unlift Type_Maybe     (Type_of_Expr root)
  88
  89  , Root_of_Expr root ~ root
  90
  91  , Implicit_HBool (Is_Last_Expr (Expr_Maybe lam root) root)
  92  ) => Expr_from AST (Expr_Maybe lam root) where
  93         expr_from px_ex ctx ast k =
  94                 case ast of
  95                  AST "maybe" asts ->
  96                         case asts of
  97                          [ast_n, ast_j, ast_m] ->
  98                                 expr_from (Proxy::Proxy root) ctx ast_n $
  99                                  \(ty_n::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context n) ->
 100                                 expr_from (Proxy::Proxy root) ctx ast_j $
 101                                  \(ty_j::Type_Root_of_Expr root h_j) (Forall_Repr_with_Context j) ->
 102                                 expr_from (Proxy::Proxy root) ctx ast_m $
 103                                  \(ty_m::Type_Root_of_Expr root h_m) (Forall_Repr_with_Context m) ->
 104                                         case type_unlift $ unType_Root ty_j of
 105                                          Nothing -> Left $
 106                                                 error_expr px_ex $
 107                                                 Error_Expr_Type_mismatch ast
 108                                                  (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
 109                                                  :: Type_Root_of_Expr (Expr_Maybe lam root) (lam Zero -> lam (Succ Zero))))
 110                                                  (Exists_Type ty_m)
 111                                          Just (ty_j_a `Type_Fun` ty_j_b
 112                                           :: Type_Fun lam (Type_Root_of_Expr root) h_j) ->
 113                                                 case type_unlift $ unType_Root ty_m of
 114                                                  Nothing -> Left $
 115                                                         error_expr px_ex $
 116                                                         Error_Expr_Type_mismatch ast
 117                                                          (Exists_Type (type_maybe $ type_var SZero
 118                                                          :: Type_Root_of_Expr (Expr_Maybe lam root) (Maybe Zero)))
 119                                                          (Exists_Type ty_m)
 120                                                  Just (Type_Maybe ty_m_a
 121                                                         :: Type_Maybe (Type_Root_of_Expr root) h_m) ->
 122                                                         when_type_eq px_ex ast
 123                                                          ty_n ty_j_b $ \Refl ->
 124                                                                 when_type_eq px_ex ast
 125                                                                  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                          _ -> Left $ error_expr px_ex $
 129                                 Error_Expr_Wrong_number_of_arguments ast 3
 130                  AST "nothing" asts ->
 131                         case asts of
 132                          [ast_ty_a] ->
 133                                 case type_from
 134                                  (Proxy::Proxy (Type_Root_of_Expr root))
 135                                  ast_ty_a (Right . Exists_Type) of
 136                                  Left err -> Left $ error_expr px_ex $ Error_Expr_Type err ast
 137                                  Right (Exists_Type (ty_a::Type_Root_of_Expr root h_a)) ->
 138                                                 k (type_maybe ty_a) $ Forall_Repr_with_Context $
 139                                                         const nothing
 140                          _ -> Left $ error_expr px_ex $
 141                                 Error_Expr_Wrong_number_of_arguments ast 1
 142                  AST "just" asts ->
 143                         case asts of
 144                          [ast_a] ->
 145                                 expr_from (Proxy::Proxy root) ctx ast_a $
 146                                  \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
 147                                         k (type_maybe ty_a) $ Forall_Repr_with_Context $
 148                                                 \c -> just (a c)
 149                          _ -> Left $ error_expr px_ex $
 150                                 Error_Expr_Wrong_number_of_arguments ast 1
 151                  _ -> Left $ error_expr_unsupported px_ex ast
 152
 153 -- ** Type 'Expr_Lambda_Bool_Maybe'
 154 -- | Convenient alias.
 155 type Expr_Lambda_Bool_Maybe lam
 156  =   Expr_Root (Expr_Alt (Expr_Lambda lam)
 157                          (Expr_Alt Expr_Bool
 158                                   (Expr_Maybe lam)))
 159
 160 -- | Convenient alias around 'expr_from'.
 161 expr_lambda_bool_maybe_from
 162  :: forall lam ast root.
 163  ( Expr_from ast (Expr_Lambda_Bool_Maybe lam)
 164  , root ~ Expr_Lambda_Bool_Maybe lam
 165  ) => Proxy lam
 166  -> ast
 167  -> Either (Error_of_Expr ast root)
 168            (Exists_Type_and_Repr (Type_Root_of_Expr root)
 169                                  (Forall_Repr root))
 170 expr_lambda_bool_maybe_from _px_lam ast =
 171         expr_from
 172          (Proxy::Proxy root)
 173          Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
 174                 Right $ Exists_Type_and_Repr ty $
 175                         Forall_Repr $ repr Context_Empty