blob: bf7685969cca24b7347306df4a89f7891a22ee0b (
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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
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
// Possibility for an atom to be true or false
:: AtomOption :== (AtomName,Bool)
:: TruthTable = {exprs :: [Expr], options :: [[AtomOption]]}
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
instance toString TruthTable
instance == Op1
instance < Op1
instance == Op2
instance < Op2
instance == Expr
instance < Expr // To sort by unrigorous 'complexity'; e.g. in truthtables
binds_stronger :: Op2 Op2 -> Bool // True iff arg1 stronger binds than arg2
all_atoms :: Expr -> [AtomName] // All the atomic expressions in an expressions
all_atom_options :: Expr -> [[AtomOption]] // All AtomOptions for all atomic expressions in an expression
substitute :: AtomOption Expr -> Expr // Substitute all atomic expressions with some name with some constant
substitute_all :: [AtomOption] Expr -> Expr // Same, for multiple options
eval :: Expr -> [Bool] // Evaluate to a simpler form
subexprs :: Expr -> [Expr] // Subexpressions of an expression
sorted_subexprs :: (Expr -> [Expr]) // Similar, but roughly sorted by complexity
truthtable :: Expr -> TruthTable // Truthtable from an expression
|
