From d26ad0e2137068f9e3ea01e27edf99cc1cee61e8 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Wed, 2 Jun 2010 12:47:43 -0400 Subject: [PATCH] Change inference to take into account index vs regular vars. original commit: 99e499a503b8b319bc0e512b698e5543634e3654 --- collects/typed-scheme/infer/infer-unit.rkt | 23 +++++-------- collects/typed-scheme/infer/signatures.rkt | 38 +++++++++++++++++++--- collects/typed-scheme/typecheck/tc-app.rkt | 4 +-- collects/typed-scheme/types/utils.rkt | 5 +-- 4 files changed, 47 insertions(+), 23 deletions(-) diff --git a/collects/typed-scheme/infer/infer-unit.rkt b/collects/typed-scheme/infer/infer-unit.rkt index 92c35874..ad372fa7 100644 --- a/collects/typed-scheme/infer/infer-unit.rkt +++ b/collects/typed-scheme/infer/infer-unit.rkt @@ -3,12 +3,11 @@ (require scheme/require (except-in (path-up - "utils/utils.rkt" "utils/tc-utils.rkt" + "utils/utils.rkt" "utils/tc-utils.rkt" "types/utils.rkt" "rep/free-variance.rkt" "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/rep-utils.rkt" "types/convenience.rkt" "types/union.rkt" "types/subtype.rkt" "types/remove-intersect.rkt" "types/resolve.rkt" "env/type-name-env.rkt" "env/index-env.rkt" "env/tvar-env.rkt") make-env) - (path-up "types/utils.rkt") "constraint-structs.rkt" "signatures.rkt" scheme/match @@ -499,26 +498,28 @@ (cset-meet* (for/list ([s S] [t T]) (cgen V X s t)))) ;; X : variables to infer +;; Y : indices to infer ;; S : actual argument types ;; T : formal argument types ;; R : result type ;; must-vars : variables that must be in the substitution +;; must-idxs : index variables that must be in the substitution ;; expected : boolean ;; returns a substitution ;; if R is #f, we don't care about the substituion ;; just return a boolean result -(define (infer X S T R must-vars [expected #f]) +(define (infer X Y S T R must-vars must-idxs [expected #f]) (with-handlers ([exn:infer? (lambda _ #f)]) - (let ([cs (cgen/list null X S T)]) + (let ([cs (cgen/list null X Y S T)]) (if (not expected) - (subst-gen cs R must-vars) - (subst-gen (cset-meet cs (cgen null X R expected)) R must-vars))))) + (subst-gen cs R (append must-vars must-idxs)) + (subst-gen (cset-meet cs (cgen null X Y R expected)) R must-vars))))) ;; like infer, but T-var is the vararg type: -(define (infer/vararg X S T T-var R must-vars [expected #f]) +(define (infer/vararg X Y S T T-var R must-vars must-idxs [expected #f]) (define new-T (if T-var (extend S T T-var) T)) (and ((length S) . >= . (length T)) - (infer X S new-T R must-vars expected))) + (infer X Y S new-T R must-vars must-idxs expected))) ;; like infer, but dotted-var is the bound on the ... ;; and T-dotted is the repeated type @@ -538,10 +539,4 @@ (subst-gen cs R must-vars) (subst-gen (cset-meet cs (cgen null X R expected)) R must-vars))))) -(define (infer/simple S T R) - (infer (fv/list T) S T R)) - -(define (i s t r) - (infer/simple (list s) (list t) r)) - ;(trace cgen) diff --git a/collects/typed-scheme/infer/signatures.rkt b/collects/typed-scheme/infer/signatures.rkt index 4dcf72ab..f9b80aa5 100644 --- a/collects/typed-scheme/infer/signatures.rkt +++ b/collects/typed-scheme/infer/signatures.rkt @@ -1,6 +1,7 @@ -#lang scheme/base -(require scheme/unit scheme/contract "constraint-structs.rkt" "../utils/utils.rkt") -(require (rep type-rep) (utils unit-utils)) +#lang racket/base +(require racket/unit racket/contract racket/require + "constraint-structs.rkt" + (path-up "utils/utils.rkt" "utils/unit-utils.rkt" "rep/type-rep.rkt")) (provide (all-defined-out)) (define-signature dmap^ @@ -29,13 +30,40 @@ ([cnt restrict (Type? Type? . -> . Type?)])) (define-signature infer^ - ([cnt infer (((listof symbol?) (listof Type?) (listof Type?) Type? (listof symbol?)) ((or/c #f Type?)) . ->* . any)] - [cnt infer/vararg (((listof symbol?) + ([cnt infer ((;; variables from the forall + (listof symbol?) + ;; indexes from the forall + (listof symbol?) + ;; actual argument types from call site + (listof Type?) + ;; domain + (listof Type?) + ;; range + Type? + ;; free variables + (listof symbol?) + ;; free indexes + (listof symbol?)) + ;; optional expected type + ((or/c #f Type?)) + . ->* . any)] + [cnt infer/vararg ((;; variables from the forall + (listof symbol?) + ;; indexes from the forall + (listof symbol?) + ;; actual argument types from call site (listof Type?) + ;; domain (listof Type?) + ;; rest (or/c #f Type?) + ;; range Type? + ;; free variables + (listof symbol?) + ;; free indexes (listof symbol?)) + ;; [optional] expected type ((or/c #f Type?)) . ->* . any)] [cnt infer/dots (((listof symbol?) symbol? diff --git a/collects/typed-scheme/typecheck/tc-app.rkt b/collects/typed-scheme/typecheck/tc-app.rkt index e34275b9..87fa124a 100644 --- a/collects/typed-scheme/typecheck/tc-app.rkt +++ b/collects/typed-scheme/typecheck/tc-app.rkt @@ -824,11 +824,11 @@ [else (= (length dom) (length argtys))])) ;; only try to infer the free vars of the rng (which includes the vars in filters/objects) ;; note that we have to use argtys-t here, since argtys is a list of tc-results - (lambda (dom rng rest drest a) + (lambda (dom rng rest drest a) (if drest (infer/dots fixed-vars dotted-var argtys-t dom (car drest) rng (fv rng) #:expected (and expected (tc-results->values expected))) - (infer/vararg vars argtys-t dom rest rng (fv rng) + (infer/vararg fixed-vars (list dotted-var) argtys-t dom rest rng (fv rng) (fi rng) (and expected (tc-results->values expected))))) t argtys expected)] ;; regular polymorphic functions without dotted rest, and without mandatory keyword args diff --git a/collects/typed-scheme/types/utils.rkt b/collects/typed-scheme/types/utils.rkt index f38b77d7..177754a0 100644 --- a/collects/typed-scheme/types/utils.rkt +++ b/collects/typed-scheme/types/utils.rkt @@ -12,7 +12,7 @@ scheme/contract (for-syntax scheme/base syntax/parse)) -(provide fv fv/list +(provide fv fv/list fi substitute substitute-dots substitute-dotted @@ -68,7 +68,7 @@ ;; implements angle bracket substitution from the formalism ;; substitute-dots : Listof[Type] Option[type] Name Type -> Type (d/c (substitute-dots images rimage name target) - ((listof Type/c) (or/c #f (cons/c Type/c symbol?)) symbol? Type? . -> . Type?) + ((listof Type/c) (or/c #f Type/c) symbol? Type? . -> . Type?) (define (sb t) (substitute-dots images rimage name t)) (if (or (hash-ref (free-idxs* target) name #f) (hash-ref (free-vars* target) name #f)) (type-case (#:Type sb #:Filter (sub-f sb)) target @@ -293,6 +293,7 @@ ;; fv : Type -> Listof[Name] (define (fv t) (hash-map (free-vars* t) (lambda (k v) k))) +(define (fi t) (for/list ([(k v) (in-hash (free-idxs* t))]) k)) ;; fv/list : Listof[Type] -> Listof[Name] (define (fv/list ts) (hash-map (combine-frees (map free-vars* ts)) (lambda (k v) k)))