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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
;;; 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-constraints)
#: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 (srfi srfi-1)
#:use-module (srfi srfi-26)
#:use-module (oop goops)
#:export (compile-constraints))
;; > The assignment operator (:=) is used to assign values to variables.
;; > Variables assigned inside a rule are locally scoped to that rule and shadow
;; > global variables.
;;
;; In Lean, assignment is represented as a `let'. Internally, it adds an
;; identifier to the scope.
;;
;; > Comparison (==) checks if two values are equal within a rule. If the left
;; > or right hand side contains a variable that has not been assigned a value,
;; > the compiler throws an error.
;;
;; In Lean, comparison is represented as a comparison (specifically `=') in the
;; conjunction of a rule.
;;
;; Unification (=) combines assignment and comparison. Rego will assign
;; variables to values that make the comparison true. Unification lets you ask
;; for values for variables that make an expression true.
;;
;; Unification is also represented as a comparison in Lean, just with one of the
;; sides being a free variable.
(define (is-local-assignment? form)
(match form
((($ <reference> (($ <variable-ref> "assign"))) left right) #t)
(_ #f)))
(define (collapse-extents extents)
(match extents
(((singleton-form)) extents)
(((singleton-form) next ...)
(if (is-local-assignment? singleton-form)
(cons (cons singleton-form (first next))
(collapse-extents (drop next 1)))
(cons (first extents)
(collapse-extents (drop extents 1)))))
(_ extents)))
(define (process-local-extent scope breadcrumb xs)
(assert (list? xs))
(if (and (positive? (length xs))
(is-local-assignment? (first xs)))
(let ((assignments (take-while is-local-assignment? xs))
(body (drop-while is-local-assignment? xs)))
`(,(make <lean-intro-locals>
#:identifiers
(map (match-lambda
((($ <reference> (($ <variable-ref> "assign"))) left right)
;; We're defining a new local, so let's add it to the scope.
(let ((local (make <local>
#:identifier left
#:lean-name left
#:constraints
(match right
(($ <reference> (right-identifier))
`((== ,(canonicalize left breadcrumb)
,(canonicalize right (originating-breadcrumb scope breadcrumb right-identifier)))))
(($ <variable-ref> _)
`((== ,(canonicalize left breadcrumb)
,(canonicalize right (originating-breadcrumb scope breadcrumb right)))))
(($ <constant> value)
`((== ,(canonicalize left breadcrumb)
,(scheme-value->type value))))
(_ '())))))
(add-to-scope scope breadcrumb local))
`(,left ,right)))
assignments)
#:body
(make <lean-conjunction> #:clauses body))))
xs))
(define (process-all scope breadcrumb form)
(fold-right append '() (map (cut process-local-extent scope breadcrumb <>)
(collapse-extents (partition-on form is-local-assignment?)))))
(define (is-assignment? scope breadcrumb left)
(match left
(($ <reference> (($ <variable-ref> identifier)))
(not (scope-contains? scope breadcrumb identifier)))
(($ <variable-ref> identifier)
(not (scope-contains? scope breadcrumb left)))
(_ #f)))
(define (compile-constraints policy)
(policy-map
policy
(lambda (scope breadcrumb form)
(match form
((($ <reference> (($ <variable-ref> name))) left right)
(if (and (string= name "assign") (is-assignment? scope breadcrumb left))
form
(make <lean-compare>
#:kind (match name
("assign" 'eq)
("equal" 'eq)
("eq" 'eq)
("gt" 'gt)
("gte" 'ge)
("lt" 'lt)
("lte" 'le))
#:left left
#:right right)))
((xs ...)
(if (any is-local-assignment? xs)
(process-all scope breadcrumb xs)
xs))
(_ form)))))
|
