More environment refactoring.

- rationalize naming of files
- split files by env constructed

collects/tests/typed-scheme/unit-tests/parse-type-tests.rkt

@@ -1,7 +1,7 @@
 #lang scheme/base
 (require "test-utils.ss" (for-syntax scheme/base)
          (utils tc-utils)
-	 (env type-alias-env type-environments type-name-env init-envs)
+	 (env type-alias-env type-env-structs tvar-env type-name-env init-envs)
 	 (rep type-rep)
 	 (rename-in (types comparison subtype union utils convenience)
                     [Un t:Un] [-> t:->])

collects/tests/typed-scheme/unit-tests/subtype-tests.rkt

@@ -3,7 +3,7 @@
 (require "test-utils.ss"
          (types subtype convenience union)
 	 (rep type-rep)
-	 (env init-envs type-environments)
+	 (env init-envs type-env-structs)
 	 (r:infer infer infer-dummy)
          rackunit
          (for-syntax scheme/base))

collects/tests/typed-scheme/unit-tests/type-annotation-test.rkt

@@ -4,7 +4,7 @@
          typed-scheme/private/type-annotation
          typed-scheme/private/parse-type
          (types abbrev utils)
-	 (env type-environments  init-envs)
+	 (env type-env-structs init-envs)
 	 (utils tc-utils)
 	 (rep type-rep filter-rep object-rep)
          rackunit)

collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt

@@ -17,12 +17,12 @@
                     [-> t:->])
          (utils tc-utils utils)
          unstable/mutated-vars
