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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
/**
* The MIT License (MIT)
*
* Copyright (c) 2015 Camil Staps
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
*/
definition module Logic
import StdEnv, StdMaybe
// 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]]}
:: FilledTruthTable = {table :: TruthTable, values :: [[Maybe Bool]]}
:: OutputOption = Plain | Html | LaTeX
DefaultOutputOption :== Plain
instance == OutputOption
class show a :: OutputOption a -> String
instance show Bool
instance show Char
instance show Op1
instance show Op2
instance show Expr
instance show FilledTruthTable
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 == Op1
instance < Op1 // Maybe useful later if more unary operators are added
instance == Op2
instance < Op2 // To sort by precedence
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
simple_truthtable :: Expr -> TruthTable // Simple truthtable: only the atomic expression and the expression itself
simple_truthtable_n :: [Expr] -> TruthTable // Simple truthtable with multiple expressions
truthtable :: Expr -> TruthTable // Truthtable from an expression
truthtable_n :: [Expr] -> TruthTable // Truthtable with multiple expressions
compute :: TruthTable -> FilledTruthTable // Fill in a truthtable
parse :: String -> Expr // Parse a string into an expression
|
