Initial fleshing out of idea

7 files changed, 168 insertions, 85 deletions

diff --git a/compiler/lean.scm b/compiler/lean.scm
index 3d16683..6e45f16 100644
--- a/compiler/lean.scm
+++ b/compiler/lean.scm
@@ -194,12 +194,6 @@
   (string-concatenate (list "(" s ")")))
 
 (define-method (compile (x <lean-predicate>))
-  (define suffix
-    (match (kind x)
-      ('value-eqv "_eqv")
-      ('field-eqv "_eqv")
-      ('set-memq  "_memq")))
-  (define inductive-name (string-concatenate `(,(name x) ,suffix)))
   (define has-default (default x))
   (define conditional-facts
     (filter (lambda (fact)
@@ -208,7 +202,7 @@
 
   (with-output-to-string
     (lambda ()
-      (format #t "inductive ~a (~a : Rego.Any) : Prop" inductive-name (subject x))
+      (format #t "inductive ~a (~a : Rego.Any) : Prop" (inductive-name (name x)) (subject x))
       (newline)
 
       (when has-default
@@ -217,7 +211,7 @@
                            #:clauses (map body conditional-facts)))
                 (subject x)                              ; (~a =( ~a))
                 (compile (conclusion (default x)))
-                inductive-name                           ; → ~a ~a
+                (inductive-name (name x))                ; → ~a ~a
                 (subject x))
         (newline))
 
@@ -227,21 +221,19 @@
            ;; Special case where the fact is true unconditionally.
            (($ <lean-compare> 'eq ($ <constant> #t) ($ <constant> #t))
             (format #t "| rule~a : (~a = (~a)) → ~a ~a"
-                     (number->subscript i) ; rule~a
-                     (subject x)           ; (~a = ~a)
+                     (number->subscript i)     ; rule~a
+                     (subject x)               ; (~a = ~a)
                      (compile (conclusion rule))
-                     inductive-name     ; → ~a
-                     (subject x)
-                     ))
+                     (inductive-name (name x)) ; → ~a
+                     (subject x)))
            (_
             (format #t "| rule~a : ~a → (~a = (~a)) → ~a ~a"
-                     (number->subscript i) ; rule~a
-                     (compile (body rule)) ; ~a →
-                     (subject x)           ; (~a = ~a)
+                     (number->subscript i)     ; rule~a
+                     (compile (body rule))     ; ~a →
+                     (subject x)               ; (~a = ~a)
                      (compile (conclusion rule))
-                     inductive-name     ; → ~a
-                     (subject x)
-                     )))
+                     (inductive-name (name x)) ; → ~a
+                     (subject x))))
          (newline))
        conditional-facts
        (iota (length conditional-facts))))))
diff --git a/compiler/main.scm b/compiler/main.scm
index 164d823..afea344 100644
--- a/compiler/main.scm
+++ b/compiler/main.scm
@@ -20,6 +20,7 @@
   #:use-module (compiler passes compile-exists-some)
   #:use-module (compiler passes compile-for-all)
   #:use-module (compiler passes compile-funcall)
+  #:use-module (compiler passes compile-local-references)
   #:use-module (compiler passes compile-object-literal)
   #:use-module (compiler passes compile-reference)
   #:use-module (compiler passes emit-specification)
@@ -29,6 +30,7 @@
   #:use-module (compiler passes parse-policy)
   #:use-module (compiler passes read-and-parse)
   #:use-module (compiler utilities)
+  #:use-module (ice-9 pretty-print)
   #:use-module (srfi srfi-1)
   #:export (main))
 
@@ -48,12 +50,16 @@ of `(program-arguments)'."
            (policy (parse-policy ast))
            (policy (compile-comprehensions policy))
            (policy (compile-exists-some policy))
-           (policy (compile-for-all policy))
-           (policy (compile-object-literal policy))
-           (policy (extract-identifiers policy))
-           (policy (lift-implicit-anonymous policy))
-           (policy (compile-constraints policy))
-           (policy (compile-funcall policy))
-           (policy (compile-reference policy))
-           (policy (compile-bool-to-prop policy)))
-      (emit-specification policy))))
+           ;; (policy (compile-for-all policy))
+           ;; (policy (compile-object-literal policy))
+           ;; (policy (extract-identifiers policy))
+           ;; (policy (lift-implicit-anonymous policy))
+           ;; (policy (compile-constraints policy))
+           ;; (policy (compile-funcall policy))
+           ;; (policy (compile-reference policy))
+           ;; (policy (compile-bool-to-prop policy))
+           (policy (compile-local-references policy))
+           )
+      (pretty-print (to-pretty-sexp policy))
+      ;; (emit-specification policy)
+      )))
diff --git a/compiler/passes/compile-exists-some.scm b/compiler/passes/compile-exists-some.scm
index e17599e..82849e3 100644
--- a/compiler/passes/compile-exists-some.scm
+++ b/compiler/passes/compile-exists-some.scm
@@ -22,6 +22,7 @@
   #: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)
