Lift implicit anonymous variables (e.g., `$0`) to `exists-some`

4 files changed, 63 insertions, 2 deletions

diff --git a/compiler/main.scm b/compiler/main.scm
index 04809c8..164d823 100644
--- a/compiler/main.scm
+++ b/compiler/main.scm
@@ -25,6 +25,7 @@
   #:use-module (compiler passes emit-specification)
   #:use-module (compiler passes extract-identifiers)
   #:use-module (compiler passes lift-comprehensions)
+  #:use-module (compiler passes lift-implicit-anonymous)
   #:use-module (compiler passes parse-policy)
   #:use-module (compiler passes read-and-parse)
   #:use-module (compiler utilities)
@@ -50,6 +51,7 @@ of `(program-arguments)'."
            (policy (compile-for-all policy))
            (policy (compile-object-literal policy))
            (policy (extract-identifiers policy))
+           (policy (lift-implicit-anonymous policy))
            (policy (compile-constraints policy))
            (policy (compile-funcall policy))
            (policy (compile-reference policy))
diff --git a/compiler/passes/lift-implicit-anonymous.scm b/compiler/passes/lift-implicit-anonymous.scm
new file mode 100644
index 0000000..5e0c0fa
--- /dev/null
+++ b/compiler/passes/lift-implicit-anonymous.scm
@@ -0,0 +1,58 @@
+;;; 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 lift-implicit-anonymous)
+  #: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-11)
+  #:export (lift-implicit-anonymous))
+
+(define (extract-anonymous-references scope breadcrumb form)
+  ;; FIXME: Do we need to validate that a generated name doesn't conflict with
+  ;; /any/ child scopes of the <conjunction>?
+  (define new-identifiers (list))
+  (define (recur scope breadcrumb form)
+    (match form
+      (($ <variable-ref> name)
+       (if (string-prefix? "$" name)
+           (let* ((new-ident (fresh-identifier (all-valid-identifiers scope breadcrumb)))
+                  (new-ref (make <variable-ref> #:name new-ident)))
+             (set! new-identifiers `(,new-ref ,@new-identifiers))
+             new-ref)
+           form))
+      (_ form)))
+  (let ((result (tree-map form recur scope breadcrumb)))
+    (values new-identifiers result)))
+
+(define (lift-implicit-anonymous policy)
+  (policy-map
+    policy
+    (lambda (scope breadcrumb form)
+      (match form
+        (($ <body> clauses)
+         (let-values (((new-identifiers new-clauses) (extract-anonymous-references scope breadcrumb clauses)))
+           (if (positive? (length new-identifiers))
+               (make <body>
+                 #:conjunction
+                 `(,(make <lean-exists>
+                      #:variables new-identifiers
+                      #:body new-clauses)))
+               form)))
+        (_ form)))))
diff --git a/compiler/test.scm b/compiler/test.scm
index 23b6898..3479d0f 100644
--- a/compiler/test.scm
+++ b/compiler/test.scm
@@ -25,6 +25,7 @@
   #:use-module (compiler passes emit-specification)
   #:use-module (compiler passes extract-identifiers)
   #:use-module (compiler passes lift-comprehensions)
+  #:use-module (compiler passes lift-implicit-anonymous)
   #:use-module (compiler passes parse-policy)
   #:use-module (compiler passes read-and-parse)
   #:use-module (compiler types)
@@ -479,6 +480,7 @@ Error if POLICY has more than one rule."
          (policy (compile-for-all policy))
          (policy (compile-object-literal policy))
          (policy (extract-identifiers policy))
+         (policy (lift-implicit-anonymous policy))
          (policy (compile-constraints policy))
          (policy (compile-funcall policy))
          (policy (compile-reference policy))
diff --git a/compiler/types.scm b/compiler/types.scm
index ec5de53..9a0fe2f 100644
--- a/compiler/types.scm
+++ b/compiler/types.scm
@@ -402,8 +402,7 @@ and `identifier' is a <reference>"
   (match form
     (($ <reference> parts)
      (let ((inner (with-modified-slot form 'parts
-                    (map (cut tree-map <> f scope breadcrumb)
-                         parts))))
+                    (tree-map parts f scope breadcrumb))))
        (f scope breadcrumb inner)))))
 
 ;; A name within a lexical environment.