diff options
Diffstat (limited to 'rego-proofs/compiler/passes/bool-to-prop.scm')
| -rw-r--r-- | rego-proofs/compiler/passes/bool-to-prop.scm | 51 |
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))))) |