Last active
February 20, 2025 01:30
-
-
Save dannypsnl/64a65c152e5f093eac8de369aad508a6 to your computer and use it in GitHub Desktop.
miniKanren in 40 minutes (so undone)
This file contains hidden or 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
| #lang racket | |
| (require (for-syntax syntax/parse)) | |
| (define (reify-name n) | |
| (string->symbol | |
| (string-append "_" (number->string n)))) | |
| (struct fresh (value count) | |
| #:methods gen:custom-write | |
| [(define (write-proc self out mode) | |
| (if (fresh-value self) | |
| (display (fresh-value self) out) | |
| (display (reify-name (fresh-count self)) out)))] | |
| #:mutable) | |
| (define (unify? a b) | |
| (cond | |
| [(empty? a) (empty? b)] | |
| [(and (list? a) (list? b)) | |
| (and (unify? (car a) (car b)) | |
| (unify? (cdr a) (cdr b)))] | |
| [(fresh? a) | |
| (if (fresh-value a) | |
| (unify? (fresh-value a) b) | |
| ; check they are not refer to the same object | |
| (if (eq? a b) ; for example, `unify? a a` | |
| a | |
| (begin | |
| (set-fresh-value! a b) | |
| #t)))] | |
| [(fresh? b) | |
| (unify? b a)] | |
| [(and (symbol? a) (symbol? b)) | |
| (eq? a b)] | |
| [else #f])) | |
| (define-syntax (run* stx) | |
| (define (parse-goal query stx) | |
| (syntax-parse stx | |
| #:datum-literals | |
| (succeed fail == fresh) | |
| [fail #'(list)] | |
| [succeed #`(list #,query)] | |
| [(== a b) | |
| #`(if (unify? a b) | |
| (list #,query) | |
| (list))] | |
| [(fresh (x:id) goal) | |
| #`(let () | |
| (define x (make-fresh)) | |
| #,(parse-goal query #'goal)) | |
| ] | |
| )) | |
| (syntax-parse stx | |
| #:datum-literals | |
| (succeed fail) | |
| [(_ query:id goal) | |
| #`(let () | |
| (define count 0) | |
| (define (make-fresh) | |
| (define v (fresh #f count)) | |
| (set! count (add1 count)) | |
| v) | |
| (define query (make-fresh)) | |
| #,(parse-goal #'query #'goal))] | |
| )) | |
| (run* q | |
| fail) | |
| (run* q | |
| succeed) | |
| (run* q | |
| (== 'pea 'pod)) | |
| (run* q | |
| (== q 'pea)) | |
| (run* q | |
| (== 'pea q)) | |
| (run* q | |
| (== q q)) | |
| (run* q | |
| (fresh (x) | |
| (== 'pea q))) | |
| (run* q | |
| (fresh (x) | |
| (== 'pea x))) | |
| (run* q | |
| (fresh (x) | |
| (== (cons x '()) q))) | |
| (run* q | |
| (== '(((pea)) pod) | |
| '(((pea)) pod))) | |
| (run* q | |
| (fresh (x) | |
| (== `(,x ,x) | |
| q))) | |
| (run* q | |
| (fresh (x) | |
| (== `(,x) | |
| q))) | |
| (run* q | |
| (fresh (x) | |
| (== `(,q ,x) | |
| `(,x pod)))) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment