From 8e2b73c2d57f753cc6e56b4d7d1cb76abbe78359 Mon Sep 17 00:00:00 2001
From: David Thompson <dthompson2@worcester.edu>
Date: Sat, 4 Feb 2023 15:04:56 -0500
Subject: Improve predicate composition and evaluation.

---
 chickadee/graphics/seagull.scm | 360 +++++++++++++++++++++++++++++------------
 1 file changed, 260 insertions(+), 100 deletions(-)

diff --git a/chickadee/graphics/seagull.scm b/chickadee/graphics/seagull.scm
index 05003d9..4cb1a21 100644
--- a/chickadee/graphics/seagull.scm
+++ b/chickadee/graphics/seagull.scm
@@ -981,6 +981,10 @@
      `(or ,@(map (lambda (pred)
                     (apply-substitution-to-predicate pred from to))
                  preds)))
+    (('list preds ...)
+     `(list ,@(map (lambda (pred)
+                     (apply-substitution-to-predicate pred from to))
+                   preds)))
     (('when test consequent)
      `(when ,(apply-substitution-to-predicate test from to)
         ,(apply-substitution-to-predicate consequent from to)))
@@ -1234,6 +1238,249 @@
         (instantiate type)
         type)))
 
+(define (predicate:and . preds)
+  ;; Combine inner 'and' predicates and remove #t predicates.
+  (define preds*
+    (let loop ((preds preds))
+      (match preds
+        (() '())
+        ((('and sub-preds ...) . rest)
+         (append sub-preds (loop rest)))
+        ((#t . rest)
+         (loop rest))
+        ((pred . rest)
+         (cons pred (loop rest))))))
+  (match preds*
+    (() #t)
+    ((pred) pred)
+    (_ `(and ,@preds*))))
+
+(define (predicate:or . preds)
+  (match preds
+    (() #f)
+    ((pred) pred)
+    ((pred ('or sub-preds ...))
+     `(or ,pred ,@sub-preds))
+    (_ `(or ,@preds))))
+
+(define (predicate:list . preds)
+  (define preds*
+    (let loop ((preds preds))
+      (match preds
+        (() '())
+        ((('list sub-preds ...) . rest)
+         (append sub-preds (loop rest)))
+        ((pred . rest)
+         (cons pred (loop rest))))))
+  `(list ,@preds*))
+
+(define (predicate:substitute from to)
+  `(substitute ,from ,to))
+
+(define (predicate:substitutes subs)
+  (apply predicate:and
+         (map (match-lambda
+                ((from . to)
+                 (predicate:substitute from to)))
+              subs)))
+
+(define (compose-predicates a b)
+  (cond
+   ((and (eq? a #t) (eq? b #t))
+    #t)
+   ((eq? a #t)
+    b)
+   ((eq? b #t)
+    a)
+   (else
+    (predicate:list a b))))
+
+(define (compose-predicates* preds)
+  (reduce (lambda (pred memo)
+            (compose-predicates pred memo))
+          #t
+          preds))
+
+(define (compose-predicates-for-types types)
+  (compose-predicates* (map predicate-for-type types)))
+
+;; Produces a simplified predicate and a new set of substitutions for
+;; predicates that have been satisfied and simplified to #t.  It's a
+;; bit of a weird process since we're dealing with partial evaluation,
+;; simplification, and constraint generation at the same time, so
+;; there are lots of comments explaining what the heck is going on.
+(define (eval-predicate pred)
+  (match pred
+    ;; #t is the simplest predicate.  It's always successful and
+    ;; results in no substitutions.
+    (#t (values #t '()))
+    (#f (values #f '()))
+    ;; '=' asserts that 'a' must equal 'b'.  If either is a type
+    ;; variable, then we don't have enough information to determine
+    ;; success or failure.
+    ((or ('= (? type-variable?) _)
+         ('= _ (? type-variable?)))
+     (values pred '()))
+    ;; Neither argument is a type variable, so we can get an answer.
+    (('= a b)
+     (values (equal? a b) '()))
+    ;; An 'or' succeeds if any of the predicates within succeed.
+    (('or preds ...)
+     (match preds
+       ;; No clause succeeded or the 'or' had no clauses to begin
+       ;; with.  Either way, the 'or' fails.
+       (() (values #f '()))
+       ((pred* . rest)
+        (define-values (new-pred subs)
+          (eval-predicate pred*))
+        (match new-pred
+          ;; This clause succeeded, so the entire 'or' can be
+          ;; reduced to #t.
+          (#t (values #t subs))
+          ;; This clause failed, so simplify the 'or' to just the
+          ;; rest of the clauses.
+          (#f (eval-predicate (apply predicate:or rest)))
+          ;; There isn't enough information to determine if this
+          ;; clause will succeed or fail.  So, we evaluate the rest
+          ;; of the 'or' clauses and compose the result with this
+          ;; undetermined clause.
+          (_
+           (define-values (rest-pred subs*)
+             (eval-predicate (apply predicate:or rest)))
+           (match rest-pred
+             ;; All of the other 'or' clauses have failed, so the
+             ;; 'or' can be removed entirely and reduced to the
+             ;; undetermined predicate.
+             (#f (values new-pred '()))
+             ;; The rest of the 'or' succeeded, so we can form a
+             ;; series of 'substitute' forms so that if this
+             ;; undetermined clause fails the substitutions from the
+             ;; rest of 'or' will still be respected.
+             (#t
+              (values (predicate:or new-pred (predicate:substitutes subs*))
+                      '()))
+             ;; The rest of the 'or' clauses have an undetermined
+             ;; answer, so the result is an 'or'.
+             (_
+              (values (predicate:or new-pred rest-pred) '()))))))))
+    ;; An 'and' succeeds if *all* of the predicates within succeed.
+    (('and preds ...)
+     (match preds
+       ;; All of the 'and' clauses succeed, so the 'and' succeeds.
+       (()
+        (values #t '()))
+       ((pred* . rest)
+        (define-values (new-pred subs)
+          (eval-predicate pred*))
+        (match new-pred
+          ;; The first 'and' clause is successful, so test the rest of
+          ;; the clauses and compose the substitutes.
+          (#t
+           (let ()
+             (define-values (rest-pred subs*)
+               (eval-predicate (apply predicate:and rest)))
+             (match rest-pred
+               ;; The rest of the 'and' clauses are successful, so the
+               ;; entire 'and' is successful and we can return the
+               ;; substitutions.
+               (#t
+                (values #t (compose-substitutions subs subs*)))
+               ;; At least one of the remaining clauses has failed, so
+               ;; the 'and' fails.
+               (#f
+                (values #f '()))
+               ;; The rest of the 'and' is undetermined, so form a new
+               ;; and that will perform the substitutions generated by
+               ;; this clause if the rest of the 'and' eventually
+               ;; succeeds.
+               (_
+                (values (predicate:and rest-pred (predicate:substitutes subs))
+                        '())
+                ;; (values (predicate:and rest-pred)
+                ;;         subs*)
+                ))))
+          ;; The clause failed, so the 'and' fails.
+          (#f (values #f '()))
+          ;; The clause is undetermined, so evaluate the rest of the
+          ;; clauses and attempt to simply the resulting 'and'
+          ;; expression.
+          (_
+           (define-values (rest-pred subs*)
+             (eval-predicate (apply predicate:and rest)))
+           (match rest-pred
+             ;; One of the remaining clauses fails, so even if the
+             ;; undetermined clause were to succeed later, the 'and'
+             ;; is going to fail so just fail now.
+             (#f (values #f '()))
+             ;; The remaining clauses pass, so we replace them with
+             ;; substitutions that will occur should this
+             ;; undertermined clause eventually succeed.
+             (#t
+              (values (predicate:and new-pred (predicate:substitutes subs*))
+                      '()))
+             ;; The remaining clauses have an undetermined result, so
+             ;; construct a new 'and'.
+             (_
+              (values (predicate:and new-pred rest-pred) '()))))))))
+    ;; A 'list' predicate is like an 'or' except if any clause
+    ;; succeeds the substitutions are propagated to the caller along
+    ;; with a new list withou the successful clause.  This is how
+    ;; multiple independent predicates are composed.
+    (('list preds ...)
+     (match preds
+       ;; No predicates, no failure.
+       (() (values #t '()))
+       ((pred* . rest)
+        (define-values (new-pred subs)
+          (eval-predicate pred*))
+        (match new-pred
+          ;; This clause succeeded, so remove it from the result, eval
+          ;; the rest of the clauses, and pass along the substitutions.
+          (#t
+           (let ()
+             (define-values (rest-pred subs*)
+               (eval-predicate (apply predicate:list rest)))
+             (values rest-pred (compose-substitutions subs subs*))))
+          ;; This clause failed, so the whole predicate fails.
+          (#f (values #f '()))
+          ;; There isn't enough information to determine if this
+          ;; clause will succeed or fail.  So, we evaluate the rest of
+          ;; the clauses and compose the result with this undetermined
+          ;; clause.
+          (_
+           (define-values (rest-pred subs*)
+             (eval-predicate (apply predicate:list rest)))
+           (values (predicate:list pred* rest-pred) subs*))))))
+    (('when test consequent)
+     (define-values (new-test subs)
+       (eval-predicate test))
+     (match new-test
+       (#t
+        (let ()
+          (define-values (new-consequent subs*)
+            (eval-predicate consequent))
+          (values new-consequent (compose-substitutions subs subs*))))
+       (#f (values #f '()))
+       (_ (values `(when ,new-test ,consequent) '()))))
+    ;; Substitution always succeeds and returns a substitution to be
+    ;; carried forward in the inference process.
+    (('substitute a b)
+     (values #t (list (cons a b))))))
+
+(define (eval-predicate* pred subs)
+  (define-values (new-pred pred-subs)
+    (eval-predicate
+     (apply-substitutions-to-predicate pred subs)))
+  ;; TODO: Get information about *why* the predicate failed.
+  (unless new-pred
+    (error "predicate failure"))
+  ;; Recursively evaluate the predicate, applying the substitutions
+  ;; generated by the last evaluation, until it cannot be simplified
+  ;; any further.
+  (if (null? pred-subs)
+      (values new-pred subs)
+      (eval-predicate* new-pred (compose-substitutions subs pred-subs))))
+
 (define* (free-variables-in-type type)
   (cond
    ((primitive-type? type) '())
@@ -1290,6 +1537,10 @@
      (append-map (lambda (pred)
                    (free-variables-in-predicate pred))
                  preds))
+    (('list preds ...)
+     (append-map (lambda (pred)
+                   (free-variables-in-predicate pred))
+                 preds))
     (('when test consequent)
      (append (free-variables-in-predicate test)
              (free-variables-in-predicate consequent)))
@@ -1332,98 +1583,6 @@
   (values (map first types+preds)
           (reduce compose-predicates #t (map second types+preds))))
 
-;; (define (strip-qualifier type)
-;;   (if (qualified-type? type)
-;;       (qualified-type-ref type)
-;;       type))
-
-;; (define (strip-qualifiers types)
-;;   (map strip-qualifier types))
-
-;; (define (predicate-for-type type)
-;;   (if (qualified-type? type)
-;;       (qualified-type-predicate type)
-;;       #t))
-
-(define (compose-predicates a b)
-  (cond
-   ((and (eq? a #t) (eq? b #t))
-    #t)
-   ((eq? a #t)
-    b)
-   ((eq? b #t)
-    a)
-   (else
-    `(and ,a ,b))))
-
-(define (compose-predicates* preds)
-  (reduce (lambda (pred memo)
-            (compose-predicates pred memo))
-          #t
-          preds))
-
-(define (compose-predicates-for-types types)
-  (compose-predicates* (map predicate-for-type types)))
-
-;; Produces a simplified predicate and a new set of substitutions for
-;; predicates that have been satisfied and simplified to #t.
-(define (eval-predicate pred)
-  (match pred
-    (#t (values #t '()))
-    ((or ('= (? type-variable?) _)
-         ('= _ (? type-variable?)))
-     (values pred '()))
-    (('= a b)
-     (values (equal? a b) '()))
-    (('or preds ...)
-     (let loop ((preds preds))
-       (match preds
-         (() (values #f '()))
-         ((pred* . rest)
-          (define-values (new-pred subs)
-            (eval-predicate pred*))
-          (match new-pred
-            (#t (values #t subs))
-            (#f (eval-predicate `(or ,@rest)))
-            (_ (values `(or ,new-pred ,@rest) '())))))))
-    (('and preds ...)
-     (let loop ((preds preds))
-       (match preds
-         (() (values #t '()))
-         ((pred* . rest)
-          (define-values (new-pred subs)
-            (eval-predicate pred*))
-          (match new-pred
-            (#t
-             (let ()
-               (define-values (new-pred* subs*)
-                 (eval-predicate `(and ,@rest)))
-               (values new-pred* (compose-substitutions subs subs*))))
-            (#f (values #f '()))
-            (_ (values `(and ,new-pred ,@rest) '())))))))
-    (('when test consequent)
-     (define-values (new-test subs)
-       (eval-predicate test))
-     (match new-test
-       (#t
-        (let ()
-          (define-values (new-consequent subs*)
-            (eval-predicate consequent))
-          (values new-consequent (compose-substitutions subs subs*))))
-       (#f (values #f '()))
-       (_ (values `(when ,new-test ,consequent) '()))))
-    (('substitute a b)
-     (values #t (list (cons a b))))))
-
-(define (eval-predicate* pred subs)
-  (define-values (new-pred pred-subs)
-    (eval-predicate
-     (apply-substitutions-to-predicate pred subs)))
-  ;; TODO: Get information about *why* the predicate failed.
-  (unless new-pred
-    (error "predicate failure"))
-  (values new-pred (compose-substitutions subs pred-subs)))
-
 (define (unify:primitives a b)
   (if (equal? a b)
       '()
@@ -1774,14 +1933,15 @@
                (c (fresh-type-variable)))
            (for-all-type
             (list a b c)
-            (function-type (list a b)
-                           (list c))
-            `(or (when (and (= ,a ,int-type)
-                            (= ,b ,int-type))
-                   (substitute ,c ,a))
-                 (when (and (= ,a ,float-type)
-                            (= ,b ,float-type))
-                   (substitute ,c ,a))))))
+            (function-type (list a b) (list c))
+            `(or (and (= ,a ,int-type)
+                      (= ,b ,int-type)
+                      (substitute ,c ,a))
+
+                 (and (= ,a ,float-type)
+                      (= ,b ,float-type)
+                      (substitute ,c ,a))
+                 ))))
    (empty-env)))
 
 ;; TODO: Add some kind of context object that is threaded through the
-- 
cgit v1.2.3