Remove a bunch of cruft.

1 files changed, 34 insertions, 353 deletions

diff --git a/chickadee/graphics/seagull.scm b/chickadee/graphics/seagull.scm
index 280aa10..4827577 100644
--- a/chickadee/graphics/seagull.scm
+++ b/chickadee/graphics/seagull.scm
@@ -764,7 +764,7 @@
    (else (error "invalid type" type))))
 
 (define (apply-substitutions-to-type type subs)
-  (pk 'sub-type type env)
+  (pk 'sub-type type subs)
   (env-fold (lambda (from to type*)
               (apply-substitution-to-type type* from to))
             type
@@ -795,13 +795,6 @@
   (texp (apply-substitutions-to-types (texp-types exp) subs)
         (texp-exp exp)))
 
-(define (substitute-type from to env)
-  (pk 'SUBSTITUTE-TYPE)
-  (let* ((to* (apply-substitutions-to-type to env)))
-    (and (not (occurs? from to*))
-         (let ((env* (pk 'new-env (apply-substitution-to-env from to* env))))
-           (extend-env from to env*)))))
-
 ;; Typed expressions:
 (define (texp types exp)
   `(t ,types ,exp))
@@ -824,34 +817,6 @@
     ((type) type)
     (_ (error "expected only 1 type" texp))))
 
-;; (define (condition-type type constraints)
-;;   `(condition ,type ,constraints))
-
-;; (define (condition-type? obj)
-;;   (match obj
-;;     (('condition _ _) #t)
-;;     (_ #f)))
-
-;; (define (condition-type-ref type)
-;;   (match type
-;;     (('condition type _) type)))
-
-;; (define (condition-type-constraints type)
-;;   (match type
-;;     (('condition _ constraints) constraints)))
-
-;; (define (one-of-type . types)
-;;   `(one-of ,types))
-
-;; (define (one-of-type? obj)
-;;   (match obj
-;;     (('one-of _) #t)
-;;     (_ #f)))
-
-;; (define (one-of-type-ref type)
-;;   (match type
-;;     (('one-of types) types)))
-
 
 ;;;
 ;;; Type annotation
@@ -916,7 +881,8 @@
             (extend-env var (fresh-type-variable) env))
           (empty-env)
           (for-all-type-quantifiers for-all)))
-  (pk 'instantiate for-all (apply-substitutions-to-type (for-all-type-ref for-all) subs)))
+  (pk 'instantiate for-all
+      (apply-substitutions-to-type (for-all-type-ref for-all) subs)))
 
 (define (fresh-type-variables-for-list lst)
   (map (lambda (_x) (fresh-type-variable)) lst))
@@ -1072,149 +1038,47 @@
     (_
      (error "type mismatch" args))))
 
-(define (infer:list exps env)
-  (pk 'infer:list exps)
-  (match exps
-    (()
-     (values '() '()))
-    ((exp . rest)
-     (define-values (exp* exp-subs)
-       (infer exp env))
-     (define-values (rest* rest-subs)
-       (infer:list rest env))
-     (values (cons exp* rest*)
-             (compose-substitutions exp-subs rest-subs)))
-    (_ (error "not a list" exps))))
-
-(define (infer:lambda params body env)
-  (pk 'infer:lambda params body)
-  (define types (fresh-type-variables-for-list params))
-  (define env* (fold extend-env env params types))
-  (define-values (body* subs) (infer body env*))
-  (define types*
-    (map (lambda (type)
-           (apply-substitutions-to-type type subs))
-         types))
-  (define lambda-type (function-type types* (texp-types body*)))
-  (values (texp (list lambda-type) `(lambda ,params ,body*))
-          subs))
-
-(define (infer:primcall operator args env)
-  (values #f #f))
-
-(define (infer:call operator args env)
-  (pk 'infer:call operator args)
-  (define-values (operator* sub0)
-    (infer operator env))
-  (define operator-type
-    (match (texp-types operator*)
-      (((? function-type? type)) type)
-      (types
-       (error "wrong type in operator position, expected function" types))))
-  (define-values (args* sub1) (infer:list args env))
-  (define sub2 (compose-substitutions sub0 sub1))
-  (define arg-types (map single-type args*))
-  (define sub3
-    (unify (function-type arg-types
-                          (fresh-type-variables-for-list
-                           (function-type-returns operator-type)))
-           operator-type))
-  (define operator-type* (apply-substitutions-to-type operator-type sub3))
-  (define sub4 (compose-substitutions sub2 sub3))
-  (define sub5 (unify (apply-substitutions-to-types
-                       (function-type-parameters operator-type*)
-                       sub4)
-                      arg-types))
-  (define sub6 (compose-substitutions sub4 sub5))
-  (define return-types
-    (apply-substitutions-to-types (function-type-returns
-                                   (single-type operator*))
-                                  sub6))
-  (values (texp return-types `(call ,operator* ,args*))
-          sub6))
-
-(define (infer:if predicate consequent alternate env)
+(define (infer:if types predicate consequent alternate)
   (pk 'infer:if predicate consequent alternate)
-  (define-values (predicate* sub0)
-    (infer predicate env))
-  (define sub1 (unify (single-type predicate*) bool-type))
-  (define sub2 (compose-substitutions sub0 sub1))
-  (define env1 (apply-substitutions-to-env sub2 env))
-  (define-values (consequent* sub3)
-    (infer consequent env1))
-  (define sub4 (compose-substitutions sub2 sub3))
-  (define env2 (apply-substitutions-to-env sub4 env1))
-  (define-values (alternate* sub5)
-    (infer alternate env2))
-  (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)))
-  (define sub8 (compose-substitutions sub6 sub7))
-  (values (texp (apply-substitutions-to-types (texp-types consequent*) sub8)
-                `(if ,predicate* ,consequent* ,alternate*))
-          sub8))
-
-(define (infer exp env)
-  (match exp
-    ((? exact-integer?)
-     (values (texp (list int-type) exp) '()))
-    ((? float?)
-     (values (texp (list float-type) exp) '()))
-    ((? boolean?)
-     (values (texp (list bool-type) exp) '()))
-    (('var var _)
-     (values (texp (list (lookup-type var env)) exp) '()))
-    (('if predicate consequent alternate)
-     (infer:if predicate consequent alternate env))
-    (('lambda (params ...) body)
-     (infer:lambda params body env))
-    (('primcall operator args ...)
-     (infer:primcall operator args env))
-    (('call operator args ...)
-     (infer:call operator args env))
-    (_ (error "unknown form" exp))))
-
-(define (infer2:if types predicate consequent alternate)
-  (pk 'infer:if predicate consequent alternate)
-  (define sub0 (infer2 predicate))
+  (define sub0 (infer predicate))
   (define sub1 (unify (single-type predicate) bool-type))
   (define sub2 (compose-substitutions sub0 sub1))
-  (define sub3 (infer2 consequent))
+  (define sub3 (infer consequent))
   (define sub4 (compose-substitutions sub2 sub3))
-  (define sub5 (infer2 alternate))
+  (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 (infer2:let types names exps body)
+(define (infer:let types names exps body)
   (define sub0
     (fold (lambda (exp subs)
-            (compose-substitutions (infer2 exp) subs))
+            (compose-substitutions (infer exp) subs))
           (empty-env)
           exps))
-  (define sub1 (infer2 body))
+  (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 (infer2:lambda type body)
+(define (infer:lambda type body)
   (pk 'infer:lambda type body)
   (define type*
-    (if (for-all-type? type)fff
+    (if (for-all-type? type)
         (for-all-type-ref type)
         type))
-  (define sub0 (infer2 body))
+  (define sub0 (infer body))
   (define sub1 (unify (apply-substitutions-to-types (texp-types body) sub0)
                       (function-type-returns type*)))
   (compose-substitutions sub0 sub1))
 
-(define (infer2:primcall types operator args)
+(define (infer:primcall types operator args)
   (pk 'infer:primcall types operator args)
   (define sub0
     (fold (lambda (arg subs)
-            (compose-substitutions (infer2 arg) subs))
+            (compose-substitutions (infer arg) subs))
           (empty-env)
           args))
   (define sub1
@@ -1225,12 +1089,12 @@
                                         sub0)))
   (compose-substitutions sub0 sub1))
 
-(define (infer2:call types operator args)
+(define (infer:call types operator args)
   (pk 'infer:call types operator args)
-  (define sub0 (infer2 operator))
+  (define sub0 (infer operator))
   (define sub1
     (fold (lambda (arg subs)
-            (compose-substitutions (infer2 arg) subs))
+            (compose-substitutions (infer arg) subs))
           sub0
           args))
   (define sub2
@@ -1241,218 +1105,33 @@
                                         sub1)))
   (compose-substitutions sub1 sub2))
 
-(define (infer2:top-level types names exps body)
+(define (infer:top-level types names exps body)
   (define sub0
     (fold (lambda (exp subs)
-            (compose-substitutions (infer2 exp) subs))
+            (compose-substitutions (infer exp) subs))
           (empty-env)
           exps))
-  (compose-substitutions (infer2 body) sub0))
+  (compose-substitutions (infer body) sub0))
 
-(define (infer2 exp)
+(define (infer exp)
   (match exp
     (('t types (or (? immediate?) ('var _ _)))
      (pk 'infer:basic exp)
      '())
     (('t types ('if predicate consequent alternate))
-     (infer2:if types predicate consequent alternate))
+     (infer:if types predicate consequent alternate))
     (('t types ('let ((names exps) ...) body))
-     (infer2:let types names exps body))
+     (infer:let types names exps body))
     (('t (type) ('lambda (params ...) body))
-     (infer2:lambda type body))
+     (infer:lambda type body))
     (('t types ('primcall operator args ...))
-     (infer2:primcall types operator args))
+     (infer:primcall types operator args))
     (('t types ('call operator args ...))
-     (infer2:call types operator args))
+     (infer:call types operator args))
     (('t types ('top-level ((names exps) ...) body))
-     (infer2:top-level types names exps body))
+     (infer:top-level types names exps body))
     (_ (error "unknown form" exp))))
 
-(define (infer* exp)
-  (infer2 exp))
-
-
-;;;
-;;; Type inference: Constraints
-;;;
-
-;; Generate type constraints for a program.
-
-(define (constrain:if types predicate consequent alternate)
-  (append (new-env ((list bool-type) (texp-types predicate))
-                   (types (texp-types consequent))
-                   (types (texp-types alternate)))
-          (constrain-texp predicate)
-          (constrain-texp consequent)
-          (constrain-texp alternate)))
-
-(define (constrain:let type rhs body)
-  (append (constrain-texp body)
-          (append-map constrain-texp rhs)))
-
-(define (constrain:lambda type body)
-  (append (new-env ((function-type-returns
-                     (if (for-all-type? type)
-                         (for-all-type-ref type)
-                         type))
-                    (texp-types body)))
-          (constrain-texp body)))
-
-(define (constrain:primitive-call types operator args)
-  (pk 'constrain:primcall types operator args)
-  (append (new-env ((texp-types operator)
-                    (list (function-type (map single-type args) types))))
-          (constrain-texp operator)
-          (append-map constrain-texp args)))
-
-(define (constrain:call types operator args)
-  (append ;; (pk 'call-return-constraints
-          ;;     (fold extend-env
-          ;;           (empty-env)
-          ;;           types
-          ;;           (function-type-returns (single-type operator))))
-          ;; (pk 'call-arg-constraints
-          ;;     (fold extend-env
-          ;;           (empty-env)
-          ;;           (map single-type args)
-          ;;           (function-type-parameters (single-type operator))))
-          (new-env ((texp-types operator)
-                    (list (function-type (map single-type args) types))))
-          (constrain-texp operator)
-          (append-map constrain-texp args)))
-
-(define (constrain:top-level types rhs body)
-  (append (constrain-texp body)
-          (append-map constrain-texp rhs)))
-
-(define (constrain-texp exp)
-  (match exp
-    (('t (types ...) ('if predicate consequent alternate))
-     (constrain:if types predicate consequent alternate))
-    (('t (type) ('let ((_ rhs) ...) body))
-     (constrain:let type rhs body))
-    (('t (type) ('lambda _ body))
-     (constrain:lambda type body))
-    (('t (types ...) ('primcall operator args ...))
-     (constrain:primitive-call types operator args))
-    (('t (types ...) ('call operator args ...))
-     (constrain:call types operator args))
-    (('t (types ...) ('top-level ((_ rhs) ...) body))
-     (constrain:top-level types rhs body))
-    (('t (_ ...) _)
-     (empty-env))))
-
-
-;;;
-;;; Type inference: Unification
-;;;
-
-;; Solve type constraints.
-
-(define %unify-prompt-tag (make-prompt-tag 'unify))
-
-(define (call-with-unify-backtrack thunk failure-handler)
-  (call-with-prompt %unify-prompt-tag
-    thunk
-    (lambda (_k) (failure-handler))))
-
-(define (unify-fail)
-  (pk 'fail)
-  (abort-to-prompt %unify-prompt-tag))
-
-(define (unify:maybe-substitute var other env)
-  (pk 'maybe-sub var other env)
-  (cond
-   ;; Tautology: matching 2 vars that are the same.
-   ((and (type-variable? other) (eq? var other))
-    (pk 'tautology var other)
-    env)
-   ;; Variable has been bound to some other value, recursively follow
-   ;; it and unify.
-   ((assq-ref env var) =>
-    (lambda (type)
-      (pk 'forward type other)
-      (unify type other env)))
-   ;; Substitute variable for value.
-   (else
-    (pk 'substitute var other)
-    (or (substitute-type var other env)
-        (unify-fail)))))
-
-(define (unify:constants a b env)
-  (if (eqv? a b) env (unify-fail)))
-
-(define (unify:lists a rest-a b rest-b env)
-  (unify rest-a rest-b (unify a b env)))
-
-(define (unify:variables a b env)
-  (unify:maybe-substitute a b env))
-
-(define (unify:functions a b env)
-  (unify (function-type-returns a)
-         (function-type-returns b)
-         (unify (function-type-parameters a)
-                (function-type-parameters b)
-                env)))
-
-(define (unify:intersection a b env)
-  (match (filter-map (lambda (t)
-                       (call-with-unify-backtrack
-                        (lambda ()
-                          (pk 'unify:try-intersect t b)
-                          (unify t b env))
-                        (lambda () #f)))
-                     (intersection-type-ref a))
-    (()
-     (pk 'intersection-fail)
-     (unify-fail))
-    ((env)
-     (pk 'intersection-success)
-     env)
-    (_
-     (pk 'loose-intersection a b)
-     ;;'undecidable
-     ;;(unify-fail)
-     ;;(pk 'env (extend-env b a env))
-     (extend-env b a env))))
-
-(define (unify . args)
-  (pk 'unify args)
-  (match args
-    (((? primitive-type? a) (? primitive-type? b) env)
-     (pk 'unify:primitives a b)
-     (if (eq? a b) env (unify-fail)))
-    ((or ((? type-variable? a) b env)
-         (b (? type-variable? a) env))
-     (pk 'unify:var a b)
-     (unify:variables a b env))
-    (((? function-type? a) (? function-type? b) env)
-     (pk 'unify:functions a b)
-     (unify:functions a b env))
-    (((? intersection-type? a) b env)
-     (pk 'unify:intersection a b)
-     (unify:intersection a b env))
-    (((a . rest-a) (b . rest-b) env)
-     (pk 'unify:lists a rest-a b rest-b)
-     (unify:lists a rest-a b rest-b env))
-    ((a b env)
-     (pk 'unify:constants a b)
-     (unify:constants a b env))))
-
-(define (unify-constraints env)
-  (call-with-unify-backtrack
-   (lambda ()
-     (unify (env-names env) (env-values env) '()))
-   (lambda () #f)))
-
-
-;;;
-;;; Type inference: Resolution
-;;;
-
-;; Replace the variables in the original typed expression to form a
-;; fully typed expression that is ready for emission to GLSL.
-
 (define (resolve:type-variable var env)
   (let ((type (assq-ref env var)))
     (if type
@@ -1480,6 +1159,10 @@
      (resolve:list exps env))
     (_ exp)))
 
+(define (infer-types exp)
+  (let ((annotated (pk 'annotated (annotate-exp* exp))))
+    (resolve annotated (infer annotated))))
+
 
 ;;;
 ;;; GLSL emission
@@ -1669,11 +1352,9 @@
     (let* ((expanded (pk 'expanded (expand exp (top-level-env))))
            (propagated (pk 'propagated (propagate-constants expanded (empty-env))))
            (hoisted (pk 'hoisted (hoist-functions* propagated)))
-           (annotated (pk 'annotated (annotate-exp* hoisted)))
-           (substitutions (pk 'subs (infer2 annotated)))
-           (resolved (pk 'resolved (resolve annotated substitutions))))
+           (inferred (pk 'inferred (infer-types hoisted))))
       ;; (display "*** BEGIN GLSL OUTPUT ***\n" port)
       ;; (emit-glsl resolved port)
       ;; (newline port)
       ;; (display "*** END GLSL OUTPUT ***\n" port)
-      resolved)))
+      inferred)))