From f8b136c3bd01898e220bfdd121388392870e18d9 Mon Sep 17 00:00:00 2001
From: David Thompson <dthompson2@worcester.edu>
Date: Sun, 22 Jan 2023 18:21:39 -0500
Subject: Use continuation-passing style to get overloads working.

---
 chickadee/graphics/seagull.scm | 387 ++++++++++++++++++++++++-----------------
 1 file changed, 225 insertions(+), 162 deletions(-)

diff --git a/chickadee/graphics/seagull.scm b/chickadee/graphics/seagull.scm
index 41aacc1..d5b2cc6 100644
--- a/chickadee/graphics/seagull.scm
+++ b/chickadee/graphics/seagull.scm
@@ -73,7 +73,7 @@
       (comparison-operator? x)))
 
 (define (primitive-call? x)
- (binary-operator? x))
+  (binary-operator? x))
 
 (define (difference a b)
   (match a
@@ -646,27 +646,29 @@
   (match type
     (('for-all _ t) t)))
 
-;; Intersection types:
-(define (intersection-type . types)
-  `(^ ,types))
+;; Overload types:
+(define (overload-type . types)
+  (match types
+    (((? function-type?) ...)
+     `(overload ,types))))
 
-(define (intersection-type? obj)
+(define (overload-type? obj)
   (match obj
-    (('^ _) #t)
+    (('overload _) #t)
     (_ #f)))
 
-(define (intersection-type-ref type)
+(define (overload-type-ref type)
   (match type
-    (('^ types) types)))
+    (('overload types) types)))
 
 (define (type? obj)
   (or (primitive-type? obj)
       (type-variable? obj)
       (function-type? obj)
-      (intersection-type? obj)))
+      (overload-type? obj)))
 
-(define arithmetic-type
-  (list (intersection-type
+(define add/sub-type
+  (list (overload-type
          (function-type (list int-type int-type)
                         (list int-type))
          (function-type (list float-type float-type)
@@ -685,14 +687,8 @@
 ;; vec4, mat4 -> mat4
 ;; mat4, vec4 -> mat4
 
-(list (intersection-type
-       (function-type (list int-type int-type)
-                      (list int-type))
-       (function-type (list float-type float-type)
-                      (list float-type))))
-
 (define comparison-type
-  (list (intersection-type
+  (list (overload-type
          (function-type (list int-type int-type)
                         (list bool-type))
          (function-type (list float-type float-type)
@@ -712,8 +708,8 @@
 ;;     (>= . ,comparison-type)))
 
 (define (top-level-type-env)
-  `((+ . (,(function-type (list int-type int-type) (list int-type))))
-    (- . (,(function-type (list int-type int-type) (list int-type))))
+  `((+ . ,add/sub-type)
+    (- . ,add/sub-type)
     (* . (,(function-type (list int-type int-type) (list int-type))))
     (/ . (,(function-type (list int-type int-type) (list int-type))))))
 
@@ -742,15 +738,11 @@
      (map (lambda (return-type)
             (apply-substitution-to-type return-type from to))
           (function-type-returns type))))
-   ;; ((intersection-type? type)
-   ;;  (apply intersection-type
-   ;;   (map (lambda (t)
-   ;;          (apply-substitution-to-type t from to))
-   ;;        (intersection-type-ref type))))
-   ;; ((one-of-type? type)
-   ;;  (if (or (one-of-type? to) (condition-type? to))
-   ;;      type
-   ;;      type))
+   ((overload-type? type)
+    (apply overload-type
+           (map (lambda (type)
+                  (apply-substitution-to-type type from to))
+                (overload-type-ref type))))
    (else (error "invalid type" type))))
 
 (define (apply-substitutions-to-type type subs)
@@ -766,25 +758,6 @@
          (apply-substitutions-to-type type subs))
        types))
 
-(define (apply-substitution-to-env from to env)
-  (pk 'sub-env from to env)
-  (env-fold (lambda (name type env*)
-              (extend-env name
-                          (apply-substitution-to-type type from to)
-                          env*))
-            (empty-env)
-            env))
-
-(define (apply-substitutions-to-env subs env)
-  (env-fold (lambda (from to env*)
-              (apply-substitution-to-env from to env*))
-            env
-            subs))
-
-(define (apply-substitutions-to-texp subs exp)
-  (texp (apply-substitutions-to-types (texp-types exp) subs)
-        (texp-exp exp)))
-
 ;; Typed expressions:
 (define (texp types exp)
   `(t ,types ,exp))
@@ -984,144 +957,226 @@
                 a))
   (pk 'compose a b (append a* b*)))
 
-(define (unify:primitives a b)
-  (if (eq? a b)
-      '()
-      (error "type mismatch" a b)))
+(define unify-prompt-tag (make-prompt-tag 'unify))
+
+(define (call-with-unify-rollback thunk handler)
+  (call-with-prompt unify-prompt-tag
+    thunk
+    (lambda (k args)
+      (apply handler args))))
 
-(define (unify:variable a b)
+(define (unify:fail . args)
+  (pk 'unify:fail args)
+  (abort-to-prompt unify-prompt-tag args))
+
+(define (unify:primitives a b success)
+  (pk 'unify:primitives a b)
+  (if (equal? a b)
+      (success '())
+      (unify:fail "type mismatch" a b)))
+
+(define (unify:variable a b success)
+  (pk 'unify:variable a b)
   (cond
    ((eq? a b)
-    '())
+    (success '()))
    ((occurs? a b)
-    (error "type contains reference to itself" a b))
+    (unify:fail "type contains reference to itself" a b))
    (else
-    (list (cons a b)))))
-
-(define (unify:functions a b)
-  (define sub0 (unify (function-type-parameters a)
-                      (function-type-parameters b)))
-  (define sub1 (unify (apply-substitutions-to-types (function-type-returns a)
-                                                    sub0)
-                      (apply-substitutions-to-types (function-type-returns b)
-                                                    sub0)))
-  (compose-substitutions sub0 sub1))
-
-(define (unify:lists a rest-a b rest-b)
-  (compose-substitutions (unify a b)
-                         (unify rest-a rest-b)))
-
-(define (unify . args)
-  (pk 'unify args)
-  (match args
+    (success (list (cons a b))))))
+
+(define (unify:functions a b success)
+  (pk 'unify:functions a b)
+  (unify (function-type-parameters a)
+         (function-type-parameters b)
+         (lambda (sub0)
+           (unify (apply-substitutions-to-types (function-type-returns a)
+                                                sub0)
+                  (apply-substitutions-to-types (function-type-returns b)
+                                                sub0)
+                  (lambda (sub1)
+                    (success (compose-substitutions sub0 sub1)))))))
+
+(define (unify:overload a b success)
+  (pk 'unify:overload a b)
+  (define (try-unify functions)
+    (match functions
+      (()
+       (unify:fail "no matching overload" a b))
+      ((function . rest)
+       (pk 'try-overload function b)
+       (call-with-unify-rollback
+        (lambda ()
+          (unify function b success))
+        (lambda _
+          (try-unify rest))))))
+  (try-unify (overload-type-ref a)))
+
+(define (unify:lists a rest-a b rest-b success)
+  (pk 'unify:lists a rest-a b rest-b)
+  (unify a b
+         (lambda (sub0)
+           (unify (apply-substitutions-to-types rest-a sub0)
+                  (apply-substitutions-to-types rest-b sub0)
+                  (lambda (sub1)
+                    (success (compose-substitutions sub0 sub1)))))))
+
+(define (unify a b success)
+  (pk 'unify a b)
+  (match (list a b)
     (((? primitive-type? a) (? primitive-type? b))
-     (unify:primitives a b))
+     (unify:primitives a b success))
     ((or ((? type-variable? a) b)
          (b (? type-variable? a)))
-     (unify:variable a b))
+     (unify:variable a b success))
     (((? function-type? a) (? function-type? b))
-     (unify:functions a b))
+     (unify:functions a b success))
+    ((a (? overload-type? b))
+     (unify:overload b a success))
     ((() ())
-     '())
+     (success '()))
     (((a rest-a ...) (b rest-b ...))
-     (unify:lists a rest-a b rest-b))
+     (unify:lists a rest-a b rest-b success))
     (_
-     (error "type mismatch" args))))
-
-(define (infer:if types predicate consequent alternate)
-  (pk 'infer:if predicate consequent alternate)
-  (define sub0 (infer predicate))
-  (define sub1 (unify (single-type predicate) bool-type))
-  (define sub2 (compose-substitutions sub0 sub1))
-  (define sub3 (infer consequent))
-  (define sub4 (compose-substitutions sub2 sub3))
-  (define sub5 (infer alternate))
-  (define sub6 (compose-substitutions sub4 sub5))
-  (define sub7 (unify (apply-substitutions-to-types (texp-types consequent) sub6)
-                      (apply-substitutions-to-types (texp-types alternate) sub6)))
-  (compose-substitutions sub6 sub7))
-
-(define (infer:let types names exps body)
-  (define sub0
-    (fold (lambda (exp subs)
-            (compose-substitutions (infer exp) subs))
-          (empty-env)
-          exps))
-  (define sub1 (infer body))
-  (define sub2 (compose-substitutions sub0 sub1))
-  (define sub3 (unify (apply-substitutions-to-types types sub2)
-                      (apply-substitutions-to-types (texp-types body) sub2)))
-  (compose-substitutions sub2 sub3))
-
-(define (infer:lambda type body)
+     (unify:fail "type mismatch" a b))))
+
+(define (infer:list exps subs success)
+  (pk 'infer:list exps)
+  (match exps
+    (() (success '()))
+    ((exp . rest)
+     (infer exp
+            subs
+            (lambda (sub0)
+              (infer:list rest
+                          sub0
+                          (lambda (sub1)
+                            (success
+                             (compose-substitutions sub0 sub1)))))))))
+
+(define (infer:if types predicate consequent alternate subs success)
+  (pk 'infer:if predicate consequent alternate subs)
+  (infer predicate
+         subs
+         (lambda (sub0)
+           (unify (single-type predicate)
+                  bool-type
+                  (lambda (sub1)
+                    (define sub2 (compose-substitutions sub0 sub1))
+                    (infer consequent
+                           sub2
+                           (lambda (sub3)
+                             (infer alternate
+                                    sub3
+                                    (lambda (sub4)
+                                      (unify (apply-substitutions-to-types
+                                              (texp-types consequent)
+                                              sub4)
+                                             (apply-substitutions-to-types
+                                              (texp-types alternate)
+                                              sub4)
+                                             (lambda (sub5)
+                                               (success
+                                                (compose-substitutions
+                                                 sub4 sub5)))))))))))))
+
+(define (infer:lambda type body subs success)
   (pk 'infer:lambda type body)
   (define type*
     (if (for-all-type? type)
         (for-all-type-ref type)
         type))
-  (define sub0 (infer body))
-  (define sub1 (unify (apply-substitutions-to-types (texp-types body) sub0)
-                      (function-type-returns type*)))
-  (compose-substitutions sub0 sub1))
-
-(define (infer:primcall types operator args)
+  (infer body
+         subs
+         (lambda (sub0)
+           (unify (apply-substitutions-to-types (texp-types body) sub0)
+                  (function-type-returns type*)
+                  (lambda (sub1)
+                    (success
+                     (compose-substitutions sub0 sub1)))))))
+
+(define (infer:call types operator args subs success)
+  (pk 'infer:call types operator args subs)
+  (infer operator
+         subs
+         (lambda (sub0)
+           (infer:list
+            args
+            sub0
+            (lambda (sub1)
+              (unify (apply-substitutions-to-type
+                      (function-type (map single-type args)
+                                     types)
+                      sub1)
+                     (apply-substitutions-to-type
+                      (single-type operator)
+                      sub1)
+                     (lambda (sub2)
+                       (success (compose-substitutions sub1 sub2)))))))))
+
+(define (infer:primcall types operator args subs success)
   (pk 'infer:primcall types operator args)
-  (define sub0
-    (fold (lambda (arg subs)
-            (compose-substitutions (infer arg) subs))
-          (empty-env)
-          args))
-  (define sub1
-    (unify (apply-substitutions-to-type (function-type (map single-type args)
-                                                       types)
-                                        sub0)
-           (apply-substitutions-to-type (single-type operator)
-                                        sub0)))
-  (compose-substitutions sub0 sub1))
-
-(define (infer:call types operator args)
-  (pk 'infer:call types operator args)
-  (define sub0 (infer operator))
-  (define sub1
-    (fold (lambda (arg subs)
-            (compose-substitutions (infer arg) subs))
-          sub0
-          args))
-  (define sub2
-    (unify (apply-substitutions-to-type (function-type (map single-type args)
-                                                       types)
-                                        sub1)
-           (apply-substitutions-to-type (single-type operator)
-                                        sub1)))
-  (compose-substitutions sub1 sub2))
-
-(define (infer:top-level types names exps body)
-  (define sub0
-    (fold (lambda (exp subs)
-            (compose-substitutions (infer exp) subs))
-          (infer body)
-          exps))
-  (define sub1
-    (unify (apply-substitutions-to-types types sub0)
-           (apply-substitutions-to-types (texp-types body) sub0)))
-  (compose-substitutions (infer body) sub0))
-
-(define (infer exp)
+  (infer:list
+   args
+   subs
+   (lambda (sub0)
+     (unify (apply-substitutions-to-type
+             (function-type (map single-type args)
+                            types)
+             sub0)
+            (apply-substitutions-to-type
+             (single-type operator)
+             sub0)
+            (lambda (sub1)
+              (success
+               (compose-substitutions sub0 sub1)))))))
+
+(define (infer:let types names exps body subs success)
+  (pk 'infer:let types names exps subs)
+  (infer:list
+   exps
+   subs
+   (lambda (sub0)
+     (infer body
+            sub0
+            (lambda (sub1)
+              (unify (apply-substitutions-to-types types sub1)
+                     (apply-substitutions-to-types (texp-types body) sub1)
+                     (lambda (sub2)
+                       (success
+                        (compose-substitutions sub1 sub2)))))))))
+
+(define (infer:top-level types names exps body subs success)
+  (infer:list
+   exps
+   subs
+   (lambda (sub0)
+     (infer body
+            sub0
+            (lambda (sub1)
+              (unify (apply-substitutions-to-types types sub1)
+                     (apply-substitutions-to-types (texp-types body) sub1)
+                     (lambda (sub2)
+                       (success
+                        (compose-substitutions sub1 sub2)))))))))
+
+(define (infer exp subs success)
   (match exp
     (('t types (or (? immediate?) ('var _ _)))
-     '())
+     (pk 'infer:basic)
+     (success subs))
     (('t types ('if predicate consequent alternate))
-     (infer:if types predicate consequent alternate))
+     (infer:if types predicate consequent alternate subs success))
     (('t types ('let ((names exps) ...) body))
-     (infer:let types names exps body))
+     (infer:let types names exps body subs success))
     (('t (type) ('lambda (params ...) body))
-     (infer:lambda type body))
+     (infer:lambda type body subs success))
     (('t types ('primcall operator args ...))
-     (infer:primcall types operator args))
+     (infer:primcall types operator args subs success))
     (('t types ('call operator args ...))
-     (infer:call types operator args))
+     (infer:call types operator args subs success))
     (('t types ('top-level ((names exps) ...) body))
-     (infer:top-level types names exps body))
+     (infer:top-level types names exps body subs success))
     (_ (error "unknown form" exp))))
 
 (define (resolve:type-variable var env)
@@ -1152,8 +1207,16 @@
     (_ exp)))
 
 (define (infer-types exp)
-  (let ((annotated (pk 'annotated (annotate-exp* exp))))
-    (resolve annotated (infer annotated))))
+  (call-with-unify-rollback
+   (lambda ()
+     (let ((annotated (pk 'annotated (annotate-exp* exp))))
+       (infer annotated
+              '()
+              (lambda (subs)
+                (pk 'result-subs subs)
+                (resolve annotated subs)))))
+   (lambda args
+     (apply error args))))
 
 
 ;;;
-- 
cgit v1.2.3