Initial compilation of 08-object-comprehension.rego

8 files changed, 120 insertions, 14 deletions

diff --git a/compiler/lean.scm b/compiler/lean.scm
index 064683b..11e6b5c 100644
--- a/compiler/lean.scm
+++ b/compiler/lean.scm
@@ -27,6 +27,7 @@
             <lean-computable-definition>
             <lean-expression>
             <lean-exists>
+            <lean-for-all>
             <lean-conjunction>
             <lean-compare>
             <lean-funcall>
@@ -86,6 +87,21 @@
                     (tree-map body f scope breadcrumb))))
        (f scope breadcrumb inner)))))
 
+;; Compiled to ∀
+(define-class <lean-for-all> (<lean-expression>)
+  ;; list of identifier/type pairs
+  (variables #:init-keyword #:variables
+             #:getter       variables)
+  (body      #:init-keyword #:body
+             #:getter       body))
+
+(define-method (tree-map (form <lean-for-all>) f scope breadcrumb)
+  (match form
+    (($ <lean-for-all> variables body)
+     (let ((inner (with-modified-slot form 'body
+                    (tree-map body f scope breadcrumb))))
+       (f scope breadcrumb inner)))))
+
 ;; Compiled to ∧
 (define-class <lean-conjunction> (<lean-expression>)
   (clauses #:init-keyword #:clauses
@@ -220,6 +236,17 @@
      ", "
      ,(wrap (compile (body x))))))
 
+(define-method (compile (x <lean-for-all>))
+  (string-concatenate
+   `("∀ "
+     ,(string-join
+       (map (lambda (identifier)
+              (format #f "(~a : Rego.Any)" (compile identifier)))
+            (variables x))
+       " ")
+     ", "
+     ,(wrap (compile (body x))))))
+
 (define-method (compile (x <lean-funcall>))
   (string-concatenate
    `(,(name x)
diff --git a/compiler/main.scm b/compiler/main.scm
index 6246d08..d395711 100644
--- a/compiler/main.scm
+++ b/compiler/main.scm
@@ -15,12 +15,15 @@
 ;;; <http://www.gnu.org/licenses/>.
 
 (define-module (compiler main)
+  #:use-module (compiler passes bool-to-prop)
   #:use-module (compiler passes compile-constraints)
   #:use-module (compiler passes compile-exists-some)
+  #:use-module (compiler passes compile-for-all)
   #:use-module (compiler passes compile-funcall)
   #:use-module (compiler passes compile-reference)
   #:use-module (compiler passes emit-specification)
   #:use-module (compiler passes extract-identifiers)
+  #:use-module (compiler passes lift-comprehensions)
   #:use-module (compiler passes parse-policy)
   #:use-module (compiler passes preprocess-policy)
   #:use-module (compiler passes read-and-parse)
@@ -43,7 +46,9 @@ of `(program-arguments)'."
     (let* ((ast (read-and-parse policy-file-name))
            (policy (preprocess-policy ast))
            (policy (parse-policy policy))
+           (policy (compile-comprehensions policy))
            (policy (compile-exists-some policy))
+           (policy (compile-for-all policy))
            (policy (extract-identifiers policy))
            (policy (compile-constraints policy))
            (policy (compile-funcall policy))
diff --git a/compiler/passes/bool-to-prop.scm b/compiler/passes/bool-to-prop.scm
index c5acacb..d0a658b 100644
--- a/compiler/passes/bool-to-prop.scm
+++ b/compiler/passes/bool-to-prop.scm
@@ -47,7 +47,5 @@
           #:conjunction (map rewrite-top-level conjunction)))
        (($ <for-all> _domain _key _value conjunction)
         (with-modified-slot form 'body
-          (map rewrite-top-level conjunction))
-        (make <for-all>
-          #:conjunction (map rewrite-top-level conjunction)))
+          (map rewrite-top-level conjunction)))
        (_ form)))))
diff --git a/compiler/passes/compile-constraints.scm b/compiler/passes/compile-constraints.scm
index ad1f447..8314f04 100644
--- a/compiler/passes/compile-constraints.scm
+++ b/compiler/passes/compile-constraints.scm
@@ -112,4 +112,4 @@
         (if (any is-local-assignment? xs)
             (process-all xs)
             xs))
-       (anything-else anything-else)))))
+       (_ form)))))
diff --git a/compiler/passes/compile-for-all.scm b/compiler/passes/compile-for-all.scm
new file mode 100644
index 0000000..60f0591
--- /dev/null
+++ b/compiler/passes/compile-for-all.scm
@@ -0,0 +1,43 @@
+;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org>
+;;;
+;;; This program is free software; you can redistribute it and/or
+;;; modify it under the terms of the GNU General Public License as
+;;; published by the Free Software Foundation; either version 3 of the
+;;; License, or (at your option) any later version.
+;;;
+;;; This program is distributed in the hope that it will be useful,
+;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+;;; General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with this program. If not, see
+;;; <http://www.gnu.org/licenses/>.
+
+(define-module (compiler passes compile-for-all)
+  #:use-module ((rnrs base) #:select (assert))
+  #:use-module (compiler lean)
+  #:use-module (compiler types)
+  #:use-module (compiler utilities)
+  #:use-module (ice-9 match)
+  #:use-module (oop goops)
+  #:use-module (srfi srfi-1)
+  #:export (compile-for-all))
+
+(define (compile-for-all policy)
+  (policy-map
+   policy
+   (lambda (scope breadcrumb form)
+     (match form
+       (($ <for-all> domain key value body)
+        (make <lean-for-all>
+          #:variables `(,value)
+          #:body (make <lean-conjunction>
+                   #:clauses
+                   `(,(cond ;; TODO: Type inference.
+                       (else (make <lean-funcall>
+                               #:name "Array.contains"
+                               #:args `(,value ,domain)
+                               )))
+                     ,@body))))
+       (_ form)))))
diff --git a/compiler/passes/compile-reference.scm b/compiler/passes/compile-reference.scm
index 72ed777..ca48d84 100644
--- a/compiler/passes/compile-reference.scm
+++ b/compiler/passes/compile-reference.scm
@@ -72,6 +72,8 @@
    policy
    (lambda (scope breadcrumb form)
      (match form
+       (($ <reference> (singleton))
+        singleton)
        (($ <reference> (first rest ...))
         (make <lean-assignment-chain> #:identifiers ((specialize breadcrumb scope) first rest '())))
        (_ form)))))
