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_Type_Lift (Error_Type_Fun AST)
  78                    (Error_of_Type AST (Type_Root_of_Expr root))
  79  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
  80                                (                   Type_Root_of_Expr root)
  81                                AST)
  82                    (Error_of_Expr AST root)
  83  , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
  84                                  (                   Type_Root_of_Expr root)
  85                                  AST)
  86                    (Error_of_Expr AST root)
  87
  88  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
  89  , Type_Unlift Type_Maybe     (Type_of_Expr root)
  90
  91  , Root_of_Expr root ~ root
  92
  93  , Implicit_HBool (Is_Last_Expr (Expr_Maybe lam root) root)
  94  ) => Expr_from AST (Expr_Maybe lam root) where
  95         expr_from px_ex ctx ast k =
  96                 case ast of
  97                  AST "maybe" asts ->
  98                         case asts of
  99                          [ast_n, ast_j, ast_m] ->
 100                                 expr_from (Proxy::Proxy root) ctx ast_n $
 101                                  \(ty_n::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context n) ->
 102                                 expr_from (Proxy::Proxy root) ctx ast_j $
 103                                  \(ty_j::Type_Root_of_Expr root h_j) (Forall_Repr_with_Context j) ->
 104                                 expr_from (Proxy::Proxy root) ctx ast_m $
 105                                  \(ty_m::Type_Root_of_Expr root h_m) (Forall_Repr_with_Context m) ->
 106                                         case type_unlift $ unType_Root ty_j of
 107                                          Just (ty_j_a `Type_Fun` ty_j_b
 108                                           :: Type_Fun lam (Type_Root_of_Expr root) h_j) ->
 109                                                 case type_unlift $ unType_Root ty_m of
 110                                                  Just (Type_Maybe ty_m_a
 111                                                         :: Type_Maybe (Type_Root_of_Expr root) h_m) ->
 112                                                         when_type_eq px_ex ast
 113                                                          ty_n ty_j_b $ \Refl ->
 114                                                                 when_type_eq px_ex ast
 115                                                                  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                          _ -> Left $ error_expr px_ex $
 119                                 Error_Expr_Wrong_number_of_arguments 3 ast
 120                  AST "nothing" asts ->
 121                         case asts of
 122                          [ast_ty_a] ->
 123                                 case type_from
 124                                  (Proxy::Proxy (Type_Root_of_Expr root))
 125                                  ast_ty_a (Right . Exists_Type) of
 126                                  Left err -> Left $ error_expr px_ex $ Error_Expr_Type err ast
 127                                  Right (Exists_Type (ty_a::Type_Root_of_Expr root h_a)) ->
 128                                                 k (type_maybe ty_a) $ Forall_Repr_with_Context $
 129                                                         const nothing
 130                          _ -> Left $ error_expr px_ex $
 131                                 Error_Expr_Wrong_number_of_arguments 1 ast
 132                  AST "just" asts ->
 133                         case asts of
 134                          [ast_a] ->
 135                                 expr_from (Proxy::Proxy root) ctx ast_a $
 136                                  \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
 137                                         k (type_maybe ty_a) $ Forall_Repr_with_Context $
 138                                                 \c -> just (a c)
 139                          _ -> Left $ error_expr px_ex $
 140                                 Error_Expr_Wrong_number_of_arguments 1 ast
 141                  _ -> Left $
 142                         case hbool :: HBool (Is_Last_Expr (Expr_Maybe lam root) root) of
 143                          HTrue  -> error_expr px_ex $ Error_Expr_Unsupported ast
 144                          HFalse -> error_expr px_ex $ Error_Expr_Unsupported_here ast
 145
 146
 147 -- ** Type 'Expr_Lambda_Bool_Maybe'
 148 -- | Convenient alias.
 149 type Expr_Lambda_Bool_Maybe lam
 150  =   Expr_Root (Expr_Alt (Expr_Lambda lam)
 151                          (Expr_Alt Expr_Bool
 152                                   (Expr_Maybe lam)))
 153
 154 -- | Convenient alias around 'expr_from'.
 155 expr_lambda_bool_maybe_from
 156  :: forall lam ast root.
 157  ( Expr_from ast (Expr_Lambda_Bool_Maybe lam)
 158  , root ~ Expr_Lambda_Bool_Maybe lam
 159  ) => Proxy lam
 160  -> ast
 161  -> Either (Error_of_Expr ast root)
 162            (Exists_Type_and_Repr (Type_Root_of_Expr root)
 163                                  (Forall_Repr root))
 164 expr_lambda_bool_maybe_from _px_lam ast =
 165         expr_from
 166          (Proxy::Proxy root)
 167          Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
 168                 Right $ Exists_Type_and_Repr ty $
 169                         Forall_Repr $ repr Context_Empty