Cleanup & fix #1

1 files changed, 84 insertions, 47 deletions

diff --git a/README.md b/README.md
index f463e28..4dcccac 100644
--- a/README.md
+++ b/README.md
@@ -3,39 +3,49 @@
 Logic toolbox in [Clean](http://wiki.clean.cs.ru.nl/Clean). Features include:
 
  * Straightforward types for (atomic) expressions, operators and truth tables
- * `show` (`toString`-like) instances for all types that take care of associativity
+ * `show` (`toString`-like) instances for all types that take care of
+   associativity
  * Substituting atomic expressions for constants
  * Evaluating expressions without atomic expressions
  * Generating truth tables for expressions, possibly with intermediate steps
  * Displaying truth tables
  * Parsing strings to expressions
- * A web frontend to access the Clean program through, so only server-side installation is necessary
+ * A web frontend to access the Clean program through, so only server-side
+   installation is necessary
  * Different output options (Plain / ASCII art, HTML, LaTeX)
 
 Read further for examples.
 
 ### Demo
 
-A demo of the web frontend may be found on https://demo.camilstaps.nl/CleanLogic.
+A demo of the web frontend may be found on
+https://demo.camilstaps.nl/CleanLogic.
 
 ### License
 
-This program and the example are distributed under the MIT license. For more details, see the LICENSE file.
+This program and the example are distributed under the MIT license. For more
+details, see the LICENSE file.
 
 ## Installation
 
-Set `CLEAN_HOME` to your Clean installation directory. To install the parser and the example program:
+Set `CLEAN_HOME` to your Clean installation directory. To install the parser
+and the example program:
 
-    clm -I $CLEAN_HOME/lib/StdLib -I $CLEAN_HOME/lib/ArgEnv LogicParser -o LogicParser
-    clm -I $CLEAN_HOME/lib/StdLib -I $CLEAN_HOME/lib/ArgEnv LogicTest -o LogicTest
+```
+make
+```
 
 ## Types
 
 ### Operators
 
-There is one unary operator (`Op1`): `Not`. It binds stronger than all other operators.
+There is one unary operator (`Op1`): `Not`. It binds stronger than all other
+operators.
 
-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.
+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:
 
@@ -47,7 +57,9 @@ The operators are represented as:
 
 ### Expressions
 
-Expressions are constants (`B Bool`), atomic expressions (`Atom Char`), or applications of operators on other expressions (`App1 Op1 Expr` or `App2 Expr Op2 Expr`).
+Expressions are constants (`B Bool`), atomic expressions (`Atom Char`), or
+applications of operators on other expressions (`App1 Op1 Expr` or `App2 Expr
+Op2 Expr`).
 
 ### Examples
 
@@ -77,19 +89,30 @@ Expressions are constants (`B Bool`), atomic expressions (`Atom Char`), or appli
 
 ## Substitution
 
-You can substitute all occurences of `Atom a` in an `Expr e` by a `Bool b` with `substitute (a,b) e`. This yields a new `Expr`, in which all occurences have been replaced by the contstant `B b`.
+You can substitute all occurrences of `Atom a` in an `Expr e` by a `Bool b`
+with `substitute (a,b) e`. This yields a new `Expr`, in which all occurrences
+have been replaced by the constant `B b`.
 
-An alternative is `substitute_all`, which takes a list of tuples `(a :: AtomName, b :: Bool)` and substitutes all atomnames with the corresponding booleans.
+An alternative is `substitute_all`, which takes a list of tuples `(a ::
+AtomName, b :: Bool)` and substitutes all atomnames with the corresponding
+booleans.
 
 ## Evaluation
 
-An expression `e` **without atomic expressions** may be evaluated to its result by calling `eval e`. This yields the empty list `[]` if `e` *did* have atomic expressions, or a singleton `[b :: Bool]` with the result of the evaluation.
+An expression `e` **without atomic expressions** may be evaluated to its result
+by calling `eval e`. This yields the empty list `[]` if `e` *did* have atomic
+expressions, or a singleton `[b :: Bool]` with the result of the evaluation.
 
 ## Truth tables
 
-A `TruthTable` has a list of expressions `exprs` and a list of `options`, which has the type `[[(AtomName,Bool)]]` and describes all the options the truth table should list.
+A `TruthTable` has a list of expressions `exprs` and a list of `options`, which
+has the type `[[(AtomName,Bool)]]` and describes all the options the truth
+table should list.
 
-A simple truth table of an expression `e` contains only the atomic expressions in `e` and `e` itself. It may be built with `simple_truthtable e`. A more complex truth table lists all `e`'s subexpressions. In either table, the expressions are roughly sorted by complexity.
+A simple truth table of an expression `e` contains only the atomic expressions
+in `e` and `e` itself. It may be built with `simple_truthtable e`. A more
+complex truth table lists all `e`'s subexpressions. In either table, the
+expressions are roughly sorted by complexity.
 
 A truth table `table` can be shown with `toString table`.
 
@@ -123,50 +146,64 @@ The `truthtable` of `e15`:
 
 ## Parsing
 
-The `parse` function may be used to read an expression from a String. The following rules are used:
+The `parse` function may be used to read an expression from a String. The
+following rules are used:
 
  * Spaces are ignored. 
- * All latin letters (`[a-zA-Z]`) are considered atomic expressions
+ * 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
  * Unknown characters will throw an error
 
-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 
-
-The parsers also recognises `-html` and `-latex` and will output an HTML or LaTeX table if these arguments are present.
+A usage example is found in `LogicParser.icl`. This file, once compiled, reads
+the command line arguments and shows their truth tables:
+
+```
+$./LogicParser -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 
+```
+
+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 
+```
+
+The parsers also recognises `-html` and `-latex` and will output an HTML or
+LaTeX table if these arguments are present.
 
 ## Web frontend
 
-There is a simple web frontend in PHP and a basic HTML template which allows one to connect to the Clean application through his browser. The files for this are `index.html` and `request.php`, and a demo may be found on https://demo.camilstaps.nl/CleanLogic. For this to work, the `exec()` function should be enabled in your PHP configuration.
+There is a simple web frontend in PHP and a basic HTML template which allows
+one to connect to the Clean application through his browser. The files for this
+are `index.html` and `request.php`, and a demo may be found on
+https://demo.camilstaps.nl/CleanLogic. For this to work, the `exec()` function
+should be enabled in your PHP configuration.
 
 ## Future ideas
 
- * Different `toString` formats for booleans: `0` and `1` or `T` and `F` instead of `True` and `False`
+ * 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
- * Would it be easier / neater / more intuitive to get rid of `Op1` and `Op2` and use `Not`, `And`, etc. as type constructors of `Expr`?
+ * Would it be easier / neater / more intuitive to get rid of `Op1` and `Op2`
+   and use `Not`, `And`, etc. as type constructors of `Expr`?