Language/LOL/Symantic/Expr/Bool.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 'Bool's.
  12 module Language.LOL.Symantic.Expr.Bool where
  13
  14 import Data.Proxy (Proxy(..))
  15 import Prelude hiding (and, not, or)
  16
  17 import Language.LOL.Symantic.AST
  18 import Language.LOL.Symantic.Type
  19 import Language.LOL.Symantic.Expr.Common
  20 import Language.LOL.Symantic.Expr.Lambda
  21 import Language.LOL.Symantic.Repr.Dup
  22 import Language.LOL.Symantic.Trans.Common
  23
  24 -- * Class 'Sym_Bool'
  25
  26 -- | Symantic.
  27 class Sym_Bool repr where
  28         bool ::      Bool -> repr Bool
  29         not  :: repr Bool -> repr Bool
  30         and  :: repr Bool -> repr Bool -> repr Bool
  31         or   :: repr Bool -> repr Bool -> repr Bool
  32         xor  :: repr Bool -> repr Bool -> repr Bool
  33         xor x y = (x `or` y) `and` not (x `and` y)
  34
  35         default bool :: Trans t repr =>        Bool -> t repr Bool
  36         default not  :: Trans t repr => t repr Bool -> t repr Bool
  37         default and  :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
  38         default or   :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
  39         bool = trans_lift . bool
  40         not  = trans_map1 not
  41         and  = trans_map2 and
  42         or   = trans_map2 or
  43
  44 instance -- Sym_Bool Dup
  45  ( Sym_Bool r1
  46  , Sym_Bool r2
  47  ) => Sym_Bool (Dup r1 r2) where
  48         bool x = bool x `Dup` bool x
  49         not (x1 `Dup` x2)               = not x1    `Dup` not x2
  50         and (x1 `Dup` x2) (y1 `Dup` y2) = and x1 y1 `Dup` and x2 y2
  51         or  (x1 `Dup` x2) (y1 `Dup` y2) = or  x1 y1 `Dup` or  x2 y2
  52         xor (x1 `Dup` x2) (y1 `Dup` y2) = xor x1 y1 `Dup` xor x2 y2
  53
  54 -- * Type 'Expr_Bool'
  55 -- | Expression.
  56 data Expr_Bool (root:: *)
  57 type instance Root_of_Expr (Expr_Bool root) = root
  58 type instance Type_of_Expr (Expr_Bool root) = Type_Bool
  59 type instance Sym_of_Expr (Expr_Bool root) repr = Sym_Bool repr
  60 type instance Error_of_Expr ast (Expr_Bool root) = Error_Expr_Bool ast
  61
  62 instance -- Expr_from AST Expr_Bool
  63  ( Type_from AST (Type_Root_of_Expr root)
  64  , Expr_from AST root
  65
  66  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
  67  , Error_Type_Lift (Error_Type_Fun AST)
  68                    (Error_of_Type AST (Type_Root_of_Expr root))
  69  , Error_Expr_Lift (Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root))
  70                                       (                   Type_Root_of_Expr root)
  71                                       AST)
  72                    (Error_of_Expr AST root)
  73  , Error_Expr_Lift (Error_Expr AST) (Error_of_Expr AST root)
  74
  75  , Type_Unlift Type_Bool (Type_of_Expr root)
  76
  77  , Root_of_Expr root ~ root
  78
  79  , Implicit_HBool (Is_Last_Expr (Expr_Bool root) root)
  80  ) => Expr_from AST (Expr_Bool root) where
  81         expr_from _px_ex ctx ast k =
  82                 case ast of
  83                  AST "bool" asts ->
  84                         case asts of
  85                          [AST ast_bool []] ->
  86                                 case read_safe ast_bool of
  87                                  Left err -> Left $ error_expr_lift $ Error_Expr_Read err ast
  88                                  Right (i::Bool) ->
  89                                         k type_bool $ Forall_Repr_with_Context $
  90                                                 const $ bool i
  91                          _ -> Left $ error_lambda_lift $
  92                                 Error_Expr_Fun_Wrong_number_of_arguments 3 ast
  93                  AST "not" asts -> unary_from  asts not
  94                  AST "and" asts -> binary_from asts and
  95                  AST "or"  asts -> binary_from asts or
  96                  AST "xor" asts -> binary_from asts xor
  97                  -- _ -> Left $ error_expr_lift $ Error_Expr_Unsupported ast
  98                  _ -> Left $
  99                         case hbool :: HBool (Is_Last_Expr (Expr_Bool root) root) of
 100                          HTrue  -> error_expr_lift $ Error_Expr_Unsupported_from_root ast
 101                          HFalse -> error_expr_lift $ Error_Expr_Unsupported ast
 102                 where
 103                 unary_from asts
 104                  (op::forall repr. Sym_Bool repr
 105                     => repr Bool -> repr Bool) =
 106                         case asts of
 107                          [ast_x] ->
 108                                 expr_from (Proxy::Proxy root) ctx ast_x $
 109                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
 110                                         case type_unlift $ unType_Root ty_x of
 111                                          Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_x) ->
 112                                                 k ty_x $ Forall_Repr_with_Context (op . x)
 113                                          _ -> Left $ error_lambda_lift $
 114                                                 Error_Expr_Fun_Argument_mismatch
 115                                                  (Exists_Type type_bool)
 116                                                  (Exists_Type ty_x) ast
 117                          _ -> Left $ error_lambda_lift $
 118                                 Error_Expr_Fun_Wrong_number_of_arguments 1 ast
 119                 binary_from asts
 120                  (op::forall repr. Sym_Bool repr
 121                     => repr Bool -> repr Bool -> repr Bool) =
 122                         case asts of
 123                          [ast_x, ast_y] ->
 124                                 expr_from (Proxy::Proxy root) ctx ast_x $
 125                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
 126                                 expr_from (Proxy::Proxy root) ctx ast_y $
 127                                  \(ty_y::Type_Root_of_Expr root h_y) (Forall_Repr_with_Context y) ->
 128                                         case type_unlift $ unType_Root ty_x of
 129                                          Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_x) ->
 130                                                 case type_unlift $ unType_Root ty_y of
 131                                                  Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_y) ->
 132                                                         k ty_x $ Forall_Repr_with_Context $
 133                                                          \c -> x c `op` y c
 134                                                  Nothing -> Left $ error_lambda_lift $
 135                                                         Error_Expr_Fun_Argument_mismatch
 136                                                          (Exists_Type type_bool)
 137                                                          (Exists_Type ty_y) ast
 138                                          Nothing -> Left $ error_lambda_lift $
 139                                                 Error_Expr_Fun_Argument_mismatch
 140                                                  (Exists_Type type_bool)
 141                                                  (Exists_Type ty_x) ast
 142                          _ -> Left $ error_lambda_lift $
 143                                 Error_Expr_Fun_Wrong_number_of_arguments 2 ast
 144                 error_lambda_lift
 145                  :: Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
 146                  -> Error_of_Expr AST root
 147                 error_lambda_lift = error_expr_lift
 148
 149 -- ** Type 'Expr_Lambda_Bool'
 150 -- | Convenient alias.
 151 type Expr_Lambda_Bool lam = Expr_Root (Expr_Cons (Expr_Lambda lam) Expr_Bool)
 152
 153 expr_lambda_bool_from
 154  :: forall lam ast.
 155  Expr_from ast (Expr_Lambda_Bool lam)
 156  => Proxy lam
 157  -> ast
 158  -> Either (Error_of_Expr ast (Expr_Lambda_Bool lam))
 159            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool lam))
 160                                  (Forall_Repr (Expr_Lambda_Bool lam)))
 161 expr_lambda_bool_from _px_lam ast =
 162         expr_from
 163          (Proxy::Proxy (Expr_Lambda_Bool lam))
 164          Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
 165                 Right $ Exists_Type_and_Repr ty $
 166                         Forall_Repr $ repr Context_Empty
 167
 168 -- * Type 'Error_Expr_Bool'
 169 data Error_Expr_Bool ast
 170  =   Error_Expr_Bool
 171  deriving (Eq, Show)