Language/Symantic/Expr/Bool.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE ScopedTypeVariables #-}
   4 {-# LANGUAGE TypeFamilies #-}
   5 -- | Expression for 'Bool'.
   6 module Language.Symantic.Expr.Bool where
   7
   8 import Data.Proxy (Proxy(..))
   9 import Prelude hiding (and, not, or)
  10
  11 import Language.Symantic.Type
  12 import Language.Symantic.Expr.Common
  13 import Language.Symantic.Expr.Lambda
  14 import Language.Symantic.Repr.Dup
  15 import Language.Symantic.Trans.Common
  16
  17 -- * Class 'Sym_Bool'
  18 -- | Symantic.
  19 class Sym_Bool repr where
  20         bool ::      Bool -> repr Bool
  21         not  :: repr Bool -> repr Bool
  22         and  :: repr Bool -> repr Bool -> repr Bool
  23         or   :: repr Bool -> repr Bool -> repr Bool
  24         xor  :: repr Bool -> repr Bool -> repr Bool
  25         xor x y = (x `or` y) `and` not (x `and` y)
  26
  27         default bool :: Trans t repr =>        Bool -> t repr Bool
  28         default not  :: Trans t repr => t repr Bool -> t repr Bool
  29         default and  :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
  30         default or   :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
  31         bool = trans_lift . bool
  32         not  = trans_map1 not
  33         and  = trans_map2 and
  34         or   = trans_map2 or
  35
  36 instance -- Sym_Bool Dup
  37  ( Sym_Bool r1
  38  , Sym_Bool r2
  39  ) => Sym_Bool (Dup r1 r2) where
  40         bool x = bool x `Dup` bool x
  41         not (x1 `Dup` x2)               = not x1    `Dup` not x2
  42         and (x1 `Dup` x2) (y1 `Dup` y2) = and x1 y1 `Dup` and x2 y2
  43         or  (x1 `Dup` x2) (y1 `Dup` y2) = or  x1 y1 `Dup` or  x2 y2
  44         xor (x1 `Dup` x2) (y1 `Dup` y2) = xor x1 y1 `Dup` xor x2 y2
  45
  46 -- * Type 'Expr_Bool'
  47 -- | Expression.
  48 data Expr_Bool (root:: *)
  49 type instance Root_of_Expr      (Expr_Bool root)      = root
  50 type instance Type_of_Expr      (Expr_Bool root)      = Type_Bool
  51 type instance Sym_of_Expr       (Expr_Bool root) repr = Sym_Bool repr
  52 type instance Error_of_Expr ast (Expr_Bool root)      = No_Error_Expr
  53
  54 -- ** Type 'Expr_Lambda_Bool'
  55 -- | Convenient alias.
  56 type Expr_Lambda_Bool lam = Expr_Root (Expr_Alt (Expr_Lambda lam) Expr_Bool)
  57
  58 -- | Convenient alias around 'expr_from'.
  59 expr_lambda_bool_from
  60  :: forall lam ast.
  61  Expr_from ast (Expr_Lambda_Bool lam)
  62  => Proxy lam
  63  -> ast
  64  -> Either (Error_of_Expr ast (Expr_Lambda_Bool lam))
  65            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool lam))
  66                                  (Forall_Repr (Expr_Lambda_Bool lam)))
  67 expr_lambda_bool_from _lam ast =
  68         expr_from (Proxy::Proxy (Expr_Lambda_Bool lam)) ast
  69          Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
  70                 Right $ Exists_Type_and_Repr ty $
  71                         Forall_Repr $ repr Context_Empty