commit 3707d90531f00997ba39e8090f91e2c1a5844b04
parent f90c464a19d6fd3f2836efa609e0c5cea70de0f0
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 20 Jul 2016 18:44:15 -0400
enable use of define-type-alias in language implementations
- using \tau.norm in define-type-alias implementation causes
"invalid type" errors when the file is compiled
Diffstat:
8 files changed, 25 insertions(+), 17 deletions(-)
diff --git a/macrotypes/examples/stlc+lit.rkt b/macrotypes/examples/stlc+lit.rkt
@@ -15,14 +15,15 @@
(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 : τ:type)
+ [(_ op:id : τ)
#:with op/tc (generate-temporary #'op)
#'(begin
(provide (rename-out [op/tc op]))
(define-primop op/tc op : τ))]
- [(_ 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
diff --git a/macrotypes/examples/stlc+reco+var.rkt b/macrotypes/examples/stlc+reco+var.rkt
@@ -18,10 +18,11 @@
;; - define-type-alias
(provide define-type-alias)
+;; Using τ.norm leads to a "not valid type" error when file is compiled
(define-syntax define-type-alias
(syntax-parser
[(_ alias:id τ:type)
- #'(define-syntax alias (make-variable-like-transformer #'τ.norm) #;(syntax-parser [x:id #'τ.norm]))]
+ #'(define-syntax alias (make-variable-like-transformer #'τ))]
[(_ (f:id x:id ...) ty)
#'(define-syntax (f stx)
(syntax-parse stx
diff --git a/macrotypes/stx-utils.rkt b/macrotypes/stx-utils.rkt
@@ -107,5 +107,5 @@
ref-stx]
[(id . args)
(let ([stx* (list* '#%app #'id (cdr (syntax-e stx)))])
- (datum->syntax stx stx* stx))])))
+ (datum->syntax stx stx* stx stx))])))
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
@@ -595,7 +595,10 @@
(define-syntax τ
(syntax-parser
;[(~var _ id) (add-orig (assign-type #'τ-internal #'kind) #'τ)])))]))
- [(~var _ id) (add-orig (assign-type #'(τ-internal) #'#%tag) #'τ)])))]))
+ [(~var _ id)
+ (add-orig
+ (assign-type
+ (syntax/loc this-syntax (τ-internal)) #'#%tag) #'τ)])))]))
; I use identifiers "τ" and "kind" but this form is not restricted to them.
; E.g., τ can be #'★ and kind can be #'#%kind (★'s type)
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
@@ -93,11 +93,6 @@
(define-base-type Stx)
-#;(define-typed-syntax syntax
- [(_ template) ≫
- --------
- [⊢ [[_ ≫ (syntax- template)] ⇒ : Stx]]])
-
;; ----------------------------------------------------------------------------
;; BV stuff
@@ -105,10 +100,14 @@
(define-base-type BV) ; represents actual bitvectors
; a predicate recognizing bv's of a certain size
+#;(define-syntax BVPred
+ (make-variable-like-transformer
+ ((current-type-eval) #'(→ BV Bool))))
(define-type-alias BVPred (→ BV Bool))
;; TODO: fix me --- need subtyping?
-(define-syntax Nat (make-rename-transformer #'Int))
+;(define-syntax Nat (make-rename-transformer #'Int))
+(define-type-alias Nat Int)
;; TODO: support higher order case --- need intersect types?
;(define-rosette-primop bv : (→ Int BVPred BV)
diff --git a/turnstile/examples/stlc+lit.rkt b/turnstile/examples/stlc+lit.rkt
@@ -15,14 +15,15 @@
(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 : τ:type)
+ [(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 : τ)
+ [(define-primop op/tc op : τ:type)
#'(begin-
; rename transformer doesnt seem to expand at the right time
; - op still has no type in #%app
diff --git a/turnstile/examples/stlc+reco+var.rkt b/turnstile/examples/stlc+reco+var.rkt
@@ -18,10 +18,11 @@
;; - define-type-alias
(provide define-type-alias)
+;; Using τ.norm leads to a "not valid type" error when file is compiled
(define-syntax define-type-alias
(syntax-parser
[(define-type-alias alias:id τ:type)
- #'(define-syntax alias (make-variable-like-transformer #'τ.norm))]
+ #'(define-syntax alias (make-variable-like-transformer #'τ))]
[(define-type-alias (f:id x:id ...) ty)
#'(define-syntax (f stx)
(syntax-parse stx
diff --git a/turnstile/examples/tests/run-all-tests.rkt b/turnstile/examples/tests/run-all-tests.rkt
@@ -27,11 +27,13 @@
(require "fomega2-tests.rkt")
(require "fomega3-tests.rkt")
-(require macrotypes/examples/tests/stlc+occurrence-tests)
-(require macrotypes/examples/tests/stlc+overloading-tests)
+;; these are not ported to turnstile yet
+;; see macrotypes/examples/tests/run-all-tests.rkt
+;(require macrotypes/examples/tests/stlc+occurrence-tests)
+;(require macrotypes/examples/tests/stlc+overloading-tests)
;; type inference
-(require macrotypes/examples/tests/infer-tests)
+;(require macrotypes/examples/tests/infer-tests)
(require "tlb-infer-tests.rkt")
;; type and effects