-         (env type-name-env type-environments init-envs)
+         (env type-name-env type-env-structs init-envs)
          rackunit rackunit/text-ui
          syntax/parse
          (for-syntax (utils tc-utils)
                      (typecheck typechecker)
-	             (env type-env)
+	             (env global-env)
 	             (private base-env base-env-numeric
 			      base-env-indexing))
          (for-template (private base-env base-types base-types-extra

collects/typed-scheme/env/dotted-env.rkt

@@ -0,0 +1,16 @@
+#lang racket/base
+
+(require "type-env-structs.rkt" syntax/id-table)
+(provide (all-defined-out))
+
+;; this environment maps lexical identifiers to pairs of types and bounds
+;; bounds are type variables which must be bound with ...
+;; bounds are represented as symbols
+
+;; the environment for types of ... variables
+(define dotted-env (make-parameter (make-empty-env (make-immutable-free-id-table))))
+
+;; run code in an extended dotted env
+(define-syntax with-dotted-env/extend
+  (syntax-rules ()
+    [(_ i t v . b) (parameterize ([dotted-env (extend (dotted-env) i (cons t v))]) . b)]))

collects/typed-scheme/env/init-envs.rkt

@@ -1,7 +1,7 @@
 #lang scheme/base
 (provide (all-defined-out))
 (require "../utils/utils.rkt"
-         "type-env.rkt" 
+         "global-env.rkt" 
 	 "type-name-env.rkt"
 	 "type-alias-env.rkt"
          unstable/struct racket/dict

collects/typed-scheme/env/lexical-env.rkt

@@ -1,8 +1,15 @@
 #lang scheme/base
 
+;; this environment maps *lexical* variables to types
+;; it also contains the proposition environment
+
+;; these environments are unified in "Logical Types for Scheme"
+;; but split here for performance
+
 (require "../utils/utils.rkt"
-	 "type-environments.rkt" 
+	 "type-env-structs.rkt"
-	 "type-env.rkt"
+         "global-env.rkt"
+         "dotted-env.rkt"
 	 unstable/mutated-vars syntax/id-table
          (only-in scheme/contract ->* -> or/c any/c listof cons/c)
          (utils tc-utils)
@@ -13,11 +20,11 @@
 (provide lexical-env with-lexical-env with-lexical-env/extend with-update-type/lexical
          with-lexical-env/extend/props)
 (p/c
- [lookup-type/lexical ((identifier?) (lex-env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))]
+ [lookup-type/lexical ((identifier?) (prop-env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))]
- [update-type/lexical (((identifier? Type/c . -> . Type/c) identifier?) (lex-env?) . ->* . env?)])
+ [update-type/lexical (((identifier? Type/c . -> . Type/c) identifier?) (prop-env?) . ->* . env?)])
 
 ;; the current lexical environment
-(define lexical-env (make-parameter (make-empty-lex-env (make-immutable-free-id-table))))
+(define lexical-env (make-parameter (make-empty-prop-env (make-immutable-free-id-table))))
 
 ;; run code in a new env
 (define-syntax-rule (with-lexical-env e . b)

collects/typed-scheme/env/tvar-env.rkt

@@ -0,0 +1,15 @@
+#lang racket/base
+
+;; this environment maps type variables names (symbols)
+;; to types representing the type variable
+;; technically, the mapped-to type is unnecessary, but it's convenient to have it around? maybe?
+
+(require "type-env-structs.rkt")
+(provide (all-defined-out))
+
+;; the initial type variable environment - empty
+;; this is used in the parsing of types
+(define initial-tvar-env (make-empty-env #hasheq()))
+
+;; a parameter for the current type variables
+(define current-tvars (make-parameter initial-tvar-env))

collects/typed-scheme/env/type-env-structs.rkt

@@ -3,34 +3,29 @@
 (require scheme/contract unstable/sequence racket/dict syntax/id-table
          (prefix-in r: "../utils/utils.rkt")
          scheme/match (r:rep filter-rep rep-utils type-rep) unstable/struct
-         (except-in (r:utils tc-utils) make-env)
+         (except-in (r:utils tc-utils) make-env))
-         #;(r:typecheck tc-metafunctions))
 
-(provide current-tvars
+(provide extend
-         extend
          env?
          lookup
          extend-env
          extend/values
-         dotted-env
-         initial-tvar-env
          env-map
          make-empty-env
          env-filter
          env-keys+vals
          env-props
          replace-props
-         with-dotted-env/extend
+         prop-env? make-empty-prop-env)
-         lex-env? make-empty-lex-env)
 
 ;; eq? has the type of equal?, and l is an alist (with conses!)
 ;; props is a list of known propositions
 (r:d-s/c env ([l (and/c (not/c dict-mutable?) dict?)]) #:transparent)
-(r:d-s/c (lex-env env) ([props (listof Filter/c)]) #:transparent)
+(r:d-s/c (prop-env env) ([props (listof Filter/c)]) #:transparent)
 
 (define (mk-env orig dict)
   (match orig
-    [(lex-env _ p) (lex-env dict p)]
+    [(prop-env _ p) (prop-env dict p)]
     [_ (env dict)]))
 
 (define (env-filter f e)
@@ -46,27 +41,17 @@
        (dict? . -> . env?)
        (env dict))
 
-(r:d/c (make-empty-lex-env dict)
+(r:d/c (make-empty-prop-env dict)
-       (dict? . -> . lex-env?)
+       (dict? . -> . prop-env?)
-       (lex-env dict null))
+       (prop-env dict null))
 
 (r:d/c (env-props e)
-       (lex-env? . -> . (listof Filter/c))
+       (prop-env? . -> . (listof Filter/c))
-       (lex-env-props e))
+       (prop-env-props e))
 
 (define (env-keys+vals e)
   (match e
-    [(env l) (for/list ([(k v) (in-dict l)]) (cons k v))]))
+    [(env l) (for/list ([(k v) (in-dict l)]) (cons k v))]))  
-
-;; the initial type variable environment - empty
-;; this is used in the parsing of types
-(define initial-tvar-env (make-empty-env #hasheq()))
-
-;; a parameter for the current type variables
-(define current-tvars (make-parameter initial-tvar-env))  
-
-;; the environment for types of ... variables
-(define dotted-env (make-parameter (make-empty-env (make-immutable-free-id-table))))
 
 (r:d/c (env-map f e)
   ((any/c any/c . -> . any/c) env? . -> . env?)
@@ -86,8 +71,8 @@
 
 (define (replace-props e props)
   (match e
-    [(lex-env l p)
+    [(prop-env l p)
-     (lex-env l props)]))
+     (prop-env l props)]))
 
 (define (lookup e key fail)
   (match e
@@ -106,7 +91,3 @@
                  [else (extend env ks vs)]))
          env kss vss))
 
-;; run code in an extended dotted env
-(define-syntax with-dotted-env/extend
-  (syntax-rules ()
-    [(_ i t v . b) (parameterize ([dotted-env (extend (dotted-env) i (cons t v))]) . b)]))

collects/typed-scheme/infer/infer-unit.rkt

@@ -9,7 +9,7 @@
            "env/type-name-env.rkt")
           make-env)
          (except-in (path-up "types/utils.rkt") Dotted)
-         (only-in (path-up "env/type-environments.rkt") lookup current-tvars)
+         (only-in (path-up "env/type-env-structs.rkt" "env/tvar-env.rkt") lookup current-tvars)
          "constraint-structs.rkt"
 	 "signatures.rkt"                  
          scheme/match

collects/typed-scheme/private/parse-type.rkt

@@ -6,7 +6,7 @@
          (utils tc-utils stxclass-util)
          syntax/stx (prefix-in c: scheme/contract)
          syntax/parse
-         (env type-environments type-name-env type-alias-env lexical-env)         
+         (env type-env-structs tvar-env dotted-env type-name-env type-alias-env lexical-env)         
          scheme/match unstable/debug
          (for-template scheme/base "colon.ss")
          ;; needed at this phase for tests

collects/typed-scheme/private/type-annotation.rkt

@@ -3,7 +3,7 @@
 (require "../utils/utils.rkt" 
 	 (rep type-rep)
 	 (utils tc-utils)
-	 (env type-env)
+	 (env global-env)
          (except-in (types subtype union convenience resolve utils) -> ->*)
          (private parse-type)
          (only-in scheme/contract listof ->)

collects/typed-scheme/private/with-types.rkt

@@ -12,8 +12,9 @@
                              "private/parse-type.rkt"
                              "private/type-contract.rkt"
                              "typecheck/typechecker.rkt"
-                             "env/type-environments.rkt" 
+                             "env/type-env-structs.rkt" 
-                             "env/type-env.rkt"
+                             "env/global-env.rkt"
+                             "env/tvar-env.rkt"
                              "infer/infer.rkt"
                              "utils/tc-utils.rkt"
                              "types/utils.rkt"

collects/typed-scheme/tc-setup.rkt

@@ -7,7 +7,7 @@
          (private type-contract)
          (types utils convenience)
          (typecheck typechecker provide-handling tc-toplevel)
-         (env type-environments type-name-env type-alias-env)
+         (env tvar-env type-name-env type-alias-env)
          (r:infer infer)
          (utils tc-utils)
          (rep type-rep)
@@ -57,4 +57,4 @@
                          [expanded-module-stx fully-expanded-stx])
             (let ([result (checker fully-expanded-stx)])
               (do-time "Typechecking Done")
-              . body)))))))
+              . body)))))))