@@ -52,26 +53,37 @@
                   `(,x))))
              identifiers)))
 
-(define (process-quantified-extent xs)
+(define (process-quantified-extent scope breadcrumb xs)
   (assert (list? xs))
   (if (and (positive? (length xs))
            (exists-some? (first xs)))
-      (make <lean-exists>
-        #:variables (exists-some->variables (identifiers (first xs)))
-        #:body
-        (make <lean-conjunction>
-          #:clauses (append (exists-some->constraints (identifiers (first xs)))
-                            (drop xs 1))))
+      ;; 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 form)
+(define (process-all scope breadcrumb form)
   (assert (list? form))
-  (map process-quantified-extent (partition-on form exists-some?)))
+  (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 form)
+         (process-all scope breadcrumb form)
          form))))
diff --git a/compiler/passes/compile-local-references.scm b/compiler/passes/compile-local-references.scm
new file mode 100644
index 0000000..85bf266
--- /dev/null
+++ b/compiler/passes/compile-local-references.scm
@@ -0,0 +1,42 @@
+;;; 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 (oop goops)
+  #:use-module (srfi srfi-1)
+  #:export (compile-local-references))
+
+(define (compile-local-references policy)
+  "Replace any local references with a reference to the appropriate Lean identifier"
+  (policy-map
+   policy
+   (lambda (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 local
+              (make <variable-ref> #:name (lean-name local))
+              form ; See above
+              )))
+       (_ form)))))
diff --git a/compiler/passes/lift-comprehensions.scm b/compiler/passes/lift-comprehensions.scm
index 35fdb49..30dd868 100644
--- a/compiler/passes/lift-comprehensions.scm
+++ b/compiler/passes/lift-comprehensions.scm
@@ -19,7 +19,6 @@
   #:use-module (compiler types)
   #:use-module (compiler utilities)
   #:use-module (ice-9 match)
-  #:use-module (ice-9 pretty-print) ;; Temporary
   #:use-module (oop goops)
   #:use-module (srfi srfi-11)
   #:export (compile-comprehensions))
@@ -30,37 +29,27 @@
   ;; For generating anonymous rule names.
   (define top-level-names (map inner (policy-top-level-names policy)))
 
-  (define (new-comprehension-rule comprehension)
+  (define (new-comprehension-rule breadcrumb comprehension)
     (match comprehension
-      ;; (($ <comprehension> 'array key value body)
-      ;;  (let ((identifier (fresh-identifier top-level-names "arraycomp")))
-      ;;    (make <rule>
-      ;;      #:default #f
-      ;;      #:head (make <head>
-      ;;               #:name identifier
-      ;;               #:kind 'array-memq
-      ;;               #:lhs
-      ;;               #:rhs)
-      ;;      #:body body))
-      ;;  )
-      ;; (($ <comprehension> 'set key value body)
-      ;;  ;; TODO
-      ;;  )
       (($ <constant> ($ <comprehension> 'object key value body))
-       (let ((identifier (fresh-identifier top-level-names "objectcomp")))
-         (values identifier
-                 (make <rule>
-                   #:default #f
-                   #:head (make <head>
-                            #:name identifier
-                            #:kind 'field-eqv
-                            #:lhs key
-                            #:rhs value)
-                   #:body (make <body>
-                            #:conjunction
-                            (if (not (list? body))
-                                `(,body)
-                                body))))))))
+       (let* ((name (fresh-identifier top-level-names "objectcomp"))
+              (rule (make <rule>
+                      #:default #f
+                      #:head (make <head>
+                               #:name name
+                               #:kind 'field-eqv
+                               #:lhs key
+                               #:rhs value)
+                      #:body (make <body>
+                               #:conjunction
+                               (if (not (list? body))
+                                   `(,body)
+                                   body))))
+              (local (make <local>
+                       #:identifier (make <variable-ref> #:name name)
+                       #:constraints `((== ,(canonicalize name breadcrumb) object))
+                       #:lean-name (inductive-name (head rule)))))
+         (values local rule)))))
 
   (let ((policy
          (policy-map
@@ -68,14 +57,19 @@
           (lambda (scope breadcrumb form)
             (match form
               (($ <constant> ($ <comprehension> 'object key value body))
-               (let-values (((identifier rule) (new-comprehension-rule form)))
+               (let-values (((identifier rule) (new-comprehension-rule breadcrumb form)))
+                 ;; Add the resulting rule to the policy.
                  (set! new-rules
-                   `((,(make <reference> #:parts `(,(make <variable-ref> #:name identifier)))
+                   `((,(make <reference> #:parts `(,(inner identifier)))
                       ,rule)
                      ,@new-rules))
+
+                 ;; Also add it to the scope.
+                 (add-to-scope scope breadcrumb identifier)
+                 
                  ;; Make like Indiana Jones and swap this out with a reference to the
                  ;; new lifted object.
-                 (make <reference> #:parts `(,(make <variable-ref> #:name identifier)))))
+                 (make <reference> #:parts `(,(inner identifier)))))
               (_ form))))))
     (match policy
       (($ <policy> _package _imports _scope rules _comments)
diff --git a/compiler/passes/parse-policy.scm b/compiler/passes/parse-policy.scm
index 28a7925..fca48f5 100644
--- a/compiler/passes/parse-policy.scm
+++ b/compiler/passes/parse-policy.scm
@@ -24,7 +24,7 @@
   #:use-module (srfi srfi-1)
   #:use-module (srfi srfi-2)
   #:use-module (srfi srfi-26)
-  #:use-module (ice-9 pretty-print) ;; Temporary
+  #:use-module (srfi srfi-69)
   #:export (parse-policy))
 
 (define (parse-policy ast)
@@ -33,7 +33,9 @@
   (make <policy>
     #:package (extract-package ast)
     #:imports (extract-imports ast)
-    #:rules   (extract-rules ast)))
+    #:rules   (extract-rules ast)
+    #:scope   (make <scope>
+                #:identifiers (make-hash-table))))
 
 (define (extract-package ast)
   "Return, as a string, the name of the package specified by `ast'"
diff --git a/compiler/types.scm b/compiler/types.scm
index 9a0fe2f..a563543 100644
--- a/compiler/types.scm
+++ b/compiler/types.scm
@@ -42,12 +42,20 @@
             collapse-constraints
             all-valid-identifiers
             scope-contains?
+            find-local
+
+            <local>
+            inner
+            constraints
+            lean-name
+            resolved?
 
             <rule>
             default-rule?
             head
             body
             ι-rule-body
+            inductive-name
 
             <head>
             name
@@ -56,7 +64,6 @@
             right
 
             <body>
-            inner
             ι-body-conjunction
 
             <funcall>
@@ -158,6 +165,20 @@
   (identifiers #:init-keyword #:identifiers
                #:accessor     inner))
 
+(define-class <local> ()
+  (identifier  #:init-keyword #:identifier
+               #:accessor     inner)
+  (constraints #:init-form    '()
+               #:init-keyword #:constraints
+               #:accessor     constraints)
+  ;; Name of the object as it will appear in the emitted Lean code.
+  (lean-name   #:init-keyword #:lean-name
+               #:accessor     lean-name)
+  ;; #f if this isan inductive predicate giving definition rules.
+  (resolved    #:init-form #f
+               #:init-keyword #:resolved
+               #:accessor     resolved?))
+
 (define-syntax with-anonymous-identifiers
   (lambda (stx)
     (syntax-case stx ()
@@ -172,17 +193,13 @@
          #`(let* (#,@let-clauses)
              body ...))))))
 
-(define (add-to-scope scope breadcrumb identifier constraint)
-  "Add a new IDENTIFIER with TYPE to BREADCRUMB in SCOPE"
+(define (add-to-scope scope breadcrumb local)
+  "Add a new LOCAL to BREADCRUMB in SCOPE"
   (define looking-at (hash-table-ref/default (inner scope) breadcrumb '()))
   (assert (is-a? scope <scope>))
-  (assert (is-a? identifier <variable-ref>))
+  (assert (is-a? local <local>))
   (assert (list? breadcrumb))
-  (let* ((constraints (or (assoc-ref looking-at identifier) '()))
-         (constraints (cons constraint constraints)))
-    (hash-table-set! (inner scope)
-                     breadcrumb
-                     (assoc-set! looking-at identifier constraints))))
+  (hash-table-append-item! (inner scope) breadcrumb local))
 
 (define (originating-breadcrumb scope breadcrumb identifier)
   "Return the part of the program in which IDENTIFIER was defined
@@ -236,8 +253,8 @@ can be associated with identifiers as they appear in the AST programmatically."
   (define (recur breadcrumb)
     (define looking-at (hash-table-ref/default (inner scope) breadcrumb '()))
     (if (null? breadcrumb)
-        (map car looking-at)
-        `(,@(map car looking-at) ,@(recur (drop-right breadcrumb 1)))))
+        looking-at
+        `(,@looking-at ,@(recur (drop-right breadcrumb 1)))))
   (assert (is-a? scope <scope>))
   (assert (list? breadcrumb))
   (recur breadcrumb))
@@ -248,10 +265,19 @@ can be associated with identifiers as they appear in the AST programmatically."
 `scope' is a <scope>, `breadcrumb' is a list given to the `f' of `mutate-tree',
 and `identifier' is a <reference>"
   (match identifier
+    ;; FIXME: It isn't clear to me that this is correct. There might be other
+    ;; variables within `parts' that also need to be validated. But, then,
+    ;; what's the point in using this function?
     (($ <reference> parts) (cut scope-contains? scope breadcrumb (first parts)))
-    (($ <variable-ref> _)  (member identifier (all-valid-identifiers scope breadcrumb)))
+    (($ <variable-ref> _)  (member identifier (map inner (all-valid-identifiers scope breadcrumb))))
     (_ (error "type unsupp"))))
 
+(define (find-local scope breadcrumb name)
+  ;; TODO: Document me!
+  (find (lambda (identifier)
+          (equal? name (inner identifier)))
+        (all-valid-identifiers scope breadcrumb)))
+
 
 
 ;; The intensional database of a Rego program is defined by its rules.
@@ -280,6 +306,14 @@ and `identifier' is a <reference>"
                      (tree-map body f scope breadcrumb))))
        (f scope breadcrumb inner)))))
 
+(define (inductive-name x)
+  (define suffix
+    (match (kind x)
+      ('value-eqv "_eqv")
+      ('field-eqv "_eqv")
+      ('set-memq  "_memq")))
+  (string-concatenate `(,(name x) ,suffix)))
+
 
 
 ;; A (named) relation (equality or inclusion) that holds if the body of the rule is true.
@@ -416,3 +450,4 @@ and `identifier' is a <reference>"
 
 (define-method (equal? (x <variable-ref>) (y <variable-ref>))
   (equal? (inner x) (inner y)))
+