Missing subject in emit-inductive

3 files changed, 12 insertions, 12 deletions

diff --git a/compiler/lean.scm b/compiler/lean.scm
index c2d2728..2e2e264 100644
--- a/compiler/lean.scm
+++ b/compiler/lean.scm
@@ -155,18 +155,20 @@
        (lambda (rule i)
          (if (equal? #t (body rule))
              ;; Special case where the fact is true unconditionally.
-             (format #t "| rule~a : (~a = (~a)) → ~a"
+             (format #t "| rule~a : (~a = (~a)) → ~a ~a"
                      (number->subscript i) ; rule~a
                      (subject x)           ; (~a = ~a)
                      (compile (conclusion rule))
                      inductive-name     ; → ~a
+                     (subject x)
                      )
-             (format #t "| rule~a : ~a → (~a = (~a)) → ~a"
+             (format #t "| rule~a : ~a → (~a = (~a)) → ~a ~a"
                      (number->subscript i) ; rule~a
                      (compile (body rule)) ; ~a →
                      (subject x)           ; (~a = ~a)
                      (compile (conclusion rule))
                      inductive-name     ; → ~a
+                     (subject x)
                      ))
          (newline))
        (facts x)
diff --git a/compiler/test.scm b/compiler/test.scm
index a93b19c..8706afc 100644
--- a/compiler/test.scm
+++ b/compiler/test.scm
@@ -233,23 +233,19 @@
   (let*-values (((ast) (read-and-parse policy-file-name))
                 ((package imports rules) (preprocess-policy ast))
                 ((policy) (parse-policy package imports rules))
-                ((policy) (extract-identifiers policy))
+                ((policy) (compile-constraints policy))
                 ((policy) (compile-exists-some policy))
-                ((policy) (compile-funcall policy))
-                ((policy) (compile-constraints policy)))
+                ((policy) (extract-identifiers policy))
+                ((policy) (compile-funcall policy)))
     (with-output-to-string
       (lambda ()
         (emit-specification policy)))))
 
 
 (test-equal (compile-policy "examples/01-computable-assign-scalar.rego")
-  "-- package data.examples.computable_assign_scalar\n\n\ninductive pi_eqv (v : Rego.Any) : Prop\n| rule₀ : (v = (Rego.Any.num 3.14159)) → pi_eqv\n\n\n")
+  "-- package data.examples.computable_assign_scalar\n\n\ninductive pi_eqv (v : Rego.Any) : Prop\n| rule₀ : (v = (Rego.Any.num 3.14159)) → pi_eqv v\n\n\n")
 
 (test-equal (compile-policy "examples/02-computable-assign-composite.rego")
-  "-- package data.examples.computable_assign_composite\n\n\ninductive rect_eqv (v : Rego.Any) : Prop\n| rule₀ : (v = (List.toAssocList' ([((Rego.Any.str \"height\"), (Rego.Any.num 4)), ((Rego.Any.str \"width\"), (Rego.Any.num 2))]))) → rect_eqv\n\n\n")
-
-(test-equal (compile-policy "examples/03-set-defined-by-predicate.rego")
-  "-- package data.examples.set_defined_by_predicate\n\n-- imports future.keywords.contains\n-- imports future.keywords.if\n-- imports future.keywords.in\n\ninductive q_memq (v : Rego.Any) : Prop\n| rule₀ : ∃ (site : Rego.Any), (([Array.contains (site) (sites)]) ∧ ((let name := site.Rego.Any.str \"name\"; ))) → (v = (name)) → q_memq\n\n\n")
-
+  "-- package data.examples.computable_assign_composite\n\n\ninductive rect_eqv (v : Rego.Any) : Prop\n| rule₀ : (v = (List.toAssocList' ([((Rego.Any.str \"height\"), (Rego.Any.num 4)), ((Rego.Any.str \"width\"), (Rego.Any.num 2))]))) → rect_eqv v\n\n\n")
 
 (test-end "integration-tests")
diff --git a/compiler/types.scm b/compiler/types.scm
index f2a62f0..613b303 100644
--- a/compiler/types.scm
+++ b/compiler/types.scm
@@ -135,6 +135,7 @@
   ;; TODO: Should this include the `head' of a rule too?
   (match form
     (($ <rule> default head body)
+     ;; A rule body introduces a new scope.
      (let* ((breadcrumb (add-to-end breadcrumb (left head)))
             (inner (with-modified-slot form 'body
                      (tree-map body f scope breadcrumb))))
@@ -214,7 +215,8 @@
 `scope' is a <scope>, `breadcrumb' is a list given to the `f' of `mutate-tree',
 and `identifier' is a <reference>"
   (define (recur breadcrumb)
-    (or (member identifier (or (map car (assoc-ref (inner scope) breadcrumb)) '()))
+    (define looking-at (hash-table-ref/default (inner scope) breadcrumb '()))
+    (or (assoc identifier looking-at)
         (if (null? breadcrumb)
             #t
             ;; (lean-builtin-function? (reference->lean-name identifier))