1 files changed, 0 insertions, 65 deletions
diff --git a/rego-proofs/compiler/passes/emit-specification.scm b/rego-proofs/compiler/passes/emit-specification.scm
deleted file mode 100644
index ae0ee45..0000000
--- a/rego-proofs/compiler/passes/emit-specification.scm
+++ /dev/null
@@ -1,65 +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 emit-specification)
-  #: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-2)
-  #:use-module (srfi srfi-26)
-  #:export (emit-specification))
-
-;; (define (compile-rule rule)
-;;   (assert (is-a? rule <rule>))
-;;   (match rule
-;;     (($ <rule> default head ($ <body> conjunction))
-;;      (make <lean-fact>
-;;        #:conclusion (right head)
-;;        #:body (if (> (length conjunction) 1)
-;;                   (make <lean-conjunction> #:clauses (map compile-expr conjunction))
-;;                   (first conjunction))))))
-
-(define (compile-definition definition)
-  (match definition
-    (($ <definition> kind left _right default rules)
-     (assert (is-a? left <reference>))
-     (make <lean-predicate>
-       ;; TODO: Not really correct now, is it?
-       #:kind kind
-       #:name (inductive-name definition)
-       ;; TODO: Find unique name
-       #:subject "rulesubject"
-       #:default default
-       #:facts rules))))
-
-(define (emit-specification policy)
-  "Emit a Lean file specifying the semantics of `policy'."
-  (assert (is-a? policy <policy>))
-  (match policy
-    (($ <policy> package imports _ rules _)
-     (format #t "-- package ~a~%" package)
-     (newline)
-     (for-each (cut format #t "-- imports ~a~%" <>) imports)
-     (newline)
-     (for-each (lambda (x)
-                 (display (compile x))
-                 (newline))
-               (map compile-definition rules))
-     (newline))))