Adjust datalog to cooperate with check syntax a little bit more.

Specifically:
 - make predicate symbols and variables be original (and,
   in the former case, have srclocs)
 - remove the originality in the quoted syntax constants
   that the expansion introduces

I think there is probably something better that should be done
with those introduced syntax constants, possibly relacing
them with #f, or possibly replacing them with source location
lists, but I'm not sure how they are used, so I've just left
them in there.

(Also, very minor Rackety in check syntax)

collects/datalog/ast.rkt

@@ -21,6 +21,8 @@
 (define (constant-equal? v1 v2)
   (equal? (constant-value v1) (constant-value v2)))
 
+(define-struct predicate-sym (srcloc sym) #:prefab)
+
 (define term/c (or/c variable? constant?))
 (define (term-equal? t1 t2)
   (cond
@@ -78,6 +80,7 @@
  [srcloc/c contract?]
  [datum/c contract?]
  [datum-equal? (datum/c datum/c . -> . boolean?)]
+ [struct predicate-sym ([srcloc srcloc/c] [sym symbol?])]
  [struct variable ([srcloc srcloc/c]
                    [sym symbol?])]
  [variable-equal? (variable? variable? . -> . boolean?)]
@@ -87,7 +90,7 @@
  [term/c contract?]
  [term-equal? (term/c term/c . -> . boolean?)]
  [struct literal ([srcloc srcloc/c]
-                  [predicate datum/c]
+                  [predicate (or/c predicate-sym? string? symbol?)]
                   [terms (listof term/c)])]
  [literal-equal? (literal? literal? . -> . boolean?)]
  [struct external ([srcloc srcloc/c]

collects/datalog/parse.rkt

@@ -50,7 +50,7 @@
               [(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)]
+     (predicate-sym [(IDENTIFIER) (make-predicate-sym (make-srcloc $1-start-pos $1-end-pos) (string->symbol $1))]
                     [(STRING) $1])
      (terms [(term) (list $1)]
             [(term COMMA terms) (list* $1 $3)])

collects/datalog/private/compiler.rkt

@@ -45,12 +45,23 @@
        (= #,@(map compile-term ts)))]
     [(literal srcloc pred ts)
      (define srcstx (datum->syntax #f 'x srcloc))
+     (define pred-stx (if (predicate-sym? pred)
+                          (sym->original-syntax (predicate-sym-sym pred)
+                                                (predicate-sym-srcloc pred))
+                          pred))
      (quasisyntax/loc srcstx
-       (#,pred #,@(map compile-term ts)))]))
+       (#,pred-stx #,@(map compile-term ts)))]))
 
 (define compile-term
   (match-lambda
     [(variable srcloc sym)
-     (datum->syntax #f sym srcloc)]
+     (sym->original-syntax sym srcloc)]
     [(constant srcloc sym)
      (datum->syntax #f sym srcloc)]))
+
+(define (sym->original-syntax sym srcloc)
+  (define p (open-input-string (symbol->string sym)))
+  (port-count-lines! p)
+  (match-define (list source-name line column position span) srcloc)
+  (set-port-next-location! p line column position)
+  (read-syntax source-name p))

collects/datalog/stx.rkt

@@ -29,7 +29,10 @@
                  :-
                  ,@(map term->datum anss))]
     [(literal _ pred ts)
-     (list* pred (map term->datum ts))]))
+     (list* (if '(predicate-sym? pred)
+                '(predicate-sym-sym pred)
+                pred)
+            (map term->datum ts))]))
 
 (define term->datum
   (match-lambda
@@ -62,13 +65,13 @@
    #:literals (! ~ ?)
    [(_ (~and tstx (! c)))
     (quasisyntax/loc #'tstx
-      (assertion #'#,#'tstx (datalog-clause c)))]
+      (assertion #'#,(unoriginal #'tstx) (datalog-clause c)))]
    [(_ (~and tstx (~ c)))
     (quasisyntax/loc #'tstx
-      (retraction #'#,#'tstx (datalog-clause c)))]
+      (retraction #'#,(unoriginal #'tstx) (datalog-clause c)))]
    [(_ (~and tstx (? l)))
     (quasisyntax/loc #'tstx
-      (query #'#,#'tstx (datalog-literal l)))]))
+      (query #'#,(unoriginal #'tstx) (datalog-literal/ref l)))]))
 
 (define-syntax (datalog-stmt-var-selector stx)
   (syntax-parse 
@@ -127,29 +130,38 @@
       (syntax-local-lift-expression
        fake-lam))
     (quasisyntax/loc #'tstx
-      (clause #'#,#'tstx (datalog-literal head) 
+      (clause #'#,(unoriginal #'tstx) (datalog-literal/bind head) 
-              (list (datalog-literal body) ...)))]
+              (list (datalog-literal/ref body) ...)))]
    [(_ e)
     (quasisyntax/loc #'e
-      (clause #'#,#'e (datalog-literal e) empty))]))
+      (clause #'#,(unoriginal #'e) (datalog-literal/bind e) empty))]))
 
-(define-syntax (datalog-literal stx)
+(define-syntax (datalog-literal/bind stx) (datalog-literal/b stx #t))
+(define-syntax (datalog-literal/ref stx) (datalog-literal/b stx #f))
+
+(define-for-syntax (datalog-literal/b stx binding?)
   (syntax-parse 
    stx
    #:literals (:-)
    [(_ sym:id)
-    (quasisyntax/loc #'sym
+    (syntax-property 
-      (literal #'#,#'sym 'sym empty))]
+     (quasisyntax/loc #'sym
+       (literal #'#,(unoriginal #'sym) 'sym empty))
+     (if binding? 'disappeared-binding 'disappeared-use)
+     (syntax-local-introduce #'sym))]
    [(_ (~and tstx (sym:id arg ... :- ans ...)))
     (quasisyntax/loc #'tstx
-      (external #'#,#'tstx 'sym sym
+      (external #'#,(unoriginal #'tstx) 'sym sym
                 (list (datalog-term arg) ...)
                 (list (datalog-term ans) ...)))]
    [(_ (~and tstx (sym:id e ...)))
-    (quasisyntax/loc #'tstx
+    (syntax-property
-      (literal #'#,#'tstx 'sym 
+     (quasisyntax/loc #'tstx
-               (list (datalog-term e)
+       (literal #'#,(unoriginal #'tstx) 'sym 
-                     ...)))]))
+                (list (datalog-term e)
+                      ...)))
+     (if binding? 'disappeared-binding 'disappeared-use)
+     (syntax-local-introduce #'sym))]))
 
 (define-syntax (datalog-literal-var-selector stx)
   (syntax-parse 
@@ -186,16 +198,26 @@
     (cond
       [(identifier-binding #'sym 0)
        (quasisyntax/loc #'sym
-         (constant #'#,#'sym sym))]
+         (constant #'#,(unoriginal #'sym) sym))]
       [(char-upper-case? (string-ref (symbol->string (syntax->datum #'sym)) 0))
        (quasisyntax/loc #'sym
-         (variable #'#,#'sym 'sym))]
+         (variable #'#,(unoriginal #'sym) 'sym))]
       [else
        (quasisyntax/loc #'sym
-         (constant #'#,#'sym 'sym))])]
+         (constant #'#,(unoriginal #'sym) 'sym))])]
    [(_ sym:expr)
     (quasisyntax/loc #'sym
-      (constant #'#,#'sym sym))]))
+      (constant #'#,(unoriginal #'sym) sym))]))
+
+(define-for-syntax (unoriginal stx)
+  (let loop ([stx stx])
+    (cond
+      [(syntax? stx)
+       (datum->syntax stx (loop (syntax-e stx)) stx)]
+      [(pair? stx)
+       (cons (loop (car stx))
+             (loop (cdr stx)))]
+      [else stx])))
 
 (provide datalog datalog!
          :- ! ~ ?)

collects/drracket/private/syncheck/traversals.rkt

@@ -144,7 +144,6 @@
                             phase-to-requires)
       
       (let ([maybe-jump (λ (vars) (visit-id vars))])
-
         (let level+tail-loop ([stx-obj stx-obj]
                               [level 0]
                               [tail-parent-src #f]
@@ -576,10 +575,9 @@
                                 phase-level user-namespace user-directory actual?)
       (let ([binders (get-ids all-binders var)])
         (when binders
-          (for-each (λ (x)
+          (for ([x (in-list binders)])
-                      (when (syntax-original? x)
+            (when (syntax-original? x)
-                        (connect-syntaxes x var actual? (id-level phase-level x))))
+              (connect-syntaxes x var actual? (id-level phase-level x)))))
-                    binders))
         
         (when (and unused/phases phase-to-requires)
           (let ([req-path/pr (get-module-req-path var phase-level)]