blob: ccc41852c553ce7ed0169cec0a147d1586274c36 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
;;; 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)))))
|
© 2015 - 2026 Jakob L. Kreuze
