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
|
## Kompsos
An experimental implementation of [miniKanren](https://minikanren.org/) 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)
which is quite short, 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 concept of four primitives.
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.</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.
Internally a Goal is structured as a directed acyclic graph. Evaluation of
a Goal involves walking the graph while applying relevant operations to the
base State and expanding any Conjuncts to more of the graph as they are
encountered. The expanded portions, bookkeeping data, and memoised partial
results are all discarded once evaluation is complete.
The various cond operations are completely absent, as they do not really make
sense in an object oriented context. Use a Disjunct operation on several Goals
instead.
All the Goal operations beyond the microKanren four take an array of Terms as
input in order to allow for Conjunct to be reasonably implemented.
The State datatype makes use of custom unrolled linked lists, and the
bookkeeping data in the Collector package uses a custom directed acyclic graph
structure that reflects the main Goal graph. This is done instead of using
Vectors or Maps from the standard library both to improve speed and reduce
memory requirements. The improvement due to tail sharing is considerable,
despite the theoretically expensive operations involved in walking the list to
reify a variable.
#### Credits and Licensing
Written by Jedidiah Barber
Licensed under the Sunset License v1.0. For details see `license.txt`.
|
