diff options
| author | Jakob L. Kreuze | 2023-12-21 13:38:41 -0500 |
|---|---|---|
| committer | Jakob L. Kreuze | 2023-12-21 13:38:41 -0500 |
| commit | 4ef90bd4f04a9df089c31f6eb44f5cb3c2680c49 (patch) | |
| tree | c7b78f5282ee36b5c22ff6a707b065288bef7d8f /rego-proofs/compiler/passes/compile-for-all.scm | |
| parent | be7067d632aa665c20f96d3b344a84c95b0f8ff8 (diff) | |
Get rid of old compiler code
Diffstat (limited to 'rego-proofs/compiler/passes/compile-for-all.scm')
| -rw-r--r-- | rego-proofs/compiler/passes/compile-for-all.scm | 48 |
1 files changed, 0 insertions, 48 deletions
diff --git a/rego-proofs/compiler/passes/compile-for-all.scm b/rego-proofs/compiler/passes/compile-for-all.scm deleted file mode 100644 index ccc4185..0000000 --- a/rego-proofs/compiler/passes/compile-for-all.scm +++ /dev/null @@ -1,48 +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-for-all) - #: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) - #:export (compile-for-all)) - -(define (compile-for-all policy) - (policy-map - policy - (lambda (scope breadcrumb form) - (match form - (($ <for-all> domain key value body) - (assert (is-a? value <variable-ref>)) - - (let ((local (variable-ref->local value))) - (add-to-scope scope breadcrumb local)) - - (make <lean-for-all> - #:variables `(,value) - #:body (make <lean-conjunction> - #:clauses - `(,(cond ;; TODO: Type inference. - (else (make <lean-funcall> - #:name "Array.contains" - #:args `(,value ,domain) - ))) - ,@body)))) - (_ form))))) |