commit df63a0bf57264a2f452942cb7fe35ed4874190ab
parent 088635c33a6bf42673c6c33eb15623e939f31baf
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Sat, 24 Sep 2016 16:43:17 -0400
predefine "type" stx-category and define-primop in typecheck.rkt (and turnstile)
Diffstat:
11 files changed, 26 insertions(+), 62 deletions(-)
diff --git a/macrotypes/examples/stlc+lit.rkt b/macrotypes/examples/stlc+lit.rkt
@@ -1,6 +1,5 @@
#lang s-exp macrotypes/typecheck
(extends "stlc.rkt")
-(provide define-primop)
;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
;; Types:
@@ -10,27 +9,9 @@
;; - terms from stlc.rkt
;; - numeric literals
;; - prim +
-;; Typechecking forms:
-;; - define-primop
(define-base-type Int)
-;; Using τ.norm leads to a "not valid type" error when file is compiled
-(define-syntax define-primop
- (syntax-parser #:datum-literals (:)
- [(_ op:id : τ)
- #:with op/tc (generate-temporary #'op)
- #'(begin
- (provide (rename-out [op/tc op]))
- (define-primop op/tc op : τ))]
- [(_ op/tc op : τ:type)
- #'(begin
- #;(define-syntax op/tc (make-rename-transformer (assign-type #'op #'τ)))
- ; rename transformer doesnt seem to expand at the right time
- ; - op still has no type in #%app
- (define-syntax op/tc
- (make-variable-like-transformer (assign-type #'op #'τ))))]))
-
(define-primop + : (→ Int Int Int))
(define-typed-syntax #%datum #:literals (#%datum)
diff --git a/macrotypes/examples/stlc+tup.rkt b/macrotypes/examples/stlc+tup.rkt
@@ -1,7 +1,5 @@
#lang s-exp macrotypes/typecheck
(extends "ext-stlc.rkt")
-
-(require (for-syntax racket/list))
;; Simply-Typed Lambda Calculus, plus tuples
;; Types:
diff --git a/macrotypes/examples/stlc.rkt b/macrotypes/examples/stlc.rkt
@@ -1,7 +1,4 @@
#lang s-exp macrotypes/typecheck
-(provide (for-syntax current-type=? types=?))
-
-(require (for-syntax racket/list))
;; Simply-Typed Lambda Calculus
;; - no base types; can't write any terms
@@ -10,12 +7,6 @@
;; - var
;; - multi-arg λ (0+)
;; - multi-arg #%app (0+)
-;; Other:
-;; - "type" syntax category; defines:
-;; - define-base-type
-;; - define-type-constructor
-
-(define-syntax-category type)
(define-type-constructor → #:arity >= 1
#:arg-variances (λ (stx)
@@ -35,7 +26,8 @@
#:with [e_fn- (~→ τ_in ... τ_out)] (infer+erase #'e_fn)
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
#:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...))
- (num-args-fail-msg #'e_fn #'(τ_in ...) #'(e_arg ...))
+ (num-args-fail-msg #'e_fn #'(τ_in ...) #'(e_arg ...))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
- (typecheck-fail-msg/multi #'(τ_in ...) #'(τ_arg ...) #'(e_arg ...))
+ (typecheck-fail-msg/multi
+ #'(τ_in ...) #'(τ_arg ...) #'(e_arg ...))
(⊢ (#%app- e_fn- e_arg- ...) : τ_out)])
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
@@ -46,7 +46,7 @@
[(_ . stuff)
(syntax/loc this-syntax
(#%module-begin
- (provide #%module-begin #%top-interaction #%top require) ; useful racket forms
+ (provide #%module-begin #%top-interaction #%top require only-in) ; useful racket forms
. stuff))]))
(struct exn:fail:type:runtime exn:fail:user ())
@@ -839,6 +839,23 @@
(syntax-parser
[(_ (~var x id) . rst) #'(define-basic-checked-stx x : name . rst)])))]))
+;; pre-declare all type-related functions and forms
+(define-syntax-category type)
+
+(define-syntax define-primop
+ (syntax-parser #:datum-literals (:)
+ [(define-primop op:id : τ)
+ #:with op/tc (generate-temporary #'op)
+ #`(begin-
+ (provide- #,(syntax/loc this-syntax (rename-out- [op/tc op])))
+ (define-primop op/tc op : τ))]
+ [(define-primop op/tc op : τ:type)
+ #'(begin-
+ ; rename transformer doesnt seem to expand at the right time
+ ; - op still has no type in #%app
+ (define-syntax op/tc
+ (make-variable-like-transformer (assign-type #'op #'τ))))]))
+
; substitution
(begin-for-syntax
(define-syntax ~Any/bvs ; matches any tycon
diff --git a/turnstile/examples/exist.rkt b/turnstile/examples/exist.rkt
@@ -21,8 +21,7 @@
--------
[⊢ e- ⇒ ∃τ.norm])
-(define-typed-syntax
- (open [x:id (~datum <=) e_packed (~datum with) X:id] e) ≫
+(define-typed-syntax (open [x:id (~datum <=) e_packed (~datum with) X:id] e) ≫
;; The subst below appears to be a hack, but it's not really.
;; It's the (TaPL) type rule itself that is fast and loose.
;; Leveraging the macro system's management of binding reveals this.
diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
@@ -1,7 +1,6 @@
#lang turnstile
(extends "rosette2.rkt" ; extends typed rosette
#:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge)
-(require (only-in "../stlc+lit.rkt" define-primop))
(require (prefix-in ro: rosette)) ; untyped
(require (only-in sdsl/bv/lang/bvops bvredand bvredor bv bv*)
(prefix-in bv: (only-in sdsl/bv/lang/bvops BV)))
diff --git a/turnstile/examples/rosette/lib/synthax.rkt b/turnstile/examples/rosette/lib/synthax.rkt
@@ -1,6 +1,6 @@
#lang turnstile
(require
- (prefix-in t/ro: (only-in "../rosette2.rkt" Int Bool type C→ CSolution Unit))
+ (prefix-in t/ro: (only-in "../rosette2.rkt" Int Bool C→ CSolution Unit))
(prefix-in ro: rosette/lib/synthax))
(provide print-forms)
@@ -10,7 +10,7 @@
#:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
--------
[⊢ [_ ≫ (??/progsrc) ⇒ : t/ro:Int]]]
- [(qq pred : ty:t/ro:type) ≫
+ [(qq pred : ty:type) ≫
#:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
[⊢ [pred ≫ pred- ⇐ : (t/ro:C→ ty.norm t/ro:Bool)]]
--------
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -38,7 +38,7 @@
(only-in "../stlc+cons.rkt" Unit [List Listof])))
(only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→])
(only-in "../stlc+cons.rkt" [~List ~CListof])
- (only-in "../stlc+reco+var.rkt" [define stlc:define] define-primop)
+ (only-in "../stlc+reco+var.rkt" [define stlc:define])
(rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?]))
;; copied from rosette.rkt
diff --git a/turnstile/examples/stlc+lit.rkt b/turnstile/examples/stlc+lit.rkt
@@ -1,6 +1,5 @@
#lang turnstile/lang
(extends "stlc.rkt")
-(provide define-primop)
;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
;; Types:
@@ -10,26 +9,9 @@
;; - terms from stlc.rkt
;; - numeric literals
;; - prim +
-;; Typechecking forms:
-;; - define-primop
(define-base-type Int)
-;; Using τ.norm leads to a "not valid type" error when file is compiled
-(define-syntax define-primop
- (syntax-parser #:datum-literals (:)
- [(define-primop op:id : τ)
- #:with op/tc (generate-temporary #'op)
- #`(begin-
- (provide- #,(syntax/loc this-syntax (rename-out- [op/tc op])))
- (define-primop op/tc op : τ))]
- [(define-primop op/tc op : τ:type)
- #'(begin-
- ; rename transformer doesnt seem to expand at the right time
- ; - op still has no type in #%app
- (define-syntax op/tc
- (make-variable-like-transformer (assign-type #'op #'τ))))]))
-
(define-primop + : (→ Int Int Int))
(define-typed-syntax #%datum
diff --git a/turnstile/examples/stlc+tup.rkt b/turnstile/examples/stlc+tup.rkt
@@ -1,8 +1,6 @@
#lang turnstile/lang
(extends "ext-stlc.rkt")
-(require (for-syntax racket/list))
-
;; Simply-Typed Lambda Calculus, plus tuples
;; Types:
;; - types from ext-stlc.rkt
diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt
@@ -1,7 +1,5 @@
#lang turnstile/lang
-(provide only-in (for-syntax current-type=? types=?))
-(define-syntax-category type)
(define-type-constructor → #:arity >= 1
#:arg-variances (λ (stx)
(syntax-parse stx
@@ -23,7 +21,7 @@
(define-typed-syntax (#%app e_fn e_arg ...) ≫
[⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)]
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
- (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
+ (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
[⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
--------
[⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out])
