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