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'.
  12 module Language.LOL.Symantic.Expr.Bool where
  13
  14 import Data.Proxy (Proxy(..))
  15 import Data.Type.Equality ((:~:)(Refl))
  16 import Prelude hiding (and, not, or)
  17
  18 import Language.LOL.Symantic.AST
  19 import Language.LOL.Symantic.Type
  20 import Language.LOL.Symantic.Expr.Common
  21 import Language.LOL.Symantic.Expr.Lambda
  22 import Language.LOL.Symantic.Repr.Dup
  23 import Language.LOL.Symantic.Trans.Common
  24
  25 -- * Class 'Sym_Bool'
  26
  27 -- | Symantic.
  28 class Sym_Bool repr where
  29         bool ::      Bool -> repr Bool
  30         not  :: repr Bool -> repr Bool
  31         and  :: repr Bool -> repr Bool -> repr Bool
  32         or   :: repr Bool -> repr Bool -> repr Bool
  33         xor  :: repr Bool -> repr Bool -> repr Bool
  34         xor x y = (x `or` y) `and` not (x `and` y)
  35
  36         default bool :: Trans t repr =>        Bool -> t repr Bool
  37         default not  :: Trans t repr => t repr Bool -> t repr Bool
  38         default and  :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
  39         default or   :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
  40         bool = trans_lift . bool
  41         not  = trans_map1 not
  42         and  = trans_map2 and
  43         or   = trans_map2 or
  44
  45 instance -- Sym_Bool Dup
  46  ( Sym_Bool r1
  47  , Sym_Bool r2
  48  ) => Sym_Bool (Dup r1 r2) where
  49         bool x = bool x `Dup` bool x
  50         not (x1 `Dup` x2)               = not x1    `Dup` not x2
  51         and (x1 `Dup` x2) (y1 `Dup` y2) = and x1 y1 `Dup` and x2 y2
  52         or  (x1 `Dup` x2) (y1 `Dup` y2) = or  x1 y1 `Dup` or  x2 y2
  53         xor (x1 `Dup` x2) (y1 `Dup` y2) = xor x1 y1 `Dup` xor x2 y2
  54
  55 -- * Type 'Expr_Bool'
  56 -- | Expression.
  57 data Expr_Bool (root:: *)
  58 type instance Root_of_Expr      (Expr_Bool root)      = root
  59 type instance Type_of_Expr      (Expr_Bool root)      = Type_Bool
  60 type instance Sym_of_Expr       (Expr_Bool root) repr = Sym_Bool repr
  61 type instance Error_of_Expr ast (Expr_Bool root)      = ()
  62
  63 instance -- Expr_from AST Expr_Bool
  64  ( Type_from AST (Type_Root_of_Expr root)
  65  , Expr_from AST root
  66
  67  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
  68  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
  69                                (                   Type_Root_of_Expr root)
  70                                AST)
  71                    (Error_of_Expr AST root)
  72
  73  , Type_Unlift Type_Bool (Type_of_Expr root)
  74
  75  , Root_of_Expr root ~ root
  76
  77  , Implicit_HBool (Is_Last_Expr (Expr_Bool root) root)
  78  ) => Expr_from AST (Expr_Bool root) where
  79         expr_from px_ex ctx ast k =
  80                 case ast of
  81                  AST "bool" asts ->
  82                         case asts of
  83                          [AST ast_bool []] ->
  84                                 case read_safe ast_bool of
  85                                  Left err -> Left $ error_expr px_ex $ Error_Expr_Read err ast
  86                                  Right (i::Bool) ->
  87                                         k type_bool $ Forall_Repr_with_Context $
  88                                                 const $ bool i
  89                          _ -> Left $ error_expr px_ex $
  90                                 Error_Expr_Wrong_number_of_arguments ast 3
  91                  AST "not" asts -> unary_from  asts not
  92                  AST "and" asts -> binary_from asts and
  93                  AST "or"  asts -> binary_from asts or
  94                  AST "xor" asts -> binary_from asts xor
  95                  _ -> Left $ error_expr_unsupported px_ex ast
  96                 where
  97                 unary_from asts
  98                  (op::forall repr. Sym_Bool repr
  99                     => repr Bool -> repr Bool) =
 100                         case asts of
 101                          [ast_x] ->
 102                                 expr_from (Proxy::Proxy root) ctx ast_x $ \ty_x (Forall_Repr_with_Context x) ->
 103                                 when_type_eq px_ex ast type_bool ty_x $ \Refl ->
 104                                         k ty_x $ Forall_Repr_with_Context (op . x)
 105                          _ -> Left $ error_expr px_ex $
 106                                 Error_Expr_Wrong_number_of_arguments ast 1
 107                 binary_from asts
 108                  (op::forall repr. Sym_Bool repr
 109                     => repr Bool -> repr Bool -> repr Bool) =
 110                         case asts of
 111                          [ast_x, ast_y] ->
 112                                 expr_from (Proxy::Proxy root) ctx ast_x $ \ty_x (Forall_Repr_with_Context x) ->
 113                                 expr_from (Proxy::Proxy root) ctx ast_y $ \ty_y (Forall_Repr_with_Context y) ->
 114                                 when_type_eq px_ex ast type_bool ty_x $ \Refl ->
 115                                 when_type_eq px_ex ast type_bool ty_y $ \Refl ->
 116                                         k ty_x $ Forall_Repr_with_Context $
 117                                          \c -> x c `op` y c
 118                          _ -> Left $ error_expr px_ex $
 119                                 Error_Expr_Wrong_number_of_arguments ast 2
 120
 121 -- ** Type 'Expr_Lambda_Bool'
 122 -- | Convenient alias.
 123 type Expr_Lambda_Bool lam = Expr_Root (Expr_Alt (Expr_Lambda lam) Expr_Bool)
 124
 125 -- | Convenient alias around 'expr_from'.
 126 expr_lambda_bool_from
 127  :: forall lam ast.
 128  Expr_from ast (Expr_Lambda_Bool lam)
 129  => Proxy lam
 130  -> ast
 131  -> Either (Error_of_Expr ast (Expr_Lambda_Bool lam))
 132            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool lam))
 133                                  (Forall_Repr (Expr_Lambda_Bool lam)))
 134 expr_lambda_bool_from _px_lam ast =
 135         expr_from
 136          (Proxy::Proxy (Expr_Lambda_Bool lam))
 137          Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
 138                 Right $ Exists_Type_and_Repr ty $
 139                         Forall_Repr $ repr Context_Empty