typed-racket icon indicating copy to clipboard operation
typed-racket copied to clipboard

Patched require/untyped-contract to accept a language spec.

Open Rscho314 opened this issue 2 years ago • 2 comments

Hi @bennn ,

This is a very modest proposal for #1286. I did not patch the docs yet, but I will do so if there is interest in this pull request. It seems to work with the following test code (changed language to typed/racket/no-check):

server.rkt

#lang typed/racket/no-check ;shallow ;optional ;no-check

(provide mynum check-array-shape)

(define mynum 42)

(define-type (MVec T) (Mutable-Vectorof T))

(define-type Indexes (MVec Index))
(define-type In-Indexes (U (MVec Integer) Indexes))

(: check-array-shape (In-Indexes (-> Nothing) -> Indexes))
(define (check-array-shape ds fail)
  (define dims (vector-length ds))
  (define: new-ds : Indexes (make-vector dims 0))
  (let loop ([#{i : Nonnegative-Fixnum} 0])
    (cond [(i . < . dims)
           (define di (vector-ref ds i))
           (cond [(index? di)  (vector-set! new-ds i di)
                               (loop (+ i 1))]
                 [else  (fail)])]
          [else  new-ds])))

main.rkt

#lang racket/base

(require typed/untyped-utils
         typed/racket/no-check
         (except-in "server.rkt"
                    check-array-shape))

(require/untyped-contract
 "server.rkt"
 'typed/racket/no-check
 [check-array-shape  #;((Mutable-Vectorof Integer) (-> Nothing) -> (Mutable-Vectorof Index))
                     ((Vectorof Integer) (-> Nothing) -> (Vectorof Index))])

(check-array-shape (vector 1 2 3) (lambda () (error 'die)))

Cheers!

Rscho314 avatar Jun 11 '23 21:06 Rscho314

Hi Raol, sorry I am so slow. Just want you to know that I know this PR exists and will take a look soon!

bennn avatar Jun 15 '23 14:06 bennn

EDIT: nevermind, the problem was that I used 'typed/racket/no-check as the language spec. We should improve the message.

Tried running this on the example, and I'm getting an error about an (only-in quote):

only-in: identifier `quote' not included in nested require spec
  at: "server.rkt"
  in: (only-in "server.rkt" (quote quote3) (check-array-shape check-array-shape4))

bennn avatar Jun 10 '24 22:06 bennn