A lot of garbage.

1 files changed, 462 insertions, 42 deletions

diff --git a/chickadee/graphics/seagull.scm b/chickadee/graphics/seagull.scm
index 291a68b..280aa10 100644
--- a/chickadee/graphics/seagull.scm
+++ b/chickadee/graphics/seagull.scm
@@ -62,8 +62,15 @@
       (char? x)
       (boolean? x)))
 
+(define (arithmetic-operator? x)
+  (memq x '(+ - * /)))
+
+(define (comparison-operator? x)
+  (memq x '(= < <= > >=)))
+
 (define (binary-operator? x)
-  (memq x '(+ - * / = < <= > >=)))
+  (or (arithmetic-operator? x)
+      (comparison-operator? x)))
 
 (define (primitive-call? x)
  (binary-operator? x))
@@ -594,8 +601,11 @@
   (string->symbol
    (format #f "T~a" (unique-type-variable-number))))
 
+(define (type-variable name)
+  `(tvar ,name))
+
 (define (fresh-type-variable)
-  `(tvar ,(unique-type-variable-name)))
+  (type-variable (unique-type-variable-name)))
 
 (define (type-variable? obj)
   (match obj
@@ -655,12 +665,67 @@
       (function-type? obj)
       (intersection-type? obj)))
 
+(define arithmetic-type
+  (list (intersection-type
+         (function-type (list int-type int-type)
+                        (list int-type))
+         (function-type (list float-type float-type)
+                        (list float-type)))))
+
+;; a, b -> c
+;; int, int -> int
+;; float, float -> float
+;; vec2, vec2 -> vec2
+;; vec3, vec3 -> vec3
+;; vec4, vec4 -> vec4
+;; mat3, mat3 -> mat3
+;; vec3, mat3 -> mat3
+;; mat3, vec3 -> mat3
+;; mat4, mat4 -> mat4
+;; vec4, mat4 -> mat4
+;; mat4, vec4 -> mat4
+
+;; (+ x (+ 1 2))
+;; e  a d  b c
+
+;; ((= a (maybe (int ((= b int) (= c int)))
+;;              (float ((= b float) (= c float)))))
+;;  (= b (maybe (int ((= a int) (= c int)))
+;;              (float ((= a float) (= c float)))))
+;;  (= c (maybe (int ((= a int) (= b int)))
+;;              (float ((= a float) (= b float))))))
+
+(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
+         (function-type (list int-type int-type)
+                        (list bool-type))
+         (function-type (list float-type float-type)
+                        (list bool-type)))))
+
+;; (define (top-level-type-env)
+;;   `(;; (+ . ,(list (function-type (list int-type int-type)
+;;     ;;                            (list int-type))))
+;;     (+ . ,arithmetic-type)
+;;     (- . ,arithmetic-type)
+;;     (* . ,arithmetic-type)
+;;     (/ . ,arithmetic-type)
+;;     (= . ,comparison-type)
+;;     (< . ,comparison-type)
+;;     (<= . ,comparison-type)
+;;     (> . ,comparison-type)
+;;     (>= . ,comparison-type)))
+
 (define (top-level-type-env)
-  `((+ . ,(list (intersection-type
-                 (function-type (list int-type int-type)
-                                (list int-type))
-                 (function-type (list float-type float-type)
-                                (list float-type)))))))
+  `((+ . (,(function-type (list int-type int-type) (list int-type))))
+    (- . (,(function-type (list int-type int-type) (list int-type))))
+    (* . (,(function-type (list int-type int-type) (list int-type))))
+    (/ . (,(function-type (list int-type int-type) (list int-type))))))
 
 (define (occurs? a b)
   (cond
@@ -674,6 +739,7 @@
    (else #f)))
 
 (define (apply-substitution-to-type type from to)
+  (pk 'apply-substitution-to-type type from to)
   (cond
    ((primitive-type? type) type)
    ((type-variable? type)
@@ -686,26 +752,54 @@
      (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))
    (else (error "invalid type" type))))
 
-(define (apply-substitutions-to-type type env)
+(define (apply-substitutions-to-type type subs)
+  (pk 'sub-type type env)
   (env-fold (lambda (from to type*)
               (apply-substitution-to-type type* from to))
             type
-            env))
+            subs))
+
+(define (apply-substitutions-to-types types subs)
+  (pk 'sub-types types subs)
+  (map (lambda (type)
+         (apply-substitutions-to-type type subs))
+       types))
 
 (define (apply-substitution-to-env from to env)
-  (env-fold (lambda (a b env*)
-              (extend-env (if (eq? a from) to a)
-                          (if (eq? b from) to b)
+  (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)))
+
 (define (substitute-type from to env)
+  (pk 'SUBSTITUTE-TYPE)
   (let* ((to* (apply-substitutions-to-type to env)))
     (and (not (occurs? from to*))
-         (let ((env* (apply-substitution-to-env from to* env)))
+         (let ((env* (pk 'new-env (apply-substitution-to-env from to* env))))
            (extend-env from to env*)))))
 
 ;; Typed expressions:
@@ -730,9 +824,37 @@
     ((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 inference: Annotation
+;;; Type annotation
 ;;;
 
 ;; Convert untyped Seagull expressions into typed expressions with
@@ -779,12 +901,14 @@
              env)))
 
 (define (generalize type env)
-  (if (function-type? type)
-      (match (difference (free-variables-in-type type)
-                         (free-variables-in-env env))
-        (() type)
-        ((quantifiers) (for-all-type quantifiers type)))
-      type))
+  (pk 'generalize type
+      (if (function-type? type)
+          (match (difference (free-variables-in-type type)
+                             (free-variables-in-env env))
+            (() type)
+            ((quantifiers ...)
+             (for-all-type quantifiers type)))
+          type)))
 
 (define (instantiate for-all)
   (define subs
@@ -792,7 +916,7 @@
             (extend-env var (fresh-type-variable) env))
           (empty-env)
           (for-all-type-quantifiers 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))
@@ -812,8 +936,6 @@
   (define env* (fold extend-env env names exp-types))
   (define body* (annotate-exp body env*))
   (texp (texp-types body*)
-        ;; (list (function-type (fresh-type-variables-for-list exps)
-        ;;                      (texp-types body*)))
         `(let ,(map list names exps*) ,body*)))
 
 (define (annotate:lambda params body env)
@@ -885,6 +1007,272 @@
 
 
 ;;;
+;;; Type inference
+;;;
+
+;; Walk the expression tree of a type annotated program and solve for
+;; the type variables present.
+
+(define (compose-substitutions a b)
+  (define b*
+    (map (match-lambda
+           ((from . to)
+            (cons from (apply-substitutions-to-type to a))))
+         b))
+  (define a*
+    (filter-map (match-lambda
+                  ((from . to)
+                   (if (assq-ref b* from)
+                       #f
+                       (cons from to))))
+                a))
+  (pk 'compose a b (append a* b*)))
+
+(define (unify:primitives a b)
+  (if (eq? a b)
+      '()
+      (error "type mismatch" a b)))
+
+(define (unify:variable a b)
+  (cond
+   ((eq? a b)
+    '())
+   ((occurs? a b)
+    (error "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
+    (((? primitive-type? a) (? primitive-type? b))
+     (unify:primitives a b))
+    ((or ((? type-variable? a) b)
+         (b (? type-variable? a)))
+     (unify:variable a b))
+    (((? function-type? a) (? function-type? b))
+     (unify:functions a b))
+    ((() ())
+     '())
+    (((a rest-a ...) (b rest-b ...))
+     (unify:lists a rest-a b rest-b))
+    (_
+     (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)
+  (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 sub1 (unify (single-type predicate) bool-type))
+  (define sub2 (compose-substitutions sub0 sub1))
+  (define sub3 (infer2 consequent))
+  (define sub4 (compose-substitutions sub2 sub3))
+  (define sub5 (infer2 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 sub0
+    (fold (lambda (exp subs)
+            (compose-substitutions (infer2 exp) subs))
+          (empty-env)
+          exps))
+  (define sub1 (infer2 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)
+  (pk 'infer:lambda type body)
+  (define type*
+    (if (for-all-type? type)fff
+        (for-all-type-ref type)
+        type))
+  (define sub0 (infer2 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)
+  (pk 'infer:primcall types operator args)
+  (define sub0
+    (fold (lambda (arg subs)
+            (compose-substitutions (infer2 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 (infer2:call types operator args)
+  (pk 'infer:call types operator args)
+  (define sub0 (infer2 operator))
+  (define sub1
+    (fold (lambda (arg subs)
+            (compose-substitutions (infer2 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 (infer2:top-level types names exps body)
+  (define sub0
+    (fold (lambda (exp subs)
+            (compose-substitutions (infer2 exp) subs))
+          (empty-env)
+          exps))
+  (compose-substitutions (infer2 body) sub0))
+
+(define (infer2 exp)
+  (match exp
+    (('t types (or (? immediate?) ('var _ _)))
+     (pk 'infer:basic exp)
+     '())
+    (('t types ('if predicate consequent alternate))
+     (infer2:if types predicate consequent alternate))
+    (('t types ('let ((names exps) ...) body))
+     (infer2:let types names exps body))
+    (('t (type) ('lambda (params ...) body))
+     (infer2:lambda type body))
+    (('t types ('primcall operator args ...))
+     (infer2:primcall types operator args))
+    (('t types ('call operator args ...))
+     (infer2:call types operator args))
+    (('t types ('top-level ((names exps) ...) body))
+     (infer2:top-level types names exps body))
+    (_ (error "unknown form" exp))))
+
+(define (infer* exp)
+  (infer2 exp))
+
+
+;;;
 ;;; Type inference: Constraints
 ;;;
 
@@ -911,16 +1299,27 @@
           (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 (new-env ((texp-types operator)
+  (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)))
+          (constrain-texp operator)
+          (append-map constrain-texp args)))
 
 (define (constrain:top-level types rhs body)
   (append (constrain-texp body)
@@ -958,20 +1357,25 @@
     (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)))))
 
@@ -995,24 +1399,44 @@
   (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))
-    ((env) env)
-    (_ (unify-fail))))
+    (()
+     (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)
@@ -1243,17 +1667,13 @@
   (parameterize ((unique-identifier-counter 0)
                  (unique-type-variable-counter 0))
     (let* ((expanded (pk 'expanded (expand exp (top-level-env))))
-           (hoisted (pk 'hoisted (hoist-functions* expanded)))
-           (texp (pk 'annotated (annotate-exp* hoisted)))
-           (constraints (pk 'constraints (constrain-texp texp)))
-           (substitutions (pk 'substitutions (unify-constraints constraints)))
-           (resolved (pk 'resolved (resolve texp substitutions))))
-      (display "*** BEGIN GLSL OUTPUT ***\n" port)
-      (emit-glsl resolved port)
-      (newline port)
-      (display "*** END GLSL OUTPUT ***\n" port)
-      ;; (list 'annotated texp
-      ;;       'constraints constraints
-      ;;       'substitutions substitutions
-      ;;       'resolved resolved)
-      )))
+           (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))))
+      ;; (display "*** BEGIN GLSL OUTPUT ***\n" port)
+      ;; (emit-glsl resolved port)
+      ;; (newline port)
+      ;; (display "*** END GLSL OUTPUT ***\n" port)
+      resolved)))