Fixing PR11515

original commit: 5014cff4c14419785de43298625a3fbf9cc5fc65

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)

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)

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)

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))
+       (parse-program in)))))

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])

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))

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 

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))

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 #<<END
 parent(john, douglas)
@@ -96,7 +96,8 @@ The following BNF describes the syntax of Datalog.
        (BNF-seq (nonterm "predicate-sym") (litchar "(") (litchar ")"))
        (BNF-seq (nonterm "predicate-sym") (litchar "(") (nonterm "terms") (litchar ")"))
        (nonterm "predicate-sym")
-       (BNF-seq (nonterm "term") (litchar "=") (nonterm "term")))
+       (BNF-seq (nonterm "term") (litchar "=") (nonterm "term"))
+       (BNF-seq (nonterm "term") (litchar "!=") (nonterm "term")))
  (list (nonterm "predicate-sym")
        (nonterm "IDENTIFIER")
        (nonterm "STRING"))

collects/datalog/stx.rkt

@@ -38,6 +38,7 @@
     [(_ thy-expr stmt ...)
      (syntax/loc stx
        (parameterize ([current-theory thy-expr])
+         (void)
          (->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))
          ...))]))
 

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)]))

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))]

collects/tests/datalog/examples/empty.rkt

@@ -0,0 +1 @@
+#lang datalog

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)?

collects/tests/datalog/paren-examples/add1.txt

@@ -1,3 +1,3 @@
 add1(2) = (3).
-
 add2(1, 3).
+

collects/tests/datalog/paren-examples/bidipath.txt

@@ -14,4 +14,3 @@ path(d, d).
 path(d, c).
 path(d, b).
 path(d, a).
-

collects/tests/datalog/paren-examples/empty.rkt

@@ -0,0 +1 @@
+#lang datalog/sexp

collects/tests/datalog/paren-examples/path.txt

@@ -14,4 +14,3 @@ path(d, b).
 path(d, c).
 path(d, d).
 path(d, a).
-

collects/tests/datalog/paren-examples/revpath.txt

@@ -14,4 +14,3 @@ path(d, d).
 path(d, c).
 path(d, b).
 path(d, a).
-

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))

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).

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).
-

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()"

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)

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)