1 files changed, 0 insertions, 89 deletions
diff --git a/rego-proofs/compiler/passes/compile-exists-some.scm b/rego-proofs/compiler/passes/compile-exists-some.scm
deleted file mode 100644
index 82849e3..0000000
--- a/rego-proofs/compiler/passes/compile-exists-some.scm
+++ /dev/null
@@ -1,89 +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-exists-some)
-  #: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)
-  #:use-module (srfi srfi-26)
-  #:export (compile-exists-some))
-
-(define (exists-some? form)
-  (is-a? form <exists-some>))
-
-(define (exists-some->variables identifiers)
-  (map (lambda (x)
-         (match x
-           (($ <variable-ref> _) x)
-           (($ <funcall>
-               ($ <reference>
-                  (($ <variable-ref> "internal")
-                   ($ <constant> "member_2")))
-               args)
-            (first args))))
-       identifiers))
-
-(define (exists-some->constraints identifiers)
-  (fold append '()
-        (map (lambda (x)
-               (match x
-                 (($ <variable-ref> _) '())
-                 (($ <funcall>
-                     ($ <reference>
-                        (($ <variable-ref> "internal")
-                         ($ <constant> "member_2")))
-                     args)
-                  `(,x))))
-             identifiers)))
-
-(define (process-quantified-extent scope breadcrumb xs)
-  (assert (list? xs))
-  (if (and (positive? (length xs))
-           (exists-some? (first xs)))
-      ;; Add any extracted variables to the scope.
-      (let ((variables (exists-some->variables (identifiers (first xs)))))
-        (for-each (lambda (variable)
-                    (let ((local (make <local>
-                                   #:identifier variable
-                                   #:lean-name  variable)))
-                      ;; (format #t "Here: ~a~%" (to-pretty-sexp local))
-                      (add-to-scope scope breadcrumb local)))
-                  variables)
-
-        (make <lean-exists>
-          #:variables variables
-          #:body
-          (make <lean-conjunction>
-            #:clauses (append (exists-some->constraints (identifiers (first xs)))
-                              (drop xs 1)))))
-      xs))
-
-(define (process-all scope breadcrumb form)
-  (assert (list? form))
-  (map (cut process-quantified-extent scope breadcrumb <>)
-       (partition-on form exists-some?)))
-
-(define (compile-exists-some policy)
-  (policy-map
-   policy
-   (lambda (scope breadcrumb form)
-     (if (and (list? form) (any exists-some? form))
-         (process-all scope breadcrumb form)
-         form))))