diff --git a/collects/meta/drdr/metadata.ss b/collects/meta/drdr/metadata.ss index 51d29fb333..ed01c30702 100644 --- a/collects/meta/drdr/metadata.ss +++ b/collects/meta/drdr/metadata.ss @@ -7,7 +7,7 @@ (define suffix (filename-extension pth)) (and suffix (ormap (lambda (bs) (bytes=? suffix bs)) - (list #"ss" #"scm" #"scrbl")))) + (list #"ss" #"scm" #"scrbl" #"rkt")))) (define PROP:command-line "drdr:command-line") (define PROP:timeout "drdr:timeout") @@ -65,5 +65,7 @@ (delete-file tmp-file)))))) (unless props:get-prop (error 'get-prop "Could not load props file for ~e" (current-rev))) - (props:get-prop a-path prop def - #:as-string? as-string?)) + ; XXX get-prop is stupid and errors when a-path is invalid rather than returning def + (with-handlers ([exn? (lambda (x) def)]) + (props:get-prop a-path prop def + #:as-string? as-string?))) diff --git a/collects/meta/drdr/render.ss b/collects/meta/drdr/render.ss index 033a9f229a..591ee20696 100644 --- a/collects/meta/drdr/render.ss +++ b/collects/meta/drdr/render.ss @@ -101,7 +101,13 @@ (regexp-replace "^(....-..-..)T(..:..:..).*Z$" date "\\1 \\2")) (define (git-date->nice-date date) (regexp-replace "^(....-..-..) (..:..:..).*$" date "\\1 \\2")) - +(define (log->url log) + (define start-commit (git-push-start-commit log)) + (define end-commit (git-push-end-commit log)) + (if (string=? start-commit end-commit) + (format "http://github.com/plt/racket/commit/~a" end-commit) + (format "http://github.com/plt/racket/compare/~a...~a" start-commit end-commit))) + (define (format-commit-msg) (define pth (revision-commit-msg (current-rev))) (define (timestamp pth) @@ -608,9 +614,7 @@ (define log (read-cache (future-record-path rev))) (define-values (committer title) (log->committer+title log)) - (define url - (format "http://github.com/plt/racket/commit/~a" - (git-push-end-commit log))) + (define url (log->url log)) `(tr ([class "dir"] [title ,title]) (td (a ([href ,url]) ,name)) diff --git a/collects/meta/drdr/scm.ss b/collects/meta/drdr/scm.ss index ec47204cb3..3c62dda6a6 100644 --- a/collects/meta/drdr/scm.ss +++ b/collects/meta/drdr/scm.ss @@ -135,9 +135,12 @@ [to string?])] [get-scm-commit-msg (exact-nonnegative-integer? path-string? . -> . git-push?)]) +(define (git-push-start-commit gp) + (git-commit-hash (last (git-push-commits gp)))) (define (git-push-end-commit gp) (git-commit-hash (first (git-push-commits gp)))) (provide/contract + [git-push-start-commit (git-push? . -> . string?)] [git-push-end-commit (git-push? . -> . string?)]) (define scm-commit-author diff --git a/collects/schelog/INSTALL b/collects/schelog/INSTALL deleted file mode 100644 index 3acb4689a2..0000000000 --- a/collects/schelog/INSTALL +++ /dev/null @@ -1,85 +0,0 @@ -Installing Schelog - - -*** JBC, 2010-04-22: I conjecture that (as a collection -within the PLT tree) installation directions are now -superfluous. The below is preserved for posterity. - - - - -- - -First, obtain the Schelog distribution. This is -available at - -http://www.ccs.neu.edu/~dorai/schelog/schelog.html - -Gunzipping and untarring this file produces a directory -called "schelog". This directory contains, among other -subsidiary files: - -the Schelog code file "schelog.scm"; - -the file INSTALL, which you are now reading. - -- - -The file schelog.scm in the distribution loads in -MzScheme (and some other Scheme dialects) without -configuration. If it does not load in your -dialect, you can configure Schelog for it using -the scmxlate package, which is available at -http://www.ccs.neu.edu/~dorai/scmxlate/scmxlate.html - -Start your Scheme in the schelog directory, and load -the file scmxlate/scmxlate.scm , using the correct -relative or full pathname. You will be asked what your -Scheme dialect is. Answer appropriately. The -following symbols are used by the porting -mechanism to identify the corresponding Scheme -dialects: bigloo (Bigloo); gambit (Gambit); guile -(Guile); mitscheme (MIT Scheme); mzscheme (MzScheme); -petite (Petite Chez Scheme); pscheme (Pocket Scheme); -scm (SCM); stk (STk). - -scmxlate will generate a file called -"my-schelog.scm", which you may rename to -"schelog.scm". - -Load schelog.scm into your Scheme in order to use -Schelog. - -The distribution comes with an "examples" subdirectory -containing some sample Schelog programs. In order to -try an example file, load it into your Scheme after -ensuring that "schelog.scm" has already been loaded. -Follow the instructions in the example file. - -- - -The file "schelog.tex" contains a tutorial on Schelog. Run it -through (plain) TeX to obtain viewable/printable -documentation. (You will need to run TeX twice to resolve -cross references.) - -You can get a browsable version of the document by -calling - -tex2page schelog.tex - -This browsable version is also available for Web -viewing at - -http://www.ccs.neu.edu/~dorai/schelog/schelog.html - -tex2page is available at - -http://www.ccs.neu.edu/~dorai/tex2page/tex2page-doc.html - -- - -Concise bug reports, questions, and suggestions -may be emailed to - -ds26 at gte dot com diff --git a/collects/schelog/README b/collects/schelog/README deleted file mode 100644 index 2fc9397a94..0000000000 --- a/collects/schelog/README +++ /dev/null @@ -1,55 +0,0 @@ -README -Schelog -Dorai Sitaram -ds26@gte.com - - -*** JBC 2010-04-22: this package has been TAMPERED WITH in an unscrupulous and -undisciplined way by John Clements 2010-04-22 in order to see how difficult it -would be to get it to compile in PLT 4.2.5. The answer is "not hard", but it's -certainly not portable any more, and crucially the two macros that cause -capture of the ! symbol now require uses of the macro to supply the bang, thus -making them non-capturing. - -TODO: -- pull some part of the docs across from their tex format -- figure out what to do with the makefile (delete it?) -- turn more of the implicit test cases into explicit test cases -- clean up this README file -- figure out whether there are copyright issues - - - ... - -Schelog is for you if you are interested in any or all -of the following: Scheme, Prolog, logic, logic -programming, AI, and expert systems. - -Schelog is an embedding of logic programming a la -Prolog in Scheme. "Embedding" means you don't lose -Scheme: You can use Prolog-style and conventional -Scheme code fragments alongside each other. Schelog -contains the full repertoire of Prolog features, -including meta-logical and second-order ("set") -predicates, leaving out only those features that could -be more easily and more efficiently done with Scheme -subexpressions. The Schelog distribution includes -examples and comprehensive documentation. - -Schelog has been tested successfully on the following -Scheme dialects: - -Bigloo, Gambit, Guile, MIT Scheme, MzScheme, Petite -Chez Scheme, Pocket Scheme, SCM, and STk. - - ... - -The Schelog distribution is available at the URL: - - http://www.cs.rice.edu/CS/PLT/packages/schelog/ - -Unpacking (using gunzip and tar xf) the Schelog distribution -produces a directory called "schelog". In it is a file -called INSTALL which contains detailed installation -instructions. Read INSTALL now. - diff --git a/collects/schelog/info.ss b/collects/schelog/info.ss index 13a63c4835..7905bec2a8 100644 --- a/collects/schelog/info.ss +++ b/collects/schelog/info.ss @@ -1,2 +1,4 @@ #lang setup/infotab +(define scribblings + '(("schelog.scrbl" (multi-page) (tool)))) diff --git a/collects/schelog/main.rkt b/collects/schelog/main.rkt new file mode 100644 index 0000000000..141fff5b0f --- /dev/null +++ b/collects/schelog/main.rkt @@ -0,0 +1,3 @@ +#lang racket +(require "schelog.rkt") +(provide (all-from-out "schelog.rkt")) \ No newline at end of file diff --git a/collects/schelog/makefile b/collects/schelog/makefile deleted file mode 100644 index 69d8cb0ce5..0000000000 --- a/collects/schelog/makefile +++ /dev/null @@ -1,48 +0,0 @@ -# JBC, 2010-04-22: -# this makefile could probably be usefully rendered in scheme... but -# I'm not going to try. - - -TRIGGER_FILES = history manifest makefile version.tex \ - schelog.scm schelog.tex - -default: - @echo Please read the file INSTALL. - -%.html: %.tex - tex2page $(@:%.html=%) - while grep -i "rerun: tex2page" $(@:%.html=%.hlog); do \ - tex2page $(@:%.html=%); \ - done - -schelog.pdf: schelog.tex - pdftex $^ - -schelog.tar: - echo tar cf schelog.tar schelog/manifest > .tarscript - for f in `grep "^[^;]" manifest`; do \ - echo tar uf schelog.tar schelog/$$f >> .tarscript; \ - done - chmod +x .tarscript - cd ..; schelog/.tarscript - mv ../schelog.tar . - -schelog.tar.bz2: $(TRIGGER_FILES) - make schelog.tar - bzip2 -f schelog.tar - -schelog.tar.gz: $(TRIGGER_FILES) - make schelog.tar - gzip -f schelog.tar - -html: schelog.html - -pdf: schelog.pdf - -dist: schelog.tar.bz2 - -webdist: schelog.tar.gz html - -clean: - @rm -f *~ *.bak - cd dialects; rm -f *~ *.bak diff --git a/collects/schelog/manifest b/collects/schelog/manifest deleted file mode 100644 index 5d3091d762..0000000000 --- a/collects/schelog/manifest +++ /dev/null @@ -1,20 +0,0 @@ -COPYING -README -manifest -makefile -schelog-version.tex -INSTALL -history -schelog.tex -schelog.scm -schelog.bib -dialects/*.scm -examples/bible.scm -examples/england.scm -examples/england2.scm -examples/games.scm -examples/holland.scm -examples/houses.scm -examples/mapcol.scm -examples/puzzle.scm -examples/toys.scm diff --git a/collects/schelog/schelog-version.tex b/collects/schelog/schelog-version.tex deleted file mode 100644 index 5dca9b0e71..0000000000 --- a/collects/schelog/schelog-version.tex +++ /dev/null @@ -1 +0,0 @@ -2003-06-01% last change diff --git a/collects/schelog/schelog.bib b/collects/schelog/schelog.bib deleted file mode 100644 index 98e6a41ba1..0000000000 --- a/collects/schelog/schelog.bib +++ /dev/null @@ -1,95 +0,0 @@ - -@book{sicp, - author = "Harold Abelson and Gerald Jay {Sussman with Julie Sussman}", - title = "\urlp{Structure and Interpretation of - Computer Programs (``SICP'')}{http://mitpress.mit.edu/sicp/full-text/book/book.html}", - edition = "2nd", - publisher = "MIT Press", - year = 1996, -} - -@book{aop, - author = "Leon Sterling and Ehud Shapiro", - title = "\urlh{http://mitpress.mit.edu/book-home.tcl?isbn=0262193388}{The Art - of Prolog}", - publisher = "MIT Press", - year = 1994, - edition = "2nd", -} - -@book{tls, - author = "Daniel P Friedman and Matthias Felleisen", - title = "\urlh{http://www.ccs.neu.edu/~matthias/BTLS}{The Little Schemer}", - publisher = "MIT Press", - year = 1996, - edition = "4th", -} - -@book{tss, - author = "Daniel P Friedman and Matthias Felleisen", - title = "\urlh{http://www.ccs.neu.edu/~matthias/BTSS}{The Seasoned Schemer}", - publisher = "MIT Press", - year = 1996, -} - -@book{eopl, - author = "Daniel P Friedman and Mitchell Wand and Christopher T Haynes", - title = "\urlh{http://mitpress.mit.edu/book-home.tcl?isbn=0262061457}{Essentials - of Programming Languages}", - publisher = "MIT Press, McGraw-Hill", - year = 1992, -} - -@book{bratko, - author = "Ivan Bratko", - title = "Prolog Programming for Artificial Intelligence", - publisher = "Addison-Wesley", - year = 1986, -} - -@book{campbell, - editor = "J A Campbell", - title = "Implementations of Prolog", - publisher = "Ellis Horwood", - year = 1984, -} - -@book{ok:prolog, - author = "Richard A O'Keefe", - title = "\urlh{http://mitpress.mit.edu/book-home.tcl?isbn=0262150395}{The - Craft of Prolog}", - publisher = "MIT Press", - year = 1990, -} - -@inproceedings{logick, - author = "Christopher T Haynes", - title = "{Logic continuations}", - booktitle = "{J Logic Program}", - year = 1987, - note = "vol 4", - pages = "157--176", -} - -@misc{r5rs, - author = "Richard Kelsey and William Clinger and - Jonathan {Rees (eds)}", - title = "\urlp{Revised\^{}5 - Report on the Algorithmic Language Scheme - (``R5RS'')}{http://www.schemers.org/Documents/Standards/R5RS/HTML/r5rs.html}", - year = 1998, -} - -@misc{t-y-scheme, - author = "Dorai Sitaram", - title = "\urlp{Teach Yourself Scheme - in Fixnum Days}{http://www.ccs.neu.edu/~dorai/t-y-scheme/t-y-scheme.html}", -} - -@techreport{mf:prolog, - author = "Matthias Felleisen", - title = "{Transliterating Prolog into Scheme}", - institution = "{Indiana U Comp Sci Dept}", - year = 1985, - number = 182, -} diff --git a/collects/schelog/schelog.rkt b/collects/schelog/schelog.rkt index b18a68903e..54da1b1258 100644 --- a/collects/schelog/schelog.rkt +++ b/collects/schelog/schelog.rkt @@ -1,288 +1,154 @@ #lang racket +(require scheme/stxparam) - -;; TODO: figure out what should actually be 'provide'd. - -(provide (all-defined-out)) - -;; A Note on changes: define-macro isn't so nice, but -;; someone (Dorai?) helpfully provided commented-out -;; versions of each macro in syntax-rules style. -;; Unfortunately, they didn't compile, but this seemed -;; related to an inability to capture the '!' name. -;; The easiest way to fix this was just to take the -;; classic "make 'em put the identifier in there" approach, -;; which means that uses of cut and rel must now include -;; a bang explicitly. It wouldn't be too hard to change -;; back to a capturing macro; I know syntax-case can do -;; it, I don't know if syntax-rules can. - -;; Also, I changed a few top-level mutable bindings into -;; boxed bindings. - -;;-- JBC, 2010-04-22 - - -;MzScheme version of -;schelog.scm -;Schelog -;An embedding of Prolog in Scheme ;Dorai Sitaram ;1989, revised Feb. 1993, Mar. 1997 -;logic variables and their manipulation +(define-struct logic-var (val) #:mutable) -(define schelog:*ref* "ref") +(define *unbound* '_) -(define schelog:*unbound* '_) +;;unbound refs point to themselves +(define (make-ref [val *unbound*]) + (make-logic-var val)) -(define schelog:make-ref - ;;makes a fresh unbound ref; - ;;unbound refs point to themselves - (lambda opt - (vector schelog:*ref* - (if (null? opt) schelog:*unbound* - (car opt))))) +(define _ make-ref) +(define (unbound-logic-var? r) + (and (logic-var? r) (eq? (logic-var-val r) *unbound*))) +(define (unbind-ref! r) + (set-logic-var-val! r *unbound*)) -(define _ schelog:make-ref) +(define-struct frozen (val)) +(define (freeze-ref r) + (make-ref (make-frozen r))) +(define (thaw-frozen-ref r) + (frozen-val (logic-var-val r))) +(define (frozen-logic-var? r) + (frozen? (logic-var-val r))) -(define schelog:ref? - (lambda (r) - (and (vector? r) - (eq? (vector-ref r 0) schelog:*ref*)))) - -(define schelog:deref - (lambda (r) - (vector-ref r 1))) - -(define schelog:set-ref! - (lambda (r v) - (vector-set! r 1 v))) - -(define schelog:unbound-ref? - (lambda (r) - (eq? (schelog:deref r) schelog:*unbound*))) - -(define schelog:unbind-ref! - (lambda (r) - (schelog:set-ref! r schelog:*unbound*))) - -;frozen logic vars - -(define schelog:*frozen* "frozen") - -(define schelog:freeze-ref - (lambda (r) - (schelog:make-ref (vector schelog:*frozen* r)))) - -(define schelog:thaw-frozen-ref - (lambda (r) - (vector-ref (schelog:deref r) 1))) - -(define schelog:frozen-ref? - (lambda (r) - (let ((r2 (schelog:deref r))) - (and (vector? r2) - (eq? (vector-ref r2 0) schelog:*frozen*))))) - -;deref a structure completely (except the frozen ones, i.e.) - -(define schelog:deref* - (lambda (s) - (cond ((schelog:ref? s) - (if (schelog:frozen-ref? s) s - (schelog:deref* (schelog:deref s)))) - ((pair? s) (cons (schelog:deref* (car s)) - (schelog:deref* (cdr s)))) - ((vector? s) - (list->vector (map schelog:deref* (vector->list s)))) - (else s)))) - -;%let introduces new logic variables +(define (logic-var-val* s) + (cond ((logic-var? s) + (if (frozen-logic-var? s) s + (logic-var-val* (logic-var-val s)))) + ((pair? s) (cons (logic-var-val* (car s)) + (logic-var-val* (cdr s)))) + ((vector? s) + (vector-map logic-var-val* s)) + (else s))) (define-syntax %let (syntax-rules () ((%let (x ...) . e) - (let ((x (schelog:make-ref)) ...) - . e)))) + (let ((x (_)) ...) + . e)))) -#;(define-macro %let - (lambda (xx . ee) - `(let ,(map (lambda (x) `(,x (schelog:make-ref))) xx) - ,@ee))) +(define use-occurs-check? (make-parameter #f)) -;the unify predicate +(define (occurs-in? var term) + (and (use-occurs-check?) + (let loop ((term term)) + (cond ((eqv? var term) #t) + ((logic-var? term) + (cond ((unbound-logic-var? term) #f) + ((frozen-logic-var? term) #f) + (else (loop (logic-var-val term))))) + ((pair? term) + (or (loop (car term)) (loop (cdr term)))) + ((vector? term) + (loop (vector->list term))) + (else #f))))) -(define *schelog-use-occurs-check?* #f) - -(define schelog:occurs-in? - (lambda (var term) - (and *schelog-use-occurs-check?* - (let loop ((term term)) - (cond ((eqv? var term) #t) - ((schelog:ref? term) - (cond ((schelog:unbound-ref? term) #f) - ((schelog:frozen-ref? term) #f) - (else (loop (schelog:deref term))))) - ((pair? term) - (or (loop (car term)) (loop (cdr term)))) - ((vector? term) - (loop (vector->list term))) - (else #f)))))) - -(define schelog:unify - (lambda (t1 t2) - (lambda (fk) - (letrec - ((cleanup-n-fail - (lambda (s) - (for-each schelog:unbind-ref! s) - (fk 'fail))) - (unify1 - (lambda (t1 t2 s) - ;(printf "unify1 ~s ~s~%" t1 t2) - (cond ((eqv? t1 t2) s) - ((schelog:ref? t1) - (cond ((schelog:unbound-ref? t1) - (cond ((schelog:occurs-in? t1 t2) - (cleanup-n-fail s)) - (else - (schelog:set-ref! t1 t2) - (cons t1 s)))) - ((schelog:frozen-ref? t1) - (cond ((schelog:ref? t2) - (cond ((schelog:unbound-ref? t2) - ;(printf "t2 is unbound~%") - (unify1 t2 t1 s)) - ((schelog:frozen-ref? t2) - (cleanup-n-fail s)) - (else - (unify1 t1 (schelog:deref t2) s)))) - (else (cleanup-n-fail s)))) +(define (unify t1 t2) + (lambda (fk) + (define (cleanup-n-fail s) + (for-each unbind-ref! s) + (fk 'fail)) + (define (unify1 t1 t2 s) + (cond ((eqv? t1 t2) s) + ((logic-var? t1) + (cond ((unbound-logic-var? t1) + (cond ((occurs-in? t1 t2) + (cleanup-n-fail s)) (else - ;(printf "derefing t1~%") - (unify1 (schelog:deref t1) t2 s)))) - ((schelog:ref? t2) (unify1 t2 t1 s)) - ((and (pair? t1) (pair? t2)) - (unify1 (cdr t1) (cdr t2) - (unify1 (car t1) (car t2) s))) - ((and (string? t1) (string? t2)) - (if (string=? t1 t2) s - (cleanup-n-fail s))) - ((and (vector? t1) (vector? t2)) - (unify1 (vector->list t1) - (vector->list t2) s)) - (else - (for-each schelog:unbind-ref! s) - (fk 'fail)))))) - (let ((s (unify1 t1 t2 '()))) - (lambda (d) - (cleanup-n-fail s))))))) + (set-logic-var-val! t1 t2) + (cons t1 s)))) + ((frozen-logic-var? t1) + (cond ((logic-var? t2) + (cond ((unbound-logic-var? t2) + (unify1 t2 t1 s)) + ((frozen-logic-var? t2) + (cleanup-n-fail s)) + (else + (unify1 t1 (logic-var-val t2) s)))) + (else (cleanup-n-fail s)))) + (else + (unify1 (logic-var-val t1) t2 s)))) + ((logic-var? t2) (unify1 t2 t1 s)) + ((and (pair? t1) (pair? t2)) + (unify1 (cdr t1) (cdr t2) + (unify1 (car t1) (car t2) s))) + ((and (string? t1) (string? t2)) + (if (string=? t1 t2) s + (cleanup-n-fail s))) + ((and (vector? t1) (vector? t2)) + (unify1 (vector->list t1) + (vector->list t2) s)) + (else + (for-each unbind-ref! s) + (fk 'fail)))) + (define s (unify1 t1 t2 '())) + (lambda (d) + (cleanup-n-fail s)))) -(define %= schelog:unify) - -;disjunction +(define %= unify) (define-syntax %or (syntax-rules () ((%or g ...) (lambda (__fk) - (call-with-current-continuation - (lambda (__sk) - (call-with-current-continuation - (lambda (__fk) - (__sk ((schelog:deref* g) __fk)))) - ... - (__fk 'fail))))))) - -#;(define-macro %or - (lambda gg - `(lambda (__fk) - (call-with-current-continuation - (lambda (__sk) - ,@(map (lambda (g) - `(call-with-current-continuation - (lambda (__fk) - (__sk ((schelog:deref* ,g) __fk))))) - gg) - (__fk 'fail)))))) - -;conjunction + (let/cc __sk + (let/cc __fk + (__sk ((logic-var-val* g) __fk))) + ... + (__fk 'fail)))))) (define-syntax %and (syntax-rules () ((%and g ...) (lambda (__fk) - (let* ((__fk ((schelog:deref* g) __fk)) - ...) - __fk))))) + (let* ((__fk ((logic-var-val* g) __fk)) + ...) + __fk))))) -#;(define-macro %and - (lambda gg - `(lambda (__fk) - (let* ,(map (lambda (g) `(__fk ((schelog:deref* ,g) __fk))) gg) - __fk)))) +(define-syntax-parameter ! + (λ (stx) (raise-syntax-error '! "May only be used syntactically inside %rel or %cut-delimiter expression." stx))) -;cut - -;; rather arbitrarily made this macro non- -;; capturing by requiring ! to be supplied at -;; macro use... not changing docs... -- JBC 2010 (define-syntax %cut-delimiter (syntax-rules () - ((%cut-delimiter ! g) + ((%cut-delimiter g) (lambda (__fk) - (let ((! (lambda (__fk2) __fk))) - ((schelog:deref* g) __fk)))))) - -#;(define-macro %cut-delimiter - (lambda (g) - `(lambda (__fk) - (let ((! (lambda (__fk2) __fk))) - ((schelog:deref* ,g) __fk))))) - -;Prolog-like sugar + (let ((this-! (lambda (__fk2) __fk))) + (syntax-parameterize + ([! (make-rename-transformer #'this-!)]) + ((logic-var-val* g) __fk))))))) (define-syntax %rel (syntax-rules () - ((%rel ! (v ...) ((a ...) subgoal ...) ...) - (lambda __fmls - (lambda (__fk) - (call-with-current-continuation - (lambda (__sk) - (let ((! (lambda (fk1) __fk))) - (%let (v ...) - (call-with-current-continuation - (lambda (__fk) - (let* ((__fk ((%= __fmls (list a ...)) __fk)) - (__fk ((schelog:deref* subgoal) __fk)) - ...) - (__sk __fk)))) - ... - (__fk 'fail)))))))))) - -#;(define-macro %rel - (lambda (vv . cc) - `(lambda __fmls + ((%rel (v ...) ((a ...) subgoal ...) ...) + (lambda __fmls (lambda (__fk) - (call-with-current-continuation - (lambda (__sk) - (let ((! (lambda (fk1) __fk))) - (%let ,vv - ,@(map (lambda (c) - `(call-with-current-continuation - (lambda (__fk) - (let* ((__fk ((%= __fmls (list ,@(car c))) - __fk)) - ,@(map (lambda (sg) - `(__fk ((schelog:deref* ,sg) - __fk))) - (cdr c))) - (__sk __fk))))) - cc) - (__fk 'fail))))))))) - -;the fail and true preds + (let/cc __sk + (let ((this-! (lambda (fk1) __fk))) + (syntax-parameterize + ([! (make-rename-transformer #'this-!)]) + (%let (v ...) + (let/cc __fk + (let* ((__fk ((%= __fmls (list a ...)) __fk)) + (__fk ((logic-var-val* subgoal) __fk)) + ...) + (__sk __fk))) + ... + (__fk 'fail)))))))))) (define %fail (lambda (fk) (fk 'fail))) @@ -290,506 +156,401 @@ (define %true (lambda (fk) fk)) -;for structures ("functors"), use Scheme's list and vector -;functions and anything that's built using them. - -;arithmetic - (define-syntax %is - (syntax-rules (quote) + (syntax-rules () ((%is v e) (lambda (__fk) - ((%= v (%is (1) e __fk)) __fk))) + ((%= v (%is/fk e __fk)) __fk))))) +(define-syntax %is/fk + (syntax-rules (quote) + ((%is/fk (quote x) fk) (quote x)) + ((%is/fk (x ...) fk) + ((%is/fk x fk) ...)) + ((%is/fk x fk) + (if (and (logic-var? x) (unbound-logic-var? x)) + (fk 'fail) (logic-var-val* x))))) - ((%is (1) (quote x) fk) (quote x)) - ((%is (1) (x ...) fk) - ((%is (1) x fk) ...)) - ((%is (1) x fk) - (if (and (schelog:ref? x) (schelog:unbound-ref? x)) - (fk 'fail) (schelog:deref* x))))) +(define ((make-binary-arithmetic-relation f) x y) + (%and (%is #t (number? x)) + (%is #t (number? y)) + (%is #t (f x y)))) -#;(define-macro %is - (lambda (v e) - (letrec ((%is-help (lambda (e fk) - (cond ((pair? e) - (cond ((eq? (car e) 'quote) e) - (else - (map (lambda (e1) - (%is-help e1 fk)) e)))) - (else - `(if (and (schelog:ref? ,e) - (schelog:unbound-ref? ,e)) - (,fk 'fail) (schelog:deref* ,e))))))) - `(lambda (__fk) - ((%= ,v ,(%is-help e '__fk)) __fk))))) +(define %=:= (make-binary-arithmetic-relation =)) +(define %> (make-binary-arithmetic-relation >)) +(define %>= (make-binary-arithmetic-relation >=)) +(define %< (make-binary-arithmetic-relation <)) +(define %<= (make-binary-arithmetic-relation <=)) +(define %=/= (make-binary-arithmetic-relation (compose not =))) -;defining arithmetic comparison operators +(define (constant? x) + (cond ((logic-var? x) + (cond ((unbound-logic-var? x) #f) + ((frozen-logic-var? x) #t) + (else (constant? (logic-var-val x))))) + ((pair? x) #f) + ((vector? x) #f) + (else #t))) -(define schelog:make-binary-arithmetic-relation - (lambda (f) - (lambda (x y) - (%is #t (f x y))))) +(define (compound? x) + (cond ((logic-var? x) + (cond ((unbound-logic-var? x) #f) + ((frozen-logic-var? x) #f) + (else (compound? (logic-var-val x))))) + ((pair? x) #t) + ((vector? x) #t) + (else #f))) -(define %=:= (schelog:make-binary-arithmetic-relation =)) -(define %> (schelog:make-binary-arithmetic-relation >)) -(define %>= (schelog:make-binary-arithmetic-relation >=)) -(define %< (schelog:make-binary-arithmetic-relation <)) -(define %<= (schelog:make-binary-arithmetic-relation <=)) -(define %=/= (schelog:make-binary-arithmetic-relation - (lambda (m n) (not (= m n))))) +(define (%constant x) + (lambda (fk) + (if (constant? x) fk (fk 'fail)))) -;type predicates +(define (%compound x) + (lambda (fk) + (if (compound? x) fk (fk 'fail)))) -(define schelog:constant? - (lambda (x) - (cond ((schelog:ref? x) - (cond ((schelog:unbound-ref? x) #f) - ((schelog:frozen-ref? x) #t) - (else (schelog:constant? (schelog:deref x))))) - ((pair? x) #f) - ((vector? x) #f) - (else #t)))) +(define (var? x) + (cond ((logic-var? x) + (cond ((unbound-logic-var? x) #t) + ((frozen-logic-var? x) #f) + (else (var? (logic-var-val x))))) + ((pair? x) (or (var? (car x)) (var? (cdr x)))) + ((vector? x) (var? (vector->list x))) + (else #f))) -(define schelog:compound? - (lambda (x) - (cond ((schelog:ref? x) (cond ((schelog:unbound-ref? x) #f) - ((schelog:frozen-ref? x) #f) - (else (schelog:compound? (schelog:deref x))))) - ((pair? x) #t) - ((vector? x) #t) - (else #f)))) +(define (%var x) + (lambda (fk) (if (var? x) fk (fk 'fail)))) -(define %constant - (lambda (x) - (lambda (fk) - (if (schelog:constant? x) fk (fk 'fail))))) +(define (%nonvar x) + (lambda (fk) (if (var? x) (fk 'fail) fk))) -(define %compound - (lambda (x) - (lambda (fk) - (if (schelog:compound? x) fk (fk 'fail))))) - -;metalogical type predicates - -(define schelog:var? - (lambda (x) - (cond ((schelog:ref? x) - (cond ((schelog:unbound-ref? x) #t) - ((schelog:frozen-ref? x) #f) - (else (schelog:var? (schelog:deref x))))) - ((pair? x) (or (schelog:var? (car x)) (schelog:var? (cdr x)))) - ((vector? x) (schelog:var? (vector->list x))) - (else #f)))) - -(define %var - (lambda (x) - (lambda (fk) (if (schelog:var? x) fk (fk 'fail))))) - -(define %nonvar - (lambda (x) - (lambda (fk) (if (schelog:var? x) (fk 'fail) fk)))) - -; negation of unify - -(define schelog:make-negation ;basically inlined cut-fail - (lambda (p) - (lambda args - (lambda (fk) - (if (call-with-current-continuation - (lambda (k) - ((apply p args) (lambda (d) (k #f))))) - (fk 'fail) - fk))))) +(define ((make-negation p) . args) + ;basically inlined cut-fail + (lambda (fk) + (if (let/cc k + ((apply p args) (lambda (d) (k #f)))) + (fk 'fail) + fk))) (define %/= - (schelog:make-negation %=)) + (make-negation %=)) -;identical +(define (ident? x y) + (cond ((logic-var? x) + (cond ((unbound-logic-var? x) + (cond ((logic-var? y) + (cond ((unbound-logic-var? y) (eq? x y)) + ((frozen-logic-var? y) #f) + (else (ident? x (logic-var-val y))))) + (else #f))) + ((frozen-logic-var? x) + (cond ((logic-var? y) + (cond ((unbound-logic-var? y) #f) + ((frozen-logic-var? y) (eq? x y)) + (else (ident? x (logic-var-val y))))) + (else #f))) + (else (ident? (logic-var-val x) y)))) + ((pair? x) + (cond ((logic-var? y) + (cond ((unbound-logic-var? y) #f) + ((frozen-logic-var? y) #f) + (else (ident? x (logic-var-val y))))) + ((pair? y) + (and (ident? (car x) (car y)) + (ident? (cdr x) (cdr y)))) + (else #f))) + ((vector? x) + (cond ((logic-var? y) + (cond ((unbound-logic-var? y) #f) + ((frozen-logic-var? y) #f) + (else (ident? x (logic-var-val y))))) + ((vector? y) + (ident? (vector->list x) + (vector->list y))) + (else #f))) + (else + (cond ((logic-var? y) + (cond ((unbound-logic-var? y) #f) + ((frozen-logic-var? y) #f) + (else (ident? x (logic-var-val y))))) + ((pair? y) #f) + ((vector? y) #f) + (else (eqv? x y)))))) -(define schelog:ident? - (lambda (x y) - (cond ((schelog:ref? x) - (cond ((schelog:unbound-ref? x) - (cond ((schelog:ref? y) - (cond ((schelog:unbound-ref? y) (eq? x y)) - ((schelog:frozen-ref? y) #f) - (else (schelog:ident? x (schelog:deref y))))) - (else #f))) - ((schelog:frozen-ref? x) - (cond ((schelog:ref? y) - (cond ((schelog:unbound-ref? y) #f) - ((schelog:frozen-ref? y) (eq? x y)) - (else (schelog:ident? x (schelog:deref y))))) - (else #f))) - (else (schelog:ident? (schelog:deref x) y)))) - ((pair? x) - (cond ((schelog:ref? y) - (cond ((schelog:unbound-ref? y) #f) - ((schelog:frozen-ref? y) #f) - (else (schelog:ident? x (schelog:deref y))))) - ((pair? y) - (and (schelog:ident? (car x) (car y)) - (schelog:ident? (cdr x) (cdr y)))) - (else #f))) - ((vector? x) - (cond ((schelog:ref? y) - (cond ((schelog:unbound-ref? y) #f) - ((schelog:frozen-ref? y) #f) - (else (schelog:ident? x (schelog:deref y))))) - ((vector? y) - (schelog:ident? (vector->list x) - (vector->list y))) - (else #f))) - (else - (cond ((schelog:ref? y) - (cond ((schelog:unbound-ref? y) #f) - ((schelog:frozen-ref? y) #f) - (else (schelog:ident? x (schelog:deref y))))) - ((pair? y) #f) - ((vector? y) #f) - (else (eqv? x y))))))) +(define (%== x y) + (lambda (fk) (if (ident? x y) fk (fk 'fail)))) -(define %== - (lambda (x y) - (lambda (fk) (if (schelog:ident? x y) fk (fk 'fail))))) +(define (%/== x y) + (lambda (fk) (if (ident? x y) (fk 'fail) fk))) -(define %/== - (lambda (x y) - (lambda (fk) (if (schelog:ident? x y) (fk 'fail) fk)))) +(define (freeze s) + (let ((dict '())) + (let loop ((s s)) + (cond ((logic-var? s) + (cond ((or (unbound-logic-var? s) (frozen-logic-var? s)) + (let ((x (assq s dict))) + (if x (cdr x) + (let ((y (freeze-ref s))) + (set! dict (cons (cons s y) dict)) + y)))) + (else (loop (logic-var-val s))))) + ((pair? s) (cons (loop (car s)) (loop (cdr s)))) + ((vector? s) + (list->vector (map loop (vector->list s)))) + (else s))))) -;variables as objects +(define (melt f) + (cond ((logic-var? f) + (cond ((unbound-logic-var? f) f) + ((frozen-logic-var? f) (thaw-frozen-ref f)) + (else (melt (logic-var-val f))))) + ((pair? f) + (cons (melt (car f)) (melt (cdr f)))) + ((vector? f) + (list->vector (map melt (vector->list f)))) + (else f))) -(define schelog:freeze - (lambda (s) - (let ((dict '())) - (let loop ((s s)) - (cond ((schelog:ref? s) - (cond ((or (schelog:unbound-ref? s) (schelog:frozen-ref? s)) - (let ((x (assq s dict))) - (if x (cdr x) - (let ((y (schelog:freeze-ref s))) - (set! dict (cons (cons s y) dict)) - y)))) - ;((schelog:frozen-ref? s) s) ;? - (else (loop (schelog:deref s))))) - ((pair? s) (cons (loop (car s)) (loop (cdr s)))) - ((vector? s) - (list->vector (map loop (vector->list s)))) - (else s)))))) +(define (melt-new f) + (let ((dict '())) + (let loop ((f f)) + (cond ((logic-var? f) + (cond ((unbound-logic-var? f) f) + ((frozen-logic-var? f) + (let ((x (assq f dict))) + (if x (cdr x) + (let ((y (_))) + (set! dict (cons (cons f y) dict)) + y)))) + (else (loop (logic-var-val f))))) + ((pair? f) (cons (loop (car f)) (loop (cdr f)))) + ((vector? f) + (list->vector (map loop (vector->list f)))) + (else f))))) -(define schelog:melt - (lambda (f) - (cond ((schelog:ref? f) - (cond ((schelog:unbound-ref? f) f) - ((schelog:frozen-ref? f) (schelog:thaw-frozen-ref f)) - (else (schelog:melt (schelog:deref f))))) - ((pair? f) - (cons (schelog:melt (car f)) (schelog:melt (cdr f)))) - ((vector? f) - (list->vector (map schelog:melt (vector->list f)))) - (else f)))) +(define (copy s) + (melt-new (freeze s))) -(define schelog:melt-new - (lambda (f) - (let ((dict '())) - (let loop ((f f)) - (cond ((schelog:ref? f) - (cond ((schelog:unbound-ref? f) f) - ((schelog:frozen-ref? f) - (let ((x (assq f dict))) - (if x (cdr x) - (let ((y (schelog:make-ref))) - (set! dict (cons (cons f y) dict)) - y)))) - (else (loop (schelog:deref f))))) - ((pair? f) (cons (loop (car f)) (loop (cdr f)))) - ((vector? f) - (list->vector (map loop (vector->list f)))) - (else f)))))) +(define (%freeze s f) + (lambda (fk) + ((%= (freeze s) f) fk))) -(define schelog:copy - (lambda (s) - (schelog:melt-new (schelog:freeze s)))) +(define (%melt f s) + (lambda (fk) + ((%= (melt f) s) fk))) -(define %freeze - (lambda (s f) - (lambda (fk) - ((%= (schelog:freeze s) f) fk)))) +(define (%melt-new f s) + (lambda (fk) + ((%= (melt-new f) s) fk))) -(define %melt - (lambda (f s) - (lambda (fk) - ((%= (schelog:melt f) s) fk)))) +(define (%copy s c) + (lambda (fk) + ((%= (copy s) c) fk))) -(define %melt-new - (lambda (f s) - (lambda (fk) - ((%= (schelog:melt-new f) s) fk)))) +(define (%not g) + (lambda (fk) + (if (let/cc k + ((logic-var-val* g) (lambda (d) (k #f)))) + (fk 'fail) fk))) -(define %copy - (lambda (s c) - (lambda (fk) - ((%= (schelog:copy s) c) fk)))) +(define (%empty-rel . args) + %fail) -;negation as failure - -(define %not - (lambda (g) - (lambda (fk) - (if (call-with-current-continuation - (lambda (k) - ((schelog:deref* g) (lambda (d) (k #f))))) - (fk 'fail) fk)))) - -;assert, asserta - -(define %empty-rel - (lambda args - %fail)) - -(define-syntax %assert - (syntax-rules (!) - ((%assert rel-name (v ...) ((a ...) subgoal ...) ...) - (set! rel-name - (let ((__old-rel rel-name) - (__new-addition (%rel (v ...) ((a ...) subgoal ...) ...))) - (lambda __fmls - (%or (apply __old-rel __fmls) - (apply __new-addition __fmls)))))))) - -(define-syntax %assert-a - (syntax-rules (!) - ((%assert-a rel-name (v ...) ((a ...) subgoal ...) ...) - (set! rel-name - (let ((__old-rel rel-name) - (__new-addition (%rel (v ...) ((a ...) subgoal ...) ...))) - (lambda __fmls - (%or (apply __new-addition __fmls) - (apply __old-rel __fmls)))))))) - -#;(define-macro %assert - (lambda (rel-name vv . cc) - `(set! ,rel-name - (let ((__old-rel ,rel-name) - (__new-addition (%rel ,vv ,@cc))) +(define-syntax %assert! + (syntax-rules () + ((_ rel-name (v ...) ((a ...) subgoal ...) ...) + (set! rel-name + (let ((__old-rel rel-name) + (__new-addition (%rel (v ...) ((a ...) subgoal ...) ...))) (lambda __fmls (%or (apply __old-rel __fmls) - (apply __new-addition __fmls))))))) + (apply __new-addition __fmls)))))))) -#;(define-macro %assert-a - (lambda (rel-name vv . cc) - `(set! ,rel-name - (let ((__old-rel ,rel-name) - (__new-addition (%rel ,vv ,@cc))) +(define-syntax %assert-after! + (syntax-rules () + ((_ rel-name (v ...) ((a ...) subgoal ...) ...) + (set! rel-name + (let ((__old-rel rel-name) + (__new-addition (%rel (v ...) ((a ...) subgoal ...) ...))) (lambda __fmls (%or (apply __new-addition __fmls) - (apply __old-rel __fmls))))))) + (apply __old-rel __fmls)))))))) -;set predicates +(define (set-cons e s) + (if (member e s) s (cons e s))) -(define schelog:set-cons - (lambda (e s) - (if (member e s) s (cons e s)))) +(define-struct goal-with-free-vars (vars subgoal)) (define-syntax %free-vars (syntax-rules () ((%free-vars (v ...) g) - (cons 'schelog:goal-with-free-vars - (cons (list v ...) g))))) + (make-goal-with-free-vars + (list v ...) + g)))) -#;(define-macro %free-vars - (lambda (vv g) - `(cons 'schelog:goal-with-free-vars - (cons (list ,@vv) ,g)))) +(define ((make-bag-of kons) lv goal bag) + (let ((fvv '())) + (when (goal-with-free-vars? goal) + (set! fvv (goal-with-free-vars-vars goal)) + (set! goal (goal-with-free-vars-subgoal goal))) + (make-bag-of-aux kons fvv lv goal bag))) -(define schelog:goal-with-free-vars? - (lambda (x) - (and (pair? x) (eq? (car x) 'schelog:goal-with-free-vars)))) +(define (make-bag-of-aux kons fvv lv goal bag) + (lambda (fk) + (let/cc sk + (let ((lv2 (cons fvv lv))) + (let* ((acc '()) + (fk-final + (lambda (d) + (sk ((separate-bags fvv bag acc) fk)))) + (fk-retry (goal fk-final))) + (set! acc (kons (logic-var-val* lv2) acc)) + (fk-retry 'retry)))))) -(define schelog:make-bag-of - (lambda (kons) - (lambda (lv goal bag) - (let ((fvv '())) - (when (schelog:goal-with-free-vars? goal) - (set! fvv (cadr goal)) - (set! goal (cddr goal))) - (schelog:make-bag-of-aux kons fvv lv goal bag))))) - -(define schelog:make-bag-of-aux - (lambda (kons fvv lv goal bag) - (lambda (fk) - (call-with-current-continuation - (lambda (sk) - (let ((lv2 (cons fvv lv))) - (let* ((acc '()) - (fk-final - (lambda (d) - ;;(set! acc (reverse! acc)) - (sk ((schelog:separate-bags fvv bag acc) fk)))) - (fk-retry (goal fk-final))) - (set! acc (kons (schelog:deref* lv2) acc)) - (fk-retry 'retry)))))))) - -(define schelog:separate-bags - (lambda (fvv bag acc) - ;;(format #t "Accum: ~s~%" acc) - (let ((bags (let loop ((acc acc) - (current-fvv #f) (current-bag '()) - (bags '())) - (if (null? acc) +(define (separate-bags fvv bag acc) + (let ((bags (let loop ((acc acc) + (current-fvv #f) (current-bag '()) + (bags '())) + (if (null? acc) (cons (cons current-fvv current-bag) bags) (let ((x (car acc))) (let ((x-fvv (car x)) (x-lv (cdr x))) (if (or (not current-fvv) (equal? x-fvv current-fvv)) - (loop (cdr acc) x-fvv (cons x-lv current-bag) bags) - (loop (cdr acc) x-fvv (list x-lv) - (cons (cons current-fvv current-bag) bags))))))))) - ;;(format #t "Bags: ~a~%" bags) - (if (null? bags) (%= bag '()) + (loop (cdr acc) x-fvv (cons x-lv current-bag) bags) + (loop (cdr acc) x-fvv (list x-lv) + (cons (cons current-fvv current-bag) bags))))))))) + (if (null? bags) (%= bag '()) (let ((fvv-bag (cons fvv bag))) (let loop ((bags bags)) (if (null? bags) %fail - (%or (%= fvv-bag (car bags)) - (loop (cdr bags)))))))))) + (%or (%= fvv-bag (car bags)) + (loop (cdr bags))))))))) -(define %bag-of (schelog:make-bag-of cons)) -(define %set-of (schelog:make-bag-of schelog:set-cons)) +(define %bag-of (make-bag-of cons)) +(define %set-of (make-bag-of set-cons)) -;%bag-of-1, %set-of-1 hold if there's at least one solution +(define (%bag-of-1 x g b) + (%and (%bag-of x g b) + (%= b (cons (_) (_))))) -(define %bag-of-1 - (lambda (x g b) - (%and (%bag-of x g b) - (%= b (cons (_) (_)))))) +(define (%set-of-1 x g s) + (%and (%set-of x g s) + (%= s (cons (_) (_))))) -(define %set-of-1 - (lambda (x g s) - (%and (%set-of x g s) - (%= s (cons (_) (_)))))) - -;user interface - -;(%which (v ...) query) returns #f if query fails and instantiations -;of v ... if query succeeds. In the latter case, type (%more) to -;retry query for more instantiations. - -(define schelog:*more-k* (box 'forward)) -(define schelog:*more-fk* (box 'forward)) +(define *more-k* (box 'forward)) +(define *more-fk* (box (λ (d) (error '%more "No active %which")))) (define-syntax %which (syntax-rules () ((%which (v ...) g) (%let (v ...) - (call-with-current-continuation - (lambda (__qk) - (set-box! schelog:*more-k* __qk) - (set-box! schelog:*more-fk* - ((schelog:deref* g) - (lambda (d) - (set-box! schelog:*more-fk* #f) - ((unbox schelog:*more-k*) #f)))) - ((unbox schelog:*more-k*) - (map (lambda (nam val) (list nam (schelog:deref* val))) - '(v ...) - (list v ...))))))))) + (let/cc __qk + (set-box! *more-k* __qk) + (set-box! *more-fk* + ((logic-var-val* g) + (lambda (d) + (set-box! *more-fk* #f) + ((unbox *more-k*) #f)))) + ((unbox *more-k*) + (list (cons 'v (logic-var-val* v)) + ...))))))) -#;(define-macro %which - (lambda (vv g) - `(%let ,vv - (call-with-current-continuation - (lambda (__qk) - (set! schelog:*more-k* __qk) - (set! schelog:*more-fk* - ((schelog:deref* ,g) - (lambda (d) - (set! schelog:*more-fk* #f) - (schelog:*more-k* #f)))) - (schelog:*more-k* - (map (lambda (nam val) (list nam (schelog:deref* val))) - ',vv - (list ,@vv)))))))) +(define (%more) + (let/cc k + (set-box! *more-k* k) + (if (unbox *more-fk*) + ((unbox *more-fk*) 'more) + #f))) -(define %more - (lambda () - (call-with-current-continuation - (lambda (k) - (set-box! schelog:*more-k* k) - (if (unbox schelog:*more-fk*) ((unbox schelog:*more-fk*) 'more) - #f))))) +(define (%member x y) + (%let (xs z zs) + (%or + (%= y (cons x xs)) + (%and (%= y (cons z zs)) + (%member x zs))))) -;end of embedding code. The following are -;some utilities, written in Schelog - -(define %member - (lambda (x y) - (%let (xs z zs) - (%or - (%= y (cons x xs)) - (%and (%= y (cons z zs)) - (%member x zs)))))) - -(define %if-then-else - (lambda (p q r) - (%cut-delimiter ! - (%or - (%and p ! q) - r)))) - -;the above could also have been written in a more -;Prolog-like fashion, viz. - -#;'(define %member - (%rel ! (x xs y ys) - ((x (cons x xs))) - ((x (cons y ys)) (%member x ys)))) - -#;'(define %if-then-else - (%rel ! (p q r) - ((p q r) p ! q) - ((p q r) r))) +(define (%if-then-else p q r) + (%cut-delimiter + (%or + (%and p ! q) + r))) (define %append - (%rel ! (x xs ys zs) - (('() ys ys)) - (((cons x xs) ys (cons x zs)) - (%append xs ys zs)))) + (%rel (x xs ys zs) + (('() ys ys)) + (((cons x xs) ys (cons x zs)) + (%append xs ys zs)))) (define %repeat - ;;failure-driven loop - (%rel ! () - (()) - (() (%repeat)))) + (%rel () + (()) + (() (%repeat)))) -; deprecated names -- retained here for backward-compatibility +(define (atom? x) + (or (number? x) (symbol? x) (string? x) (empty? x))) +(define answer-value? + (match-lambda + [(? atom?) #t] + [(cons (? answer-value?) (? answer-value?)) #t] + [(vector (? answer-value?) ...) #t] + [x #f])) +(define answer? + (match-lambda + [#f #t] + [(list (cons (? symbol?) (? answer-value?)) ...) #t] + [_ #f])) +(define unifiable? + (match-lambda + [(? atom?) #t] + [(cons (? unifiable?) (? unifiable?)) #t] + [(vector (? unifiable?) ...) #t] + [(? logic-var?) #t] + [x #f])) +(define fk? (symbol? . -> . any)) +(define goal/c + (or/c goal-with-free-vars? + (fk? . -> . fk?))) +(define relation/c + (->* () () #:rest (listof unifiable?) goal/c)) -;; JBC, 2010-04-22 -- don't think backward compatibility counts any more. commenting -;; these out. - -#;(define == %=) -#;(define %notunify %/=) - -#;(define-macro %cut - (lambda e - `(%cur-delimiter ,@e))) - -#;(define-macro rel - (lambda e - `(%rel ,@e))) -(define %eq %=:=) -(define %gt %>) -(define %ge %>=) -(define %lt %<) -(define %le %<=) -(define %ne %=/=) -(define %ident %==) -(define %notident %/==) -;(define-syntax %exists (syntax-rules () ((%exists vv g) g))) - -#;(define-macro %exists (lambda (vv g) g)) - -#;(define-macro which - (lambda e - `(%which ,@e))) -(define more %more) - -;end of file +; XXX Add contracts in theses macro expansions +(provide %and %assert! %assert-after! %cut-delimiter %free-vars %is %let + %or %rel %which !) +(provide/contract + [goal/c contract?] + [logic-var? (any/c . -> . boolean?)] + [atom? (any/c . -> . boolean?)] + [unifiable? (any/c . -> . boolean?)] + [answer-value? (any/c . -> . boolean?)] + [answer? (any/c . -> . boolean?)] + [%/= (unifiable? unifiable? . -> . goal/c)] + [%/== (unifiable? unifiable? . -> . goal/c)] + [%< (unifiable? unifiable? . -> . goal/c)] + [%<= (unifiable? unifiable? . -> . goal/c)] + [%= (unifiable? unifiable? . -> . goal/c)] + [%=/= (unifiable? unifiable? . -> . goal/c)] + [%=:= (unifiable? unifiable? . -> . goal/c)] + [%== (unifiable? unifiable? . -> . goal/c)] + [%> (unifiable? unifiable? . -> . goal/c)] + [%>= (unifiable? unifiable? . -> . goal/c)] + [%append (unifiable? unifiable? unifiable? . -> . goal/c)] + [%bag-of (unifiable? goal/c unifiable? . -> . goal/c)] + [%bag-of-1 (unifiable? goal/c unifiable? . -> . goal/c)] + [%compound (unifiable? . -> . goal/c)] + [%constant (unifiable? . -> . goal/c)] + [%copy (unifiable? unifiable? . -> . goal/c)] + [%empty-rel relation/c] + [%fail goal/c] + [%freeze (unifiable? unifiable? . -> . goal/c)] + [%if-then-else (goal/c goal/c goal/c . -> . goal/c)] + [%melt (unifiable? unifiable? . -> . goal/c)] + [%melt-new (unifiable? unifiable? . -> . goal/c)] + [%member (unifiable? unifiable? . -> . goal/c)] + [%nonvar (unifiable? . -> . goal/c)] + [%not (goal/c . -> . goal/c)] + [%more (-> answer?)] + [%repeat (-> goal/c)] + [use-occurs-check? (parameter/c boolean?)] + [%set-of (unifiable? goal/c unifiable? . -> . goal/c)] + [%set-of-1 (unifiable? goal/c unifiable? . -> . goal/c)] + [%true goal/c] + [%var (unifiable? . -> . goal/c)] + [_ (-> logic-var?)]) diff --git a/collects/schelog/schelog.scrbl b/collects/schelog/schelog.scrbl new file mode 100644 index 0000000000..ec039f0b39 --- /dev/null +++ b/collects/schelog/schelog.scrbl @@ -0,0 +1,1460 @@ +#lang scribble/manual +@(require scribble/eval + (for-syntax scheme) + (for-label schelog + (except-in scheme _))) + +@(define schelog-eval (make-base-eval)) +@(schelog-eval '(require schelog)) + +@title{@bold{Schelog}: Prolog-style logic programming in Scheme} + +@author{Dorai Sitaram} + +@margin-note{Adapted for Racket by Dorai Sitaram, John Clements, and Jay McCarthy.} + +@defmodule[schelog] + +Schelog is an @emph{embedding} of +Prolog-style logic programming in Scheme. ``Embedding'' +means you don't lose Scheme: You can use Prolog-style and +conventional Scheme code fragments alongside each other. +Schelog contains the full repertoire of Prolog features, +including meta-logical and second-order (``set'') +predicates, leaving out only those features that could more +easily and more efficiently be done with Scheme +subexpressions. + +The Schelog implementation uses the approach to logic +programming described in Felleisen @cite{mf:prolog} and +Haynes @cite{logick}. In contrast to earlier Lisp simulations of +Prolog @cite{campbell}, +which used explicit continuation +arguments to store failure (backtrack) information, the +Felleisen and Haynes model uses the implicit reified +continuations of Scheme as provided by the operator +@scheme[call-with-current-continuation] (aka @scheme[call/cc]). This +allows Schelog to be an @emph{embedding}, ie, logic +programming is not built as a new language on top of Scheme, +but is used alongside Scheme's other features. Both styles +of programming may be mixed to any extent that a project +needs. + +The Schelog user does not need to know about the +implementation mechanism or about @scheme[call/cc] and +continuations to get on with the business of +doing logic programming with Schelog. + +This text is a gentle introduction to Schelog syntax +and programming. It assumes a working knowledge of +Scheme and an awareness of, if not actual programming +experience with, Prolog. If you need assistance in +either language, you may consult +@cite["sicp" "tls" "tss" "eopl" "r5rs" "t-y-scheme"] for Scheme, and +@cite["bratko" "ok:prolog" "aop"] for Prolog. +There are doubtless many other excellent books and +online documents available. + +@table-of-contents[] + +@section[#:tag "simple"]{Simple Goals and Queries} + +Schelog objects are the same as Scheme objects. However, there +are two subsets of these objects that are of special +interest to Schelog: @emph{goals} and @emph{predicates}. We +will first look at some simple goals. +@secref{predicates} will introduce predicates and ways +of making complex goals using predicates. + +A goal is an object whose truth or falsity we can check. A +goal that turns out to be true is said to succeed. +A goal that turns out to be false is said to +fail. + +Two simple goals that are provided in Schelog are: +@schemeblock[ +%true +%fail +] + +The goal @scheme[%true] succeeds. The goal @scheme[%fail] +always fails. + +(The names of all Schelog primitive objects +start with @litchar{%}. This is to avoid clashes with the names +of conventional Scheme objects of related meaning. +User-created objects in Schelog are not required to +follow this convention.) + +A Schelog user can @emph{query} a goal by wrapping it in a +@scheme[%which]-form. + +@schemeblock[ +(%which () %true) +] + +evaluates to @schemeresult[()], indicating success, whereas: + +@schemeblock[ +(%which () %fail) +] + +evaluates to @scheme[#f], indicating failure. + +Note 1: The second subexpression of the @scheme[%which]-form +is the empty list @schemeresult[()]. Later (@secref{solving-goals}), +we will see @scheme[%which]es +with other lists as the second subform. + +Henceforth, we will use the notation: + +@interaction[(eval:alts E 'F)] + +to say that @scheme[E] @emph{evaluates to} @scheme[F]. Thus, + +@interaction[#:eval schelog-eval (%which () %true)] + +@section[#:tag "predicates"]{Predicates} + +More interesting goals are created by applying a special +kind of Schelog object called a @emph{predicate} (or +@emph{relation}) to other +Schelog objects. Schelog comes with some primitive +predicates, such as the arithmetic operators +@scheme[%=:=] and @scheme[%<], +standing for arithmetic ``equal'' and ``less than'' +respectively. For example, the following are some goals +involving these predicates: + +@interaction[ + #:eval schelog-eval + (%which () (%=:= 1 1)) + (%which () (%< 1 2)) + (%which () (%=:= 1 2)) + (%which () (%< 1 1)) + ] + +Other arithmetic predicates are +@scheme[%>] (``greater than''), +@scheme[%<=] (``less than or equal''), +@scheme[%>=] (``greater than or equal''), and +@scheme[%=/=] (``not equal''). + +Schelog predicates are not to be confused with conventional +Scheme predicates (such as @scheme[<] and @scheme[=]). Schelog +predicates, when applied to arguments, produce goals +that +may either succeed or fail. Scheme predicates, when applied +to arguments, yield a boolean value. Henceforth, we will +use the term ``predicate'' to mean Schelog predicates. +Conventional predicates will be explicitly called ``Scheme +predicates''. + +@subsection[#:tag "facts"]{Predicates Introducing Facts} + +Users can create their own predicates using the Schelog form +@scheme[%rel]. For example, let's +define the predicate @scheme[%knows]: + +@schemeblock+eval[#:eval schelog-eval +(define %knows + (%rel () + [('Odysseus 'TeX)] + [('Odysseus 'Scheme)] + [('Odysseus 'Prolog)] + [('Odysseus 'Penelope)] + [('Penelope 'TeX)] + [('Penelope 'Prolog)] + [('Penelope 'Odysseus)] + [('Telemachus 'TeX)] + [('Telemachus 'calculus)])) +] + +The expression has the expected meaning. Each +@emph{clause} in the @scheme[%rel] establishes a @emph{fact}: +Odysseus +knows TeX, Telemachus knows calculus, &c. In general, if we +apply the predicate to the arguments in any one of its +clauses, we will get a successful goal. Thus, since +@scheme[%knows] has a clause that reads +@scheme[[('Odysseus 'TeX)]], the goal +@scheme[(%knows 'Odysseus 'TeX)] +will be true. + +We can now get answers for the following types of queries: + +@interaction[#:eval schelog-eval +(%which () + (%knows 'Odysseus 'TeX)) +(%which () + (%knows 'Telemachus 'Scheme)) +] + +@subsection[#:tag "rules"]{Predicates with Rules} + +Predicates can be more complicated than the above bald +recitation of facts. The predicate clauses can be @emph{rules}, eg, + +@schemeblock+eval[#:eval schelog-eval +(define %computer-literate + (%rel (person) + [(person) + (%knows person 'TeX) + (%knows person 'Scheme)] + [(person) + (%knows person 'TeX) + (%knows person 'Prolog)])) +] + +This defines the predicate +@scheme[%computer-literate] in +terms of the predicate @scheme[%knows]. In effect, a person is +defined as computer-literate if they know TeX and +Scheme, @emph{or} TeX and Prolog. + +Note that this use of +@scheme[%rel] employs a local @emph{logic variable} called @scheme[_person]. +In general, a @scheme[%rel]-expression can have a list of symbols +as its second subform. These name new logic variables that +can be used within the body of the @scheme[%rel]. + +The following query can now be answered: + +@interaction[#:eval schelog-eval +(%which () + (%computer-literate 'Penelope)) +] + +Since Penelope knows TeX and Prolog, she is computer-literate. + +@subsection[#:tag "solving-goals"]{Solving Goals} + +The above queries are yes/no questions. Logic programming +allows more: We can formulate a goal with @emph{uninstantiated} +logic variables and then ask the querying process to +provide, if possible, values for these variables that cause +the goal to succeed. For instance, the query: + +@interaction[#:eval schelog-eval +(%which (what) + (%knows 'Odysseus what)) +] + +asks for an instantiation of the logic variable @scheme[_what] +that satisfies the goal @scheme[(%knows 'Odysseus what)]. +In other words, we are asking, ``What does Odysseus know?'' + +Note that this use of @scheme[%which] --- like @scheme[%rel] +in the definition of @scheme[%computer-literate] --- +uses a local logic +variable, @scheme[_what]. In general, the second subform of +@scheme[%which] can be a list of local logic variables. The +@scheme[%which]-query returns an answer that is a list of +bindings, one for each logic variable mentioned in its +second subform. Thus, + +@interaction[#:eval schelog-eval +(%which (what) + (%knows 'Odysseus what)) +] + +But that is not all that wily Odysseus knows. Schelog +provides a zero-argument procedure (``thunk'') called +@scheme[%more] +that @emph{retries} the goal in the last +@scheme[%which]-query for a different solution. + +@interaction[#:eval schelog-eval +(%more) +] + +We can keep pumping for more solutions: + +@interaction[#:eval schelog-eval +(%more) +(%more) +(%more) +] + +The final @scheme[#f] shows that there are no more +solutions. This is because there are no more clauses in the +@scheme[%knows] predicate that list Odysseus as knowing anything +else. + +@subsection[#:tag "assert"]{Asserting Extra Clauses} + +We can add more clauses to a predicate after it has already +been defined with a @scheme[%rel]. Schelog provides the +@scheme[%assert!] form for this purpose. Eg, + +@schemeblock+eval[#:eval schelog-eval +(%assert! %knows () + [('Odysseus 'archery)]) +] + +tacks on a new clause at the end of the existing clauses +of the @scheme[%knows] +predicate. Now, the query: + +@interaction[#:eval schelog-eval +(%which (what) + (%knows 'Odysseus what)) +] + +gives TeX, Scheme, Prolog, and Penelope, as before, but +a subsequent @scheme[(%more)] yields a new result: +@interaction-eval[#:eval schelog-eval (begin (%more) (%more) (%more))] +@interaction[#:eval schelog-eval +(%more) +] + +The Schelog form @scheme[%assert-after!] is similar to @scheme[%assert!] but +adds clauses @emph{before} any of the current clauses. + +Both @scheme[%assert!] and @scheme[%assert-after!] assume that the variable +they are adding to already names a predicate (presumably +defined using @scheme[%rel]). +In order to allow defining a predicate entirely through +@scheme[%assert!]s, Schelog provides an empty predicate value +@scheme[%empty-rel]. @scheme[%empty-rel] takes any number of arguments +and always fails. A typical use of the +@scheme[%empty-rel] and @scheme[%assert!] combination: + +@schemeblock+eval[#:eval schelog-eval +(define %parent %empty-rel) + +(%assert! %parent () + [('Laertes 'Odysseus)]) + +(%assert! %parent () + [('Odysseus 'Telemachus)] + [('Penelope 'Telemachus)]) +] + +(Schelog does not provide a predicate for @emph{retracting} +assertions, since we can keep track of older versions of +predicates using conventional Scheme features (@scheme[let] and @scheme[set!]).) + +@subsection[#:tag "local-vars"]{Local Variables} + +The local logic variables of @scheme[%rel]- and +@scheme[%which]-expressions are in reality introduced by the +Schelog syntactic form called @scheme[%let]. (@scheme[%rel] and +@scheme[%which] are macros written using @scheme[%let].) + +@scheme[%let] introduces new lexically scoped logic variables. +Supposing, instead of + +@interaction[#:eval schelog-eval +(%which (what) + (%knows 'Odysseus what)) +] + +we had asked + +@interaction[#:eval schelog-eval +(%let (what) + (%which () + (%knows 'Odysseus what))) +] + +This query, too, succeeds five times, since +Odysseus knows five things. However, @scheme[%which] emits +bindings only for the local variables that @emph{it} +introduces. Thus, this query emits @schemeresult[()] five times before +@scheme[(%more)] finally returns @scheme[#f]. + +@section[#:tag "scheme-w-schelog"]{Using Conventional Scheme Expressions in Schelog} + +The arguments of Schelog predicates can be any Scheme +objects. In particular, composite structures such as lists, +vectors and strings can be used, as also Scheme expressions +using the full array of Scheme's construction and +decomposition operators. For instance, consider the +following goal: + +@schemeblock[ +(%member x '(1 2 3)) +] + +Here, @scheme[%member] is a predicate, @scheme[x] is a logic +variable, and @scheme['(1 2 3)] is a structure. Given a suitably +intuitive definition for @scheme[%member], the above goal +succeeds for @scheme[x] = @schemeresult[1], @schemeresult[2], and @schemeresult[3]. + +Now to defining predicates like @scheme[%member]: + +@schemeblock[ +(define %member + (%rel (x y xs) + [(x (cons x xs))] + [(x (cons y xs)) + (%member x xs)])) +] + +Ie, @scheme[%member] is defined with three local variables: +@scheme[x], @scheme[y], @scheme[xs]. It has two +clauses, identifying the two ways of determining membership. + +The first clause of @scheme[%member] states a fact: For any +@scheme[x], @scheme[x] is a member of a list whose head is also @scheme[x]. + +The second clause of @scheme[%member] is a rule: @scheme[x] is a +member of a list if we can show that it is a member of the +@emph{tail} of that list. In other words, the original +@scheme[%member] goal is translated into a @emph{sub}goal, which is also +a @scheme[%member] goal. + +Note that the variable @scheme[y] in the definition of +@scheme[%member] occurs only once in the second clause. As such, +it doesn't need you to make the effort of naming it. (Names +help only in matching a second occurrence to a first.) Schelog +lets you use the expression @scheme[(_)] to denote an anonymous +variable. (Ie, @scheme[_] is a thunk that generates a fresh +anonymous variable at each call.) The predicate @scheme[%member] can be +rewritten as + +@schemeblock[ +(define %member + (%rel (x xs) + [(x (cons x (_)))] + [(x (cons (_) xs)) + (%member x xs)])) +] + +@subsection[#:tag "constructors"]{Constructors} + +We can use constructors --- Scheme procedures for creating +structures --- to simulate data types in Schelog. For +instance, let's define a natural-number data-type where +@scheme[0] denotes zero, and @scheme[(succ x)] denotes the natural number +whose immediate predecessor is @scheme[x]. The constructor +@scheme[succ] can +be defined in Scheme as: + +@schemeblock+eval[#:eval schelog-eval +(define succ + (lambda (x) + (vector 'succ x))) +] + +Addition and multiplication can be defined as: + +@schemeblock+eval[#:eval schelog-eval +(define %add + (%rel (x y z) + [(0 y y)] + [((succ x) y (succ z)) + (%add x y z)])) + +(define %times + (%rel (x y z z1) + [(0 y 0)] + [((succ x) y z) + (%times x y z1) + (%add y z1 z)])) +] + +We can do a lot of arithmetic with this in place. For +instance, the factorial predicate looks like: + +@schemeblock+eval[#:eval schelog-eval +(define %factorial + (%rel (x y y1) + [(0 (succ 0))] + [((succ x) y) + (%factorial x y1) + (%times (succ x) y1 y)])) +] + +@subsection[#:tag "is"]{@scheme[\%is]} + +The above is a very inefficient way to do arithmetic, +especially when the underlying language Scheme offers +excellent arithmetic facilities (including a comprehensive +number ``tower'' and exact rational arithmetic). One +problem with using Scheme calculations directly in Schelog +clauses is that the expressions used may contain logic +variables that need to be dereferenced. Schelog provides +the predicate @scheme[%is] that takes care of this. The goal + +@schemeblock[ +(%is _X _E) +] + +unifies @scheme[_X] with the value of @scheme[_E] considered as a +Scheme expression. @scheme[_E] can have logic variables, but +usually they should at least be bound, as unbound variables +may not be palatable values to the Scheme operators used in +@scheme[_E]. + +We can now directly use the numbers of Scheme to write a +more efficient @scheme[%factorial] predicate: + +@schemeblock+eval[#:eval schelog-eval +(define %factorial + (%rel (x y x1 y1) + [(0 1)] + [(x y) (%is x1 (- x 1)) + (%factorial x1 y1) + (%is y (* y1 x))])) +] + +A price that this efficiency comes with is that we can +use @scheme[%factorial] only with its first argument already +instantiated. In many cases, this is not an unreasonable +constraint. In fact, given this limitation, there is +nothing to prevent us from using Scheme's factorial +directly: + +@schemeblock+eval[#:eval schelog-eval +(define %factorial + (%rel (x y) + [(x y) + (%is y (scheme-factorial + x))])) +] + +or better yet, ``in-line'' any calls to @scheme[%factorial] with +@scheme[%is]-expressions calling @scheme[scheme-factorial], where the +latter is defined in the usual manner: + +@schemeblock+eval[#:eval schelog-eval +(define scheme-factorial + (lambda (n) + (if (= n 0) 1 + (* n (factorial + (- n 1)))))) +] + +@subsection[#:tag "lexical-scoping"]{Lexical Scoping} + +One can use Scheme's lexical scoping to enhance predicate +definition. Here is a list-reversal predicate defined using +a hidden auxiliary predicate: + +@schemeblock+eval[#:eval schelog-eval +(define %reverse + (letrec + ([revaux + (%rel (x y z w) + [('() y y)] + [((cons x y) z w) + (revaux y + (cons x z) w)])]) + (%rel (x y) + [(x y) (revaux x '() y)]))) +] + +@scheme[(revaux _X _Y _Z)] uses @scheme[_Y] as an accumulator for +reversing @scheme[_X] into @scheme[_Z]. (@scheme[_Y] starts out as @schemeresult[()]. +Each head of @scheme[_X] is @scheme[cons]ed on to @scheme[_Y]. Finally, when +@scheme[_X] has wound down to @schemeresult[()], @scheme[_Y] contains the reversed +list and can be returned as @scheme[_Z].) + +@scheme[revaux] is used purely as a helper predicate for +@scheme[%reverse], and so it can be concealed within a lexical +contour. We use @scheme[letrec] instead of @scheme[let] because +@scheme[revaux] is a recursive procedure. + +@subsection[#:tag "type-predicates"]{Type Predicates} + +Schelog provides a couple of predicates that let the user +probe the type of objects. + +The goal +@schemeblock[ +(%constant _X) +] + +succeeds if @scheme[_X] is an @emph{atomic} object, ie, not a +list or vector. + +The predicate @scheme[%compound], the negation of @scheme[%constant], +checks if its argument is indeed a list or a vector. + +The above are merely the logic-programming equivalents of +corresponding Scheme predicates. Users can use the +predicate @scheme[%is] and Scheme predicates to write more type +checks in Schelog. Thus, to test if @scheme[_X] is a string, the +following goal could be used: + +@schemeblock[ +(%is #t (string? _X)) +] + +User-defined Scheme predicates, in addition to primitive Scheme +predicates, can be thus imported. + +@section[#:tag "backtracking"]{Backtracking} + +It is helpful to go into the following evaluation (@secref{rules}) +in a +little detail: + +@schemeblock+eval[#:eval schelog-eval +(%which () + (%computer-literate 'Penelope)) +] + +The starting goal +is: + +@(define goal litchar) +@schemeblock[ +G0 = (%computer-literate Penelope) +] + +(I've taken out the quote because @schemeresult[Penelope] is the result +of evaluating @scheme['Penelope].) + +Schelog tries to match this with the head of the first +clause of @scheme[%computer-literate]. It succeeds, generating a +binding @scheme[[person . Penelope]]. + +But this means it now has two new goals --- @emph{subgoals} +--- to solve. These are the goals in the body of the +matching clause, with the logic variables substituted by +their instantiations: + +@schemeblock[ +G1 = (%knows Penelope TeX) +G2 = (%knows Penelope Scheme) +] + +For @goal{G1}, Schelog attempts matches with the clauses of +@scheme[%knows], and succeeds at the fifth try. (There are no +subgoals in this case, because the bodies of these ``fact'' +clauses are empty, in contrast to the ``rule'' clauses of +@scheme[%computer-literate].) +Schelog then tries to solve @goal{G2} against the clauses of +@scheme[%knows], and since there is no clause stating that +Penelope knows Scheme, it fails. + +All is not lost though. Schelog now @emph{backtracks} to the +goal that was solved just before, viz., @goal{G1}. It +@emph{retries} @goal{G1}, ie, tries to solve it in a +different way. +This entails searching down the previously unconsidered +@scheme[%knows] +clauses for @goal{G1}, ie, the sixth onwards. Obviously, +Schelog fails again, because the fact that Penelope knows +TeX occurs only once. + +Schelog now backtracks to the goal before @goal{G1}, ie, +@goal{G0}. We abandon the current successful match with the +first clause-head of @scheme[%computer-literate], and try the +next clause-head. Schelog succeeds, again producing a binding +@scheme[[person . Penelope]], and two new subgoals: + +@schemeblock[ +G3 = (%knows Penelope TeX) +G4 = (%knows Penelope Prolog) +] + +It is now easy to trace that Schelog finds both @goal{G3} and @goal{G4} to be +true. Since both of @goal{G0}'s subgoals are true, @goal{G0} is +itself considered true. And this is what Schelog reports. The +interested reader can now trace why the +following query has a different denouement: + +@interaction[#:eval schelog-eval +(%which () + (%computer-literate 'Telemachus)) +] + +@section[#:tag "unification"]{Unification} + +When we say that a goal matches with a clause-head, we mean +that the predicate and argument positions line up. Before +making this comparison, Schelog dereferences all already +bound logic variables. The resulting structures are then +compared to see if they are recursively identical. Thus, +@scheme[1] unifies with @scheme[1], and @scheme[(list 1 2)] with @scheme['(1 2)]; but @scheme[1] and +@scheme[2] do not unify, and neither do @scheme['(1 2)] and @scheme['(1 3)]. + +In general, there could be quite a few uninstantiated logic +variables in the compared objects. Unification will then +endeavor to find the most natural way of binding these +variables so that we arrive at structurally identical +objects. Thus, @scheme[(list _x 1)], where @scheme[_x] is an unbound logic +variable, unifies with @scheme['(0 1)], producing the +binding +@scheme[[_x 0]]. + +Unification is thus a goal, and Schelog makes the unification predicate +available to the user as @scheme[%=]. Eg, + +@interaction[#:eval schelog-eval +(%which (x) + (%= (list x 1) '(0 1))) +] + +Schelog also provides the predicate @scheme[%/=], the @emph{negation} of +@scheme[%=]. @scheme[(%/= _X _Y)] succeeds if and only if @scheme[_X] does +@emph{not} unify with @scheme[_Y]. + +Unification goals constitute the basic subgoals that all +Schelog goals devolve to. A goal succeeds because all the +eventual unification subgoals that it decomposes to in at +least one of its subgoal-branching succeeded. It fails +because every possible subgoal-branching was thwarted by the +failure of a crucial unification subgoal. + +Going back to the example in @secref{backtracking}, the goal +@scheme[(%computer-literate 'Penelope)] succeeds because +(a) it unified with +@scheme[(%computer-literate person)]; and then (b) with the binding +@scheme[[person . Penelope]] in place, @scheme[(%knows person 'TeX)] +unified with @scheme[(%knows 'Penelope 'TeX)] and +@scheme[(%knows person 'Prolog)] unified with @scheme[(%knows 'Penelope 'Prolog)]. + +In contrast, the goal @scheme[(%computer-literate 'Telemachus)] +fails because, with @scheme[[person . Telemachus]], +the subgoals @scheme[(%knows person 'Scheme)] and +@scheme[(%knows person 'Prolog)] have no facts they can +unify with. + +@subsection{The Occurs Check} + +A robust unification algorithm uses the @deftech{occurs check}, which ensures that a logic variable +isn't bound to a structure that contains itself. +Not performing the check can cause the unification +to go into an infinite loop in some cases. On the +other hand, performing the occurs check greatly +increases the time taken by unification, even in cases +that wouldn't require the check. + +Schelog uses the global parameter +@scheme[use-occurs-check?] to decide whether to +use the occurs check. By default, this variable is +@scheme[#f], ie, Schelog disables the occurs check. To +enable the check, + +@schemeblock[ +(use-occurs-check? #t) +] + +@section[#:tag "and-or"]{Conjuctions and Disjunctions} + +Goals may be combined using the forms @scheme[%and] +and @scheme[%or] +to form compound goals. (For @scheme[%not], see @secref{not}.) +Eg, + +@interaction[#:eval schelog-eval +(%which (x) + (%and (%member x '(1 2 3)) + (%< x 3))) +] + +gives solutions for @scheme[_x] that satisfy both the +argument goals of the @scheme[%and]. +Ie, @scheme[_x] should both be a member of @scheme['(1 2 3)] +@emph{and} be less than @scheme[3]. Typing @scheme[(%more)] gives another solution: + +@interaction[#:eval schelog-eval +(%more) +(%more) +] + +There are no more solutions, because @scheme[[x 3]] satisfies +the first but not the second goal. + +Similarly, the query + +@interaction[#:eval schelog-eval +(%which (x) + (%or (%member x '(1 2 3)) + (%member x '(3 4 5)))) +] + +lists all @scheme[_x] that are members of either list. + +@interaction[#:eval schelog-eval +(%more) +(%more) +(%more) +(%more) +(%more) +] + +(Yes, @scheme[([x 3])] is listed twice.) + +We can rewrite the predicate @scheme[%computer-literate] +from @secref{rules} using @scheme[%and] and @scheme[%or]: + +@schemeblock+eval[#:eval schelog-eval +(define %computer-literate + (%rel (person) + [(person) + (%or + (%and (%knows person + 'TeX) + (%knows person + 'Scheme)) + (%and (%knows person + 'TeX) + (%knows person + 'Prolog)))])) +] + +Or, more succinctly: + +@schemeblock+eval[#:eval schelog-eval +(define %computer-literate + (%rel (person) + [(person) + (%and (%knows person + 'TeX) + (%or (%knows person + 'Scheme) + (%knows person + 'Prolog)))])) +] + +We can even dispense with the @scheme[%rel] altogether: + +@schemeblock+eval[#:eval schelog-eval +(define %computer-literate + (lambda (person) + (%and (%knows person + 'TeX) + (%or (%knows person + 'Scheme) + (%knows person + 'Prolog))))) +] + +This last looks like a conventional Scheme predicate +definition, and is arguably +the most readable format for a Scheme programmer. + +@section[#:tag "lv-manip"]{Manipulating Logic Variables} + +Schelog provides special predicates for probing logic +variables, without risking their getting bound. + +@subsection[#:tag "var"]{Checking for Variables} + +The goal + +@schemeblock[ +(%== _X _Y) +] + +succeeds if @scheme[_X] and @scheme[_Y] are @emph{identical} objects. This +is not quite the unification predicate @scheme[%=], for @scheme[%==] +doesn't touch unbound objects the way @scheme[%=] does. Eg, +@scheme[%==] will not equate an unbound logic variable with a +bound one, nor will it equate two unbound logic variables +unless they are the @emph{same} variable. + +The predicate @scheme[%/==] is the negation of @scheme[%==]. + +The goal + +@schemeblock[ +(%var _X) +] + +succeeds if @scheme[_X] isn't completely bound --- ie, it has at +least one unbound logic variable in its innards. + +The predicate @scheme[%nonvar] is the negation of @scheme[%var]. + +@subsection[#:tag "freeze"]{Preserving Variables} + +Schelog lets the user protect a term with variables from +unification by allowing that term to be treated as a +(completely) bound object. The predicates provided for this +purpose are +@scheme[%freeze], +@scheme[%melt], @scheme[%melt-new], and @scheme[%copy]. + +The goal + +@schemeblock[ +(%freeze _S _F) +] + +unifies @scheme[_F] to the frozen version of @scheme[_S]. Any lack +of bindings in @scheme[_S] are preserved no matter how much you +toss @scheme[_F] about. + +The goal + +@schemeblock[ +(%melt _F _S) +] + +retrieves the object frozen in @scheme[_F] into @scheme[_S]. + +The goal + +@schemeblock[ +(%melt-new _F _S) +] + +is similar to @scheme[%melt], +except that when @scheme[_S] is made, the unbound variables in +@scheme[_F] are replaced by brand-new unbound variables. + +The goal + +@schemeblock[ +(%copy _S _C) +] + +is an abbreviation for @scheme[(%freeze _S _F)] +followed by @scheme[(%melt-new _F _C)]. + +@section[#:tag "cut"]{The Cut (@scheme[!])} + +The cut (called @scheme[!]) is a special goal that is used to +prune backtracking options. Like the @scheme[%true] goal, the +cut goal too succeeds, when accosted by the Schelog +subgoaling engine. However, when a further subgoal down the +line fails, and time comes to retry the cut goal, Schelog +will refuse to try alternate clauses for the predicate in +whose definition the cut occurs. In other words, the cut +causes Schelog to commit to all the decisions made from the +time that the predicate was selected to match a subgoal till +the time the cut was satisfied. + +For example, consider again the @scheme[%factorial] +predicate, as defined in @secref{is}: + +@schemeblock+eval[#:eval schelog-eval +(define %factorial + (%rel (x y x1 y1) + [(0 1)] + [(x y) (%is x1 (- x 1)) + (%factorial x1 y1) + (%is y (* y1 x))])) +] + +Clearly, + +@interaction[#:eval schelog-eval +(%which () + (%factorial 0 1)) +(%which (n) + (%factorial 0 n)) +] + +But what if we asked for @scheme[(%more)] for either query? +Backtracking will try +the second clause of @scheme[%factorial], and sure enough the +clause-head unifies, producing binding @scheme[[x . 0]]. +We now get three subgoals. Solving the first, we get @scheme[[x1 . -1]], and then we have to solve @scheme[(%factorial -1 y1)]. It +is easy to see there is no end to this, as we fruitlessly +try to get the factorials of numbers that get more and more +negative. + +If we placed a cut at the first clause: + +@schemeblock[ +... +[(0 1) !] +... +] + +the attempt to find more solutions for @scheme[(%factorial 0 1)] is nipped in the bud. + +Calling @scheme[%factorial] with a @emph{negative} number would still cause an +infinite loop. To take care of that problem as well, we +use another cut: + +@schemeblock+eval[#:eval schelog-eval +(define %factorial + (%rel (x y x1 y1) + [(0 1) !] + [(x y) (%< x 0) ! %fail] + [(x y) (%is x1 (- x 1)) + (%factorial x1 y1) + (%is y (* y1 x))])) +] + +@interaction[#:eval schelog-eval +(%which () + (%factorial 0 1)) +(%more) +(%which () + (%factorial -1 1)) +] + +Using @emph{raw} cuts as above can get very confusing. For this +reason, it is advisable to use it hidden away in +well-understood abstractions. Two such common abstractions +are the conditional and negation. + +@subsection[#:tag "if-then-else"]{Conditional Goals} + +An ``if ... then ... else ...'' predicate can be defined +as follows + +@schemeblock+eval[#:eval schelog-eval +(define %if-then-else + (%rel (p q r) + [(p q r) p ! q] + [(p q r) r])) +] + +(Note that for the first time we have predicate arguments that +are themselves goals.) + +Consider the goal + +@schemeblock[ +G0 = (%if-then-else Gbool Gthen Gelse) +] + +We first unify @goal{G0} with the first clause-head, +giving +@scheme[[p . Gbool]], @scheme[[q . Gthen]], @scheme[[r . Gelse]]. @goal{Gbool} can +now either succeed or fail. + +Case 1: If @goal{Gbool} fails, backtracking will cause the +@goal{G0} to unify with the second clause-head. @scheme[r] is bound +to @goal{Gelse}, and so @goal{Gelse} is tried, as expected. + +Case 2: If @goal{Gbool} succeeds, the cut commits to this +clause of the @scheme[%if-then-else]. We now try @goal{Gthen}. If +@goal{Gthen} should now fail --- or even if we simply retry for +more solutions --- we are guaranteed that the second +clause-head will not be tried. If it were not for the cut, +@goal{G0} would attempt to unify with the second clause-head, which will +of course succeed, and @goal{Gelse} @emph{will} be tried. + +@subsection[#:tag "not"]{Negation as Failure} + +Another common abstraction using the cut is @emph{negation}. +The negation of goal @goal{G} is defined as @scheme[(%not G)], where +the predicate @scheme[%not] is defined as follows: + +@schemeblock+eval[#:eval schelog-eval +(define %not + (%rel () + [(g) g ! %fail] + [(g) %true])) +] + +Thus, @scheme[g]'s negation is deemed a failure if @scheme[g] +succeeds, and a success if @scheme[g] fails. This is of course +confusing goal failure with falsity. In some cases, this +view of negation is actually helpful. + +@section[#:tag "set-of"]{Set Predicates} + +The goal + +@schemeblock[ +(%bag-of _X _G _Bag) +] + +unifies with @scheme[_Bag] the list of all instantiations of +@scheme[_X] for which @scheme[_G] succeeds. Thus, the following query +asks for all the things known --- ie, the collection of things +such that someone knows them: + +@interaction[#:eval schelog-eval +(%which (things-known) + (%let (someone x) + (%bag-of x (%knows someone x) + things-known))) +] + +This is the only solution for this goal: + +@interaction[#:eval schelog-eval +(%more) +] + +Note that some things --- eg, TeX --- are enumerated +more than once. This is because more than one person knows +TeX. To remove duplicates, use the predicate +@scheme[%set-of] +instead of @scheme[%bag-of]: + +@interaction[#:eval schelog-eval +(%which (things-known) + (%let (someone x) + (%set-of x (%knows someone x) + things-known))) +] + +In the above, the free variable @scheme[_someone] in the +@scheme[%knows]-goal is used as if it +were existentially quantified. In contrast, Prolog's +versions of +@scheme[%bag-of] and @scheme[%set-of] fix it for each solution of the +set-predicate goal. We can do it too with some additional +syntax that identifies the free variable. +Eg, + +@interaction[#:eval schelog-eval +(%which (someone things-known) + (%let (x) + (%bag-of x + (%free-vars (someone) + (%knows someone x)) + things-known))) +] + +The bag of things known by @emph{one} someone is +returned. That someone is Odysseus. The query can be +retried for more solutions, each listing the things known by +a different someone: + +@interaction[#:eval schelog-eval +(%more) +(%more) +(%more) +(%more) +] + +Schelog also provides two variants of these set predicates, +viz., @scheme[%bag-of-1] and @scheme[%set-of-1]. These act like @scheme[%bag-of] +and @scheme[%set-of] but fail if the resulting bag or set is empty. + +@section[#:tag "glossary"]{Glossary of Schelog Primitives} + +@(define-syntax (defpred stx) + (syntax-case stx () + [(_ (id arg ...) pre ...) + (syntax/loc stx + (defproc (id arg ...) + goal/c + pre ...))])) +@(define-syntax-rule (defgoal id pre ...) + (defthing id goal/c pre ...)) + +@subsection{Racket Predicates} + +@defproc[(logic-var? [x any/c]) boolean?]{Identifies a logic variable.} + +@defproc[(atom? [x any/c]) boolean?]{Identifies atomic values that may appear in Schelog programs. Equivalent to the contract @scheme[(or/c number? symbol? string? empty?)].} + +@defproc[(unifiable? [x any/c]) boolean?]{Identifies values that may appear in Schelog programs. Either an @scheme[atom?], @scheme[logic-var?], pair of @scheme[unifiable?], or vector of @scheme[unifiable?]s.} + +@defproc[(answer-value? [x any/c]) boolean?]{Identifies values that may appear in @scheme[answer?]. Either an @scheme[atom?], pair of @scheme[answer-value?], or vector of @scheme[answer-value?]s.} + +@defproc[(answer? [x any/c]) boolean?]{Identifies answers returned by @scheme[%more] and @scheme[%which]. Equivalent to the contract @scheme[(or/c false/c (listof (cons/c symbol? answer-value?)))].} + +@defthing[goal/c contract?]{A contract for goals.} + +@subsection{User Interface} + +@defform[(%which (V ...) G ...) + #:contracts ([V identifier?] + [G goal/c])]{ +Returns an @scheme[answer?] +of the variables @scheme[V], ..., that satisfies all of @scheme[G], +... If @scheme[G], ..., cannot be satisfied, returns @scheme[#f]. +Calling the thunk @scheme[%more] produces more +instantiations, if available.} + +@defproc[(%more) answer?]{ +The thunk @scheme[%more] produces more instantiations of the +variables in the most recent @scheme[%which]-form that satisfy the +goals in that @scheme[%which]-form. If no more solutions can +be found, @scheme[%more] returns @scheme[#f].} + +@subsection{Relations} + +@defform/subs[(%rel (V ...) clause ...) + ([clause [(E ...) G ...]]) + #:contracts ([V identifier?] + [E expression?] + [G goal/c])]{ +Returns a predicate function. +Each clause @scheme[C] signifies +that the goal created by applying the predicate object to +anything that matches @scheme[(E ...)] is deemed to succeed if all +the goals @scheme[G], ..., can, in their turn, be shown to succeed.} + +@defpred[(%empty-rel [E unifiable?] ...)]{ +The goal @scheme[(%empty-rel E ...)] always fails. The @emph{value} +@scheme[%empty-rel] is used as a starting value for predicates +that can later be enhanced with @scheme[%assert!] and @scheme[%assert-after!].} + +@defform[(%assert! Pname (V ...) clause ...) + #:contracts ([Pname identifier?] + [V identifier?])]{ +Adds the clauses +@scheme[clauses], ..., to the @emph{end} of the predicate that is the value of +the Scheme variable @scheme[Pname]. The variables @scheme[V], ..., are +local logic variables for @scheme[clause], ....} + +@defform[(%assert-after! Pname (V ...) clause ...) + #:contracts ([Pname identifier?] + [V identifier?])]{ +Like @scheme[%assert!], but adds the new clauses to the @emph{front} +of the existing predicate.} + +@subsection{Logic Variables} + +@defproc[(_) logic-var?]{ +A thunk that produces a new logic variable. Can be +used in situations where we want a logic variable but +don't want to name it. (@scheme[%let], in contrast, introduces new +lexical names for the logic variables it creates.) +} + +@defform[(%let (V ...) expr ...) + #:contracts ([V identifier?])]{ +Introduces @scheme[V], ..., as +lexically scoped logic variables to be used in @scheme[expr], ...} + +@subsection{Cut} + +@defform[(%cut-delimiter . any)]{ +Introduces a cut point. See @secref{cut}.} + +@defidform[!]{ +The cut goal, see @secref{cut}. + +May only be used syntactically inside @scheme[%cut-delimiter] or @scheme[%rel].} + +@subsection{Logical Operators} + +@defgoal[%fail]{ +The goal @scheme[%fail] always fails.} + +@defgoal[%true]{ +The goal @scheme[%true] succeeds. Fails on retry.} + +@defpred[(%repeat)]{ +The goal @scheme[(%repeat)] always succeeds (even on retries). +Useful for failure-driven loops.} + +@defform[(%and G ...) #:contracts ([G goal/c])]{ +The goal @scheme[(%and G ...)] succeeds if all the goals +@scheme[G], ..., succeed.} + +@defform[(%or G ...) #:contracts ([G goal/c])]{ +The goal @scheme[(%or G ...)] succeeds if one of @scheme[G], ..., tried +in that order, succeeds.} + +@defpred[(%not [G goal/c])]{ +The goal @scheme[(%not G)] succeeds if @scheme[G] fails.} + +@defpred[(%if-then-else [G1 goal/c] [G2 goal/c] [G3 goal/c])]{ +The goal @scheme[(%if-then-else G1 G2 G3)] tries @scheme[G1] first: if it +succeeds, tries @scheme[G2]; if not, tries @scheme[G3].} + +@subsection{Unification} + +@defpred[(%= [E1 unifiable?] [E2 unifiable?])]{ +The goal @scheme[(%= E1 E2)] succeeds if @scheme[E1] can be unified with +@scheme[E2]. Any resulting bindings for logic variables are kept.} + +@defpred[(%/= [E1 unifiable?] [E2 unifiable?])]{@scheme[%/=] is the negation of @scheme[%=]. +The goal @scheme[(%/= E1 E2)] succeeds if @scheme[E1] can not be unified +with @scheme[E2].} + +@defpred[(%== [E1 unifiable?] [E2 unifiable?])]{ +The goal @scheme[(%== E1 E2)] succeeds if @scheme[E1] is @emph{identical} +to @scheme[E2]. They should be structurally equal. If containing +logic variables, they should have the same variables in the +same position. Unlike a @scheme[%=]-call, this goal will not bind +any logic variables.} + +@defpred[(%/== [E1 unifiable?] [E2 unifiable?])]{ +@scheme[%/==] is the negation of @scheme[%==]. +The goal @scheme[(%/== E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are not +identical.} + +@defform[(%is E1 E2)]{ +The goal @scheme[(%is E1 E2)] unifies with @scheme[E1] the result of +evaluating @scheme[E2] as a Scheme expression. @scheme[E2] may contain +logic variables, which are dereferenced automatically. +Fails if @scheme[E2] contains unbound logic variables.} + +@defparam[use-occurs-check? on? boolean?]{ +If this is false (the default), +Schelog's unification will not use the occurs check. +If it is true, the occurs check is enabled.} + +@subsection{Numeric Predicates} + +@defpred[(%< [E1 unifiable?] [E2 unifiable?])]{ +The goal @scheme[(%< E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is less than @scheme[E2].} + +@defpred[(%<= [E1 unifiable?] [E2 unifiable?])]{ +The goal @scheme[(%<= E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is less than or equal to @scheme[E2].} + +@defpred[(%=/= [E1 unifiable?] [E2 unifiable?])]{ +The goal @scheme[(%=/= E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is not equal to @scheme[E2].} + +@defpred[(%=:= [E1 unifiable?] [E2 unifiable?])]{ +The goal @scheme[(%=:= E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is equal to @scheme[E2].} + +@defpred[(%> [E1 unifiable?] [E2 unifiable?])]{ +The goal @scheme[(%> E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is greater than @scheme[E2].} + +@defpred[(%>= [E1 unifiable?] [E2 unifiable?])]{ +The goal @scheme[(%>= E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is greater than or equal to @scheme[E2].} + +@subsection{List Predicates} + +@defpred[(%append [E1 unifiable?] [E2 unifiable?] [E3 unifiable?])]{ +The goal @scheme[(%append E1 E2 E3)] succeeds if @scheme[E3] is unifiable +with the list obtained by appending @scheme[E1] and @scheme[E2].} + +@defpred[(%member [E1 unifiable?] [E2 unifiable?])]{ +The goal @scheme[(%member E1 E2)] succeeds if @scheme[E1] is a member +of the list in @scheme[E2].} + +@subsection{Set Predicates} + +@defpred[(%set-of [E1 unifiable?] [G goal/c] [E2 unifiable?])]{ +The goal @scheme[(%set-of E1 G E2)] unifies with @scheme[E2] the @emph{set} +of all the +instantiations of @scheme[E1] for which goal @scheme[G] succeeds.} + +@defpred[(%set-of-1 [E1 unifiable?] [G goal/c] [E2 unifiable?])]{ +Similar to @scheme[%set-of], but fails if the set is empty.} + +@defpred[(%bag-of [E1 unifiable?] [G goal/c] [E2 unifiable?])]{ +The goal @scheme[(%bag-of E1 G E2)] unifies with @scheme[E2] the @emph{bag} +(multiset) +of all the +instantiations of @scheme[E1] for which goal @scheme[G] succeeds.} + +@defpred[(%bag-of-1 [E1 unifiable?] [G goal/c] [E2 unifiable?])]{ +Similar to @scheme[%bag-of], but fails if the bag is empty.} + +@defform[(%free-vars (V ...) G) + #:contracts ([V identifier?] + [G goal/c])]{ +Identifies +the occurrences of the variables @scheme[V], ..., in goal +@scheme[G] as free. It is used to avoid existential quantification +in calls to set predicates (@scheme[%bag-of], @scheme[%set-of], &c.).} + +@subsection{Schelog Predicates} + +@defpred[(%compound [E unifiable?])]{ +The goal @scheme[(%compound E)] succeeds if @scheme[E] is a non-atomic +structure, ie, a vector or a list.} + +@defpred[(%constant [E unifiable?])]{ +The goal @scheme[(%compound E)] succeeds if @scheme[E] is an atomic +structure, ie, not a vector or a list.} + +@defpred[(%var [E unifiable?])]{ +The goal @scheme[(%var E)] succeeds if @scheme[E] is not completely +instantiated, ie, it has at least one unbound variable in +it.} + +@defpred[(%nonvar [E unifiable?])]{ +@scheme[%nonvar] is the negation of @scheme[%var]. +The goal @scheme[(%nonvar E)] succeeds if @scheme[E] is completely +instantiated, ie, it has no unbound variable in it.} + +@subsection{Logic Variable Manipulation} + +@defpred[(%freeze [S unifiable?] [F unifiable?])]{ +The goal @scheme[(%freeze S F)] unifies with @scheme[F] a new frozen +version of the structure in @scheme[S]. Freezing implies that all +the unbound variables are preserved. @scheme[F] can henceforth be +used as @emph{bound} object with no fear of its variables +getting bound by unification.} + +@defpred[(%melt [F unifiable?] [S unifiable?])]{ +The goal @scheme[(%melt F S)] unifies @scheme[S] with the thawed +(original) form of the frozen structure in @scheme[F].} + +@defpred[(%melt-new [F unifiable?] [S unifiable?])]{ +The goal @scheme[(%melt-new F S)] unifies @scheme[S] with a thawed +@emph{copy} of the frozen structure in @scheme[F]. This means +new logic variables are used for unbound logic variables in +@scheme[F].} + +@defpred[(%copy [F unifiable?] [S unifiable?])]{ +The goal @scheme[(%copy F S)] unifies with @scheme[S] a copy of the +frozen structure in @scheme[F].} + +@bibliography[ + @bib-entry[#:key "sicp" + #:author "Harold Abelson and Gerald Jay Sussman with Julie Sussman" + #:title "Structure and Interpretation of Computer Programs (``SICP''), 2nd Edition" + #:url "http://mitpress.mit.edu/sicp/full-text/book/book.html" + #:date "1996" + #:location "MIT Press" + #:is-book? #t] + @bib-entry[#:key "aop" + #:author "Leon Sterling and Ehud Shapiro" + #:url "http://mitpress.mit.edu/book-home.tcl?isbn=0262193388" + #:title "The Art of Prolog, 2nd Edition" + #:location "MIT Press" + #:date "1994" + #:is-book? #t] + @bib-entry[#:key "tls" + #:author "Daniel P Friedman and Matthias Felleisen" + #:url "http://www.ccs.neu.edu/~matthias/BTLS" + #:title "The Little Schemer, 4th Edition" + #:location "MIT Press" + #:date "1996" + #:is-book? #t] + @bib-entry[#:key "tss" + #:author "Daniel P Friedman and Matthias Felleisen" + #:url "http://www.ccs.neu.edu/~matthias/BTSS" + #:title "The Seasoned Schemer" + #:location "MIT Press" + #:date "1996" + #:is-book? #t] + @bib-entry[#:key "eopl" + #:author "Daniel P Friedman and Mitchell Wand and Christopher T Haynes" + #:url "http://mitpress.mit.edu/book-home.tcl?isbn=0262061457" + #:title "Essentials of Programming Languages" + #:location "MIT Press, McGraw-Hill" + #:date "1992" + #:is-book? #t] + @bib-entry[#:key "bratko" + #:author "Ivan Bratko" + #:title "Prolog Programming for Artificial Intelligence" + #:location "Addison-Wesley" + #:date "1986" + #:is-book? #t] + @bib-entry[#:key "campbell" + #:author "J A Campbell (editor)" + #:title "Implementations of Prolog" + #:location "Ellis Horwood" + #:date "1984" + #:is-book? #t] + @bib-entry[#:key "ok:prolog" + #:author "Richard A O'Keefe" + #:url "http://mitpress.mit.edu/book-home.tcl?isbn=0262150395" + #:title "The Craft of Prolog" + #:location "MIT Press" + #:date "1990" + #:is-book? #t] + @bib-entry[#:key "logick" + #:author "Christopher T Haynes" + #:title "Logic continuations" + #:location "J Logic Program, vol 4, 157--176" + #:date "1987"] + @bib-entry[#:key "r5rs" + #:author "Richard Kelsey and William Clinger and Jonathan {Rees (eds)}" + #:url "http://www.schemers.org/Documents/Standards/R5RS/HTML/r5rs.html" + #:title "Revised^5 Report on the Algorithmic Language Scheme (``R5RS'')" + #:date "1998"] + @bib-entry[#:key "t-y-scheme" + #:author "Dorai Sitaram" + #:title "Teach Yourself Scheme in Fixnum Days" + #:url "http://www.ccs.neu.edu/~dorai/t-y-scheme/t-y-scheme.html"] + @bib-entry[#:key "mf:prolog" + #:author "Matthias Felleisen" + #:title "Transliterating Prolog into Scheme" + #:location "Indiana U Comp Sci Dept Tech Report #182" + #:date "1985"] + ] \ No newline at end of file diff --git a/collects/schelog/schelog.tex b/collects/schelog/schelog.tex deleted file mode 100644 index ce7f3b4f55..0000000000 --- a/collects/schelog/schelog.tex +++ /dev/null @@ -1,1572 +0,0 @@ -\magnification\magstephalf - -\input tex2page -\input btxmac -\texonly -%\input 2col - -\sidemargin 1.75 true in - -%\input defun - -% avoiding overfull boxes, without making -% paragraphs too bad - -\pretolerance -1 -\emergencystretch 5pt -\tolerance 3000 - -\hfuzz 1pt - -\hyphenpenalty -1000 -\exhyphenpenalty -1000 -\doublehyphendemerits -100000 -\finalhyphendemerits -100000 - -% ! is special char for makeindex -%\def\bang{!} - -\let\n\noindent - -\let\origverb\verb - -\def\verb{\def\verbatimhook{\parindent0pt \relax}\origverb} - -\def\p{\let\verbatimhook\relax\origverb} - -%sign for ``evaluates to'' -\def\y{$\Rightarrow$} - -%notation for true nil -\def\t{{\tt()}$^{\rm true}$} - -\overfullrule 0pt - - -\def\ar/#1{{\it/#1\/}} - -\hyphenation{sche-log} - -\let\ab\allowbreak - - -%that's all -%\input ptm - -\endtexonly - -\htmlonly -\def\defun#1#2{% -\evalh{(do-end-para)}% -\rawhtml
\endrawhtml -#2% -\rawhtml\endrawhtml{#1}% -\rawhtml
\endrawhtml -\evalh{(do-para)}} - -\def\t{()\rawhtmltrue\endrawhtml} -\def\y{{\tt =>}} - - -\endhtmlonly - -\let\byline\centerline - -\def\defproc{\defun{[{\it procedure}]}} -\def\defpred{\defun{[{\it predicate}]}} -\def\defmac{\defun{[{\it macro}]}} -\def\defgoal{\defun{[{\it goal}]}} -\def\defflag{\defun{[{\it flag}]}} - -\def\newsection{\htmlpagebreak\section} - -\let\q\scm -\let\sverbatim\scm - -\scmkeyword{%which %rel %assert %assert-a %let %and %or %is -! %free-vars -} - -\texonly -\def\t{()$^t$} -\def\y{$\Rightarrow$} -\endtexonly - -\title{Programming in Schelog} - -\byline{\urlh{http://www.ccs.neu.edu/~dorai}{Dorai -Sitaram}} -%\byline{\urlh{mailto:ds26@gte.com}{ds26@gte.com}} -\byline{\urlh{schelog.tar.gz}{\htmlonly Download -\endhtmlonly Version \input ./schelog-version }} -\htmlonly -\byline{\urlh{INSTALL}{Installation instructions}} -\endhtmlonly - -\bigskip - -\n Schelog is an {\em embedding} of -Prolog-style logic programming in Scheme. ``Embedding'' -means you don't lose Scheme: You can use Prolog-style and -conventional Scheme code fragments alongside each other. -Schelog contains the full repertoire of Prolog features, -including meta-logical and second-order (``set'') -predicates, leaving out only those features that could more -easily and more efficiently be done with Scheme -subexpressions. - -The Schelog implementation uses the approach to logic -programming described in Felleisen \cite{mf:prolog} and -Haynes \cite{logick}. In contrast to earlier Lisp simulations of -Prolog \cite{campbell}, -which used explicit continuation -arguments to store failure (backtrack) information, the -Felleisen and Haynes model uses the implicit reified -continuations of Scheme as provided by the operator -\q{call-with-current-continuation} (aka \q{call/cc}). This -allows Schelog to be an {\em embedding}, ie, logic -programming is not built as a new language on top of Scheme, -but is used alongside Scheme's other features. Both styles -of programming may be mixed to any extent that a project -needs. - -The Schelog user does not need to know about the -implementation mechanism or about \q{call/cc} and -continuations to get on with the business of -doing logic programming with Schelog. - -This text is a gentle introduction to Schelog syntax -and programming. It assumes a working knowledge of -Scheme and an awareness of, if not actual programming -experience with, Prolog. If you need assistance in -either language, you may consult -\cite{sicp,tls,tss,eopl,r5rs,t-y-scheme} for Scheme, and -\cite{bratko,ok:prolog,aop} for Prolog. -There are doubtless many other excellent books and -online documents available. - -\beginsection Contents - -\tableofcontents - -\newsection{Simple Goals and Queries} -\label{simple} - -Schelog objects are the same as Scheme objects. However, there -are two subsets of these objects that are of special -interest to Schelog: {\em goals} and {\em predicates}. We -will first look at some simple goals. -Section \ref{predicates} will introduce predicates and ways -of making complex goals using predicates. - -A goal is an object whose truth or falsity we can check. A -goal that turns out to be true is said to succeed. -A goal that turns out to be false is said to -fail. - -Two simple goals that are provided in Schelog are: - -\sverbatim{ -%true -%fail -} - -\n The goal \q{%true} succeeds. The goal \q{%fail} -always fails. - -(The names of all Schelog primitive objects -start with \q{%}. This is to avoid clashes with the names -of conventional Scheme objects of related meaning. -User-created objects in Schelog are not required to -follow this convention.) - -A Schelog user can {\em query} a goal by wrapping it in a -\q{%which}-form. - -\sverbatim{ -(%which () %true) -} - -\n evaluates to \q{()}, indicating success, whereas: - -\sverbatim{ -(%which () %fail) -} - -\n evaluates to \q{#f}, indicating failure. - -Note 1: The second subexpression of the \q{%which}-form -is the empty list \q{()}. Later (sec \ref{solving-goals}), -we will see \q{%which}es -with other lists as the second subform. - -Note 2: The distinction between successful and failing goals -depends on Scheme's distinguishing \q{#f} from -\q{()}. We will see later (sec \ref{false-vs-nil}) -what to do in Scheme dialects where \q{#f} and \q{()} are -identical. For the moment, we will use the annotation -\q{|t} to signal that \q{()} is being used as a true -value. - -Henceforth, we will use the notation: - -\sverbatim{ -E |y F -} - -\n to say that \q{E} {\em evaluates to} \q{F}. Thus, - -\sverbatim{ -(%which () %true) |y |t -} - -\newsection{Predicates} -\label{predicates} - -More interesting goals are created by applying a special -kind of Schelog object called a {\em predicate} (or -{\em relation}) to other -Schelog objects. Schelog comes with some primitive -predicates, such as the arithmetic operators -\q{%=:=} and \q{%<}, -standing for arithmetic ``equal'' and ``less than'' -respectively. For example, the following are some goals -involving these predicates: - -\sverbatim{ -(%which () (%=:= 1 1)) |y |t -(%which () (%< 1 2)) |y |t -(%which () (%=:= 1 2)) |y #f -(%which () (%< 1 1)) |y #f -} - -\n Other arithmetic predicates are -\q{%>} (``greater than''), -\q{%<=} (``less than or equal''), -\q{%>=} (``greater than or equal''), and -\q{%=/=} (``not equal''). - -Schelog predicates are not to be confused with conventional -Scheme predicates (such as \q{<} and \q{=}). Schelog -predicates, when applied to arguments, produce goals -that -may either succeed or fail. Scheme predicates, when applied -to arguments, yield a boolean value. Henceforth, we will -use the term ``predicate'' to mean Schelog predicates. -Conventional predicates will be explicitly called ``Scheme -predicates''. - -\subsection{Predicates Introducing Facts} -\label{facts} - -Users can create their own predicates using the Schelog form -\q{%rel}. For example, let's -define the predicate \q{%knows}: - -\sverbatim{ -(define %knows - (%rel () - [('Odysseus 'TeX)] - [('Odysseus 'Scheme)] - [('Odysseus 'Prolog)] - [('Odysseus 'Penelope)] - [('Penelope 'TeX)] - [('Penelope 'Prolog)] - [('Penelope 'Odysseus)] - [('Telemachus 'TeX)] - [('Telemachus 'calculus)])) -} - -\n The expression has the expected meaning. Each -{\em clause} in the \q{%rel} establishes a {\em fact}: -Odysseus -knows TeX, Telemachus knows calculus, \&c. In general, if we -apply the predicate to the arguments in any one of its -clauses, we will get a successful goal. Thus, since -\q{%knows} has a clause that reads -\q{[('Odysseus 'TeX)]}, the goal -\q{(%knows 'Odysseus 'TeX)} -will be true. - -(In the code in -this text, brackets have the same behavior as parentheses. -We use a mix of brackets and parentheses solely to improve -the readability of the code for humans.] - -We can now get answers for the following types of queries: - -\sverbatim{ -(%which () - (%knows 'Odysseus 'TeX)) -|y |t - -(%which () - (%knows 'Telemachus 'Scheme)) -|y #f -} - -\subsection{Predicates with Rules} -\label{rules} - -Predicates can be more complicated than the above bald -recitation of facts. The predicate clauses can be {\em rules}, eg, - -\sverbatim{ -(define %computer-literate - (%rel (person) - [(person) - (%knows person 'TeX) - (%knows person 'Scheme)] - [(person) - (%knows person 'TeX) - (%knows person 'Prolog)])) -} - -\n This defines the predicate -\q{%computer-literate} in -terms of the predicate \q{%knows}. In effect, a person is -defined as computer-literate if they know TeX and -Scheme, {\em or} TeX and Prolog. - -Note that this use of -\q{%rel} employs a local {\em logic variable} called \q{person}. -In general, a \q{%rel}-expression can have a list of symbols -as its second subform. These name new logic variables that -can be used within the body of the \q{%rel}. - -The following query can now be answered: - -\sverbatim{ -(%which () - (%computer-literate 'Penelope)) -|y |t -} - -\n Since Penelope knows TeX and Prolog, she is computer-literate. - -\subsection{Solving Goals} -\label{solving-goals} - -The above queries are yes/no questions. Logic programming -allows more: We can formulate a goal with {\em uninstantiated} -logic variables and then ask the querying process to -provide, if possible, values for these variables that cause -the goal to succeed. For instance, the query: - -\sverbatim{ -(%which (what) - (%knows 'Odysseus what)) -} - -\n asks for an instantiation of the logic variable \q{what} -that satisfies the goal \q{(%knows 'Odysseus what)}. -In other words, we are asking, ``What does Odysseus know?'' - -Note that this use of \q{%which} --- like \q{%rel} -in the definition of \q{%computer-literate} --- -uses a local logic -variable, \q{what}. In general, the second subform of -\q{%which} can be a list of local logic variables. The -\q{%which}-query returns an answer that is a list of -bindings, one for each logic variable mentioned in its -second subform. Thus, - -\sverbatim{ -(%which (what) - (%knows 'Odysseus what)) -|y ([what TeX]) -} - -\n But that is not all that wily Odysseus knows. Schelog -provides a zero-argument procedure (``thunk'') called -\q{%more} -that {\em retries} the goal in the last -\q{%which}-query for a different solution. - -\sverbatim{ -(%more) |y ([what Scheme]) -} - -\n We can keep pumping for more solutions: - -\sverbatim{ -(%more) |y ([what Prolog]) -(%more) |y ([what Penelope]) -(%more) |y #f -} - -\n The final \q{#f} shows that there are no more -solutions. This is because there are no more clauses in the -\q{%knows} predicate that list Odysseus as knowing anything -else. - -\subsubsection{A Note on {\tt\#f} vs {\tt()}} -\label{false-vs-nil} - -It is now clear why \q{|t} was the right choice for truth in -the previous yes/no \q{%which}-queries that had no logic -variables (sec \ref{simple}). \q{%which} returns a -list of bindings -for true -goals: the list is empty when there are no variables. - -For such Schemes as don't distinguish between \q{()} and -\q{#f}, we can still ask fruitful yes/no queries. Simply -use a dummy local -variable in the -\q{%which}-expression. Truth will give an (ignorable) -binding for the dummy variable, while falsity will, as -usual, produce \q{#f}. - -\sverbatim{ -(%which (bingo) - (%knows 'Odysseus 'TeX)) -|y ([bingo _]) - -(%which (bingo) - (%knows 'Odysseus 'calculus)) -|y #f -} - -\subsection{ Asserting Extra Clauses} -\label{assert} - -We can add more clauses to a predicate after it has already -been defined with a \q{%rel}. Schelog provides the -\q{%assert} form for this purpose. Eg, - -\sverbatim{ -(%assert %knows () - [('Odysseus 'archery)]) -} - -\n tacks on a new clause at the end of the existing clauses -of the \q{%knows} -predicate. Now, the query: - -\sverbatim{ -(%which (what) - (%knows 'Odysseus what)) -} - -\n gives TeX, Scheme, Prolog, and Penelope, as before, but -a subsequent \q{(%more)} yields a new result: \q{archery}. - -The Schelog form \q{%assert-a} is similar to \q{%assert} but -adds clauses {\em before} any of the current clauses. - -Both \q{%assert} and \q{%assert-a} assume that the variable -they are adding to already names a predicate (presumably -defined using \q{%rel}). -In order to allow defining a predicate entirely through -\q{%assert}s, Schelog provides an empty predicate value -\q{%empty-rel}. \q{%empty-rel} takes any number of arguments -and always fails. A typical use of the -\q{%empty-rel} and \q{%assert} combination: - -\sverbatim{ -(define %parent %empty-rel) - -(%assert %parent () - [('Laertes 'Odysseus)]) - -(%assert %parent () - [('Odysseus 'Telemachus)] - [('Penelope 'Telemachus)]) -} - -(Schelog does not provide a predicate for {\em retracting} -assertions, since we can keep track of older versions of -predicates using conventional Scheme features (\q{let} and \q{set!}).) - -\subsection{Local Variables} -\label{local-vars} - -The local logic variables of \q{%rel}- and -\q{%which}-expressions are in reality introduced by the -Schelog syntactic form called \q{%let}. (\q{%rel} and -\q{%which} are macros written using \q{%let}.) - -\q{%let} introduces new lexically scoped logic variables. -Supposing, instead of - -\sverbatim{ -(%which (what) - (%knows 'Odysseus what)) -} - -\n we had asked - -\sverbatim{ -(%let (what) - (%which () - (%knows 'Odysseus what))) -} - -\n This query, too, succeeds five times, since -Odysseus knows five things. However, \q{%which} emits -bindings only for the local variables that {\em it} -introduces. Thus, this query emits \q{|t} five times before -\q{(%more)} finally returns \q{#f}. - -\newsection{Using Conventional Scheme Expressions in Schelog} -\label{scheme-w-schelog} - -The arguments of Schelog predicates can be any Scheme -objects. In particular, composite structures such as lists, -vectors and strings can be used, as also Scheme expressions -using the full array of Scheme's construction and -decomposition operators. For instance, consider the -following goal: - -\sverbatim{ -(%member x '(1 2 3)) -} - -\n Here, \q{%member} is a predicate, \q{x} is a logic -variable, and \q{'(1 2 3)} is a structure. Given a suitably -intuitive definition for \q{%member}, the above goal -succeeds for \q{x} = \q{1}, \q{2}, and \q{3}. - -Now to defining predicates like \q{%member}: - -\sverbatim{ -(define %member - (%rel (x y xs) - [(x (cons x xs))] - [(x (cons y xs)) - (%member x xs)])) -} - -\n Ie, \q{%member} is defined with three local variables: -\q{x}, \q{y}, \q{xs}. It has two -clauses, identifying the two ways of determining membership. - -The first clause of \q{%member} states a fact: For any -\q{x}, \q{x} is a member of a list whose head is also \q{x}. - -The second clause of \q{%member} is a rule: \q{x} is a -member of a list if we can show that it is a member of the -{\em tail} of that list. In other words, the original -\q{%member} goal is translated into a {\em sub}goal, which is also -a \q{%member} goal. - -Note that the variable \q{y} in the definition of -\q{%member} occurs only once in the second clause. As such, -it doesn't need you to make the effort of naming it. (Names -help only in matching a second occurrence to a first.) Schelog -lets you use the expression \q{(_)} to denote an anonymous -variable. (Ie, \q{_} is a thunk that generates a fresh -anonymous variable at each call.) The predicate \q{%member} can be -rewritten as - -\sverbatim{ -(define %member - (%rel (x xs) - [(x (cons x (_)))] - [(x (cons (_) xs)) - (%member x xs)])) -} - -\subsection{Constructors} -\label{constructors} - -We can use constructors --- Scheme procedures for creating -structures --- to simulate data types in Schelog. For -instance, let's define a natural-number data-type where -\q{0} denotes zero, and \q{(succ x)} denotes the natural number -whose immediate predecessor is \q{x}. The constructor -\q{succ} can -be defined in Scheme as: - -\sverbatim{ -(define succ - (lambda (x) - (vector 'succ x))) -} - -\n Addition and multiplication can be defined as: - -\sverbatim{ -(define %add - (%rel (x y z) - [(0 y y)] - [((succ x) y (succ z)) - (%add x y z)])) - -(define %times - (%rel (x y z z1) - [(0 y 0)] - [((succ x) y z) - (%times x y z1) - (%add y z1 z)])) -} - -\n We can do a lot of arithmetic with this in place. For -instance, the factorial predicate looks like: - -\sverbatim{ -(define %factorial - (%rel (x y y1) - [(0 (succ 0))] - [((succ x) y) - (%factorial x y1) - (%times (succ x) y1 y)])) -} - -\subsection{\tt\%is} -\label{is} - -The above is a very inefficient way to do arithmetic, -especially when the underlying language Scheme offers -excellent arithmetic facilities (including a comprehensive -number ``tower'' and exact rational arithmetic). One -problem with using Scheme calculations directly in Schelog -clauses is that the expressions used may contain logic -variables that need to be dereferenced. Schelog provides -the predicate \q{%is} that takes care of this. The goal - -\sverbatim{ -(%is X E) -} - -\n unifies \q{X} with the value of \q{E} considered as a -Scheme expression. \q{E} can have logic variables, but -usually they should at least be bound, as unbound variables -may not be palatable values to the Scheme operators used in -\q{E}. - -We can now directly use the numbers of Scheme to write a -more efficient \q{%factorial} predicate: - -\sverbatim{ -(define %factorial - (%rel (x y x1 y1) - [(0 1)] - [(x y) (%is x1 (- x 1)) - (%factorial x1 y1) - (%is y (* y1 x))])) -} - -\n A price that this efficiency comes with is that we can -use \q{%factorial} only with its first argument already -instantiated. In many cases, this is not an unreasonable -constraint. In fact, given this limitation, there is -nothing to prevent us from using Scheme's factorial -directly: - -\sverbatim{ -(define %factorial - (%rel (x y) - [(x y) - (%is y (scheme-factorial - x))])) -} - -\n or better yet, ``in-line'' any calls to \q{%factorial} with -\q{%is}-expressions calling \q{scheme-factorial}, where the -latter is defined in the usual manner: - -\sverbatim{ -(define scheme-factorial - (lambda (n) - (if (= n 0) 1 - (* n (factorial - (- n 1)))))) -} - -\subsection{Lexical Scoping} -\label{lexical-scoping} - -One can use Scheme's lexical scoping to enhance predicate -definition. Here is a list-reversal predicate defined using -a hidden auxiliary predicate: - -\sverbatim{ -(define %reverse - (letrec - ([revaux - (%rel (x y z w) - [('() y y)] - [((cons x y) z w) - (revaux y - (cons x z) w)])]) - (%rel (x y) - [(x y) (revaux x '() y)]))) -} - -\n \q{(revaux X Y Z)} uses \q{Y} as an accumulator for -reversing \q{X} into \q{Z}. (\q{Y} starts out as \q{()}. -Each head of \q{X} is \q{cons}ed on to \q{Y}. Finally, when -\q{X} has wound down to \q{()}, \q{Y} contains the reversed -list and can be returned as \q{Z}.) - -\q{revaux} is used purely as a helper predicate for -\q{%reverse}, and so it can be concealed within a lexical -contour. We use \q{letrec} instead of \q{let} because -\q{revaux} is a recursive procedure. - -\subsection{Type Predicates} -\label{type-predicates} - -Schelog provides a couple of predicates that let the user -probe the type of objects. - -The goal - -\sverbatim{ -(%constant X) -} - -\n succeeds if \q{X} is an {\em atomic} object, ie, not a -list or vector. - -The predicate \q{%compound}, the negation of \q{%constant}, -checks if its argument is indeed a list or a vector. - -The above are merely the logic-program\-ming equivalents of -corresponding Scheme predicates. Users can use the -predicate \q{%is} and Scheme predicates to write more type -checks in Schelog. Thus, to test if \q{X} is a string, the -following goal could be used: - -\sverbatim{ -(%is #t (string? X)) -} - -\n User-defined Scheme predicates, in addition to primitive Scheme -predicates, can be thus imported. - -\newsection{Backtracking} -\label{backtracking} - -It is helpful to go into the following evaluation (sec \ref{rules}) -in a -little detail: - -\sverbatim{ -(%which () - (%computer-literate 'Penelope)) -|y |t -} - -\n The starting goal -is: - -\sverbatim{ -G0 = (%computer-literate Penelope) -} - -\n (I've taken out the quote because \q{Penelope} is the result -of evaluating \q{'Penelope}.) - -Schelog tries to match this with the head of the first -clause of \q{%computer-literate}. It succeeds, generating a -binding \q{[person Penelope]}. - -But this means it now has two new goals --- {\em subgoals} ---- to solve. These are the goals in the body of the -matching clause, with the logic variables substituted by -their instantiations: - -\sverbatim{ -G1 = (%knows Penelope TeX) -G2 = (%knows Penelope Scheme) -} - -\n For \q{G1}, Schelog attempts matches with the clauses of -\q{%knows}, and succeeds at the fifth try. (There are no -subgoals in this case, because the bodies of these ``fact'' -clauses are empty, in contrast to the ``rule'' clauses of -\q{%computer-literate}.) -Schelog then tries to solve \q{G2} against the clauses of -\q{%knows}, and since there is no clause stating that -Penelope knows Scheme, it fails. - -All is not lost though. Schelog now {\em backtracks} to the -goal that was solved just before, viz., \q{G1}. It -{\em retries} \q{G1}, ie, tries to solve it in a -different way. -This entails searching down the previously unconsidered -\q{%knows} -clauses for \q{G1}, ie, the sixth onwards. Obviously, -Schelog fails again, because the fact that Penelope knows -TeX occurs only once. - -Schelog now backtracks to the goal before \q{G1}, ie, -\q{G0}. We abandon the current successful match with the -first clause-head of \q{%computer-literate}, and try the -next clause-head. Schelog succeeds, again producing a binding -\q{[person Penelope]}, and two new subgoals: - -\sverbatim{ -G3 = (%knows Penelope TeX) -G4 = (%knows Penelope Prolog) -} - -\n It is now easy to trace that Schelog finds both \q{G3} and \q{G4} to be -true. Since both of \q{G0}'s subgoals are true, \q{G0} is -itself considered true. And this is what Schelog reports. The -interested reader can now trace why the -following query has a different denouement: - -\sverbatim{ -(%which () - (%computer-literate 'Telemachus)) -|y #f -} - -\newsection{Unification} -\label{unification} - -When we say that a goal matches with a clause-head, we mean -that the predicate and argument positions line up. Before -making this comparison, Schelog dereferences all already -bound logic variables. The resulting structures are then -compared to see if they are recursively identical. Thus, -\q{1} unifies with \q{1}, and \q{(list 1 2)} with \q{'(1 -2)}; but \q{1} and -\q{2} do not unify, and neither do \q{'(1 2)} and \q{'(1 -3)}. - -In general, there could be quite a few uninstantiated logic -variables in the compared objects. Unification will then -endeavor to find the most natural way of binding these -variables so that we arrive at structurally identical -objects. Thus, \q{(list x 1)}, where \q{x} is an unbound logic -variable, unifies with \q{'(0 1)}, producing the -binding -\q{[x 0]}. - -Unification is thus a goal, and Schelog makes the unification predicate -available to the user as \q{%=}. Eg, - -\sverbatim{ -(%which (x) - (%= (list x 1) '(0 1)) -|y ([x 0]) -} - -\n Schelog also provides the predicate \q{%/=}, the {\em negation} of -\q{%=}. \q{(%/= X Y)} succeeds if and only if \q{X} does -{\em not} unify with \q{Y}. - -Unification goals constitute the basic subgoals that all -Schelog goals devolve to. A goal succeeds because all the -eventual unification subgoals that it decomposes to in at -least one of its subgoal-branching succeeded. It fails -because every possible subgoal-branching was thwarted by the -failure of a crucial unification subgoal. - -Going back to the example in sec \ref{backtracking}, the goal -\q{(%computer-literate 'Penelope)} succeeds because -(a) it unified with -\q{(%computer-literate person)}; and then (b) with the binding -\q{[person Penelope]} in place, \q{(%knows person 'TeX)} -unified with \q{(%knows 'Penelope 'TeX)} and -\q{(%knows person 'Prolog)} unified with \q{(%knows 'Penelope -'Prolog)}. - -In contrast, the goal \q{(%computer-literate 'Telemachus)} -fails because, with \q{[person Telemachus]}, -the subgoals \q{(%knows person 'Scheme)} and -\q{(%knows person 'Prolog)} have no facts they can -unify with. - -\subsection{The Occurs Check} - -A robust unification algorithm uses the {\em -occurs check}, which ensures that a logic variable -isn't bound to a structure that contains itself. -Not performing the check can cause the unification -to go into an infinite loop in some cases. On the -other hand, performing the occurs check greatly -increases the time taken by unification, even in cases -that wouldn't require the check. - -Schelog uses the global variable -\q{*schelog-use-occurs-check?*} to decide whether to -use the occurs check. By default, this variable is -\q{#f}, ie, Schelog disables the occurs check. To -enable the check, - -\q{ -(set! *schelog-use-occurs-check?* #t) -} - -\newsection{Conjuctions and Disjunctions} -\label{and-or} - -Goals may be combined using the forms \q{%and} -and \q{%or} -to form compound goals. (For \q{%not}, see sec \ref{not}.) -Eg, - -\sverbatim{ -(%which (x) - (%and (%member x '(1 2 3)) - (%< x 3))) -} - -\n gives solutions for \q{x} that satisfy both the -argument goals of the \q{%and}. -Ie, \q{x} should both be a member of \q{'(1 2 3)} -{\em and} be less than \q{3}. The first -solution is - -\sverbatim{ -([x 1]) -} - -\n Typing \q{(%more)} gives another solution: - -\sverbatim{ -([x 2]) -} - -\n There are no more solutions, because \q{[x 3]} satisfies -the first but not the second goal. - -Similarly, the query - -\sverbatim{ -(%which (x) - (%or (%member x '(1 2 3)) - (%member x '(3 4 5)))) -} - -\n lists all \q{x} that are members of either list. - -\sverbatim{ - ([x 1]) -(%more) |y ([x 2]) -(%more) |y ([x 3]) -(%more) |y ([x 3]) -(%more) |y ([x 4]) -(%more) |y ([x 5]) -} - -\n (Yes, \q{([x 3])} is listed twice.) - -We can rewrite the predicate \q{%computer-literate} -from sec \ref{rules} using \q{%and} and \q{%or}: - -\sverbatim{ -(define %computer-literate - (%rel (person) - [(person) - (%or - (%and (%knows person - 'TeX) - (%knows person - 'Scheme)) - (%and (%knows person - 'TeX) - (%knows person - 'Prolog)))])) -} - -\n Or, more succinctly: - -\sverbatim{ -(define %computer-literate - (%rel (person) - [(person) - (%and (%knows person - 'TeX) - (%or (%knows person - 'Scheme) - (%knows person - 'Prolog)))])) -} - -\n We can even dispense with the \q{%rel} altogether: - -\sverbatim{ -(define %computer-literate - (lambda (person) - (%and (%knows person - 'TeX) - (%or (%knows person - 'Scheme) - (%knows person - 'Prolog))))) -} - -\n This last looks like a conventional Scheme predicate -definition, and is arguably -the most readable format for a Scheme programmer. - -\newsection{Manipulating Logic Variables} -\label{lv-manip} - -Schelog provides special predicates for probing logic -variables, without risking their getting bound. - -\subsection{Checking for Variables} -\label{var} - -The goal - -\sverbatim{ -(%== X Y) -} - -\n succeeds if \q{X} and \q{Y} are {\em identical} objects. This -is not quite the unification predicate \q{%=}, for \q{%==} -doesn't touch unbound objects the way \q{%=} does. Eg, -\q{%==} will not equate an unbound logic variable with a -bound one, nor will it equate two unbound logic variables -unless they are the {\em same} variable. - -The predicate \q{%/==} is the negation of \q{%==}. - -The goal - -\sverbatim{ -(%var X) -} - -\n succeeds if \q{X} isn't completely bound --- ie, it has at -least one unbound logic variable in its innards. - -The predicate \q{%nonvar} is the negation of \q{%var}. - -\subsection{Preserving Variables} -\label{freeze} - -Schelog lets the user protect a term with variables from -unification by allowing that term to be treated as a -(completely) bound object. The predicates provided for this -purpose are -\q{%freeze}, -\q{%melt}, \q{%melt-new}, and \q{%copy}. - -The goal - -\sverbatim{ -(%freeze S F) -} - -\n unifies \q{F} to the frozen version of \q{S}. Any lack -of bindings in \q{S} are preserved no matter how much you -toss \q{F} about. - -The goal - -\sverbatim{ -(%melt F S) -} - -\n retrieves the object frozen in \q{F} into \q{S}. - -The goal - -\sverbatim{ -(%melt-new F S) -} - -\n is similar to \q{%melt}, -except that when \q{S} is made, the unbound variables in -\q{F} are replaced by brand-new unbound variables. - -The goal - -\sverbatim{ -(%copy S C) -} - -\n is an abbreviation for \q{(%freeze S F)} -followed by \q{(%melt-new F C)}. - -\newsection{The Cut ({\tt!})} -\label{cut} - -The cut (called \q{!}) is a special goal that is used to -prune backtracking options. Like the \q{%true} goal, the -cut goal too succeeds, when accosted by the Schelog -subgoaling engine. However, when a further subgoal down the -line fails, and time comes to retry the cut goal, Schelog -will refuse to try alternate clauses for the predicate in -whose definition the cut occurs. In other words, the cut -causes Schelog to commit to all the decisions made from the -time that the predicate was selected to match a subgoal till -the time the cut was satisfied. - -For example, consider again the \q{%factorial} -predicate, as defined in sec \ref{is}: - -\sverbatim{ -(define %factorial - (%rel (x y x1 y1) - [(0 1)] - [(x y) (%is x1 (- x 1)) - (%factorial x1 y1) - (%is y (* y1 x))])) -} - -\n Clearly, - -\sverbatim{ -(%which () - (%factorial 0 1)) |y |t -(%which (n) - (%factorial 0 n)) |y ([n 1]) -} - -\n But what if we asked for \q{(%more)} for either query? -Backtracking will try -the second clause of \q{%factorial}, and sure enough the -clause-head unifies, producing binding \q{[x 0]}. -We now get three subgoals. Solving the first, we get \q{[x1 --1]}, and then we have to solve \q{(%factorial -1 y1)}. It -is easy to see there is no end to this, as we fruitlessly -try to get the factorials of numbers that get more and more -negative. - -If we placed a cut at the first clause: - -\sverbatim{ -... -[(0 1) !] -... -} - -\n the attempt to find more solutions for \q{(%factorial 0 -1)} is nipped in the bud. - -Calling \q{%factorial} with a {\em negative} number would still cause an -infinite loop. To take care of that problem as well, we -use another cut: - -\sverbatim{ -(define %factorial - (%rel (x y x1 y1) - [(0 1) !] - [(x y) (< x 0) ! %fail] - [(x y) (%is x1 (- x 1)) - (%factorial x1 y1) - (%is y (* y1 x))])) -} - -Using {\em raw} cuts as above can get very confusing. For this -reason, it is advisable to use it hidden away in -well-understood abstractions. Two such common abstractions -are the conditional and negation. - -\subsection{Conditional Goals} -\label{if-then-else} - -An ``if ... then ... else ...'' predicate can be defined -as follows - -\sverbatim{ -(define %if-then-else - (%rel (p q r) - [(p q r) p ! q] - [(p q r) r])) -} - -\n (Note that for the first time we have predicate arguments that -are themselves goals.) - -Consider the goal - -\sverbatim{ -G0 = (%if-then-else Gbool - Gthen Gelse) -} - -\n We first unify \q{G0} with the first clause-head, -giving -\q{[p Gbool]}, \q{[q Gthen]}, \q{[r Gelse]}. \q{Gbool} can -now either succeed or fail. - -Case 1: If \q{Gbool} fails, backtracking will cause the -\q{G0} to unify with the second clause-head. \q{r} is bound -to \q{Gelse}, and so \q{Gelse} is tried, as expected. - -Case 2: If \q{Gbool} succeeds, the cut commits to this -clause of the \q{%if-then-else}. We now try \q{Gthen}. If -\q{Gthen} should now fail --- or even if we simply retry for -more solutions --- we are guaranteed that the second -clause-head will not be tried. If it were not for the cut, -\q{G0} would attempt to unify with the second clause-head, which will -of course succeed, and \q{Gelse} {\em will} be tried. - -\subsection{Negation as Failure} -\label{not} - -Another common abstraction using the cut is {\em negation}. -The negation of goal \q{G} is defined as \q{(%not G)}, where -the predicate \q{%not} is defined as follows: - -\sverbatim{ -(define %not - (%rel () - [(g) g ! %fail] - [(g) %true])) -} - -\n Thus, \q{g}'s negation is deemed a failure if \q{g} -succeeds, and a success if \q{g} fails. This is of course -confusing goal failure with falsity. In some cases, this -view of negation is actually helpful. - -\newsection{Set Predicates} -\label{set-of} - -The goal - -\sverbatim{ -(%bag-of X G Bag) -} - -\n unifies with \q{Bag} the list of all instantiations of -\q{X} for which \q{G} succeeds. Thus, the following query -asks for all the things known --- ie, the collection of things -such that someone knows them: - -\sverbatim{ -(%which (things-known) - (%let (someone x) - (%bag-of x (%knows someone x) - things-known))) -|y ([things-known - (TeX Scheme Prolog - Penelope TeX Prolog - Odysseus TeX calculus)]) -} - -\n This is the only solution for this goal: - -\sverbatim{ -(%more) |y #f -} - -\n Note that some things --- eg, TeX --- are enumerated -more than once. This is because more than one person knows -TeX. To remove duplicates, use the predicate -\q{%set-of} -instead of \q{%bag-of}: - -\sverbatim{ -(%which (things-known) - (%let (someone x) - (%set-of x (%knows someone x) - things-known))) -|y ([things-known - (TeX Scheme Prolog - Penelope Odysseus calculus)]) -} - -\n In the above, the free variable \q{someone} in the -\q{%knows}-goal is used as if it -were existentially quantified. In contrast, Prolog's -versions of -\q{%bag-of} and \q{%set-of} fix it for each solution of the -set-predicate goal. We can do it too with some additional -syntax that identifies the free variable. -Eg, - -\sverbatim{ -(%which (someone things-known) - (%let (x) - (%bag-of x - (%free-vars (someone) - (%knows someone x)) - things-known))) -|y ([someone Odysseus] - [things-known - (TeX Scheme Prolog - Penelope)]) -} - -\n The bag of things known by {\em one} someone is -returned. That someone is Odysseus. The query can be -retried for more solutions, each listing the things known by -a different someone: - -\sverbatim{ -(%more) |y ([someone Penelope] - [things-known - (TeX Prolog - Odysseus)]) -(%more) |y ([someone Telemachus] - [things-known - (TeX calculus)]) -(%more) |y #f -} - -Schelog also provides two variants of these set predicates, -viz., \q{%bag-of-1} and \q{%set-of-1}. These act like \q{%bag-of} -and \q{%set-of} but fail if the resulting bag or set is empty. - -\newsection{Glossary of Schelog Primitives} -\label{glossary} - -This section lists, in ascii order, all the Schelog -primitives, with a brief explanation for each. Each entry is -identified -\texonly - --- on the right-hand side of its entry title --- -\endtexonly -as either {\em procedure}, {\em macro}, {\em predicate}, -{\em goal}, or {\em flag}. (Note that predicates and goals are also -procedures. We nevertheless use the more specific names -because of their importance to Schelog programming.) - -Following Prolog style, a predicate's arity is also noted in -its title. Thus, \q{%<}\ar/2 means that \q{%<} takes two -arguments. Variable-arity predicates use an asterisk -instead of a number, eg, \q{%and}\ar/*. - -\defpred{\q{%/=}\ar/2} - -\q{%/=} is the negation of \q{%=}. -The goal \q{(%/= E1 E2)} succeeds if \q{E1} can not be unified -with \q{E2}. - -\defpred{\q{%/==}\ar/2} - -\q{%/==} is the negation of \q{%==}. -The goal \q{(%/== E1 E2)} succeeds if \q{E1} and \q{E2} are not -identical. - -\defpred{\q{%<}\ar/2} - -The goal \q{(%< E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is less than \q{E2}. - -\defpred{\q{%<=}\ar/2} - -The goal \q{(%<= E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is less than or equal to \q{E2}. - -\defpred{\q{%=}\ar/2} - -The goal \q{(%= E1 E2)} succeeds if \q{E1} can be unified with -\q{E2}. Any resulting bindings for logic variables are kept. - -\defpred{\q{%=/=}\ar/2} - -The goal \q{(%=/= E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is not equal to \q{E2}. - -\defpred{\q{%=:=}\ar/2} - -The goal \q{(%=:= E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is equal to \q{E2}. - -\defpred{\q{%==}\ar/2} - -The goal \q{(%== E1 E2)} succeeds if \q{E1} is {\em identical} -to \q{E2}. They should be structurally equal. If containing -logic variables, they should have the same variables in the -same position. Unlike a \q{%=}-call, this goal will not bind -any logic variables. - -\defpred{\q{%>}\ar/2} - -The goal \q{(%> E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is greater than \q{E2}. - -\defpred{\q{%>=}\ar/2} - -The goal \q{(%>= E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is greater than or equal to \q{E2}. - -\defmac{\q{%and}\ar/*} - -The goal \q{(%and G ...)} succeeds if all the goals -\q{G}, ..., succeed. - -\defpred{\q{%append}\ar/3} - -The goal \q{(%append E1 E2 E3)} succeeds if \q{E3} is unifiable -with the list obtained by appending \q{E1} and \q{E2} - -\defmac{\q{%assert}} - -The form \q{(%assert Pname (V ...) C ...)} adds the clauses -\q{C}, ..., to the {\em end} of the predicate that is the value of -the Scheme variable \q{Pname}. The variables \q{V}, ..., are -local logic variables for \q{C}, ... - -\defmac{\q{%assert-a}} - -Like \q{%assert}, but adds the new clauses to the {\em front} -of the existing predicate. - -\defpred{\q{%bag-of}\ar/3} - -The goal \q{(%bag-of E1 G E2)} unifies with \q{E2} the {\em bag} -(multiset) -of all the -instantiations of \q{E1} for which goal \q{G} succeeds. - -\defpred{\q{%bag-of-1}\ar/3} - -Similar to \q{%bag-of}, but fails if the bag is empty. - -\defpred{\q{%compound}\ar/1} - -The goal \q{(%compound E)} succeeds if \q{E} is a non-atomic -structure, ie, a vector or a list. - -\defpred{\q{%constant}\ar/1} - -The goal \q{(%compound E)} succeeds if \q{E} is an atomic -structure, ie, not a vector or a list. - -\defpred{\q{%copy}\ar/2} - -The goal \q{(%copy F S)} unifies with \q{S} a copy of the -frozen structure in \q{F}. - -\defpred{\q{%empty-rel}\ar/*} - -The goal \q{(%empty-rel E ...)} always fails. The {\em value} -\q{%empty-rel} is used as a starting value for predicates -that can later be enhanced with \q{%assert} and \q{%assert-a}. - -\defgoal{\q{%fail}} - -The goal \q{%fail} always fails. - -\defmac{\q{%free-vars}} - -The form \q{(%free-vars (V ...) G)} identifies -the occurrences of the variables \q{V}, ..., in goal -\q{G} as free. It is used to avoid existential quantification -in calls to set predicates (\q{%bag-of}, \q{%set-of}, \&c.). - -\defpred{\q{%freeze}\ar/2} - -The goal \q{(%freeze S F)} unifies with \q{F} a new frozen -version of the structure in \q{S}. Freezing implies that all -the unbound variables are preserved. \q{F} can henceforth be -used as {\em bound} object with no fear of its variables -getting bound by unification. - -\defpred{\q{%if-then-else}\ar/3} - -The goal \q{(%if-then-else G1 G2 G3)} tries \q{G1} first: if it -succeeds, tries \q{G2}; if not, tries \q{G3}. - -\defpred{\q{%is}\ar/2} - -The goal \q{(%is E1 E2)} unifies with \q{E1} the result of -evaluating \q{E2} as a Scheme expression. \q{E2} may contain -logic variables, which are dereferenced automatically. -Fails if \q{E2} contains unbound logic variables. -(Note: Unlike other Schelog predicates, \q{%is} is implemented -as a macro and not a procedure.) - -\defmac{\q{%let}} - -The form \q{(%let (V ...) E ...)} introduces \q{V}, ..., as -lexically scoped logic variables to be used in \q{E}, ... - -\defpred{\q{%melt}\ar/2} - -The goal \q{(%melt F S)} unifies \q{S} with the thawed -(original) form of the frozen structure in \q{F}. - -\defpred{\q{%melt-new}\ar/2} - -The goal \q{(%melt-new F S)} unifies \q{S} with a thawed -{\em copy} of the frozen structure in \q{F}. This means -new logic variables are used for unbound logic variables in -\q{F} - -\defpred{\q{%member}\ar/2} - -The goal \q{(%member E1 E2)} succeeds if \q{E1} is a member -of the list in \q{E2}. - -\defpred{\q{%nonvar}\ar/1} - -\q{%nonvar} is the negation of \q{%var}. -The goal \q{(%nonvar E)} succeeds if \q{E} is completely -instantiated, ie, it has no unbound variable in it. - -\defpred{\q{%not}\ar/1} - -The goal \q{(%not G)} succeeds if \q{G} fails. - -\defproc{\q{%more}} - -The thunk \q{%more} produces more instantiations of the -variables in the most recent \q{%which}-form that satisfy the -goals in that \q{%which}-form. If no more solutions can -be found, \q{%more} returns \q{#f}. - -\defmac{\q{%or}\ar/*} - -The goal \q{(%or G ...)} succeeds if one of \q{G}, ..., tried -in that order, succeeds. - -\defmac{\q{%rel}} - -The form \q{(%rel (V ...) C ...)} creates a predicate object. -Each clause \q{C} is of the form \q{[(E ...) G ...]}, signifying -that the goal created by applying the predicate object to -anything that matches \q{(E ...)} is deemed to succeed if all -the goals \q{G}, ..., can, in their turn, be shown to succeed. - -\defpred{\q{%repeat}\ar/0} - -The goal \q{(%repeat)} always succeeds (even on retries). -Used for failure-driven loops. - -\defflag{\q{*schelog-use-occurs-check?*}} - -If the global flag -\q{*schelog-use-occurs-check?*} is false (the default), -Schelog's unification will not use the occurs check. -If it is true, the occurs check is enabled. - -\defpred{\q{%set-of}\ar/3} - -The goal \q{(%set-of E1 G E2)} unifies with \q{E2} the {\em set} -of all the -instantiations of \q{E1} for which goal \q{G} succeeds. - -\defpred{\q{%set-of-1}\ar/3} - -Similar to \q{%set-of}, but fails if the set is empty. - -\defgoal{\q{%true}} - -The goal \q{%true} succeeds. Fails on retry. - -\defpred{\q{%var}\ar/1} - -The goal \q{(%var E)} succeeds if \q{E} is not completely -instantiated, ie, it has at least one unbound variable in -it. - -\defmac{\q{%which}} - -The form \q{(%which (V ...) G ...)} returns an instantiation -of the variables \q{V}, ..., that satisfies all of \q{G}, -... If \q{G}, ..., cannot be satisfied, returns \q{#f}. -Calling the thunk \q{%more} produces more -instantiations, if available. - -\defproc{\q{_} ~~(underscore)} - -A thunk that produces a new logic variable. Can be -used in situations where we want a logic variable but -don't want to name it. (\q{%let}, in contrast, introduces new -lexical names for the logic variables it creates.) - -\newsection{References} -\label{references} - - -\bibliographystyle{plain} -\bibliography{schelog} - -\bye diff --git a/collects/schelog/examples/bible.rkt b/collects/tests/schelog/bible.rkt similarity index 79% rename from collects/schelog/examples/bible.rkt rename to collects/tests/schelog/bible.rkt index 7a055e10ea..88039d52c2 100644 --- a/collects/schelog/examples/bible.rkt +++ b/collects/tests/schelog/bible.rkt @@ -1,6 +1,6 @@ #lang racket -(require "../schelog.rkt" +(require schelog schemeunit) ;The following is the "Biblical" database from "The Art of @@ -9,7 +9,7 @@ ;(%father X Y) :- X is the father of Y. (define %father - (%rel ! () + (%rel () (('terach 'abraham)) (('terach 'nachor)) (('terach 'haran)) (('abraham 'isaac)) (('haran 'lot)) (('haran 'milcah)) (('haran 'yiscah)))) @@ -17,14 +17,14 @@ ;(%mother X Y) :- X is the mother of Y. (define %mother - (%rel ! () (('sarah 'isaac)))) + (%rel () (('sarah 'isaac)))) (define %male - (%rel ! () + (%rel () (('terach)) (('abraham)) (('isaac)) (('lot)) (('haran)) (('nachor)))) (define %female - (%rel ! () + (%rel () (('sarah)) (('milcah)) (('yiscah)))) ;AoP, ch. 17. Finding all the children of a particular @@ -36,13 +36,13 @@ (define %children-1 (letrec ((children-aux - (%rel ! (x a cc c) + (%rel (x a cc c) ((x a cc) (%father x c) (%not (%member c a)) ! (children-aux x (cons c a) cc)) ((x cc cc))))) - (%rel ! (x cc) + (%rel (x cc) ((x cc) (children-aux x '() cc))))) (define terachs-kids-test @@ -53,7 +53,7 @@ (%children-1 'terach cc)))) (check-equal? (terachs-kids-test) - `((cc (haran nachor abraham)))) + `((cc . (haran nachor abraham)))) (define dad-kids-test ;find a father and all his children. Returns @@ -65,7 +65,7 @@ (%children-1 f cc)))) (check-equal? (dad-kids-test) - `((f terach) (cc (haran nachor abraham)))) + `((f . terach) (cc . (haran nachor abraham)))) (define terachs-kids-test-2 ;find all the kids of Terach, using %set-of. @@ -75,11 +75,14 @@ (%which (kk) (%set-of k (%father 'terach k) kk))))) +(check-equal? (terachs-kids-test-2) + `((kk . (abraham nachor haran)))) + ;This is a better definition of the %children predicate. ;Uses set predicate %bag-of (define %children - (%rel ! (x kids c) + (%rel (x kids c) ((kids) (%set-of c (%father x c) kids)))) (define dad-kids-test-2 @@ -93,6 +96,9 @@ (%father dad x)) kids))))) +(check-equal? (dad-kids-test-2) + `((dad . terach) (kids . (abraham nachor haran)))) + (define dad-kids-test-3 ;looks like dad-kids-test-2, but dad is now ;existentially quantified. returns a set of @@ -103,6 +109,9 @@ (%set-of x (%father dad x) kids))))) +(check-equal? (dad-kids-test-3) + `((dad . _) (kids . (abraham nachor haran isaac lot milcah yiscah)))) + (define dad-kids-test-4 ;find the set of dad-kids. ;since dad is existentially quantified, @@ -115,6 +124,9 @@ (%set-of x (%father dad x) kids) dad-kids))))) +(check-equal? (dad-kids-test-4) + `((dad-kids . ((_ (abraham nachor haran isaac lot milcah yiscah)))))) + (define dad-kids-test-5 ;the correct solution. dad is ;identified as a free var. @@ -128,3 +140,6 @@ (%father dad x)) kids) dad-kids))))) + +(check-equal? (dad-kids-test-5) + `((dad-kids . ((terach (abraham nachor haran)) (abraham (isaac)) (haran (lot milcah yiscah)))))) \ No newline at end of file diff --git a/collects/schelog/examples/england.rkt b/collects/tests/schelog/england.rkt similarity index 87% rename from collects/schelog/examples/england.rkt rename to collects/tests/schelog/england.rkt index 3a911d6400..7a4ae74535 100644 --- a/collects/schelog/examples/england.rkt +++ b/collects/tests/schelog/england.rkt @@ -1,6 +1,6 @@ #lang racket -(require "../schelog.rkt" +(require schelog schemeunit) ;The following is a simple database about a certain family in England. @@ -11,47 +11,47 @@ ;The file england2.scm uses a Scheme-like syntax. (define %male - (%rel ! () + (%rel () (('philip)) (('charles)) (('andrew)) (('edward)) (('mark)) (('william)) (('harry)) (('peter)))) (define %female - (%rel ! () + (%rel () (('elizabeth)) (('anne)) (('diana)) (('sarah)) (('zara)))) (define %husband-of - (%rel ! () + (%rel () (('philip 'elizabeth)) (('charles 'diana)) (('mark 'anne)) (('andrew 'sarah)))) (define %wife-of - (%rel ! (w h) + (%rel (w h) ((w h) (%husband-of h w)))) (define %married-to - (%rel ! (x y) + (%rel (x y) ((x y) (%husband-of x y)) ((x y) (%wife-of x y)))) (define %father-of - (%rel ! () + (%rel () (('philip 'charles)) (('philip 'anne)) (('philip 'andrew)) (('philip 'edward)) (('charles 'william)) (('charles 'harry)) (('mark 'peter)) (('mark 'zara)))) (define %mother-of - (%rel ! (m c f) + (%rel (m c f) ((m c) (%wife-of m f) (%father-of f c)))) (define %child-of - (%rel ! (c p) + (%rel (c p) ((c p) (%father-of p c)) ((c p) (%mother-of p c)))) (define %parent-of - (%rel ! (p c) + (%rel (p c) ((p c) (%child-of c p)))) (define %brother-of - (%rel ! (b x f) + (%rel (b x f) ((b x) (%male b) (%father-of f b) (%father-of f x) (%/= b x)))) diff --git a/collects/schelog/examples/england2.rkt b/collects/tests/schelog/england2.rkt similarity index 98% rename from collects/schelog/examples/england2.rkt rename to collects/tests/schelog/england2.rkt index aecc98f3aa..ab1775b629 100644 --- a/collects/schelog/examples/england2.rkt +++ b/collects/tests/schelog/england2.rkt @@ -1,6 +1,6 @@ #lang racket -(require "../schelog.rkt") +(require schelog) ;The following is a simple database about a certain family in England. ;Should be a piece of cake, but given here so that you can hone diff --git a/collects/tests/schelog/fac.rkt b/collects/tests/schelog/fac.rkt new file mode 100644 index 0000000000..c9667ee687 --- /dev/null +++ b/collects/tests/schelog/fac.rkt @@ -0,0 +1,26 @@ +#lang racket +(require schelog tests/eli-tester) + +(define %factorial + (%rel (x y x1 y1) + [(0 1) !] + [(x y) (%< x 0) ! %fail] + [(x y) (%is x1 (- x 1)) + (%factorial x1 y1) + (%is y (* y1 x))])) + +(test + (%which () + (%factorial 0 1)) + => empty + (%more) + => #f + + (%which () + (%factorial -1 1)) + => #f + (%which (x) + (%factorial 3 x)) + => `((x . 6)) + (%more) + => #f) \ No newline at end of file diff --git a/collects/schelog/examples/games.rkt b/collects/tests/schelog/games.rkt similarity index 83% rename from collects/schelog/examples/games.rkt rename to collects/tests/schelog/games.rkt index 9575a08595..4fb251f8b7 100644 --- a/collects/schelog/examples/games.rkt +++ b/collects/tests/schelog/games.rkt @@ -1,6 +1,6 @@ -#lang scheme +#lang racket -(require "../schelog.rkt" +(require schelog "./puzzle.rkt" schemeunit) @@ -20,7 +20,7 @@ (list 'person name country sport))) (define %games - (%rel ! (clues queries solution the-men + (%rel (clues queries solution the-men n1 n2 n3 c1 c2 c3 s1 s2 s3) ((clues queries solution) (%= the-men @@ -29,7 +29,7 @@ (%games-queries the-men queries solution)))) (define %games-clues - (%rel ! (the-men clue1-man1 clue1-man2 clue2-man1 clue2-man2 clue3-man) + (%rel (the-men clue1-man1 clue1-man2 clue2-man1 clue2-man2 clue3-man) ((the-men (list (%did-better clue1-man1 clue1-man2 the-men) @@ -46,7 +46,7 @@ (%sport clue3-man 'cricket)))))) (define %games-queries - (%rel ! (the-men man1 man2 aussies-name dicks-sport) + (%rel (the-men man1 man2 aussies-name dicks-sport) ((the-men (list (%member man1 the-men) @@ -61,25 +61,25 @@ (list 'richard 'plays dicks-sport)))))) (define %did-better - (%rel ! (a b c) + (%rel (a b c) ((a b (list a b c))) ((a c (list a b c))) ((b c (list a b c))))) (define %name - (%rel ! (name country sport) + (%rel (name country sport) (((person name country sport) name)))) (define %country - (%rel ! (name country sport) + (%rel (name country sport) (((person name country sport) country)))) (define %sport - (%rel ! (name country sport) + (%rel (name country sport) (((person name country sport) sport)))) (define %first - (%rel ! (car cdr) + (%rel (car cdr) (((cons car cdr) car)))) ;;With the above as the database, and also loading the file @@ -89,4 +89,4 @@ ;;((michael is the australian) (richard plays tennis)) (check-equal? (solve-puzzle %games) - '((solution= ((michael is the australian) (richard plays tennis))))) + '((solution= . ((michael is the australian) (richard plays tennis))))) diff --git a/collects/schelog/examples/holland.rkt b/collects/tests/schelog/holland.rkt similarity index 50% rename from collects/schelog/examples/holland.rkt rename to collects/tests/schelog/holland.rkt index c7aa0b8be1..79f39fd4b5 100644 --- a/collects/schelog/examples/holland.rkt +++ b/collects/tests/schelog/holland.rkt @@ -1,6 +1,7 @@ #lang racket -(require "../schelog.rkt") +(require schelog + tests/eli-tester) ;This is a very trivial program. In Prolog, it would be: ; @@ -12,29 +13,34 @@ (define %city (lambda (x) (%or (%= x 'amsterdam) - (%= x 'brussels)))) + (%= x 'brussels)))) (define %country (lambda (x) (%or (%= x 'holland) - (%= x 'belgium)))) + (%= x 'belgium)))) ;For a more Prolog-style syntax, you can rewrite the same thing, ;using the `%rel' macro, as the following: -'(define %city +(define %city* (%rel () - (('amsterdam)) - (('brussels)))) + (('amsterdam)) + (('brussels)))) -'(define %country +(define %country* (%rel () - (('holland)) - (('belgium)))) + (('holland)) + (('belgium)))) ;Typical easy queries: -; -; (%which (x) (%city x)) succeeds twice -; (%which (x) (%country x)) succeeds twice -; (%which () (%city 'amsterdam)) succeeds -; (%which () (%country 'amsterdam)) fails +(test + (%which (x) (%city x)) + (%more) + (%more) => #f + (%which (x) (%country x)) + (%more) + (%more) => #f + (%which () (%city 'amsterdam)) + (%more) => #f + (%which () (%country 'amsterdam)) => #f) diff --git a/collects/schelog/examples/houses.rkt b/collects/tests/schelog/houses.rkt similarity index 80% rename from collects/schelog/examples/houses.rkt rename to collects/tests/schelog/houses.rkt index 08e4601215..9b73f589a9 100644 --- a/collects/schelog/examples/houses.rkt +++ b/collects/tests/schelog/houses.rkt @@ -1,6 +1,6 @@ #lang racket -(require "../schelog.rkt") +(require schelog) ;Exercise 14.1 (iv) from Sterling & Shapiro, p. 217-8 @@ -29,25 +29,25 @@ (lambda (hue nation pet drink cigarette) (list 'house hue nation pet drink cigarette))) -(define %hue (%rel ! (h) (((house h (_) (_) (_) (_)) h)))) -(define %nation (%rel ! (n) (((house (_) n (_) (_) (_)) n)))) -(define %pet (%rel ! (p) (((house (_) (_) p (_) (_)) p)))) -(define %drink (%rel ! (d) (((house (_) (_) (_) d (_)) d)))) -(define %cigarette (%rel ! (c) (((house (_) (_) (_) (_) c) c)))) +(define %hue (%rel (h) (((house h (_) (_) (_) (_)) h)))) +(define %nation (%rel (n) (((house (_) n (_) (_) (_)) n)))) +(define %pet (%rel (p) (((house (_) (_) p (_) (_)) p)))) +(define %drink (%rel (d) (((house (_) (_) (_) d (_)) d)))) +(define %cigarette (%rel (c) (((house (_) (_) (_) (_) c) c)))) (define %adjacent - (%rel ! (a b) + (%rel (a b) ((a b (list a b (_) (_) (_)))) ((a b (list (_) a b (_) (_)))) ((a b (list (_) (_) a b (_)))) ((a b (list (_) (_) (_) a b))))) (define %middle - (%rel ! (a) + (%rel (a) ((a (list (_) (_) a (_) (_)))))) (define %houses - (%rel ! (row-of-houses clues queries solution + (%rel (row-of-houses clues queries solution h1 h2 h3 h4 h5 n1 n2 n3 n4 n5 p1 p2 p3 p4 p5 d1 d2 d3 d4 d5 c1 c2 c3 c4 c5) ((clues queries solution) @@ -62,7 +62,7 @@ (%houses-queries row-of-houses queries solution)))) (define %houses-clues - (%rel ! (row-of-houses abode1 abode2 abode3 abode4 abode5 abode6 abode7 + (%rel (row-of-houses abode1 abode2 abode3 abode4 abode5 abode6 abode7 abode8 abode9 abode10 abode11 abode12 abode13 abode14 abode15) ((row-of-houses (list @@ -126,7 +126,7 @@ (%hue abode15 'blue)))))) (define %houses-queries - (%rel ! (row-of-houses abode1 abode2 zebra-owner water-drinker) + (%rel (row-of-houses abode1 abode2 zebra-owner water-drinker) ((row-of-houses (list (%member abode1 row-of-houses) @@ -140,13 +140,9 @@ (list (list zebra-owner 'owns 'the 'zebra) (list water-drinker 'drinks 'water)))))) -;Load puzzle.scm and type (solve-puzzle %houses) - -;Note: This program, as written, requires -;the occurs check. Make sure the global -;*schelog-use-occurs-check?* is set to #t before -;calling solve-puzzle. If not, you will get into -;an infinite loop. - -;Note 2: Perhaps there is a way to rewrite the +;Note: Perhaps there is a way to rewrite the ;program so that it doesn't rely on the occurs check. + +(require "puzzle.rkt" tests/eli-tester) +(use-occurs-check? #t) +(test (solve-puzzle %houses)) diff --git a/collects/schelog/examples/mapcol.rkt b/collects/tests/schelog/mapcol.rkt similarity index 81% rename from collects/schelog/examples/mapcol.rkt rename to collects/tests/schelog/mapcol.rkt index 3c0de24d9c..172f36b623 100644 --- a/collects/schelog/examples/mapcol.rkt +++ b/collects/tests/schelog/mapcol.rkt @@ -1,6 +1,6 @@ #lang racket -(require (except-in "../schelog.rkt" %member)) +(require (except-in schelog %member)) ;map coloring, example from Sterling & Shapiro, p. 212 @@ -9,21 +9,21 @@ ;; is this different from the %member provided by schelog? fencing that one out. (define %member - (%rel ! (X Xs Y Ys) + (%rel (X Xs Y Ys) ((X (cons X Xs))) ((X (cons Y Ys)) (%member X Ys)))) ;(%members x y) holds if x is a subset of y (define %members - (%rel ! (X Xs Ys) + (%rel (X Xs Ys) (((cons X Xs) Ys) (%member X Ys) (%members Xs Ys)) (('() Ys)))) ;(%select x y z) holds if z is y with one less occurrence of x (define %select - (%rel ! (X Xs Y Ys Zs) + (%rel (X Xs Y Ys Zs) ((X (cons X Xs) Xs)) ((X (cons Y Ys) (cons Y Zs)) (%select X Ys Zs)))) @@ -35,26 +35,26 @@ (list 'region name color neighbors))) (define %color-map - (%rel ! (Region Regions Colors) + (%rel (Region Regions Colors) (((cons Region Regions) Colors) (%color-region Region Colors) (%color-map Regions Colors)) (('() Colors)))) (define %color-region - (%rel ! (Name Color Neighbors Colors Colors1) + (%rel (Name Color Neighbors Colors Colors1) (((region Name Color Neighbors) Colors) (%select Color Colors Colors1) (%members Neighbors Colors1)))) (define %test-color - (%rel ! (Name Map Colors) + (%rel (Name Map Colors) ((Name Map) (%map Name Map) (%colors Colors) (%color-map Map Colors)))) (define %map - (%rel ! (A B C D E F G H I L P S) + (%rel (A B C D E F G H I L P S) (('test (list (region 'a A (list B C D)) (region 'b B (list A C E)) @@ -76,10 +76,9 @@ (region 'austria A (list I S G))))))) (define %colors - (%rel ! () + (%rel () (('(red yellow blue white))))) -;ask (%which (M) (%test-color 'test M)) or -;ask (%which (M) (%test-color 'western-europe M)) for the -;respective (non-unique) colorings. - +(require tests/eli-tester) +(test (%which (M) (%test-color 'test M)) + (%which (M) (%test-color 'western-europe M))) diff --git a/collects/schelog/examples/puzzle.rkt b/collects/tests/schelog/puzzle.rkt similarity index 92% rename from collects/schelog/examples/puzzle.rkt rename to collects/tests/schelog/puzzle.rkt index 302fcd9594..6598f71b9a 100644 --- a/collects/schelog/examples/puzzle.rkt +++ b/collects/tests/schelog/puzzle.rkt @@ -1,6 +1,6 @@ -#lang scheme +#lang racket -(require "../schelog.rkt") +(require schelog) (provide (all-defined-out)) @@ -19,13 +19,13 @@ ; solve([]). (define %solve-puzzle - (%rel ! (clues queries solution) + (%rel (clues queries solution) ((clues queries solution) (%solve clues) (%solve queries)))) (define %solve - (%rel ! (clue clues) + (%rel (clue clues) (((cons clue clues)) clue (%solve clues)) diff --git a/collects/tests/schelog/run-all.rkt b/collects/tests/schelog/run-all.rkt new file mode 100644 index 0000000000..b4a1bce97d --- /dev/null +++ b/collects/tests/schelog/run-all.rkt @@ -0,0 +1,9 @@ +#lang racket +(require racket/runtime-path tests/eli-tester) +(define-runtime-path here ".") +(define this-file (build-path "run-all.rkt")) + +(test + (for ([p (in-list (directory-list here))] + #:when (not (equal? this-file p))) + (dynamic-require (build-path here p) #f))) \ No newline at end of file diff --git a/collects/schelog/examples/toys.rkt b/collects/tests/schelog/toys.rkt similarity index 80% rename from collects/schelog/examples/toys.rkt rename to collects/tests/schelog/toys.rkt index 628a071dea..73033d4b08 100644 --- a/collects/schelog/examples/toys.rkt +++ b/collects/tests/schelog/toys.rkt @@ -1,6 +1,6 @@ #lang racket -(require (except-in "../schelog.rkt" %append)) +(require (except-in schelog %append)) ;A list of trivial programs in Prolog, just so you can get used ;to schelog syntax. @@ -8,14 +8,14 @@ ;(%length l n) holds if length(l) = n (define %length - (%rel ! (h t n m) + (%rel (h t n m) (('() 0)) (((cons h t) n) (%length t m) (%is n (+ m 1))))) ;(%delete x y z) holds if z is y with all x's removed (define %delete - (%rel ! (x y z w) + (%rel (x y z w) ((x '() '())) ((x (cons x w) y) (%delete x w y)) ((x (cons z w) (cons z y)) (%not (%= x z)) (%delete x w y)))) @@ -23,39 +23,39 @@ ;(%remdup x y) holds if y is x without duplicates (define %remdup - (%rel ! (x y z w) + (%rel (x y z w) (('() '())) (((cons x y) (cons x z)) (%delete x y w) (%remdup w z)))) ;(%count x n) holds if n is the number of elements in x without ;counting duplicates -'(define %count - (%rel ! (x n y) +(define %count* + (%rel (x n y) ((x n) (%remdup x y) (%length y n)))) ;same thing (define %count (letrec ((countaux - (%rel ! (m n m+1 x y z) + (%rel (m n m+1 x y z) (('() m m)) (((cons x y) m n) (%delete x y z) (%is m+1 (+ m 1)) (countaux z m+1 n))))) - (%rel ! (x n) + (%rel (x n) ((x n) (countaux x 0 n))))) ;(%append x y z) holds if z is the concatenation of x and y (define %append - (%rel ! (x y z w) + (%rel (x y z w) (('() x x)) (((cons x y) z (cons x w)) (%append y z w)))) ;(%reverse x y) holds if the y is the reversal of x -'(define %reverse - (%rel ! (x y z yy) +(define %reverse* + (%rel (x y z yy) (('() '())) (((cons x y) z) (%reverse y yy) (%append yy (list x) z)))) @@ -63,16 +63,16 @@ (define %reverse (letrec ((revaux - (%rel ! (x y z w) + (%rel (x y z w) (('() y y)) (((cons x y) z w) (revaux y (cons x z) w))))) - (%rel ! (x y) + (%rel (x y) ((x y) (revaux x '() y))))) ;(%fact n m) holds if m = n! -'(define %fact - (%rel ! (n n! n-1 n-1!) +(define %fact* + (%rel (n n! n-1 n-1!) ((0 1)) ((n n!) (%is n-1 (- n 1)) (%fact n-1 n-1!) (%is n! (* n n-1!))))) @@ -80,9 +80,9 @@ (define %fact (letrec ((factaux - (%rel ! (n! m x m-1 xx) + (%rel (n! m x m-1 xx) ((0 n! n!)) ((m x n!) (%is m-1 (- m 1)) (%is xx (* x m)) (factaux m-1 xx n!))))) - (%rel ! (n n!) + (%rel (n n!) ((n n!) (factaux n 1 n!))))) diff --git a/collects/tests/schelog/unit.rkt b/collects/tests/schelog/unit.rkt new file mode 100644 index 0000000000..c490ea2d81 --- /dev/null +++ b/collects/tests/schelog/unit.rkt @@ -0,0 +1,306 @@ +#lang racket +(require schelog + tests/eli-tester) + +(test + (logic-var? (_)) + + (%which () (%/= 1 1)) => #f + (%which () (%/= 1 2)) => empty + (%more) => #f + + (%which (x) (%/== x x)) => #f + (%which (x y) (%/== x y)) => `((x . _) (y . _)) + (%more) => #f + + (%which () (%/== 1 1)) => #f + (%which () (%/== 1 2)) => empty + (%more) => #f + + (%which () (%< 1 2)) => empty + (%more) => #f + (%which () (%< 1 1)) => #f + (%which () (%< 2 1)) => #f + (%which () (%< 'a 2)) => #f + (%which () (%< 1 'b)) => #f + (%which () (%< 'a 'b)) => #f + + (%which () (%<= 1 2)) => empty + (%more) => #f + (%which () (%<= 1 1)) => empty + (%more) => #f + (%which () (%<= 2 1)) => #f + (%which () (%<= 'a 2)) => #f + (%which () (%<= 1 'b)) => #f + (%which () (%<= 'a 'b)) => #f + + (%which () (%= 1 1)) => empty + (%more) => #f + (%which () (%= 'a 'a)) => empty + (%more) => #f + (%which () (%= (cons 1 2) (cons 1 2))) => empty + (%more) => #f + (%which () (%= (vector 1 2) (vector 1 2))) => empty + (%more) => #f + (%which (x) (%= x 1)) => `((x . 1)) + (%more) => #f + (%which (x) (%= (cons x 2) (cons 1 2))) => `((x . 1)) + (%more) => #f + (%which (x) (%= (vector x 2) (vector 1 2))) => `((x . 1)) + (%more) => #f + (%which (x) (%and (%= x 1) (%= x 2))) => #f + (%which () (%= 1 2)) => #f + + (%which () (%=/= 1 1)) => #f + (%which () (%=/= 'a 'a)) => #f + (%which () (%=/= 1 2)) => empty + (%more) => #f + + (%which () (%=:= 1 1)) => empty + (%more) => #f + (%which () (%=:= 'a 'a)) => #f + (%which () (%=:= 1 2)) => #f + + (%which () (%== 1 1)) => empty + (%more) => #f + (%which (x) (%== x x)) => `((x . _)) + (%more) => #f + (%which (x) (%== (cons 1 x) (cons 1 x))) => `((x . _)) + (%more) => #f + ; XXX This answer seems wrong + (%which (x) (%and (%= x 1) (%== x 1))) => `((x . 1)) + (%more) => #f + ; XXX This answer seems wrong + (%which (x y) (%and (%= x 1) (%= y 1) (%== x y))) => `((x . 1) (y . 1)) + (%more) => #f + (%which (x y) (%== x y)) => #f + (%which (x y) (%== (cons 1 x) (cons y 2))) => #f + + (%which () (%> 2 1)) => empty + (%more) => #f + (%which () (%> 1 1)) => #f + (%which () (%> 1 2)) => #f + (%which () (%> 'a 2)) => #f + (%which () (%> 1 'b)) => #f + (%which () (%> 'a 'b)) => #f + + (%which () (%>= 2 1)) => empty + (%more) => #f + (%which () (%>= 1 1)) => empty + (%more) => #f + (%which () (%>= 1 2)) => #f + (%which () (%>= 'a 2)) => #f + (%which () (%>= 1 'b)) => #f + (%which () (%>= 'a 'b)) => #f + + (%which () (%and %true %true)) => empty + (%more) => #f + (%which () (%and %fail %true)) => #f + (%more) => #f + + (%which () (%append empty empty empty)) => empty + (%more) => #f + (%which () (%append (list 1) empty (list 1))) => empty + (%more) => #f + (%which () (%append empty (list 2) (list 2))) => empty + (%more) => #f + (%which () (%append (list 1) (list 2) (list 1 2))) => empty + (%more) => #f + + (let ([rel %empty-rel]) + (test (%which (y) (rel 'x y)) => #f + (%assert! rel () [('x 1)]) + (%which (y) (rel 'x y)) => `([y . 1]) + (%more) => #f + (%assert-after! rel () [('x 2)]) + (%which (y) (rel 'x y)) => `([y . 2]) + (%more) => `([y . 1]) + (%more) => #f + (%assert! rel () [('x 3)]) + (%which (y) (rel 'x y)) => `([y . 2]) + (%more) => `([y . 1]) + (%more) => `([y . 3]) + (%more) => #f)) + + (%which (y) (%let (x) (%bag-of x (%or (%= x 1) (%= x 1) (%= x 2)) y))) => `([y . (1 1 2)]) + (%more) => #f + ; XXX I don't know a program that would get these outputs + ;(%which (y) (%let (x) (%bag-of x XXX y))) => `([y . ()]) + (%more) => #f + (%which (y) (%let (x) (%bag-of-1 x (%or (%= x 1) (%= x 1) (%= x 2)) y))) => `([y . (1 1 2)]) + (%more) => #f + ; XXX I don't know a program that would get these outputs + ;(%which (y) (%let (x) (%bag-of-1 x XXX y))) => #f + + (%which () (%compound (cons 1 1))) => empty + (%more) => #f + (%which () (%compound (vector 1 1))) => empty + (%more) => #f + (%which () (%let (x) (%and (%= x (cons 1 1)) (%compound x)))) => empty + (%more) => #f + (%which () (%compound 1)) => #f + (%which () (%compound "1")) => #f + (%which () (%compound '1)) => #f + (%which () (%compound empty)) => #f + + (%which () (%constant (cons 1 1))) => #f + (%which () (%constant (vector 1 1))) => #f + (%which () (%let (x) (%and (%= x 1) (%constant x)))) => empty + (%more) => #f + (%which () (%constant 1)) => empty + (%more) => #f + (%which () (%constant "1")) => empty + (%more) => #f + (%which () (%constant '1)) => empty + (%more) => #f + (%which () (%constant empty)) => empty + (%more) => #f + + (%which (x) (%let (y) (%and (%copy x y) (%= y 1)))) => `([x . _]) + (%more) => #f + + ! =error> "syntactically" + + (%which () (%cut-delimiter %true)) => empty + (%more) => #f + (%which () (%cut-delimiter !)) => empty + (%more) => #f + (%which () (%cut-delimiter %fail)) => #f + (%which () (%or %true %true)) => empty + (%more) => empty + (%more) => #f + (%which () (%cut-delimiter (%or (%and ! %true) %true))) => empty + (%more) => #f + + (%which () (%empty-rel 1 1)) => #f + + (%which () %fail) => #f + + ; %free-vars example from documentation + (local [(define %knows + (%rel () + [('Odysseus 'TeX)] + [('Odysseus 'Scheme)] + [('Odysseus 'Prolog)] + [('Odysseus 'Penelope)] + [('Penelope 'TeX)] + [('Penelope 'Prolog)] + [('Penelope 'Odysseus)] + [('Telemachus 'TeX)] + [('Telemachus 'calculus)]))] + (test (%which (someone things-known) + (%let (x) + (%set-of x (%knows someone x) + things-known))) + => + `((someone . _) (things-known TeX Scheme Prolog Penelope Odysseus calculus)) + (%more) => #f + (%which (someone things-known) + (%let (x) + (%bag-of x + (%free-vars (someone) + (%knows someone x)) + things-known))) + => + `((someone . Odysseus) (things-known TeX Scheme Prolog Penelope)) + (%more) => + `((someone . Penelope) (things-known TeX Prolog Odysseus)) + (%more) => + `((someone . Telemachus) (things-known TeX calculus)) + (%more) => + #f)) + + (%which (x) (%let (y) (%and (%freeze x y) (%nonvar y)))) => `([x . _]) + + (%which () (%if-then-else %true %true %true)) => empty + (%more) => #f + (%which () (%if-then-else %true %fail %true)) => #f + (%which () (%if-then-else %fail %true %true)) => empty + (%more) => #f + + (%which (x) (%is x (* 6 7))) => `([x . 42]) + (%more) => #f + (%which (x) (%let (y) (%and (%= y 7) (%is x (* 6 y))))) => `([x . 42]) + (%more) => #f + + (%which () (%let (x) (%= x x))) => empty + (%more) => #f + + (%which (x) (%let (y z) (%and (%freeze x y) (%melt y z) (%= z 1)))) => `([x . 1]) + (%more) => #f + + (%which (x) (%let (y z) (%and (%freeze x y) (%melt-new y z) (%= z 1)))) => `([x . _]) + (%more) => #f + + (%which () (%member 3 (list 1 2 3))) => empty + (%more) => #f + (%which () (%member 3 (list 1 2 3 3))) => empty + (%more) => empty + (%more) => #f + (%which () (%member 3 (list 1 2))) => #f + + (%which () (%let (x) (%nonvar x))) => #f + (%which () (%let (x) (%nonvar (cons 1 x)))) => #f + (%which () (%let (x) (%nonvar (vector x)))) => #f + (%which () (%let (x) (%nonvar 1))) => empty + (%more) => #f + (%which () (%let (x) (%and (%= x 1) (%nonvar x)))) => empty + (%more) => #f + + (%which () (%not %true)) => #f + (%which () (%not %fail)) => empty + (%more) => #f + + (%which () (%or %true %true)) => empty + (%more) => empty + (%more) => #f + (%which () (%or %true %fail %true)) => empty + (%more) => empty + (%more) => #f + + (let ([rel (%rel () [(1)] [(2) %fail])]) + (test (%which () (rel 1)) => empty + (%more) => #f + (%which () (rel 2)) => #f)) + (let ([rel (%rel () [(1) !] [(1) (%repeat)])]) + (test (%which () (rel 1)) => empty + (%more) => #f)) + + (local [(define (many-%more n) + (if (zero? n) + empty + (and (%more) + (many-%more (sub1 n)))))] + (test (%which () (%repeat)) => empty + (many-%more (random 50)) => empty)) + + (parameterize ([use-occurs-check? #f]) + (%which () (%let (x) (%= x (cons 1 x))))) + => empty + (parameterize ([use-occurs-check? #t]) + (%which () (%let (x) (%= x (cons 1 x))))) + => #f + + (%which (y) (%let (x) (%set-of x (%or (%= x 1) (%= x 1) (%= x 2)) y))) => `([y . (1 2)]) + (%more) => #f + ; XXX I don't know a program that would get these outputs + ;(%which (y) (%let (x) (%set-of x XXX y))) => `([y . ()]) + (%more) => #f + (%which (y) (%let (x) (%set-of-1 x (%or (%= x 1) (%= x 1) (%= x 2)) y))) => `([y . (1 2)]) + (%more) => #f + ; XXX I don't know a program that would get these outputs + ;(%which (y) (%let (x) (%set-of-1 x XXX y))) => #f + + (%which () %true) => empty + (%more) => #f + + (%which () (%let (x) (%var x))) => empty + (%more) => #f + (%which () (%let (x) (%var (cons 1 x)))) => empty + (%more) => #f + (%which () (%let (x) (%var (vector x)))) => empty + (%more) => #f + (%which () (%let (x) (%var 1))) => #f + (%which () (%let (x) (%and (%= x 1) (%var x)))) => #f + + ) \ No newline at end of file