]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Bool.hs
init
[haskell/symantic.git] / 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