Persistent scope information + funcall

8 files changed, 216 insertions, 182 deletions

diff --git a/compiler/lean.scm b/compiler/lean.scm
index e5ad281..939c52f 100644
--- a/compiler/lean.scm
+++ b/compiler/lean.scm
@@ -35,7 +35,10 @@
 
             compile
 
-            lean-expression?))
+            lean-expression?
+
+            lean-builtin-function?
+            reference->lean-name))
 
 ;; For inductive predicates
 (define-class <lean-predicate> ()
@@ -196,3 +199,21 @@
   (cons (class-name (class-of inst))
         (map (compose (cut slot-ref inst <>) slot-definition-name)
              (class-slots (class-of inst)))))
+
+
+
+(define (lean-builtin-function? lean-name)
+  "Whether LEAN-NAME is a function provided by the Rego library or Lean prelude"
+  (member lean-name '("Array.contains")))
+
+(define (sanitize s)
+  s)
+
+(define (reference->lean-name reference)
+  (match reference
+    (($ <reference> (x)) (sanitize x))
+    (($ <reference> (x xs ...))
+     (if (and (equal? x (make-variable-ref "internal"))
+              (equal? xs (list (make-constant "member_2"))))
+         "Array.contains"
+         (error "Unimplemented")))))
diff --git a/compiler/passes/compile-funcall.scm b/compiler/passes/compile-funcall.scm
index 4f24a8b..2e170c0 100644
--- a/compiler/passes/compile-funcall.scm
+++ b/compiler/passes/compile-funcall.scm
@@ -15,35 +15,22 @@
 ;;; <http://www.gnu.org/licenses/>.
 
 (define-module (compiler passes compile-funcall)
+  #:use-module ((rnrs base) #:select (assert))
+  #:use-module (compiler lean)
   #:use-module (compiler types)
-  #:use-module (compiler utilities)
+  #:use-module (compiler walk)
   #:use-module (ice-9 match)
-  #:use-module (lens)
-  #:use-module (srfi srfi-1)
+  #:use-module (oop goops)
   #:export (compile-funcall))
 
-(define (maybe-compile-funcall term)
-  (if (and (list? term)
-           (positive? (length term))
-           (reference? (car term)))
-      (make-funcall (car term) (map maybe-compile-funcall (cdr term)))
-      (if (list? term) (map maybe-compile-funcall term) term)))
-
 (define (compile-funcall policy)
-  "Compile any constraints in the body of `policy'"
-  (define rule-parts
-    (compose (ι-body-conjunction) (ι-rule-body)))
-
-  (define (affect-rule rule)
-    (over rule-parts
-          (lambda (terms) (map maybe-compile-funcall terms))
-          rule))
-  (define (affect-group group)
-    (over (tail)
-          (lambda (rules) (map affect-rule rules))
-          group))
-
-  (over (ι-policy-rules)
-        (lambda (rule-groups)
-          (map affect-group rule-groups))
-        policy))
+  (mutate-tree
+   policy
+   (lambda (scope breadcrumb form)
+     (match form
+       (($ <funcall> function-name args)
+        (assert (scope-contains? scope breadcrumb function-name))
+        (make <lean-funcall>
+          #:name (reference->lean-name function-name)
+          #:args args))
+       (anything-else anything-else)))))
diff --git a/compiler/passes/extract-identifiers.scm b/compiler/passes/extract-identifiers.scm
index 00a4cbc..1420176 100644
--- a/compiler/passes/extract-identifiers.scm
+++ b/compiler/passes/extract-identifiers.scm
@@ -19,47 +19,79 @@
   #:use-module (compiler utilities)
   #:use-module (ice-9 match)
   #:use-module (ice-9 regex)
+  #:use-module (lens)
   #:use-module (srfi srfi-1)
+  #:use-module (srfi srfi-69)
   #:export (extract-identifiers))
 
-(define (maybe-demangle-identifier name)
-  (define substitutions '(("\\$" "anony")))
-  (define (recur new-name substitutions)
-    (if (null? substitutions)
-        new-name
-        (match (first substitutions)
-          ((regexp replacement)
-           (if (string-match regexp new-name)
-               (regexp-substitute #f (string-match regexp new-name) 'pre replacement 'post)
-               new-name)))))
-  (recur name substitutions))
+(define types
+  '(null bool number string array set object
+    any))
 
+(define (more-specific? x y)
+  "Predicate on whether X is a more specific type than Y"
+  (cond ((eqv? y 'any) #t)
+        ((and (list? x)
+              (list? y)
+              (< (length x) (length y))) #t)
+        (else #f)))
 
+(define (identify-variables policy)
+  "Recursively search the body of a <rule> for variable occurrences"
+  (define scopes (make-hash-table))
+  (define (recur breadcrumb form)
+    (match form
+      ;; A rule body introduces a new scope.
+      (($ <body> conjunction)
+       (let ((identified-variables (recur breadcrumb conjunction)))
+         (when (not (null? identified-variables))
+           (hash-table-append! scopes breadcrumb identified-variables)))
+       '())
 
-;; TODO: Also document identifier demangling
+      ;; Quantification introduces a new scope.
+      ;;
+      ;; This is implemented by propagating upwards. The new scope will be
+      ;; reflected when later terms query for their enclosing scope.
+      (($ <exists-some> identifiers)
+       ;; Inner is a <variable-ref>.
+       (recur breadcrumb identifiers))
+      (($ <for-all> key domain value body) ; TODO: Domain gives us some constraints on the type.
+       ;; Inner is a <variable-ref>.
+       (recur breadcrumb key))
 
-(define (annotate-rule rule)
-  "Recursively search the body of a <rule> for variable occurrences"
-  (define body (rule-body rule))
-  (define terms (body-conjunction body))
-  (define (recur form)
-    (cond ((list? form)
-           (fold update-alist '() (map recur form)))
-          ((constant? form)
-           (recur (constant-value form)))
-          ((set-literal? form)
-           (recur (set-literal-elems form)))
-          ((object-literal? form)
-           (recur (obect-literal-pairs form)))
-          ((reference? form)
-           (recur (reference-parts form)))
-          ((variable-ref? form)
-           (let ((name (variable-ref-name form)))
-             (list (list (maybe-demangle-identifier name) 'free))))
-          (else '())))
-  (make-rule (rule-default rule)
-             (rule-head rule)
-             (make-body (make-scope (recur terms) terms))))
+      ;; TODO: I know that a comprehension is going to create a new scope for
+      ;; the body, but I'm not yet sure how we're going to use `key' or `value'.
+      (($ <comprehension> _ key value body)
+       (error "unimplemented"))
+
+      ;; Indices are used to create a breadcrumb trail when dereferencing lists.
+      ((x xs ...)
+       (fold append '()
+             (map (lambda (x i)
+                    (recur (add-to-end breadcrumb i) x))
+                  (cons x xs)
+                  (iota (+ 1 (length xs))))))
+
+      ;; TODO: In what cases do we error out, instead of treating this as a free variable?
+       (($ <variable-ref> name)
+       `((,(make-reference (list (make-variable-ref name))) any)))
+      (($ <funcall> _ args)
+       (recur breadcrumb args))
+
+      ;; Anything else is a terminal, giving us no further information about the scope.
+      ;;
+      ;; - References
+      ;; - Constants
+      ;;   - Set and object literals
+      ;;
+      ;; `recur' won't encounter heads. Similarly, policy documents can't be nested.
+      (_ '())))
+  (for-each (lambda (rule)
+              (hash-table-append-item! scopes '() `(,(head-lhs (rule-head rule)) any))
+              (recur (list (head-lhs (rule-head rule)))
+                     (rule-body rule)))
+            (map cadr (policy-rules policy)))
+  (make-scope scopes))
 
 (define (extract-identifiers policy)
   "Annotate `policy' with any variable occurrences
@@ -67,10 +99,15 @@
 The result is a <scope>, which should notate identifiers as either local or
 free. After this pass, all identifiers will be notated as free, even if they
 aren't. This is updated in later passes."
-  (make-policy
-   (policy-package policy)
-   (policy-imports policy)
-   (map (lambda (kv)
-          (cons (car kv) (map annotate-rule (cdr kv))))
-        (policy-rules policy))
-   (policy-comments policy)))
+  (over (ι-policy-scope) (lambda (_) (identify-variables policy)) policy))
+
+;; TODO: Incorporate into `extract-identifiers'.
+(define (my-rewrite-anonymous form)
+  (match form
+    (($ <variable-ref> name)
+     (make-variable-ref
+      (if (string= name "$0")
+          "anony_0"
+          name)))
+    (anything-else
+     anything-else)))
diff --git a/compiler/passes/parse-policy.scm b/compiler/passes/parse-policy.scm
index cacf374..280d366 100644
--- a/compiler/passes/parse-policy.scm
+++ b/compiler/passes/parse-policy.scm
@@ -93,4 +93,4 @@
   (assert (string? package))
   (assert (and (list? imports) (every string? imports)))
   (assert (list? rules))
-  (make-policy package imports (extract-rules rules) #f))
+  (make-policy package imports #f (extract-rules rules) #f))
diff --git a/compiler/passes/preprocess-policy.scm b/compiler/passes/preprocess-policy.scm
index ae1d385..17a7318 100644
--- a/compiler/passes/preprocess-policy.scm
+++ b/compiler/passes/preprocess-policy.scm
@@ -112,6 +112,8 @@ field-eqv: assignment to a reference   (varname[field] IS value IF condition)
               body-obj))
         ;; Recurse on list.
         ((list? body-obj) (map preprocess-body body-obj))
+        ;; Look inside the `identifiers' of an `<exists-some>'
+        ((exists-some? body-obj) (preprocess-body (exists-some-identifiers body-obj)))
         ;; Anything else is the identity.
         (else body-obj)))
 
diff --git a/compiler/types.scm b/compiler/types.scm
index e73e932..eae55d7 100644
--- a/compiler/types.scm
+++ b/compiler/types.scm
@@ -15,14 +15,18 @@
 ;;; <http://www.gnu.org/licenses/>.
 
 (define-module (compiler types)
+  #:use-module ((rnrs base) #:select (assert))
   #:use-module (lens)
+  #:use-module (srfi srfi-1)
   #:use-module (srfi srfi-9)
   #:export (make-policy
             policy?
             policy-package
             policy-imports
+            policy-scope
             policy-rules
             policy-comments
+            ι-policy-scope
             ι-policy-rules
 
             make-rule
@@ -81,6 +85,7 @@
             make-scope
             scope?
             scope-identifiers
+            scope-contains?
 
             make-funcall
             <funcall>
@@ -103,10 +108,11 @@
 
 ;; Type representing an individual `.rego' file
 (define-record-type <policy>
-  (make-policy package imports rules comments)
+  (make-policy package imports scope rules comments)
   policy?
   (package  policy-package)
   (imports  policy-imports)
+  (scope    policy-scope)
   (rules    policy-rules)
   (comments policy-comments))
 
@@ -117,9 +123,21 @@
           (make-policy
            (policy-package s)
            (policy-imports s)
+           (policy-scope s)
            (f (policy-rules s))
            (policy-comments s)))))
 
+(define (ι-policy-scope)
+  "Lens for focusing the global of a <policy>"
+  (lens policy-rules
+        (lambda (s f)
+          (make-policy
+           (policy-package s)
+           (policy-imports s)
+           (f (policy-scope s))
+           (policy-rules s)
+           (policy-comments s)))))
+
 ;; The intensional database of a Rego program is defined by its rules.
 (define-record-type <rule>
   (make-rule default head body)
@@ -212,6 +230,22 @@
   scope?
   (identifiers scope-identifiers))
 
+(define (scope-contains? scope breadcrumb identifier)
+  "Whether SCOPE contains IDENTIFIER at the point indicated by BREADCRUMB
+
+`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 (assoc-ref (scope-identifiers scope) breadcrumb) '()))
+        (if (null? breadcrumb)
+            #t
+            ;; (lean-builtin-function? (reference->lean-name identifier))
+            (recur (drop-right breadcrumb 1)))))
+  (assert (scope? scope))
+  (assert (reference? identifier))
+  (assert (list? breadcrumb))
+  (recur breadcrumb))
+
 (define-record-type <funcall>
   (make-funcall ref args)
   funcall?
@@ -231,5 +265,4 @@
 (define-record-type <exists-some>
   (make-exists-some identifiers)
   exists-some?
-  (identifiers exists-some-identifiers)
-  )
+  (identifiers exists-some-identifiers))
diff --git a/compiler/utilities.scm b/compiler/utilities.scm
index dd43c13..7591536 100644
--- a/compiler/utilities.scm
+++ b/compiler/utilities.scm
@@ -18,10 +18,16 @@
   #:use-module (ice-9 match)
   #:use-module (srfi srfi-1)
   #:use-module (srfi srfi-31)
+  #:use-module (srfi srfi-69)
   #:export (alist?
             map-key
             update-alist
 
+            add-to-end
+
+            hash-table-append!
+            hash-table-append-item!
+
             fresh-identifier
             number->subscript))
 
@@ -45,6 +51,22 @@
   "Return X ∪ Y where the values for any duplicate keys come from Y"
   (append y (filter (lambda (kv) (not (member (car kv) y))) x)))
 
+(define (add-to-end xs x)
+  "Add a single item X to the end of XS"
+  (append xs (list x)))
+
+(define (hash-table-append! hash-table key xs)
+  "Append list XS to the value stored at KEY in HASH-TABLE, or '() if KEY not present"
+  (if (hash-table-exists? hash-table key)
+      (hash-table-set! hash-table key (append (hash-table-ref hash-table key) xs))
+      (hash-table-set! hash-table key xs)))
+
+(define (hash-table-append-item! hash-table key item)
+  "Append single ITEM to the value stored at KEY in HASH-TABLE, or '() if KEY not present"
+  (if (hash-table-exists? hash-table key)
+      (hash-table-set! hash-table key (add-to-end (hash-table-ref hash-table key) item))
+      (hash-table-set! hash-table key (list item))))
+
 (define* (fresh-identifier identifiers #:optional (pre "anonym"))
   "Return an identifier which does not occur in IDENTIFIERS"
   (define (try n)
diff --git a/compiler/walk.scm b/compiler/walk.scm
index dabd438..bffb74b 100644
--- a/compiler/walk.scm
+++ b/compiler/walk.scm
@@ -16,126 +16,58 @@
 
 (define-module (compiler walk)
   #:use-module (compiler types)
+  #:use-module (compiler utilities)
   #:use-module (ice-9 match)
+  #:use-module (lens)
   #:use-module (srfi srfi-1)
-  #:use-module (srfi srfi-69)
-  ;; #:use-module (srfi srfi-26)
-  ;; #:export ()
-  )
-
-(define types
-  '(null bool number string array set object
-    any))
-
-(define (more-specific? x y)
-  "Predicate on whether X is a more specific type than Y"
-  (cond ((eqv? y 'any) #t)
-        ((and (list? x)
-              (list? y)
-              (< (length x) (length y))) #t)
-        (else #f)))
-
-(define (add-to-end xs x)
-  (append xs (list x)))
-
-(define (hash-table-append! hash-table key xs)
-  (if (hash-table-exists? hash-table key)
-      (hash-table-set! hash-table key (append (hash-table-ref hash-table key) xs))
-      (hash-table-set! hash-table key xs)))
-
-(define (hash-table-append-item! hash-table key item)
-  (if (hash-table-exists? hash-table key)
-      (hash-table-set! hash-table key (add-to-end (hash-table-ref hash-table key) item))
-      (hash-table-set! hash-table key (list item))))
-
-(define (identify-scope policy)
-  (define scopes (make-hash-table))
-  (define (recur breadcrumb form)
-    (match form
-      ;; A rule body introduces a new scope.
-      (($ <body> conjunction)
-       (let ((identified-variables (recur breadcrumb conjunction)))
-         (when (not (null? identified-variables))
-           (hash-table-append! scopes breadcrumb identified-variables)))
-       '())
-
-      ;; Quantification introduces a new scope.
-      ;;
-      ;; This is implemented by propagating upwards. The new scope will be
-      ;; reflected when later terms query for their enclosing scope.
-      (($ <exists-some> identifiers)
-       ;; Inner is a <variable-ref>.
-       (recur breadcrumb identifiers))
-      (($ <for-all> key domain value body) ; TODO: Domain gives us some constraints on the type.
-       ;; Inner is a <variable-ref>.
-       (recur breadcrumb key))
-
-      ;; TODO: I know that a comprehension is going to create a new scope for
-      ;; the body, but I'm not yet sure how we're going to use `key' or `value'.
-      (($ <comprehension> _ key value body)
-       (error "unimplemented"))
-
-      ;; Indices are used to create a breadcrumb trail when dereferencing lists.
-      ((x xs ...)
-       (fold append '()
-             (map (lambda (x i)
-                    (recur (add-to-end breadcrumb i) x))
-                  (cons x xs)
-                  (iota (+ 1 (length xs))))))
-
-      ;; TODO: In what cases do we error out, instead of treating this as a free variable?
-      (($ <variable-ref> name)
-       `((,(make-reference (list (make-variable-ref name))) any)))
-      (($ <funcall> _ args)
-       (recur breadcrumb args))
-
-      ;; Anything else is a terminal, giving us no further information about the scope.
-      ;;
-      ;; - References
-      ;; - Constants
-      ;;   - Set and object literals
-      ;;
-      ;; `recur' won't encounter heads. Similarly, policy documents can't be nested.
-      (_ '())))
-  (for-each (lambda (rule)
-              (hash-table-append-item! scopes '() `(,(head-lhs (rule-head rule)) any))
-              (recur (list (head-lhs (rule-head rule)))
-                     (rule-body rule)))
-            (map cadr (policy-rules policy)))
-  scopes)
+  #:use-module (srfi srfi-26)
+  #:export (mutate-tree))
 
 (define (mutate-tree policy f)
-  (define (recur form)
+  ;; TODO: Document interface for `f'.
+  ;;
+  ;; Called as `(f scope breadcrumb form)'
+  (define scope (policy-scope policy))
+  (define (recur breadcrumb form)
     (match form
       ((x xs ...)
-       (map (lambda (x) (f (recur x))) (cons x xs)))
+       (map (lambda (x i)
+              (let ((breadcrumb (add-to-end breadcrumb i)))
+                (f scope breadcrumb (recur breadcrumb x))))
+            (cons x xs)
+            (iota (+ 1 (length xs)))))
 
       ;; TODO: Should this include the `head' of a rule too?
       (($ <rule> default head body)
-       (f (make-rule default head (recur body))))
+       (let* ((breadcrumb (add-to-end breadcrumb (head-lhs head)))
+              (inner (make-rule default head (recur breadcrumb body))))
+         (f scope breadcrumb inner)))
       (($ <body> conjunction)
-       (f (make-body (recur conjunction))))
+       (let ((inner (make-body (recur breadcrumb conjunction))))
+         (f scope breadcrumb inner)))
+      (($ <exists-some> identifiers)
+       (let* ((breadcrumb breadcrumb)
+              (inner (make-exists-some (recur breadcrumb identifiers))))
+         (f scope breadcrumb inner)))
       (($ <for-all> domain key value body)
-       (f (make-for-all domain key value (recur body))))
+       (let* ((breadcrumb breadcrumb)
+              (inner (make-for-all domain key value (recur breadcrumb body))))
+         (f scope breadcrumb inner)))
       (($ <comprehension> kind key value body)
-       (f (make-comprehension kind key value (recur body))))
-
+       (error "unimplemented")
+       ;; (let* ((breadcrumb breadcrumb)
+       ;;        (inner (make-comprehension kind key value (recur breadcrumb body))))
+       ;;   (f scope breadcrumb inner))
+       )
       (($ <reference> parts)
-       (f (make-reference (recur parts))))
-      (anything-else (f anything-else))))
-  (make-policy
-   (policy-package policy)
-   (policy-imports policy)
-   (zip (map car (policy-rules policy))
-        (map (compose recur cadr) (policy-rules policy)))
-   (policy-comments policy)))
+       (let* ((breadcrumb breadcrumb)
+              (inner (make-reference (recur breadcrumb parts))))
+         (f scope breadcrumb inner)))
+
+      (anything-else (f scope breadcrumb anything-else))))
 
-(define (my-rewrite-anonymous form)
-  (match form
-    (($ <variable-ref> name)
-     (make-variable-ref
-      (if (string= name "$0")
-          "anony_0"
-          name)))
-    (anything-else
-     anything-else)))
+  (over (ι-policy-rules)
+        (lambda (rules)
+          (zip (map car rules)
+               (map (compose (cut recur '() <>) cadr) rules)))
+        policy))