rego-proofs/compiler/passes/compile-definition.scm


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-definition)
  #: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-definition))

(define (find-default rules)
  (find default-rule? rules))

(define (all-but-default rules)
  (let ((result (filter (negate default-rule?) rules)))
    (unless (member (- (length rules) (length result)) '(0 1) )
      (error "expected at most 1 default rule, found"
             (- (length rules) (length result))))
    result))

(define (process-rule-group rule-group)
  (define subject-ref (make <variable-ref> #:name "rulesubject"))
  (define (collapse-rule rule)
    (match rule
      (($ <rule> default head ($ <body> clauses) else-arm)
       (make <lean-conjunction>
         #:clauses `(,@clauses
                     ,(make <lean-compare>
                        #:left subject-ref
                        #:right (right head)
                        #:kind 'eq))))))
  (match rule-group
    ((left rules ...)
     (list
      (make <definition>
        #:left left
        #:kind (kind (head (first rules))) ;; TODO: When do we rewrite as `plain'?
        #:right #f
        #:default (let ((default (find-default rules)))
                    (if default
                        (collapse-rule default)
                        default))
        #:rules (map collapse-rule (all-but-default rules)))
      (variable-ref->local subject-ref)))))

;; Convert grouped rules into a `<definition>'
(define (compile-definition policy)
  (define new-scope (scope policy))
  (define new-rules
    (map (lambda (rule-group)
           (match (process-rule-group rule-group)
             ((definition subject-ref)
              (add-to-scope new-scope `(,(left definition)) subject-ref) 
              definition)))
         (rules policy)))
  (with-modified-slot (with-modified-slot policy 'rules new-rules) 'scope new-scope))