diff --git a/compiler/passes/extract-identifiers.scm b/compiler/passes/extract-identifiers.scm
index 377fe6a..1f3e31d 100644
--- a/compiler/passes/extract-identifiers.scm
+++ b/compiler/passes/extract-identifiers.scm
@@ -30,8 +30,6 @@
 
 (define any-type '(null bool number string array object))
 
-(use-modules (ice-9 pretty-print))
-
 (define (identify-variables policy)
   "Recursively search the body of a <rule> for variable occurrences"
   (define new-scope (make <scope> #:identifiers (make-hash-table)))
@@ -71,17 +69,30 @@
                (lhs        (left (head rule)))
                (rhs        (right (head rule))))
           (match `(,lhs ,rhs)
-            ((($ <reference> (($ <variable-ref> identifier-left))) ($ <variable-ref> identifier))
+            ((($ <reference> (($ <variable-ref> identifier-left)))
+              ($ <reference> (($ <variable-ref> identifier))))
+             (add-to-scope new-scope breadcrumb (first (inner rhs))
+                           `(membero ,(canonicalize identifier breadcrumb)
+                                     ,any-type))
+             (add-to-scope new-scope breadcrumb (make <variable-ref> #:name identifier)
+                           `(== ,(canonicalize identifier-left breadcrumb)
+                                ,(canonicalize identifier breadcrumb))))
+            ;; Deprecated form?
+            ((($ <reference> (($ <variable-ref> identifier-left)))
+              ($ <variable-ref> identifier))
              (add-to-scope new-scope breadcrumb rhs
                            `(membero ,(canonicalize identifier breadcrumb)
                                      ,any-type))
              (add-to-scope new-scope breadcrumb (make <variable-ref> #:name identifier)
                            `(== ,(canonicalize identifier-left breadcrumb)
                                 ,(canonicalize identifier breadcrumb))))
-            ((($ <reference> (($ <variable-ref> identifier))) ($ <constant> value))
+            ((($ <reference> (($ <variable-ref> identifier)))
+              ($ <constant> value))
              (add-to-scope new-scope breadcrumb (make <variable-ref> #:name identifier)
                            `(== ,(canonicalize identifier breadcrumb)
-                                ,(scheme-value->type value)))))))
+                                ,(scheme-value->type value))))
+            (_ #f ;; TODO: Type inference should work on object keys as well.
+             ))))
       (cdr rule-group)
       (iota (length (cdr rule-group)))))
    (rules policy))
