Fix expansion for relations in term positions.

Explicitly disables random generation for relations in term
positions, but fixes a problem with runtime functionality
for the same.

collects/redex/private/judgment-form.rkt

@@ -1291,11 +1291,13 @@
        (free-identifier=? stx (quote-syntax ...))))
 
 (define-for-syntax (where-keyword? id)
-  (or (free-identifier=? id #'where)
+  (and (identifier? id)
-      (free-identifier=? id #'where/hidden)))
+       (or (free-identifier=? id #'where)
+           (free-identifier=? id #'where/hidden))))
 (define-for-syntax (side-condition-keyword? id)
-  (or (free-identifier=? id #'side-condition)
+  (and (identifier? id)
-      (free-identifier=? id #'side-condition/hidden)))
+       (or (free-identifier=? id #'side-condition)
+           (free-identifier=? id #'side-condition/hidden))))
 ;                                                                        
 ;                                                                        
 ;                                                      ;                 
@@ -1357,7 +1359,7 @@
                      (append (syntax->datum #'new-names) ns))))]
         [(side-cond . rest)
          (side-condition-keyword? #'side-cond)
-         ;; TODO - side condition handling
+         ;; TODO - enable side conditions for judgment form only
          (values ps-rw eqs ns)]
         [(prem-name . prem-body)
          (and (judgment-form-id? #'prem-name) in-judgment-form?)
@@ -1370,9 +1372,9 @@
          ;; TODO - fix when implementing ellipses
          (values ps-rw eqs ns)]
         [term
-         (not in-judgment-form?) ;; in a relation
+         (not in-judgment-form?) ;; in a relation ;; TODO - eliminate this (relations become SCs)
          (let-values ([(term-rws mf-cs) (rewrite-terms (list #'term) ns)])
-           (values (append mf-cs ps-rw)
+           (values (append mf-cs ps-rw) 
                    eqs
                    ns))]
         [else (raise-syntax-error what "malformed premise" prem)])))
@@ -1397,7 +1399,9 @@
                  [((mf-clauses ...) ...) (map (λ (fs) 
                                                 (map (λ (f-id)
                                                        (with-syntax ([f-id f-id])
-                                                         #'(metafunc-proc-gen-clauses f-id)))
+                                                         (if (judgment-form-id? #'f-id)
+                                                             #'(error 'generate-term "generation disabled for relations in term positions")
+                                                             #'(metafunc-proc-gen-clauses f-id))))
                                                      (syntax->list fs)))
                                               (syntax->list #'((f ...) ...)))])
                 (values (syntax->list #'(body-pat ...))

collects/redex/private/term.rkt

@@ -70,17 +70,17 @@
     [(_ mf)
      #'(λ (x) (mf x))]))
 
-(define-syntax (mf-map stx)
-  (syntax-case stx ()
-    [(_ inner-apps)
-     #'(λ (l) (map inner-apps l))]))
-
 (define-syntax (jf-apply stx)
   (syntax-case stx ()
     [(_ jf)
      (judgment-form-id? #'jf)
      (judgment-form-term-proc (syntax-local-value #'jf (λ () #f)))]))
 
+(define-syntax (mf-map stx)
+  (syntax-case stx ()
+    [(_ inner-apps)
+     #'(λ (l) (map inner-apps l))]))
+
 (define-for-syntax currently-expanding-term-fn (make-parameter #f))
 
 
@@ -318,7 +318,11 @@
     [(mf-apply f)
      (and (identifier? #'mf-apply)
           (eq? (syntax-e #'mf-apply) 'mf-apply))
-     #'(metafunc f)]))
+     #'(metafunc f)]
+    [(jf-apply f)
+     (and (identifier? #'jf-apply)
+          (eq? (syntax-e #'jf-apply) 'jf-apply))
+     #'(jform f)]))
 
 (define-syntax (term-let-fn stx)
   (syntax-case stx ()

collects/redex/tests/gen-test.rkt

@@ -474,7 +474,7 @@
   (test (with-handlers ([exn:fail? exn-message])
           (generate-term L #:satisfying (f r_1) = r_2 +inf.0))
         #rx".*generate-term:.*undatum.*"))
-             
+
 
 (let ()
   (define-language L (n 2))
@@ -499,14 +499,14 @@
   (define-language l (n number))
   
   (define-metafunction l
-  [(t n n)
+    [(t n n)
-   1]
+     1]
-  [(t n 2)
+    [(t n 2)
-   2]
+     2]
-  [(t 1 n)
+    [(t 1 n)
-   3]
+     3]
-  [(t n_1 n_2)
+    [(t n_1 n_2)
-   4])
+     4])
   
   (test-equal (generate-term l #:satisfying (t 1 1) = 1 +inf.0)
               '((t 1 1) = 1))
@@ -567,3 +567,34 @@
                  (raise e))])
       (for ([n 10])
         (g)))))
+
+(let ()
+  (define-language L0)
+  (define-relation L0
+    [(a any)])
+  (define-relation L0
+    [(b any)])
+  (define-relation L0
+    [(c any) (a (b any))])
+  
+  (define-metafunction L0
+    [(f any)
+     (a ny)])
+
+  (define-judgment-form L0
+    #:mode (J I O)
+    [(J any_1 any_2)
+     (J (a any_1) any_2)]
+    [(J #t #f)])
+  
+  (test (with-handlers ([exn:fail? exn-message])
+          (generate-term L0 #:satisfying (c any) +inf.0))
+        #rx".*generate-term:.*relation.*")
+  
+  (test (with-handlers ([exn:fail? exn-message])
+          (generate-term L0 #:satisfying (f any_1) = any_2 +inf.0))
+        #rx".*generate-term:.*relation.*")
+  
+  (test (with-handlers ([exn:fail? exn-message])
+          (generate-term L0 #:satisfying (J any_1 any_2) +inf.0))
+        #rx".*generate-term:.*relation.*"))

collects/redex/tests/tl-test.rkt

@@ -1254,6 +1254,31 @@
     (test (term (b 1)) #t)
     (test (term (b 2)) #t)
     (test (term (b 3)) #f))
+  
+  (let ()
+    (define-relation empty-language
+      [(a any)])
+    (define-relation empty-language
+      [(b any)])
+    (define-relation empty-language
+      [(c any) (a (b any))])
+    
+    (define-metafunction empty-language
+      [(f any)
+       (c any)])
+    
+    (define-judgment-form empty-language
+      #:mode (J I O)
+      [(J any_1 (a any_1))])
+    
+    (test (term (a 1)) #t)
+    (test (term (b 2)) #t)
+    (test (term (c 3)) #t)
+    (test (term (c (b (a x)))) #t)
+    (test (term (f q)) #t)
+    (test (judgment-holds (J Z #t)) #t)
+    (test (judgment-holds (J Z Z)) #f)
+    )
 
   
   (exec-syntax-error-tests "syn-err-tests/relation-definition.rktd")