Last active
December 23, 2015 12:59
-
-
Save timyates/6639004 to your computer and use it in GitHub Desktop.
A miniKanren in Groovy blatantly copied from https://github.com/funjs/friebyrd
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import groovy.transform.* | |
////////////////////////////////////// | |
// Testing | |
////////////////////////////////////// | |
new MiniKanren().with { | |
// for a given 'q' and 'r' | |
def (q,r) = [ lvar( 'q' ), lvar( 'r' ) ] | |
def result = run( | |
goal( | |
[ q, r ], // q == r | |
[ true, q ] // and q == true | |
) | |
).head() | |
// Then q should be true | |
assert result.bind[ q ] == true | |
// and so should r | |
assert result.bind[ r ] == true | |
} | |
////////////////////////////////////// | |
// Implementation | |
////////////////////////////////////// | |
class MiniKanren { | |
@Immutable | |
static class Lvar { | |
String name | |
} | |
@Immutable | |
static class Bindings { | |
Map bind | |
Bindings extend( lvar, value ) { | |
return new Bindings( bind + [ (lvar): value ] ) | |
} | |
boolean has( lvar ) { | |
return bind.containsKey( lvar ) | |
} | |
def lookup( lvar ) { | |
if( !( lvar instanceof Lvar ) ) { | |
lvar | |
} | |
else if( has( lvar ) ) { | |
lookup( bind[ lvar ] ) | |
} | |
else { | |
lvar | |
} | |
} | |
} | |
def lvar = { name -> new Lvar( name ) } | |
def isLvar = { v -> v instanceof Lvar } | |
def succeed = { result -> [ result ] } | |
def fail = { [] } | |
def disjunction = { l, r -> | |
r.inject( l.inject( [] ) { p, w -> p + w } ) { o, v -> o + v } | |
} | |
def conjunction = { l, r -> | |
{ x -> | |
l( x ).collect { r( it ) } | |
} | |
} | |
def disj = { | |
if( it == null || it.size() == 0 ) { | |
fail | |
} | |
else { | |
disjunction( it.head(), disj( it.tail() ) ) | |
} | |
} | |
def conj = { | |
if( it == null || it.size() == 0 ) { | |
succeed | |
} | |
else if( it.size() == 1 ) { | |
it.head() | |
} | |
else { | |
conjunction( it.head(), { s -> | |
conj( it.tail() )( s ) | |
} ) | |
} | |
} | |
def ignorance = new Bindings( [:] ) | |
def find = { v, bindings -> | |
def lvar = bindings.lookup( v ) | |
if( lvar instanceof Lvar ) { | |
return lvar | |
} | |
if( lvar instanceof List ) { | |
if( lvar.size() == 0 ) { | |
return lvar | |
} | |
return cons( find( lvar.head(), bindings ), find( lvar.tail(), bindings ) ) | |
} | |
return lvar | |
} | |
def unify = { l, r, bindings -> | |
def t1 = bindings.lookup( l ) | |
def t2 = bindings.lookup( r ) | |
if( t1 == t2 ) { | |
return bindings | |
} | |
if( isLvar( t1 ) ) { | |
return bindings.extend( t1, t2 ) | |
} | |
if( isLvar( t2 ) ) { | |
return bindings.extend( t2, t1 ) | |
} | |
if( t1 instanceof List && t2 instanceof List ) { | |
bindings = unify( t1.head(), t2.head(), bindings ) | |
return bindings != null ? | |
unify( t1.tail(), t2.tail(), bindings ) : | |
bindings | |
} | |
return null | |
} | |
def goal = { l, r -> | |
{ bindings -> | |
def result = unify( l, r, bindings ) | |
if( result != null ) { | |
return succeed( result ) | |
} | |
return fail( bindings ) | |
} | |
} | |
def run = { goal -> | |
goal( ignorance ) | |
} | |
def choice = { v, list -> | |
if( list == null || list.size() == 0 ) { | |
return fail | |
} | |
disj( goal( v, list.head() ), choice( v, list.tail() ) ) | |
} | |
def membero = choice | |
def commono = { l, r -> | |
def x = lvar( 'x' ) | |
conj( choice( x, l ), choice( x, r ) ) | |
} | |
def conso = { a, b, list -> | |
goal( cons( a, b ), list ) | |
} | |
def joino = { a, b, list -> | |
goal( [ a, b ], list ) | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment