1 files changed, 0 insertions, 74 deletions
diff --git a/rego-proofs/compiler/passes/compile-definition.scm b/rego-proofs/compiler/passes/compile-definition.scm
deleted file mode 100644
index b9f7ce8..0000000
--- a/rego-proofs/compiler/passes/compile-definition.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-definition)
-  #: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-definition))
-
-(define (find-default rules)
-  (find default-rule? rules))
-
-(define (all-but-default rules)
-  (let ((result (filter (negate default-rule?) rules)))
-    (unless (member (- (length rules) (length result)) '(0 1) )
-      (error "expected at most 1 default rule, found"
-             (- (length rules) (length result))))
-    result))
-
-(define (process-rule-group rule-group)
-  (define subject-ref (make <variable-ref> #:name "rulesubject"))
-  (define (collapse-rule rule)
-    (match rule
-      (($ <rule> default head ($ <body> clauses) else-arm)
-       (make <lean-conjunction>
-         #:clauses `(,@clauses
-                     ,(make <lean-compare>
-                        #:left subject-ref
-                        #:right (right head)
-                        #:kind 'eq))))))
-  (match rule-group
-    ((left rules ...)
-     (list
-      (make <definition>
-        #:left left
-        #:kind (kind (head (first rules))) ;; TODO: When do we rewrite as `plain'?
-        #:right #f
-        #:default (let ((default (find-default rules)))
-                    (if default
-                        (collapse-rule default)
-                        default))
-        #:rules (map collapse-rule (all-but-default rules)))
-      (variable-ref->local subject-ref)))))
-
-;; Convert grouped rules into a `<definition>'
-(define (compile-definition policy)
-  (define new-scope (scope policy))
-  (define new-rules
-    (map (lambda (rule-group)
-           (match (process-rule-group rule-group)
-             ((definition subject-ref)
-              (add-to-scope new-scope `(,(left definition)) subject-ref) 
-              definition)))
-         (rules policy)))
-  (with-modified-slot (with-modified-slot policy 'rules new-rules) 'scope new-scope))