commit e17ae9e5feb5992e6e4e5955afa7414919275f7a
parent e573a0927c5ce937bdbb9133b7bcb7828576eead
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 19 Jul 2016 15:42:35 -0400
update `extends` and `reuse` in typecheck.rkt to:
- support paths instead of filenames
- require prefix-in by default
- fix srclocs of extends
Diffstat:
10 files changed, 55 insertions(+), 40 deletions(-)
diff --git a/macrotypes/examples/fomega.rkt b/macrotypes/examples/fomega.rkt
@@ -1,5 +1,5 @@
#lang s-exp macrotypes/typecheck
-(extends "sysf.rkt" #:except #%datum ∀ Λ inst)
+(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst)
(reuse String #%datum #:from "stlc+reco+var.rkt")
;; System F_omega
diff --git a/macrotypes/examples/fomega2.rkt b/macrotypes/examples/fomega2.rkt
@@ -1,5 +1,5 @@
#lang s-exp macrotypes/typecheck
-(extends "sysf.rkt" #:except #%datum ∀ Λ inst);#:rename [~∀ ~sysf:∀])
+(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst)
(reuse String #%datum #:from "stlc+reco+var.rkt")
; same as fomega.rkt except here λ and #%app works as both type and terms
diff --git a/macrotypes/examples/stlc+effect.rkt b/macrotypes/examples/stlc+effect.rkt
@@ -1,5 +1,5 @@
#lang s-exp macrotypes/typecheck
-(extends "stlc+box.rkt" #:except ref deref := #%app λ)
+(extends "stlc+box.rkt" #:except ref Ref ~Ref ~Ref* Ref? deref := #%app λ)
(provide (for-syntax get-new-effects))
diff --git a/macrotypes/examples/stlc+reco+var.rkt b/macrotypes/examples/stlc+reco+var.rkt
@@ -1,6 +1,6 @@
#lang s-exp macrotypes/typecheck
-(extends "stlc+tup.rkt" #:except × ×? tup proj
- #:rename [~× ~stlc:×])
+(extends "stlc+tup.rkt" #:except × ×? tup proj ~× ~×*)
+(require (only-in "stlc+tup.rkt" [~× ~stlc:×]))
(provide × ∨ (for-syntax ~× ~×* ~∨ ~∨*))
@@ -30,6 +30,7 @@
(define-typed-syntax define
[(define x:id e)
#:with (e- τ) (infer+erase #'e)
+
#:with y (generate-temporary)
#'(begin-
(define-syntax x (make-rename-transformer (⊢ y : τ)))
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
@@ -43,14 +43,19 @@
(define-syntax (mb stx)
(syntax-parse stx
[(_ . stuff)
- #'(#%module-begin
+ (syntax/loc this-syntax
+ (#%module-begin
(provide #%module-begin #%top-interaction #%top require) ; useful racket forms
- . stuff)]))
+ . stuff))]))
(struct exn:fail:type:runtime exn:fail:user ())
+;; drop-file-ext : String -> String
(define-for-syntax (drop-file-ext filename)
(car (string-split filename ".")))
+;; extract-filename : PathString -> String
+(define-for-syntax (extract-filename f)
+ (path->string (path-replace-suffix (file-name-from-path f) "")))
(begin-for-syntax
(define-syntax-parameter stx (syntax-rules ())))
@@ -78,29 +83,35 @@
(define-syntax extends
(syntax-parser
[(_ base-lang
- (~optional (~seq #:except (~and x:id (~not _:keyword)) ...) #:defaults ([(x 1) null]))
- (~optional (~seq #:rename [old new] ...) #:defaults ([(old 1) null][(new 1) null]))
- (~optional (~seq #:prefix p ...) #:defaults ([(p 1) null])))
- #:with pre (or (let ([dat (syntax-e #'base-lang)])
- (and (string? dat)
- (string->symbol (drop-file-ext dat))))
- #'base-lang)
- #:with pre: (format-id #'pre "~a:" #'pre)
+ (~optional (~seq #:except (~and x:id (~not _:keyword)) ...)
+ #:defaults ([(x 1) null]))
+ (~optional (~seq #:rename [old new] ...)
+ #:defaults ([(old 1) null][(new 1) null])))
+ #:with pre:
+ (let ([pre (or (let ([dat (syntax-e #'base-lang)])
+ (and (string? dat) (extract-filename dat)))
+ #'base-lang)])
+ (format-id #'base-lang "~a:" pre))
#:with internal-pre (generate-temporary)
- #:with non-excluded-imports #'(except-in base-lang p ... x ... old ...)
+ #:with non-excluded-imports #'(except-in base-lang x ... old ...)
#:with conflicted? #'(λ (n) (member (string->symbol n) '(#%app λ #%datum begin let let* letrec if define)))
#:with not-conflicted? #'(λ (n) (and (not (conflicted? n)) n))
#`(begin
- (require (prefix-in pre: (only-in base-lang p ... x ...))) ; prefixed
- (require (rename-in (only-in base-lang old ...) [old new] ...))
- (require (filtered-in not-conflicted? non-excluded-imports))
- (require (filtered-in ; conflicted names, with (internal) prefix
+ #,(syntax/loc this-syntax
+ (require (prefix-in pre: base-lang))) ; prefixed
+ #,(syntax/loc this-syntax
+ (require (rename-in (only-in base-lang old ...) [old new] ...)))
+ #,(syntax/loc this-syntax
+ (require (filtered-in not-conflicted? non-excluded-imports)))
+ #,(syntax/loc this-syntax
+ (require (filtered-in ; conflicted names, with (internal) prefix
(let ([conflicted-pre (symbol->string (syntax->datum #'internal-pre))])
(λ (name) (and (conflicted? name)
(string-append conflicted-pre name))))
- non-excluded-imports))
- (provide (filtered-out
- (let* ([pre-str #,(string-append (drop-file-ext (syntax-e #'base-lang)) ":")]
+ non-excluded-imports)))
+ #,(quasisyntax/loc this-syntax
+ (provide (filtered-out
+ (let* ([pre-str #,(string-append (extract-filename (syntax-e #'base-lang)) ":")]
[int-pre-str #,(symbol->string (syntax->datum #'internal-pre))]
[pre-str-len (string-length pre-str)]
[int-pre-str-len (string-length int-pre-str)]
@@ -116,20 +127,23 @@
name))
(and (not (member out-name excluded)) out-name)))
(all-from-out base-lang))
- ))]))
+ )))]))
(define-syntax reuse
(syntax-parser
[(_ (~or x:id [old:id new:id]) ... #:from base-lang)
- #:with pre (or (let ([dat (syntax-e #'base-lang)])
- (and (string? dat)
- (string->symbol (drop-file-ext dat))))
- #'base-lang)
- #:with pre: (format-id #'pre "~a:" #'pre)
+ #:with pre:
+ (let ([pre (or (let ([dat (syntax-e #'base-lang)])
+ (and (string? dat) (extract-filename dat)))
+ #'base-lang)])
+ (format-id #'base-lang "~a:" pre))
#`(begin
- (require (rename-in (only-in base-lang old ...) [old new] ...))
- (require (prefix-in pre: (only-in base-lang x ...)))
- (provide (filtered-out
- (let* ([pre-str #,(string-append (drop-file-ext (syntax-e #'base-lang)) ":")]
+ #,(syntax/loc this-syntax
+ (require (rename-in (only-in base-lang old ...) [old new] ...)))
+ #,(syntax/loc this-syntax
+ (require (prefix-in pre: (only-in base-lang x ...))))
+ #,(quasisyntax/loc this-syntax
+ (provide (filtered-out
+ (let* ([pre-str #,(string-append (extract-filename (syntax-e #'base-lang)) ":")]
[pre-str-len (string-length pre-str)]
[drop-pre (λ (s) (substring s pre-str-len))]
[excluded (map (compose symbol->string syntax->datum) (syntax->list #'(new ...)))]
@@ -142,7 +156,7 @@
(and (not (member out-name excluded))
(member out-name origs)
out-name)))
- (all-from-out base-lang))))]))
+ (all-from-out base-lang)))))]))
(define-syntax add-expected
(syntax-parser
diff --git a/turnstile/examples/fomega.rkt b/turnstile/examples/fomega.rkt
@@ -1,5 +1,5 @@
#lang turnstile
-(extends "sysf.rkt" #:except #%datum ∀ Λ inst)
+(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst)
(reuse String #%datum #:from "stlc+reco+var.rkt")
;; System F_omega
diff --git a/turnstile/examples/fomega2.rkt b/turnstile/examples/fomega2.rkt
@@ -1,5 +1,5 @@
#lang turnstile
-(extends "sysf.rkt" #:except #%datum ∀ Λ inst);#:rename [~∀ ~sysf:∀])
+(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst)
(reuse String #%datum #:from "stlc+reco+var.rkt")
; same as fomega.rkt except here λ and #%app works as both type and terms
diff --git a/turnstile/examples/infer.rkt b/turnstile/examples/infer.rkt
@@ -1,5 +1,5 @@
#lang turnstile
-(extends "ext-stlc.rkt" #:except #%app λ)
+(extends "ext-stlc.rkt" #:except #%app λ ann)
(reuse inst #:from "sysf.rkt")
(require (only-in "sysf.rkt" ∀ ~∀ ∀? Λ))
(reuse cons [head hd] [tail tl] nil [isnil nil?] List list #:from "stlc+cons.rkt")
diff --git a/turnstile/examples/stlc+effect.rkt b/turnstile/examples/stlc+effect.rkt
@@ -1,5 +1,5 @@
#lang turnstile
-(extends "stlc+box.rkt" #:except ref deref := #%app λ)
+(extends "stlc+box.rkt" #:except ref Ref ~Ref ~Ref* Ref? deref := #%app λ)
;; Simply-Typed Lambda Calculus, plus mutable references
;; Types:
diff --git a/turnstile/examples/stlc+reco+var.rkt b/turnstile/examples/stlc+reco+var.rkt
@@ -1,6 +1,6 @@
#lang turnstile
-(extends "stlc+tup.rkt" #:except × ×? tup proj
- #:rename [~× ~stlc:×])
+(extends "stlc+tup.rkt" #:except × ×? tup proj ~× ~×*)
+(require (only-in "stlc+tup.rkt" [~× ~stlc:×]))
(provide × ∨ (for-syntax ~× ~×* ~∨ ~∨*))
