Language/LOL/Symantic/Expr/Bool.hs

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