aboutsummaryrefslogtreecommitdiff
path: root/README.md
diff options
context:
space:
mode:
authorCamil Staps2015-07-03 17:24:29 +0200
committerCamil Staps2015-07-03 17:32:30 +0200
commite7eddf78e5fc3c9621b4e819d98e406dd9cb4748 (patch)
tree87c455f97f1211fdd227d374dcece9c5fb50d20e /README.md
parentParser; cleanup (diff)
Improved parser
Diffstat (limited to 'README.md')
-rw-r--r--README.md49
1 files changed, 47 insertions, 2 deletions
diff --git a/README.md b/README.md
index dc01fb5..49b6125 100644
--- a/README.md
+++ b/README.md
@@ -8,6 +8,7 @@ Logic toolbox in [Clean](http://wiki.clean.cs.ru.nl/Clean). Features include:
* Evaluating expressions without atomic expressions
* Generating truth tables for expressions, possibly with intermediate steps
* Displaying truth tables
+ * Parsing strings to expressions
Read further for examples.
@@ -15,9 +16,17 @@ Read further for examples.
### Operators
-There is one unary operator (`Op1`): `Not`.
+There is one unary operator (`Op1`): `Not`. It binds stronger than all other operators.
-There are four binary operators (`Op2`): `And`, `Or`, `Impl` and `Equiv`. `And` is considered left-associative; all others are considered right-associative. Associativity is only important in `toString` functions. `Expr` itself is an unambiguous recursive type.
+There are four binary operators (`Op2`). In order of descending precedence: `And`, `Or`, `Impl` and `Equiv`. `And` is considered left-associative; all others are considered right-associative. Associativity is only important in `toString` functions. `Expr` itself is an unambiguous recursive type.
+
+The operators are represented as:
+
+ * Not: `~`
+ * And: `&`
+ * Or: `|`
+ * Impl: `->`
+ * Equiv: `<->`
### Expressions
@@ -95,12 +104,48 @@ The `truthtable` of `e15`:
True | True | False | False | False
True | True | True | True | True
+## Parsing
+
+The `parse` function may be used to read an expression from a String. The following rules are used:
+
+ * Whitespace is ignored.
+ * All latin letters (`[a-zA-Z]`) are considered atomic expressions
+ * Operators are expected in their representation described above
+ * True and False are expected as `1` and `0`, respectively
+
+A usage example is found in `LogicParser.icl`. This file, once compiled, reads the command line arguments and shows their truth tables:
+
+ $./LogicParser -b -nt -e "~~(((A | (A -> B)) -> B) -> B)"
+ A | B | A -> B | A | (A -> B) | A | (A -> B) -> B | (A | (A -> B) -> B) -> B | ~((A | (A -> B) -> B) -> B) | ~~((A | (A -> B) -> B) -> B)
+ -------+-------+--------+--------------+-------------------+--------------------------+-----------------------------+------------------------------
+ False | False | True | True | False | True | False | True
+ False | True | True | True | True | True | False | True
+ True | False | False | True | False | True | False | True
+ True | True | True | True | True | True | False | True
+
+Here, `-b` and `-nt` are common Clean options to disable outputting basic values for constructors, and disable outputting execution times, respectively.
+
+The option `-e` tells the parser to show the extended truth table. With this option, only the first formula is considered. Without `-e`, multiple formulas may be given (possibly with different atomic expressions), and all will be evaluated in one table:
+
+ $./LogicParser -b -nt "~~(((A | (A -> B)) -> B) -> B)" "A & B"
+ A | B | ~~((A | (A -> B) -> B) -> B) | A & B
+ -------+-------+------------------------------+-------
+ False | False | True | False
+ False | True | True | False
+ True | False | True | False
+ True | True | True | True
+ False | False | True | False
+ False | True | True | False
+ True | False | True | False
+ True | True | True | True
+
## Future ideas
* Different `toString` formats for operators: HTML (`&not;`), UTF-8 (&not;), LaTeX (`\neg`)
* Different `toString` formats for booleans: `0` and `1` or `T` and `F` instead of `True` and `False`
* Simplifying expressions with atomic expressions as far as possible
* Testing equivalence or impliance of expressions with atomic expressions
+ * Add support for multi-letter atomic expressions
## License