commit c019b4fe223ad8feb0f9078094b1d020c519d877
parent 0b1fa17fd5a927f6e96c15d62d8e4ab437b24c98
Author: Jan Pobříslo <ccx@te2000.cz>
Date: Wed, 29 Nov 2023 08:10:09 +0000
WIP fixes
Diffstat:
5 files changed, 176 insertions(+), 57 deletions(-)
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1 @@
+*.sw[op]
diff --git a/Makefile b/Makefile
@@ -0,0 +1,2 @@
+example:
+ jsonnet -J . example.jsonnet
diff --git a/example.jsonnet b/example.jsonnet
@@ -0,0 +1,15 @@
+local uK = import 'microkanren.libsonnet';
+local uKc = import 'microkanren_checks.libsonnet';
+
+{
+ justFive:
+ local goal = uK.callFresh(function(q) q.eq(5));
+ assert uKc.Goal(goal);
+ assert uKc.trace('goal', goal, true);
+ local stream = goal.pursue(uK.emptyState);
+ assert std.type(stream);
+ true, /*
+ assert uKc.Stream(stream);
+ stream.takeAll(), */
+}
+// vim: sts=2 ts=2 sw=2 et
diff --git a/microkanren.libsonnet b/microkanren.libsonnet
@@ -1,28 +1,31 @@
+local uKc = import 'microkanren_checks.libsonnet';
+// helper functions
+
local baseStream(streamType) = {
['µK:stream']: streamType,
- pull::
+ pull()::
if self['µK:stream'] == 'immature' then
- self.call().pull
+ self.call().pull()
else
self,
- takeAll::
+ takeAll()::
local takeRecursive(accumulator, stream) =
- local mature = stream.pull,
+ local mature = stream.pull();
if mature['µK:stream'] == 'empty' then
accumulator
else
- takeRecursive(accumulator + [mature.state], mature.next),
+ takeRecursive(accumulator + [mature.state], mature.next);
takeRecursive([], self),
take(n)::
local takeRecursive(accumulator, stream) =
if std.length(accumulator) >= n then
accumulator
else
- local mature = stream.pull,
+ local mature = stream.pull();
if mature['µK:stream'] == 'empty' then
accumulator
else
- takeRecursive(accumulator + [mature.state], mature.next),
+ takeRecursive(accumulator + [mature.state], mature.next);
takeRecursive([], self),
};
@@ -37,11 +40,14 @@ local immatureStream(func) = baseStream('immature') + {
local makeGoal(callable) = {
['µK:goal']: callable,
- pursue(state):: self['µK:goal'](state),
+ pursue(state)::
+ assert uKc.trace('pursuing goal in state', state, true);
+ assert uKc.State(state);
+ self['µK:goal'](state),
};
local mplus(stream1, stream2) =
- local t1 = stream1['µK:stream'],
+ local t1 = stream1['µK:stream'];
if t1 == 'empty' then
immatureStream(function() stream2)
else if t1 == 'immature' then
@@ -52,25 +58,26 @@ local mplus(stream1, stream2) =
error 'Invalid stream';
local bind(stream, goal) =
- local t = stream['µK:stream'],
+ local t = stream['µK:stream'];
if t == 'empty' then
stream
else if t == 'immature' then
- immatureStream(function() bind(stream1.call(), goal))
+ immatureStream(function() bind(stream.call(), goal))
else if t == 'mature' then
- immatureStream(function() mplus(goal.pursue(stream1.state), bind(stream2, goal)))
+ immatureStream(function() mplus(goal.pursue(stream.state), bind(stream.next, goal)))
else
error 'Invalid stream';
+// public interface
{
type(value):
- local t = std.type(value),
+ local t = std.type(value);
if t == 'object' then
if std.type(std.get(value, 'µK:var')) == 'number' then
'variable'
- else if std.type(std.get(value, 'µK:goal'), 'function') then
+ else if std.type(std.get(value, 'µK:goal')) == 'function' then
'goal'
- else if std.type(std.get(value, 'µK:stream'), 'string') then
+ else if std.type(std.get(value, 'µK:stream')) == 'string' then
'stream'
else
t
@@ -79,22 +86,22 @@ local bind(stream, goal) =
// state
emptyState: {
- variable_count: 0,
+ variableCount: 0,
substitution: {
walk(var)::
- if type(var) == 'variable' then
- local bound = std.get(self, var['µK:var'])),
+ if $.type(var) == 'variable' then
+ local bound = std.get(self, var['µK:var']);
if bound == null then
- u
+ var
else
self.walk(bound)
else
var,
unify(value1, value2)::
- local w1 = self.walk(value1),
- local w2 = self.walk(value1),
- local t1 = type(w1),
- local t2 = type(w2),
+ local w1 = self.walk(value1);
+ local w2 = self.walk(value1);
+ local t1 = $.type(w1);
+ local t2 = $.type(w2);
if t1 == 'variable' && t2 == 'variable' && w1 == w2 then
self
else if t1 == 'variable' then
@@ -106,7 +113,7 @@ local bind(stream, goal) =
if std.length(w1) == 0 then
self
else
- local s1 = self.unify(w1[0], w2[0]),
+ local s1 = self.unify(w1[0], w2[0]);
if s1 == null then
null
else
@@ -131,54 +138,70 @@ local bind(stream, goal) =
else
null,
},
- freshVar:: {
+ freshVar():: {
variable: {
- ['µK:var']: self.variable_count,
+ ['µK:var']: self.variableCount,
eq(value):: $.eq(self, value),
},
- newState: self + {variable_count: self.variable_count + 1}
+ newState: self + {variableCount: self.variableCount + 1}
},
},
// streams
emptyStream: baseStream('empty'),
- unitStream(state): matureStream(state, emptyStream),
+ unitStream(state): matureStream(state, $.emptyStream),
// goal constructors
eq(value1, value2): makeGoal(function(state)
- local newState = state.unify(value1, value2),
- if newState == null then
- emptyStream
+ assert uKc.State(state);
+ local newSubst = state.substitution.unify(value1, value2);
+ if newSubst == null then
+ $.emptyStream
else
- unitStream(newState)
- ),
- conj(goal1, goal2): makeGoal(function(state)
- $.bind(goal1.pursue(state), goal2)
+ $.unitStream(state + {substitution: newSubst})
),
- disj(goal1, goal2): makeGoal(function(state)
- $.mplus(goal1.pursue(state), goal2.pursue(state))
- ),
- callFresh(func): makeGoal(function(state)
- local fresh = state.freshVar,
- local newGoal = func(fresh.variable),
- local t = type(newGoal),
- (if t == 'goal' then
- newGoal
- else if t == 'array' then
- local subgoals = std.reverse(newGoal[1::]),
- (if newGoal[0] == 'and' then
- std.foldl($.conj, subgoals[1::], subgoals[0])
- else if newGoal[0] == 'or' then
- std.foldl($.disj, subgoals[1::], subgoals[0])
- else if newGoal[0] == 'eq' then
- std.foldl($.disj, subgoals[1::], subgoals[0])
+ conj(goal1, goal2):
+ assert uKc.Goal(goal1);
+ assert uKc.Goal(goal2);
+ makeGoal(function(state)
+ assert uKc.State(state);
+ $.bind(goal1.pursue(state), goal2)
+ ),
+
+ disj(goal1, goal2):
+ assert uKc.Goal(goal1);
+ assert uKc.Goal(goal2);
+ makeGoal(function(state)
+ assert uKc.State(state);
+ $.mplus(goal1.pursue(state), goal2.pursue(state))
+ ),
+
+ callFresh(func):
+ assert std.assertEqual(std.type(func), 'function');
+ makeGoal(function(state)
+ assert uKc.State(state);
+ local fresh = state.freshVar();
+ assert uKc.Variable(fresh.variable);
+ assert uKc.State(fresh.newState);
+ local newGoal = func(fresh.variable);
+ local t = $.type(newGoal);
+ (if t == 'goal' then
+ newGoal
+ else if t == 'array' then
+ local subgoals = std.reverse(newGoal[1::]);
+ (if newGoal[0] == 'and' then
+ std.foldl($.conj, subgoals[1::], subgoals[0])
+ else if newGoal[0] == 'or' then
+ std.foldl($.disj, subgoals[1::], subgoals[0])
+ else if newGoal[0] == 'eq' then
+ std.foldl($.disj, subgoals[1::], subgoals[0])
+ else
+ error 'Invalid goal'
+ )
else
error 'Invalid goal'
- )
- else
- error 'Invalid goal'
- ).pursue(fresh.newState)
- ),
+ ).pursue(fresh.newState)
+ ),
}
// vim: sts=2 ts=2 sw=2 et
diff --git a/microkanren_checks.libsonnet b/microkanren_checks.libsonnet
@@ -0,0 +1,78 @@
+local safeString(value) =
+ local t = std.type(value);
+ if t == 'function' then
+ '<function>'
+ else if t == 'array' then
+ '[%s]' % [std.join(', ', std.map(safeString, value))]
+ else if t == 'object' then
+ '{%s}' % [std.join(', ', std.map(
+ function(f) '%s: %s' % [std.escapeStringJson(f.key), safeString(f.value)],
+ std.objectKeysValuesAll(value)
+ ))]
+ else
+ std.toString(value);
+
+local checkType(type) = function(value) std.assertEqual(std.type(value), type);
+// value checks
+{
+ trace(str, val, rest):
+ std.trace("%s: %s" % [str, safeString(val)], rest),
+
+ objectFields(obj, checks):
+ assert std.assertEqual(std.type(obj), 'object');
+ assert std.assertEqual(std.objectFields(obj), std.objectFields(checks));
+ std.all(std.map(
+ function(f) checks[f.key](f.value),
+ std.objectKeysValues(obj)
+ )),
+
+ Variable(var):
+ $.objectFields(var, {
+ ['µK:var']: function(value)
+ assert std.assertEqual(std.type(value), 'number');
+ assert value >= 0: "Incorrect variable number: %s" % [value];
+ true,
+ }),
+
+ VariableCount(vc):
+ assert vc >= 0: "Incorrect state.variableCount: less than zero";
+ true,
+
+ Substitution(subst):
+ assert std.assertEqual(std.type(subst), 'object');
+ std.all(std.map(
+ function(f) std.assertEqual(std.type(f.name), 'number'),
+ std.objectKeysValues(subst)
+ )),
+
+ State(state):
+ $.objectFields(state, {
+ variableCount: $.VariableCount,
+ substitution: $.Substitution,
+ }),
+
+ Stream(stream):
+ assert std.assertEqual(std.type(stream), 'object');
+ local t = stream['µK:stream'];
+ assert std.type(t) == 'string';
+ if t == 'empty' then
+ $.objectFields(stream, {['µK:stream']: checkType('string')})
+ else if t == 'immature' then
+ $.objectFields(stream, {
+ ['µK:stream']: checkType('string'),
+ call: checkType('function'),
+ })
+ else if t == 'mature' then
+ $.objectFields(stream, {
+ ['µK:stream']: checkType('string'),
+ call: checkType('function'),
+ })
+ else
+ error "Incorrect stream type",
+
+ Goal(goal): $.objectFields(goal, {
+ ['µK:goal']: checkType('function'),
+ }),
+
+}
+// vim: sts=2 ts=2 sw=2 et
