jsonnet-microkanren

microKanren implementation in Jsonnet
git clone https://ccx.te2000.cz/git/jsonnet-microkanren
Log | Files | Refs

commit 0b1fa17fd5a927f6e96c15d62d8e4ab437b24c98
Author: Jan Pobříslo <ccx@te2000.cz>
Date:   Wed, 29 Nov 2023 05:11:39 +0000

Initial untested implementation

Diffstat:
Amicrokanren.libsonnet | 184+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 184 insertions(+), 0 deletions(-)

diff --git a/microkanren.libsonnet b/microkanren.libsonnet @@ -0,0 +1,184 @@ +local baseStream(streamType) = { + ['µK:stream']: streamType, + pull:: + if self['µK:stream'] == 'immature' then + self.call().pull + else + self, + takeAll:: + local takeRecursive(accumulator, stream) = + local mature = stream.pull, + if mature['µK:stream'] == 'empty' then + accumulator + else + 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, + if mature['µK:stream'] == 'empty' then + accumulator + else + takeRecursive(accumulator + [mature.state], mature.next), + takeRecursive([], self), +}; + +local matureStream(state, next) = baseStream('mature') + { + state: state, + next: next, +}; + +local immatureStream(func) = baseStream('immature') + { + call: func, +}; + +local makeGoal(callable) = { + ['µK:goal']: callable, + pursue(state):: self['µK:goal'](state), +}; + +local mplus(stream1, stream2) = + local t1 = stream1['µK:stream'], + if t1 == 'empty' then + immatureStream(function() stream2) + else if t1 == 'immature' then + immatureStream(function() mplus(stream2, stream1.call())) + else if t1 == 'mature' then + immatureStream(function() matureStream(stream1.state, mplus(stream2, stream1.next))) + else + error 'Invalid stream'; + +local bind(stream, goal) = + local t = stream['µK:stream'], + if t == 'empty' then + stream + else if t == 'immature' then + immatureStream(function() bind(stream1.call(), goal)) + else if t == 'mature' then + immatureStream(function() mplus(goal.pursue(stream1.state), bind(stream2, goal))) + else + error 'Invalid stream'; + +{ + 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 + 'goal' + else if std.type(std.get(value, 'µK:stream'), 'string') then + 'stream' + else + t + else + t, + + // state + emptyState: { + variable_count: 0, + substitution: { + walk(var):: + if type(var) == 'variable' then + local bound = std.get(self, var['µK:var'])), + if bound == null then + u + 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), + if t1 == 'variable' && t2 == 'variable' && w1 == w2 then + self + else if t1 == 'variable' then + self.extend(w1, w2) + else if t2 == 'variable' then + self.extend(w2, w1) + else if t1 == 'array' && t2 == 'array' then + if std.length(w1) == std.length(w2) then + if std.length(w1) == 0 then + self + else + local s1 = self.unify(w1[0], w2[0]), + if s1 == null then + null + else + s1.unify(w1[1::], w2[1::]) + else + null + else if t1 == 'object' && t2 == 'object' then + if std.objectFields(w1) == std.objectFields(w2) then + std.foldl( + function(field, prev_subst) + if prev_subst == null then + null + else + prev_subst.unify(w1[field], w2[field]), + std.objectFields(w1), + self + ) + else + null + else if w1 == w2 then + self + else + null, + }, + freshVar:: { + variable: { + ['µK:var']: self.variable_count, + eq(value):: $.eq(self, value), + }, + newState: self + {variable_count: self.variable_count + 1} + }, + }, + + // streams + emptyStream: baseStream('empty'), + + unitStream(state): matureStream(state, emptyStream), + + // goal constructors + eq(value1, value2): makeGoal(function(state) + local newState = state.unify(value1, value2), + if newState == null then + emptyStream + else + unitStream(newState) + ), + conj(goal1, goal2): makeGoal(function(state) + $.bind(goal1.pursue(state), goal2) + ), + 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]) + else + error 'Invalid goal' + ) + else + error 'Invalid goal' + ).pursue(fresh.newState) + ), +} +// vim: sts=2 ts=2 sw=2 et