blob: 82849e32b89180a1766d2599d688259dd7004576 (
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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
;;; 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-exists-some)
#: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-26)
#:export (compile-exists-some))
(define (exists-some? form)
(is-a? form <exists-some>))
(define (exists-some->variables identifiers)
(map (lambda (x)
(match x
(($ <variable-ref> _) x)
(($ <funcall>
($ <reference>
(($ <variable-ref> "internal")
($ <constant> "member_2")))
args)
(first args))))
identifiers))
(define (exists-some->constraints identifiers)
(fold append '()
(map (lambda (x)
(match x
(($ <variable-ref> _) '())
(($ <funcall>
($ <reference>
(($ <variable-ref> "internal")
($ <constant> "member_2")))
args)
`(,x))))
identifiers)))
(define (process-quantified-extent scope breadcrumb xs)
(assert (list? xs))
(if (and (positive? (length xs))
(exists-some? (first xs)))
;; Add any extracted variables to the scope.
(let ((variables (exists-some->variables (identifiers (first xs)))))
(for-each (lambda (variable)
(let ((local (make <local>
#:identifier variable
#:lean-name variable)))
;; (format #t "Here: ~a~%" (to-pretty-sexp local))
(add-to-scope scope breadcrumb local)))
variables)
(make <lean-exists>
#:variables variables
#:body
(make <lean-conjunction>
#:clauses (append (exists-some->constraints (identifiers (first xs)))
(drop xs 1)))))
xs))
(define (process-all scope breadcrumb form)
(assert (list? form))
(map (cut process-quantified-extent scope breadcrumb <>)
(partition-on form exists-some?)))
(define (compile-exists-some policy)
(policy-map
policy
(lambda (scope breadcrumb form)
(if (and (list? form) (any exists-some? form))
(process-all scope breadcrumb form)
form))))
|
© 2015 - 2026 Jakob L. Kreuze
