diff --git a/collects/datalog/eval.rkt b/collects/datalog/eval.rkt index 2bea9d0..c6d289a 100644 --- a/collects/datalog/eval.rkt +++ b/collects/datalog/eval.rkt @@ -15,7 +15,7 @@ (datum->syntax #f (format-statement s) (assertion-srcloc s)))))) (define (print-questions ls) - (displayln + (displayln (format-questions ls))) (define (eval-program p) diff --git a/collects/datalog/lang/configure-runtime.rkt b/collects/datalog/lang/configure-runtime.rkt new file mode 100644 index 0000000..5985d59 --- /dev/null +++ b/collects/datalog/lang/configure-runtime.rkt @@ -0,0 +1,20 @@ +#lang racket/base + +(define (configure data) + (printf "Configuring\n") + (current-read-interaction even-read)) +(provide configure) + +(require datalog/parse + datalog/private/compiler) + +; XXX This is almost certainly wrong. +(define (even-read src ip) + (begin0 + (compile-statement + (parameterize ([current-source-name src]) + (parse-statement ip))) + (current-read-interaction odd-read))) +(define (odd-read src ip) + (current-read-interaction even-read) + eof) \ No newline at end of file diff --git a/collects/datalog/lang/lang-info.rkt b/collects/datalog/lang/lang-info.rkt new file mode 100644 index 0000000..760c5af --- /dev/null +++ b/collects/datalog/lang/lang-info.rkt @@ -0,0 +1,10 @@ +#lang racket/base + +(define (get-info data) + (λ (key default) + (case key + [(configure-runtime) + '(#(datalog/lang/configure-runtime configure #f))] + [else + default]))) +(provide get-info) \ No newline at end of file diff --git a/collects/datalog/lang/reader.rkt b/collects/datalog/lang/reader.rkt index 43f2068..ece754f 100644 --- a/collects/datalog/lang/reader.rkt +++ b/collects/datalog/lang/reader.rkt @@ -3,6 +3,8 @@ #:read (lambda ([in (current-input-port)]) (this-read-syntax #f in)) #:read-syntax this-read-syntax #:whole-body-readers? #t + #:language-info + '#(datalog/lang/lang-info get-info #f) #:info (lambda (key defval default) ; XXX Should have different comment character key (case key @@ -10,8 +12,6 @@ (dynamic-require 'datalog/tool/submit 'repl-submit?)] [(color-lexer) (dynamic-require 'datalog/tool/syntax-color 'get-syntax-token)] - [(configure-runtime) - (λ () (current-read-interaction even-read))] [else (default key defval)])) (require datalog/parse datalog/private/compiler) @@ -19,15 +19,4 @@ (define (this-read-syntax [src #f] [in (current-input-port)]) (compile-program (parameterize ([current-source-name src]) - (parse-program in)))) - - ; XXX This is almost certainly wrong. - (define (even-read src ip) - (begin0 - (compile-statement - (parameterize ([current-source-name src]) - (parse-statement ip))) - (current-read-interaction odd-read))) - (define (odd-read src ip) - (current-read-interaction even-read) - eof)) \ No newline at end of file + (parse-program in))))) \ No newline at end of file diff --git a/collects/datalog/parse.rkt b/collects/datalog/parse.rkt index 83e5249..04531cd 100644 --- a/collects/datalog/parse.rkt +++ b/collects/datalog/parse.rkt @@ -31,7 +31,7 @@ (datum->syntax #f tok-value (make-srcloc start-pos end-pos))))) (grammar (program [(statements) $1]) - (statements [(statement) (list $1)] + (statements [() empty] [(statement statements) (list* $1 $2)]) (statement [(assertion) $1] [(query) $1] @@ -46,6 +46,7 @@ (literal [(predicate-sym LPAREN RPAREN) (make-literal (make-srcloc $1-start-pos $3-end-pos) $1 empty)] [(predicate-sym LPAREN terms RPAREN) (make-literal (make-srcloc $1-start-pos $4-end-pos) $1 $3)] [(predicate-sym) (make-literal (make-srcloc $1-start-pos $1-end-pos) $1 empty)] + [(term NEQUAL term) (make-literal (make-srcloc $1-start-pos $3-end-pos) '!= (list $1 $3))] [(term EQUAL term) (make-literal (make-srcloc $1-start-pos $3-end-pos) '= (list $1 $3))]) (predicate-sym [(IDENTIFIER) (string->symbol $1)] [(STRING) $1]) diff --git a/collects/datalog/pretty.rkt b/collects/datalog/pretty.rkt index 39f92f6..9aaed2a 100644 --- a/collects/datalog/pretty.rkt +++ b/collects/datalog/pretty.rkt @@ -48,10 +48,9 @@ (format-external e)])) (define (format-questions ls) (v-concat - (append (map (lambda (l) - (h-append (format-question l) dot)) - ls) - (list line)))) + (map (lambda (l) + (h-append (format-question l) dot)) + ls))) (define (format-clause c) (if (empty? (clause-body c)) (format-literal (clause-head c)) diff --git a/collects/datalog/private/lex.rkt b/collects/datalog/private/lex.rkt index 58b9f49..e2ca602 100644 --- a/collects/datalog/private/lex.rkt +++ b/collects/datalog/private/lex.rkt @@ -3,7 +3,7 @@ (prefix-in : parser-tools/lex-sre)) (define-tokens dtokens (VARIABLE IDENTIFIER STRING)) -(define-empty-tokens dpunct (LPAREN COMMA RPAREN TSTILE DOT EQUAL TILDE QMARK EOF)) +(define-empty-tokens dpunct (LPAREN COMMA RPAREN TSTILE DOT EQUAL NEQUAL TILDE QMARK EOF)) (define-lex-abbrev line-break #\newline) (define-lex-abbrev id-chars (char-complement (char-set "(,)=:.~?\"% \n"))) (define-lex-abbrev variable-re (:: upper-case (:* (:or upper-case lower-case (char-set "0123456789_"))))) @@ -38,6 +38,7 @@ [#\~ (token-TILDE)] [#\? (token-QMARK)] [#\= (token-EQUAL)] + ["!=" (token-NEQUAL)] [(eof) (token-EOF)])) (provide dtokens dpunct diff --git a/collects/datalog/runtime.rkt b/collects/datalog/runtime.rkt index 481d1c8..4bf5b5f 100644 --- a/collects/datalog/runtime.rkt +++ b/collects/datalog/runtime.rkt @@ -128,6 +128,14 @@ [(unify-term (empty-env) a b) => (lambda (env) (equal-test (subst-term env a) (subst-term env b)))] [else (equal-test a b)])] + [(struct literal (srcloc '!= (list a b))) + (define (equal-test a b) + (unless (term-equal? a b) + (fact! sg (make-literal srcloc '!= (list a b))))) + (cond + [(unify-term (empty-env) a b) + => (lambda (env) (equal-test (subst-term env a) (subst-term env b)))] + [else (equal-test a b)])] [_ (search-theory! sg)])) (define sg (make-subgoal q empty empty)) diff --git a/collects/datalog/scribblings/datalog.scrbl b/collects/datalog/scribblings/datalog.scrbl index 6942712..79d7414 100644 --- a/collects/datalog/scribblings/datalog.scrbl +++ b/collects/datalog/scribblings/datalog.scrbl @@ -43,7 +43,7 @@ included in a string. The remaining characters may be specified using escape cha A literal, is a predicate symbol followed by an optional parenthesized list of comma separated terms. A predicate symbol is either an identifier or a string. A term is either a variable or a constant. As with predicate symbols, a constant is either an identifier or a string. As a special case, -two terms separated by @litchar["="] is a literal for the equality predicate. +two terms separated by @litchar["="] (@litchar["!="]) is a literal for the equality (inequality) predicate. The following are literals: @verbatim[#:indent 4 #<substitutions (datalog-stmt-var-selector stmt) (eval-statement (datalog-stmt stmt))) @@ -48,6 +49,7 @@ [(_ thy-expr stmt ...) (syntax/loc stx (parameterize ([current-theory thy-expr]) + (void) (eval-top-level-statement (datalog-stmt stmt)) ...))])) diff --git a/collects/datalog/tool/syntax-color.rkt b/collects/datalog/tool/syntax-color.rkt index 5966b2e..7974d22 100644 --- a/collects/datalog/tool/syntax-color.rkt +++ b/collects/datalog/tool/syntax-color.rkt @@ -30,7 +30,7 @@ [identifier-re (syn-val lexeme 'identifier #f start-pos end-pos)] [(:or #\) #\() (syn-val lexeme 'parenthesis #f start-pos end-pos)] - [(:or #\= #\? #\~ #\. #\, ":-") (syn-val lexeme 'parenthesis #f start-pos end-pos)] + [(:or "!=" #\= #\? #\~ #\. #\, ":-") (syn-val lexeme 'parenthesis #f start-pos end-pos)] [(eof) (syn-val lexeme 'eof #f start-pos end-pos)] [#\" ((colorize-string start-pos) input-port)] [any-char (syn-val lexeme 'error #f start-pos end-pos)])) \ No newline at end of file diff --git a/collects/tests/datalog/eval.rkt b/collects/tests/datalog/eval.rkt index 3611fd5..4cdf4b2 100644 --- a/collects/tests/datalog/eval.rkt +++ b/collects/tests/datalog/eval.rkt @@ -14,15 +14,11 @@ (define test-rkt (build-path examples-dir (format "~a.rkt" t))) (define test-txt (build-path examples-dir (format "~a.txt" t))) (test-equal? t - (filter (lambda (l) - (not (string=? l ""))) - (with-input-from-string - (with-output-to-string - (lambda () (dynamic-require test-rkt #f))) - port->lines)) - (filter (lambda (l) - (not (string=? l ""))) - (file->lines test-txt)))) + (with-input-from-string + (with-output-to-string + (lambda () (dynamic-require test-rkt #f))) + port->lines) + (file->lines test-txt))) (define (test-files d) (for ([f (in-list (directory-list d))] diff --git a/collects/tests/datalog/examples/empty.rkt b/collects/tests/datalog/examples/empty.rkt new file mode 100644 index 0000000..892af15 --- /dev/null +++ b/collects/tests/datalog/examples/empty.rkt @@ -0,0 +1 @@ +#lang datalog \ No newline at end of file diff --git a/collects/tests/datalog/examples/sym.rkt b/collects/tests/datalog/examples/sym.rkt new file mode 100644 index 0000000..1fd6368 --- /dev/null +++ b/collects/tests/datalog/examples/sym.rkt @@ -0,0 +1,8 @@ +#lang datalog + +sym(a). +sym(b). +sym(c). +perm(X,Y) :- sym(X), sym(Y), X != Y. + +perm(X,Y)? \ No newline at end of file diff --git a/collects/tests/datalog/paren-examples/add1.txt b/collects/tests/datalog/paren-examples/add1.txt index dc6a141..70700ca 100644 --- a/collects/tests/datalog/paren-examples/add1.txt +++ b/collects/tests/datalog/paren-examples/add1.txt @@ -1,3 +1,3 @@ add1(2) = (3). - add2(1, 3). + diff --git a/collects/tests/datalog/paren-examples/bidipath.txt b/collects/tests/datalog/paren-examples/bidipath.txt index 6c197dd..f10d340 100644 --- a/collects/tests/datalog/paren-examples/bidipath.txt +++ b/collects/tests/datalog/paren-examples/bidipath.txt @@ -14,4 +14,3 @@ path(d, d). path(d, c). path(d, b). path(d, a). - diff --git a/collects/tests/datalog/paren-examples/empty.rkt b/collects/tests/datalog/paren-examples/empty.rkt new file mode 100644 index 0000000..548c66d --- /dev/null +++ b/collects/tests/datalog/paren-examples/empty.rkt @@ -0,0 +1 @@ +#lang datalog/sexp \ No newline at end of file diff --git a/collects/tests/datalog/paren-examples/empty.txt b/collects/tests/datalog/paren-examples/empty.txt new file mode 100644 index 0000000..e69de29 diff --git a/collects/tests/datalog/paren-examples/path.txt b/collects/tests/datalog/paren-examples/path.txt index 9319f8c..c014bca 100644 --- a/collects/tests/datalog/paren-examples/path.txt +++ b/collects/tests/datalog/paren-examples/path.txt @@ -14,4 +14,3 @@ path(d, b). path(d, c). path(d, d). path(d, a). - diff --git a/collects/tests/datalog/paren-examples/revpath.txt b/collects/tests/datalog/paren-examples/revpath.txt index 6c197dd..f10d340 100644 --- a/collects/tests/datalog/paren-examples/revpath.txt +++ b/collects/tests/datalog/paren-examples/revpath.txt @@ -14,4 +14,3 @@ path(d, d). path(d, c). path(d, b). path(d, a). - diff --git a/collects/tests/datalog/paren-examples/sym.rkt b/collects/tests/datalog/paren-examples/sym.rkt new file mode 100644 index 0000000..9d05e6b --- /dev/null +++ b/collects/tests/datalog/paren-examples/sym.rkt @@ -0,0 +1,11 @@ +#lang datalog/sexp + +(! (sym a)) +(! (sym b)) +(! (sym c)) +(! (:- (perm X Y) + (sym X) + (sym Y) + (!= X Y))) + +(? (perm X Y)) \ No newline at end of file diff --git a/collects/tests/datalog/paren-examples/sym.txt b/collects/tests/datalog/paren-examples/sym.txt new file mode 100644 index 0000000..b410824 --- /dev/null +++ b/collects/tests/datalog/paren-examples/sym.txt @@ -0,0 +1,6 @@ +perm(a, c). +perm(a, b). +perm(c, a). +perm(b, a). +perm(b, c). +perm(c, b). diff --git a/collects/tests/datalog/paren-examples/tutorial.txt b/collects/tests/datalog/paren-examples/tutorial.txt index 629d2dc..7171742 100644 --- a/collects/tests/datalog/paren-examples/tutorial.txt +++ b/collects/tests/datalog/paren-examples/tutorial.txt @@ -1,26 +1,19 @@ parent(john, douglas). - parent(john, douglas). parent(bob, john). parent(ebbon, bob). - parent(john, douglas). - ancestor(ebbon, bob). ancestor(bob, john). ancestor(john, douglas). ancestor(bob, douglas). ancestor(ebbon, john). ancestor(ebbon, douglas). - ancestor(bob, john). ancestor(ebbon, john). - parent(john, douglas). parent(ebbon, bob). - ancestor(ebbon, bob). ancestor(john, douglas). - diff --git a/collects/tests/datalog/parse.rkt b/collects/tests/datalog/parse.rkt index db86b57..293aff4 100644 --- a/collects/tests/datalog/parse.rkt +++ b/collects/tests/datalog/parse.rkt @@ -21,6 +21,8 @@ (make-literal #f 'parent (list (make-constant #f 'john) (make-constant #f 'douglas)))) (test-literal-parse "1 = 2" (make-literal #f '= (list (make-constant #f '|1|) (make-constant #f '|2|)))) + (test-literal-parse "1 != 2" + (make-literal #f '!= (list (make-constant #f '|1|) (make-constant #f '|2|)))) (test-literal-parse "zero-arity-literal" (make-literal #f 'zero-arity-literal empty)) (test-literal-parse "zero-arity-literal()" diff --git a/collects/tests/datalog/private/lex.rkt b/collects/tests/datalog/private/lex.rkt index 6648cfd..f4efacd 100644 --- a/collects/tests/datalog/private/lex.rkt +++ b/collects/tests/datalog/private/lex.rkt @@ -17,6 +17,7 @@ "lex" (test-lexer "=" 'EQUAL #f) + (test-lexer "!=" 'NEQUAL #f) (test-lexer "?" 'QMARK #f) (test-lexer "~" 'TILDE #f) (test-lexer "." 'DOT #f) diff --git a/collects/tests/datalog/tool/syntax-color.rkt b/collects/tests/datalog/tool/syntax-color.rkt index 6b48bb8..5103300 100644 --- a/collects/tests/datalog/tool/syntax-color.rkt +++ b/collects/tests/datalog/tool/syntax-color.rkt @@ -24,6 +24,7 @@ (test-color "123var" 'identifier) (test-color "(" 'parenthesis) (test-color ")" 'parenthesis) + (test-color "!=" 'parenthesis) (test-color "=" 'parenthesis) (test-color "?" 'parenthesis) (test-color "~" 'parenthesis)