Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
270 lines (211 sloc) 7.88 KB
private
import Extend
open Extend
open Parse
open Lex
in
# TODO: maybe split this up into multiple modules?
fun askExt(ext) = Env.get@(@ext, ask)
fun nextIn(ext) =
bind extVal = askExt(ext)
in tryOneMaybe(\(t) Hash.lookup(t, extVal))
# term constructors
# terms are either Vars, lists, or uninterpreted atoms
tag Var(name)
# type Term = Var | (Term . Term) | anything else
# type Stream = () | (State . Stream) | () -> Stream
# type State = {db = DB, sub = Subst}
# type Subst = {Var: Term}
# type DB = {Symbol: [Term] -> Goal}
# type Goal = State -> Stream
# type Renaming = {Symbol: Symbol}
# microKanren implementation
fun ext(x,v,s) = Hash.put(x,v,s)
fun walk(Var(i), s) = (case Hash.lookup(i, s)
| None -> Var(i)
| Just(t) -> walk(t,s))
| walk(x, _) = x
# unify : Term, Term, Subst -> Maybe Subst
# TODO: more powerful circularity check?
fun unify(u,v,s) =
let fun unif(Var(x), Var(y)) = if x == y then s else ext(x, Var(y), s)
| unif(Var(x), t) = ext(x, t, s)
| unif(t, Var(x)) = ext(x, t, s)
| unif([a, ..as], [b, ..bs]) =
(case unify(a,b,s)
| None -> None
| s -> unify(as,bs,s))
| unif(x,y) = if x == y then s else None
in unif(walk(u,s), walk(v,s))
fun eq(u,v) = \(st) case unify(u, v, st.sub)
| None -> []
| s -> [st with {sub = s}]
fun freshly(f) = f(Var(gensym()))
fun mplus([], y) = y
| mplus([x, ..xs], y) = [x, ..mplus(xs,y)]
| mplus(f, y) = \() mplus(y, f())
fun mbind([], g) = []
| mbind([x, ..xs], g) = mplus(g(x), mbind(xs, g))
| mbind(f, g) = \() mbind(f(), g)
val no = \(st) [] # failing goal, identity of disj
val ok = \(st) [st] # succeeding goal, identity of conj
fun disj(g1, g2) = \(st) mplus(g1(st), g2(st))
fun conj(g1, g2) = \(st) mbind(g1(st), g2)
# Some utilities
# TODO: Reifies a term in a substitution
# fun reify(x, s) =
# case x
# | Lit(x) -> AST.exprLit(x)
# | Var(x) ->
# Compiling terms to expressions which produce those terms, with fresh
# variables.
# uniqTerm : Term, Renaming -> (Expr Term, Renaming)
fun uniqTerm(Var(n), d) =
(case Hash.lookup(n, d)
| Just(id) -> [AST.exprVar(AST.varLocal(id)), d]
| None -> let val id = AST.mkId(n)
in [AST.exprVar(AST.varLocal(id)), Hash.put(n, id, d)])
| uniqTerm([a, ..as], d) =
let val [a, d] = uniqTerm(a, d)
val [as, d] = uniqTerm(as, d)
in [`e([~a, .. ~as]), d]
| uniqTerm(x, d) = [`e(`!e(~x)), d]
# uniqTerms : [Term], Renaming -> (Expr [Term], Renaming)
fun uniqTerms(l,d) =
let fun f(x, [xs, d]) = let val [x,d] = uniqTerm(x, d)
in [`e([~x, .. ~xs]), d]
in List.foldr(f, [`e([]),d], l)
# Parsing Kanren.
extension Terms({}, Hash.union)
extension Goals({}, Hash.union)
extension InfixGoals({}, Hash.union)
# upper-case vars, like in prolog
val pVar = Quasi.pure@(Var@(capsId))
# should we really parse single atoms "y" as calls "y()"?
rec val pTerms = eta listishQ(pTerm)
and val pCall = List.cons^ @(Quasi.pure@(varId), option(^[], parens(pTerms)))
and val pTerm = choice(
, join(nextIn(Terms))
, pCall, pVar
, Quasi.pure@(literal)
, keysym("~") >> unquoExpr )
extend Ext.QuoteForms = { TID("term"): pTerm }
# NB. the vars we get from parsing are NOT the vars we use in unify, etc.
# need to uniqify them first.
# recall type Goal = State -> Stream
# prefixGoal : Parse (Q (Renaming -> (Expr Goal, Renaming)))
val prefixGoal =
# app : Sym, [Term] -> (Renaming -> (Expr Goal, Renaming))
let fun app(id, terms) = \(d)
let val [termsE, d] = uniqTerms(terms, d)
fun g(terms) = \(st) Hash.get(id, st.db)(terms)(st)
in [`e(`!e(~g)(~termsE)), d]
fun eqify(t1, t2) = \(d)
let val [t1, d] = uniqTerm(t1, d)
val [t2, d] = uniqTerm(t2, d)
in [`e(`!e(~eq)(~t1, ~t2)), d]
in choice( app^ @(Quasi.pure@(try(anyId <* lparen)), pTerms <* rparen)
, eqify^ @ (pTerm, equals >> pTerm) )
# infixGoal : Int, Q (Renaming -> (Expr Goal, Renaming))
# -> Parse (Q (Renaming -> (Expr Goal, Renaming)))
fun infixGoal(prec, leftExpr) =
option(leftExpr,
bind infixes = askExt(InfixGoals)
in bind ext = tryOneMaybe(\(t) maybeFilter(Hash.lookup(t, infixes),
\(x) prec <= x.precedence))
in bind r = ext.parse(leftExpr)
in infixGoal(prec, r))
rec fun goalAt(prec) = bind g = prefixGoal in infixGoal(prec, g)
# pGoal : Parse (Q (Renaming -> (Expr Goal, Renaming)))
val pGoal = goalAt(0)
fun goalInfix(prec,assoc,make) =
let fun liftMake(a,b) = \(d) let val [a,d] = a(d)
val [b,d] = b(d)
in [make(a,b),d]
in infix(goalAt)(prec,assoc,liftMake^)
extend InfixGoals =
{ TSYM(","): goalInfix(1, R, \(x,y) `e(conj(~x, ~y)))
, TSYM(";"): goalInfix(0, R, \(x,y) `e(disj(~x, ~y))) }
extend Ext.QuoteForms = { TID("goal"): pGoal }
val dbEmpty = {}
fun dbSingle(n,f) = {n: f}
fun dbJoin(x,y) = Hash.union(x, y, \ (_,l,r) \ (args) disj(l(args), r(args)))
# Parses a statement to a DB
# TODO: symbol should be Q'd and unquotable
# do we really want the argument list to be optional?
# pHead : Parse (Symbol, Q [Term])
val pHead = List.list@(varId, option(^[], parens(pTerms)))
# delays a goal?
fun zzz(f) = \(st) \() f(st)
# freshVars : Renaming -> Decl
fun freshVars(renaming) =
let fun declify(id) = `d(val ~(AST.patVar(id)) = Var(gensym(`!e(~id))))
in AST.declBegin(List.map(declify, Hash.values(renaming)))
# pStmt : Parse (Q DB)
val pStmt =
let fun rule(params, body) =
let val [params, d] = uniqTerms(params, {})
val [body, d] = body(d)
val argsym = AST.mkTemp("args")
val argexp = AST.exprVar(AST.varLocal(argsym))
val decls = freshVars(d)
in AST.exprLambda([AST.patVar(argsym)],
`e(let ~decls in conj(eq(~params, ~argexp), zzz(~body))))
# in `e(\(argsym) conj(eq(~params, args), ~body))
#in \(args) conj(eq(params, args), body)
fun single(n,r) = `e({`!e(~n): ~r})
in bind [name, params] = pHead
in bind body = option(^ \(d) [`e(ok), d], keysym(":-") >> pGoal)
in dot >> @single^(^name, rule^(params, body))
# NB. foldl reverses argument order.
val pStmts = let fun f(x,y) = `e(dbJoin(~y, ~x))
in List.foldl@(@(f^), @ ^ `e({}), many(pStmt))
extend Ext.QuoteForms = { TID("stmt"): pStmt
, TID("kanren"): pStmts }
# Embedding Kanren in Moxy
extend Ext.Exprs =
{ TID("kanren"): braces(pStmts) }
# Queries
val pQuery =
let fun make(f) =
let val [goal, d] = f({})
val decls = freshVars(d)
in `e(let ~decls in ~goal)
in make^ @(pGoal)
extend Ext.QuoteForms = { TID("query"): pQuery }
# List terms
# TODO: _real_ list terms, not just lists of things.
# in particular, [X,Y|Z] patterns.
extend Terms = { TLBRACK: pTerms <* rbrack }
# TODO: more things.
fun query(db, goal) = goal({db = db, sub = {}})
# forces the head of a stream
fun force([]) = []
| force([x, ..ys]) = [x, ..ys]
| force(f) = force(f())
fun take(0, _) = []
| take(n, []) = []
| take(n, [x, ..xs]) = [x, ..(take(n-1, xs))]
| take(n, f) = take(n, force(f))
fun head(x) = fst(take(1,x))
# A test
val db = kanren {
yes.
no :- 2 = 3.
eq(X,Y) :- X = Y.
foo(X,Y) :- eq(X,Y).
foo(X,Y,Z) :- eq(Y,X), eq(Z,X).
append(nil(), X, X).
append(cons(X,Xs), Ys, cons(X,XYs)) :- append(Xs, Ys, XYs).
}
fun app(a,b,c) =
disj(conj(eq(a,[]), eq(b,c)),
let val [x,xs,cs] = List.map(\(x) Var(gensym(x)), ["x", "xs", "cs"])
in conj(eq(a, [x, ..xs]),
conj(eq(c, [x, ..cs]),
\(st) app(xs, b, cs)(st))))
fun reify(s, Var(i)) = (case Hash.lookup(i, s)
| None -> Var(i)
| Just(t) -> reify(s, t))
| reify(s, [x, ..xs]) = [reify(s,x), ..reify(s, xs)]
| reify(s, x) = x