1 files changed, 0 insertions, 74 deletions
diff --git a/rego-proofs/compiler/passes/compile-local-references.scm b/rego-proofs/compiler/passes/compile-local-references.scm
deleted file mode 100644
index 42d4585..0000000
--- a/rego-proofs/compiler/passes/compile-local-references.scm
+++ /dev/null
@@ -1,74 +0,0 @@
-;;; 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-local-references)
-  #: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 (ice-9 pretty-print)
-  #:use-module (oop goops)
-  #:use-module (srfi srfi-1)
-  #:use-module (srfi srfi-11)
-  #:export (compile-local-references))
-
-(define (extract-references-to-unresolved scope breadcrumb form)
-  ;; TODO: Document me!
-  (define new-identifiers (list))
-  (define new-clauses (list))
-  (define (recur scope breadcrumb form)
-    (match form
-      (($ <variable-ref> name)
-       ;; FIXME: Really, we should panic if the above fails.
-       ;; (unless (scope-contains? scope breadcrumb)
-       ;;   (error "reference to unidentified variable" name))
-       (let ((local (find-local scope breadcrumb form)))
-         (if (and local (not (resolved? local)))
-             (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))
-               ;; FIXME: This is syntactically a funcall but semantically something else.
-               (set! new-clauses `(,(make <lean-funcall>
-                                      #:name (lean-name local)
-                                      #:args `(,new-ref))
-                                   ,@new-clauses))
-               (make <variable-ref> #:name (lean-name local)))
-             form                       ; See above
-             )))
-      (_ form)))
-  (let ((result (tree-map form recur scope breadcrumb)))
-    (values new-identifiers `(,@result ,@new-clauses))))
-
-(define (compile-local-references policy)
-  (policy-map
-   policy
-   (lambda (scope breadcrumb form)
-     (match form
-       (($ <lean-conjunction> clauses)
-        (let-values (((new-identifiers new-clauses) (extract-references-to-unresolved scope breadcrumb clauses)))
-          ;; Add new identifiers to the scope.
-          (for-each (lambda (identifier)
-                      (add-to-scope scope breadcrumb (variable-ref->local identifier)))
-                    new-identifiers)
-          (if (positive? (length new-identifiers))
-              (make <lean-conjunction>
-                #:clauses
-                `(,(make <lean-exists>
-                     #:variables new-identifiers
-                     #:body new-clauses)))
-              form)))
-       (_ form)))))