diff --git a/compiler/types.scm b/compiler/types.scm
index d3ee3dc..94c1e1b 100644
--- a/compiler/types.scm
+++ b/compiler/types.scm
@@ -29,6 +29,7 @@
             <policy>
             scope
             rules
+            policy-top-level-names
             ι-policy-scope
             ι-policy-rules
 
@@ -114,6 +115,10 @@
   (comments #:init-value #f
             #:init-keyword #:comments))
 
+(define (policy-top-level-names policy)
+  "Names of all rules defined in POLICY"
+  (map car (rules policy)))
+
 (define (ι-policy-rules)
   "Lens for focusing the rules of a <policy>"
   (lens (lambda (s)   (slot-ref s 'rules))
@@ -139,12 +144,13 @@
         (lambda (s f) (map-slot s 'body f))))
 
 (define-method (tree-map (form <rule>) f scope breadcrumb)
-  ;; 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 (name head)))
-            (inner (with-modified-slot form 'body
+            (inner (with-modified-slot form 'head
+                     (tree-map head f scope breadcrumb)))
+            (inner (with-modified-slot inner 'body
                      (tree-map body f scope breadcrumb))))
        (f scope breadcrumb inner)))))
 
@@ -152,13 +158,25 @@
 (define-class <head> ()
   (name #:init-keyword #:name
         #:accessor     name)
-  (kind #:init-keyword #:kind ; memq '(value-eqv field-eqv set-memq)
+  (kind #:init-keyword #:kind ; memq '(value-eqv field-eqv set-memq array-memq)
         #:accessor     kind)
   (lhs  #:init-keyword #:lhs
         #:accessor     left)
   (rhs  #:init-keyword #:rhs
         #:accessor     right))
 
+(define-method (tree-map (form <head>) f scope breadcrumb)
+  (match form
+    (($ <head> name kind lhs rhs)
+     ;; A rule body introduces a new scope.
+     (let* ((inner (with-modified-slot form 'kind
+                     (tree-map kind f scope breadcrumb)))
+            ;; (inner (with-modified-slot inner 'lhs
+            ;;          (tree-map lhs f scope breadcrumb)))
+            (inner (with-modified-slot inner 'rhs
+                     (tree-map rhs f scope breadcrumb))))
+       (f scope breadcrumb inner)))))
+
 ;; A conjunction that defines whether a rule should apply.
 (define-class <body> ()
   (conjunction #:init-keyword #:conjunction
@@ -181,6 +199,9 @@
 (define-class <constant> ()
   (value #:init-keyword #:value)) ; scheme value
 
+(define-method (tree-map (form <constant>) f scope breadcrumb)
+  (f scope breadcrumb form))
+
 (define-class <set-literal> ()
   (elems #:init-keyword #:elems)) ; list of [scheme value | <set-literal> | <object-literal>]
 
@@ -333,8 +354,7 @@ and `identifier' is a <reference>"
   (match form
     (($ <for-all> domain key value body)
      (let ((inner (with-modified-slot form 'body
-                    (map (cut tree-map <> f scope breadcrumb)
-                         body))))
+                    (tree-map body f scope breadcrumb))))
        (f scope breadcrumb inner)))))
 
 (define-class <exists-some> ()