aboutsummaryrefslogtreecommitdiff
path: root/rego-proofs/compiler/passes/bool-to-prop.scm
diff options
context:
space:
mode:
authorJakob L. Kreuze2023-12-21 13:38:41 -0500
committerJakob L. Kreuze2023-12-21 13:38:41 -0500
commit4ef90bd4f04a9df089c31f6eb44f5cb3c2680c49 (patch)
treec7b78f5282ee36b5c22ff6a707b065288bef7d8f /rego-proofs/compiler/passes/bool-to-prop.scm
parentbe7067d632aa665c20f96d3b344a84c95b0f8ff8 (diff)
Get rid of old compiler code
Diffstat (limited to 'rego-proofs/compiler/passes/bool-to-prop.scm')
-rw-r--r--rego-proofs/compiler/passes/bool-to-prop.scm51
1 files changed, 0 insertions, 51 deletions
diff --git a/rego-proofs/compiler/passes/bool-to-prop.scm b/rego-proofs/compiler/passes/bool-to-prop.scm
deleted file mode 100644
index 4c2fb95..0000000
--- a/rego-proofs/compiler/passes/bool-to-prop.scm
+++ /dev/null
@@ -1,51 +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 bool-to-prop)
- #:use-module (compiler lean)
- #:use-module (compiler types)
- #:use-module (compiler utilities)
- #:use-module (ice-9 match)
- #:use-module (oop goops)
- #:export (compile-bool-to-prop))
-
-(define (compile-bool-to-prop policy)
- (define (rewrite-top-level form)
- (match form
- (($ <constant> value)
- (if (boolean? value)
- (make <lean-compare>
- #:kind 'eq
- #:left form
- #:right (make <constant> #:value #t))
- form))
- (($ <lean-assignment-chain> value)
- (make <lean-compare>
- #:kind 'eq
- #:left form
- #:right (make <constant> #:value #t)))
- (_ form)))
- (policy-map
- policy
- (lambda (_scope _breadcrumb form)
- (match form
- (($ <lean-conjunction> conjunction)
- (make <lean-conjunction>
- #:clauses (map rewrite-top-level conjunction)))
- (($ <for-all> _domain _key _value conjunction)
- (with-modified-slot form 'body
- (map rewrite-top-level conjunction)))
- (_ form)))))

© 2015 - 2026 Jakob L. Kreuze