aboutsummaryrefslogtreecommitdiff
path: root/rego-proofs/compiler/passes/compile-local-references.scm
blob: 42d4585dc57f29e6c05201d9d8c0df8960a65d01 (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
;;; 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-local-references)
  #: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 (ice-9 pretty-print)
  #:use-module (oop goops)
  #:use-module (srfi srfi-1)
  #:use-module (srfi srfi-11)
  #:export (compile-local-references))

(define (extract-references-to-unresolved scope breadcrumb form)
  ;; TODO: Document me!
  (define new-identifiers (list))
  (define new-clauses (list))
  (define (recur scope breadcrumb form)
    (match form
      (($ <variable-ref> name)
       ;; FIXME: Really, we should panic if the above fails.
       ;; (unless (scope-contains? scope breadcrumb)
       ;;   (error "reference to unidentified variable" name))
       (let ((local (find-local scope breadcrumb form)))
         (if (and local (not (resolved? local)))
             (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))
               ;; FIXME: This is syntactically a funcall but semantically something else.
               (set! new-clauses `(,(make <lean-funcall>
                                      #:name (lean-name local)
                                      #:args `(,new-ref))
                                   ,@new-clauses))
               (make <variable-ref> #:name (lean-name local)))
             form                       ; See above
             )))
      (_ form)))
  (let ((result (tree-map form recur scope breadcrumb)))
    (values new-identifiers `(,@result ,@new-clauses))))

(define (compile-local-references policy)
  (policy-map
   policy
   (lambda (scope breadcrumb form)
     (match form
       (($ <lean-conjunction> clauses)
        (let-values (((new-identifiers new-clauses) (extract-references-to-unresolved 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