Compilation of locals

4 files changed, 86 insertions, 25 deletions

diff --git a/compiler/lean.scm b/compiler/lean.scm
index 622d215..c2d2728 100644
--- a/compiler/lean.scm
+++ b/compiler/lean.scm
@@ -28,7 +28,7 @@
             <lean-conjunction>
             <lean-compare>
             <lean-funcall>
-            <lean-intro-local>
+            <lean-intro-locals>
             <lean-assignment-chain>
             <lean-option>
             <lean-tuple>
@@ -114,9 +114,11 @@
                      (tree-map args f scope breadcrumb))))
        (f scope breadcrumb inner)))))
 
-(define-class <lean-intro-local> (<lean-expression>)
-  (identifier #:init-keyword #:identifier)
-  (value      #:init-keyword #:value))
+(define-class <lean-intro-locals> (<lean-expression>)
+  (identifiers #:init-keyword #:identifiers ; (name value) pairs
+               #:getter       identifiers)
+  (body        #:init-keyword #:body
+               #:accessor     inner))
 
 (define-class <lean-assignment-chain> (<lean-expression>))
 
@@ -199,6 +201,18 @@
      " "
      ,(string-join (map (compose wrap compile) (args x)) " "))))
 
+(define-method (compile (x <lean-intro-locals>))
+  (string-concatenate
+   `("("
+     ,(string-join
+       (map (match-lambda
+              ((name value) (format #f "let ~a := ~a" (compile name) (compile value))))
+            (identifiers x))
+       "; ")
+     "; "
+     ,(compile (inner x))
+     ")")))
+
 (define-method (compile (x <lean-conjunction>))
   (string-join (map (compose wrap compile) (clauses x)) " ∧ "))
 
diff --git a/compiler/passes/compile-constraints.scm b/compiler/passes/compile-constraints.scm
index 82efbd1..b57e9af 100644
--- a/compiler/passes/compile-constraints.scm
+++ b/compiler/passes/compile-constraints.scm
@@ -15,6 +15,7 @@
 ;;; <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)
@@ -45,18 +46,60 @@
 ;; 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
+    ((whole *** ((singleton-form) next ...))
+     (if (is-local-assignment? singleton-form)
+         (cons (cons singleton-form (first next))
+               (drop next 1))
+         whole))
+    (anything-else anything-else)))
+
+(define (process-local-extent 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)
+                  `(,left ,right)))
+               assignments)
+          #:body
+          (make <lean-conjunction> #:clauses body)))
+      xs))
+
+(define (process-all form)
+  (map process-local-extent
+       (collapse-extents (partition-on form is-local-assignment?))))
+
 (define (compile-constraints policy)
   (policy-map
    policy
    (lambda (scope breadcrumb form)
      (match form
-       ((($ <reference> (($ <variable-ref> "assign"))) left right)
-        (display (make <lean-compare>
-          #:kind 'eq
-          #:left left
-          #:right right))
-        (make <lean-compare>
-          #:kind 'eq
-          #:left left
-          #:right right))
+       ((($ <reference> (($ <variable-ref> name))) left right)
+        (if (string= name "assign")
+            form
+            (make <lean-compare>
+              #:kind (match name
+                       ("equal"  'eq)
+                       ("eq"     'eq)
+                       ("gt"     'gt)
+                       ("gte"    'ge)
+                       ("lt"     'lt)
+                       ("lte"    'le))
+              #:left left
+              #:right right)))
+       ((xs ...)
+        (if (any is-local-assignment? form)
+            (process-all form)
+            form))
        (anything-else anything-else)))))
diff --git a/compiler/passes/compile-exists-some.scm b/compiler/passes/compile-exists-some.scm
index 56714b9..957ecab 100644
--- a/compiler/passes/compile-exists-some.scm
+++ b/compiler/passes/compile-exists-some.scm
@@ -19,6 +19,7 @@
   #:use-module (compiler lean)
   #:use-module (compiler types)
   #:use-module (compiler walk)
+  #:use-module (compiler utilities)
   #:use-module (ice-9 match)
   #:use-module (oop goops)
   #:use-module (srfi srfi-1)
@@ -27,16 +28,6 @@
 (define (exists-some? form)
   (is-a? form <exists-some>))
 
-(define (partition-on-quantification xs)
-  (define (recur result running cur)
-    (cond ((null? cur)
-           (cons (reverse! running) result))
-          ((exists-some? (first cur))
-           (recur (cons (reverse! running) result) (list (first cur)) (cdr cur)))
-          (else
-           (recur result (cons (car cur) running) (cdr cur)))))
-  (filter (negate null?) (recur '() '() xs)))
-
 (define (exists-some->variables identifiers)
   (map (lambda (x)
          (cond ((is-a? x <variable-ref>) x)
@@ -67,7 +58,7 @@
 
 (define (process-all form)
   (assert (list? form))
-  (map process-quantified-extent (partition-on-quantification form)))
+  (map process-quantified-extent (partition-on form exists-some?)))
 
 (define (compile-exists-some policy)
   (policy-map
diff --git a/compiler/utilities.scm b/compiler/utilities.scm
index 598d014..c9ad3e9 100644
--- a/compiler/utilities.scm
+++ b/compiler/utilities.scm
@@ -36,7 +36,9 @@
             map-slot
             with-modified-slot
             derive-display
-            to-pretty-sexp))
+            to-pretty-sexp
+
+            partition-on))
 
 (define (alist? xs)
   "Return #t when XS is an alist"
@@ -136,3 +138,14 @@
                   (class-slots (class-of form)))))
         ((list? form) (map to-pretty-sexp form))
         (else form)))
+
+
+(define (partition-on xs pred)
+  (define (recur result running cur)
+    (cond ((null? cur)
+           (cons (reverse! running) result))
+          ((pred (first cur))
+           (recur (cons (reverse! running) result) (list (first cur)) (cdr cur)))
+          (else
+           (recur result (cons (car cur) running) (cdr cur)))))
+  (reverse! (filter (negate null?) (recur '() '() xs))))