add make-vector refinement types

typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl

@@ -126,10 +126,11 @@ specifying the language of your program:
 @racketmod[typed/racket #:with-refinements]
 
 
-With this language option on, type checking the following arithmetic
+With this language option on, type checking the following
 primitives will produce more specific logical info (when they are being
 applied to 2 or 3 arguments): @racket[*], @racket[+], @racket[-],
-@racket[<], @racket[<=], @racket[=], @racket[>=], and @racket[>].
+@racket[<], @racket[<=], @racket[=], @racket[>=], @racket[>],
+and @racket[make-vector].
 
 This allows code such as the following to type check:
 

typed-racket-lib/typed-racket/rep/object-rep.rkt

@@ -100,7 +100,7 @@
          Path-intern-table
          name* elems* #:construct (make-Path elems* name*)))]
      [(? LExp? l) (if (null? elems) l -empty-obj)]
-     [(Empty:) -empty-obj])])
+     [_ -empty-obj])])
 
 (define Path-intern-table (make-weak-hash))
 

typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt

@@ -22,7 +22,8 @@
          ;; Needed for current implementation of typechecking letrec-syntax+values
          (for-template (only-in racket/base list letrec-values
                                 + - * < <= = >= > add1 sub1 modulo
-                                min max vector-length random)
+                                min max vector-length random
+                                make-vector)
                        ;; see tc-app-contracts.rkt
                        racket/contract/private/provide)
 
@@ -468,7 +469,7 @@
 
 
 ;; adds linear info for the following operations:
-;; + - * < <= = >= >
+;; + - * < <= = >= > make-vector
 ;; when the arguments are integers w/ objects.
 ;; These are the 'axiomatized' arithmetic operators.
 ;; NOTE: We should keep these axiomatizations so that they
@@ -518,7 +519,7 @@
   ;; integer compatible form we want to enrich with info when
   ;; #:with-logical-refinements is specified by the user
   (match result
-    [(tc-result1: ret-t ps _)
+    [(tc-result1: ret-t ps orig-obj)
      (syntax-parse form
        ;; *
        [(#%plain-app (~literal *) (~var e1 (t/obj -Int)) (~var e2 (t/obj -Int)))
@@ -572,6 +573,15 @@
                          (obj e2)
                          (obj e3))))
         (add-p/not-p result p)]
+       ;; make-vector include length in result
+       [(#%plain-app (~literal make-vector)
+                     (~var size (t/obj -Int))
+                     . _)
+        #:when (Object? (obj size))
+        (ret (-refine/fresh v ret-t (-eq (-lexp (-vec-len-of (-id-path v)))
+                                         (obj size)))
+             ps
+             orig-obj)]
        [_ result])]
     [_ result]))
 

typed-racket-test/succeed/safe-vector-untyped.rkt

@@ -1,6 +1,6 @@
 #lang racket/base
 
-(require (prefix-in safe- "safe-vector.rkt"))
+(require "safe-vector.rkt")
 
 (define len 50)
  
@@ -11,7 +11,7 @@
   (collect-garbage)
   (time (for*/sum ([_ (in-range 10000)]
                    [i (in-range len)])
-          (safe-vec-ref vec i))))
+          (safe-vector-ref vec i))))
 
 (define (run-safe-set!-test)
   (define vec (make-vector len 0))
@@ -20,7 +20,7 @@
   (collect-garbage)
   (time (for* ([_ (in-range 10000)]
                [i (in-range len)])
-          (safe-vec-set! vec i 0))))
+          (safe-vector-set! vec i 0))))
 
 
 

typed-racket-test/succeed/safe-vector.rkt

@@ -3,14 +3,6 @@
 (require typed/racket/unsafe
          racket/unsafe/ops)
 
-(unsafe-require/typed 
- typed/racket/base
- [make-vector
-  (All (A) (-> ([size : Natural]
-                [val : A])
-               (Refine [v : (Vectorof A)]
-                       (= size (vector-length v)))))])
-
 (provide (all-defined-out))
 
 (: safe-vector-ref (All (A) (-> ([v : (Vectorof A)]