collects/typed-scheme/typecheck/tc-app.rkt

@@ -16,7 +16,7 @@
          (types utils abbrev union subtype resolve convenience type-table)
          (utils tc-utils)
          (only-in srfi/1 alist-delete)
-         (except-in (env type-environments) extend)
+         (except-in (env type-env-structs tvar-env) extend)
          (rep type-rep filter-rep object-rep)
          (r:infer infer)
          '#%paramz

collects/typed-scheme/typecheck/tc-dots-unit.rkt

@@ -3,7 +3,7 @@
 (require "../utils/utils.rkt" 
 	 "signatures.rkt"
          (utils tc-utils)
-         (env type-environments)
+         (env type-env-structs dotted-env tvar-env)
          (types utils)
          (rep type-rep)
          syntax/kerncase

collects/typed-scheme/typecheck/tc-envops.rkt

@@ -9,7 +9,7 @@
          (rep type-rep object-rep)
          (utils tc-utils)
          (types resolve)
-         (only-in (env type-environments lexical-env) env? update-type/lexical env-map env-props replace-props)
+         (only-in (env type-env-structs lexical-env) env? update-type/lexical env-map env-props replace-props)
          scheme/contract scheme/match
          mzlib/trace unstable/debug unstable/struct
          (typecheck tc-metafunctions)

collects/typed-scheme/typecheck/tc-expr-unit.rkt

@@ -11,7 +11,7 @@
          (only-in (infer infer) restrict)
          (except-in (utils tc-utils stxclass-util))
          (env lexical-env)
-         (only-in (env type-environments) lookup current-tvars extend-env)
+         (only-in (env type-env-structs tvar-env) lookup current-tvars extend-env)
          racket/private/class-internal unstable/debug
          (except-in syntax/parse id)
          (only-in srfi/1 split-at))

