diff options
| -rw-r--r-- | infer2.scm | 43 |
1 files changed, 37 insertions, 6 deletions
@@ -1,3 +1,7 @@ +;; features: +;; - multiple return values +;; - for all types +;; - intersection types (operator overloading) (use-modules (ice-9 format) (ice-9 match) (srfi srfi-1) @@ -91,20 +95,30 @@ (variables for-all-type-variables) (type for-all-type-type)) +(define-record-type <intersection-type> + (make-intersection-type types) + intersection-type? + (types intersection-type-types)) + (define (type? obj) (or (primitive-type? obj) (type-variable? obj) - (procedure-type? obj))) + (procedure-type? obj) + (intersection-type? obj))) (define (top-level-env) - '()) + `((+ . ,(make-intersection-type + (list (make-procedure-type (list int-type int-type) + (list int-type)) + (make-procedure-type (list float-type float-type) + (list float-type))))))) (define (lookup var env) (let ((type (assq-ref env var))) (cond - ((type-variable? type) type) + ((type? type) type) ((for-all-type? type) (instantiate type)) - (else (error "unbound variable" var))))) + (else (error "unbound variable:" var))))) (define (occurs-in? a b) (cond @@ -418,6 +432,11 @@ (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 'unify-fail) (abort-to-prompt %unify-prompt-tag)) @@ -474,20 +493,32 @@ (procedure-type-return-types b) dict*)) +(define-matcher (unify:intersection (? intersection-type? a) (? type? b) dict) + (let loop ((types (intersection-type-types a))) + (match types + (() (unify-fail)) + ((t . rest) + (call-with-prompt %unify-prompt-tag + (lambda () + (unify t b dict)) + (lambda (_k) + (loop rest))))))) + (define unify (compose-matchers unify:variable-left unify:variable-right unify:procedures + unify:intersection unify:lists unify:constants)) (define (unify-constraints constraints) - (call-with-prompt %unify-prompt-tag + (call-with-unify-backtrack (lambda () (unify (map constraint-lhs constraints) (map constraint-rhs constraints) '())) - (lambda (_k) #f))) + (lambda () #f))) ;;; |