## Kompsos

An experimental implementation of [miniKanren](https://minikanren.org/).
Written in Ada, a language very much unsuited for the exercise due to its lack
of support for the functional programming paradigm. Came about after reading the
[2013 microKanren paper](http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf)
and then noticing that nobody had tried writing it in Ada. The name Kompsos
comes from Greek, meaning "elegant" or "refined" or "dainty" and is in
reference to the microKanren four primitive concept.

Typical usage involves declaring a Goal, applying some operations to it
including creating a few variable Terms, evaluating that Goal to obtain a
number of States, then reifying the variable Terms with respect to one of those
States. The reified Terms can then be decomposed at your leisure.

Most commonly only the main Kompsos package and the Math and Pretty_Print
child packages will be needed. Although Collector is also used internally for
the basic reification.



#### Dependencies

Build time:
<ul>
  <li>GNAT</li>
  <li>GPRbuild</li>
</ul>

There are no particular run time dependencies.



#### Building and Installation

This repository is written to use the GNAT Project Manager build tools. To
build, use the following command

`gprbuild kompsos.gpr`

There is a single build switch of `-Xbuild` which can have a value of `release`
(the default) or `debug`.

If you want to install this project, use

`gprinstall -p -m kompsos.gpr`

In addition, the project files `tests.gpr` and `examples.gpr` can be used to
compile several small test and example programs respectively.

For further information on the build tools, consult the
[GPRbuild docs](https://docs.adacore.com/gprbuild-docs/html/gprbuild_ug.html).



#### Technical Notes

A brief explanation of the package hierarchy:
<ul>
  <li>`Kompsos` Term, State, Goal datatypes, microKanren operations,
  evaluation, Term reification, and non-numeric miniKanren prelude.</li>
  <li>`Kompsos.Advanced_Reify` Functions to convert from Term to either a
  flattened array of data elements or a Multiway_Tree from the Ada Containers
  library. Reification into a Multiway_Tree.</li>
  <li>`Kompsos.Collector` Manual stepthrough evaluation of a Goal to find
  satisfying States.</li>
  <li>`Kompsos.Math` Arithmetic parts of miniKanren prelude. Includes extra
  Greater Than operations.</li>
  <li>`Kompsos.Pretty_Print` Conversion of datatypes to Strings, conversion
  of Goal graphs to the DOT graph desciption language.</li>
</ul>

Since the arithmetic prelude subprograms are in a child package they are
unfortunately not considered primitive operations of the Goal datatype. This
makes using them slightly more awkward than they otherwise would be. But
placing them all in the main package would not have made sense due to the math
operations needing to know what zero and one are. It would also have made the
main package unreasonably large.

The various cond operations are completely absent, as this implementation
instead follows microKanren for its core workings. The cond variations do not
really make sense in an object oriented context anyway. Use a Disjunct
operation on several Goals instead.

All the Goal operations beyond those from microKanren take either zero, one,
or an array of Terms as input in order to allow for Conjunct to be reasonably
implemented. The practical implication of this is there will be a lot of use
of the `&` operator when using this library, as can be seen in the example
programs.

Internally a Goal is structured as a directed acyclic graph. Evaluation of a
Goal involves inverting the arrows in the graph, interleaving those arrows
according to Disjunct choices made from the top to get there, and then running
an iterative deepening depth-first search from the bottom upwards using the
inverted graph. The depth limit that is iterated on is the number of Conjunct
nodes seen. When a Conjunct node is encountered it is expanded, inverted,
and interleaved before the search continues. If too many Conjunct nodes have
been encountered, the search will backtrack to before where the first one was,
increase the limit, and keep going on other branches before coming back later.
The inversions and expanded portions are all discarded once evaluation is
complete.

The State datatype makes use of a Vector of Variable->Term bindings and a
Hashed_Map to get from Variable to the index for the Vector. Both are needed so
that lookups can be fast and truncations of the State to remove the newest
bindings are easy to do when backtracking during the depth-first search.



#### Credits and Licensing

Written by Jedidiah Barber.

Licensed under the Sunset License v1.0. For details see `license.txt`.