collects/typed-scheme/typecheck/tc-if.rkt

@@ -6,7 +6,7 @@
          (rep type-rep filter-rep object-rep)
          (rename-in (types convenience subtype union utils comparison remove-intersect abbrev filter-ops)
                     [remove *remove])
-         (env lexical-env type-environments)
+         (env lexical-env type-env-structs)
          (r:infer infer)
 	 (utils tc-utils)
          (typecheck tc-envops tc-metafunctions)

collects/typed-scheme/typecheck/tc-lambda-unit.rkt

@@ -13,7 +13,7 @@
                     [make-arr* make-arr])
          (private type-annotation)
          (types abbrev utils)
-	 (env type-environments lexical-env)
+	 (env type-env-structs lexical-env dotted-env tvar-env)
 	 (utils tc-utils)
          unstable/debug
          scheme/match)

collects/typed-scheme/typecheck/tc-let-unit.rkt

@@ -4,7 +4,7 @@
 (require "signatures.rkt" "tc-metafunctions.rkt" "tc-subst.rkt"
          (types utils convenience)
          (private type-annotation parse-type)
-	 (env lexical-env type-alias-env type-env type-environments)
+	 (env lexical-env type-alias-env global-env type-env-structs)
          (rep type-rep)
          syntax/free-vars
          mzlib/trace unstable/debug

collects/typed-scheme/typecheck/tc-structs.rkt

@@ -4,7 +4,7 @@
 	 (except-in (rep type-rep free-variance) Dotted)
          (private parse-type)
 	 (types convenience utils union resolve abbrev)
-	 (env type-env type-environments type-name-env)
+	 (env global-env type-env-structs type-name-env tvar-env)
 	 (utils tc-utils)
          "def-binding.rkt"
          syntax/kerncase

collects/typed-scheme/typecheck/tc-toplevel.rkt

@@ -13,8 +13,8 @@
          (rep type-rep)
          (types utils convenience)
          (private parse-type type-annotation type-contract)
-         (env type-env init-envs type-name-env type-alias-env lexical-env)
+         (env global-env init-envs type-name-env type-alias-env lexical-env)
-         unstable/mutated-vars syntax/id-table
+	 unstable/mutated-vars syntax/id-table
          (utils tc-utils)
          "provide-handling.rkt"
          "def-binding.rkt"

collects/typed-scheme/typed-scheme.rkt

@@ -8,7 +8,7 @@
           (private type-contract optimize)
           (types utils convenience)
 	  (typecheck typechecker provide-handling tc-toplevel)
-	  (env type-environments type-name-env type-alias-env)
+	  (env type-name-env type-alias-env)
 	  (r:infer infer)
 	  (utils tc-utils)
 	  (rep type-rep)