Fix provide: when it's after the definition

Closes PR 11172

Please merge into 6.0
(cherry picked from commit 7e1b3c306d)
This commit is contained in:
Asumu Takikawa 2013-11-20 18:42:28 -05:00 committed by Ryan Culpepper
parent f2129e105f
commit 3e7c9bcadf
2 changed files with 22 additions and 2 deletions

View File

@ -1097,9 +1097,17 @@ This file defines two sorts of primitives. All of them are provided into any mod
(define-syntax (provide: stx)
(syntax-parse stx
[(_ [i:id t] ...)
;; indirection through i*s allows `provide: to come
;; before the original definitions/type annotations
(define i*s (generate-temporaries #'(i ...)))
(for ([i* (in-list i*s)]
[i (in-list (syntax->list #'(i ...)))])
;; lift allows `provide:` to come before original definition
(syntax-local-lift-module-end-declaration #`(define #,i* #,i)))
(define/with-syntax (i* ...) i*s)
(syntax/loc stx
(begin (: i t) ...
(provide i ...)))]))
(begin (: i* t) ...
(provide (rename-out [i* i] ...))))]))
(define-syntax (declare-refinement stx)
(syntax-parse stx

View File

@ -0,0 +1,12 @@
#lang racket/load
;; Test for PR 11172
(module a typed/racket (: n Positive-Integer) (define n 10) (provide: [n Integer]))
(module b typed/racket (define n 10) (provide: [n Integer]))
(module c typed/racket (provide: [n Integer]) (define n 10))
(module d typed/racket (provide: [n Integer]) (: n Positive-Integer) (define n 10))
(require 'a)
n