From ee1d005ab9fcd20f185cbfe116f4c45942f67e62 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 02:21:39 +0100
Subject: [PATCH 01/32] Update .gitignore

---
 .gitignore | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/.gitignore b/.gitignore
index 02c0875..623b3b2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,11 @@
+# macOS
 .DS_Store
+
+# Swift PM and Xcode
 /.build
 /Packages
+/Package.resolved
 /*.xcodeproj
+
+# Project specific files
+InputSamples/

From b6b585eb5453c9f51f99d75644639c75df0e9cae Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 02:27:16 +0100
Subject: [PATCH 02/32] Remove the interpreter

---
 Package.swift                                 |   25 +-
 README.md                                     |   40 -
 Sources/LogicKitParser/Parser.swift           |  100 --
 Sources/linenoise/LICENSE                     |   25 -
 Sources/linenoise/Makefile                    |    7 -
 Sources/linenoise/README.markdown             |  229 ----
 Sources/linenoise/include/linenoise.h         |   75 --
 Sources/linenoise/linenoise.c                 | 1199 -----------------
 Sources/lki/main.swift                        |  125 --
 .../LogicKitParserTests.swift                 |   85 --
 10 files changed, 8 insertions(+), 1902 deletions(-)
 delete mode 100644 Sources/LogicKitParser/Parser.swift
 delete mode 100644 Sources/linenoise/LICENSE
 delete mode 100644 Sources/linenoise/Makefile
 delete mode 100644 Sources/linenoise/README.markdown
 delete mode 100644 Sources/linenoise/include/linenoise.h
 delete mode 100644 Sources/linenoise/linenoise.c
 delete mode 100644 Sources/lki/main.swift
 delete mode 100644 Tests/LogicKitParserTests/LogicKitParserTests.swift

diff --git a/Package.swift b/Package.swift
index 3310605..c2999ba 100644
--- a/Package.swift
+++ b/Package.swift
@@ -3,21 +3,12 @@
 import PackageDescription
 
 let package = Package(
-    name: "LogicKit",
-    products: [
-        .library(name: "LogicKit", type: .static, targets: ["LogicKit"]),
-        .executable(name: "lki", targets: ["lki"]),
-    ],
-    dependencies: [
-        .package(url: "https://github.com/rxwei/Parsey.git", .revision("32f653044f95c880cd0cce929cfef29efb07ee5b")),
-    ],
-    targets: [
-        .target(name: "LogicKit"),
-        .target(name: "LogicKitParser", dependencies: ["LogicKit", "Parsey"]),
-        .target(name: "lki", dependencies: ["LogicKit", "LogicKitParser", "linenoise"]),
-        .target(name: "linenoise"),
-
-        .testTarget(name: "LogicKitTests", dependencies: ["LogicKit"]),
-        .testTarget(name: "LogicKitParserTests", dependencies: ["LogicKit", "LogicKitParser"]),
-    ]
+  name: "LogicKit",
+  products: [
+    .library(name: "LogicKit", type: .static, targets: ["LogicKit"]),
+  ],
+  targets: [
+    .target(name: "LogicKit"),
+    .testTarget(name: "LogicKitTests", dependencies: ["LogicKit"]),
+  ]
 )
diff --git a/README.md b/README.md
index 6d68cdf..8ae288d 100644
--- a/README.md
+++ b/README.md
@@ -217,46 +217,6 @@ import LogicKit
 > The schemes of the auto-generated package might require some manual configuration.
 > Please refer to Xcode's documentation for more information on that end.
 
-### Using the interpreter
-
-LogicKit comes with an interpreter, `lki`,
-that you can use to design and/or debug knowledge bases.
-To use the interpreter, first clone this repository:
-
-```bash
-git clone git@github.com:kyouko-taiga/LogicKit.git
-```
-
-You can then compile `lki`:
-
-```bash
-swift build --configuration release --product lki
-```
-
-Which will create a binary `lki` in `.build/release/`.
-Feel free to symlink copy or symlink this binary to include it in your path.
-
-To use `lki`, first write your knowledge base in some file, for instance `nat.kb`:
-
-```swift
-.fact("add", zero, y, y),
-.rule("add", .fact("succ", x), y, z) {
-  .fact("add", x, .fact("succ", y), z)
-}
-```
-
-Then, invoke the interpreter with a path to your knowledge base:
-
-```bash
-lki /path/to/nat.kb
-```
-
-You'll be presented a prompt that lets you issue queries against your knowledge base.
-
-> Note that `lki` can only read knowledge bases written with the LogicKit syntax,
-> meaning that you can't use the full power of Swift
-> like you would be able to in actual Swift sources.
-
 ## License
 
 LogicKit is licensed under the MIT License.
diff --git a/Sources/LogicKitParser/Parser.swift b/Sources/LogicKitParser/Parser.swift
deleted file mode 100644
index 0fc9309..0000000
--- a/Sources/LogicKitParser/Parser.swift
+++ /dev/null
@@ -1,100 +0,0 @@
-import LogicKit
-import Parsey
-
-@available(swift, deprecated: 4.1)
-public struct Grammar {
-
-    // MARK: Knowledge base (entry point of the grammar)
-
-    public static let knowledge = newlines.? ~~> statement.*
-    public static let statement = (term | rule).amid(ws.?) <~~ terminator
-
-    public static let terminator =
-        (comma.amid(ws.?) <~~ newlines).skipped()
-        | newlines.skipped()
-        | Lexer.end.skipped()
-
-    // MARK: Variables
-
-    public static let variable =
-        ".var(" ~~> string.amid(ws.?) <~~ ")"
-        <!-- "a variable"
-        ^^ { Term.var($0) }
-
-    // MARK: Literals
-
-    public static let literal =
-        ".lit(" ~~> (intLiteral | boolLiteral | strLiteral).amid(ws.?) <~~ ")"
-
-    public static let intLiteral =
-        Lexer.signedInteger <!-- "an integer literal"
-        ^^ { Term.lit(Int($0)!) }
-
-    public static let boolLiteral =
-        (Lexer.token("true") | Lexer.token("false")) <!-- "a bool literal"
-        ^^ { Term.lit($0 == "true") }
-
-    public static let strLiteral =
-        string <!-- "a string literal"
-        ^^ { Term.lit($0) }
-
-    // MARK: Terms
-
-    public static let term = disjunction
-
-    public static let disjunction = conjunction.amid(ws.?).infixedLeft(by: orOperator)
-    public static let orOperator  =
-        Lexer.token("||").amid(newlines.?)
-        <!-- "an or operator"
-        ^^ { _ in { Term.disjunction($0, $1) } }
-
-    public static let conjunction = atom.amid(ws.?).infixedLeft(by: andOperator)
-    public static let andOperator =
-        Lexer.token("&&").amid(newlines.?)
-        <!-- "an and operator"
-        ^^ { _ in { Term.conjunction($0, $1) } }
-
-    public static let atom = variable | literal | fact
-
-    public static let fact: Parser<Term> =
-        ".fact(" ~~> string.amid(ws.?) ~~ (comma ~~> arguments).? <~~ ")"
-        <!-- "a fact"
-        ^^ { val in ._term(name: val.0, arguments: val.1 ?? []) }
-
-    public static let arguments =
-        (variable | literal | fact).many(separatedBy: comma) <~~ ws.?
-        <!-- "a subterm"
-
-    // MARK: Rules
-
-    public static let rule: Parser<Term> =
-        (".rule(" ~~> string.amid(ws.?) ~~ (comma ~~> arguments).? <~~ ")") ~~
-        (lbrace ~~> term.amid(ws.?).amid(newlines.?) <~~ rbrace)
-        //(lbrace ~~> term.amid(ws.?) <~~ rbrace)
-        ^^ { val in ._rule(name: val.0.0, arguments: val.0.1 ?? [], body: val.1) }
-
-    public static let lbrace = Lexer.character("{").amid(ws.?)
-    public static let rbrace = Lexer.character("}").amid(ws.?)
-
-    // MARK: Other terminal symbols
-
-    public static let string =
-        Lexer.regex("\"[^\"\\\\]*(\\\\.[^\"\\\\]*)*\"")
-        ^^ { $0[1 ..< ($0.count - 1)] }
-
-    public static let comment  = Lexer.regex("\\//[^\\n]*")
-    public static let ws       = Lexer.whitespaces
-    public static let newlines = (Lexer.newLine | ws.? ~~> comment).+
-    public static let comma    = Lexer.character(",").amid(ws.?)
-
-}
-
-extension String {
-
-    subscript (bounds: CountableRange<Int>) -> String {
-        let start = index(startIndex, offsetBy: bounds.lowerBound)
-        let end   = index(startIndex, offsetBy: bounds.upperBound)
-        return String(self[start ..< end])
-    }
-
-}
diff --git a/Sources/linenoise/LICENSE b/Sources/linenoise/LICENSE
deleted file mode 100644
index 18e8148..0000000
--- a/Sources/linenoise/LICENSE
+++ /dev/null
@@ -1,25 +0,0 @@
-Copyright (c) 2010-2014, Salvatore Sanfilippo <antirez at gmail dot com>
-Copyright (c) 2010-2013, Pieter Noordhuis <pcnoordhuis at gmail dot com>
-
-All rights reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are met:
-
-* Redistributions of source code must retain the above copyright notice,
-  this list of conditions and the following disclaimer.
-
-* Redistributions in binary form must reproduce the above copyright notice,
-  this list of conditions and the following disclaimer in the documentation
-  and/or other materials provided with the distribution.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
-ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
-WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR
-ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
-(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
-ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Sources/linenoise/Makefile b/Sources/linenoise/Makefile
deleted file mode 100644
index a285410..0000000
--- a/Sources/linenoise/Makefile
+++ /dev/null
@@ -1,7 +0,0 @@
-linenoise_example: linenoise.h linenoise.c
-
-linenoise_example: linenoise.c example.c
-	$(CC) -Wall -W -Os -g -o linenoise_example linenoise.c example.c
-
-clean:
-	rm -f linenoise_example
diff --git a/Sources/linenoise/README.markdown b/Sources/linenoise/README.markdown
deleted file mode 100644
index feaa356..0000000
--- a/Sources/linenoise/README.markdown
+++ /dev/null
@@ -1,229 +0,0 @@
-# Linenoise
-
-A minimal, zero-config, BSD licensed, readline replacement used in Redis,
-MongoDB, and Android.
-
-* Single and multi line editing mode with the usual key bindings implemented.
-* History handling.
-* Completion.
-* Hints (suggestions at the right of the prompt as you type).
-* About 1,100 lines of BSD license source code.
-* Only uses a subset of VT100 escapes (ANSI.SYS compatible).
-
-## Can a line editing library be 20k lines of code?
-
-Line editing with some support for history is a really important feature for command line utilities. Instead of retyping almost the same stuff again and again it's just much better to hit the up arrow and edit on syntax errors, or in order to try a slightly different command. But apparently code dealing with terminals is some sort of Black Magic: readline is 30k lines of code, libedit 20k. Is it reasonable to link small utilities to huge libraries just to get a minimal support for line editing?
-
-So what usually happens is either:
-
- * Large programs with configure scripts disabling line editing if readline is not present in the system, or not supporting it at all since readline is GPL licensed and libedit (the BSD clone) is not as known and available as readline is (Real world example of this problem: Tclsh).
- * Smaller programs not using a configure script not supporting line editing at all (A problem we had with Redis-cli for instance).
- 
-The result is a pollution of binaries without line editing support.
-
-So I spent more or less two hours doing a reality check resulting in this little library: is it *really* needed for a line editing library to be 20k lines of code? Apparently not, it is possibe to get a very small, zero configuration, trivial to embed library, that solves the problem. Smaller programs will just include this, supporing line editing out of the box. Larger programs may use this little library or just checking with configure if readline/libedit is available and resorting to Linenoise if not.
-
-## Terminals, in 2010.
-
-Apparently almost every terminal you can happen to use today has some kind of support for basic VT100 escape sequences. So I tried to write a lib using just very basic VT100 features. The resulting library appears to work everywhere I tried to use it, and now can work even on ANSI.SYS compatible terminals, since no
-VT220 specific sequences are used anymore.
-
-The library is currently about 1100 lines of code. In order to use it in your project just look at the *example.c* file in the source distribution, it is trivial. Linenoise is BSD code, so you can use both in free software and commercial software.
-
-## Tested with...
-
- * Linux text only console ($TERM = linux)
- * Linux KDE terminal application ($TERM = xterm)
- * Linux xterm ($TERM = xterm)
- * Linux Buildroot ($TERM = vt100)
- * Mac OS X iTerm ($TERM = xterm)
- * Mac OS X default Terminal.app ($TERM = xterm)
- * OpenBSD 4.5 through an OSX Terminal.app ($TERM = screen)
- * IBM AIX 6.1
- * FreeBSD xterm ($TERM = xterm)
- * ANSI.SYS
- * Emacs comint mode ($TERM = dumb)
-
-Please test it everywhere you can and report back!
-
-## Let's push this forward!
-
-Patches should be provided in the respect of Linenoise sensibility for small
-easy to understand code.
-
-Send feedbacks to antirez at gmail
-
-# The API
-
-Linenoise is very easy to use, and reading the example shipped with the
-library should get you up to speed ASAP. Here is a list of API calls
-and how to use them.
-
-    char *linenoise(const char *prompt);
-
-This is the main Linenoise call: it shows the user a prompt with line editing
-and history capabilities. The prompt you specify is used as a prompt, that is,
-it will be printed to the left of the cursor. The library returns a buffer
-with the line composed by the user, or NULL on end of file or when there
-is an out of memory condition.
-
-When a tty is detected (the user is actually typing into a terminal session)
-the maximum editable line length is `LINENOISE_MAX_LINE`. When instead the
-standard input is not a tty, which happens every time you redirect a file
-to a program, or use it in an Unix pipeline, there are no limits to the
-length of the line that can be returned.
-
-The returned line should be freed with the `free()` standard system call.
-However sometimes it could happen that your program uses a different dynamic
-allocation library, so you may also used `linenoiseFree` to make sure the
-line is freed with the same allocator it was created.
-
-The canonical loop used by a program using Linenoise will be something like
-this:
-
-    while((line = linenoise("hello> ")) != NULL) {
-        printf("You wrote: %s\n", line);
-        linenoiseFree(line); /* Or just free(line) if you use libc malloc. */
-    }
-
-## Single line VS multi line editing
-
-By default, Linenoise uses single line editing, that is, a single row on the
-screen will be used, and as the user types more, the text will scroll towards
-left to make room. This works if your program is one where the user is
-unlikely to write a lot of text, otherwise multi line editing, where multiple
-screens rows are used, can be a lot more comfortable.
-
-In order to enable multi line editing use the following API call:
-
-    linenoiseSetMultiLine(1);
-
-You can disable it using `0` as argument.
-
-## History
-
-Linenoise supporst history, so that the user does not have to retype
-again and again the same things, but can use the down and up arrows in order
-to search and re-edit already inserted lines of text.
-
-The followings are the history API calls:
-
-    int linenoiseHistoryAdd(const char *line);
-    int linenoiseHistorySetMaxLen(int len);
-    int linenoiseHistorySave(const char *filename);
-    int linenoiseHistoryLoad(const char *filename);
-
-Use `linenoiseHistoryAdd` every time you want to add a new element
-to the top of the history (it will be the first the user will see when
-using the up arrow).
-
-Note that for history to work, you have to set a length for the history
-(which is zero by default, so history will be disabled if you don't set
-a proper one). This is accomplished using the `linenoiseHistorySetMaxLen`
-function.
-
-Linenoise has direct support for persisting the history into an history
-file. The functions `linenoiseHistorySave` and `linenoiseHistoryLoad` do
-just that. Both functions return -1 on error and 0 on success.
-
-## Completion
-
-Linenoise supports completion, which is the ability to complete the user
-input when she or he presses the `<TAB>` key.
-
-In order to use completion, you need to register a completion callback, which
-is called every time the user presses `<TAB>`. Your callback will return a
-list of items that are completions for the current string.
-
-The following is an example of registering a completion callback:
-
-    linenoiseSetCompletionCallback(completion);
-
-The completion must be a function returning `void` and getting as input
-a `const char` pointer, which is the line the user has typed so far, and
-a `linenoiseCompletions` object pointer, which is used as argument of
-`linenoiseAddCompletion` in order to add completions inside the callback.
-An example will make it more clear:
-
-    void completion(const char *buf, linenoiseCompletions *lc) {
-        if (buf[0] == 'h') {
-            linenoiseAddCompletion(lc,"hello");
-            linenoiseAddCompletion(lc,"hello there");
-        }
-    }
-
-Basically in your completion callback, you inspect the input, and return
-a list of items that are good completions by using `linenoiseAddCompletion`.
-
-If you want to test the completion feature, compile the example program
-with `make`, run it, type `h` and press `<TAB>`.
-
-## Hints
-
-Linenoise has a feature called *hints* which is very useful when you
-use Linenoise in order to implement a REPL (Read Eval Print Loop) for
-a program that accepts commands and arguments, but may also be useful in
-other conditions.
-
-The feature shows, on the right of the cursor, as the user types, hints that
-may be useful. The hints can be displayed using a different color compared
-to the color the user is typing, and can also be bold.
-
-For example as the user starts to type `"git remote add"`, with hints it's
-possible to show on the right of the prompt a string `<name> <url>`.
-
-The feature works similarly to the history feature, using a callback.
-To register the callback we use:
-
-    linenoiseSetHintsCallback(hints);
-
-The callback itself is implemented like this:
-
-    char *hints(const char *buf, int *color, int *bold) {
-        if (!strcasecmp(buf,"git remote add")) {
-            *color = 35;
-            *bold = 0;
-            return " <name> <url>";
-        }
-        return NULL;
-    }
-
-The callback function returns the string that should be displayed or NULL
-if no hint is available for the text the user currently typed. The returned
-string will be trimmed as needed depending on the number of columns available
-on the screen.
-
-It is possible to return a string allocated in dynamic way, by also registering
-a function to deallocate the hint string once used:
-
-    void linenoiseSetFreeHintsCallback(linenoiseFreeHintsCallback *);
-
-The free hint callback will just receive the pointer and free the string
-as needed (depending on how the hits callback allocated it).
-
-As you can see in the example above, a `color` (in xterm color terminal codes)
-can be provided together with a `bold` attribute. If no color is set, the
-current terminal foreground color is used. If no bold attribute is set,
-non-bold text is printed.
-
-Color codes are:
-
-    red = 31
-    green = 32
-    yellow = 33
-    blue = 34
-    magenta = 35
-    cyan = 36
-    white = 37;
-
-## Screen handling
-
-Sometimes you may want to clear the screen as a result of something the
-user typed. You can do this by calling the following function:
-
-    void linenoiseClearScreen(void);
-
-## Related projects
-
-* [Linenoise NG](https://github.com/arangodb/linenoise-ng) is a fork of Linenoise that aims to add more advanced features like UTF-8 support, Windows support and other features. Uses C++ instead of C as development language.
-* [Linenoise-swift](https://github.com/andybest/linenoise-swift) is a reimplementation of Linenoise written in Swift.
diff --git a/Sources/linenoise/include/linenoise.h b/Sources/linenoise/include/linenoise.h
deleted file mode 100644
index c388e25..0000000
--- a/Sources/linenoise/include/linenoise.h
+++ /dev/null
@@ -1,75 +0,0 @@
-/* linenoise.h -- VERSION 1.0
- *
- * Guerrilla line editing library against the idea that a line editing lib
- * needs to be 20,000 lines of C code.
- *
- * See linenoise.c for more information.
- *
- * ------------------------------------------------------------------------
- *
- * Copyright (c) 2010-2014, Salvatore Sanfilippo <antirez at gmail dot com>
- * Copyright (c) 2010-2013, Pieter Noordhuis <pcnoordhuis at gmail dot com>
- *
- * All rights reserved.
- *
- * Redistribution and use in source and binary forms, with or without
- * modification, are permitted provided that the following conditions are
- * met:
- *
- *  *  Redistributions of source code must retain the above copyright
- *     notice, this list of conditions and the following disclaimer.
- *
- *  *  Redistributions in binary form must reproduce the above copyright
- *     notice, this list of conditions and the following disclaimer in the
- *     documentation and/or other materials provided with the distribution.
- *
- * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
- * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
- * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
- * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
- * HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
- * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
- * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
- * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
- * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
- * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
- * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
- */
-
-#ifndef __LINENOISE_H
-#define __LINENOISE_H
-
-#include <stddef.h>
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-typedef struct linenoiseCompletions {
-  size_t len;
-  char **cvec;
-} linenoiseCompletions;
-
-typedef void(linenoiseCompletionCallback)(const char *, linenoiseCompletions *);
-typedef char*(linenoiseHintsCallback)(const char *, int *color, int *bold);
-typedef void(linenoiseFreeHintsCallback)(void *);
-void linenoiseSetCompletionCallback(linenoiseCompletionCallback *);
-void linenoiseSetHintsCallback(linenoiseHintsCallback *);
-void linenoiseSetFreeHintsCallback(linenoiseFreeHintsCallback *);
-void linenoiseAddCompletion(linenoiseCompletions *, const char *);
-
-char *linenoise(const char *prompt);
-void linenoiseFree(void *ptr);
-int linenoiseHistoryAdd(const char *line);
-int linenoiseHistorySetMaxLen(int len);
-int linenoiseHistorySave(const char *filename);
-int linenoiseHistoryLoad(const char *filename);
-void linenoiseClearScreen(void);
-void linenoiseSetMultiLine(int ml);
-void linenoisePrintKeyCodes(void);
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif /* __LINENOISE_H */
diff --git a/Sources/linenoise/linenoise.c b/Sources/linenoise/linenoise.c
deleted file mode 100644
index b8996f2..0000000
--- a/Sources/linenoise/linenoise.c
+++ /dev/null
@@ -1,1199 +0,0 @@
-/* linenoise.c -- guerrilla line editing library against the idea that a
- * line editing lib needs to be 20,000 lines of C code.
- *
- * You can find the latest source code at:
- *
- *   http://github.com/antirez/linenoise
- *
- * Does a number of crazy assumptions that happen to be true in 99.9999% of
- * the 2010 UNIX computers around.
- *
- * ------------------------------------------------------------------------
- *
- * Copyright (c) 2010-2016, Salvatore Sanfilippo <antirez at gmail dot com>
- * Copyright (c) 2010-2013, Pieter Noordhuis <pcnoordhuis at gmail dot com>
- *
- * All rights reserved.
- *
- * Redistribution and use in source and binary forms, with or without
- * modification, are permitted provided that the following conditions are
- * met:
- *
- *  *  Redistributions of source code must retain the above copyright
- *     notice, this list of conditions and the following disclaimer.
- *
- *  *  Redistributions in binary form must reproduce the above copyright
- *     notice, this list of conditions and the following disclaimer in the
- *     documentation and/or other materials provided with the distribution.
- *
- * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
- * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
- * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
- * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
- * HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
- * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
- * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
- * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
- * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
- * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
- * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
- *
- * ------------------------------------------------------------------------
- *
- * References:
- * - http://invisible-island.net/xterm/ctlseqs/ctlseqs.html
- * - http://www.3waylabs.com/nw/WWW/products/wizcon/vt220.html
- *
- * Todo list:
- * - Filter bogus Ctrl+<char> combinations.
- * - Win32 support
- *
- * Bloat:
- * - History search like Ctrl+r in readline?
- *
- * List of escape sequences used by this program, we do everything just
- * with three sequences. In order to be so cheap we may have some
- * flickering effect with some slow terminal, but the lesser sequences
- * the more compatible.
- *
- * EL (Erase Line)
- *    Sequence: ESC [ n K
- *    Effect: if n is 0 or missing, clear from cursor to end of line
- *    Effect: if n is 1, clear from beginning of line to cursor
- *    Effect: if n is 2, clear entire line
- *
- * CUF (CUrsor Forward)
- *    Sequence: ESC [ n C
- *    Effect: moves cursor forward n chars
- *
- * CUB (CUrsor Backward)
- *    Sequence: ESC [ n D
- *    Effect: moves cursor backward n chars
- *
- * The following is used to get the terminal width if getting
- * the width with the TIOCGWINSZ ioctl fails
- *
- * DSR (Device Status Report)
- *    Sequence: ESC [ 6 n
- *    Effect: reports the current cusor position as ESC [ n ; m R
- *            where n is the row and m is the column
- *
- * When multi line mode is enabled, we also use an additional escape
- * sequence. However multi line editing is disabled by default.
- *
- * CUU (Cursor Up)
- *    Sequence: ESC [ n A
- *    Effect: moves cursor up of n chars.
- *
- * CUD (Cursor Down)
- *    Sequence: ESC [ n B
- *    Effect: moves cursor down of n chars.
- *
- * When linenoiseClearScreen() is called, two additional escape sequences
- * are used in order to clear the screen and position the cursor at home
- * position.
- *
- * CUP (Cursor position)
- *    Sequence: ESC [ H
- *    Effect: moves the cursor to upper left corner
- *
- * ED (Erase display)
- *    Sequence: ESC [ 2 J
- *    Effect: clear the whole screen
- *
- */
-
-#include <termios.h>
-#include <unistd.h>
-#include <stdlib.h>
-#include <stdio.h>
-#include <errno.h>
-#include <string.h>
-#include <stdlib.h>
-#include <ctype.h>
-#include <sys/stat.h>
-#include <sys/types.h>
-#include <sys/ioctl.h>
-#include <unistd.h>
-#include "linenoise.h"
-
-#define LINENOISE_DEFAULT_HISTORY_MAX_LEN 100
-#define LINENOISE_MAX_LINE 4096
-static char *unsupported_term[] = {"dumb","cons25","emacs",NULL};
-static linenoiseCompletionCallback *completionCallback = NULL;
-static linenoiseHintsCallback *hintsCallback = NULL;
-static linenoiseFreeHintsCallback *freeHintsCallback = NULL;
-
-static struct termios orig_termios; /* In order to restore at exit.*/
-static int rawmode = 0; /* For atexit() function to check if restore is needed*/
-static int mlmode = 0;  /* Multi line mode. Default is single line. */
-static int atexit_registered = 0; /* Register atexit just 1 time. */
-static int history_max_len = LINENOISE_DEFAULT_HISTORY_MAX_LEN;
-static int history_len = 0;
-static char **history = NULL;
-
-/* The linenoiseState structure represents the state during line editing.
- * We pass this state to functions implementing specific editing
- * functionalities. */
-struct linenoiseState {
-    int ifd;            /* Terminal stdin file descriptor. */
-    int ofd;            /* Terminal stdout file descriptor. */
-    char *buf;          /* Edited line buffer. */
-    size_t buflen;      /* Edited line buffer size. */
-    const char *prompt; /* Prompt to display. */
-    size_t plen;        /* Prompt length. */
-    size_t pos;         /* Current cursor position. */
-    size_t oldpos;      /* Previous refresh cursor position. */
-    size_t len;         /* Current edited line length. */
-    size_t cols;        /* Number of columns in terminal. */
-    size_t maxrows;     /* Maximum num of rows used so far (multiline mode) */
-    int history_index;  /* The history index we are currently editing. */
-};
-
-enum KEY_ACTION{
-	LN_KEY_NULL = 0,	   /* NULL */
-	LN_CTRL_A = 1,         /* Ctrl+a */
-	LN_CTRL_B = 2,         /* Ctrl-b */
-	LN_CTRL_C = 3,         /* Ctrl-c */
-	LN_CTRL_D = 4,         /* Ctrl-d */
-	LN_CTRL_E = 5,         /* Ctrl-e */
-	LN_CTRL_F = 6,         /* Ctrl-f */
-	LN_CTRL_H = 8,         /* Ctrl-h */
-	LN_TAB = 9,            /* Tab */
-	LN_CTRL_K = 11,        /* Ctrl+k */
-	LN_CTRL_L = 12,        /* Ctrl+l */
-	LN_ENTER = 13,         /* Enter */
-	LN_CTRL_N = 14,        /* Ctrl-n */
-	LN_CTRL_P = 16,        /* Ctrl-p */
-	LN_CTRL_T = 20,        /* Ctrl-t */
-	LN_CTRL_U = 21,        /* Ctrl+u */
-	LN_CTRL_W = 23,        /* Ctrl+w */
-	LN_ESC = 27,           /* Escape */
-	LN_BACKSPACE =  127    /* Backspace */
-};
-
-static void linenoiseAtExit(void);
-int linenoiseHistoryAdd(const char *line);
-static void refreshLine(struct linenoiseState *l);
-
-/* Debugging macro. */
-#if 0
-FILE *lndebug_fp = NULL;
-#define lndebug(...) \
-    do { \
-        if (lndebug_fp == NULL) { \
-            lndebug_fp = fopen("/tmp/lndebug.txt","a"); \
-            fprintf(lndebug_fp, \
-            "[%d %d %d] p: %d, rows: %d, rpos: %d, max: %d, oldmax: %d\n", \
-            (int)l->len,(int)l->pos,(int)l->oldpos,plen,rows,rpos, \
-            (int)l->maxrows,old_rows); \
-        } \
-        fprintf(lndebug_fp, ", " __VA_ARGS__); \
-        fflush(lndebug_fp); \
-    } while (0)
-#else
-#define lndebug(fmt, ...)
-#endif
-
-/* ======================= Low level terminal handling ====================== */
-
-/* Set if to use or not the multi line mode. */
-void linenoiseSetMultiLine(int ml) {
-    mlmode = ml;
-}
-
-/* Return true if the terminal name is in the list of terminals we know are
- * not able to understand basic escape sequences. */
-static int isUnsupportedTerm(void) {
-    char *term = getenv("TERM");
-    int j;
-
-    if (term == NULL) return 0;
-    for (j = 0; unsupported_term[j]; j++)
-        if (!strcasecmp(term,unsupported_term[j])) return 1;
-    return 0;
-}
-
-/* Raw mode: 1960 magic shit. */
-static int enableRawMode(int fd) {
-    struct termios raw;
-
-    if (!isatty(STDIN_FILENO)) goto fatal;
-    if (!atexit_registered) {
-        atexit(linenoiseAtExit);
-        atexit_registered = 1;
-    }
-    if (tcgetattr(fd,&orig_termios) == -1) goto fatal;
-
-    raw = orig_termios;  /* modify the original mode */
-    /* input modes: no break, no CR to NL, no parity check, no strip char,
-     * no start/stop output control. */
-    raw.c_iflag &= ~(BRKINT | ICRNL | INPCK | ISTRIP | IXON);
-    /* output modes - disable post processing */
-    raw.c_oflag &= ~(OPOST);
-    /* control modes - set 8 bit chars */
-    raw.c_cflag |= (CS8);
-    /* local modes - choing off, canonical off, no extended functions,
-     * no signal chars (^Z,^C) */
-    raw.c_lflag &= ~(ECHO | ICANON | IEXTEN | ISIG);
-    /* control chars - set return condition: min number of bytes and timer.
-     * We want read to return every single byte, without timeout. */
-    raw.c_cc[VMIN] = 1; raw.c_cc[VTIME] = 0; /* 1 byte, no timer */
-
-    /* put terminal in raw mode after flushing */
-    if (tcsetattr(fd,TCSAFLUSH,&raw) < 0) goto fatal;
-    rawmode = 1;
-    return 0;
-
-fatal:
-    errno = ENOTTY;
-    return -1;
-}
-
-static void disableRawMode(int fd) {
-    /* Don't even check the return value as it's too late. */
-    if (rawmode && tcsetattr(fd,TCSAFLUSH,&orig_termios) != -1)
-        rawmode = 0;
-}
-
-/* Use the ESC [6n escape sequence to query the horizontal cursor position
- * and return it. On error -1 is returned, on success the position of the
- * cursor. */
-static int getCursorPosition(int ifd, int ofd) {
-    char buf[32];
-    int cols, rows;
-    unsigned int i = 0;
-
-    /* Report cursor location */
-    if (write(ofd, "\x1b[6n", 4) != 4) return -1;
-
-    /* Read the response: ESC [ rows ; cols R */
-    while (i < sizeof(buf)-1) {
-        if (read(ifd,buf+i,1) != 1) break;
-        if (buf[i] == 'R') break;
-        i++;
-    }
-    buf[i] = '\0';
-
-    /* Parse it. */
-    if (buf[0] != LN_ESC || buf[1] != '[') return -1;
-    if (sscanf(buf+2,"%d;%d",&rows,&cols) != 2) return -1;
-    return cols;
-}
-
-/* Try to get the number of columns in the current terminal, or assume 80
- * if it fails. */
-static int getColumns(int ifd, int ofd) {
-    struct winsize ws;
-
-    if (ioctl(1, TIOCGWINSZ, &ws) == -1 || ws.ws_col == 0) {
-        /* ioctl() failed. Try to query the terminal itself. */
-        int start, cols;
-
-        /* Get the initial position so we can restore it later. */
-        start = getCursorPosition(ifd,ofd);
-        if (start == -1) goto failed;
-
-        /* Go to right margin and get position. */
-        if (write(ofd,"\x1b[999C",6) != 6) goto failed;
-        cols = getCursorPosition(ifd,ofd);
-        if (cols == -1) goto failed;
-
-        /* Restore position. */
-        if (cols > start) {
-            char seq[32];
-            snprintf(seq,32,"\x1b[%dD",cols-start);
-            if (write(ofd,seq,strlen(seq)) == -1) {
-                /* Can't recover... */
-            }
-        }
-        return cols;
-    } else {
-        return ws.ws_col;
-    }
-
-failed:
-    return 80;
-}
-
-/* Clear the screen. Used to handle ctrl+l */
-void linenoiseClearScreen(void) {
-    if (write(STDOUT_FILENO,"\x1b[H\x1b[2J",7) <= 0) {
-        /* nothing to do, just to avoid warning. */
-    }
-}
-
-/* Beep, used for completion when there is nothing to complete or when all
- * the choices were already shown. */
-static void linenoiseBeep(void) {
-    fprintf(stderr, "\x7");
-    fflush(stderr);
-}
-
-/* ============================== Completion ================================ */
-
-/* Free a list of completion option populated by linenoiseAddCompletion(). */
-static void freeCompletions(linenoiseCompletions *lc) {
-    size_t i;
-    for (i = 0; i < lc->len; i++)
-        free(lc->cvec[i]);
-    if (lc->cvec != NULL)
-        free(lc->cvec);
-}
-
-/* This is an helper function for linenoiseEdit() and is called when the
- * user types the <tab> key in order to complete the string currently in the
- * input.
- *
- * The state of the editing is encapsulated into the pointed linenoiseState
- * structure as described in the structure definition. */
-static int completeLine(struct linenoiseState *ls) {
-    linenoiseCompletions lc = { 0, NULL };
-    int nread, nwritten;
-    char c = 0;
-
-    completionCallback(ls->buf,&lc);
-    if (lc.len == 0) {
-        linenoiseBeep();
-    } else {
-        size_t stop = 0, i = 0;
-
-        while(!stop) {
-            /* Show completion or original buffer */
-            if (i < lc.len) {
-                struct linenoiseState saved = *ls;
-
-                ls->len = ls->pos = strlen(lc.cvec[i]);
-                ls->buf = lc.cvec[i];
-                refreshLine(ls);
-                ls->len = saved.len;
-                ls->pos = saved.pos;
-                ls->buf = saved.buf;
-            } else {
-                refreshLine(ls);
-            }
-
-            nread = read(ls->ifd,&c,1);
-            if (nread <= 0) {
-                freeCompletions(&lc);
-                return -1;
-            }
-
-            switch(c) {
-                case 9: /* tab */
-                    i = (i+1) % (lc.len+1);
-                    if (i == lc.len) linenoiseBeep();
-                    break;
-                case 27: /* escape */
-                    /* Re-show original buffer */
-                    if (i < lc.len) refreshLine(ls);
-                    stop = 1;
-                    break;
-                default:
-                    /* Update buffer and return */
-                    if (i < lc.len) {
-                        nwritten = snprintf(ls->buf,ls->buflen,"%s",lc.cvec[i]);
-                        ls->len = ls->pos = nwritten;
-                    }
-                    stop = 1;
-                    break;
-            }
-        }
-    }
-
-    freeCompletions(&lc);
-    return c; /* Return last read character */
-}
-
-/* Register a callback function to be called for tab-completion. */
-void linenoiseSetCompletionCallback(linenoiseCompletionCallback *fn) {
-    completionCallback = fn;
-}
-
-/* Register a hits function to be called to show hits to the user at the
- * right of the prompt. */
-void linenoiseSetHintsCallback(linenoiseHintsCallback *fn) {
-    hintsCallback = fn;
-}
-
-/* Register a function to free the hints returned by the hints callback
- * registered with linenoiseSetHintsCallback(). */
-void linenoiseSetFreeHintsCallback(linenoiseFreeHintsCallback *fn) {
-    freeHintsCallback = fn;
-}
-
-/* This function is used by the callback function registered by the user
- * in order to add completion options given the input string when the
- * user typed <tab>. See the example.c source code for a very easy to
- * understand example. */
-void linenoiseAddCompletion(linenoiseCompletions *lc, const char *str) {
-    size_t len = strlen(str);
-    char *copy, **cvec;
-
-    copy = malloc(len+1);
-    if (copy == NULL) return;
-    memcpy(copy,str,len+1);
-    cvec = realloc(lc->cvec,sizeof(char*)*(lc->len+1));
-    if (cvec == NULL) {
-        free(copy);
-        return;
-    }
-    lc->cvec = cvec;
-    lc->cvec[lc->len++] = copy;
-}
-
-/* =========================== Line editing ================================= */
-
-/* We define a very simple "append buffer" structure, that is an heap
- * allocated string where we can append to. This is useful in order to
- * write all the escape sequences in a buffer and flush them to the standard
- * output in a single call, to avoid flickering effects. */
-struct abuf {
-    char *b;
-    int len;
-};
-
-static void abInit(struct abuf *ab) {
-    ab->b = NULL;
-    ab->len = 0;
-}
-
-static void abAppend(struct abuf *ab, const char *s, int len) {
-    char *new = realloc(ab->b,ab->len+len);
-
-    if (new == NULL) return;
-    memcpy(new+ab->len,s,len);
-    ab->b = new;
-    ab->len += len;
-}
-
-static void abFree(struct abuf *ab) {
-    free(ab->b);
-}
-
-/* Helper of refreshSingleLine() and refreshMultiLine() to show hints
- * to the right of the prompt. */
-void refreshShowHints(struct abuf *ab, struct linenoiseState *l, int plen) {
-    char seq[64];
-    if (hintsCallback && plen+l->len < l->cols) {
-        int color = -1, bold = 0;
-        char *hint = hintsCallback(l->buf,&color,&bold);
-        if (hint) {
-            int hintlen = strlen(hint);
-            int hintmaxlen = l->cols-(plen+l->len);
-            if (hintlen > hintmaxlen) hintlen = hintmaxlen;
-            if (bold == 1 && color == -1) color = 37;
-            if (color != -1 || bold != 0)
-                snprintf(seq,64,"\033[%d;%d;49m",bold,color);
-            abAppend(ab,seq,strlen(seq));
-            abAppend(ab,hint,hintlen);
-            if (color != -1 || bold != 0)
-                abAppend(ab,"\033[0m",4);
-            /* Call the function to free the hint returned. */
-            if (freeHintsCallback) freeHintsCallback(hint);
-        }
-    }
-}
-
-/* Single line low level line refresh.
- *
- * Rewrite the currently edited line accordingly to the buffer content,
- * cursor position, and number of columns of the terminal. */
-static void refreshSingleLine(struct linenoiseState *l) {
-    char seq[64];
-    size_t plen = strlen(l->prompt);
-    int fd = l->ofd;
-    char *buf = l->buf;
-    size_t len = l->len;
-    size_t pos = l->pos;
-    struct abuf ab;
-
-    while((plen+pos) >= l->cols) {
-        buf++;
-        len--;
-        pos--;
-    }
-    while (plen+len > l->cols) {
-        len--;
-    }
-
-    abInit(&ab);
-    /* Cursor to left edge */
-    snprintf(seq,64,"\r");
-    abAppend(&ab,seq,strlen(seq));
-    /* Write the prompt and the current buffer content */
-    abAppend(&ab,l->prompt,strlen(l->prompt));
-    abAppend(&ab,buf,len);
-    /* Show hits if any. */
-    refreshShowHints(&ab,l,plen);
-    /* Erase to right */
-    snprintf(seq,64,"\x1b[0K");
-    abAppend(&ab,seq,strlen(seq));
-    /* Move cursor to original position. */
-    snprintf(seq,64,"\r\x1b[%dC", (int)(pos+plen));
-    abAppend(&ab,seq,strlen(seq));
-    if (write(fd,ab.b,ab.len) == -1) {} /* Can't recover from write error. */
-    abFree(&ab);
-}
-
-/* Multi line low level line refresh.
- *
- * Rewrite the currently edited line accordingly to the buffer content,
- * cursor position, and number of columns of the terminal. */
-static void refreshMultiLine(struct linenoiseState *l) {
-    char seq[64];
-    int plen = strlen(l->prompt);
-    int rows = (plen+l->len+l->cols-1)/l->cols; /* rows used by current buf. */
-    int rpos = (plen+l->oldpos+l->cols)/l->cols; /* cursor relative row. */
-    int rpos2; /* rpos after refresh. */
-    int col; /* colum position, zero-based. */
-    int old_rows = l->maxrows;
-    int fd = l->ofd, j;
-    struct abuf ab;
-
-    /* Update maxrows if needed. */
-    if (rows > (int)l->maxrows) l->maxrows = rows;
-
-    /* First step: clear all the lines used before. To do so start by
-     * going to the last row. */
-    abInit(&ab);
-    if (old_rows-rpos > 0) {
-        lndebug("go down %d", old_rows-rpos);
-        snprintf(seq,64,"\x1b[%dB", old_rows-rpos);
-        abAppend(&ab,seq,strlen(seq));
-    }
-
-    /* Now for every row clear it, go up. */
-    for (j = 0; j < old_rows-1; j++) {
-        lndebug("clear+up");
-        snprintf(seq,64,"\r\x1b[0K\x1b[1A");
-        abAppend(&ab,seq,strlen(seq));
-    }
-
-    /* Clean the top line. */
-    lndebug("clear");
-    snprintf(seq,64,"\r\x1b[0K");
-    abAppend(&ab,seq,strlen(seq));
-
-    /* Write the prompt and the current buffer content */
-    abAppend(&ab,l->prompt,strlen(l->prompt));
-    abAppend(&ab,l->buf,l->len);
-
-    /* Show hits if any. */
-    refreshShowHints(&ab,l,plen);
-
-    /* If we are at the very end of the screen with our prompt, we need to
-     * emit a newline and move the prompt to the first column. */
-    if (l->pos &&
-        l->pos == l->len &&
-        (l->pos+plen) % l->cols == 0)
-    {
-        lndebug("<newline>");
-        abAppend(&ab,"\n",1);
-        snprintf(seq,64,"\r");
-        abAppend(&ab,seq,strlen(seq));
-        rows++;
-        if (rows > (int)l->maxrows) l->maxrows = rows;
-    }
-
-    /* Move cursor to right position. */
-    rpos2 = (plen+l->pos+l->cols)/l->cols; /* current cursor relative row. */
-    lndebug("rpos2 %d", rpos2);
-
-    /* Go up till we reach the expected positon. */
-    if (rows-rpos2 > 0) {
-        lndebug("go-up %d", rows-rpos2);
-        snprintf(seq,64,"\x1b[%dA", rows-rpos2);
-        abAppend(&ab,seq,strlen(seq));
-    }
-
-    /* Set column. */
-    col = (plen+(int)l->pos) % (int)l->cols;
-    lndebug("set col %d", 1+col);
-    if (col)
-        snprintf(seq,64,"\r\x1b[%dC", col);
-    else
-        snprintf(seq,64,"\r");
-    abAppend(&ab,seq,strlen(seq));
-
-    lndebug("\n");
-    l->oldpos = l->pos;
-
-    if (write(fd,ab.b,ab.len) == -1) {} /* Can't recover from write error. */
-    abFree(&ab);
-}
-
-/* Calls the two low level functions refreshSingleLine() or
- * refreshMultiLine() according to the selected mode. */
-static void refreshLine(struct linenoiseState *l) {
-    if (mlmode)
-        refreshMultiLine(l);
-    else
-        refreshSingleLine(l);
-}
-
-/* Insert the character 'c' at cursor current position.
- *
- * On error writing to the terminal -1 is returned, otherwise 0. */
-int linenoiseEditInsert(struct linenoiseState *l, char c) {
-    if (l->len < l->buflen) {
-        if (l->len == l->pos) {
-            l->buf[l->pos] = c;
-            l->pos++;
-            l->len++;
-            l->buf[l->len] = '\0';
-            if ((!mlmode && l->plen+l->len < l->cols && !hintsCallback)) {
-                /* Avoid a full update of the line in the
-                 * trivial case. */
-                if (write(l->ofd,&c,1) == -1) return -1;
-            } else {
-                refreshLine(l);
-            }
-        } else {
-            memmove(l->buf+l->pos+1,l->buf+l->pos,l->len-l->pos);
-            l->buf[l->pos] = c;
-            l->len++;
-            l->pos++;
-            l->buf[l->len] = '\0';
-            refreshLine(l);
-        }
-    }
-    return 0;
-}
-
-/* Move cursor on the left. */
-void linenoiseEditMoveLeft(struct linenoiseState *l) {
-    if (l->pos > 0) {
-        l->pos--;
-        refreshLine(l);
-    }
-}
-
-/* Move cursor on the right. */
-void linenoiseEditMoveRight(struct linenoiseState *l) {
-    if (l->pos != l->len) {
-        l->pos++;
-        refreshLine(l);
-    }
-}
-
-/* Move cursor to the start of the line. */
-void linenoiseEditMoveHome(struct linenoiseState *l) {
-    if (l->pos != 0) {
-        l->pos = 0;
-        refreshLine(l);
-    }
-}
-
-/* Move cursor to the end of the line. */
-void linenoiseEditMoveEnd(struct linenoiseState *l) {
-    if (l->pos != l->len) {
-        l->pos = l->len;
-        refreshLine(l);
-    }
-}
-
-/* Substitute the currently edited line with the next or previous history
- * entry as specified by 'dir'. */
-#define LINENOISE_HISTORY_NEXT 0
-#define LINENOISE_HISTORY_PREV 1
-void linenoiseEditHistoryNext(struct linenoiseState *l, int dir) {
-    if (history_len > 1) {
-        /* Update the current history entry before to
-         * overwrite it with the next one. */
-        free(history[history_len - 1 - l->history_index]);
-        history[history_len - 1 - l->history_index] = strdup(l->buf);
-        /* Show the new entry */
-        l->history_index += (dir == LINENOISE_HISTORY_PREV) ? 1 : -1;
-        if (l->history_index < 0) {
-            l->history_index = 0;
-            return;
-        } else if (l->history_index >= history_len) {
-            l->history_index = history_len-1;
-            return;
-        }
-        strncpy(l->buf,history[history_len - 1 - l->history_index],l->buflen);
-        l->buf[l->buflen-1] = '\0';
-        l->len = l->pos = strlen(l->buf);
-        refreshLine(l);
-    }
-}
-
-/* Delete the character at the right of the cursor without altering the cursor
- * position. Basically this is what happens with the "Delete" keyboard key. */
-void linenoiseEditDelete(struct linenoiseState *l) {
-    if (l->len > 0 && l->pos < l->len) {
-        memmove(l->buf+l->pos,l->buf+l->pos+1,l->len-l->pos-1);
-        l->len--;
-        l->buf[l->len] = '\0';
-        refreshLine(l);
-    }
-}
-
-/* Backspace implementation. */
-void linenoiseEditBackspace(struct linenoiseState *l) {
-    if (l->pos > 0 && l->len > 0) {
-        memmove(l->buf+l->pos-1,l->buf+l->pos,l->len-l->pos);
-        l->pos--;
-        l->len--;
-        l->buf[l->len] = '\0';
-        refreshLine(l);
-    }
-}
-
-/* Delete the previosu word, maintaining the cursor at the start of the
- * current word. */
-void linenoiseEditDeletePrevWord(struct linenoiseState *l) {
-    size_t old_pos = l->pos;
-    size_t diff;
-
-    while (l->pos > 0 && l->buf[l->pos-1] == ' ')
-        l->pos--;
-    while (l->pos > 0 && l->buf[l->pos-1] != ' ')
-        l->pos--;
-    diff = old_pos - l->pos;
-    memmove(l->buf+l->pos,l->buf+old_pos,l->len-old_pos+1);
-    l->len -= diff;
-    refreshLine(l);
-}
-
-/* This function is the core of the line editing capability of linenoise.
- * It expects 'fd' to be already in "raw mode" so that every key pressed
- * will be returned ASAP to read().
- *
- * The resulting string is put into 'buf' when the user type enter, or
- * when ctrl+d is typed.
- *
- * The function returns the length of the current buffer. */
-static int linenoiseEdit(int stdin_fd, int stdout_fd, char *buf, size_t buflen, const char *prompt)
-{
-    struct linenoiseState l;
-
-    /* Populate the linenoise state that we pass to functions implementing
-     * specific editing functionalities. */
-    l.ifd = stdin_fd;
-    l.ofd = stdout_fd;
-    l.buf = buf;
-    l.buflen = buflen;
-    l.prompt = prompt;
-    l.plen = strlen(prompt);
-    l.oldpos = l.pos = 0;
-    l.len = 0;
-    l.cols = getColumns(stdin_fd, stdout_fd);
-    l.maxrows = 0;
-    l.history_index = 0;
-
-    /* Buffer starts empty. */
-    l.buf[0] = '\0';
-    l.buflen--; /* Make sure there is always space for the nulterm */
-
-    /* The latest history entry is always our current buffer, that
-     * initially is just an empty string. */
-    linenoiseHistoryAdd("");
-
-    if (write(l.ofd,prompt,l.plen) == -1) return -1;
-    while(1) {
-        char c;
-        int nread;
-        char seq[3];
-
-        nread = read(l.ifd,&c,1);
-        if (nread <= 0) return l.len;
-
-        /* Only autocomplete when the callback is set. It returns < 0 when
-         * there was an error reading from fd. Otherwise it will return the
-         * character that should be handled next. */
-        if (c == 9 && completionCallback != NULL) {
-            c = completeLine(&l);
-            /* Return on errors */
-            if (c < 0) return l.len;
-            /* Read next character when 0 */
-            if (c == 0) continue;
-        }
-
-        switch(c) {
-        case LN_ENTER:    /* enter */
-            history_len--;
-            free(history[history_len]);
-            if (mlmode) linenoiseEditMoveEnd(&l);
-            if (hintsCallback) {
-                /* Force a refresh without hints to leave the previous
-                 * line as the user typed it after a newline. */
-                linenoiseHintsCallback *hc = hintsCallback;
-                hintsCallback = NULL;
-                refreshLine(&l);
-                hintsCallback = hc;
-            }
-            return (int)l.len;
-        case LN_CTRL_C:     /* ctrl-c */
-            errno = EAGAIN;
-            return -1;
-        case LN_BACKSPACE:   /* backspace */
-        case 8:     /* ctrl-h */
-            linenoiseEditBackspace(&l);
-            break;
-        case LN_CTRL_D:     /* ctrl-d, remove char at right of cursor, or if the
-                            line is empty, act as end-of-file. */
-            if (l.len > 0) {
-                linenoiseEditDelete(&l);
-            } else {
-                history_len--;
-                free(history[history_len]);
-                return -1;
-            }
-            break;
-        case LN_CTRL_T:    /* ctrl-t, swaps current character with previous. */
-            if (l.pos > 0 && l.pos < l.len) {
-                int aux = buf[l.pos-1];
-                buf[l.pos-1] = buf[l.pos];
-                buf[l.pos] = aux;
-                if (l.pos != l.len-1) l.pos++;
-                refreshLine(&l);
-            }
-            break;
-        case LN_CTRL_B:     /* ctrl-b */
-            linenoiseEditMoveLeft(&l);
-            break;
-        case LN_CTRL_F:     /* ctrl-f */
-            linenoiseEditMoveRight(&l);
-            break;
-        case LN_CTRL_P:    /* ctrl-p */
-            linenoiseEditHistoryNext(&l, LINENOISE_HISTORY_PREV);
-            break;
-        case LN_CTRL_N:    /* ctrl-n */
-            linenoiseEditHistoryNext(&l, LINENOISE_HISTORY_NEXT);
-            break;
-        case LN_ESC:    /* escape sequence */
-            /* Read the next two bytes representing the escape sequence.
-             * Use two calls to handle slow terminals returning the two
-             * chars at different times. */
-            if (read(l.ifd,seq,1) == -1) break;
-            if (read(l.ifd,seq+1,1) == -1) break;
-
-            /* ESC [ sequences. */
-            if (seq[0] == '[') {
-                if (seq[1] >= '0' && seq[1] <= '9') {
-                    /* Extended escape, read additional byte. */
-                    if (read(l.ifd,seq+2,1) == -1) break;
-                    if (seq[2] == '~') {
-                        switch(seq[1]) {
-                        case '3': /* Delete key. */
-                            linenoiseEditDelete(&l);
-                            break;
-                        }
-                    }
-                } else {
-                    switch(seq[1]) {
-                    case 'A': /* Up */
-                        linenoiseEditHistoryNext(&l, LINENOISE_HISTORY_PREV);
-                        break;
-                    case 'B': /* Down */
-                        linenoiseEditHistoryNext(&l, LINENOISE_HISTORY_NEXT);
-                        break;
-                    case 'C': /* Right */
-                        linenoiseEditMoveRight(&l);
-                        break;
-                    case 'D': /* Left */
-                        linenoiseEditMoveLeft(&l);
-                        break;
-                    case 'H': /* Home */
-                        linenoiseEditMoveHome(&l);
-                        break;
-                    case 'F': /* End*/
-                        linenoiseEditMoveEnd(&l);
-                        break;
-                    }
-                }
-            }
-
-            /* ESC O sequences. */
-            else if (seq[0] == 'O') {
-                switch(seq[1]) {
-                case 'H': /* Home */
-                    linenoiseEditMoveHome(&l);
-                    break;
-                case 'F': /* End*/
-                    linenoiseEditMoveEnd(&l);
-                    break;
-                }
-            }
-            break;
-        default:
-            if (linenoiseEditInsert(&l,c)) return -1;
-            break;
-        case LN_CTRL_U: /* Ctrl+u, delete the whole line. */
-            buf[0] = '\0';
-            l.pos = l.len = 0;
-            refreshLine(&l);
-            break;
-        case LN_CTRL_K: /* Ctrl+k, delete from current to end of line. */
-            buf[l.pos] = '\0';
-            l.len = l.pos;
-            refreshLine(&l);
-            break;
-        case LN_CTRL_A: /* Ctrl+a, go to the start of the line */
-            linenoiseEditMoveHome(&l);
-            break;
-        case LN_CTRL_E: /* ctrl+e, go to the end of the line */
-            linenoiseEditMoveEnd(&l);
-            break;
-        case LN_CTRL_L: /* ctrl+l, clear screen */
-            linenoiseClearScreen();
-            refreshLine(&l);
-            break;
-        case LN_CTRL_W: /* ctrl+w, delete previous word */
-            linenoiseEditDeletePrevWord(&l);
-            break;
-        }
-    }
-    return l.len;
-}
-
-/* This special mode is used by linenoise in order to print scan codes
- * on screen for debugging / development purposes. It is implemented
- * by the linenoise_example program using the --keycodes option. */
-void linenoisePrintKeyCodes(void) {
-    char quit[4];
-
-    printf("Linenoise key codes debugging mode.\n"
-            "Press keys to see scan codes. Type 'quit' at any time to exit.\n");
-    if (enableRawMode(STDIN_FILENO) == -1) return;
-    memset(quit,' ',4);
-    while(1) {
-        char c;
-        int nread;
-
-        nread = read(STDIN_FILENO,&c,1);
-        if (nread <= 0) continue;
-        memmove(quit,quit+1,sizeof(quit)-1); /* shift string to left. */
-        quit[sizeof(quit)-1] = c; /* Insert current char on the right. */
-        if (memcmp(quit,"quit",sizeof(quit)) == 0) break;
-
-        printf("'%c' %02x (%d) (type quit to exit)\n",
-            isprint(c) ? c : '?', (int)c, (int)c);
-        printf("\r"); /* Go left edge manually, we are in raw mode. */
-        fflush(stdout);
-    }
-    disableRawMode(STDIN_FILENO);
-}
-
-/* This function calls the line editing function linenoiseEdit() using
- * the STDIN file descriptor set in raw mode. */
-static int linenoiseRaw(char *buf, size_t buflen, const char *prompt) {
-    int count;
-
-    if (buflen == 0) {
-        errno = EINVAL;
-        return -1;
-    }
-
-    if (enableRawMode(STDIN_FILENO) == -1) return -1;
-    count = linenoiseEdit(STDIN_FILENO, STDOUT_FILENO, buf, buflen, prompt);
-    disableRawMode(STDIN_FILENO);
-    printf("\n");
-    return count;
-}
-
-/* This function is called when linenoise() is called with the standard
- * input file descriptor not attached to a TTY. So for example when the
- * program using linenoise is called in pipe or with a file redirected
- * to its standard input. In this case, we want to be able to return the
- * line regardless of its length (by default we are limited to 4k). */
-static char *linenoiseNoTTY(void) {
-    char *line = NULL;
-    size_t len = 0, maxlen = 0;
-
-    while(1) {
-        if (len == maxlen) {
-            if (maxlen == 0) maxlen = 16;
-            maxlen *= 2;
-            char *oldval = line;
-            line = realloc(line,maxlen);
-            if (line == NULL) {
-                if (oldval) free(oldval);
-                return NULL;
-            }
-        }
-        int c = fgetc(stdin);
-        if (c == EOF || c == '\n') {
-            if (c == EOF && len == 0) {
-                free(line);
-                return NULL;
-            } else {
-                line[len] = '\0';
-                return line;
-            }
-        } else {
-            line[len] = c;
-            len++;
-        }
-    }
-}
-
-/* The high level function that is the main API of the linenoise library.
- * This function checks if the terminal has basic capabilities, just checking
- * for a blacklist of stupid terminals, and later either calls the line
- * editing function or uses dummy fgets() so that you will be able to type
- * something even in the most desperate of the conditions. */
-char *linenoise(const char *prompt) {
-    char buf[LINENOISE_MAX_LINE];
-    int count;
-
-    if (!isatty(STDIN_FILENO)) {
-        /* Not a tty: read from file / pipe. In this mode we don't want any
-         * limit to the line size, so we call a function to handle that. */
-        return linenoiseNoTTY();
-    } else if (isUnsupportedTerm()) {
-        size_t len;
-
-        printf("%s",prompt);
-        fflush(stdout);
-        if (fgets(buf,LINENOISE_MAX_LINE,stdin) == NULL) return NULL;
-        len = strlen(buf);
-        while(len && (buf[len-1] == '\n' || buf[len-1] == '\r')) {
-            len--;
-            buf[len] = '\0';
-        }
-        return strdup(buf);
-    } else {
-        count = linenoiseRaw(buf,LINENOISE_MAX_LINE,prompt);
-        if (count == -1) return NULL;
-        return strdup(buf);
-    }
-}
-
-/* This is just a wrapper the user may want to call in order to make sure
- * the linenoise returned buffer is freed with the same allocator it was
- * created with. Useful when the main program is using an alternative
- * allocator. */
-void linenoiseFree(void *ptr) {
-    free(ptr);
-}
-
-/* ================================ History ================================= */
-
-/* Free the history, but does not reset it. Only used when we have to
- * exit() to avoid memory leaks are reported by valgrind & co. */
-static void freeHistory(void) {
-    if (history) {
-        int j;
-
-        for (j = 0; j < history_len; j++)
-            free(history[j]);
-        free(history);
-    }
-}
-
-/* At exit we'll try to fix the terminal to the initial conditions. */
-static void linenoiseAtExit(void) {
-    disableRawMode(STDIN_FILENO);
-    freeHistory();
-}
-
-/* This is the API call to add a new entry in the linenoise history.
- * It uses a fixed array of char pointers that are shifted (memmoved)
- * when the history max length is reached in order to remove the older
- * entry and make room for the new one, so it is not exactly suitable for huge
- * histories, but will work well for a few hundred of entries.
- *
- * Using a circular buffer is smarter, but a bit more complex to handle. */
-int linenoiseHistoryAdd(const char *line) {
-    char *linecopy;
-
-    if (history_max_len == 0) return 0;
-
-    /* Initialization on first call. */
-    if (history == NULL) {
-        history = malloc(sizeof(char*)*history_max_len);
-        if (history == NULL) return 0;
-        memset(history,0,(sizeof(char*)*history_max_len));
-    }
-
-    /* Don't add duplicated lines. */
-    if (history_len && !strcmp(history[history_len-1], line)) return 0;
-
-    /* Add an heap allocated copy of the line in the history.
-     * If we reached the max length, remove the older line. */
-    linecopy = strdup(line);
-    if (!linecopy) return 0;
-    if (history_len == history_max_len) {
-        free(history[0]);
-        memmove(history,history+1,sizeof(char*)*(history_max_len-1));
-        history_len--;
-    }
-    history[history_len] = linecopy;
-    history_len++;
-    return 1;
-}
-
-/* Set the maximum length for the history. This function can be called even
- * if there is already some history, the function will make sure to retain
- * just the latest 'len' elements if the new history length value is smaller
- * than the amount of items already inside the history. */
-int linenoiseHistorySetMaxLen(int len) {
-    char **new;
-
-    if (len < 1) return 0;
-    if (history) {
-        int tocopy = history_len;
-
-        new = malloc(sizeof(char*)*len);
-        if (new == NULL) return 0;
-
-        /* If we can't copy everything, free the elements we'll not use. */
-        if (len < tocopy) {
-            int j;
-
-            for (j = 0; j < tocopy-len; j++) free(history[j]);
-            tocopy = len;
-        }
-        memset(new,0,sizeof(char*)*len);
-        memcpy(new,history+(history_len-tocopy), sizeof(char*)*tocopy);
-        free(history);
-        history = new;
-    }
-    history_max_len = len;
-    if (history_len > history_max_len)
-        history_len = history_max_len;
-    return 1;
-}
-
-/* Save the history in the specified file. On success 0 is returned
- * otherwise -1 is returned. */
-int linenoiseHistorySave(const char *filename) {
-    mode_t old_umask = umask(S_IXUSR|S_IRWXG|S_IRWXO);
-    FILE *fp;
-    int j;
-
-    fp = fopen(filename,"w");
-    umask(old_umask);
-    if (fp == NULL) return -1;
-    chmod(filename,S_IRUSR|S_IWUSR);
-    for (j = 0; j < history_len; j++)
-        fprintf(fp,"%s\n",history[j]);
-    fclose(fp);
-    return 0;
-}
-
-/* Load the history from the specified file. If the file does not exist
- * zero is returned and no operation is performed.
- *
- * If the file exists and the operation succeeded 0 is returned, otherwise
- * on error -1 is returned. */
-int linenoiseHistoryLoad(const char *filename) {
-    FILE *fp = fopen(filename,"r");
-    char buf[LINENOISE_MAX_LINE];
-
-    if (fp == NULL) return -1;
-
-    while (fgets(buf,LINENOISE_MAX_LINE,fp) != NULL) {
-        char *p;
-
-        p = strchr(buf,'\r');
-        if (!p) p = strchr(buf,'\n');
-        if (p) *p = '\0';
-        linenoiseHistoryAdd(buf);
-    }
-    fclose(fp);
-    return 0;
-}
diff --git a/Sources/lki/main.swift b/Sources/lki/main.swift
deleted file mode 100644
index 5915f44..0000000
--- a/Sources/lki/main.swift
+++ /dev/null
@@ -1,125 +0,0 @@
-#if os(Linux)
-    import Glibc
-#else
-    import Darwin
-#endif
-import linenoise
-import LogicKit
-import LogicKitParser
-
-let bulbasaur : Term = .lit("Bulbasaur")
-let squirtle  : Term = .lit("Squirtle")
-let charmander: Term = .lit("Charmander")
-
-func makeCString(from string: String) -> UnsafeMutablePointer<Int8>? {
-    return string.withCString {
-        let len = Int(strlen($0) - 1)
-        return strcpy(UnsafeMutablePointer<Int8>.allocate(capacity: len), $0)
-    }
-}
-
-let logger = DefaultLogger()
-
-guard CommandLine.argc > 1 else {
-    logger.log(message: "error: ", terminator: "", fontAttributes: [.foreground(.red)])
-    logger.log(message: "no input file")
-    fatalError()
-}
-
-let path = CommandLine.arguments[1]
-guard let fp = fopen(path, "r") else {
-    logger.log(message: "error: ", terminator: "", fontAttributes: [.foreground(.red)])
-    logger.log(message: "could not read '\(path)'")
-    fatalError()
-}
-
-var source = ""
-var buffer = [CChar](repeating: 0, count: 1024)
-var n = 1024
-while fgets(&buffer, 1025, fp) != nil {
-    source += String(cString: buffer)
-}
-fclose(fp)
-
-let knowledgeBase: KnowledgeBase
-do {
-    knowledgeBase = KnowledgeBase(knowledge: try Grammar.knowledge.parse(source))
-} catch let e {
-    logger.log(message: "error: ", terminator: "", fontAttributes: [.foreground(.red)])
-    logger.log(message: "invalid input")
-    logger.log(message: "\(e)")
-    fatalError()
-}
-
-linenoiseHistorySetMaxLen(50)
-
-linenoiseSetCompletionCallback { buf, completions in
-    guard buf != nil else { return }
-    let input = String(cString: buf!)
-
-    for command in [".var", ".lit", ".fact", ".rule"] {
-        var i = command.index(before: command.endIndex)
-        let s = command.index(after : command.startIndex)
-
-        while i > s {
-            if input.hasSuffix(String(command[command.startIndex ..< i])) {
-                linenoiseAddCompletion(
-                    completions, input + String(command[i ..< command.endIndex]))
-                return
-            }
-            i = command.index(before: i)
-        }
-    }
-}
-
-linenoiseSetHintsCallback { (buf, color, bold) -> UnsafeMutablePointer<Int8>? in
-    guard buf != nil else { return nil }
-    let input = String(cString: buf!)
-
-    bold?.pointee  = 2
-
-    if input.hasSuffix(".var") {
-        return makeCString(from: "(<name>)")
-    } else if input.hasSuffix(".lit") {
-        return makeCString(from: "(<literal>)")
-    } else if input.hasSuffix(".fact") {
-        return makeCString(from: "(<name>, <arg0>, <arg1>, ...)")
-    } else if input.hasSuffix(".rule") {
-        return makeCString(from: "(<name>, <arg0>, <arg1>, ...) { <goal> }")
-    }
-
-    return nil
-}
-
-linenoiseSetFreeHintsCallback {
-    let cString = $0!.assumingMemoryBound(to: Int8.self)
-    cString.deallocate(capacity: strlen(cString) - 1)
-}
-
-while true {
-    guard let buf = linenoise("?- ") else { break }
-    linenoiseHistoryAdd(buf)
-    let q = String(cString: buf)
-
-    var response: RealizerAlternator? = nil
-    do {
-        let query = try Grammar.atom.parse(q)
-        response = knowledgeBase.ask(query, logger: logger)
-    } catch let e {
-        logger.log(message: "error: ", terminator: "", fontAttributes: [.foreground(.red)])
-        logger.log(message: "invalid query '\(q)'")
-        logger.log(message: "\(e)")
-    }
-
-    guard response != nil else { continue }
-    while let result = response!.next() {
-        for (variable, term) in result {
-            logger.log(message: "  \(variable) ↦ \(term)", fontAttributes: [.bold])
-        }
-        print("continue [y/n]? ", terminator: "")
-        if let command = readLine() {
-            if command == "y" { continue } else { break }
-        }
-    }
-    logger.log(message: "no result")
-}
diff --git a/Tests/LogicKitParserTests/LogicKitParserTests.swift b/Tests/LogicKitParserTests/LogicKitParserTests.swift
deleted file mode 100644
index d70dba1..0000000
--- a/Tests/LogicKitParserTests/LogicKitParserTests.swift
+++ /dev/null
@@ -1,85 +0,0 @@
-@testable import LogicKit
-@testable import LogicKitParser
-import XCTest
-
-#if swift(>=4.0)
-#else
-class LogicKitParserTests: XCTestCase {
-
-    func testParseVariable() {
-        XCTAssertEqual(try Grammar.variable.parse(".var(\"x\")")  , .var("x"))
-        XCTAssertEqual(try Grammar.variable.parse(".var( \"x\")") , .var("x"))
-        XCTAssertEqual(try Grammar.variable.parse(".var(\"x\" )") , .var("x"))
-        XCTAssertEqual(try Grammar.variable.parse(".var( \"x\" )"), .var("x"))
-    }
-
-    func testParseLiteral() {
-        XCTAssertEqual(try Grammar.literal.parse(".lit(\"a\")")   , .lit("a"))
-        XCTAssertEqual(try Grammar.literal.parse(".lit( \"a\")")  , .lit("a"))
-        XCTAssertEqual(try Grammar.literal.parse(".lit(\"a\" )")  , .lit("a"))
-        XCTAssertEqual(try Grammar.literal.parse(".lit( \"a\" )") , .lit("a"))
-
-        XCTAssertEqual(try Grammar.literal.parse(".lit(0)")       , .lit(0))
-        XCTAssertEqual(try Grammar.literal.parse(".lit(true)")    , .lit(true))
-    }
-
-    func testParseFact() {
-        XCTAssertEqual(try Grammar.fact.parse(".fact(\"a\")")     , .fact("a"))
-        XCTAssertEqual(try Grammar.fact.parse(".fact( \"a\")")    , .fact("a"))
-        XCTAssertEqual(try Grammar.fact.parse(".fact(\"a\" )")    , .fact("a"))
-        XCTAssertEqual(try Grammar.fact.parse(".fact( \"a\" )")   , .fact("a"))
-
-        XCTAssertEqual(
-            try Grammar.fact.parse(".fact(\"a\", .var(\"x\"))"),
-            .fact("a", .var("x")))
-        XCTAssertEqual(
-            try Grammar.fact.parse(".fact(\"a\" , .var(\"x\"))"),
-            .fact("a", .var("x")))
-        XCTAssertEqual(
-            try Grammar.fact.parse(".fact(\"a\", .var(\"x\"), .var(\"y\"))"),
-            .fact("a", .var("x"), .var("y")))
-        XCTAssertEqual(
-            try Grammar.fact.parse(".fact(\"a\", .fact(\"a\", .var(\"x\")))"),
-            .fact("a", .fact("a", .var("x"))))
-    }
-
-    func testParseRule() {
-        XCTAssertEqual(try Grammar.rule.parse(
-            ".rule(\"a\") { .var(\"x\") }"), .rule("a") { .var("x") })
-        XCTAssertEqual(try Grammar.rule.parse(
-            ".rule( \"a\"){ .var(\"x\") }"), .rule("a") { .var("x") })
-        XCTAssertEqual(try Grammar.rule.parse(
-            ".rule(\"a\" ) {.var(\"x\") }"), .rule("a") { .var("x") })
-        XCTAssertEqual(try Grammar.rule.parse(
-            ".rule( \"a\" ) {.var(\"x\")}"), .rule("a") { .var("x") })
-
-        let input =
-        """
-        .rule("a") {
-            .var("x")
-        }
-        """
-        XCTAssertEqual(try Grammar.rule.parse(input), .rule("a") { .var("x") })
-    }
-
-    func testParseConjunction() {
-        XCTAssertEqual(try Grammar.conjunction.parse(
-            ".var(\"x\") && .var(\"y\")"), .var("x") && .var("y"))
-        XCTAssertEqual(try Grammar.conjunction.parse(
-            ".var(\"x\") && .var(\"y\") && .var(\"z\")"), .var("x") && .var("y") && .var("z"))
-    }
-
-    func testParseDisjunction() {
-        XCTAssertEqual(try Grammar.disjunction.parse(
-            ".var(\"x\") || .var(\"y\")"), .var("x") || .var("y"))
-        XCTAssertEqual(try Grammar.disjunction.parse(
-            ".var(\"x\") || .var(\"y\") || .var(\"z\")"), .var("x") || .var("y") || .var("z"))
-    }
-
-    func testParsePrecedence() {
-        XCTAssertEqual(try Grammar.disjunction.parse(
-            ".var(\"x\") || .var(\"y\") && .var(\"z\")"), .var("x") || .var("y") && .var("z"))
-    }
-
-}
-#endif

From 328a7d6b4927bf9397e47250305be7a3a9a3810c Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 02:29:58 +0100
Subject: [PATCH 03/32] Remove dead code

---
 Sources/LogicKit/Hashing.swift | 37 ----------------------------------
 1 file changed, 37 deletions(-)
 delete mode 100644 Sources/LogicKit/Hashing.swift

diff --git a/Sources/LogicKit/Hashing.swift b/Sources/LogicKit/Hashing.swift
deleted file mode 100644
index 181eecb..0000000
--- a/Sources/LogicKit/Hashing.swift
+++ /dev/null
@@ -1,37 +0,0 @@
-#if arch(x86_64) || arch(arm64)
-    let FNV_OFFSET_BASIS = Int(bitPattern: 0xcbf29ce484222325)
-    let FNV_PRIME        = Int(bitPattern: 0x100000001b3)
-#elseif arch(i386) || arch(arm)
-    let FNV_OFFSET_BASIS = Int(bitPattern: 0x811c9dc5)
-    let FNV_PRIME        = Int(bitPattern: 0x1000193)
-#endif
-
-/// Fowler–Noll–Vo hash function implementation.
-public func fnv1(data: UnsafeRawPointer, size: Int) -> Int {
-    var h = FNV_OFFSET_BASIS
-    for i in 0 ..< size {
-        h = h &* FNV_PRIME
-        h = h ^ Int(data.load(fromByteOffset: i, as: UInt8.self))
-    }
-    return h
-}
-
-/// Fowler–Noll–Vo hash function implementation.
-public func fnv1(_ n: Int) -> Int {
-    var h = FNV_OFFSET_BASIS
-    for i in 0 ..< MemoryLayout<Int>.size {
-        h = h &* FNV_PRIME
-        h = h ^ Int(UInt8(truncatingIfNeeded: n >> (8 * i)))
-    }
-    return h
-}
-
-/// Hashes a sequence of integers.
-public func hash<S>(_ sequence: S) -> Int where S: Sequence, S.Element == Int {
-    let data = Array(sequence)
-    return data.withUnsafeBufferPointer { buffer in
-        return fnv1(
-            data: UnsafeRawPointer(buffer.baseAddress)!,
-            size: MemoryLayout<S.Element>.size * data.count)
-    }
-}

From b7cc51231c42d520fae9205f64924694d2620cc8 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 02:35:54 +0100
Subject: [PATCH 04/32] Re-indent to 2 spaces

---
 Sources/LogicKit/BindingMap.swift         |  92 ++---
 Sources/LogicKit/KnowledgeBase.swift      | 136 ++++----
 Sources/LogicKit/Logger.swift             |  90 +++--
 Sources/LogicKit/Realizer.swift           | 398 +++++++++++-----------
 Sources/LogicKit/Term.swift               | 286 ++++++++--------
 Tests/LogicKitTests/BindingMapTests.swift | 108 +++---
 Tests/LogicKitTests/LogicKitTests.swift   | 248 +++++++-------
 7 files changed, 678 insertions(+), 680 deletions(-)

diff --git a/Sources/LogicKit/BindingMap.swift b/Sources/LogicKit/BindingMap.swift
index 0619197..274a3b8 100644
--- a/Sources/LogicKit/BindingMap.swift
+++ b/Sources/LogicKit/BindingMap.swift
@@ -2,56 +2,56 @@ public typealias BindingMap = Dictionary<String, Term>
 
 extension Dictionary where Key == String, Value == Term {
 
-    func reified() -> [String: Term] {
-        var result: [String: Term] = [:]
-        for (name, term) in self {
-            result[name] = self.deepWalk(term)
-        }
-        return result
+  func reified() -> [String: Term] {
+    var result: [String: Term] = [:]
+    for (name, term) in self {
+      result[name] = self.deepWalk(term)
     }
-
-    func shallowWalk(_ term: Term) -> Term {
-        switch term {
-        case .var(let name):
-            return self[name].map({
-                self.shallowWalk($0)
-            }) ?? term
-        default:
-            return term
-        }
-    }
-
-    func deepWalk(_ term: Term) -> Term {
-        let walked = self.shallowWalk(term)
-        switch walked {
-        case ._term(name: let name, arguments: let arguments):
-            return ._term(name: name, arguments: arguments.map(self.deepWalk))
-        case .conjunction(let lhs, let rhs):
-            return .conjunction(self.deepWalk(lhs), self.deepWalk(rhs))
-        case .disjunction(let lhs, let rhs):
-            return .disjunction(self.deepWalk(lhs), self.deepWalk(rhs))
-        default:
-            return walked
-        }
+    return result
+  }
+
+  func shallowWalk(_ term: Term) -> Term {
+    switch term {
+    case .var(let name):
+      return self[name].map({
+        self.shallowWalk($0)
+      }) ?? term
+    default:
+      return term
     }
-
-    func binding(_ name: String, to term: Term) -> Dictionary {
-        var result = self
-        result[name] = term
-        return result
+  }
+
+  func deepWalk(_ term: Term) -> Term {
+    let walked = self.shallowWalk(term)
+    switch walked {
+    case ._term(name: let name, arguments: let arguments):
+      return ._term(name: name, arguments: arguments.map(self.deepWalk))
+    case .conjunction(let lhs, let rhs):
+      return .conjunction(self.deepWalk(lhs), self.deepWalk(rhs))
+    case .disjunction(let lhs, let rhs):
+      return .disjunction(self.deepWalk(lhs), self.deepWalk(rhs))
+    default:
+      return walked
     }
-
-    func merged(with other: Dictionary) -> Dictionary {
-        var result = self
-        for (name, term) in other {
-            result[name] = term
-        }
-        return result
+  }
+
+  func binding(_ name: String, to term: Term) -> Dictionary {
+    var result = self
+    result[name] = term
+    return result
+  }
+
+  func merged(with other: Dictionary) -> Dictionary {
+    var result = self
+    for (name, term) in other {
+      result[name] = term
     }
+    return result
+  }
 
-    public subscript(name: Term) -> Term? {
-        guard case let .var(val) = name else { fatalError() }
-        return self[val]
-    }
+  public subscript(name: Term) -> Term? {
+    guard case let .var(val) = name else { fatalError() }
+    return self[val]
+  }
 
 }
diff --git a/Sources/LogicKit/KnowledgeBase.swift b/Sources/LogicKit/KnowledgeBase.swift
index 7dca44f..ae472df 100644
--- a/Sources/LogicKit/KnowledgeBase.swift
+++ b/Sources/LogicKit/KnowledgeBase.swift
@@ -1,55 +1,55 @@
 public struct KnowledgeBase {
 
-    public init(knowledge: [Term]) {
-        self.knowledge = knowledge
+  public init(knowledge: [Term]) {
+    self.knowledge = knowledge
+  }
+
+  public func ask(_ query: Term, logger: Logger? = nil) -> RealizerAlternator {
+    switch query {
+    case .var(_), ._rule(_, _, _):
+      preconditionFailure("invalid query")
+    default:
+      return RealizerAlternator(realizers: query.goals.map({
+        Realizer(goals: $0, knowledge: self.refreshed, logger: logger)
+      }))
     }
-
-    public func ask(_ query: Term, logger: Logger? = nil) -> RealizerAlternator {
-        switch query {
-        case .var(_), ._rule(_, _, _):
-            preconditionFailure("invalid query")
-        default:
-            return RealizerAlternator(realizers: query.goals.map({
-                Realizer(goals: $0, knowledge: self.refreshed, logger: logger)
-            }))
-        }
+  }
+
+  public func union(with other: KnowledgeBase) -> KnowledgeBase {
+    var newClauses = self.knowledge
+    for clause in other.knowledge {
+      if !newClauses.contains(clause) {
+        newClauses.append(clause)
+      }
     }
-
-    public func union(with other: KnowledgeBase) -> KnowledgeBase {
-        var newClauses = self.knowledge
-        for clause in other.knowledge {
-            if !newClauses.contains(clause) {
-                newClauses.append(clause)
-            }
-        }
-        return KnowledgeBase(knowledge: newClauses)
+    return KnowledgeBase(knowledge: newClauses)
+  }
+
+  var refreshed: KnowledgeBase {
+    return KnowledgeBase(knowledge: self.knowledge.map(self.renameVariables))
+  }
+
+  func renameVariables(of term: Term) -> Term {
+    switch term {
+    case .var(let name):
+      return .var(name + "'")
+    case ._term(let name, let arguments):
+      return ._term(name: name, arguments: arguments.map(self.renameVariables))
+    case ._rule(let name, let arguments, let body):
+      return ._rule(
+        name     : name,
+        arguments: arguments.map(self.renameVariables),
+        body     : self.renameVariables(of: body))
+    case .conjunction(let lhs, let rhs):
+      return .conjunction(self.renameVariables(of: lhs), self.renameVariables(of: rhs))
+    case .disjunction(let lhs, let rhs):
+      return .disjunction(self.renameVariables(of: lhs), self.renameVariables(of: rhs))
+    default:
+      return term
     }
+  }
 
-    var refreshed: KnowledgeBase {
-        return KnowledgeBase(knowledge: self.knowledge.map(self.renameVariables))
-    }
-
-    func renameVariables(of term: Term) -> Term {
-        switch term {
-        case .var(let name):
-            return .var(name + "'")
-        case ._term(let name, let arguments):
-            return ._term(name: name, arguments: arguments.map(self.renameVariables))
-        case ._rule(let name, let arguments, let body):
-            return ._rule(
-                name     : name,
-                arguments: arguments.map(self.renameVariables),
-                body     : self.renameVariables(of: body))
-        case .conjunction(let lhs, let rhs):
-            return .conjunction(self.renameVariables(of: lhs), self.renameVariables(of: rhs))
-        case .disjunction(let lhs, let rhs):
-            return .disjunction(self.renameVariables(of: lhs), self.renameVariables(of: rhs))
-        default:
-            return term
-        }
-    }
-
-    public let knowledge: [Term]
+  public let knowledge: [Term]
 
 }
 
@@ -58,42 +58,42 @@ extension KnowledgeBase: Hashable {
 
 extension KnowledgeBase: Collection {
 
-    public typealias Element = Term
+  public typealias Element = Term
 
-    public var startIndex: Int {
-        return self.knowledge.startIndex
-    }
+  public var startIndex: Int {
+    return self.knowledge.startIndex
+  }
 
-    public var endIndex: Int {
-        return self.knowledge.endIndex
-    }
+  public var endIndex: Int {
+    return self.knowledge.endIndex
+  }
 
-    public func index(after i: Int) -> Int {
-        return self.knowledge.index(after: i)
-    }
+  public func index(after i: Int) -> Int {
+    return self.knowledge.index(after: i)
+  }
 
-    public func makeIterator() -> Array<Term>.Iterator {
-        return self.knowledge.makeIterator()
-    }
+  public func makeIterator() -> Array<Term>.Iterator {
+    return self.knowledge.makeIterator()
+  }
 
-    public subscript(position: Int) -> Term {
-        return self.knowledge[position]
-    }
+  public subscript(position: Int) -> Term {
+    return self.knowledge[position]
+  }
 
 }
 
 extension KnowledgeBase: ExpressibleByArrayLiteral {
 
-    public init(arrayLiteral knowledge: Term...) {
-        self.init(knowledge: knowledge)
-    }
+  public init(arrayLiteral knowledge: Term...) {
+    self.init(knowledge: knowledge)
+  }
 
 }
 
 extension KnowledgeBase: CustomStringConvertible {
 
-    public var description: String {
-        return self.knowledge.description
-    }
+  public var description: String {
+    return self.knowledge.description
+  }
 
 }
diff --git a/Sources/LogicKit/Logger.swift b/Sources/LogicKit/Logger.swift
index 11761ae..b96769b 100644
--- a/Sources/LogicKit/Logger.swift
+++ b/Sources/LogicKit/Logger.swift
@@ -1,72 +1,70 @@
 public enum FontColor {
 
-    case red, green, yellow
+  case red, green, yellow
 
 }
 
 public enum FontAttribute {
 
-    case bold
-    case dim
-    case foreground(FontColor)
-    case background(FontColor)
+  case bold
+  case dim
+  case foreground(FontColor)
+  case background(FontColor)
 
 }
 
 public protocol Logger {
 
-    func log(message: String, terminator: String, fontAttributes: [FontAttribute])
+  func log(message: String, terminator: String, fontAttributes: [FontAttribute])
 
 }
 
 extension Logger {
 
-    public func log(message: String) {
-        self.log(message: message, terminator: "\n", fontAttributes: [])
-    }
+  public func log(message: String) {
+    self.log(message: message, terminator: "\n", fontAttributes: [])
+  }
 
-    public func log(message: String, fontAttributes: [FontAttribute]) {
-        self.log(message: message, terminator: "\n", fontAttributes: fontAttributes)
-    }
+  public func log(message: String, fontAttributes: [FontAttribute]) {
+    self.log(message: message, terminator: "\n", fontAttributes: fontAttributes)
+  }
 
-    public func log(message: String, terminator: String) {
-        self.log(message: message, terminator: terminator, fontAttributes: [])
-    }
+  public func log(message: String, terminator: String) {
+    self.log(message: message, terminator: terminator, fontAttributes: [])
+  }
 
 }
 
 public struct DefaultLogger: Logger {
 
-    public init() {}
-
-    public func log(message: String, terminator: String, fontAttributes: [FontAttribute]) {
-        let attributes = fontAttributes.compactMap({
-            switch $0 {
-            case .bold:
-                return "\u{001B}[1m"
-            case .dim:
-                return "\u{001B}[2m"
-            case .foreground(let color):
-                return "\u{001B}[\(DefaultLogger.foreground[color] ?? "39m")"
-            case .background(let color):
-                return "\u{001B}[\(DefaultLogger.background[color] ?? "40m")"
-            }
-
-        }).joined(separator: "")
-
-        print("\(attributes)\(message)\u{001B}[0m", terminator: terminator)
-    }
-
-    static let foreground: [FontColor: String] = [
-        .red   : "31m",
-        .green : "32m",
-        .yellow: "33m",
-    ]
-
-    static let background: [FontColor: String] = [
-        .red   : "41m",
-        .green : "42m",
-        .yellow: "43m",
-    ]
+  public init() {}
+
+  public func log(message: String, terminator: String, fontAttributes: [FontAttribute]) {
+    let attributes = fontAttributes.compactMap({
+      switch $0 {
+      case .bold:
+        return "\u{001B}[1m"
+      case .dim:
+        return "\u{001B}[2m"
+      case .foreground(let color):
+        return "\u{001B}[\(DefaultLogger.foreground[color] ?? "39m")"
+      case .background(let color):
+        return "\u{001B}[\(DefaultLogger.background[color] ?? "40m")"
+      }
+    }).joined(separator: "")
+    print("\(attributes)\(message)\u{001B}[0m", terminator: terminator)
+  }
+
+  static let foreground: [FontColor: String] = [
+    .red   : "31m",
+    .green : "32m",
+    .yellow: "33m",
+  ]
+
+  static let background: [FontColor: String] = [
+    .red   : "41m",
+    .green : "42m",
+    .yellow: "43m",
+  ]
 
 }
diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index 3d0df7a..c93129f 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -1,232 +1,232 @@
 public struct RealizerAlternator: IteratorProtocol, Sequence {
 
-    init<S>(realizers: S) where S: Sequence, S.Element == Realizer {
-        self.realizers = Array(realizers)
-    }
-
-    public mutating func next() -> [String: Term]? {
-        while !self.realizers.isEmpty {
-            guard let result = self.realizers[self.index].next() else {
-                self.realizers.remove(at: index)
-                if !self.realizers.isEmpty {
-                    self.index = self.index % self.realizers.count
-                }
-                continue
-            }
-            self.index = (self.index + 1) % self.realizers.count
-            return result
+  init<S>(realizers: S) where S: Sequence, S.Element == Realizer {
+    self.realizers = Array(realizers)
+  }
+
+  public mutating func next() -> [String: Term]? {
+    while !self.realizers.isEmpty {
+      guard let result = self.realizers[self.index].next() else {
+        self.realizers.remove(at: index)
+        if !self.realizers.isEmpty {
+          self.index = self.index % self.realizers.count
         }
-        return nil
+        continue
+      }
+      self.index = (self.index + 1) % self.realizers.count
+      return result
     }
+    return nil
+  }
 
-    public func makeIterator() -> RealizerAlternator {
-        return self
-    }
+  public func makeIterator() -> RealizerAlternator {
+    return self
+  }
 
-    var index    : Int = 0
-    var realizers: [Realizer]
+  var index    : Int = 0
+  var realizers: [Realizer]
 
 }
 
 struct Realizer: IteratorProtocol {
 
-    init(
-        goals         : [Term],
-        knowledge     : KnowledgeBase,
-        parentBindings: BindingMap = [:],
-        logger        : Logger? = nil)
-    {
-        self.goals          = goals
-        self.knowledge      = knowledge
-        self.parentBindings = parentBindings
-        self.logger         = logger
+  init(
+    goals         : [Term],
+    knowledge     : KnowledgeBase,
+    parentBindings: BindingMap = [:],
+    logger        : Logger? = nil)
+  {
+    self.goals          = goals
+    self.knowledge      = knowledge
+    self.parentBindings = parentBindings
+    self.logger         = logger
+  }
+
+  mutating func next() -> [String: Term]? {
+    // If we have a subrealizer running, pull its results first.
+    if let result = self.subRealizer?.next() {
+      return result
+    } else {
+      if self.subRealizer != nil {
+        self.logger?.log(message: "backtacking", fontAttributes: [.dim])
+        self.subRealizer = nil
+      }
     }
 
-    mutating func next() -> [String: Term]? {
-        // If we have a subrealizer running, pull its results first.
-        if let result = self.subRealizer?.next() {
-            return result
+    let goal = self.goals.first!
+    self.logger?.log(message: "Attempting to realize ", terminator: "")
+    self.logger?.log(message: goal.description, fontAttributes: [.bold])
+
+    // Check for the built-in `~=~/2` predicate.
+    if case ._term("lk.~=~", let args) = goal {
+      assert(args.count == 2)
+      if let nodeResult = self.unify(goal: args[0], fact: args[1]) {
+        if self.goals.count > 1 {
+          let subGoals     = self.goals.dropFirst().map(nodeResult.deepWalk)
+          self.subRealizer = RealizerAlternator(realizers: [
+            Realizer(
+              goals         : subGoals,
+              knowledge     : self.knowledge,
+              parentBindings: nodeResult,
+              logger        : self.logger)
+            ])
+          if let branchResult = self.subRealizer!.next() {
+            return branchResult
+              .merged(with: parentBindings)
+              .reified()
+          }
         } else {
-            if self.subRealizer != nil {
-                self.logger?.log(message: "backtacking", fontAttributes: [.dim])
-                self.subRealizer = nil
-            }
+          return nodeResult
+            .merged(with: parentBindings)
+            .reified()
         }
+      }
+    }
 
-        let goal = self.goals.first!
-        self.logger?.log(message: "Attempting to realize ", terminator: "")
-        self.logger?.log(message: goal.description, fontAttributes: [.bold])
-
-        // Check for the built-in `~=~/2` predicate.
-        if case ._term("lk.~=~", let args) = goal {
-            assert(args.count == 2)
-            if let nodeResult = self.unify(goal: args[0], fact: args[1]) {
-                if self.goals.count > 1 {
-                    let subGoals     = self.goals.dropFirst().map(nodeResult.deepWalk)
-                    self.subRealizer = RealizerAlternator(realizers: [
-                        Realizer(
-                            goals         : subGoals,
-                            knowledge     : self.knowledge,
-                            parentBindings: nodeResult,
-                            logger        : self.logger)
-                    ])
-                    if let branchResult = self.subRealizer!.next() {
-                        return branchResult
-                            .merged(with: parentBindings)
-                            .reified()
-                    }
-                } else {
-                    return nodeResult
-                        .merged(with: parentBindings)
-                        .reified()
-                }
-            }
+    // Look for the next root clause.
+    while self.clauseIndex != self.knowledge.endIndex {
+      let clause = self.knowledge[self.clauseIndex]
+      self.clauseIndex += 1
+
+      self.logger?.log(message: "using "    , terminator: "", fontAttributes: [.dim])
+      self.logger?.log(message: "\(clause) ")
+
+      switch (goal, clause) {
+      case (.val(let lvalue), .val(let rvalue)) where lvalue == rvalue:
+        if self.goals.count > 1 {
+          let subGoals     = Array(self.goals.dropFirst())
+          self.subRealizer = RealizerAlternator(realizers: [
+            Realizer(goals: subGoals, knowledge: self.knowledge, logger: self.logger)
+          ])
+          if let branchResult = self.subRealizer!.next() {
+            return branchResult
+              .merged(with: parentBindings)
+              .reified()
+          }
         }
 
-        // Look for the next root clause.
-        while self.clauseIndex != self.knowledge.endIndex {
-            let clause = self.knowledge[self.clauseIndex]
-            self.clauseIndex += 1
-
-            self.logger?.log(message: "using "    , terminator: "", fontAttributes: [.dim])
-            self.logger?.log(message: "\(clause) ")
-
-            switch (goal, clause) {
-            case (.val(let lvalue), .val(let rvalue)) where lvalue == rvalue:
-                if self.goals.count > 1 {
-                    let subGoals     = Array(self.goals.dropFirst())
-                    self.subRealizer = RealizerAlternator(realizers: [
-                        Realizer(goals: subGoals, knowledge: self.knowledge, logger: self.logger)
-                    ])
-                    if let branchResult = self.subRealizer!.next() {
-                        return branchResult
-                            .merged(with: parentBindings)
-                            .reified()
-                    }
-                }
-
-            case (._term(_, _), ._term(_, _)):
-                if let nodeResult = self.unify(goal: goal, fact: clause) {
-                    if self.goals.count > 1 {
-                        let subGoals     = self.goals.dropFirst().map(nodeResult.deepWalk)
-                        self.subRealizer = RealizerAlternator(realizers: [
-                            Realizer(
-                                goals         : subGoals,
-                                knowledge     : self.knowledge,
-                                parentBindings: nodeResult,
-                                logger        : self.logger)
-                        ])
-                        if let branchResult = self.subRealizer!.next() {
-                            return branchResult
-                                .merged(with: parentBindings)
-                                .reified()
-                        }
-                    } else {
-                        return nodeResult
-                            .merged(with: parentBindings)
-                            .reified()
-                    }
-                }
-
-            case let (._term(goalName, _), ._rule(ruleName, ruleArguments, ruleBody))
-                where goalName == ruleName:
-
-                // First we try to unify the rule head with the goal.
-                let head: Term = ._term(name: goalName, arguments: ruleArguments)
-                if let nodeResult = self.unify(goal: goal, fact: head) {
-                    let subGoals  = self.goals.dropFirst()
-                        .map(nodeResult.deepWalk)
-                    let ruleGoals = ruleBody.goals
-                        .map({ $0.map(nodeResult.deepWalk) + subGoals })
-
-                    // Note that we have to make sure all variables of the sub-realizer's knowldge
-                    // are fresh, otherwise they may collide with the ones we already bound. For
-                    // instance, consider a recursive rule `p(q($x), $y) ⊢ p($x, q($y))` and a
-                    // goal `p($z, 0)`. In this example, `$z` would get bound to `q($x)` and `$y`
-                    // to `0` before we try satisfy `p($x, q(0))`. But if `$x` wasn't renamed,
-                    // we'd be trying to unify `$x` with `q($x)` while recursing.
-
-                    self.subRealizer = RealizerAlternator(realizers: ruleGoals.map({
-                        Realizer(
-                            goals         : $0,
-                            knowledge     : self.knowledge.refreshed,
-                            parentBindings: nodeResult,
-                            logger        : self.logger)
-                    }))
-                    if let branchResult = self.subRealizer!.next() {
-                        return nodeResult
-                            .merged(with: branchResult)
-                            .merged(with: parentBindings)
-                            .reified()
-                    }
-                }
-
-            default:
-                break
+      case (._term(_, _), ._term(_, _)):
+        if let nodeResult = self.unify(goal: goal, fact: clause) {
+          if self.goals.count > 1 {
+            let subGoals     = self.goals.dropFirst().map(nodeResult.deepWalk)
+            self.subRealizer = RealizerAlternator(realizers: [
+              Realizer(
+                goals         : subGoals,
+                knowledge     : self.knowledge,
+                parentBindings: nodeResult,
+                logger        : self.logger)
+            ])
+            if let branchResult = self.subRealizer!.next() {
+              return branchResult
+                .merged(with: parentBindings)
+                .reified()
             }
+          } else {
+            return nodeResult
+              .merged(with: parentBindings)
+              .reified()
+          }
         }
 
-        return nil
-    }
-
-    func unify(goal: Term, fact: Term, knowing bindings: BindingMap = [:]) -> BindingMap? {
-        // Shallow-walk the terms to unify.
-        let lhs = bindings.shallowWalk(goal)
-        let rhs = bindings.shallowWalk(fact)
-
-        // Equal terms always unify.
-        if lhs == rhs {
-            return bindings
+      case let (._term(goalName, _), ._rule(ruleName, ruleArguments, ruleBody))
+        where goalName == ruleName:
+
+        // First we try to unify the rule head with the goal.
+        let head: Term = ._term(name: goalName, arguments: ruleArguments)
+        if let nodeResult = self.unify(goal: goal, fact: head) {
+          let subGoals  = self.goals.dropFirst()
+            .map(nodeResult.deepWalk)
+          let ruleGoals = ruleBody.goals
+            .map({ $0.map(nodeResult.deepWalk) + subGoals })
+
+          // Note that we have to make sure all variables of the sub-realizer's knowldge
+          // are fresh, otherwise they may collide with the ones we already bound. For
+          // instance, consider a recursive rule `p(q($x), $y) ⊢ p($x, q($y))` and a
+          // goal `p($z, 0)`. In this example, `$z` would get bound to `q($x)` and `$y`
+          // to `0` before we try satisfy `p($x, q(0))`. But if `$x` wasn't renamed,
+          // we'd be trying to unify `$x` with `q($x)` while recursing.
+
+          self.subRealizer = RealizerAlternator(realizers: ruleGoals.map({
+            Realizer(
+              goals         : $0,
+              knowledge     : self.knowledge.refreshed,
+              parentBindings: nodeResult,
+              logger        : self.logger)
+          }))
+          if let branchResult = self.subRealizer!.next() {
+            return nodeResult
+              .merged(with: branchResult)
+              .merged(with: parentBindings)
+              .reified()
+          }
         }
 
-        switch (lhs, rhs) {
-        case let (.var(name), _):
-            switch bindings[name] {
-            case .none: return bindings.binding(name, to: rhs)
-            case rhs? : return bindings
-            default   : return nil
-            }
+      default:
+        break
+      }
+    }
 
-        case let (_, .var(name)):
-            switch bindings[name] {
-            case .none: return bindings.binding(name, to: lhs)
-            case lhs? : return bindings
-            default   : return nil
-            }
+    return nil
+  }
 
-        case let (.val(lvalue), .val(rvalue)):
-            return lvalue == rvalue
-                ? bindings
-                : nil
-
-        case let (._term(lname, largs), ._term(rname, rargs)) where lname == rname:
-            // Make sure both terms are of same arity.
-            guard largs.count == rargs.count else { return nil }
-
-            // Try unify subterms (i.e. arguments).
-            var intermediateResult = bindings
-            for (larg, rarg) in zip(largs, rargs) {
-                if let b = self.unify(goal: larg, fact: rarg, knowing: intermediateResult) {
-                    intermediateResult = b
-                } else {
-                    return nil
-                }
-            }
+  func unify(goal: Term, fact: Term, knowing bindings: BindingMap = [:]) -> BindingMap? {
+    // Shallow-walk the terms to unify.
+    let lhs = bindings.shallowWalk(goal)
+    let rhs = bindings.shallowWalk(fact)
 
-            // Unification succeeded.
-            return intermediateResult
+    // Equal terms always unify.
+    if lhs == rhs {
+      return bindings
+    }
 
-        default:
-            return nil
+    switch (lhs, rhs) {
+    case let (.var(name), _):
+      switch bindings[name] {
+      case .none: return bindings.binding(name, to: rhs)
+      case rhs? : return bindings
+      default   : return nil
+      }
+
+    case let (_, .var(name)):
+      switch bindings[name] {
+      case .none: return bindings.binding(name, to: lhs)
+      case lhs? : return bindings
+      default   : return nil
+      }
+
+    case let (.val(lvalue), .val(rvalue)):
+      return lvalue == rvalue
+        ? bindings
+        : nil
+
+    case let (._term(lname, largs), ._term(rname, rargs)) where lname == rname:
+      // Make sure both terms are of same arity.
+      guard largs.count == rargs.count else { return nil }
+
+      // Try unify subterms (i.e. arguments).
+      var intermediateResult = bindings
+      for (larg, rarg) in zip(largs, rargs) {
+        if let b = self.unify(goal: larg, fact: rarg, knowing: intermediateResult) {
+          intermediateResult = b
+        } else {
+          return nil
         }
+      }
+
+      // Unification succeeded.
+      return intermediateResult
+
+    default:
+      return nil
     }
+  }
 
-    let goals         : [Term]
-    let knowledge     : KnowledgeBase
-    let parentBindings: BindingMap
-    var logger        : Logger?
+  let goals         : [Term]
+  let knowledge     : KnowledgeBase
+  let parentBindings: BindingMap
+  var logger        : Logger?
 
-    var clauseIndex   : Int = 0
-    var subRealizer   : RealizerAlternator? = nil
+  var clauseIndex   : Int = 0
+  var subRealizer   : RealizerAlternator? = nil
 
 }
diff --git a/Sources/LogicKit/Term.swift b/Sources/LogicKit/Term.swift
index b7f35c0..17fb182 100644
--- a/Sources/LogicKit/Term.swift
+++ b/Sources/LogicKit/Term.swift
@@ -7,128 +7,128 @@ infix operator ∨
 
 public enum Term {
 
-    case `var`(String)
-    case val(AnyHashable)
-    indirect case _term(name: String, arguments: [Term])
-    indirect case _rule(name: String, arguments: [Term], body: Term)
-
-    indirect case conjunction(Term, Term)
-    indirect case disjunction(Term, Term)
-
-    var dnf: Term {
-        switch self {
-        case .conjunction(let a, .disjunction(let b, let c)):
-            return (a && b) || (a && c)
-        case .conjunction(.disjunction(let a, let b), let c):
-            return (a && c) || (b && c)
-        default:
-            return self
-        }
-    }
-
-    var goals: [[Term]] {
-        switch self.dnf {
-        case .conjunction(let lhs, let rhs):
-            assert((lhs.goals.count == 1) && (rhs.goals.count == 1))
-            return [lhs.goals[0] + rhs.goals[0]]
-        case .disjunction(let lhs, let rhs):
-            return lhs.goals + rhs.goals
-        default:
-            return [[self]]
-        }
-    }
-
-    // MARK: EDSL
-
-    public static func lit<T>(_ value: T) -> Term where T: Hashable {
-        return .val(AnyHashable(value))
-    }
-
-    /////
-
-    public static func fact(_ name: Term, _ arguments: Term...) -> Term {
-        guard case let .val(val) = name else { fatalError() }
-        guard let name = val as? String else { fatalError() }
-        return ._term(name: name, arguments: arguments)
-    }
-
-    public static func fact(_ name: String, _ arguments: Term...) -> Term {
-        return ._term(name: name, arguments: arguments)
-    }
-
-    public subscript(terms: Term...) -> Term {
-        guard case let .val(val) = self else { fatalError() }
-        guard let name = val as? String else { fatalError() }
-        return ._term(name: name, arguments: terms)
-    }
-
-    /////
-
-    public static func rule(_ name: Term, _ arguments: Term..., body: () -> Term) -> Term {
-        guard case let .val(val) = name else { fatalError() }
-        guard let name = val as? String else { fatalError() }
-        return ._rule(name: name, arguments: arguments, body: body())
-    }
-
-    public static func rule(_ name: String, _ arguments: Term..., body: () -> Term) -> Term {
-        return ._rule(name: name, arguments: arguments, body: body())
-    }
-
-    public static func =>(lhs: Term, rhs: Term) -> Term {
-      guard case let ._term(name: name, arguments: arguments) = rhs else { fatalError() }
-      return ._rule(name: name, arguments: arguments, body: lhs)
-    }
-
-    public static func =>(lhs: () -> Term, rhs: Term) -> Term {
-      guard case let ._term(name: name, arguments: arguments) = rhs else { fatalError() }
-      return ._rule(name: name, arguments: arguments, body: lhs())
-    }
-
-    public static func |-(lhs: Term, rhs: Term) -> Term {
-      guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
-      return ._rule(name: name, arguments: arguments, body: rhs)
-    }
+  case `var`(String)
+  case val(AnyHashable)
+  indirect case _term(name: String, arguments: [Term])
+  indirect case _rule(name: String, arguments: [Term], body: Term)
+
+  indirect case conjunction(Term, Term)
+  indirect case disjunction(Term, Term)
+
+  var dnf: Term {
+    switch self {
+    case .conjunction(let a, .disjunction(let b, let c)):
+      return (a && b) || (a && c)
+    case .conjunction(.disjunction(let a, let b), let c):
+      return (a && c) || (b && c)
+    default:
+      return self
+    }
+  }
+
+  var goals: [[Term]] {
+    switch self.dnf {
+    case .conjunction(let lhs, let rhs):
+      assert((lhs.goals.count == 1) && (rhs.goals.count == 1))
+      return [lhs.goals[0] + rhs.goals[0]]
+    case .disjunction(let lhs, let rhs):
+      return lhs.goals + rhs.goals
+    default:
+      return [[self]]
+    }
+  }
+
+  // MARK: EDSL
+
+  public static func lit<T>(_ value: T) -> Term where T: Hashable {
+    return .val(AnyHashable(value))
+  }
+
+  /////
+
+  public static func fact(_ name: Term, _ arguments: Term...) -> Term {
+    guard case let .val(val) = name else { fatalError() }
+    guard let name = val as? String else { fatalError() }
+    return ._term(name: name, arguments: arguments)
+  }
+
+  public static func fact(_ name: String, _ arguments: Term...) -> Term {
+    return ._term(name: name, arguments: arguments)
+  }
+
+  public subscript(terms: Term...) -> Term {
+    guard case let .val(val) = self else { fatalError() }
+    guard let name = val as? String else { fatalError() }
+    return ._term(name: name, arguments: terms)
+  }
+
+  /////
+
+  public static func rule(_ name: Term, _ arguments: Term..., body: () -> Term) -> Term {
+    guard case let .val(val) = name else { fatalError() }
+    guard let name = val as? String else { fatalError() }
+    return ._rule(name: name, arguments: arguments, body: body())
+  }
+
+  public static func rule(_ name: String, _ arguments: Term..., body: () -> Term) -> Term {
+    return ._rule(name: name, arguments: arguments, body: body())
+  }
+
+  public static func =>(lhs: Term, rhs: Term) -> Term {
+    guard case let ._term(name: name, arguments: arguments) = rhs else { fatalError() }
+    return ._rule(name: name, arguments: arguments, body: lhs)
+  }
+
+  public static func =>(lhs: () -> Term, rhs: Term) -> Term {
+    guard case let ._term(name: name, arguments: arguments) = rhs else { fatalError() }
+    return ._rule(name: name, arguments: arguments, body: lhs())
+  }
+
+  public static func |-(lhs: Term, rhs: Term) -> Term {
+    guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
+    return ._rule(name: name, arguments: arguments, body: rhs)
+  }
+
+  public static func |-(lhs: Term, rhs: () -> Term) -> Term {
+    guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
+    return ._rule(name: name, arguments: arguments, body: rhs())
+  }
+
+  public static func ⊢(lhs: Term, rhs: Term) -> Term {
+    guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
+    return ._rule(name: name, arguments: arguments, body: rhs)
+  }
+
+  public static func ⊢(lhs: Term, rhs: () -> Term) -> Term {
+    guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
+    return ._rule(name: name, arguments: arguments, body: rhs())
+  }
+
+  /////
+
+  public static func &&(lhs: Term, rhs: Term) -> Term {
+    return .conjunction(lhs, rhs)
+  }
+
+  public static func ∧(lhs: Term, rhs: Term) -> Term {
+    return .conjunction(lhs, rhs)
+  }
+
+  /////
+
+  public static func ||(lhs: Term, rhs: Term) -> Term {
+    return .disjunction(lhs, rhs)
+  }
 
-    public static func |-(lhs: Term, rhs: () -> Term) -> Term {
-      guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
-      return ._rule(name: name, arguments: arguments, body: rhs())
-    }
+  public static func ∨(lhs: Term, rhs: Term) -> Term {
+    return .disjunction(lhs, rhs)
+  }
 
-    public static func ⊢(lhs: Term, rhs: Term) -> Term {
-      guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
-      return ._rule(name: name, arguments: arguments, body: rhs)
-    }
+  /////
 
-    public static func ⊢(lhs: Term, rhs: () -> Term) -> Term {
-      guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
-      return ._rule(name: name, arguments: arguments, body: rhs())
-    }
-
-    /////
-
-    public static func &&(lhs: Term, rhs: Term) -> Term {
-        return .conjunction(lhs, rhs)
-    }
-
-    public static func ∧(lhs: Term, rhs: Term) -> Term {
-        return .conjunction(lhs, rhs)
-    }
-
-    /////
-
-    public static func ||(lhs: Term, rhs: Term) -> Term {
-        return .disjunction(lhs, rhs)
-    }
-
-    public static func ∨(lhs: Term, rhs: Term) -> Term {
-        return .disjunction(lhs, rhs)
-    }
-
-    /////
-
-    public static func ~=~(lhs: Term, rhs: Term) -> Term {
-        return ._term(name: "lk.~=~", arguments: [lhs, rhs])
-    }
+  public static func ~=~(lhs: Term, rhs: Term) -> Term {
+    return ._term(name: "lk.~=~", arguments: [lhs, rhs])
+  }
 
 }
 
@@ -138,32 +138,32 @@ extension Term: Hashable {
 
 extension Term: CustomStringConvertible {
 
-    public var description: String {
-        switch self {
-        case let .var(name):
-            return "$\(name)"
-        case let .val(value):
-            return "\(value)"
-        case let ._term(name, arguments):
-            return arguments.isEmpty
-                ? name.description
-                : "\(name)[\(arguments.map({ $0.description }).joined(separator: ", "))]"
-        case let ._rule(name, arguments, body):
-            let head = arguments.isEmpty
-                ? name.description
-                : "\(name)[\(arguments.map({ $0.description }).joined(separator: ", "))]"
-            return "(\(head) ⊢ \(body))"
-        case let .conjunction(lhs, rhs):
-            return "(\(lhs) ∧ \(rhs))"
-        case let .disjunction(lhs, rhs):
-            return "(\(lhs) ∨ \(rhs))"
-        }
-    }
+  public var description: String {
+    switch self {
+    case let .var(name):
+      return "$\(name)"
+    case let .val(value):
+      return "\(value)"
+    case let ._term(name, arguments):
+      return arguments.isEmpty
+        ? name.description
+        : "\(name)[\(arguments.map({ $0.description }).joined(separator: ", "))]"
+    case let ._rule(name, arguments, body):
+      let head = arguments.isEmpty
+        ? name.description
+        : "\(name)[\(arguments.map({ $0.description }).joined(separator: ", "))]"
+      return "(\(head) ⊢ \(body))"
+    case let .conjunction(lhs, rhs):
+      return "(\(lhs) ∧ \(rhs))"
+    case let .disjunction(lhs, rhs):
+      return "(\(lhs) ∨ \(rhs))"
+    }
+  }
 
 }
 
 extension Term : ExpressibleByStringLiteral {
-    public init(stringLiteral : String) {
-        self = .lit(stringLiteral)
-    }
+  public init(stringLiteral : String) {
+    self = .lit(stringLiteral)
+  }
 }
diff --git a/Tests/LogicKitTests/BindingMapTests.swift b/Tests/LogicKitTests/BindingMapTests.swift
index aab5ea8..f7ee649 100644
--- a/Tests/LogicKitTests/BindingMapTests.swift
+++ b/Tests/LogicKitTests/BindingMapTests.swift
@@ -3,59 +3,59 @@ import XCTest
 
 class BindingMapTests: XCTestCase {
 
-    func testShallowWalk() {
-        let bindingMap: BindingMap = [
-            "w": .fact("a"),
-            "x": .var("y"),
-            "y": .var("z"),
-            "z": .fact("t", .var("w"))
-        ]
-
-        XCTAssertEqual(bindingMap.shallowWalk(.fact("u")), .fact("u"))
-        XCTAssertEqual(bindingMap.shallowWalk(.var("z")) , .fact("t", .var("w")))
-        XCTAssertEqual(bindingMap.shallowWalk(.var("y")) , .fact("t", .var("w")))
-        XCTAssertEqual(bindingMap.shallowWalk(.var("x")) , .fact("t", .var("w")))
-    }
-
-    func testDeepWalk() {
-        let bindingMap: BindingMap = [
-            "w": .fact("a"),
-            "x": .var("y"),
-            "y": .var("z"),
-            "z": .fact("t", .var("w"))
-        ]
-
-        XCTAssertEqual(bindingMap.deepWalk(.fact("u")), .fact("u"))
-        XCTAssertEqual(bindingMap.deepWalk(.var("z")) , .fact("t", .fact("a")))
-        XCTAssertEqual(bindingMap.deepWalk(.var("y")) , .fact("t", .fact("a")))
-        XCTAssertEqual(bindingMap.deepWalk(.var("x")) , .fact("t", .fact("a")))
-    }
-
-    func testReified() {
-        let bindingMap: BindingMap = [
-            "w": .fact("a"),
-            "x": .var("y"),
-            "y": .var("z"),
-            "z": .fact("t", .var("w"))
-        ]
-        let reifiedMap = bindingMap.reified()
-
-        XCTAssertEqual(reifiedMap["w"], .fact("a"))
-        XCTAssertEqual(reifiedMap["x"], .fact("t", .fact("a")))
-        XCTAssertEqual(reifiedMap["y"], .fact("t", .fact("a")))
-        XCTAssertEqual(reifiedMap["z"], .fact("t", .fact("a")))
-    }
-
-    func testBinding() {
-        let bindingMap: BindingMap = ["x": .var("y")]
-        XCTAssertEqual(bindingMap.binding("v", to: .fact("b"))["v"], .fact("b"))
-        XCTAssertEqual(bindingMap.binding("x", to: .fact("b"))["x"], .fact("b"))
-    }
-
-    func testMerged() {
-        let bindingMap: BindingMap = ["x": .var("y")]
-        XCTAssertEqual(bindingMap.merged(with: ["y": .var("z")])["y"], .var("z"))
-        XCTAssertEqual(bindingMap.merged(with: ["x": .var("z")])["x"], .var("z"))
-    }
+  func testShallowWalk() {
+    let bindingMap: BindingMap = [
+      "w": .fact("a"),
+      "x": .var("y"),
+      "y": .var("z"),
+      "z": .fact("t", .var("w"))
+    ]
+
+    XCTAssertEqual(bindingMap.shallowWalk(.fact("u")), .fact("u"))
+    XCTAssertEqual(bindingMap.shallowWalk(.var("z")) , .fact("t", .var("w")))
+    XCTAssertEqual(bindingMap.shallowWalk(.var("y")) , .fact("t", .var("w")))
+    XCTAssertEqual(bindingMap.shallowWalk(.var("x")) , .fact("t", .var("w")))
+  }
+
+  func testDeepWalk() {
+    let bindingMap: BindingMap = [
+      "w": .fact("a"),
+      "x": .var("y"),
+      "y": .var("z"),
+      "z": .fact("t", .var("w"))
+    ]
+
+    XCTAssertEqual(bindingMap.deepWalk(.fact("u")), .fact("u"))
+    XCTAssertEqual(bindingMap.deepWalk(.var("z")) , .fact("t", .fact("a")))
+    XCTAssertEqual(bindingMap.deepWalk(.var("y")) , .fact("t", .fact("a")))
+    XCTAssertEqual(bindingMap.deepWalk(.var("x")) , .fact("t", .fact("a")))
+  }
+
+  func testReified() {
+    let bindingMap: BindingMap = [
+      "w": .fact("a"),
+      "x": .var("y"),
+      "y": .var("z"),
+      "z": .fact("t", .var("w"))
+    ]
+    let reifiedMap = bindingMap.reified()
+
+    XCTAssertEqual(reifiedMap["w"], .fact("a"))
+    XCTAssertEqual(reifiedMap["x"], .fact("t", .fact("a")))
+    XCTAssertEqual(reifiedMap["y"], .fact("t", .fact("a")))
+    XCTAssertEqual(reifiedMap["z"], .fact("t", .fact("a")))
+  }
+
+  func testBinding() {
+    let bindingMap: BindingMap = ["x": .var("y")]
+    XCTAssertEqual(bindingMap.binding("v", to: .fact("b"))["v"], .fact("b"))
+    XCTAssertEqual(bindingMap.binding("x", to: .fact("b"))["x"], .fact("b"))
+  }
+
+  func testMerged() {
+    let bindingMap: BindingMap = ["x": .var("y")]
+    XCTAssertEqual(bindingMap.merged(with: ["y": .var("z")])["y"], .var("z"))
+    XCTAssertEqual(bindingMap.merged(with: ["x": .var("z")])["x"], .var("z"))
+  }
 
 }
diff --git a/Tests/LogicKitTests/LogicKitTests.swift b/Tests/LogicKitTests/LogicKitTests.swift
index e20e578..e2d121f 100644
--- a/Tests/LogicKitTests/LogicKitTests.swift
+++ b/Tests/LogicKitTests/LogicKitTests.swift
@@ -3,133 +3,133 @@ import XCTest
 
 class LogicKitTests: XCTestCase {
 
-    func testConstantFacts() {
-        let kb: KnowledgeBase = [
-            .fact("<", .lit(0), .lit(1)),
-            .fact("<", .lit(1), .lit(2)),
-            .fact("<", .lit(2), .lit(3)),
-        ]
-
-        let answers0 = Array(kb.ask(.fact("<", .lit(0), .lit(1))))
-        XCTAssertEqual(answers0.count, 1)
-        XCTAssertEqual(answers0[0]   , [:])
-
-        let answers1 = Array(kb.ask(.fact("<", .lit(2), .lit(3))))
-        XCTAssertEqual(answers1.count, 1)
-        XCTAssertEqual(answers1[0]   , [:])
-
-        let answers2 = Array(kb.ask(.fact("<", .lit(0), .lit(3))))
-        XCTAssertEqual(answers2.count, 0)
+  func testConstantFacts() {
+    let kb: KnowledgeBase = [
+      .fact("<", .lit(0), .lit(1)),
+      .fact("<", .lit(1), .lit(2)),
+      .fact("<", .lit(2), .lit(3)),
+    ]
+
+    let answers0 = Array(kb.ask(.fact("<", .lit(0), .lit(1))))
+    XCTAssertEqual(answers0.count, 1)
+    XCTAssertEqual(answers0[0]   , [:])
+
+    let answers1 = Array(kb.ask(.fact("<", .lit(2), .lit(3))))
+    XCTAssertEqual(answers1.count, 1)
+    XCTAssertEqual(answers1[0]   , [:])
+
+    let answers2 = Array(kb.ask(.fact("<", .lit(0), .lit(3))))
+    XCTAssertEqual(answers2.count, 0)
+  }
+
+  func testFactsWithVariables() {
+    let kb: KnowledgeBase = [
+      .fact("<", .lit(0), .lit(1)),
+      .fact("<", .lit(1), .lit(2)),
+      .fact("<", .lit(2), .lit(3)),
+    ]
+
+    let answers0 = Array(kb.ask(.fact("<", .lit(0), .var("x"))))
+    XCTAssertEqual(answers0.count, 1)
+    XCTAssertEqual(answers0[0]   , ["x": .lit(1)])
+
+    let answers1 = Array(kb.ask(.fact("<", .var("x"), .var("y"))))
+    XCTAssertEqual(answers1.count, 3)
+    XCTAssert(answers1.contains(where: { $0["x"] == .lit(0) && $0["y"] == .lit(1) }))
+    XCTAssert(answers1.contains(where: { $0["x"] == .lit(1) && $0["y"] == .lit(2) }))
+    XCTAssert(answers1.contains(where: { $0["x"] == .lit(2) && $0["y"] == .lit(3) }))
+  }
+
+  func testSimpleDeductions() {
+    let kb: KnowledgeBase = [
+      .fact("play" , .lit("mia")),
+      .rule("happy", .lit("mia")) {
+        .fact("play", .lit("mia"))
+      },
+    ]
+
+    let answers0 = Array(kb.ask(.fact("happy", .lit("mia"))))
+    XCTAssertEqual(answers0.count, 1)
+    XCTAssertEqual(answers0[0]   , [:])
+
+    let answers1 = Array(kb.ask(.fact("happy", .var("who"))))
+    XCTAssertEqual(answers1.count, 1)
+    XCTAssertEqual(answers1[0]   , ["who": .lit("mia")])
+  }
+
+  func testRecursion() {
+    let x   : Term = .var("x")
+    let y   : Term = .var("y")
+    let z   : Term = .var("z")
+    let zero: Term = .lit("zero")
+
+    func succ(_ x: Term) -> Term {
+      return .fact("succ", x)
     }
 
-    func testFactsWithVariables() {
-        let kb: KnowledgeBase = [
-            .fact("<", .lit(0), .lit(1)),
-            .fact("<", .lit(1), .lit(2)),
-            .fact("<", .lit(2), .lit(3)),
-        ]
-
-        let answers0 = Array(kb.ask(.fact("<", .lit(0), .var("x"))))
-        XCTAssertEqual(answers0.count, 1)
-        XCTAssertEqual(answers0[0]   , ["x": .lit(1)])
-
-        let answers1 = Array(kb.ask(.fact("<", .var("x"), .var("y"))))
-        XCTAssertEqual(answers1.count, 3)
-        XCTAssert(answers1.contains(where: { $0["x"] == .lit(0) && $0["y"] == .lit(1) }))
-        XCTAssert(answers1.contains(where: { $0["x"] == .lit(1) && $0["y"] == .lit(2) }))
-        XCTAssert(answers1.contains(where: { $0["x"] == .lit(2) && $0["y"] == .lit(3) }))
+    func nat(value n: Int) -> Term {
+      if n == 0 {
+        return zero
+      } else {
+        return succ(nat(value: n - 1))
+      }
     }
 
-    func testSimpleDeductions() {
-        let kb: KnowledgeBase = [
-            .fact("play" , .lit("mia")),
-            .rule("happy", .lit("mia")) {
-                .fact("play", .lit("mia"))
-            },
-        ]
-
-        let answers0 = Array(kb.ask(.fact("happy", .lit("mia"))))
-        XCTAssertEqual(answers0.count, 1)
-        XCTAssertEqual(answers0[0]   , [:])
-
-        let answers1 = Array(kb.ask(.fact("happy", .var("who"))))
-        XCTAssertEqual(answers1.count, 1)
-        XCTAssertEqual(answers1[0]   , ["who": .lit("mia")])
-    }
-
-    func testRecursion() {
-        let x   : Term = .var("x")
-        let y   : Term = .var("y")
-        let z   : Term = .var("z")
-        let zero: Term = .lit("zero")
-
-        func succ(_ x: Term) -> Term {
-           return .fact("succ", x)
-        }
-
-        func nat(value n: Int) -> Term {
-           if n == 0 {
-               return zero
-           } else {
-               return succ(nat(value: n - 1))
-           }
-        }
-
-        let kb: KnowledgeBase = [
-           .fact("diff", zero, x, x),
-           .fact("diff", x, zero, x),
-           .rule("diff", succ(x), succ(y), z) {
-               .fact("diff", x, y, z)
-           },
-        ]
-
-        let query: Term = .fact("diff", nat(value: 2), nat(value: 4), .var("result"))
-        var answers = kb.ask(query)
-        let answer  = answers.next()
-        XCTAssertNotNil(answer)
-        XCTAssertEqual(answer?["result"], nat(value: 2))
-    }
-
-    func testLitSyntax() {
-        let play  : Term = "play"
-        let mia   : Term = "mia"
-        let happy : Term = "happy"
-        let who   = Term.var("who")
-        let kb: KnowledgeBase = [
-            play[mia],
-            { play[mia] && play[mia] } => happy[mia],
-        ]
-
-        let answers0 = Array(kb.ask(happy[mia]))
-        XCTAssertEqual(answers0.count, 1)
-        XCTAssertEqual(answers0[0]   , [:])
-
-        let answers1 = Array(kb.ask(happy[who]))
-        XCTAssertEqual(answers1.count, 1)
-        XCTAssertEqual(answers1[0]       , ["who": mia])
-        XCTAssertEqual(answers1[0]["who"], mia)
-        XCTAssertEqual(answers1[0][who]  , mia)
-
-        XCTAssertEqual(
-          { play[mia] && play[mia] } => happy[mia],
-          (play[mia] && play[mia]) => happy[mia]
-        )
-        XCTAssertEqual(
-          { play[mia] && play[mia] } => happy[mia],
-          happy[mia] |- { play[mia] && play[mia] }
-        )
-        XCTAssertEqual(
-          { play[mia] && play[mia] } => happy[mia],
-          happy[mia] |- (play[mia] && play[mia])
-        )
-        XCTAssertEqual(
-          { play[mia] && play[mia] } => happy[mia],
-          happy[mia] ⊢ { play[mia] ∧ play[mia] }
-        )
-        XCTAssertEqual(
-          { play[mia] && play[mia] } => happy[mia],
-          happy[mia] ⊢ (play[mia] ∧ play[mia])
-        )
-    }
+    let kb: KnowledgeBase = [
+      .fact("diff", zero, x, x),
+      .fact("diff", x, zero, x),
+      .rule("diff", succ(x), succ(y), z) {
+        .fact("diff", x, y, z)
+      },
+    ]
+
+    let query: Term = .fact("diff", nat(value: 2), nat(value: 4), .var("result"))
+    var answers = kb.ask(query)
+    let answer  = answers.next()
+    XCTAssertNotNil(answer)
+    XCTAssertEqual(answer?["result"], nat(value: 2))
+  }
+
+  func testLitSyntax() {
+    let play  : Term = "play"
+    let mia   : Term = "mia"
+    let happy : Term = "happy"
+    let who   = Term.var("who")
+    let kb: KnowledgeBase = [
+      play[mia],
+      { play[mia] && play[mia] } => happy[mia],
+    ]
+
+    let answers0 = Array(kb.ask(happy[mia]))
+    XCTAssertEqual(answers0.count, 1)
+    XCTAssertEqual(answers0[0]   , [:])
+
+    let answers1 = Array(kb.ask(happy[who]))
+    XCTAssertEqual(answers1.count, 1)
+    XCTAssertEqual(answers1[0]       , ["who": mia])
+    XCTAssertEqual(answers1[0]["who"], mia)
+    XCTAssertEqual(answers1[0][who]  , mia)
+
+    XCTAssertEqual(
+      { play[mia] && play[mia] } => happy[mia],
+      (play[mia] && play[mia]) => happy[mia]
+    )
+    XCTAssertEqual(
+      { play[mia] && play[mia] } => happy[mia],
+      happy[mia] |- { play[mia] && play[mia] }
+    )
+    XCTAssertEqual(
+      { play[mia] && play[mia] } => happy[mia],
+      happy[mia] |- (play[mia] && play[mia])
+    )
+    XCTAssertEqual(
+      { play[mia] && play[mia] } => happy[mia],
+      happy[mia] ⊢ { play[mia] ∧ play[mia] }
+    )
+    XCTAssertEqual(
+      { play[mia] && play[mia] } => happy[mia],
+      happy[mia] ⊢ (play[mia] ∧ play[mia])
+    )
+  }
 
 }

From a8fe0781f9ec0f6838439347505c5d9533cb0277 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 02:40:03 +0100
Subject: [PATCH 05/32] Remove useless references to `self`

---
 Sources/LogicKit/BindingMap.swift    | 12 ++--
 Sources/LogicKit/KnowledgeBase.swift | 26 ++++----
 Sources/LogicKit/Logger.swift        |  6 +-
 Sources/LogicKit/Realizer.swift      | 88 ++++++++++++++--------------
 Sources/LogicKit/Term.swift          |  2 +-
 5 files changed, 67 insertions(+), 67 deletions(-)

diff --git a/Sources/LogicKit/BindingMap.swift b/Sources/LogicKit/BindingMap.swift
index 274a3b8..afeb9ba 100644
--- a/Sources/LogicKit/BindingMap.swift
+++ b/Sources/LogicKit/BindingMap.swift
@@ -5,7 +5,7 @@ extension Dictionary where Key == String, Value == Term {
   func reified() -> [String: Term] {
     var result: [String: Term] = [:]
     for (name, term) in self {
-      result[name] = self.deepWalk(term)
+      result[name] = deepWalk(term)
     }
     return result
   }
@@ -14,7 +14,7 @@ extension Dictionary where Key == String, Value == Term {
     switch term {
     case .var(let name):
       return self[name].map({
-        self.shallowWalk($0)
+        shallowWalk($0)
       }) ?? term
     default:
       return term
@@ -22,14 +22,14 @@ extension Dictionary where Key == String, Value == Term {
   }
 
   func deepWalk(_ term: Term) -> Term {
-    let walked = self.shallowWalk(term)
+    let walked = shallowWalk(term)
     switch walked {
     case ._term(name: let name, arguments: let arguments):
-      return ._term(name: name, arguments: arguments.map(self.deepWalk))
+      return ._term(name: name, arguments: arguments.map(deepWalk))
     case .conjunction(let lhs, let rhs):
-      return .conjunction(self.deepWalk(lhs), self.deepWalk(rhs))
+      return .conjunction(deepWalk(lhs), deepWalk(rhs))
     case .disjunction(let lhs, let rhs):
-      return .disjunction(self.deepWalk(lhs), self.deepWalk(rhs))
+      return .disjunction(deepWalk(lhs), deepWalk(rhs))
     default:
       return walked
     }
diff --git a/Sources/LogicKit/KnowledgeBase.swift b/Sources/LogicKit/KnowledgeBase.swift
index ae472df..9df502f 100644
--- a/Sources/LogicKit/KnowledgeBase.swift
+++ b/Sources/LogicKit/KnowledgeBase.swift
@@ -10,7 +10,7 @@ public struct KnowledgeBase {
       preconditionFailure("invalid query")
     default:
       return RealizerAlternator(realizers: query.goals.map({
-        Realizer(goals: $0, knowledge: self.refreshed, logger: logger)
+        Realizer(goals: $0, knowledge: refreshed, logger: logger)
       }))
     }
   }
@@ -26,7 +26,7 @@ public struct KnowledgeBase {
   }
 
   var refreshed: KnowledgeBase {
-    return KnowledgeBase(knowledge: self.knowledge.map(self.renameVariables))
+    return KnowledgeBase(knowledge: knowledge.map(renameVariables))
   }
 
   func renameVariables(of term: Term) -> Term {
@@ -34,16 +34,16 @@ public struct KnowledgeBase {
     case .var(let name):
       return .var(name + "'")
     case ._term(let name, let arguments):
-      return ._term(name: name, arguments: arguments.map(self.renameVariables))
+      return ._term(name: name, arguments: arguments.map(renameVariables))
     case ._rule(let name, let arguments, let body):
       return ._rule(
         name     : name,
-        arguments: arguments.map(self.renameVariables),
-        body     : self.renameVariables(of: body))
+        arguments: arguments.map(renameVariables),
+        body     : renameVariables(of: body))
     case .conjunction(let lhs, let rhs):
-      return .conjunction(self.renameVariables(of: lhs), self.renameVariables(of: rhs))
+      return .conjunction(renameVariables(of: lhs), renameVariables(of: rhs))
     case .disjunction(let lhs, let rhs):
-      return .disjunction(self.renameVariables(of: lhs), self.renameVariables(of: rhs))
+      return .disjunction(renameVariables(of: lhs), renameVariables(of: rhs))
     default:
       return term
     }
@@ -61,23 +61,23 @@ extension KnowledgeBase: Collection {
   public typealias Element = Term
 
   public var startIndex: Int {
-    return self.knowledge.startIndex
+    return knowledge.startIndex
   }
 
   public var endIndex: Int {
-    return self.knowledge.endIndex
+    return knowledge.endIndex
   }
 
   public func index(after i: Int) -> Int {
-    return self.knowledge.index(after: i)
+    return knowledge.index(after: i)
   }
 
   public func makeIterator() -> Array<Term>.Iterator {
-    return self.knowledge.makeIterator()
+    return knowledge.makeIterator()
   }
 
   public subscript(position: Int) -> Term {
-    return self.knowledge[position]
+    return knowledge[position]
   }
 
 }
@@ -93,7 +93,7 @@ extension KnowledgeBase: ExpressibleByArrayLiteral {
 extension KnowledgeBase: CustomStringConvertible {
 
   public var description: String {
-    return self.knowledge.description
+    return knowledge.description
   }
 
 }
diff --git a/Sources/LogicKit/Logger.swift b/Sources/LogicKit/Logger.swift
index b96769b..4e57391 100644
--- a/Sources/LogicKit/Logger.swift
+++ b/Sources/LogicKit/Logger.swift
@@ -22,15 +22,15 @@ public protocol Logger {
 extension Logger {
 
   public func log(message: String) {
-    self.log(message: message, terminator: "\n", fontAttributes: [])
+    log(message: message, terminator: "\n", fontAttributes: [])
   }
 
   public func log(message: String, fontAttributes: [FontAttribute]) {
-    self.log(message: message, terminator: "\n", fontAttributes: fontAttributes)
+    log(message: message, terminator: "\n", fontAttributes: fontAttributes)
   }
 
   public func log(message: String, terminator: String) {
-    self.log(message: message, terminator: terminator, fontAttributes: [])
+    log(message: message, terminator: terminator, fontAttributes: [])
   }
 
 }
diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index c93129f..99d75a2 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -5,15 +5,15 @@ public struct RealizerAlternator: IteratorProtocol, Sequence {
   }
 
   public mutating func next() -> [String: Term]? {
-    while !self.realizers.isEmpty {
-      guard let result = self.realizers[self.index].next() else {
-        self.realizers.remove(at: index)
-        if !self.realizers.isEmpty {
-          self.index = self.index % self.realizers.count
+    while !realizers.isEmpty {
+      guard let result = realizers[index].next() else {
+        realizers.remove(at: index)
+        if !realizers.isEmpty {
+          index = index % realizers.count
         }
         continue
       }
-      self.index = (self.index + 1) % self.realizers.count
+      index = (index + 1) % realizers.count
       return result
     }
     return nil
@@ -44,33 +44,33 @@ struct Realizer: IteratorProtocol {
 
   mutating func next() -> [String: Term]? {
     // If we have a subrealizer running, pull its results first.
-    if let result = self.subRealizer?.next() {
+    if let result = subRealizer?.next() {
       return result
     } else {
-      if self.subRealizer != nil {
-        self.logger?.log(message: "backtacking", fontAttributes: [.dim])
-        self.subRealizer = nil
+      if subRealizer != nil {
+        logger?.log(message: "backtacking", fontAttributes: [.dim])
+        subRealizer = nil
       }
     }
 
-    let goal = self.goals.first!
-    self.logger?.log(message: "Attempting to realize ", terminator: "")
-    self.logger?.log(message: goal.description, fontAttributes: [.bold])
+    let goal = goals.first!
+    logger?.log(message: "Attempting to realize ", terminator: "")
+    logger?.log(message: goal.description, fontAttributes: [.bold])
 
     // Check for the built-in `~=~/2` predicate.
     if case ._term("lk.~=~", let args) = goal {
       assert(args.count == 2)
-      if let nodeResult = self.unify(goal: args[0], fact: args[1]) {
-        if self.goals.count > 1 {
-          let subGoals     = self.goals.dropFirst().map(nodeResult.deepWalk)
-          self.subRealizer = RealizerAlternator(realizers: [
+      if let nodeResult = unify(goal: args[0], fact: args[1]) {
+        if goals.count > 1 {
+          let subGoals     = goals.dropFirst().map(nodeResult.deepWalk)
+          subRealizer = RealizerAlternator(realizers: [
             Realizer(
               goals         : subGoals,
-              knowledge     : self.knowledge,
+              knowledge     : knowledge,
               parentBindings: nodeResult,
-              logger        : self.logger)
+              logger        : logger)
             ])
-          if let branchResult = self.subRealizer!.next() {
+          if let branchResult = subRealizer!.next() {
             return branchResult
               .merged(with: parentBindings)
               .reified()
@@ -84,21 +84,21 @@ struct Realizer: IteratorProtocol {
     }
 
     // Look for the next root clause.
-    while self.clauseIndex != self.knowledge.endIndex {
-      let clause = self.knowledge[self.clauseIndex]
-      self.clauseIndex += 1
+    while clauseIndex != knowledge.endIndex {
+      let clause = knowledge[clauseIndex]
+      clauseIndex += 1
 
-      self.logger?.log(message: "using "    , terminator: "", fontAttributes: [.dim])
-      self.logger?.log(message: "\(clause) ")
+      logger?.log(message: "using "    , terminator: "", fontAttributes: [.dim])
+      logger?.log(message: "\(clause) ")
 
       switch (goal, clause) {
       case (.val(let lvalue), .val(let rvalue)) where lvalue == rvalue:
-        if self.goals.count > 1 {
-          let subGoals     = Array(self.goals.dropFirst())
-          self.subRealizer = RealizerAlternator(realizers: [
-            Realizer(goals: subGoals, knowledge: self.knowledge, logger: self.logger)
+        if goals.count > 1 {
+          let subGoals     = Array(goals.dropFirst())
+          subRealizer = RealizerAlternator(realizers: [
+            Realizer(goals: subGoals, knowledge: knowledge, logger: logger)
           ])
-          if let branchResult = self.subRealizer!.next() {
+          if let branchResult = subRealizer!.next() {
             return branchResult
               .merged(with: parentBindings)
               .reified()
@@ -106,17 +106,17 @@ struct Realizer: IteratorProtocol {
         }
 
       case (._term(_, _), ._term(_, _)):
-        if let nodeResult = self.unify(goal: goal, fact: clause) {
-          if self.goals.count > 1 {
-            let subGoals     = self.goals.dropFirst().map(nodeResult.deepWalk)
-            self.subRealizer = RealizerAlternator(realizers: [
+        if let nodeResult = unify(goal: goal, fact: clause) {
+          if goals.count > 1 {
+            let subGoals     = goals.dropFirst().map(nodeResult.deepWalk)
+            subRealizer = RealizerAlternator(realizers: [
               Realizer(
                 goals         : subGoals,
-                knowledge     : self.knowledge,
+                knowledge     : knowledge,
                 parentBindings: nodeResult,
-                logger        : self.logger)
+                logger        : logger)
             ])
-            if let branchResult = self.subRealizer!.next() {
+            if let branchResult = subRealizer!.next() {
               return branchResult
                 .merged(with: parentBindings)
                 .reified()
@@ -133,8 +133,8 @@ struct Realizer: IteratorProtocol {
 
         // First we try to unify the rule head with the goal.
         let head: Term = ._term(name: goalName, arguments: ruleArguments)
-        if let nodeResult = self.unify(goal: goal, fact: head) {
-          let subGoals  = self.goals.dropFirst()
+        if let nodeResult = unify(goal: goal, fact: head) {
+          let subGoals  = goals.dropFirst()
             .map(nodeResult.deepWalk)
           let ruleGoals = ruleBody.goals
             .map({ $0.map(nodeResult.deepWalk) + subGoals })
@@ -146,14 +146,14 @@ struct Realizer: IteratorProtocol {
           // to `0` before we try satisfy `p($x, q(0))`. But if `$x` wasn't renamed,
           // we'd be trying to unify `$x` with `q($x)` while recursing.
 
-          self.subRealizer = RealizerAlternator(realizers: ruleGoals.map({
+          subRealizer = RealizerAlternator(realizers: ruleGoals.map({
             Realizer(
               goals         : $0,
-              knowledge     : self.knowledge.refreshed,
+              knowledge     : knowledge.refreshed,
               parentBindings: nodeResult,
-              logger        : self.logger)
+              logger        : logger)
           }))
-          if let branchResult = self.subRealizer!.next() {
+          if let branchResult = subRealizer!.next() {
             return nodeResult
               .merged(with: branchResult)
               .merged(with: parentBindings)
@@ -206,7 +206,7 @@ struct Realizer: IteratorProtocol {
       // Try unify subterms (i.e. arguments).
       var intermediateResult = bindings
       for (larg, rarg) in zip(largs, rargs) {
-        if let b = self.unify(goal: larg, fact: rarg, knowing: intermediateResult) {
+        if let b = unify(goal: larg, fact: rarg, knowing: intermediateResult) {
           intermediateResult = b
         } else {
           return nil
diff --git a/Sources/LogicKit/Term.swift b/Sources/LogicKit/Term.swift
index 17fb182..6d7bc42 100644
--- a/Sources/LogicKit/Term.swift
+++ b/Sources/LogicKit/Term.swift
@@ -27,7 +27,7 @@ public enum Term {
   }
 
   var goals: [[Term]] {
-    switch self.dnf {
+    switch dnf {
     case .conjunction(let lhs, let rhs):
       assert((lhs.goals.count == 1) && (rhs.goals.count == 1))
       return [lhs.goals[0] + rhs.goals[0]]

From 85cdc594852840ebcff8df8e877972be398c0075 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 11:37:29 +0100
Subject: [PATCH 06/32] Map goal realizers onto a class hierarchy

---
 Sources/LogicKit/KnowledgeBase.swift    |  2 +-
 Sources/LogicKit/Realizer.swift         | 23 +++++++++++++++++++----
 Tests/LogicKitTests/LogicKitTests.swift |  2 +-
 3 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/Sources/LogicKit/KnowledgeBase.swift b/Sources/LogicKit/KnowledgeBase.swift
index 9df502f..1fd3418 100644
--- a/Sources/LogicKit/KnowledgeBase.swift
+++ b/Sources/LogicKit/KnowledgeBase.swift
@@ -4,7 +4,7 @@ public struct KnowledgeBase {
     self.knowledge = knowledge
   }
 
-  public func ask(_ query: Term, logger: Logger? = nil) -> RealizerAlternator {
+  public func ask(_ query: Term, logger: Logger? = nil) -> RealizerBase {
     switch query {
     case .var(_), ._rule(_, _, _):
       preconditionFailure("invalid query")
diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index 99d75a2..14fd2f1 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -1,10 +1,24 @@
-public struct RealizerAlternator: IteratorProtocol, Sequence {
+/// Base class for realizers.
+public class RealizerBase: IteratorProtocol, Sequence {
+
+  public typealias Element = [String: Term]
+
+  fileprivate init() {}
+
+  public func next() -> [String: Term]? {
+    fatalError("not implemented")
+  }
+
+}
+
+/// Realizer that alternatively pulls results from multiple sub-realizers.
+public final class RealizerAlternator: RealizerBase {
 
   init<S>(realizers: S) where S: Sequence, S.Element == Realizer {
     self.realizers = Array(realizers)
   }
 
-  public mutating func next() -> [String: Term]? {
+  public override func next() -> [String: Term]? {
     while !realizers.isEmpty {
       guard let result = realizers[index].next() else {
         realizers.remove(at: index)
@@ -28,7 +42,8 @@ public struct RealizerAlternator: IteratorProtocol, Sequence {
 
 }
 
-struct Realizer: IteratorProtocol {
+/// Standard goal realizer.
+public final class Realizer: RealizerBase {
 
   init(
     goals         : [Term],
@@ -42,7 +57,7 @@ struct Realizer: IteratorProtocol {
     self.logger         = logger
   }
 
-  mutating func next() -> [String: Term]? {
+  public override func next() -> [String: Term]? {
     // If we have a subrealizer running, pull its results first.
     if let result = subRealizer?.next() {
       return result
diff --git a/Tests/LogicKitTests/LogicKitTests.swift b/Tests/LogicKitTests/LogicKitTests.swift
index e2d121f..12dbed7 100644
--- a/Tests/LogicKitTests/LogicKitTests.swift
+++ b/Tests/LogicKitTests/LogicKitTests.swift
@@ -84,7 +84,7 @@ class LogicKitTests: XCTestCase {
     ]
 
     let query: Term = .fact("diff", nat(value: 2), nat(value: 4), .var("result"))
-    var answers = kb.ask(query)
+    let answers = kb.ask(query)
     let answer  = answers.next()
     XCTAssertNotNil(answer)
     XCTAssertEqual(answer?["result"], nat(value: 2))

From d9b0d3066b3ddd790f6f208c5756b7922b926276 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 11:42:38 +0100
Subject: [PATCH 07/32] Code style and comments

---
 Sources/LogicKit/Realizer.swift | 46 +++++++++++++++++----------------
 1 file changed, 24 insertions(+), 22 deletions(-)

diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index 14fd2f1..c930a8e 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -18,6 +18,9 @@ public final class RealizerAlternator: RealizerBase {
     self.realizers = Array(realizers)
   }
 
+  private var index = 0
+  private var realizers: [Realizer]
+
   public override func next() -> [String: Term]? {
     while !realizers.isEmpty {
       guard let result = realizers[index].next() else {
@@ -33,30 +36,37 @@ public final class RealizerAlternator: RealizerBase {
     return nil
   }
 
-  public func makeIterator() -> RealizerAlternator {
-    return self
-  }
-
-  var index    : Int = 0
-  var realizers: [Realizer]
-
 }
 
 /// Standard goal realizer.
 public final class Realizer: RealizerBase {
 
-  init(
-    goals         : [Term],
-    knowledge     : KnowledgeBase,
+  internal init(
+    goals: [Term],
+    knowledge: KnowledgeBase,
     parentBindings: BindingMap = [:],
-    logger        : Logger? = nil)
+    logger: Logger? = nil)
   {
-    self.goals          = goals
-    self.knowledge      = knowledge
+    self.goals = goals
+    self.knowledge = knowledge
     self.parentBindings = parentBindings
-    self.logger         = logger
+    self.logger = logger
   }
 
+  /// The goals to realize.
+  private let goals: [Term]
+  /// The knowledge base.
+  private let knowledge: KnowledgeBase
+  /// The bindings already  determined by the parent realizer.
+  private let parentBindings: BindingMap
+  /// The optional logger, for debug purpose.
+  private var logger: Logger?
+
+  /// The index of the next clause to check.
+  private var clauseIndex = 0
+  /// The subrealizer, if any.
+  private var subRealizer: RealizerBase? = nil
+
   public override func next() -> [String: Term]? {
     // If we have a subrealizer running, pull its results first.
     if let result = subRealizer?.next() {
@@ -236,12 +246,4 @@ public final class Realizer: RealizerBase {
     }
   }
 
-  let goals         : [Term]
-  let knowledge     : KnowledgeBase
-  let parentBindings: BindingMap
-  var logger        : Logger?
-
-  var clauseIndex   : Int = 0
-  var subRealizer   : RealizerAlternator? = nil
-
 }

From 377b293cb6cfc66d5c7ce60875b2e6349020072a Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 11:47:41 +0100
Subject: [PATCH 08/32] Avoid creating unnecessary realizer alternators

---
 Sources/LogicKit/KnowledgeBase.swift | 12 ++++++++--
 Sources/LogicKit/Realizer.swift      | 34 +++++++++-------------------
 2 files changed, 21 insertions(+), 25 deletions(-)

diff --git a/Sources/LogicKit/KnowledgeBase.swift b/Sources/LogicKit/KnowledgeBase.swift
index 1fd3418..d75db58 100644
--- a/Sources/LogicKit/KnowledgeBase.swift
+++ b/Sources/LogicKit/KnowledgeBase.swift
@@ -8,10 +8,18 @@ public struct KnowledgeBase {
     switch query {
     case .var(_), ._rule(_, _, _):
       preconditionFailure("invalid query")
+
     default:
-      return RealizerAlternator(realizers: query.goals.map({
+      // Build an array of realizers for each conjunction of goals in the query.
+      let realizers = query.goals.map {
         Realizer(goals: $0, knowledge: refreshed, logger: logger)
-      }))
+      }
+
+      // Return the goal realizer(s).
+      assert(!realizers.isEmpty)
+      return realizers.count > 1
+        ? RealizerAlternator(realizers: realizers)
+        : realizers[0]
     }
   }
 
diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index c930a8e..68e687b 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -87,14 +87,9 @@ public final class Realizer: RealizerBase {
       assert(args.count == 2)
       if let nodeResult = unify(goal: args[0], fact: args[1]) {
         if goals.count > 1 {
-          let subGoals     = goals.dropFirst().map(nodeResult.deepWalk)
-          subRealizer = RealizerAlternator(realizers: [
-            Realizer(
-              goals         : subGoals,
-              knowledge     : knowledge,
-              parentBindings: nodeResult,
-              logger        : logger)
-            ])
+          let subGoals = goals.dropFirst().map(nodeResult.deepWalk)
+          subRealizer = Realizer(
+            goals: subGoals, knowledge: knowledge, parentBindings: nodeResult, logger: logger)
           if let branchResult = subRealizer!.next() {
             return branchResult
               .merged(with: parentBindings)
@@ -119,10 +114,8 @@ public final class Realizer: RealizerBase {
       switch (goal, clause) {
       case (.val(let lvalue), .val(let rvalue)) where lvalue == rvalue:
         if goals.count > 1 {
-          let subGoals     = Array(goals.dropFirst())
-          subRealizer = RealizerAlternator(realizers: [
-            Realizer(goals: subGoals, knowledge: knowledge, logger: logger)
-          ])
+          let subGoals = Array(goals.dropFirst())
+          subRealizer = Realizer(goals: subGoals, knowledge: knowledge, logger: logger)
           if let branchResult = subRealizer!.next() {
             return branchResult
               .merged(with: parentBindings)
@@ -133,14 +126,9 @@ public final class Realizer: RealizerBase {
       case (._term(_, _), ._term(_, _)):
         if let nodeResult = unify(goal: goal, fact: clause) {
           if goals.count > 1 {
-            let subGoals     = goals.dropFirst().map(nodeResult.deepWalk)
-            subRealizer = RealizerAlternator(realizers: [
-              Realizer(
-                goals         : subGoals,
-                knowledge     : knowledge,
-                parentBindings: nodeResult,
-                logger        : logger)
-            ])
+            let subGoals = goals.dropFirst().map(nodeResult.deepWalk)
+            subRealizer = Realizer(
+              goals: subGoals, knowledge: knowledge, parentBindings: nodeResult, logger: logger)
             if let branchResult = subRealizer!.next() {
               return branchResult
                 .merged(with: parentBindings)
@@ -173,10 +161,10 @@ public final class Realizer: RealizerBase {
 
           subRealizer = RealizerAlternator(realizers: ruleGoals.map({
             Realizer(
-              goals         : $0,
-              knowledge     : knowledge.refreshed,
+              goals: $0,
+              knowledge: knowledge.refreshed,
               parentBindings: nodeResult,
-              logger        : logger)
+              logger: logger)
           }))
           if let branchResult = subRealizer!.next() {
             return nodeResult

From 159ed1fd8725ee4b2bec346b626963d56fb0902d Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 12:00:09 +0100
Subject: [PATCH 09/32] Minor refactoring

---
 Sources/LogicKit/BindingMap.swift | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Sources/LogicKit/BindingMap.swift b/Sources/LogicKit/BindingMap.swift
index afeb9ba..c0040da 100644
--- a/Sources/LogicKit/BindingMap.swift
+++ b/Sources/LogicKit/BindingMap.swift
@@ -35,13 +35,13 @@ extension Dictionary where Key == String, Value == Term {
     }
   }
 
-  func binding(_ name: String, to term: Term) -> Dictionary {
+  func binding(_ name: String, to term: Term) -> BindingMap {
     var result = self
     result[name] = term
     return result
   }
 
-  func merged(with other: Dictionary) -> Dictionary {
+  func merged(with other: BindingMap) -> BindingMap {
     var result = self
     for (name, term) in other {
       result[name] = term

From 1a901178eda9b0745ed9384171792ffde32336c0 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 12:05:39 +0100
Subject: [PATCH 10/32] Minor refactoring

---
 Sources/LogicKit/Realizer.swift | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index 804b881..7f8c28b 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -69,12 +69,12 @@ public final class Realizer: RealizerBase {
 
   public override func next() -> [String: Term]? {
     // If we have a subrealizer running, pull its results first.
-    if let result = subRealizer?.next() {
-      return result
-        .merged(with: parentBindings)
-        .reified()
-    } else {
-      if subRealizer != nil {
+    if let sub = subRealizer {
+      if let result = sub.next() {
+        return result
+          .merged(with: parentBindings)
+          .reified()
+      } else {
         logger?.log(message: "backtacking", fontAttributes: [.dim])
         subRealizer = nil
       }

From 65394bc92f00427627c11cba74ac821969dcf4ab Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 12:36:06 +0100
Subject: [PATCH 11/32] Hide realizers and filter out intermediate variables
 from query results

---
 Sources/LogicKit/AnswerSet.swift        | 15 +++++++++++++++
 Sources/LogicKit/KnowledgeBase.swift    |  5 +++--
 Sources/LogicKit/Realizer.swift         |  8 ++++----
 Sources/LogicKit/Term.swift             | 18 ++++++++++++++++++
 Tests/LogicKitTests/LogicKitTests.swift |  2 +-
 5 files changed, 41 insertions(+), 7 deletions(-)
 create mode 100644 Sources/LogicKit/AnswerSet.swift

diff --git a/Sources/LogicKit/AnswerSet.swift b/Sources/LogicKit/AnswerSet.swift
new file mode 100644
index 0000000..a26f753
--- /dev/null
+++ b/Sources/LogicKit/AnswerSet.swift
@@ -0,0 +1,15 @@
+public struct AnswerSet: IteratorProtocol, Sequence {
+
+  init(realizer: RealizerBase, variables: Set<String>) {
+    self.realizer = realizer
+    self.variables = variables
+  }
+
+  private var realizer: RealizerBase
+  private var variables: Set<String>
+
+  public func next() -> BindingMap? {
+    return realizer.next()?.reified().filter { variables.contains($0.key) }
+  }
+
+}
diff --git a/Sources/LogicKit/KnowledgeBase.swift b/Sources/LogicKit/KnowledgeBase.swift
index d75db58..ac5fb4d 100644
--- a/Sources/LogicKit/KnowledgeBase.swift
+++ b/Sources/LogicKit/KnowledgeBase.swift
@@ -4,7 +4,7 @@ public struct KnowledgeBase {
     self.knowledge = knowledge
   }
 
-  public func ask(_ query: Term, logger: Logger? = nil) -> RealizerBase {
+  public func ask(_ query: Term, logger: Logger? = nil) -> AnswerSet {
     switch query {
     case .var(_), ._rule(_, _, _):
       preconditionFailure("invalid query")
@@ -17,9 +17,10 @@ public struct KnowledgeBase {
 
       // Return the goal realizer(s).
       assert(!realizers.isEmpty)
-      return realizers.count > 1
+      let iterator = realizers.count > 1
         ? RealizerAlternator(realizers: realizers)
         : realizers[0]
+      return AnswerSet(realizer: iterator, variables: query.variables)
     }
   }
 
diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index 7f8c28b..1ae9a96 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -1,5 +1,5 @@
 /// Base class for realizers.
-public class RealizerBase: IteratorProtocol, Sequence {
+class RealizerBase: IteratorProtocol {
 
   public typealias Element = [String: Term]
 
@@ -12,7 +12,7 @@ public class RealizerBase: IteratorProtocol, Sequence {
 }
 
 /// Realizer that alternatively pulls results from multiple sub-realizers.
-public final class RealizerAlternator: RealizerBase {
+final class RealizerAlternator: RealizerBase {
 
   init<S>(realizers: S) where S: Sequence, S.Element == Realizer {
     self.realizers = Array(realizers)
@@ -39,9 +39,9 @@ public final class RealizerAlternator: RealizerBase {
 }
 
 /// Standard goal realizer.
-public final class Realizer: RealizerBase {
+final class Realizer: RealizerBase {
 
-  internal init(
+  init(
     goals: [Term],
     knowledge: KnowledgeBase,
     parentBindings: BindingMap = [:],
diff --git a/Sources/LogicKit/Term.swift b/Sources/LogicKit/Term.swift
index 6d7bc42..25b0332 100644
--- a/Sources/LogicKit/Term.swift
+++ b/Sources/LogicKit/Term.swift
@@ -38,6 +38,24 @@ public enum Term {
     }
   }
 
+  var variables: Set<String> {
+    switch self {
+    case .var(let x):
+      return [x]
+    case ._term(name: _, arguments: let subterms):
+      return subterms.map({ $0.variables }).reduce(Set<String>(), { $0.union($1) })
+    case ._rule(name: _, arguments: let subterms, body: let body):
+      let subtermVariables = subterms.map({ $0.variables }).reduce(Set<String>(), { $0.union($1) })
+      return body.variables.union(subtermVariables)
+    case .conjunction(let lhs, let rhs):
+      return lhs.variables.union(rhs.variables)
+    case .disjunction(let lhs, let rhs):
+      return lhs.variables.union(rhs.variables)
+    default:
+      return []
+    }
+  }
+
   // MARK: EDSL
 
   public static func lit<T>(_ value: T) -> Term where T: Hashable {
diff --git a/Tests/LogicKitTests/LogicKitTests.swift b/Tests/LogicKitTests/LogicKitTests.swift
index 12dbed7..8803ec7 100644
--- a/Tests/LogicKitTests/LogicKitTests.swift
+++ b/Tests/LogicKitTests/LogicKitTests.swift
@@ -85,7 +85,7 @@ class LogicKitTests: XCTestCase {
 
     let query: Term = .fact("diff", nat(value: 2), nat(value: 4), .var("result"))
     let answers = kb.ask(query)
-    let answer  = answers.next()
+    var answer  = answers.next()
     XCTAssertNotNil(answer)
     XCTAssertEqual(answer?["result"], nat(value: 2))
   }

From 13b032117af10c9677e04ab9b1acb8f12b0faaf4 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 12:46:29 +0100
Subject: [PATCH 12/32] Add test for backtracking

---
 Tests/LogicKitTests/LogicKitTests.swift   | 31 +++++++++++++++++++++++
 Tests/LogicKitTests/XCTestManifests.swift |  2 ++
 2 files changed, 33 insertions(+)

diff --git a/Tests/LogicKitTests/LogicKitTests.swift b/Tests/LogicKitTests/LogicKitTests.swift
index 8803ec7..e9f4fb4 100644
--- a/Tests/LogicKitTests/LogicKitTests.swift
+++ b/Tests/LogicKitTests/LogicKitTests.swift
@@ -90,6 +90,37 @@ class LogicKitTests: XCTestCase {
     XCTAssertEqual(answer?["result"], nat(value: 2))
   }
 
+  func testBacktracking() {
+    let x: Term = .var("x")
+    let y: Term = .var("y")
+    let z: Term = .var("z")
+    let w: Term = .var("w")
+
+    let kb: KnowledgeBase = [
+      .fact("link", "0", "1"),
+      .fact("link", "1", "2"),
+      .fact("link", "2", "4"),
+      .fact("link", "1", "3"),
+      .fact("link", "3", "4"),
+      .rule("path", x, y, .fact("c", x, .fact("c", y, "nil"))) {
+        .fact("link", x, y)
+      },
+      .rule("path", x, y, .fact("c", x, w)) {
+        .fact("link", x, z) && .fact("path", z, y, w)
+      }
+    ]
+
+    let query: Term = .fact("path", "0", "4", .var("nodes"))
+    let answers = Array(kb.ask(query))
+
+    // There should be two paths from 0 to 4.
+    XCTAssertEqual(answers.count, 2)
+
+    // All paths should bind the variable `nodes`.
+    XCTAssertNotNil(answers[0]["nodes"])
+    XCTAssertNotNil(answers[1]["nodes"])
+  }
+
   func testLitSyntax() {
     let play  : Term = "play"
     let mia   : Term = "mia"
diff --git a/Tests/LogicKitTests/XCTestManifests.swift b/Tests/LogicKitTests/XCTestManifests.swift
index d94e336..e759a96 100644
--- a/Tests/LogicKitTests/XCTestManifests.swift
+++ b/Tests/LogicKitTests/XCTestManifests.swift
@@ -12,8 +12,10 @@ extension BindingMapTests {
 
 extension LogicKitTests {
     static let __allTests = [
+        ("testBacktracking", testBacktracking),
         ("testConstantFacts", testConstantFacts),
         ("testFactsWithVariables", testFactsWithVariables),
+        ("testLitSyntax", testLitSyntax),
         ("testRecursion", testRecursion),
         ("testSimpleDeductions", testSimpleDeductions),
     ]

From e1c91da1dcc55c849e543105fa89482f57b34467 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 12:48:02 +0100
Subject: [PATCH 13/32] Code style

---
 Sources/LogicKit/KnowledgeBase.swift | 2 +-
 Sources/LogicKit/Realizer.swift      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Sources/LogicKit/KnowledgeBase.swift b/Sources/LogicKit/KnowledgeBase.swift
index ac5fb4d..3647a49 100644
--- a/Sources/LogicKit/KnowledgeBase.swift
+++ b/Sources/LogicKit/KnowledgeBase.swift
@@ -6,7 +6,7 @@ public struct KnowledgeBase {
 
   public func ask(_ query: Term, logger: Logger? = nil) -> AnswerSet {
     switch query {
-    case .var(_), ._rule(_, _, _):
+    case .var, ._rule:
       preconditionFailure("invalid query")
 
     default:
diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index 1ae9a96..f55f00a 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -125,7 +125,7 @@ final class Realizer: RealizerBase {
           }
         }
 
-      case (._term(_, _), ._term(_, _)):
+      case (._term, ._term):
         if let nodeResult = unify(goal: goal, fact: clause) {
           if goals.count > 1 {
             let subGoals = goals.dropFirst().map(nodeResult.deepWalk)

From 28bb409d4339be19ad3fa8739f560088fc3a87a8 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 12:49:22 +0100
Subject: [PATCH 14/32] Reify only once in `AnswerSet.next()`

---
 Sources/LogicKit/Realizer.swift | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index f55f00a..0333d01 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -73,7 +73,6 @@ final class Realizer: RealizerBase {
       if let result = sub.next() {
         return result
           .merged(with: parentBindings)
-          .reified()
       } else {
         logger?.log(message: "backtacking", fontAttributes: [.dim])
         subRealizer = nil
@@ -95,12 +94,10 @@ final class Realizer: RealizerBase {
           if let branchResult = subRealizer!.next() {
             return branchResult
               .merged(with: parentBindings)
-              .reified()
           }
         } else {
           return nodeResult
             .merged(with: parentBindings)
-            .reified()
         }
       }
     }
@@ -121,7 +118,6 @@ final class Realizer: RealizerBase {
           if let branchResult = subRealizer!.next() {
             return branchResult
               .merged(with: parentBindings)
-              .reified()
           }
         }
 
@@ -134,12 +130,10 @@ final class Realizer: RealizerBase {
             if let branchResult = subRealizer!.next() {
               return branchResult
                 .merged(with: parentBindings)
-                .reified()
             }
           } else {
             return nodeResult
               .merged(with: parentBindings)
-              .reified()
           }
         }
 
@@ -172,7 +166,6 @@ final class Realizer: RealizerBase {
             return nodeResult
               .merged(with: branchResult)
               .merged(with: parentBindings)
-              .reified()
           }
         }
 

From ef7c9298cb6ac3913382473424dcc91af0b81025 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 12:49:59 +0100
Subject: [PATCH 15/32] Refactor `BindingMap.reified` as a computed property

---
 Sources/LogicKit/AnswerSet.swift          | 2 +-
 Sources/LogicKit/BindingMap.swift         | 2 +-
 Tests/LogicKitTests/BindingMapTests.swift | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Sources/LogicKit/AnswerSet.swift b/Sources/LogicKit/AnswerSet.swift
index a26f753..e8e3555 100644
--- a/Sources/LogicKit/AnswerSet.swift
+++ b/Sources/LogicKit/AnswerSet.swift
@@ -9,7 +9,7 @@ public struct AnswerSet: IteratorProtocol, Sequence {
   private var variables: Set<String>
 
   public func next() -> BindingMap? {
-    return realizer.next()?.reified().filter { variables.contains($0.key) }
+    return realizer.next()?.reified.filter { variables.contains($0.key) }
   }
 
 }
diff --git a/Sources/LogicKit/BindingMap.swift b/Sources/LogicKit/BindingMap.swift
index c0040da..64782b5 100644
--- a/Sources/LogicKit/BindingMap.swift
+++ b/Sources/LogicKit/BindingMap.swift
@@ -2,7 +2,7 @@ public typealias BindingMap = Dictionary<String, Term>
 
 extension Dictionary where Key == String, Value == Term {
 
-  func reified() -> [String: Term] {
+  var reified: [String: Term] {
     var result: [String: Term] = [:]
     for (name, term) in self {
       result[name] = deepWalk(term)
diff --git a/Tests/LogicKitTests/BindingMapTests.swift b/Tests/LogicKitTests/BindingMapTests.swift
index f7ee649..cc37a07 100644
--- a/Tests/LogicKitTests/BindingMapTests.swift
+++ b/Tests/LogicKitTests/BindingMapTests.swift
@@ -38,7 +38,7 @@ class BindingMapTests: XCTestCase {
       "y": .var("z"),
       "z": .fact("t", .var("w"))
     ]
-    let reifiedMap = bindingMap.reified()
+    let reifiedMap = bindingMap.reified
 
     XCTAssertEqual(reifiedMap["w"], .fact("a"))
     XCTAssertEqual(reifiedMap["x"], .fact("t", .fact("a")))

From 87b882c9a4238e5124bf393a631c7e12081955cd Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 12:51:52 +0100
Subject: [PATCH 16/32] Code style

---
 Sources/LogicKit/BindingMap.swift    | 4 +---
 Sources/LogicKit/KnowledgeBase.swift | 4 ++--
 Sources/LogicKit/Term.swift          | 1 -
 3 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/Sources/LogicKit/BindingMap.swift b/Sources/LogicKit/BindingMap.swift
index 64782b5..6cab79d 100644
--- a/Sources/LogicKit/BindingMap.swift
+++ b/Sources/LogicKit/BindingMap.swift
@@ -13,9 +13,7 @@ extension Dictionary where Key == String, Value == Term {
   func shallowWalk(_ term: Term) -> Term {
     switch term {
     case .var(let name):
-      return self[name].map({
-        shallowWalk($0)
-      }) ?? term
+      return self[name].map({ shallowWalk($0) }) ?? term
     default:
       return term
     }
diff --git a/Sources/LogicKit/KnowledgeBase.swift b/Sources/LogicKit/KnowledgeBase.swift
index 3647a49..5d4de1c 100644
--- a/Sources/LogicKit/KnowledgeBase.swift
+++ b/Sources/LogicKit/KnowledgeBase.swift
@@ -46,9 +46,9 @@ public struct KnowledgeBase {
       return ._term(name: name, arguments: arguments.map(renameVariables))
     case ._rule(let name, let arguments, let body):
       return ._rule(
-        name     : name,
+        name: name,
         arguments: arguments.map(renameVariables),
-        body     : renameVariables(of: body))
+        body: renameVariables(of: body))
     case .conjunction(let lhs, let rhs):
       return .conjunction(renameVariables(of: lhs), renameVariables(of: rhs))
     case .disjunction(let lhs, let rhs):
diff --git a/Sources/LogicKit/Term.swift b/Sources/LogicKit/Term.swift
index 25b0332..0e63c78 100644
--- a/Sources/LogicKit/Term.swift
+++ b/Sources/LogicKit/Term.swift
@@ -150,7 +150,6 @@ public enum Term {
 
 }
 
-
 extension Term: Hashable {
 }
 

From 1cd1bb50f6e7243d7b91d2674db38782046118d2 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 16:15:29 +0100
Subject: [PATCH 17/32] Remove synthetized conformance requirement

---
 Sources/LogicKit/KnowledgeBase.swift | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Sources/LogicKit/KnowledgeBase.swift b/Sources/LogicKit/KnowledgeBase.swift
index 5d4de1c..53bd7fb 100644
--- a/Sources/LogicKit/KnowledgeBase.swift
+++ b/Sources/LogicKit/KnowledgeBase.swift
@@ -81,10 +81,6 @@ extension KnowledgeBase: Collection {
     return knowledge.index(after: i)
   }
 
-  public func makeIterator() -> Array<Term>.Iterator {
-    return knowledge.makeIterator()
-  }
-
   public subscript(position: Int) -> Term {
     return knowledge[position]
   }

From 73332c3e369ec511d8547ff9518a951c950afe86 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sat, 23 Feb 2019 16:16:11 +0100
Subject: [PATCH 18/32] Allow the default logger to discard styling

---
 Sources/LogicKit/Logger.swift | 36 +++++++++++++++++++++--------------
 1 file changed, 22 insertions(+), 14 deletions(-)

diff --git a/Sources/LogicKit/Logger.swift b/Sources/LogicKit/Logger.swift
index 4e57391..cbf551f 100644
--- a/Sources/LogicKit/Logger.swift
+++ b/Sources/LogicKit/Logger.swift
@@ -37,22 +37,30 @@ extension Logger {
 
 public struct DefaultLogger: Logger {
 
-  public init() {}
+  public init(useFontAttributes: Bool = true) {
+    self.useFontAttributes = useFontAttributes
+  }
+
+  public let useFontAttributes: Bool
 
   public func log(message: String, terminator: String, fontAttributes: [FontAttribute]) {
-    let attributes = fontAttributes.compactMap({
-      switch $0 {
-      case .bold:
-        return "\u{001B}[1m"
-      case .dim:
-        return "\u{001B}[2m"
-      case .foreground(let color):
-        return "\u{001B}[\(DefaultLogger.foreground[color] ?? "39m")"
-      case .background(let color):
-        return "\u{001B}[\(DefaultLogger.background[color] ?? "40m")"
-      }
-    }).joined(separator: "")
-    print("\(attributes)\(message)\u{001B}[0m", terminator: terminator)
+    if useFontAttributes {
+      let attributes = fontAttributes.compactMap({
+        switch $0 {
+        case .bold:
+          return "\u{001B}[1m"
+        case .dim:
+          return "\u{001B}[2m"
+        case .foreground(let color):
+          return "\u{001B}[\(DefaultLogger.foreground[color] ?? "39m")"
+        case .background(let color):
+          return "\u{001B}[\(DefaultLogger.background[color] ?? "40m")"
+        }
+      }).joined(separator: "")
+      print("\(attributes)\(message)\u{001B}[0m", terminator: terminator)
+    } else {
+      print(message, terminator: terminator)
+    }
   }
 
   static let foreground: [FontColor: String] = [

From 9f7dd81510b6cc27156c30c24332fd93091a7e88 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 00:51:16 +0100
Subject: [PATCH 19/32] Implement some built-in axioms

---
 Package.swift                               |   4 +-
 Sources/LogicKitBuiltins/List.swift         | 101 ++++++++++
 Sources/LogicKitBuiltins/Nat.swift          | 185 ++++++++++++++++++
 Tests/LogicKitBuiltinsTests/ListTests.swift |  56 ++++++
 Tests/LogicKitBuiltinsTests/NatTests.swift  | 197 ++++++++++++++++++++
 5 files changed, 542 insertions(+), 1 deletion(-)
 create mode 100644 Sources/LogicKitBuiltins/List.swift
 create mode 100644 Sources/LogicKitBuiltins/Nat.swift
 create mode 100644 Tests/LogicKitBuiltinsTests/ListTests.swift
 create mode 100644 Tests/LogicKitBuiltinsTests/NatTests.swift

diff --git a/Package.swift b/Package.swift
index c2999ba..62524d4 100644
--- a/Package.swift
+++ b/Package.swift
@@ -5,10 +5,12 @@ import PackageDescription
 let package = Package(
   name: "LogicKit",
   products: [
-    .library(name: "LogicKit", type: .static, targets: ["LogicKit"]),
+    .library(name: "LogicKit", type: .static, targets: ["LogicKit", "LogicKitBuiltins"]),
   ],
   targets: [
     .target(name: "LogicKit"),
+    .target(name: "LogicKitBuiltins", dependencies: ["LogicKit"]),
     .testTarget(name: "LogicKitTests", dependencies: ["LogicKit"]),
+    .testTarget(name: "LogicKitBuiltinsTests", dependencies: ["LogicKitBuiltins"]),
   ]
 )
diff --git a/Sources/LogicKitBuiltins/List.swift b/Sources/LogicKitBuiltins/List.swift
new file mode 100644
index 0000000..e657e49
--- /dev/null
+++ b/Sources/LogicKitBuiltins/List.swift
@@ -0,0 +1,101 @@
+import LogicKit
+
+public enum List {
+
+  // MARK: Generators
+
+  public static let empty: Term = .lit("list::empty")
+
+  public static func cons(_ head: Term, _ tail: Term) -> Term {
+    guard isList(tail)
+      else { fatalError("'\(tail)' is not a list") }
+    return .fact("list::cons", head, tail)
+  }
+
+  // MARK: Predicates
+
+  public static func count(list: Term, count: Term) -> Term {
+    assert(isList(list), "'\(list)' is not a builtin list")
+
+    return .fact("list::count", list, count)
+  }
+
+  public static func contains(list: Term, element: Term) -> Term {
+    assert(isList(list), "'\(list)' is not a builtin list")
+
+    return .fact("list::contains", list, element)
+  }
+
+  public static func concat(_ lhs: Term, _ rhs: Term, _ res: Term) -> Term {
+    assert(isList(lhs), "'\(lhs)' is not a builtin list")
+    assert(isList(rhs), "'\(rhs)' is not a builtin list")
+    assert(isList(res), "'\(res)' is not a builtin list")
+
+    return .fact("list::concat", lhs, rhs, res)
+  }
+
+  // MARK: Axioms
+
+  public static var axioms: [Term] { return countAxioms + containsAxioms + concatAxioms }
+
+  public static let countAxioms: [Term] = {
+    let a: Term = .var("a")
+    let b: Term = .var("b")
+    let c: Term = .var("c")
+
+    return [
+      .fact("list::count", empty, Nat.zero),
+      .rule("list::count", cons(a, b), Nat.succ(c)) {
+        .fact("list::count", b, c)
+      },
+    ]
+  }()
+
+  public static let containsAxioms: [Term] = {
+    let a: Term = .var("a")
+    let b: Term = .var("b")
+    let c: Term = .var("c")
+
+    return [
+      .fact("list::contains", cons(a, b), a),
+      .rule("list::contains", cons(a, b), c) {
+        .fact("list::contains", b, c)
+      },
+    ]
+  }()
+
+  public static let concatAxioms: [Term] = {
+    let a: Term = .var("a")
+    let b: Term = .var("b")
+    let c: Term = .var("c")
+    let d: Term = .var("d")
+
+    return [
+      .fact("list::concat", empty, a, a),
+      .fact("list::concat", a, empty, a),
+      .rule("list::concat", cons(a, b), c, cons(a, d)) {
+        .fact("list::concat", b, c, d)
+      },
+    ]
+  }()
+
+  // MARK: Helpers
+
+  public static func from<C>(elements: C) -> Term where C: Collection, C.Element == Term {
+    return !elements.isEmpty
+      ? cons(elements.first!, from(elements: elements.dropFirst()))
+      : empty
+  }
+
+  public static func isList(_ t: Term) -> Bool {
+    switch t {
+    case .var, empty:
+      return true
+    case ._term("list::cons", let args):
+      return args.count == 2 && isList(args[1])
+    default:
+      return false
+    }
+  }
+
+}
diff --git a/Sources/LogicKitBuiltins/Nat.swift b/Sources/LogicKitBuiltins/Nat.swift
new file mode 100644
index 0000000..0475e7c
--- /dev/null
+++ b/Sources/LogicKitBuiltins/Nat.swift
@@ -0,0 +1,185 @@
+import LogicKit
+
+public enum Nat {
+
+  // MARK: Generators
+
+  public static let zero: Term = .lit("nat::0")
+
+  public static func succ(_ n: Term) -> Term {
+    assert(isNat(n), "'\(n)' is not a builtin natural number")
+    return .fact("nat::succ", n)
+  }
+
+  // MARK: Predicates
+
+  public static func greater(_ lhs: Term, _ rhs: Term) -> Term {
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(rhs), "'\(rhs)' is not a builtin natural number")
+
+    return .fact("nat::>", lhs, rhs)
+  }
+
+  public static func greaterOrEqual(_ lhs: Term, _ rhs: Term) -> Term {
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(rhs), "'\(rhs)' is not a builtin natural number")
+
+    return .fact("nat::>=", lhs, rhs)
+  }
+
+  public static func smaller(_ lhs: Term, _ rhs: Term) -> Term {
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(rhs), "'\(rhs)' is not a builtin natural number")
+
+    return .fact("nat::<", lhs, rhs)
+  }
+
+  public static func smallerOrEqual(_ lhs: Term, _ rhs: Term) -> Term {
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(rhs), "'\(rhs)' is not a builtin natural number")
+
+    return .fact("nat::<=", lhs, rhs)
+  }
+
+  public static func add(_ lhs: Term, _ rhs: Term, _ res: Term) -> Term {
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(res), "'\(res)' is not a builtin natural number")
+
+    return .fact("nat::+", lhs, rhs, res)
+  }
+
+  public static func sub(_ lhs: Term, _ rhs: Term, _ res: Term) -> Term {
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(res), "'\(res)' is not a builtin natural number")
+
+    return .fact("nat::-", lhs, rhs, res)
+  }
+
+  public static func mul(_ lhs: Term, _ rhs: Term, _ res: Term) -> Term {
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(res), "'\(res)' is not a builtin natural number")
+
+    return .fact("nat::*", lhs, rhs, res)
+  }
+
+  public static func div(_ lhs: Term, _ rhs: Term, _ res: Term) -> Term {
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(res), "'\(res)' is not a builtin natural number")
+
+    return .fact("nat::/", lhs, rhs, res)
+  }
+
+  public static func mod(_ lhs: Term, _ rhs: Term, _ res: Term) -> Term {
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(lhs), "'\(lhs)' is not a builtin natural number")
+    assert(isNat(res), "'\(res)' is not a builtin natural number")
+
+    return .fact("nat::%", lhs, rhs, res)
+  }
+
+  // MARK: Axioms
+
+  public static var axioms: [Term] { return arithmeticAxioms }
+
+  public static let relationAxioms: [Term] = {
+    let x: Term = .var("x")
+    let y: Term = .var("y")
+
+    return [
+      .fact("nat::>", succ(x), zero),
+      .rule("nat::>", succ(x), succ(y)) {
+        greater(x, y)
+      },
+
+      .fact("nat::>=", x, x),
+      .rule("nat::>=", x, y) {
+        greater(x, y)
+      },
+
+      .fact("nat::<", zero, succ(x)),
+      .rule("nat::<", succ(x), succ(y)) {
+        smaller(x, y)
+      },
+
+      .fact("nat::<=", x, x),
+      .rule("nat::<=", x, y) {
+        smaller(x, y)
+      },
+    ]
+  }()
+
+  public static let arithmeticAxioms: [Term] = {
+    let v: Term = .var("v")
+    let w: Term = .var("w")
+    let x: Term = .var("x")
+    let y: Term = .var("y")
+    let z: Term = .var("z")
+
+    return relationAxioms + [
+      .fact("nat::+", zero, y, y),
+      .rule("nat::+", succ(x), y, z) {
+        add(x, succ(y), z)
+      },
+
+      .fact("nat::-", x, zero, x),
+      .rule("nat::-", succ(x), succ(y), z) {
+        sub(x, y, z)
+      },
+
+      .fact("nat::*", zero, y, zero),
+      .rule("nat::*", succ(x), y, z) {
+        mul(x, y, w) && add(w, y, z)
+      },
+
+      .rule("nat::/", x, y, zero) {
+        smaller(x, y)
+      },
+      .rule("nat::/", x, succ(y), succ(z)) {
+        sub(x, succ(y), w) && div(w, succ(y), z)
+      },
+
+      .rule("nat::%", x, succ(y), z) {
+        div(x, succ(y), w) && mul(succ(y), w, v) && sub(x, v, z)
+      }
+    ]
+  }()
+
+  // MARK: Helpers
+
+  public static func from(_ i: Int) -> Term {
+    return i > 0
+      ? succ(from(i - 1))
+      : zero
+  }
+
+  public static func asSwiftInt(_ t: Term) -> Int? {
+    switch t {
+    case zero:
+      return 0
+    case ._term("nat::succ", let u):
+      if let n = asSwiftInt(u.first!) {
+        return n + 1
+      } else {
+        return nil
+      }
+    default:
+      return nil
+    }
+  }
+
+  public static func isNat(_ t: Term) -> Bool {
+    switch t {
+    case .var, zero:
+      return true
+    case ._term("nat::succ", let n):
+      return n.count == 1 && isNat(n[0])
+    default:
+      return false
+    }
+  }
+
+}
diff --git a/Tests/LogicKitBuiltinsTests/ListTests.swift b/Tests/LogicKitBuiltinsTests/ListTests.swift
new file mode 100644
index 0000000..5d83bdd
--- /dev/null
+++ b/Tests/LogicKitBuiltinsTests/ListTests.swift
@@ -0,0 +1,56 @@
+import LogicKit
+@testable import LogicKitBuiltins
+import XCTest
+
+class ListTests: XCTestCase {
+
+  func testCount() {
+    let kb = KnowledgeBase(knowledge: List.countAxioms)
+    var query: Term
+    var binding: BindingMap?
+
+    let list = List.from(elements: ["1", "2", "3"])
+
+    query = List.count(list: list, count: .var("?"))
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"],  Nat.from(3))
+  }
+
+  func testContains() {
+    let kb = KnowledgeBase(knowledge: List.containsAxioms)
+    var query: Term
+    var binding: BindingMap?
+
+    let list = List.from(elements: ["1", "2", "3"])
+
+    query = List.contains(list: list, element: "0")
+    binding = kb.ask(query).next()
+    XCTAssertNil(binding)
+
+    query = List.contains(list: list, element: "1")
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    query = List.contains(list: list, element: "2")
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    query = List.contains(list: list, element: "3")
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+  }
+
+  func testConcat() {
+    let kb = KnowledgeBase(knowledge: List.concatAxioms)
+    var query: Term
+    var binding: BindingMap?
+
+    let list1 = List.from(elements: ["1", "2", "3"])
+    let list2 = List.from(elements: ["4", "5", "6"])
+
+    query = List.concat(list1, list2, .var("?"))
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"],  List.from(elements: ["1", "2", "3", "4", "5", "6"]))
+  }
+
+}
diff --git a/Tests/LogicKitBuiltinsTests/NatTests.swift b/Tests/LogicKitBuiltinsTests/NatTests.swift
new file mode 100644
index 0000000..925eee4
--- /dev/null
+++ b/Tests/LogicKitBuiltinsTests/NatTests.swift
@@ -0,0 +1,197 @@
+import LogicKit
+@testable import LogicKitBuiltins
+import XCTest
+
+class NatTests: XCTestCase {
+
+  func testGreater() {
+    let kb = KnowledgeBase(knowledge: Nat.relationAxioms)
+    var query: Term
+
+    query = Nat.greater(Nat.from(2), Nat.from(2))  // 2 > 2
+    XCTAssert(Array(kb.ask(query)).isEmpty)
+    query = Nat.greater(Nat.from(5), Nat.from(2))  // 5 > 2
+    XCTAssertEqual(Array(kb.ask(query)).count, 1)
+    query = Nat.greater(Nat.from(2), Nat.from(5))  // 2 > 5
+    XCTAssert(Array(kb.ask(query)).isEmpty)
+  }
+
+  func testGreaterOrEqual() {
+    let kb = KnowledgeBase(knowledge: Nat.relationAxioms)
+    var query: Term
+
+    query = Nat.greaterOrEqual(Nat.from(2), Nat.from(2))  // 2 >= 2
+    XCTAssertEqual(Array(kb.ask(query)).count, 1)
+    query = Nat.greaterOrEqual(Nat.from(5), Nat.from(2))  // 5 >= 2
+    XCTAssertEqual(Array(kb.ask(query)).count, 1)
+    query = Nat.greaterOrEqual(Nat.from(2), Nat.from(5))  // 2 >= 5
+    XCTAssert(Array(kb.ask(query)).isEmpty)
+  }
+
+  func testSmaller() {
+    let kb = KnowledgeBase(knowledge: Nat.relationAxioms)
+    var query: Term
+
+    query = Nat.smaller(Nat.from(2), Nat.from(2))  // 2 < 2
+    XCTAssert(Array(kb.ask(query)).isEmpty)
+    query = Nat.smaller(Nat.from(5), Nat.from(2))  // 5 < 2
+    XCTAssert(Array(kb.ask(query)).isEmpty)
+    query = Nat.smaller(Nat.from(2), Nat.from(5))  // 2 < 5
+    XCTAssertEqual(Array(kb.ask(query)).count, 1)
+  }
+
+  func testSmallerOrEqual() {
+    let kb = KnowledgeBase(knowledge: Nat.relationAxioms)
+    var query: Term
+
+    query = Nat.smallerOrEqual(Nat.from(2), Nat.from(2))  // 2 <= 2
+    XCTAssertEqual(Array(kb.ask(query)).count, 1)
+    query = Nat.smallerOrEqual(Nat.from(5), Nat.from(2))  // 5 <= 2
+    XCTAssert(Array(kb.ask(query)).isEmpty)
+    query = Nat.smallerOrEqual(Nat.from(2), Nat.from(5))  // 2 <= 5
+    XCTAssertEqual(Array(kb.ask(query)).count, 1)
+  }
+
+  func testAdd() {
+    let kb = KnowledgeBase(knowledge: Nat.arithmeticAxioms)
+    let res = Term.var("?")
+
+    var query: Term
+    var binding: BindingMap?
+
+    query = Nat.add(Nat.from(2), Nat.from(5), res)  // 2 + 5 = ?
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding!["?"], Nat.from(7))
+
+    query = Nat.add(Nat.from(2), res, Nat.from(7))  // 2 + ? = 7
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(5))
+
+    query = Nat.add(res, Nat.from(5), Nat.from(7))  // ? + 5 = 7
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(2))
+  }
+
+  func testSub() {
+    let kb = KnowledgeBase(knowledge: Nat.arithmeticAxioms)
+    let res = Term.var("?")
+
+    var query: Term
+    var binding: BindingMap?
+
+    query = Nat.sub(Nat.from(2), Nat.from(5), res)  // 2 - 5 = ?
+    binding = kb.ask(query).next()
+    XCTAssertNil(binding)
+
+    query = Nat.sub(Nat.from(5), Nat.from(2), res)  // 5 - 2 = ?
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(3))
+
+    query = Nat.sub(Nat.from(5), res, Nat.from(3))  // 5 - ? = 3
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(2))
+
+    query = Nat.sub(res, Nat.from(2), Nat.from(3))  // ? - 2 = 3
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(5))
+  }
+
+  func testMul() {
+    let kb = KnowledgeBase(knowledge: Nat.arithmeticAxioms)
+    let res = Term.var("?")
+
+    var query: Term
+    var binding: BindingMap?
+
+    query = Nat.mul(Nat.from(5), Nat.from(2), res)  // 5 * 2 = ?
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(10))
+
+    query = Nat.mul(Nat.from(5), res, Nat.from(10))  // 5 * ? = 10
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(2))
+
+    query = Nat.mul(res, Nat.from(2), Nat.from(10))  // ? * 2 = 10
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(5))
+  }
+
+  func testDiv() {
+    let kb = KnowledgeBase(knowledge: Nat.arithmeticAxioms)
+    let res = Term.var("?")
+
+    var query: Term
+    var binding: BindingMap?
+
+    query = Nat.div(Nat.from(2), Nat.from(0), res)  // 2 / 0 = ?
+    binding = kb.ask(query).next()
+    XCTAssertNil(binding)
+
+    query = Nat.div(Nat.from(2), Nat.from(6), res)  // 2 / 6 = ?
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.zero)
+
+    query = Nat.div(Nat.from(6), Nat.from(2), res)  // 6 / 2 = ?
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(3))
+
+    query = Nat.div(Nat.from(6), res, Nat.from(3))  // 6 / ? = 3
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(2))
+
+     query = Nat.div(res, Nat.from(2), Nat.from(3))  // ? / 2 = 3
+     binding = kb.ask(query).next()
+     XCTAssertNotNil(binding)
+     XCTAssertEqual(binding?["?"], Nat.from(6))
+
+     query = Nat.div(res, Nat.from(3), Nat.from(2))  // ? / 3 = 2
+     binding = kb.ask(query).next()
+     XCTAssertNotNil(binding)
+     XCTAssertEqual(binding?["?"], Nat.from(6))
+  }
+
+  func testMod() {
+    let kb = KnowledgeBase(knowledge: Nat.arithmeticAxioms)
+    let res = Term.var("?")
+
+    var query: Term
+    var binding: BindingMap?
+
+    query = Nat.mod(Nat.from(2), Nat.from(0), res)  // 2 % 0 = ?
+    binding = kb.ask(query).next()
+    XCTAssertNil(binding)
+
+    query = Nat.mod(Nat.from(2), Nat.from(6), res)  // 2 % 6 = ?
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(2))
+
+    query = Nat.mod(Nat.from(6), Nat.from(2), res)  // 6 % 2 = ?
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.zero)
+
+    query = Nat.mod(Nat.from(6), Nat.from(4), res)  // 6 % 4 = ?
+    binding = kb.ask(query).next()
+    XCTAssertNotNil(binding)
+    XCTAssertEqual(binding?["?"], Nat.from(2))
+  }
+
+  func testAsSwiftInt() {
+    XCTAssertEqual(Nat.asSwiftInt(Nat.from(5)), 5)
+    XCTAssertNil(Nat.asSwiftInt(Nat.succ(.var("?"))))
+  }
+
+}

From 944ea444ea5abe0e68dbb2bdd4d0c6783f2b7aa6 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 00:56:56 +0100
Subject: [PATCH 20/32] Avoid creating unnecessary realizer alternators

---
 Sources/LogicKit/Realizer.swift | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index 0333d01..d76f597 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -155,13 +155,18 @@ final class Realizer: RealizerBase {
           // to `0` before we try satisfy `p($x, q(0))`. But if `$x` wasn't renamed,
           // we'd be trying to unify `$x` with `q($x)` while recursing.
 
-          subRealizer = RealizerAlternator(realizers: ruleGoals.map({
+          let subRealizers = ruleGoals.map {
             Realizer(
               goals: $0,
               knowledge: knowledge.refreshed,
               parentBindings: nodeResult,
               logger: logger)
-          }))
+          }
+          assert(!subRealizers.isEmpty)
+          subRealizer = subRealizers.count > 1
+            ? RealizerAlternator(realizers: subRealizers)
+            : subRealizers[0]
+
           if let branchResult = subRealizer!.next() {
             return nodeResult
               .merged(with: branchResult)

From b5a38567f2286e6c5c213b6249340fb372ec78bc Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 01:08:15 +0100
Subject: [PATCH 21/32] Add a coverage test for realizer alternators

---
 Tests/LogicKitTests/LogicKitTests.swift | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/Tests/LogicKitTests/LogicKitTests.swift b/Tests/LogicKitTests/LogicKitTests.swift
index e9f4fb4..4b4a112 100644
--- a/Tests/LogicKitTests/LogicKitTests.swift
+++ b/Tests/LogicKitTests/LogicKitTests.swift
@@ -57,6 +57,24 @@ class LogicKitTests: XCTestCase {
     XCTAssertEqual(answers1[0]   , ["who": .lit("mia")])
   }
 
+  func testDisjunction() {
+    let x: Term = .var("x")
+    let kb: KnowledgeBase = [
+      .fact("hot", .lit("fire")),
+      .fact("cold", .lit("ice")),
+      .rule("painful", x) {
+        .fact("hot", x) || .fact("cold", x)
+      },
+    ]
+
+    let answers = Array(kb.ask(.fact("painful", x)))
+    XCTAssertEqual(answers.count, 2)
+
+    let results = Set(answers.compactMap({ $0["x"] }))
+    XCTAssert(results.contains("fire"))
+    XCTAssert(results.contains("ice"))
+  }
+
   func testRecursion() {
     let x   : Term = .var("x")
     let y   : Term = .var("y")

From ce1740fdd9f76733b00ba62a6b9f84e9b6a93582 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 13:09:21 +0100
Subject: [PATCH 22/32] Simplify the EDSL

---
 Sources/LogicKit/Term.swift             | 15 ---------------
 Tests/LogicKitTests/LogicKitTests.swift | 18 +++++++-----------
 2 files changed, 7 insertions(+), 26 deletions(-)

diff --git a/Sources/LogicKit/Term.swift b/Sources/LogicKit/Term.swift
index 0e63c78..13b53ed 100644
--- a/Sources/LogicKit/Term.swift
+++ b/Sources/LogicKit/Term.swift
@@ -97,31 +97,16 @@ public enum Term {
     return ._rule(name: name, arguments: arguments, body: lhs)
   }
 
-  public static func =>(lhs: () -> Term, rhs: Term) -> Term {
-    guard case let ._term(name: name, arguments: arguments) = rhs else { fatalError() }
-    return ._rule(name: name, arguments: arguments, body: lhs())
-  }
-
   public static func |-(lhs: Term, rhs: Term) -> Term {
     guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
     return ._rule(name: name, arguments: arguments, body: rhs)
   }
 
-  public static func |-(lhs: Term, rhs: () -> Term) -> Term {
-    guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
-    return ._rule(name: name, arguments: arguments, body: rhs())
-  }
-
   public static func ⊢(lhs: Term, rhs: Term) -> Term {
     guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
     return ._rule(name: name, arguments: arguments, body: rhs)
   }
 
-  public static func ⊢(lhs: Term, rhs: () -> Term) -> Term {
-    guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
-    return ._rule(name: name, arguments: arguments, body: rhs())
-  }
-
   /////
 
   public static func &&(lhs: Term, rhs: Term) -> Term {
diff --git a/Tests/LogicKitTests/LogicKitTests.swift b/Tests/LogicKitTests/LogicKitTests.swift
index 4b4a112..fc2d777 100644
--- a/Tests/LogicKitTests/LogicKitTests.swift
+++ b/Tests/LogicKitTests/LogicKitTests.swift
@@ -146,7 +146,7 @@ class LogicKitTests: XCTestCase {
     let who   = Term.var("who")
     let kb: KnowledgeBase = [
       play[mia],
-      { play[mia] && play[mia] } => happy[mia],
+      (play[mia] && play[mia]) => happy[mia],
     ]
 
     let answers0 = Array(kb.ask(happy[mia]))
@@ -160,23 +160,19 @@ class LogicKitTests: XCTestCase {
     XCTAssertEqual(answers1[0][who]  , mia)
 
     XCTAssertEqual(
-      { play[mia] && play[mia] } => happy[mia],
-      (play[mia] && play[mia]) => happy[mia]
-    )
-    XCTAssertEqual(
-      { play[mia] && play[mia] } => happy[mia],
-      happy[mia] |- { play[mia] && play[mia] }
+      (play[mia] && play[mia]) => happy[mia],
+      happy[mia] |- (play[mia] && play[mia])
     )
     XCTAssertEqual(
-      { play[mia] && play[mia] } => happy[mia],
+      (play[mia] && play[mia]) => happy[mia],
       happy[mia] |- (play[mia] && play[mia])
     )
     XCTAssertEqual(
-      { play[mia] && play[mia] } => happy[mia],
-      happy[mia] ⊢ { play[mia] ∧ play[mia] }
+      (play[mia] && play[mia]) => happy[mia],
+      happy[mia] ⊢ (play[mia] ∧ play[mia])
     )
     XCTAssertEqual(
-      { play[mia] && play[mia] } => happy[mia],
+      (play[mia] && play[mia]) => happy[mia],
       happy[mia] ⊢ (play[mia] ∧ play[mia])
     )
   }

From 722913046da35124dc3845a0725e3625741ab915 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 13:56:43 +0100
Subject: [PATCH 23/32] Map string literals to terms of arity 0 rather than
 literal values.

---
 Sources/LogicKit/Term.swift             |  6 +++---
 Tests/LogicKitTests/LogicKitTests.swift | 16 ++++++++--------
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/Sources/LogicKit/Term.swift b/Sources/LogicKit/Term.swift
index 13b53ed..c94a646 100644
--- a/Sources/LogicKit/Term.swift
+++ b/Sources/LogicKit/Term.swift
@@ -75,8 +75,8 @@ public enum Term {
   }
 
   public subscript(terms: Term...) -> Term {
-    guard case let .val(val) = self else { fatalError() }
-    guard let name = val as? String else { fatalError() }
+    guard case ._term(let name, let subterms) = self, subterms.isEmpty
+      else { fatalError("\(self) cannot be coerced into a functor") }
     return ._term(name: name, arguments: terms)
   }
 
@@ -166,6 +166,6 @@ extension Term: CustomStringConvertible {
 
 extension Term : ExpressibleByStringLiteral {
   public init(stringLiteral : String) {
-    self = .lit(stringLiteral)
+    self = .fact(stringLiteral)
   }
 }
diff --git a/Tests/LogicKitTests/LogicKitTests.swift b/Tests/LogicKitTests/LogicKitTests.swift
index fc2d777..06fc318 100644
--- a/Tests/LogicKitTests/LogicKitTests.swift
+++ b/Tests/LogicKitTests/LogicKitTests.swift
@@ -42,26 +42,26 @@ class LogicKitTests: XCTestCase {
 
   func testSimpleDeductions() {
     let kb: KnowledgeBase = [
-      .fact("play" , .lit("mia")),
-      .rule("happy", .lit("mia")) {
-        .fact("play", .lit("mia"))
+      .fact("play" , "mia"),
+      .rule("happy", "mia") {
+        .fact("play", "mia")
       },
     ]
 
-    let answers0 = Array(kb.ask(.fact("happy", .lit("mia"))))
+    let answers0 = Array(kb.ask(.fact("happy", "mia")))
     XCTAssertEqual(answers0.count, 1)
     XCTAssertEqual(answers0[0]   , [:])
 
     let answers1 = Array(kb.ask(.fact("happy", .var("who"))))
     XCTAssertEqual(answers1.count, 1)
-    XCTAssertEqual(answers1[0]   , ["who": .lit("mia")])
+    XCTAssertEqual(answers1[0]   , ["who": "mia"])
   }
 
   func testDisjunction() {
     let x: Term = .var("x")
     let kb: KnowledgeBase = [
-      .fact("hot", .lit("fire")),
-      .fact("cold", .lit("ice")),
+      .fact("hot", "fire"),
+      .fact("cold", "ice"),
       .rule("painful", x) {
         .fact("hot", x) || .fact("cold", x)
       },
@@ -79,7 +79,7 @@ class LogicKitTests: XCTestCase {
     let x   : Term = .var("x")
     let y   : Term = .var("y")
     let z   : Term = .var("z")
-    let zero: Term = .lit("zero")
+    let zero: Term = "zero"
 
     func succ(_ x: Term) -> Term {
       return .fact("succ", x)

From 9a84bc0f3eb3465984fbcada2839f8a7967b0e2d Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 16:11:22 +0100
Subject: [PATCH 24/32] Optimize the knowledge base representation

---
 Sources/LogicKit/KnowledgeBase.swift       | 98 ++++++++++++++--------
 Sources/LogicKit/Realizer.swift            | 53 ++++++------
 Sources/LogicKit/Sequence+Extensions.swift | 31 +++++++
 Sources/LogicKit/Term.swift                | 32 +++++--
 4 files changed, 150 insertions(+), 64 deletions(-)
 create mode 100644 Sources/LogicKit/Sequence+Extensions.swift

diff --git a/Sources/LogicKit/KnowledgeBase.swift b/Sources/LogicKit/KnowledgeBase.swift
index 53bd7fb..922501b 100644
--- a/Sources/LogicKit/KnowledgeBase.swift
+++ b/Sources/LogicKit/KnowledgeBase.swift
@@ -1,9 +1,49 @@
-public struct KnowledgeBase {
+public struct KnowledgeBase: Hashable {
+
+  public init(predicates: [String: [Term]], literals: Set<Term>) {
+    let terms = predicates.values.joined().concatenated(with: literals)
+    for term in terms {
+      switch term {
+      case ._term, ._rule:
+        continue
+      default:
+        fatalError("Cannot use '\(term)' as a predicate.")
+      }
+    }
+
+    self.predicates = predicates
+    self.literals = literals
+  }
 
   public init(knowledge: [Term]) {
-    self.knowledge = knowledge
+    /// Extract predicates and literals from the given list of terms.
+    for term in knowledge {
+      switch term {
+      case ._term(let name, _):
+        let group = predicates[name] ?? []
+        predicates[name] = group + [term]
+
+      case ._rule(let name, _, _):
+        let group = predicates[name] ?? []
+        predicates[name] = group + [term]
+
+      case .val:
+        literals.insert(term)
+
+      case .var, .conjunction, .disjunction:
+        fatalError("Cannot use '\(term)' as a predicate.")
+      }
+    }
   }
 
+  /// The list of predicates in the knowledge base, grouped by functor.
+  public private(set) var predicates: [String: [Term]] = [:]
+  /// The list of isolated literals in the knowledge base.
+  public private(set) var literals: Set<Term> = []
+
+  /// The number of predicates and literals in the knowledge base.
+  public var count: Int { return predicates.values.reduce(0, { $0 + $1.count }) + literals.count }
+
   public func ask(_ query: Term, logger: Logger? = nil) -> AnswerSet {
     switch query {
     case .var, ._rule:
@@ -12,7 +52,7 @@ public struct KnowledgeBase {
     default:
       // Build an array of realizers for each conjunction of goals in the query.
       let realizers = query.goals.map {
-        Realizer(goals: $0, knowledge: refreshed, logger: logger)
+        Realizer(goals: $0, knowledge: renaming(query.variables), logger: logger)
       }
 
       // Return the goal realizer(s).
@@ -24,18 +64,13 @@ public struct KnowledgeBase {
     }
   }
 
-  public func union(with other: KnowledgeBase) -> KnowledgeBase {
-    var newClauses = self.knowledge
-    for clause in other.knowledge {
-      if !newClauses.contains(clause) {
-        newClauses.append(clause)
-      }
+  func renaming(_ variables: Set<String>) -> KnowledgeBase {
+    var result = KnowledgeBase(knowledge: [])
+    for (name, terms) in predicates {
+      result.predicates[name] = terms.map { $0.renaming(variables) }
     }
-    return KnowledgeBase(knowledge: newClauses)
-  }
-
-  var refreshed: KnowledgeBase {
-    return KnowledgeBase(knowledge: knowledge.map(renameVariables))
+    result.literals = literals
+    return result
   }
 
   func renameVariables(of term: Term) -> Term {
@@ -58,31 +93,26 @@ public struct KnowledgeBase {
     }
   }
 
-  public let knowledge: [Term]
-
-}
+  public static func + (lhs: KnowledgeBase, rhs: KnowledgeBase) -> KnowledgeBase {
+    var result = KnowledgeBase(knowledge: [])
+    for (name, terms) in lhs.predicates {
+      result.predicates[name] = terms
+      if let right = rhs.predicates[name] {
+        result.predicates[name]!.append(contentsOf: right)
+      }
+    }
+    result.literals = lhs.literals.union(rhs.literals)
+    return result
+  }
 
-extension KnowledgeBase: Hashable {
 }
 
-extension KnowledgeBase: Collection {
+extension KnowledgeBase: Sequence {
 
   public typealias Element = Term
 
-  public var startIndex: Int {
-    return knowledge.startIndex
-  }
-
-  public var endIndex: Int {
-    return knowledge.endIndex
-  }
-
-  public func index(after i: Int) -> Int {
-    return knowledge.index(after: i)
-  }
-
-  public subscript(position: Int) -> Term {
-    return knowledge[position]
+  public func makeIterator() -> AnyIterator<Element> {
+    return predicates.values.joined().concatenated(with: literals).makeIterator()
   }
 
 }
@@ -98,7 +128,7 @@ extension KnowledgeBase: ExpressibleByArrayLiteral {
 extension KnowledgeBase: CustomStringConvertible {
 
   public var description: String {
-    return knowledge.description
+    return "[" + self.map({ "\($0)" }).joined(separator: ", ") + "]"
   }
 
 }
diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index d76f597..621ca5f 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -51,6 +51,17 @@ final class Realizer: RealizerBase {
     self.knowledge = knowledge
     self.parentBindings = parentBindings
     self.logger = logger
+
+    // Identify which part of the knowledge base the realizer should explore.
+    assert(goals.count > 0)
+    switch goals.first! {
+    case ._term(let name, _):
+      clauseIterator = knowledge.predicates[name].map { AnyIterator($0.makeIterator()) }
+    case ._rule(let name, _, _):
+      clauseIterator = knowledge.predicates[name].map { AnyIterator($0.makeIterator()) }
+    default:
+      clauseIterator = AnyIterator(knowledge.literals.makeIterator())
+    }
   }
 
   /// The goals to realize.
@@ -62,8 +73,8 @@ final class Realizer: RealizerBase {
   /// The optional logger, for debug purpose.
   private var logger: Logger?
 
-  /// The index of the next clause to check.
-  private var clauseIndex = 0
+  /// An iterator on the knowledge clauses to check.
+  private var clauseIterator: AnyIterator<Term>?
   /// The subrealizer, if any.
   private var subRealizer: RealizerBase? = nil
 
@@ -103,10 +114,7 @@ final class Realizer: RealizerBase {
     }
 
     // Look for the next root clause.
-    while clauseIndex != knowledge.endIndex {
-      let clause = knowledge[clauseIndex]
-      clauseIndex += 1
-
+    while let clause = clauseIterator?.next() {
       logger?.log(message: "using "    , terminator: "", fontAttributes: [.dim])
       logger?.log(message: "\(clause) ")
 
@@ -137,39 +145,36 @@ final class Realizer: RealizerBase {
           }
         }
 
-      case let (._term(goalName, _), ._rule(ruleName, ruleArguments, ruleBody))
-        where goalName == ruleName:
+      case let (._term(goalName, _), ._rule(ruleName, ruleArguments, ruleBody)):
+        assert(goalName == ruleName)
 
         // First we try to unify the rule head with the goal.
         let head: Term = ._term(name: goalName, arguments: ruleArguments)
         if let nodeResult = unify(goal: goal, fact: head) {
-          let subGoals  = goals.dropFirst()
+          let subGoals = goals.dropFirst()
             .map(nodeResult.deepWalk)
           let ruleGoals = ruleBody.goals
             .map({ $0.map(nodeResult.deepWalk) + subGoals })
-
-          // Note that we have to make sure all variables of the sub-realizer's knowldge
-          // are fresh, otherwise they may collide with the ones we already bound. For
-          // instance, consider a recursive rule `p(q($x), $y) ⊢ p($x, q($y))` and a
-          // goal `p($z, 0)`. In this example, `$z` would get bound to `q($x)` and `$y`
-          // to `0` before we try satisfy `p($x, q(0))`. But if `$x` wasn't renamed,
-          // we'd be trying to unify `$x` with `q($x)` while recursing.
-
+          assert(!ruleGoals.isEmpty)
+
+          // We have to make sure bound knowledge variables are renamed in the sub-realizer's
+          // knowledge, otherwise they may collide with the ones we already bound. For instance,
+          // consider a recursive rule `p(q($x), $y) ⊢ p($x, q($y))` and a goal `p($z, 0)`. `$z`
+          // would get bound to `q($x)` and `$y` to `0` before we try satisfy `p($x, q(0))`. But
+          // if `$x` wasn't renamed, we'd be trying to unify `$x` with `q($x)` while recursing.
+          let subKnowledge = knowledge.renaming(Set(clause.variables))
           let subRealizers = ruleGoals.map {
             Realizer(
-              goals: $0,
-              knowledge: knowledge.refreshed,
-              parentBindings: nodeResult,
-              logger: logger)
+              goals: $0, knowledge: subKnowledge, parentBindings: nodeResult, logger: logger)
           }
-          assert(!subRealizers.isEmpty)
           subRealizer = subRealizers.count > 1
             ? RealizerAlternator(realizers: subRealizers)
             : subRealizers[0]
 
           if let branchResult = subRealizer!.next() {
-            return nodeResult
-              .merged(with: branchResult)
+            // Note the `branchResult` already contains the bindings of `nodeResult`, as the these
+            // will have been merged by sub-realizer.
+            return branchResult
               .merged(with: parentBindings)
           }
         }
diff --git a/Sources/LogicKit/Sequence+Extensions.swift b/Sources/LogicKit/Sequence+Extensions.swift
new file mode 100644
index 0000000..78b70ea
--- /dev/null
+++ b/Sources/LogicKit/Sequence+Extensions.swift
@@ -0,0 +1,31 @@
+extension Sequence {
+
+  func concatenated<S>(with other: S) -> SequenceConcatenation<Self, S>
+    where S: Sequence, S.Element == Element
+  {
+    return SequenceConcatenation(self, other)
+  }
+
+}
+
+struct SequenceConcatenation<S1, S2>: Sequence
+  where S1: Sequence, S2: Sequence, S1.Element == S2.Element
+{
+
+  init(_ first: S1, _ second: S2) {
+    self.first = first
+    self.second = second
+  }
+
+  func makeIterator() -> AnyIterator<S1.Element> {
+    var iter1 = first.makeIterator()
+    var iter2 = second.makeIterator()
+    return AnyIterator {
+      return iter1.next() ?? iter2.next()
+    }
+  }
+
+  private let first: S1
+  private let second: S2
+
+}
diff --git a/Sources/LogicKit/Term.swift b/Sources/LogicKit/Term.swift
index c94a646..b9fe264 100644
--- a/Sources/LogicKit/Term.swift
+++ b/Sources/LogicKit/Term.swift
@@ -42,17 +42,37 @@ public enum Term {
     switch self {
     case .var(let x):
       return [x]
-    case ._term(name: _, arguments: let subterms):
-      return subterms.map({ $0.variables }).reduce(Set<String>(), { $0.union($1) })
-    case ._rule(name: _, arguments: let subterms, body: let body):
-      let subtermVariables = subterms.map({ $0.variables }).reduce(Set<String>(), { $0.union($1) })
+    case .val:
+      return []
+    case ._term(_, let args):
+      return args.map({ $0.variables }).reduce(Set<String>(), { $0.union($1) })
+    case ._rule(_, let args, let body):
+      let subtermVariables = args.map({ $0.variables }).reduce(Set<String>(), { $0.union($1) })
       return body.variables.union(subtermVariables)
     case .conjunction(let lhs, let rhs):
       return lhs.variables.union(rhs.variables)
     case .disjunction(let lhs, let rhs):
       return lhs.variables.union(rhs.variables)
-    default:
-      return []
+    }
+  }
+
+  func renaming(_ variables: Set<String>) -> Term {
+    switch self {
+    case .var(let x) where variables.contains(x):
+      return .var(x + "'")
+    case .var, .val:
+      return self
+    case ._term(let name, let args):
+      return ._term(name: name, arguments: args.map({ $0.renaming(variables) }))
+    case ._rule(let name, let args, let body):
+      return ._rule(
+        name: name,
+        arguments: args.map({ $0.renaming(variables) }),
+        body: body.renaming(variables))
+    case .conjunction(let lhs, let rhs):
+      return .conjunction(lhs.renaming(variables), rhs.renaming(variables))
+    case .disjunction(let lhs, let rhs):
+      return .disjunction(lhs.renaming(variables), rhs.renaming(variables))
     }
   }
 

From e9d461f6c6697521739100cbb592d7ec096f7e28 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 16:23:09 +0100
Subject: [PATCH 25/32] Variable name and code style consistency

---
 Sources/LogicKit/BindingMap.swift    |  4 +--
 Sources/LogicKit/KnowledgeBase.swift | 10 +++----
 Sources/LogicKit/Realizer.swift      |  6 ++--
 Sources/LogicKit/Term.swift          | 45 +++++++++++++++-------------
 4 files changed, 34 insertions(+), 31 deletions(-)

diff --git a/Sources/LogicKit/BindingMap.swift b/Sources/LogicKit/BindingMap.swift
index 6cab79d..4f2e2c5 100644
--- a/Sources/LogicKit/BindingMap.swift
+++ b/Sources/LogicKit/BindingMap.swift
@@ -22,8 +22,8 @@ extension Dictionary where Key == String, Value == Term {
   func deepWalk(_ term: Term) -> Term {
     let walked = shallowWalk(term)
     switch walked {
-    case ._term(name: let name, arguments: let arguments):
-      return ._term(name: name, arguments: arguments.map(deepWalk))
+    case ._term(let name, let args):
+      return ._term(name: name, arguments: args.map(deepWalk))
     case .conjunction(let lhs, let rhs):
       return .conjunction(deepWalk(lhs), deepWalk(rhs))
     case .disjunction(let lhs, let rhs):
diff --git a/Sources/LogicKit/KnowledgeBase.swift b/Sources/LogicKit/KnowledgeBase.swift
index 922501b..76656a7 100644
--- a/Sources/LogicKit/KnowledgeBase.swift
+++ b/Sources/LogicKit/KnowledgeBase.swift
@@ -47,7 +47,7 @@ public struct KnowledgeBase: Hashable {
   public func ask(_ query: Term, logger: Logger? = nil) -> AnswerSet {
     switch query {
     case .var, ._rule:
-      preconditionFailure("invalid query")
+      fatalError("invalid query")
 
     default:
       // Build an array of realizers for each conjunction of goals in the query.
@@ -77,12 +77,12 @@ public struct KnowledgeBase: Hashable {
     switch term {
     case .var(let name):
       return .var(name + "'")
-    case ._term(let name, let arguments):
-      return ._term(name: name, arguments: arguments.map(renameVariables))
-    case ._rule(let name, let arguments, let body):
+    case ._term(let name, let args):
+      return ._term(name: name, arguments: args.map(renameVariables))
+    case ._rule(let name, let args, let body):
       return ._rule(
         name: name,
-        arguments: arguments.map(renameVariables),
+        arguments: args.map(renameVariables),
         body: renameVariables(of: body))
     case .conjunction(let lhs, let rhs):
       return .conjunction(renameVariables(of: lhs), renameVariables(of: rhs))
diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index 621ca5f..939464c 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -92,7 +92,7 @@ final class Realizer: RealizerBase {
 
     let goal = goals.first!
     logger?.log(message: "Attempting to realize ", terminator: "")
-    logger?.log(message: goal.description, fontAttributes: [.bold])
+    logger?.log(message: "\(goal)", fontAttributes: [.bold])
 
     // Check for the built-in `~=~/2` predicate.
     if case ._term("lk.~=~", let args) = goal {
@@ -145,11 +145,11 @@ final class Realizer: RealizerBase {
           }
         }
 
-      case let (._term(goalName, _), ._rule(ruleName, ruleArguments, ruleBody)):
+      case let (._term(goalName, _), ._rule(ruleName, ruleArgs, ruleBody)):
         assert(goalName == ruleName)
 
         // First we try to unify the rule head with the goal.
-        let head: Term = ._term(name: goalName, arguments: ruleArguments)
+        let head: Term = ._term(name: goalName, arguments: ruleArgs)
         if let nodeResult = unify(goal: goal, fact: head) {
           let subGoals = goals.dropFirst()
             .map(nodeResult.deepWalk)
diff --git a/Sources/LogicKit/Term.swift b/Sources/LogicKit/Term.swift
index b9fe264..b361c97 100644
--- a/Sources/LogicKit/Term.swift
+++ b/Sources/LogicKit/Term.swift
@@ -85,7 +85,7 @@ public enum Term {
   /////
 
   public static func fact(_ name: Term, _ arguments: Term...) -> Term {
-    guard case let .val(val) = name else { fatalError() }
+    guard case .val(let val) = name else { fatalError() }
     guard let name = val as? String else { fatalError() }
     return ._term(name: name, arguments: arguments)
   }
@@ -96,14 +96,14 @@ public enum Term {
 
   public subscript(terms: Term...) -> Term {
     guard case ._term(let name, let subterms) = self, subterms.isEmpty
-      else { fatalError("\(self) cannot be coerced into a functor") }
+      else { fatalError("Cannot coerce '\(self)' into a functor") }
     return ._term(name: name, arguments: terms)
   }
 
   /////
 
   public static func rule(_ name: Term, _ arguments: Term..., body: () -> Term) -> Term {
-    guard case let .val(val) = name else { fatalError() }
+    guard case .val(let val) = name else { fatalError() }
     guard let name = val as? String else { fatalError() }
     return ._rule(name: name, arguments: arguments, body: body())
   }
@@ -113,18 +113,21 @@ public enum Term {
   }
 
   public static func =>(lhs: Term, rhs: Term) -> Term {
-    guard case let ._term(name: name, arguments: arguments) = rhs else { fatalError() }
-    return ._rule(name: name, arguments: arguments, body: lhs)
+    guard case ._term(let name, let args) = rhs
+      else { fatalError("Cannot use '\(self)' as a rule head.") }
+    return ._rule(name: name, arguments: args, body: lhs)
   }
 
   public static func |-(lhs: Term, rhs: Term) -> Term {
-    guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
-    return ._rule(name: name, arguments: arguments, body: rhs)
+    guard case ._term(let name, let args) = lhs
+      else { fatalError("Cannot use '\(self)' as a rule head.") }
+    return ._rule(name: name, arguments: args, body: rhs)
   }
 
   public static func ⊢(lhs: Term, rhs: Term) -> Term {
-    guard case let ._term(name: name, arguments: arguments) = lhs else { fatalError() }
-    return ._rule(name: name, arguments: arguments, body: rhs)
+    guard case ._term(let name, let args) = lhs
+      else { fatalError("Cannot use '\(self)' as a rule head.") }
+    return ._rule(name: name, arguments: args, body: rhs)
   }
 
   /////
@@ -162,22 +165,22 @@ extension Term: CustomStringConvertible {
 
   public var description: String {
     switch self {
-    case let .var(name):
+    case .var(let name):
       return "$\(name)"
-    case let .val(value):
+    case .val(let value):
       return "\(value)"
-    case let ._term(name, arguments):
-      return arguments.isEmpty
-        ? name.description
-        : "\(name)[\(arguments.map({ $0.description }).joined(separator: ", "))]"
-    case let ._rule(name, arguments, body):
-      let head = arguments.isEmpty
-        ? name.description
-        : "\(name)[\(arguments.map({ $0.description }).joined(separator: ", "))]"
+    case ._term(let name, let args):
+      return args.isEmpty
+        ? "\(name)"
+        : "\(name)[\(args.map({ "\($0)" }).joined(separator: ", "))]"
+    case ._rule(let name, let args, let body):
+      let head = args.isEmpty
+        ? "\(name)"
+        : "\(name)[\(args.map({ "\($0)" }).joined(separator: ", "))]"
       return "(\(head) ⊢ \(body))"
-    case let .conjunction(lhs, rhs):
+    case .conjunction(let lhs, let rhs):
       return "(\(lhs) ∧ \(rhs))"
-    case let .disjunction(lhs, rhs):
+    case .disjunction(let lhs, let rhs):
       return "(\(lhs) ∨ \(rhs))"
     }
   }

From b5d5d6da2e63c39e7a19347f04d8ded634dcab96 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 16:26:06 +0100
Subject: [PATCH 26/32] Minor fix on the EDSL

---
 Sources/LogicKit/Term.swift | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/Sources/LogicKit/Term.swift b/Sources/LogicKit/Term.swift
index b361c97..0fb866a 100644
--- a/Sources/LogicKit/Term.swift
+++ b/Sources/LogicKit/Term.swift
@@ -84,12 +84,6 @@ public enum Term {
 
   /////
 
-  public static func fact(_ name: Term, _ arguments: Term...) -> Term {
-    guard case .val(let val) = name else { fatalError() }
-    guard let name = val as? String else { fatalError() }
-    return ._term(name: name, arguments: arguments)
-  }
-
   public static func fact(_ name: String, _ arguments: Term...) -> Term {
     return ._term(name: name, arguments: arguments)
   }
@@ -102,12 +96,6 @@ public enum Term {
 
   /////
 
-  public static func rule(_ name: Term, _ arguments: Term..., body: () -> Term) -> Term {
-    guard case .val(let val) = name else { fatalError() }
-    guard let name = val as? String else { fatalError() }
-    return ._rule(name: name, arguments: arguments, body: body())
-  }
-
   public static func rule(_ name: String, _ arguments: Term..., body: () -> Term) -> Term {
     return ._rule(name: name, arguments: arguments, body: body())
   }

From db47b4e70d281255d39269dba22b2a9488958914 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 19:22:23 +0100
Subject: [PATCH 27/32] Refactor the Logger protocol

---
 Sources/LogicKit/Logger.swift   | 44 +++++++++++++++++++++------------
 Sources/LogicKit/Realizer.swift |  8 +++---
 2 files changed, 31 insertions(+), 21 deletions(-)

diff --git a/Sources/LogicKit/Logger.swift b/Sources/LogicKit/Logger.swift
index cbf551f..3aa1380 100644
--- a/Sources/LogicKit/Logger.swift
+++ b/Sources/LogicKit/Logger.swift
@@ -15,33 +15,33 @@ public enum FontAttribute {
 
 public protocol Logger {
 
-  func log(message: String, terminator: String, fontAttributes: [FontAttribute])
+  func didBacktrack()
+  func willRealize(goal: Term)
+  func willAttempt(clause: Term)
 
 }
 
-extension Logger {
+public struct DefaultLogger: Logger {
 
-  public func log(message: String) {
-    log(message: message, terminator: "\n", fontAttributes: [])
+  public init(useFontAttributes: Bool = true) {
+    self.useFontAttributes = useFontAttributes
   }
 
-  public func log(message: String, fontAttributes: [FontAttribute]) {
-    log(message: message, terminator: "\n", fontAttributes: fontAttributes)
-  }
+  public let useFontAttributes: Bool
 
-  public func log(message: String, terminator: String) {
-    log(message: message, terminator: terminator, fontAttributes: [])
+  public func didBacktrack() {
+    log(message: "backtacking", fontAttributes: [.dim])
   }
 
-}
-
-public struct DefaultLogger: Logger {
-
-  public init(useFontAttributes: Bool = true) {
-    self.useFontAttributes = useFontAttributes
+  public func willRealize(goal: Term) {
+    log(message: "Attempting to realize ", terminator: "")
+    log(message: "\(goal)", fontAttributes: [.bold])
   }
 
-  public let useFontAttributes: Bool
+  public func willAttempt(clause: Term) {
+    log(message: "using "    , terminator: "", fontAttributes: [.dim])
+    log(message: "\(clause) ")
+  }
 
   public func log(message: String, terminator: String, fontAttributes: [FontAttribute]) {
     if useFontAttributes {
@@ -63,6 +63,18 @@ public struct DefaultLogger: Logger {
     }
   }
 
+  public func log(message: String) {
+    log(message: message, terminator: "\n", fontAttributes: [])
+  }
+
+  public func log(message: String, fontAttributes: [FontAttribute]) {
+    log(message: message, terminator: "\n", fontAttributes: fontAttributes)
+  }
+
+  public func log(message: String, terminator: String) {
+    log(message: message, terminator: terminator, fontAttributes: [])
+  }
+
   static let foreground: [FontColor: String] = [
     .red   : "31m",
     .green : "32m",
diff --git a/Sources/LogicKit/Realizer.swift b/Sources/LogicKit/Realizer.swift
index 939464c..1b64a05 100644
--- a/Sources/LogicKit/Realizer.swift
+++ b/Sources/LogicKit/Realizer.swift
@@ -85,14 +85,13 @@ final class Realizer: RealizerBase {
         return result
           .merged(with: parentBindings)
       } else {
-        logger?.log(message: "backtacking", fontAttributes: [.dim])
+        logger?.didBacktrack()
         subRealizer = nil
       }
     }
 
     let goal = goals.first!
-    logger?.log(message: "Attempting to realize ", terminator: "")
-    logger?.log(message: "\(goal)", fontAttributes: [.bold])
+    logger?.willRealize(goal: goal)
 
     // Check for the built-in `~=~/2` predicate.
     if case ._term("lk.~=~", let args) = goal {
@@ -115,8 +114,7 @@ final class Realizer: RealizerBase {
 
     // Look for the next root clause.
     while let clause = clauseIterator?.next() {
-      logger?.log(message: "using "    , terminator: "", fontAttributes: [.dim])
-      logger?.log(message: "\(clause) ")
+      logger?.willAttempt(clause: clause)
 
       switch (goal, clause) {
       case (.val(let lvalue), .val(let rvalue)) where lvalue == rvalue:

From 5cc25a154ea492391690b591dbb6c1eaf58d0a9d Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 21:22:37 +0100
Subject: [PATCH 28/32] Set the precedence of custom infix operators

---
 Sources/LogicKit/Term.swift | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Sources/LogicKit/Term.swift b/Sources/LogicKit/Term.swift
index 0fb866a..9464c10 100644
--- a/Sources/LogicKit/Term.swift
+++ b/Sources/LogicKit/Term.swift
@@ -1,9 +1,9 @@
 infix operator ~=~: ComparisonPrecedence
-infix operator =>
-infix operator |-
-infix operator ⊢
-infix operator ∧
-infix operator ∨
+infix operator => : AssignmentPrecedence
+infix operator |- : AssignmentPrecedence
+infix operator ⊢  : AssignmentPrecedence
+infix operator ∧  : LogicalConjunctionPrecedence
+infix operator ∨  : LogicalDisjunctionPrecedence
 
 public enum Term {
 

From 354d5c0328730b527d308344c218826b0bfa64da Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 21:23:07 +0100
Subject: [PATCH 29/32] Implement a method to extract the value of a literal

---
 Sources/LogicKit/Term.swift | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Sources/LogicKit/Term.swift b/Sources/LogicKit/Term.swift
index 9464c10..8827443 100644
--- a/Sources/LogicKit/Term.swift
+++ b/Sources/LogicKit/Term.swift
@@ -82,6 +82,12 @@ public enum Term {
     return .val(AnyHashable(value))
   }
 
+  func extractValue<T>(ofType type: T.Type) -> T? {
+    guard case .val(let v) = self
+      else { return nil }
+    return v as? T
+  }
+
   /////
 
   public static func fact(_ name: String, _ arguments: Term...) -> Term {

From 9e06e746c527a5256e6a9f310651c44e931374c2 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 21:23:44 +0100
Subject: [PATCH 30/32] Update the README

---
 README.md | 101 ++++++++++++++++++++++++++++++------------------------
 1 file changed, 57 insertions(+), 44 deletions(-)

diff --git a/README.md b/README.md
index 8ae288d..2e708d7 100644
--- a/README.md
+++ b/README.md
@@ -12,7 +12,7 @@ A program is expressed in terms of relations,
 and computation in terms of queries over these relations.
 The beauty of logic programming is that
 we no longer have to tell a computer *how* to compute a result,
-but only describe the constrains it should respect.
+but only describe the constraints it should respect.
 For instance, the following Prolog snippet finds all the pairs of operands whose sum is 2.
 
 ```prolog
@@ -23,73 +23,79 @@ add(succ(X), Y, Z) :-
 ?- add(X, Y, succ(succ(zero))).
 ```
 
-This is nice and all, but as any other paradigm, logic programming isn't a fit-them-all solution.
-Let's imagine we've to program a complex user interface with a lot of stateful components.
-In fact, algorithms that are easily expressed in an imperative way
+Writing programs this way is arguably quite interesting.
+However, just as any other paradigm, logic programming isn't a fit-them-all solution.
+For instance, algorithms that are easily expressed in an imperative way
 often prove to be difficult to write in a functional logic programming style.
+This is why most modern programming languages, like Swift, are all about miying paradigms.
 
-But modern languages like Swift are all about mixing paradigms right?
 So why not bringing logic programming into the mix as well!
 With LogicKit, the above Prolog example can be rewritten entirely in Swift:
 
 ```swift
-let zero: Term = .lit("zero")
-let x   : Term = .var("x")
-let y   : Term = .var("y")
-let z   : Term = .var("z")
+let zero: Term = "zero"
+let x: Term = .var("x")
+let y: Term = .var("y")
+let z: Term = .var("z")
 
 let kb: KnowledgeBase = [
    .fact("add", zero, y, y),
-   .rule("add", .fact("succ", x), y, z) {
-     .fact("add", x, .fact("succ", y), z)
-   }
+   .fact("add", .fact("succ", x), y, z) |-
+     .fact("add", x, .fact("succ", y), z),
 ]
 
-let answers = kb.ask(.fact("add", x, y, .fact("succ", .fact("succ", zero))))
+var answers = kb.ask(.fact("add", x, y, .fact("succ", .fact("succ", zero))))
+for result in answers.prefix(3) {
+  print(result)
+}
 ```
 
-## Getting started
+## Getting Started
+
+The following is a quick *Getting Started* introduction the installation and use of LogicKit
+that only brushes over the library.
+You may refer want to refer to the *User Manual* for more details.
 
 ### Quick tutorial
 
 Like Prolog, LogicKit revolves around a knowledge base (or database),
 against which one can make queries.
 There are four constructs in LogicKit:
-literals (`Term.lit(_:)`) that denote atomic values,
-facts (`Term.fact(_:_:)`) that denote predicates,
-rules (`Term.rule(_:_:_:)`) that denote conditional facts and
+Facts (`Term.fact(_:_:)`) that denote predicates and propositions,
+rules (`Term.rule(_:_:_:)`) that denote conditional facts,
+literals (`Term.lit(_:)`) that denote atomic values, and
 variables (`Term.var(_:)`) that act as placeholders for other terms.
 
 Knowledge bases are nothing more than a collection of such constructs:
 
 ```swift
 let kb: KnowledgeBase = [
-  .fact("is effective against", .lit("water"), .lit("fire")),
-  .fact("is effective against", .lit("fire") , .lit("grass")),
-  .fact("is effective against", .lit("grass"), .lit("water")),
+  .fact("is effective against", .fact("water"), .fact("fire")),
+  .fact("is effective against", .fact("fire"), .fact("grass")),
+  .fact("is effective against", .fact("grass"), .fact("water")),
 
-  .fact("has type", .lit("Bulbasaur") , .lit("grass")),
-  .fact("has type", .lit("Squirtle")  , .lit("water")),
-  .fact("has type", .lit("Charmander"), .lit("fire")),
+  .fact("has type", .fact("Bulbasaur")), .fact("grass")),
+  .fact("has type", .fact("Squirtle")), .fact("water")),
+  .fact("has type", .fact("Charmander")), .fact("fire")),
 ]
 ```
 
-The above knowledge base only makes use of facts and literals.
+The above knowledge base only makes use of facts and propositions.
 It states for instance that *water is effective against fire*,
 or that *Squirtle has type water*.
 One can query such knowledge base as follows:
 
 ```swift
-var answers = kb.ask(.fact("has type", .lit("Squirtle"), .lit("water")))
+var answers = kb.ask(.fact("has type", .fact("Squirtle"), .fact("water")))
 ```
 
 Since there might be several answers to a single query,
-`Knowledge.ask(_:_:)` doesn't return a single yes/no answer.
+`Knowledge.ask(_:logger:)` doesn't return a single yes/no answer.
 Instead, it returns a sequence whose each element denote one correct answer.
 If the sequence is empty, then there isn't any solution.
 
 ```swift
-print("Squirtle has type water:" answers.next() != nil)
+print("Squirtle has type water:", answers.next() != nil)
 // Prints "Squirtle has type water: true"
 ```
 
@@ -111,20 +117,20 @@ if the type of `x` is effective against that of `y`.
 Now we can ask things like:
 
 ```swift
-let answers = kb.ask(.fact("is stronger", .lit("Charmander"), .lit("Bulbasaur")))
+var answers = kb.ask(.fact("is stronger", .fact("Charmander"), .fact("Bulbasaur")))
 ```
 
 or even more interestingly:
 
 ```swift
-let answers = kb.ask(.fact("is stronger", .var("a"), .var("b")))
+var answers = kb.ask(.fact("is stronger", .var("a"), .var("b")))
 ```
 
 Note that because the query involves variables,
 not only are we interested to know if it is satisfiable,
 but also for what binding of `a` and `b`.
-Well, in fact each element of the sequence returned by `Knowledge.ask(_:_:)`
-denotes such a binding:
+Well, in fact each element of the sequence returned by `Knowledge.ask(_:logger:)`
+denotes such binding:
 
 ```swift
 for binding in answers {
@@ -141,9 +147,9 @@ Note that since LogicKit is an EDSL,
 nothing prevents us from using the full power of Swift to make our definitions more readable:
 
 ```swift
-let bulbasaur : Term = .lit("Bulbasaur")
-let squirtle  : Term = .lit("Squirtle")
-let charmander: Term = .lit("Charmander")
+let bulbasaur: Term = "Bulbasaur"
+let squirtle: Term = "Squirtle"
+let charmander: Term = "Charmander"
 
 infix operator !>
 func !>(lhs: Term, rhs: Term) -> Term {
@@ -156,12 +162,15 @@ let kb: KnowledgeBase = [
   charmander !> bulbasaur,
 ]
 
-let answer = kb.ask(bulbasaur !> squirtle)
+var answer = kb.ask(bulbasaur !> squirtle)
 ```
 
+LogicKit offers a bunch of syntax sugars to improve the legibility of your code.
+Make sure to check the *User Manual* for a comprehensive documentation.
+
 ### Installation
 
-LogicKit is distributed in the form of a Switch package
+LogicKit is distributed in the form of a Swift package
 and can be integrated with the [Swift Package Manager](https://swift.org/package-manager/).
 
 Start by creating a new package (unless you already have one):
@@ -178,16 +187,20 @@ Then add LogicKit as a dependency to your package, from your `Package.swift` fil
 import PackageDescription
 
 let package = Package(
-    name: "MyLogicProgram",
-    dependencies: [
-        .package(url: "https://github.com/kyouko-taiga/LogicKit", from: "1.0.0"),
-    ],
-    targets: [
-        .target(name: "MyLogicProgram", dependencies: ["LogicKit"]),
-    ]
+  name: "MyLogicProgram",
+  dependencies: [
+    .package(url: "https://github.com/kyouko-taiga/LogicKit", .branch("master")),
+  ],
+  targets: [
+    .target(name: "MyLogicProgram", dependencies: ["LogicKit"]),
+  ]
 )
 ```
 
+> The master branch of the LogicKit always refers to the latest stable version of LogicKit, so
+> using `.branch("master")` to specify the dependency location guarantees you'll always pull the
+> latest version. See Swift Package Manager's documentation for alternative configurations.
+
 Make sure the Swift Package Manager is able to properly download, compile and link LogicKit
 with the following command:
 
@@ -213,7 +226,7 @@ import LogicKit
 > swift package generate-xcodeproj
 > ```
 >
-> It will create a `YourPackage.xcodeproj` directory you can edit with Xcode.
+> It will create a `MyLogicProgram.xcodeproj` directory you can edit with Xcode.
 > The schemes of the auto-generated package might require some manual configuration.
 > Please refer to Xcode's documentation for more information on that end.
 

From d93f53157cbc17866a003247dd9ca015ffe64f7c Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 21:23:56 +0100
Subject: [PATCH 31/32] Write a user manual

---
 Docs/UserManual.md | 455 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 455 insertions(+)
 create mode 100644 Docs/UserManual.md

diff --git a/Docs/UserManual.md b/Docs/UserManual.md
new file mode 100644
index 0000000..7445ca7
--- /dev/null
+++ b/Docs/UserManual.md
@@ -0,0 +1,455 @@
+# LogicKit's User Manual
+
+This user manual documents the installation and usage of the LogicKit library.
+
+## Installation
+
+### Swift Package Manager
+
+The recommended approach to integrate LogicKit with your project is to declare it as a dependency
+by the means of the [Swift Package Manager](https://swift.org/package-manager/).
+
+The most likely use case is to use LogicKit in an executable package.
+Start by creating a new package:
+
+```bash
+mkdir MyLogicProgram
+cd MyLogicProgram
+swift package init --type executable
+```
+
+Then add LogicKit as a dependency to your package, from your `Package.swift` file:
+
+```swift
+import PackageDescription
+
+let package = Package(
+  name: "MyLogicProgram",
+  dependencies: [
+    .package(url: "https://github.com/kyouko-taiga/LogicKit", .branch("master")),
+  ],
+  targets: [
+    .target(name: "MyLogicProgram", dependencies: ["LogicKit"]),
+  ]
+)
+```
+
+LogicKit adopts [semantic versioning](https://semver.org) to label its releases,
+which is fully compatible with how Swift Package Manager handles dependency versions.
+Hence, you may replace `.branch("master")` with any other particular specification
+to have a better control over the version your code is linked against.
+Please refer to Swift Package Manager's documentation for the syntax of such specifications.
+The master branch of the LogicKit always refers to the latest stable version of LogicKit,
+so linking against `.branch("master")` guarantees your project will always pull the latest version.
+
+Make sure the Swift Package Manager is able to properly download, compile and link LogicKit
+with the following command:
+
+```bash
+swift build
+```
+
+If everything goes well,
+you should then be able to import LogicKit in your own Swift sources:
+
+```swift
+import LogicKit
+
+// Your code here ...
+```
+
+To update your package with the latest version of LogicKit,
+simply run the following command:
+
+```bash
+swift package update
+```
+
+### Xcode
+
+Xcode users may also use Swift Package Manager to create their Xcode projects.
+Once you've added LogicKit has a dependency and compiled your project at least once,
+type the command:
+
+```bash
+  swift package generate-xcodeproj
+```
+
+It will create a `MyLogicProgram.xcodeproj` directory you can edit with Xcode.
+The schemes of the auto-generated package might require some manual configuration.
+Please refer to Xcode's documentation for more information on that end.
+
+To integrate LogicKit with an existing Xcode project **without** using Swift Package Manager,
+create two targets in your project: `LogicKit` and `LogicKitBuiltins`.
+Copy the files in `Sources/LogicKit/` and `Sources/LogicKitBuiltins` to your own project,
+and add them to the build phase of your `LogicKit` and `LogicKitBuiltins` targets, respectively.
+
+## Usage
+
+### Simple Facts
+
+Like Prolog, LogicKit revolves around a knowledge base (or database),
+against which one can make queries.
+There are four constructs in LogicKit:
+Facts (`Term.fact(_:_:)`) that denote predicates and propositions,
+rules (`Term.rule(_:_:_:)`) that denote conditional facts,
+literals (`Term.lit(_:)`) that denote atomic values, and
+variables (`Term.var(_:)`) that act as placeholders for other terms.
+
+Knowledge bases are nothing more than a collection of such constructs:
+
+```swift
+let kb: KnowledgeBase = [
+  .fact("is effective against", .fact("water"), .fact("fire")),
+  .fact("is effective against", .fact("fire"), .fact("grass")),
+  .fact("is effective against", .fact("grass"), .fact("water")),
+
+  .fact("has type", .fact("Bulbasaur")), .fact("grass")),
+  .fact("has type", .fact("Squirtle")), .fact("water")),
+  .fact("has type", .fact("Charmander")), .fact("fire")),
+]
+```
+
+The above knowledge base only makes use of facts and propositions.
+It states for instance that *water is effective against fire*,
+or that *Squirtle has type water*.
+One can query such knowledge base as follows:
+
+```swift
+var answers = kb.ask(.fact("has type", .fact("Squirtle"), .fact("water")))
+```
+
+Since there might be several answers to a single query,
+`Knowledge.ask(_:logger:)` doesn't return a single yes/no answer.
+Instead, it returns a sequence whose each element denote one correct answer.
+If the sequence is empty, then there isn't any solution.
+
+```swift
+print("Squirtle has type water:" answers.next() != nil)
+// Prints "Squirtle has type water: true"
+```
+
+The type `Term` conforms to Swift's [`ExpressibleByStringLiteral`](https://developer.apple.com/documentation/swift/expressiblebystringliteral) protocol,
+so that propositions (i.e. terms of arity 0) may be written as simple string literals.
+Therefore, one can rewrite the above knowledge base as follows:
+
+```swift
+let kb: KnowledgeBase = [
+  .fact("is effective against", "water", "fire"),
+  .fact("is effective against", "fire", "grass"),
+  .fact("is effective against", "grass", "water"),
+
+  .fact("has type", "Bulbasaur", "grass"),
+  .fact("has type", "Squirtle", "water"),
+  .fact("has type", "Charmander", "fire"),
+]
+```
+
+See the *API* section for more details and examples about LogicKit's syntax sugars.
+
+### Variables and Unification
+
+Being able to query our knowledge base this way has its use cases,
+but does not improve much from using a simple set.
+What's more interesting is to query a knowledge base for information we do not fully have.
+For instance, one could wonder what Pokemon has type grass.
+This is done by the means of *variables*.
+
+```swift
+var answers = kb.ask(.fact("has type", .var("x"), "grass"))
+```
+
+The above query reads as *Pokemon `x` has type grass*,
+`X` being a variable that could represent any term.
+
+Unlike before, when we were simply asking whether or not something is known for fact,
+we now also want to know for *which* values a given term is a fact.
+Fortunately, `Knowledge.ask(_:logger:)` gives us everything we need to answer that question.
+The method returns an instance of type called `AnswerSet`,
+which acts as a sequence of bindings that map variable names to terms.
+Therefore one should iterate over it to pull all possible results:
+
+```swift
+for answer in answers {
+  print(answer["x"]!, "has type grass")
+}
+```
+
+> There's only a single result in our particular example,
+> but try to modify the knowledge base so that the above query may have multiple valid answers.
+
+Queries are not constrained to contain a single variable.
+Hence, one could for instance ask for all pairs of Pokemon/type with the following query:
+
+```swift
+var answers = kb.ask(.fact("has type", .var("x"), .var("y")))
+for answer in answers {
+  print(answer["x"]!, "has type", answer["y"]!)
+}
+
+```
+
+LogicKit relies on [*unification*](https://en.wikipedia.org/wiki/Unification_(computer_science))
+to carry out its deduction.
+In a nutshell, given two term `p($x, b)` and `p(a, $y)`,
+the engine attempts to find values for each free variable
+(i.e. `$x` and `$y` in this particular example)
+so that both terms are equal.
+Unification usually occurs implicitly when one wants to match a given term with a particular *pattern*.
+Nevertheless, a special built-in predicate `~=~` allow one to request unification explicitly:
+
+```swift
+let goal: Term = .fact("a") ~=~ .vat("x")
+```
+
+### Rules
+
+Being able to query our knowledge base this way is nice,
+but only gets us so far.
+What's more interesting is to use LogicKit to make deductions.
+Let's add a rule to our knowledge base:
+
+```swift
+.rule("is stronger", .var("x"), .var("y")) {
+  .fact("has type", .var("x"), .var("tx")) &&
+  .fact("has type", .var("y"), .var("ty")) &&
+  .fact("is effective against", .var("tx"), .var("ty"))
+}
+```
+
+This rule states that a Pokemon `x` is stronger than a Pokemon `y`
+if the type of `x` is effective against that of `y`.
+Now we can ask things like:
+
+```swift
+var answers = kb.ask(.fact("is stronger", "Charmander", "Bulbasaur"))
+```
+
+or even more interestingly:
+
+```swift
+var answers = kb.ask(.fact("is stronger", .var("a"), .var("b")))
+```
+
+### Atomic Values (a.k.a. Literals)
+
+The 4th construct of LogicKit is the atomic value (a.k.a. literal).
+An atomic value is like a proposition,
+but can be represented by any type of Swift, as long as it is `Hashable`.
+For instance, one may create the following program:
+
+```swift
+let kb: KnowledgeBase = [
+  .fact("is big", .lit(1 ... 10_000_000)),
+  .fact("is small", .lit(1 ... 2)),
+]
+
+var answers = kb.ask(.fact("is big", .var("a")))
+for answer in answers {
+  print(answer["a"]!, "is big")
+}
+```
+
+Note however than we may not interact the same way with atomic values as we can with regular terms.
+Indeed, LogicKit sees them as equatable black boxes,
+but cannot use any predicate on their intrinsic value to make deductions.
+They are indeed *atomic*.
+For instance, one may store a whole Swift array as an atomic value,
+but may not ask LogicKit to use its values to make deductions.
+
+> Swift's `String` is obviously hashable, and hence could be used as a literal value. This is
+> however discouraged, as using character strings as propositions offers more flexibility.
+
+Why using atomic values at all then?
+Because they can act as a glue between native Swift code and logic programs written with LogicKit.
+While one cannot use predicates on their intrinsic value,
+one may write a Knowledge base that defines predicates over their identity.
+
+### Troubleshooting
+
+Debugging a logic program can be a little daunting,
+as one cannot easily follow the sequence of instructions the machine will do,
+which is quite a departure from the much more classic imperative paradigm.
+Nevertheless, LogicKit offers a rudimental way to get a look into its deduction engine,
+by the means of a logger.
+
+The method `Knowledge.ask(_:logger:)` accepts an optional logger
+(i.e. any type that conforms to LogicKit's `Logger` protocol).
+If provided, LogicKit will call the methods
+`Logger.willRealize(goal:)`,
+`Logger.willAttempt(clause:)` and
+`Logger.didBacktrack()`
+so as to provide the user with some information about the current state of its engine.
+
+A default logger named `DefaultLogger`
+that simply prints every call to the above methods
+is shipped with LogicKit.
+
+```swift
+var answers = kb.ask(.fact("is stronger", .var("a"), .var("b")), logger: DefaultLogger())
+_ = Array(answers)
+
+// Prints:
+//
+//     Attempting to realize has type[$x, $tx]
+//     using has type[Bulbasaur, grass]
+//     Attempting to realize has type[$y, $ty]
+//     using has type[Bulbasaur, grass]
+//     Attempting to realize is effective against[grass, grass]
+//     using is effective against[water, fire]
+//     using is effective against[fire, grass]
+//     using is effective against[grass, water]
+//     using has type[Squirtle, water]
+//     Attempting to realize is effective against[grass, water]
+//     using is effective against[water, fire]
+//     using is effective against[fire, grass]
+//     using is effective against[grass, water]
+//     Attempting to realize is effective against[grass, water]
+//     backtacking
+//     ...
+//
+```
+
+## API
+
+This section describes the API of LogicKit,
+with a particular focus on its syntax sugars.
+
+### The `Term` Enumeration
+
+At the core of the API sits the `Term` enumeration,
+that describes the data type handled by LogicKit.
+Although the enumeration has 5 cases,
+namely `var`, `val`, `_term`, `_rule`, `conjunction` and `disjunction`,
+only the first one should be manipulated directly by the user code.
+More elaborated constructors are available for other cases.
+
+**Atomic Values**:
+
+The static method `Term.lit<T>(_:)` creates atomic values.
+It accepts any value as argument, as long as its type conforms to `Hashable`,
+and wraps it within a term.
+
+```swift
+let atom: Term = .lit([1, 2, 3])
+```
+
+You may use the method `Term.extractValue(ofType:)` to extract a value from a term.
+The method expects the type of the value to extract as parameter.
+Note that the function returns an optional,
+that will be set to `nil` if the term either isn't an atomic value,
+or doesn't wrap a value with the requested type.
+
+```swift
+let array = atom.extractValue(ofType: [Int].self)
+```
+
+**Facts**:
+
+Facts can be created with the static method `Term.fact(name:arguments:)`,
+which expects a functor name and an arbitrary number arguments,
+in the form of terms.
+
+```swift
+let proposition: Term = .fact("proposition")
+print(proposition)
+// Prints "proposition"
+
+let predicate1: Term = .fact("is a letter", "a")
+print(predicate1)
+// Prints "is a letter[a]"
+
+let predicate2: Term = .fact("is shorter", .lit([1, 2]), .lit([2, 3, 4]))
+print(predicate2)
+// Prints "is shorter[[1, 2], [2, 3, 4]]"
+```
+
+Notice that because `Term` conforms to `ExpressibleByStringLiteral`,
+the argument of the predicate `is a letter` is indeed a term,
+and not an atomic value.
+
+Facts may also be created by subscripting propositions with an arbitrary number of arguments.
+In this case, the proposition becomes the functor of the produced term.
+
+```swift
+let love: Term = "love"
+print(love["Ash", "Pikachu"])
+// Prints "love(Ash, Pikachu)"
+```
+
+> Attempting to subscript a term that is not a proposition will trigger an unrecoverable error.
+
+**Rules**:
+
+Facts can be created with the static method `Term.rule(name:arguments:body:)`,
+which expects a functor name, an arbitrary number arguments in the form of terms,
+and a closure that returns the rule's body, also as a term.
+
+```swift
+let pred: Term = .rule("painful", .var("x")) {
+  .fact("too hot", .var("x")) || .fact("too cold", .var("x"))
+}
+print(pred)
+// Print "(painful[$x] ⊢ (too hot[$x] ∨ too cold[$x]))"
+```
+
+Using `Term.rule(name:arguments:body:)` is recommended,
+as it's simpler to parse by the Swift compiler, compared to other constructures.
+Therefore the compiler is likely to produce more insightful error messages in case of syntax errors.
+Nevertheless, you may use the operators `=>`, `|-` or `⊢` to achieve the same result.
+
+```swift
+let pred1: Term = .fact("too hot", .var("x")) || .fact("too cold", .var("x")) =>
+  .fact("painful", .var("x"))
+let pred2: Term = .fact("painful", .var("x")) |-
+  .fact("too hot", .var("x")) || .fact("too cold", .var("x"))
+let pred3: Term = .fact("painful", .var("x")) ⊢
+  .fact("too hot", .var("x")) || .fact("too cold", .var("x"))
+```
+
+**Conjunctions and Disjunction**:
+
+Conjunctions and disjunction of terms can be created with the operators `&&` and `||`,
+respectively.
+An variant of each operator that more closely resembles formal notations is also available.
+
+```swift
+let pred1: Term = .fact("a") && .var("x")
+let pred2: Term = .fact("a") ∧ .var("x")
+
+let pred3: Term = .fact("a") || .var("x")
+let pred4: Term = .fact("a") ∨ .var("x")
+```
+
+**Unification Predicate**
+
+A special built-in predicate allows one to express a goal as the mere unification of two terms.
+It can be constructed with the operator `~=~`.
+
+```swift
+let pred: Term = love["Ash", "Pikachu"] ~=~ love["Ash", .var("x")]
+```
+
+### Built-ins
+
+LogicKit comes with some built-ins facts and rules that are commonly found in knowledge bases.
+See `Sources/LogicKitBuiltins` for the exhaustive list.
+
+First import the Swift module where they are defined:
+
+```swift
+import LogicKitBuiltins
+```
+
+All built-in modules are in the form of a namespace that contains generators for the related terms,
+constructors for their predicates and a static variable `axioms` with the corresponding facts and rules.
+
+```swift
+import LogicKitBuiltins
+
+let kb = KnowledgeBase(knowledge: Nat.axioms)
+let query = Nat.mul(Nat.from(2), Nat.from(5), .var("x"))  // 5 * 2 = x
+let binding = kb.ask(query).next()
+print(Nat.asSwiftInt(binding!["x"]!)!)
+// Prints "10"
+```

From 33e995c61afe993b7b76272a8e1f2585094e05a3 Mon Sep 17 00:00:00 2001
From: Dimitri Racordon <dimitri.racordon@gmail.com>
Date: Sun, 24 Feb 2019 21:41:37 +0100
Subject: [PATCH 32/32] Typo

---
 Docs/UserManual.md | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/Docs/UserManual.md b/Docs/UserManual.md
index 7445ca7..250e093 100644
--- a/Docs/UserManual.md
+++ b/Docs/UserManual.md
@@ -35,11 +35,11 @@ let package = Package(
 ```
 
 LogicKit adopts [semantic versioning](https://semver.org) to label its releases,
-which is fully compatible with how Swift Package Manager handles dependency versions.
+which is fully compatible with the way Swift Package Manager handles dependency versions.
 Hence, you may replace `.branch("master")` with any other particular specification
 to have a better control over the version your code is linked against.
 Please refer to Swift Package Manager's documentation for the syntax of such specifications.
-The master branch of the LogicKit always refers to the latest stable version of LogicKit,
+The master branch of the LogicKit repository always refers to the latest stable version of LogicKit,
 so linking against `.branch("master")` guarantees your project will always pull the latest version.
 
 Make sure the Swift Package Manager is able to properly download, compile and link LogicKit
@@ -190,13 +190,13 @@ for answer in answers {
 ```
 
 LogicKit relies on [*unification*](https://en.wikipedia.org/wiki/Unification_(computer_science))
-to carry out its deduction.
+to carry out its deductions.
 In a nutshell, given two term `p($x, b)` and `p(a, $y)`,
-the engine attempts to find values for each free variable
-(i.e. `$x` and `$y` in this particular example)
-so that both terms are equal.
-Unification usually occurs implicitly when one wants to match a given term with a particular *pattern*.
-Nevertheless, a special built-in predicate `~=~` allow one to request unification explicitly:
+the engine attempts to find values for each free variable so that both terms are equal
+(i.e. `$x := a` and `$y := b` in this particular example).
+Unification usually occurs implicitly,
+when a given term is matched with a particular *pattern*.
+Nevertheless, a special built-in predicate `~=~` allows one to request unification explicitly:
 
 ```swift
 let goal: Term = .fact("a") ~=~ .vat("x")
@@ -206,7 +206,7 @@ let goal: Term = .fact("a") ~=~ .vat("x")
 
 Being able to query our knowledge base this way is nice,
 but only gets us so far.
-What's more interesting is to use LogicKit to make deductions.
+What's more interesting is to use LogicKit to make more elaborate deductions.
 Let's add a rule to our knowledge base:
 
 ```swift
@@ -250,9 +250,9 @@ for answer in answers {
 }
 ```
 
-Note however than we may not interact the same way with atomic values as we can with regular terms.
+Note however than LogicKit doesn't interact the same way with atomic values as it does with regular terms.
 Indeed, LogicKit sees them as equatable black boxes,
-but cannot use any predicate on their intrinsic value to make deductions.
+but can't use any predicate on their intrinsic value to make deductions.
 They are indeed *atomic*.
 For instance, one may store a whole Swift array as an atomic value,
 but may not ask LogicKit to use its values to make deductions.
@@ -263,7 +263,7 @@ but may not ask LogicKit to use its values to make deductions.
 Why using atomic values at all then?
 Because they can act as a glue between native Swift code and logic programs written with LogicKit.
 While one cannot use predicates on their intrinsic value,
-one may write a Knowledge base that defines predicates over their identity.
+one may write a knowledge base that defines predicates over their identity.
 
 ### Troubleshooting
 
@@ -394,7 +394,7 @@ print(pred)
 ```
 
 Using `Term.rule(name:arguments:body:)` is recommended,
-as it's simpler to parse by the Swift compiler, compared to other constructures.
+as it's simpler to parse by the Swift compiler, compared to other constructuors.
 Therefore the compiler is likely to produce more insightful error messages in case of syntax errors.
 Nevertheless, you may use the operators `=>`, `|-` or `⊢` to achieve the same result.
 
@@ -411,7 +411,7 @@ let pred3: Term = .fact("painful", .var("x")) ⊢
 
 Conjunctions and disjunction of terms can be created with the operators `&&` and `||`,
 respectively.
-An variant of each operator that more closely resembles formal notations is also available.
+A variant of each operator that more closely resembles formal notations is also available.
 
 ```swift
 let pred1: Term = .fact("a") && .var("x")
@@ -435,7 +435,7 @@ let pred: Term = love["Ash", "Pikachu"] ~=~ love["Ash", .var("x")]
 LogicKit comes with some built-ins facts and rules that are commonly found in knowledge bases.
 See `Sources/LogicKitBuiltins` for the exhaustive list.
 
-First import the Swift module where they are defined:
+First, import the Swift module where they are defined:
 
 ```swift
 import LogicKitBuiltins