diff options
| -rw-r--r-- | chickadee/graphics/seagull.scm | 504 |
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))) |