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_Type_Lift (Error_Type_Fun AST)
  69                    (Error_of_Type AST (Type_Root_of_Expr root))
  70  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
  71                                (                   Type_Root_of_Expr root)
  72                                AST)
  73                    (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 px_ex $ Error_Expr_Read err ast
  88                                  Right (i::Bool) ->
  89                                         k type_bool $ Forall_Repr_with_Context $
  90                                                 const $ bool i
  91                          _ -> Left $ error_expr px_ex $
  92                                 Error_Expr_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 $
  98                         case hbool :: HBool (Is_Last_Expr (Expr_Bool root) root) of
  99                          HTrue  -> error_expr px_ex $ Error_Expr_Unsupported ast
 100                          HFalse -> error_expr px_ex $ Error_Expr_Unsupported_here ast
 101                 where
 102                 unary_from asts
 103                  (op::forall repr. Sym_Bool repr
 104                     => repr Bool -> repr Bool) =
 105                         case asts of
 106                          [ast_x] ->
 107                                 expr_from (Proxy::Proxy root) ctx ast_x $ \ty_x (Forall_Repr_with_Context x) ->
 108                                 when_type_eq px_ex ast type_bool ty_x $ \Refl ->
 109                                         k ty_x $ Forall_Repr_with_Context (op . x)
 110                          _ -> Left $ error_expr px_ex $
 111                                 Error_Expr_Wrong_number_of_arguments 1 ast
 112                 binary_from asts
 113                  (op::forall repr. Sym_Bool repr
 114                     => repr Bool -> repr Bool -> repr Bool) =
 115                         case asts of
 116                          [ast_x, ast_y] ->
 117                                 expr_from (Proxy::Proxy root) ctx ast_x $ \ty_x (Forall_Repr_with_Context x) ->
 118                                 expr_from (Proxy::Proxy root) ctx ast_y $ \ty_y (Forall_Repr_with_Context y) ->
 119                                 when_type_eq px_ex ast type_bool ty_x $ \Refl ->
 120                                 when_type_eq px_ex ast type_bool ty_y $ \Refl ->
 121                                         k ty_x $ Forall_Repr_with_Context $
 122                                          \c -> x c `op` y c
 123                          _ -> Left $ error_expr px_ex $
 124                                 Error_Expr_Wrong_number_of_arguments 2 ast
 125
 126 -- ** Type 'Expr_Lambda_Bool'
 127 -- | Convenient alias.
 128 type Expr_Lambda_Bool lam = Expr_Root (Expr_Alt (Expr_Lambda lam) Expr_Bool)
 129
 130 -- | Convenient alias around 'expr_from'.
 131 expr_lambda_bool_from
 132  :: forall lam ast.
 133  Expr_from ast (Expr_Lambda_Bool lam)
 134  => Proxy lam
 135  -> ast
 136  -> Either (Error_of_Expr ast (Expr_Lambda_Bool lam))
 137            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool lam))
 138                                  (Forall_Repr (Expr_Lambda_Bool lam)))
 139 expr_lambda_bool_from _px_lam ast =
 140         expr_from
 141          (Proxy::Proxy (Expr_Lambda_Bool lam))
 142          Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
 143                 Right $ Exists_Type_and_Repr ty $
 144                         Forall_Repr $ repr Context_Empty