Created
October 12, 2020 22:10
-
-
Save aphyr/4d41e7655b10a68e753f729bdc1c5a6d to your computer and use it in GitHub Desktop.
Minikanren in Lisp in Prolog
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
| :- use_module(library(pairs)). | |
| :- use_module(library(reif)). | |
| not_in_list(K, L) :- | |
| if_((L = []), | |
| true, | |
| ([X | More] = L, | |
| dif(K, X), | |
| not_in_list(K, More))). | |
| not_in_env(K, Env) :- | |
| /* \+ get_dict(K, Env, _) */ | |
| dict_pairs(Env, _, Pairs), | |
| pairs_keys(Pairs, Keys), | |
| not_in_list(K, Keys). | |
| /* Binds a single binding form to a value. Symbols are assigned directly. */ | |
| bind(K, V, Env, Env2) :- | |
| atom(K), | |
| Env2 = Env.put(K, V). | |
| /* Vectors are recursively destructured. &(V) denotes varargs. */ | |
| bind([], _, Env, Env). | |
| bind([K|Ks], Vs, Env, Env3) :- | |
| /* Varargs */ | |
| (K = &(K2), | |
| bind(K2, Vs, Env, Env3), !) ; | |
| /* Out of values */ | |
| ([] = Vs, | |
| bind(K, nil, Env, Env2), | |
| bind(Ks, [], Env2, Env3)); | |
| /* Standard vector of bindings: bind first and recur */ | |
| ([V1|V1s] = Vs, | |
| bind(K, V1, Env, Env2), | |
| bind(Ks, V1s, Env2, Env3)). | |
| /* Self-evaluating literals */ | |
| eval_lit(Exp, _Env, Exp) :- | |
| Exp = [] ; | |
| Exp = nil ; | |
| Exp = true ; | |
| string(Exp) ; | |
| number(Exp). | |
| /* a bare variable x which is in scope */ | |
| eval_variable(Var, Env, R) :- | |
| atom(Var), | |
| get_dict(Var, Env, R). | |
| /* Evaluates all elements of list */ | |
| eval_each([], _, []). | |
| eval_each(Exp, Env, R) :- | |
| [X | More] = Exp, | |
| [XR | MoreR] = R, | |
| eval_exp(X, Env, XR), | |
| eval_each(More, Env, MoreR). | |
| /* Binds vars to args in env, evaluates body, yielding R. */ | |
| call_closure(Vars, Args, Body, Env, R) :- | |
| bind(Vars, Args, Env, Env2), | |
| eval_exp(Body, Env2, R). | |
| /* [f, a, b] */ | |
| eval_application([Fun | Args], Env, R) :- | |
| dif(Fun, quote), | |
| /* format("Trying to apply ~w to ~w~n", [Fun, Args]), */ | |
| /* Evaluate operator in env, yielding a closure */ | |
| eval_uexp(Fun, Env, λ(Type, Vars, Body, Env2)), | |
| /* format("Evaluated fun.~n", []), */ | |
| /* Depending on the type of the closure... */ | |
| ((Type = lambda, | |
| /* Lambdas evaluate their arguments */ | |
| eval_each(Args, Env, ArgsR), | |
| /* format("args evaluated~n", []), */ | |
| /* And invoke their body with those evaluated args. */ | |
| call_closure(Vars, ArgsR, Body, Env2, R), !) ; | |
| (Type = macro, | |
| /* Macros receive unevaluated arguments, and invoke their body to generate | |
| an expression */ | |
| call_closure(Vars, Args, Body, Env2, Code), | |
| /* Which is then evaluated */ | |
| eval_exp(Code, Env, R))). | |
| /* [lambda [a b] body1 body2] or [macro ...]*/ | |
| eval_lambda([Type, Args | Body], Env, R) :- | |
| /* Must be either macro or lambda, and not shadowed */ | |
| ((Type = lambda, not_in_env(lambda, Env)) ; | |
| (Type = macro, not_in_env(macro, Env))), | |
| /* Construct a closure with the type, argument, body, and env. The | |
| environment includes a `recur` target which is bound to the closure itself. | |
| HOLY SHIT, you can just DO this and Prolog will LET you */ | |
| R = λ(Type, Args, [do | Body], Env.put(recur, R)). | |
| eval_do([do], _Env, nil). | |
| eval_do([do, X], Env, R) :- | |
| eval_exp(X, Env, R). | |
| eval_do([do, X1, X2 | More], Env, R) :- | |
| eval_exp(X1, Env, _), | |
| eval_do([do, X2 | More], Env, R). | |
| /* [let [a val b val] body1 body2 ...] */ | |
| eval_let([let, [] | Body], Env, R) :- | |
| eval_do([do | Body], Env, R). | |
| eval_let([let, [K, V | More] | Body], Env, R) :- | |
| eval_exp(V, Env, VR), | |
| bind(K, VR, Env, Env2), | |
| eval_let([let, More | Body], Env2, R). | |
| /* [cond test branch test branch default] */ | |
| eval_cond([cond], _Env, nil). | |
| eval_cond([cond, Default], Env, R) :- | |
| eval_exp(Default, Env, R). | |
| eval_cond([cond, Test, Branch | More], Env, R) :- | |
| eval_uexp(Test, Env, TestR), | |
| if_((nil = TestR), | |
| eval_cond([cond | More], Env, R), | |
| eval_exp(Branch, Env, R)). | |
| /* [quote x] */ | |
| eval_quote([quote, R], Env, R) :- | |
| /* Ensure quote isn't shadowed */ | |
| not_in_env(quote, Env). | |
| /* M-M-M-METACIRCULARRRRR */ | |
| eval_eval([eval, X], Env, R) :- | |
| eval_exp(X, Env, XR), | |
| eval_exp(XR, Env, R). | |
| /* Matches a typebox */ | |
| is_typed(τ(_,_)). | |
| /* Every compound other than a lambda or typebox is a struct. */ | |
| is_struct(X) :- | |
| compound(X), | |
| compound_name_arity(X, T, _), | |
| dif(T, λ), | |
| dif(T, τ), | |
| dif(T, '[|]'). | |
| /* Relational version */ | |
| is_typed_or_struct(X, R) :- | |
| (is_typed(X) ; is_struct(X)), R = true , ! ; | |
| R = false. | |
| type(X, R) :- | |
| (atomic(X), | |
| ([] = X , R = list) ; | |
| (atom(X), R = atom) ; | |
| (number(X), R = number) ; | |
| (string(X), R = string)), ! ; | |
| (compound(X), | |
| ((functor(X, '[|]', _), R = list), ! ; | |
| (compound_name_arity(X, λ, _), R = function), ! ; | |
| (compound_name_arguments(X, τ, [Type, _]), R = Type), ! ; | |
| (compound_name_arity(X, Type, _), R = Type))). | |
| /* True if X is of type Type; explodes with an error otherwise. */ | |
| typecheck(Type, X) :- | |
| type(X, Type), ! ; | |
| (format("Type error: expected ~p, received ~p~n", | |
| [Type, X]), | |
| false). | |
| /* Unwraps type boxes */ | |
| untyped(X, R) :- | |
| (X = τ(_, Value), | |
| R = Value) ; | |
| (dif(X, τ(_, _)), | |
| R = X). | |
| /* With one arg, type gets the type of an expression. */ | |
| eval_type([type, X], Env, R) :- | |
| not_in_env(type, Env), | |
| eval_exp(X, Env, XR), | |
| type(XR, R). | |
| /* This is the worst hack. (type cat x) serves both as a type-returning | |
| * introspection, and also as a type assertion, both at runtime. If x is an | |
| * untyped object, the type call succeeds and constructs a transparent type | |
| * wrapper typed(name, X). This wrapper is transparent in that it is unwrapped | |
| * within eval_exp--except, of course, for calls to eval_type!--most language | |
| * features don't see the type-box's existence. | |
| * | |
| * When calling (type cat x) with a type-boxed x, this serves as a type | |
| * *assertion*: x is returned unchanged iff its type is cat; otherwise, this | |
| * explodes with a type error. */ | |
| eval_type([type, Name, X], Env, R) :- | |
| not_in_env(type, Env), | |
| eval_exp(X, Env, XR), | |
| /* Type boxes and structs must match type Name; otherwise, wrap them in a | |
| * type box. */ | |
| is_typed_or_struct(XR, Typed), | |
| if_(Typed = true, | |
| (typecheck(Name, XR), | |
| R = XR), | |
| /* Construct type box around untyped value. */ | |
| (R = τ(Name, XR))). | |
| /* An explicit typecheck: like type, but does not promote untyped values to | |
| * typed ones. Note that you can [check list []] transparently, but [type list []] introduces a type wrapper. */ | |
| eval_type([check, Name, X], Env, R) :- | |
| not_in_env(check, Env), | |
| eval_exp(X, Env, R), | |
| typecheck(Name, R). | |
| /* Used to unbox typed objects, allowing you to write map, filter, etc. lmao, | |
| * not even 2 hours and already I need type polymorphism. */ | |
| eval_type([untype, X], Env, R) :- | |
| not_in_env(untype, Env), | |
| eval_exp(X, Env, XR), | |
| untyped(XR, R). | |
| /* [list x y] */ | |
| eval_list([list | Args], Env, R) :- | |
| /* Ensure it's not shadowed */ | |
| not_in_env(list, Env), | |
| /* And evaluate */ | |
| eval_each(Args, Env, R). | |
| list_sense(X, R) :- | |
| if_((nil = X), R = [], R = X). | |
| eval_first([first, List], Env, R) :- | |
| not_in_env(first, Env), | |
| eval_uexp(List, Env, ListR), | |
| if_(([] = ListR), | |
| R = nil, | |
| [R|_] = ListR). | |
| eval_rest([rest, List], Env, R) :- | |
| not_in_env(rest, Env), | |
| eval_uexp(List, Env, ListR), | |
| ((ListR = [], R = nil) ; | |
| (ListR = [_|R])). | |
| eval_cons([cons, Head, Tail], Env, R) :- | |
| not_in_env(cons, Env), | |
| eval_exp(Head, Env, HeadR), | |
| eval_exp(Tail, Env, TailR), | |
| list_sense(TailR, TailL), | |
| R = [HeadR | TailL]. | |
| eval_eq([eq, A, B], Env, R) :- | |
| not_in_env(eq, Env), | |
| eval_exp(A, Env, ARes), | |
| eval_exp(B, Env, BRes), | |
| if_((ARes = BRes), R = true, R = nil). | |
| eval_plus([plus, A, B], Env, R) :- | |
| eval_uexp(A, Env, AR), | |
| eval_uexp(B, Env, BR), | |
| R is AR + BR. | |
| prn_helper([]) :- | |
| format("~n"). | |
| prn_helper([X | Xs]) :- | |
| format("~p ", [X]), | |
| prn_helper(Xs). | |
| eval_prn([prn | Args], Env, nil) :- | |
| not_in_env(prn, Env), | |
| eval_each(Args, Env, ArgsR), | |
| prn_helper(ArgsR). | |
| /* We use functors for structs */ | |
| eval_struct([struct, Type | Fields], Env, R) :- | |
| not_in_env(struct, Env), | |
| eval_each(Fields, Env, FieldsR), | |
| compound_name_arguments(R, Type, FieldsR). | |
| eval_struct([destruct, Type, Struct], Env, R) :- | |
| not_in_env(destruct, Env), | |
| eval_uexp(Struct, Env, StructR), | |
| ((atomic(StructR), | |
| format("Can't destruct atom ~w~n", [StructR]), | |
| false) ; | |
| (compound(StructR), | |
| compound_name_arguments(StructR, Type, R))). | |
| eval_gensym([gensym, Prefix], _Env, R) :- | |
| atom_concat(Prefix, '__auto__', Sym), | |
| gensym(Sym, R). | |
| /* Symbol concatenation */ | |
| eval_symcat([symcat, A, B], Env, R) :- | |
| eval_exp(A, Env, AR), | |
| eval_exp(B, Env, BR), | |
| atom_concat(AR, BR, R). | |
| eval_env(env, Env, Env) :- | |
| not_in_env(env, Env). | |
| eval_exp(Exp, Env, R) :- | |
| /* format('eval ~w~n', [Exp]), */ | |
| eval_quote(Exp, Env, R), ! ; | |
| eval_lambda(Exp, Env, R), ! ; | |
| eval_do(Exp, Env, R), ! ; | |
| eval_let(Exp, Env, R), ! ; | |
| eval_cond(Exp, Env, R), ! ; | |
| eval_eq(Exp, Env, R), ! ; | |
| eval_list(Exp, Env, R), ! ; | |
| eval_cons(Exp, Env, R), ! ; | |
| eval_first(Exp, Env, R), ! ; | |
| eval_rest(Exp, Env, R), ! ; | |
| eval_plus(Exp, Env, R), ! ; | |
| eval_struct(Exp, Env, R), ! ; | |
| eval_prn(Exp, Env, R), ! ; | |
| eval_env(Exp, Env, R), ! ; | |
| eval_gensym(Exp, Env, R), ! ; | |
| eval_symcat(Exp, Env, R), ! ; | |
| eval_type(Exp, Env, R), ! ; | |
| eval_eval(Exp, Env, R), ! ; | |
| eval_lit(Exp, Env, R), ! ; | |
| eval_variable(Exp, Env, R), ! ; | |
| eval_application(Exp, Env, R), ! ; | |
| (format('unable to eval ~p~n', [Exp]), | |
| false). | |
| /* Like eval_exp, but unwraps type boxes. This is where we ground out for | |
| * prolog interop */ | |
| eval_uexp(Exp, Env, R) :- | |
| eval_exp(Exp, Env, Typed), | |
| untyped(Typed, R). | |
| prologue([ | |
| /* Booleans ************************************************************/ | |
| and, [macro, [a, b], | |
| [list, [quote, cond], a, b]], | |
| or, [macro, [a, b], | |
| [let, [a_, [gensym, a]], | |
| [list, [quote, let], | |
| [list, a_, a], | |
| [cond, a_, a_, b]]]], | |
| not, [lambda, [x], [cond, x, nil, true]], | |
| /* Predicates ********************************************************/ | |
| is_null, [lambda, [x], | |
| [let, [x, [untype, x]], | |
| [or, [eq, x, []], | |
| [eq, x, nil]]]], | |
| is_empty, [lambda, [coll], [eq, [], [untype, coll]]], | |
| is_list, [lambda, [x], | |
| [eq, [type, [untype, x]], [quote, list]]], | |
| is_pair, [lambda, [x], | |
| [and, [not, [is_empty, x]], | |
| [is_list, x]]], | |
| is_fn, [lambda, [x], | |
| [eq, [type, [untype, x]], [quote, function]]], | |
| /* Basic sequence operations, polymorphic over all types. */ | |
| second, [lambda, [coll], [first, [rest, coll]]], | |
| third, [lambda, [coll], [first, [rest, [rest, coll]]]], | |
| count, [lambda, [coll], | |
| [cond, [is_empty, coll], | |
| 0, | |
| [plus, 1, [recur, [rest, coll]]]]], | |
| map, [lambda, [f, coll], | |
| [cond, [is_empty, coll], | |
| [], | |
| [cons, [f, [first, coll]], | |
| [recur, f, [rest, coll]]]]], | |
| filter, [lambda, [f, coll], | |
| [cond, [is_empty, coll], | |
| [], | |
| [let, [x, [first, coll], | |
| xs, [rest, coll]], | |
| [cond, [f, x], | |
| [cons, x, [recur, f, xs]], | |
| [recur, f, xs]]]]], | |
| fold, [lambda, [f, init, coll], | |
| [cond, [is_empty, coll], init, | |
| [recur, f, [f, init, [first, coll]], [rest, coll]]]], | |
| rev, [lambda, [coll], | |
| [fold, [lambda, [list, elem], [cons, elem, list]], [], coll]], | |
| concat, [lambda, [as, bs], | |
| [fold, [lambda, [res, a], | |
| [cons, a, res]], | |
| bs, | |
| [rev, as]]], | |
| /* Control flow *****************************************************/ | |
| /* Passes through nils, typechecks otherwise. */ | |
| check_option, [macro, [type, expr], | |
| [let, [res_, [gensym, res]], | |
| [list, [quote, let], [list, res_, expr], | |
| [list, [quote, cond], [list, [quote, eq], nil, res_], | |
| nil, | |
| [list, [quote, check], type, res_]]]]], | |
| assert, [macro, [expr, message], | |
| [list, [quote, cond], | |
| expr, | |
| true, | |
| [list, [quote, do], | |
| [list, [quote, prn], "Assert failed:", | |
| [list, [quote, quote], expr], | |
| message], | |
| [quote, throw]]]], | |
| /* Apply a function to every node of a tree (list), preorder application, | |
| * recursively */ | |
| treemap, [lambda, [f, x], | |
| [let, [treemap, recur, | |
| x2, [f, x]], | |
| [cond, [is_pair, x2], | |
| [cons, [f, [first, x2]], [recur, f, [rest, x2]]], | |
| x2]]], | |
| /* Utilities ***********************************************************/ | |
| /* Syntax-quote takes an expression and quotes it, except for [unquote, x] | |
| * forms, which unquotes a single term. */ | |
| syntax_quote_fn, [lambda, [expr], | |
| [let, [q, [quote, quote], | |
| sq, recur], | |
| [cond, [is_empty, expr], expr, | |
| [is_list, expr], | |
| [let, [f, [first, expr]], | |
| [cond, /* Unquote means *don't* descend into this term. */ | |
| [eq, f, [quote, unquote]], | |
| [second, expr], | |
| /* Otherwise, recur into term and build up a list expr. */ | |
| [cons, [quote, list], | |
| [map, sq, expr]]]], | |
| /* Non-list terminals are all quoted. */ | |
| [list, q, expr]]]], | |
| syntax_quote, [macro, [expr], [syntax_quote_fn, expr]], | |
| syntax_quote_test, [macro, [x], | |
| [syntax_quote, [prn, [list, 1], [unquote, x]]]], | |
| /* Rewrites closures to be more readable. */ | |
| unfn, [lambda, [x], | |
| [first, | |
| [treemap, [lambda, [x], | |
| /* Print functions without envs */ | |
| [cond, [is_fn, x], | |
| [let, [[type, args, [do, &(body)]], | |
| [destruct, λ, x]], | |
| [struct, λ, args, body]], | |
| x]], | |
| [list, x]]]], | |
| /* MICROKANREN ************************************************************/ | |
| /* Logic vars are their own struct type. We do this for safety--it's too easy | |
| * to accidentally destructure/cons/etc lvars otherwise. */ | |
| lvar, [lambda, [num], [struct, lvar, num]], | |
| is_lvar, [lambda, [x], [eq, [quote, lvar], [type, x]]], | |
| lvar_num, [lambda, [x], [first, [destruct, foo, x]]], | |
| /* We represent a binding as a struct as well. */ | |
| binding, [lambda, [var, val], | |
| [struct, binding, var, val]], | |
| is_binding, [lambda, [x], [eq, [type, x], [quote, binding]]], | |
| bvar, [lambda, [b], [first, [destruct, binding, b]]], | |
| bval, [lambda, [b], [second, [destruct, binding, b]]], | |
| /* A substitution map is a list of bindings */ | |
| empty_subs, [type, subs, []], | |
| /* Returns the binding of lvar num in substitution subs */ | |
| lvar_binding, [lambda, [num, subs], | |
| [first, [filter, [lambda, [x], | |
| [eq, num, [first, x]]], | |
| subs]]], | |
| /* A state is a substitution paired with a fresh variable counter. */ | |
| state, [lambda, [subs, counter], | |
| [check, subs, subs], | |
| [struct, state, subs, counter]], | |
| is_state, [lambda, [x], [eq, [type, x], [quote, state]]], | |
| empty_state, [state, empty_subs, 0], | |
| st_subs, [lambda, [s], [check, subs, [first, [destruct, state, s]]]], | |
| st_counter, [lambda, [s], [second, [destruct, state, s]]], | |
| /* Search for the value of u in a given substitution. */ | |
| walk, [lambda, [u, subs], | |
| [check, subs, subs], | |
| [let, [pr, [and, [is_lvar, u], | |
| [first, [filter, [lambda, [v], | |
| /* u is equal to the binding's lvar */ | |
| [eq, u, [bvar, v]]], | |
| subs]]], | |
| res, [cond, pr, | |
| [recur, [bval, pr], subs], | |
| u]], | |
| /* [prn, "walk", u, [quote, '->'], res, "in", subs], */ | |
| res]], | |
| /* Adds a binding of x to v to the given substitution. */ | |
| ext_s, [lambda, [x, v, subs], | |
| [check, subs, subs], | |
| [type, subs, [cons, [binding, x, v], subs]]], | |
| /* Unifies u with v in a substitution */ | |
| unify, [lambda, [u, v, subs], | |
| [check, subs, subs], | |
| /* Look up u and v in the substitution map */ | |
| [check_option, subs, | |
| [let, [u, [walk, u, subs], | |
| v, [walk, v, subs]], | |
| /* If both are equal, return subs unchanged. This covers both normal | |
| * values and lvars. */ | |
| [cond, [eq, u, v], subs, | |
| /* If we have one lvar, and something else (either a value or a | |
| * different lvar) extend the substitution with that | |
| * association. */ | |
| [is_lvar, u], [ext_s, u, v, subs], | |
| [is_lvar, v], [ext_s, v, u, subs], | |
| /* If both are bindings, unify their vars and vals. The Scheme | |
| * implementation gets around this by encoding bindings as | |
| * pairs. TODO: when we're done being type-safe, go back to | |
| * that. */ | |
| [and, [is_binding, u], [is_binding, v]], | |
| [let, [subs, [recur, [bvar, u], [bvar, v], subs]], | |
| [and, subs, [recur, [bval, u], [bval, v]], subs]], | |
| /* We unify lists recursively. Note that this works for improper | |
| * lists too! */ | |
| [and, [is_pair, u], [is_pair, v]], | |
| [let, [subs, [recur, [first, u], [first, v], subs]], | |
| [and, subs, [recur, [rest, u], [rest, v], subs]]]]]]], | |
| /* M'zero, the empty stream */ | |
| mzero, [type, stream, []], | |
| unit, [lambda, [state], | |
| [assert, [is_state, state], "unit"], | |
| [type, stream, [cons, state, mzero]]], | |
| /* A goal constructor which asserts u and v are equal */ | |
| eql, [lambda, [u, v], | |
| [type, goal, | |
| [lambda, [st], | |
| [assert, [is_state, st], "eql"], | |
| [check, stream, | |
| [let, [subs, [unify, u, v, [st_subs, st]]], | |
| [cond, subs, | |
| [unit, [state, subs, [st_counter, st]]], | |
| mzero]]]]]], | |
| ≡, eql, | |
| /* A goal which introduces a new logical variable. Takes a function [f, lvar] | |
| which yields a goal, and constructs a goal using it. The constructed goal | |
| takes a state sc, derives a goal with a fresh logic variable in that state, | |
| and passes the (evolved) state to the goal that f yields. */ | |
| call_fresh, [lambda, [f], | |
| [type, goal, | |
| [lambda, [st], | |
| [assert, [is_state, st], "call_fresh"], | |
| /* Construct a new logic variable and call f with it, yielding a goal | |
| * function. That goal function gets called with our state, evolved to | |
| * account for the new variable. */ | |
| [check, stream, | |
| [let, [c, [st_counter, st]], | |
| [[check, goal, [f, [lvar, c]]], | |
| [state, [st_subs, st], [plus, 1, c]]]]]]]], | |
| /* Merges two alternative streams (i.e. representing the two forks of a | |
| * disjunction) together. */ | |
| mplus, [lambda, [a, b], | |
| [check, stream, a], | |
| [check, stream, b], | |
| [check, stream, | |
| [let, [mplus, recur], | |
| [cond, /* When one stream is exhausted, yield the other. */ | |
| [is_null, a], b, | |
| /* A fn is a lazy stream; if given one, we yield our own lazy | |
| * stream which, when evaluated, tries the opposite order: b, | |
| * then the concrete stream [a]. Flipping a and b is what lets | |
| * us trade off between streams, ensuring no single fork | |
| * dominates the search. */ | |
| [is_fn, a], [type, stream, [lambda, [], [mplus, b, [a]]]], | |
| /* a must be a concrete non-empty list. We yield its first | |
| * state, followed by the disjunction of later states of a with | |
| * b. */ | |
| [type, stream, | |
| [cons, [first, a], [mplus, [rest, a], b]]]]]]], | |
| /* Bind applies a goal (a function of states to streams) over a stream. */ | |
| bind, [lambda, [stream, goal], | |
| [check, stream, stream], | |
| [check, goal, goal], | |
| [check, stream, | |
| [let, [bind, recur], | |
| [cond, /* If the stream is empty, we return the empty stream. */ | |
| [is_null, stream], mzero, | |
| /* If the stream is lazy, we construct a lazy stream. */ | |
| [is_fn, stream], [type, stream, | |
| [lambda, [], [bind, [stream], goal]]], | |
| /* Otherwise, the stream is a concrete, non-empty stream. We | |
| * have two choices now: either apply the goal to the first | |
| * thing in the stream, or mapping the goal over the rest of the | |
| * stream. We express these two options via mplus! */ | |
| [mplus, [goal, [first, stream]], | |
| [bind, [type, stream, [rest, stream]], goal]]]]]], | |
| /* Logical disjunction of two goals. */ | |
| disj, [lambda, [g1, g2], | |
| [check, goal, g1], | |
| [check, goal, g2], | |
| [type, goal, | |
| [lambda, [state], | |
| [assert, [is_state, state], "disj"], | |
| [check, stream, | |
| [mplus, [g1, state], [g2, state]]]]]], | |
| /* Logical conjunction of two goals */ | |
| conj, [lambda, [g1, g2], | |
| [check, goal, g1], | |
| [check, goal, g2], | |
| [type, goal, | |
| [lambda, [state], | |
| [assert, [is_state, state], "conj"], | |
| /* We apply the first goal to the state, yielding a stream. We then map | |
| * the second goal over that stream, ensuring both goals hold. */ | |
| [check, stream, | |
| [bind, [g1, state], g2]]]]], | |
| /* Basic uKanren examples */ | |
| fives, [call_fresh, [lambda, [x], [≡, x, 5]]], | |
| sixes, [call_fresh, [lambda, [x], [≡, x, 6]]], | |
| either, [call_fresh, [lambda, [x], [disj, [≡, x, 3], | |
| [≡, x, 4]]]], | |
| alts, [conj, [call_fresh, [lambda, [x], [≡, x, 3]]], | |
| /* This is a different logic variable! */ | |
| [call_fresh, [lambda, [x], [disj, [≡, x, 5], [≡, x, 6]]]]], | |
| /* Evals until realized */ | |
| pull, [lambda, [stream], | |
| [check, stream, stream], | |
| [cond, [is_fn, stream], | |
| [recur, [stream]], | |
| stream]], | |
| /* Limited take */ | |
| take, [lambda, [n, stream], | |
| [cond, [eq, 0, n], | |
| [], | |
| [let, [stream, [pull, stream], | |
| state, [first, stream]], | |
| [cond, [is_fn, state], | |
| [recur, n, state], | |
| state, | |
| [do, [assert, [is_state, state], "take"], | |
| [cons, state, [recur, [plus, n, -1], [rest, stream]]]], | |
| /* Out of elements */ | |
| []]]]], | |
| /* A basic function which takes n solutions from the goal on the empty state | |
| * */ | |
| run_raw, [lambda, [n, goal], | |
| [take, n, [goal, empty_state]]], | |
| /* Reifier **************************************************************/ | |
| /* walkr reifies a term by replacing logic variables in it with their | |
| * corresponding values in some substitution. */ | |
| walkr, [lambda, [v, subs], | |
| /* Look up v in subs */ | |
| [let, [v, [walk, v, subs], | |
| /* A little mutually-recursive helper to simplify traversal */ | |
| walkr, recur, | |
| w, [lambda, [v2], [walkr, v2, subs]]], | |
| [cond, /* If we have a logic variable, that's all we can do. */ | |
| [is_lvar, v], v, | |
| /* If we have a binding, walk its var and val, and construct a new | |
| * binding from that. TODO: if we use lists for bindings, this | |
| * goes away too. */ | |
| [is_binding, v], [binding, [w, [bvar, v]], [w, [bval, v]]], | |
| /* Walk lists recursively. */ | |
| [is_pair, v], [cons, [w, [first, v]], | |
| [w, [rest, v]]], | |
| /* A ground term */ | |
| v]]], | |
| /* This is how we construct names for logic variables */ | |
| reify_name, [lambda, [n], | |
| [symcat, [quote, '_'], n]], | |
| /* Reifies a substitution map, by extending subs with extra entries for any | |
| * unknowns in v. */ | |
| reify_s, [lambda, [v, subs], | |
| /* Look up v in subs */ | |
| [let, [v, [walk, v, subs]], | |
| [cond, /* If we have a logic variable, extend the substitution by binding | |
| v to a new logic var named after the size of the substitution. */ | |
| [is_lvar, v], | |
| [let, [n, [reify_name, [count, subs]]], | |
| [ext_s, v, n, subs]], | |
| /* If we have a binding, extend the substitution (recursively) | |
| * with this variable name and value. */ | |
| [is_binding, v], | |
| [recur, [bval, v], [recur, [bvar, v], subs]], | |
| /* Recur through pairs */ | |
| [is_pair, v], | |
| [recur, [rest, v], [recur, [first, v], subs]], | |
| /* Ground out */ | |
| subs]]], | |
| reify_state_first_var, [lambda, [state], | |
| /* [prn], | |
| [prn, "state", state], */ | |
| /* Look up the first logic variable in this state's substitution. */ | |
| [let, [v, [walkr, [lvar, 0], [st_subs, state]]], | |
| /* Then reify the substitution for v, starting with an empty | |
| * substitution, and walk v in *that*. Why? No clue. */ | |
| [prn, "v", v, "subs", [reify_s, v, empty_subs]], | |
| [walkr, v, [reify_s, v, empty_subs]]]], | |
| /* Reifies a state with respect to the first n vars */ | |
| reify_state_vars, [lambda, [num_vars, state], | |
| /* [prn], | |
| [prn, "state", state], */ | |
| [let, [subs, [st_subs, state]], | |
| [[lambda, [n, r], | |
| [cond, [eq, -1, n], | |
| /* Done */ | |
| r, | |
| /* Resolve the nth variable */ | |
| [let, [v, [walkr, [lvar, n], subs]], | |
| /* And resolve that again... */ | |
| [recur, [plus, n, -1], | |
| [cons, [walkr, v, [reify_s, v, empty_subs]], | |
| r]]]]], | |
| /* The first variable to resolve, and the list of our resolutions */ | |
| [plus, num_vars, -1], | |
| []]]], | |
| /* Reifies states with respect to the first n vars. */ | |
| mk_reify, [lambda, [num_vars, states], | |
| [prn], | |
| [prn, "REIFY =============="], | |
| [map, [lambda, [state], | |
| [reify_state_vars, num_vars, state]], | |
| states]], | |
| /* Shortcut for running goals. Takes a number of solutions to find, a list of | |
| * variable names which will be bound in the given goal, and reified when | |
| * returned. */ | |
| run, [macro, [n, vars, &(goals)], | |
| [syntax_quote, | |
| [mk_reify, [unquote, [count, vars]], | |
| [run_raw, [unquote, n], | |
| [unquote, | |
| [cons, [quote, fresh], | |
| [cons, vars, goals]]]]]]], | |
| /* Syntax! **************************************************************/ | |
| /* This defers evaluation of a goal via inverse-eta-delay */ | |
| zzz, [macro, [g], | |
| [let, [state_, [gensym, state]], | |
| [syntax_quote, | |
| [type, goal, | |
| [lambda, [[unquote, state_]], | |
| [assert, [is_state, [unquote, state_]], | |
| [list, "zzz", [unquote, state_]]], | |
| [type, stream, | |
| [lambda, [], | |
| [check, stream, | |
| [[unquote, g], [unquote, state_]]]]]]]]]], | |
| /* conj or disj of multiple goals */ | |
| conjall, [macro, [&(gs)], | |
| [let, [[g, &(gs)], [rev, gs], | |
| code, [fold, [lambda, [form, goal], | |
| [list, [quote, conj], | |
| [list, [quote, zzz], goal], | |
| form]], | |
| /* Infinite loops? */ | |
| [list, [quote, zzz], g], | |
| gs]], | |
| code]], | |
| disjall, [macro, [&(gs)], | |
| [let, [[g, &(gs)], [rev, gs], | |
| code, [fold, [lambda, [form, goal], | |
| [list, [quote, disj], | |
| [list, [quote, zzz], goal], | |
| form]], | |
| g, | |
| gs]], | |
| code]], | |
| /* A disjunction of conjunctions */ | |
| conde, [macro, [&(clauses)], | |
| [let, [code, [cons, [quote, disjall], | |
| [map, [lambda, [goals], | |
| [cons, [quote, conjall], goals]], | |
| clauses]]], | |
| code]], | |
| fresh, [macro, [vars, &(goals)], | |
| [let, [code, [fold, [lambda, [form, var], | |
| /* Wrap in [call_fresh, [lambda, [x], ...]] */ | |
| [list, [quote, call_fresh], | |
| [list, [quote, lambda], | |
| [list, var], | |
| [list, [quote, type], | |
| [quote, goal], | |
| form]]]], | |
| /* Start with conjunction of all goals */ | |
| [cons, [quote, conjall], goals], | |
| [rev, vars]]], | |
| code]], | |
| /* Sequence goals **************************************************** | |
| * | |
| * Adapted from https://github.com/mullr/micrologic/blob/master/src/micro_logic/sequence.clj */ | |
| /* Conso provides an abstraction for (cons head tail) = list. */ | |
| conso, [lambda, [hd, tl, lst], | |
| [eql, [cons, hd, tl], lst]], | |
| /* We can assert things about the first and rest of a list now */ | |
| firsto, [lambda, [head, list], | |
| [fresh, [tail], | |
| [conso, head, tail, list]]], | |
| resto, [lambda, [tail, list], | |
| [fresh, [head], | |
| [conso, head, tail, list]]], | |
| /* Here's sequence append */ | |
| /* From microkanren A Lucid Little Logic Language with a Simple Complete | |
| * Search */ | |
| appendo, [lambda, [as, bs, combined], | |
| [let, [appendo, recur], | |
| [conde, [[eql, [], as], | |
| [eql, bs, combined]], | |
| [[fresh, [head, tail, rec], | |
| /* Pull apart as */ | |
| [conso, head, tail, as], | |
| /* Pull apart combined */ | |
| [conso, head, rec, combined], | |
| /* And we can recur from there */ | |
| [appendo, tail, bs, rec]]]]]], | |
| /* Peano numbers */ | |
| succ, [lambda, [n], [cons, [quote, 'S'], n]], | |
| n0, [list, 0], | |
| n1, [succ, n0], | |
| n2, [succ, n1], | |
| n3, [succ, n2], | |
| /* Coercions to and from normal numbers */ | |
| peano, [lambda, [n], | |
| [cond, [eq, 0, n], | |
| n0, | |
| [succ, [recur, [plus, -1, n]]]]], | |
| unpeano1, [lambda, [n], | |
| [cond, [eq, n, [list, 0]], 0, | |
| [and, [is_pair, n], [eq, [quote, 'S'], [first, n]]], | |
| [let, [m, [recur, [rest, n]]], | |
| [cond, [eq, [type, m], [quote, number]], | |
| [plus, 1, m], | |
| [struct, 'S', m]]], | |
| n]], | |
| unpeano, [lambda, [x], [treemap, unpeano1, x]], | |
| /* Successor and addition relations */ | |
| succo, [lambda, [n, next], [eql, [succ, n], next]], | |
| pluso, [lambda, [a, b, sum], | |
| [let, [pluso, recur], | |
| [conde, [[eql, a, n0], [eql, b, sum]], | |
| [[fresh, [a_, sum_], | |
| [succo, a_, a], | |
| [succo, sum_, sum], | |
| [pluso, a_, b, sum_]]]]]], | |
| lesso, [lambda, [lesser, greater], | |
| [fresh, [n], [pluso, lesser, [succ, n], greater]]], | |
| /* Maximum */ | |
| maxo, [lambda, [a, b, max], | |
| [conde, [[eql, a, b], [eql, max, a]], | |
| [[lesso, a, b], [eql, max, b]], | |
| [[lesso, b, a], [eql, max, a]]]], | |
| /* Ensures a and b are within 1 of each other. */ | |
| approxo, [lambda, [a, b], | |
| [conde, [[eql, a, b]], | |
| [[succo, a, b]], | |
| [[succo, b, a]]]], | |
| /* Construct a leaf node */ | |
| leaf, [lambda, [x], | |
| [list, [quote, l], x]], | |
| /* Construct a branch node with left and right parts */ | |
| branch, [lambda, [left, right], | |
| [list, [quote, b], left, right]], | |
| /* Converts a compact notation [l,r] to explicit leaf/branch */ | |
| tree, [lambda, [t], | |
| [cond, [is_list, t], | |
| [let, [[left, right], t], | |
| [branch, [recur, left], [recur, right]]], | |
| [leaf, t]]], | |
| /* Maps explicit leaf/branch back to compact lists. */ | |
| untree, [lambda, [[type, a, b]], | |
| [cond, [eq, type, [quote, b]], [list, [recur, a], [recur, b]], | |
| [eq, type, [quote, l]], a]], | |
| /* Rotates between two trees: [a, [b, c]] <-> [[a, b], c]*/ | |
| rot_lefto, [lambda, [t1, t2], | |
| [fresh, [a, b, c], | |
| [eql, t1, [branch, a, [branch, b, c]]], | |
| [eql, t2, [branch, [branch, a, b], c]]]], | |
| /* Left and right rotations */ | |
| rot_botho, [lambda, [t1, t2], | |
| [conde, [[rot_lefto, t1, t2]], | |
| [[rot_lefto, t2, t1]]]], | |
| /* All possible rotations of a node at any depth between two trees. */ | |
| roto, [lambda, [t1, t2], | |
| [let, [roto, recur], | |
| /* Rotate this node */ | |
| [conde, [[rot_botho, t1, t2]], | |
| /* Break apart this tree as a branch */ | |
| [[fresh, [t1l, t1r, t2l, t2r], | |
| [eql, t1, [branch, t1l, t1r]], | |
| [eql, t2, [branch, t2l, t2r]], | |
| [conde, | |
| /* And rotate left branch */ | |
| [[eql, t1r, t2r], [roto, t1l, t2l]], | |
| /* Or right branch*/ | |
| [[eql, t1l, t2l], [roto, t1r, t2r]]]]]]]], | |
| /* Any number of rotations at any level */ | |
| rotso, [lambda, [t1, t2], | |
| [let, [rotso, recur], | |
| [conde, [[eql, t1, t2]], | |
| [[fresh, [t], | |
| [roto, t1, t], | |
| [rotso, t, t2]]]]]], | |
| /* Height of a tree */ | |
| heighto, [lambda, [t, h], | |
| [let, [heighto, recur], | |
| [conde, /* Leaf */ | |
| [[fresh, [x], | |
| [eql, t, [leaf, x]], | |
| [eql, h, n0]]], | |
| /* Branch */ | |
| [[fresh, [left, right, left_height, right_height, max_height], | |
| [eql, t, [branch, left, right]], | |
| [heighto, left, left_height], | |
| [heighto, right, right_height], | |
| [maxo, left_height, right_height, max_height], | |
| [succo, max_height, h]]]]]], | |
| /* Balanced tress have approximately equal heights at every level. Oh god, | |
| * this is SO expensive. */ | |
| balancedo, [lambda, [t, h], | |
| [let, [balancedo, recur], | |
| [conde, /* Leaf nodes are trivially balanced */ | |
| [[fresh, [x], [eql, t, [leaf, x]]]], | |
| /* Branch nodes are balanced if their left and right heights are | |
| * approximately equal, and both left and right nodes are | |
| * themselves balanced. */ | |
| [[fresh, [left, right, left_height, right_height], | |
| [eql, t, [branch, left, right]], | |
| [balancedo, left], | |
| [balancedo, right], | |
| [heighto, left, left_height], | |
| [heighto, right, right_height], | |
| [approxo, left_height, right_height]]]]]], | |
| /* Takes any tree and finds an equivalent (via rotation) balanced tree. */ | |
| balanceo, [lambda, [tree, balanced], | |
| [conde, [[rotso, tree, balanced], | |
| [balancedo, balanced]]]] | |
| /* Look up a variable in an association list */ | |
| lookupo, [lambda, [var, env, r], | |
| [let, [lookupo, recur], | |
| [fresh, [k, v, more], | |
| [eql, env, [cons, [cons, k, v], more]], | |
| /* Found it! */ | |
| [conde, [[eql, k, var], | |
| [eql, v, r]], | |
| /* Keep looking */ | |
| [[lookupo, var, more, r]]]]]], | |
| /* How many symbols do you really need */ | |
| symbolo, [lambda, [var], | |
| [conde, [[eql, var, [quote, f]]], | |
| [[eql, var, [quote, x]]]]], | |
| evalo, [lambda, [exp, env, r], | |
| [let, [evalo, recur], | |
| [conde, | |
| /* Application */ | |
| [[fresh, [f, arg, var, body, env2, argr], | |
| /* Break up [f arg] */ | |
| [eql, exp, [list, f, arg]], | |
| /* Evaluate f to a closure */ | |
| [evalo, f, env, [list, [quote, λ], var, body, env2]], | |
| /* And eval arg */ | |
| [evalo, arg, env, argr], | |
| /* Then evaluate body with arg bound */ | |
| [evalo, body, [cons, [cons, var, argr], env2], r]]], | |
| /* Lambda */ | |
| [[fresh, [var, body], | |
| [eql, exp, [list, [quote, lambda], [list, var], body]], | |
| [eql, r, [list, [quote, λ], var, body, env]]]], | |
| /* A symbol */ | |
| [[symbolo, exp], | |
| [lookupo, exp, env, r]]]]] | |
| ]). | |
| demos(conde, [run, 2, [q,w,x,y], | |
| [conde, | |
| [[≡, [list, x, w, x], q], | |
| [≡, y, w]], | |
| [[≡, [list, w, x, w], q], | |
| [≡, y, w]]]]). | |
| demos(conde_anon, [run, 2, [q], | |
| [fresh, [w, x, y], | |
| [conde, | |
| [[≡, [list, x, w, x], q], | |
| [≡, y, w]], | |
| [[≡, [list, w, x, w], q], | |
| [≡, y, w]]]]]). | |
| /* Define a relation which reverses a list. */ | |
| demos(nrev, [let, [nrev, [lambda, [l1, l2], | |
| [lambda, [sc], | |
| /* Either both lists are empty, or... */ | |
| [[conde, [[≡, l1, []], | |
| [≡, l2, []]], | |
| /* Or we can pull apart l2 */ | |
| [fresh, [h, t], | |
| [≡, h, [first, l2]], | |
| [≡, tl, [rest, l2]], | |
| /* And reverse t to r */ | |
| [fresh, [r], | |
| [nrev, t, r], | |
| [append, r, [list, h], l2]]]], | |
| sc]]]], | |
| [run, 5, [q], | |
| [nrev, [list], q]]]). | |
| /* Should this work? */ | |
| demos(cons, [run, 5, [l, hd, tl], | |
| [≡, [cons, hd, tl], l], | |
| [≡, hd, 1], | |
| [≡, tl, [list,2,3]]]). | |
| /* Balancing trees */ | |
| /* ?- demos(balance, Code), eval(Code, R). */ | |
| demos(balance, | |
| [map, [lambda, [[x]], [untree, x]], [run, 1, [a], [balanceo, [tree, [quote, [[[1,2],3],4]]], a]]] | |
| ). | |
| eval(Exp, R) :- | |
| prologue(P), | |
| eval_exp([let, P, Exp], e{}, R). |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Which compiler are you using? It doesn't seem to work with SWI-Prolog (as suggested in the blog post).