1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
## 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
a depth-first search from the bottom upwards using the inverted graph. When
a Conjunct node is encountered it is expanded, inverted, and interleaved in a
similar way before the search continues. 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`.
|
