blob: 46228dcfe18b07d1c2e73ddace12839822e59988 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
definition module Logic
import StdEnv
// Expressions
:: Expr = B Bool // A constant
| Atom AtomName // An atomic expression
| App1 Op1 Expr // Applying an Op1 on an expression
| App2 Expr Op2 Expr // Applying an Op2 on two expressions
// Operators with one argument
:: Op1 = Not // logical not
// Operators with two arguments
:: Op2 = And // logical and; left-associative
| Or // logical or; right-associative
| Impl // material implication; right-associative
| Equiv // equivalence; right-associative
// All Chars may be used, but typically only [a-zA-Z] are used
:: AtomName :== Char
isBool :: Expr -> Bool
isAtom :: Expr -> Bool
isApp1 :: Expr -> Bool
isApp2 :: Expr -> Bool
isApp :: Expr -> Bool
isNot :: Expr -> Bool
isAnd :: Expr -> Bool
isOr :: Expr -> Bool
isImpl :: Expr -> Bool
isEquiv :: Expr -> Bool
instance toString Op1
instance toString Op2
instance toString Expr
binds_stronger :: Op2 Op2 -> Bool // True iff arg1 stronger binds than arg2
|
