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