blob: cb718e8e78f8fadbdcef1148db45f2e75d50da78 (
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
|
;;; 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 lift-implicit-anonymous)
#: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-11)
#:export (lift-implicit-anonymous))
(define (extract-anonymous-references scope breadcrumb form)
;; FIXME: Do we need to validate that a generated name doesn't conflict with
;; /any/ child scopes of the <conjunction>?
(define new-identifiers (list))
(define (recur scope breadcrumb form)
(match form
(($ <variable-ref> name)
(if (string-prefix? "$" name)
(let* ((new-ident (fresh-identifier (all-valid-identifiers scope breadcrumb)))
(new-ref (make <variable-ref> #:name new-ident)))
(set! new-identifiers `(,new-ref ,@new-identifiers))
new-ref)
form))
(_ form)))
(let ((result (tree-map form recur scope breadcrumb)))
(values new-identifiers result)))
(define (lift-implicit-anonymous policy)
(policy-map
policy
(lambda (scope breadcrumb form)
(match form
(($ <lean-conjunction> clauses)
(let-values (((new-identifiers new-clauses) (extract-anonymous-references scope breadcrumb clauses)))
;; Add new identifiers to the scope.
(for-each (lambda (identifier)
(add-to-scope scope breadcrumb (variable-ref->local identifier)))
new-identifiers)
(if (positive? (length new-identifiers))
(make <lean-conjunction>
#:clauses
`(,(make <lean-exists>
#:variables new-identifiers
#:body new-clauses)))
form)))
(_ form)))))
|
© 2015 - 2026 Jakob L. Kreuze
