commit fc5731de00c595e3e878fb130e15e5dee0009a71
parent 8cce856e08a07e976c7d05a33c21d5f5bd62a468
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Sun, 9 Oct 2016 18:12:12 -0400
dont auto provide define-primops; add typed-out
Diffstat:
25 files changed, 632 insertions(+), 589 deletions(-)
diff --git a/macrotypes/examples/ext-stlc.rkt b/macrotypes/examples/ext-stlc.rkt
@@ -1,6 +1,5 @@
#lang s-exp macrotypes/typecheck
(extends "stlc+lit.rkt" #:except #%datum)
-(provide ⊔ (for-syntax current-join))
;; Simply-Typed Lambda Calculus, plus extensions (TAPL ch11)
;; Types:
@@ -17,10 +16,22 @@
;; - ascription (ann)
;; - let, let*, letrec
-(define-base-type Bool)
-(define-base-type String)
-(define-base-type Float)
-(define-base-type Char)
+(provide (for-syntax current-join)
+ ⊔ zero? =
+ (rename-out [typed- -] [typed* *])
+ ;; test all variations of typed-out
+ (typed-out [add1 (→ Int Int)]
+ [sub1 : (→ Int Int)]
+ [[not- (→ Bool Bool)] not]
+ [[void- : (→ Unit)] void]))
+
+(define-base-types Bool String Float Char Unit)
+
+;; test all variations of define-primop-out
+(define-primop zero? (→ Int Bool))
+(define-primop = : (→ Int Int Bool))
+(define-primop typed- - (→ Int Int Int))
+(define-primop typed* * : (→ Int Int Int))
(define-typed-syntax #%datum
[(#%datum . b:boolean) (⊢ #,(syntax/loc stx (#%datum- . b)) : Bool)]
@@ -29,13 +40,6 @@
[(#%datum . c:char) (⊢ #,(syntax/loc stx (#%datum- . c)) : Char)]
[(#%datum . x) (syntax/loc stx (stlc+lit:#%datum . x))])
-(define-primop zero? : (→ Int Bool))
-(define-primop = : (→ Int Int Bool))
-(define-primop - : (→ Int Int Int))
-(define-primop add1 : (→ Int Int))
-(define-primop sub1 : (→ Int Int))
-(define-primop not : (→ Bool Bool))
-
(define-typed-syntax and
[(and e1 e2)
#:with Bool* ((current-type-eval) #'Bool)
@@ -80,9 +84,6 @@
#:with (e2- τ2) (infer+erase #'e2_ann)
(⊢ (if- e_tst- e1- e2-) : (⊔ τ1 τ2))])
-(define-base-type Unit)
-(define-primop void : (→ Unit))
-
(define-typed-syntax begin
[(begin e_unit ... e)
#:with ([e_unit- _] ...) (infers+erase #'(e_unit ...)) ;(⇑s (e_unit ...) as Unit)
diff --git a/macrotypes/examples/fsub.rkt b/macrotypes/examples/fsub.rkt
@@ -14,7 +14,7 @@
;; - current-promote, expose
;; - extend current-sub? to call current-promote
-(define-primop + : (→ Nat Nat Nat))
+(provide (typed-out [+ : (→ Nat Nat Nat)]))
; can't just call expose in type-eval,
; otherwise typevars will have bound as type, rather than instantiated type
diff --git a/macrotypes/examples/infer.rkt b/macrotypes/examples/infer.rkt
@@ -12,6 +12,16 @@
;; a language with partial (local) type inference using bidirectional type checking
+(provide (typed-out [+ : (→ Int Int Int)]
+ [- : (→ Int Int Int)]
+ [void : (→ Unit)]
+ [= : (→ Int Int Bool)]
+ [zero? : (→ Int Bool)]
+ [sub1 : (→ Int Int)]
+ [add1 : (→ Int Int)]
+ [not : (→ Bool Bool)]
+ [abs : (→ Int Int)]))
+
(define-syntax → ; wrapping →
(syntax-parser
[(→ (~and Xs {X:id ...}) . rst)
@@ -19,16 +29,6 @@
(add-orig #'(∀ (X ...) (ext-stlc:→ . rst)) (get-orig this-syntax))]
[(→ . rst) (add-orig #'(∀ () (ext-stlc:→ . rst)) (get-orig this-syntax))]))
-(define-primop + : (→ Int Int Int))
-(define-primop - : (→ Int Int Int))
-(define-primop void : (→ Unit))
-(define-primop = : (→ Int Int Bool))
-(define-primop zero? : (→ Int Bool))
-(define-primop sub1 : (→ Int Int))
-(define-primop add1 : (→ Int Int))
-(define-primop not : (→ Bool Bool))
-(define-primop abs : (→ Int Int))
-
(begin-for-syntax
;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id)
;; finds the free Xs in the type
diff --git a/macrotypes/examples/mlish+adhoc.rkt b/macrotypes/examples/mlish+adhoc.rkt
@@ -1,7 +1,7 @@
#lang s-exp "../typecheck.rkt"
(require racket/fixnum racket/flonum)
-(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let let* and #%datum begin
+(extends "ext-stlc.rkt" #:except #%app λ → + - * void = zero? sub1 add1 not let let* and #%datum begin
#:rename [~→ ~ext-stlc:→])
;(reuse [inst sysf:inst] #:from "sysf.rkt")
(require (rename-in (only-in "sysf.rkt" inst) [inst sysf:inst]))
@@ -796,25 +796,25 @@
#'(∀ Xs (=> TC ... (ext-stlc:→ . tys_arr)))]))
; redefine these to use lifted →
-(define-primop + : (→ Int Int Int))
-(define-primop - : (→ Int Int Int))
-(define-primop * : (→ Int Int Int))
-(define-primop max : (→ Int Int Int))
-(define-primop min : (→ Int Int Int))
-(define-primop void : (→ Unit))
-(define-primop = : (→ Int Int Bool))
-(define-primop <= : (→ Int Int Bool))
-(define-primop >= : (→ Int Int Bool))
-(define-primop < : (→ Int Int Bool))
-(define-primop > : (→ Int Int Bool))
-(define-primop modulo : (→ Int Int Int))
-(define-primop zero? : (→ Int Bool))
-(define-primop sub1 : (→ Int Int))
-(define-primop add1 : (→ Int Int))
-(define-primop not : (→ Bool Bool))
-(define-primop abs : (→ Int Int))
-(define-primop even? : (→ Int Bool))
-(define-primop odd? : (→ Int Bool))
+(provide (typed-out [+ : (→ Int Int Int)]
+ [- : (→ Int Int Int)]
+ [* : (→ Int Int Int)]
+ [max : (→ Int Int Int)]
+ [min : (→ Int Int Int)]
+ [void : (→ Unit)]
+ [= : (→ Int Int Bool)]
+ [<= : (→ Int Int Bool)]
+ [>= : (→ Int Int Bool)]
+ [< : (→ Int Int Bool)]
+ [> : (→ Int Int Bool)]
+ [modulo : (→ Int Int Int)]
+ [zero? : (→ Int Bool)]
+ [sub1 : (→ Int Int)]
+ [add1 : (→ Int Int)]
+ [not : (→ Bool Bool)]
+ [abs : (→ Int Int)]
+ [even? : (→ Int Bool)]
+ [odd? : (→ Int Bool)]))
;; λ --------------------------------------------------------------------------
@@ -1124,11 +1124,10 @@
#:with (th- (~∀ () (~ext-stlc:→ τ_out))) (infer+erase #'th)
(⊢ (thread- th-) : Thread)])
-(define-primop random : (→ Int Int))
-(define-primop integer->char : (→ Int Char))
-(define-primop string->list : (→ String (List Char)))
-(define-primop string->number : (→ String Int))
-;(define-primop number->string : (→ Int String))
+(provide (typed-out [random : (→ Int Int)]
+ [integer->char : (→ Int Char)]
+ [string->list : (→ String (List Char))]
+ [string->number : (→ String Int)]))
(define-typed-syntax num->str #:export-as number->string
[f:id (assign-type #'number->string #'(→ Int String))]
[(_ n)
@@ -1136,18 +1135,18 @@
[(_ n rad)
#:with args- (⇑s (n rad) as Int)
(⊢ (number->string- . args-) : String)])
-(define-primop string : (→ Char String))
-(define-primop sleep : (→ Int Unit))
-(define-primop string=? : (→ String String Bool))
-(define-primop string<? : (→ String String Bool))
-(define-primop string<=? : (→ String String Bool))
-(define-primop string>? : (→ String String Bool))
-(define-primop string>=? : (→ String String Bool))
-(define-primop char=? : (→ Char Char Bool))
-(define-primop char<? : (→ Char Char Bool))
-(define-primop char<=? : (→ Char Char Bool))
-(define-primop char>? : (→ Char Char Bool))
-(define-primop char>=? : (→ Char Char Bool))
+(provide (typed-out [string : (→ Char String)]
+ [sleep : (→ Int Unit)]
+ [string=? : (→ String String Bool)]
+ [string<? : (→ String String Bool)]
+ [string<=? : (→ String String Bool)]
+ [string>? : (→ String String Bool)]
+ [string>=? : (→ String String Bool)]
+ [char=? : (→ Char Char Bool)]
+ [char<? : (→ Char Char Bool)]
+ [char<=? : (→ Char Char Bool)]
+ [char>? : (→ Char Char Bool)]
+ [char>=? : (→ Char Char Bool)]))
(define-typed-syntax string-append
[(_ . strs)
@@ -1314,7 +1313,7 @@
[(_ e)
#:with [e- _] (infer+erase #'e)
(⊢ (displayln- e-) : Unit)])
-(define-primop newline : (→ Unit))
+(provide (typed-out [newline : (→ Unit)]))
(define-typed-syntax list->vector
[(_ e)
@@ -1398,9 +1397,9 @@
(define-base-type String-Port)
(define-base-type Input-Port)
-(define-primop open-output-string : (→ String-Port))
-(define-primop get-output-string : (→ String-Port String))
-(define-primop string-upcase : (→ String String))
+(provide (typed-out [open-output-string : (→ String-Port)]
+ [get-output-string : (→ String-Port String)]
+ [string-upcase : (→ String String)]))
(define-typed-syntax write-string/tc #:export-as write-string
[(_ str out)
@@ -1416,9 +1415,9 @@
[(_ str)
#:with str- (⇑ str as String)
(⊢ (string-length- str-) : Int)])
-(define-primop make-string : (→ Int String))
-(define-primop string-set! : (→ String Int Char Unit))
-(define-primop string-ref : (→ String Int Char))
+(provide (typed-out [make-string : (→ Int String)]
+ [string-set! : (→ String Int Char Unit)]
+ [string-ref : (→ String Int Char)]))
(define-typed-syntax string-copy!/tc #:export-as string-copy!
[(_ dest dest-start src)
#'(string-copy!/tc
@@ -1431,25 +1430,25 @@
#:with src-end- (⇑ src-end as Int)
(⊢ (string-copy!- dest- dest-start- src- src-start- src-end-) : Unit)])
-(define-primop fl+ : (→ Float Float Float))
-(define-primop fl- : (→ Float Float Float))
-(define-primop fl* : (→ Float Float Float))
-(define-primop fl/ : (→ Float Float Float))
-(define-primop fl= : (→ Float Float Bool))
-(define-primop flsqrt : (→ Float Float))
-(define-primop flceiling : (→ Float Float))
-(define-primop inexact->exact : (→ Float Int))
-(define-primop exact->inexact : (→ Int Float))
-(define-primop char->integer : (→ Char Int))
-(define-primop real->decimal-string : (→ Float Int String))
-(define-primop fx->fl : (→ Int Float))
+(provide (typed-out [fl+ : (→ Float Float Float)]
+ [fl- : (→ Float Float Float)]
+ [fl* : (→ Float Float Float)]
+ [fl/ : (→ Float Float Float)]
+ [fl= : (→ Float Float Bool)]
+ [flsqrt : (→ Float Float)]
+ [flceiling : (→ Float Float)]
+ [inexact->exact : (→ Float Int)]
+ [exact->inexact : (→ Int Float)]
+ [char->integer : (→ Char Int)]
+ [real->decimal-string : (→ Float Int String)]
+ [fx->fl : (→ Int Float)]))
(define-typed-syntax quotient+remainder
[(_ x y)
#:with x- (⇑ x as Int)
#:with y- (⇑ y as Int)
(⊢ (call-with-values- (λ- () (quotient/remainder- x- y-)) list-)
: (stlc+rec-iso:× Int Int))])
-(define-primop quotient : (→ Int Int Int))
+(provide (typed-out [quotient : (→ Int Int Int)]))
(define-typed-syntax set!
[(_ x:id e)
@@ -1460,7 +1459,7 @@
(define-typed-syntax provide-type [(_ ty ...) #'(provide- ty ...)])
-(define-typed-syntax provide
+(define-typed-syntax mlish-provide #:export-as provide
[(_ x:id ...)
#:with ([x- ty_x] ...) (infers+erase #'(x ...))
; TODO: use hash-code to generate this tmp
@@ -1478,8 +1477,8 @@
(define-syntax- x (make-rename-transformer (assign-type #'y #'x-ty))) ...)])
(define-base-type Regexp)
-(define-primop regexp-match : (→ Regexp String (List String)))
-(define-primop regexp : (→ String Regexp))
+(provide (typed-out [regexp-match : (→ Regexp String (List String))]
+ [regexp : (→ String Regexp)]))
(define-typed-syntax equal?
[(_ e1 e2)
diff --git a/macrotypes/examples/mlish.rkt b/macrotypes/examples/mlish.rkt
@@ -2,7 +2,7 @@
(require racket/fixnum racket/flonum
(for-syntax macrotypes/type-constraints macrotypes/variance-constraints))
-(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let let* and #%datum begin
+(extends "ext-stlc.rkt" #:except #%app λ → + - * void = zero? sub1 add1 not let let* and #%datum begin
#:rename [~→ ~ext-stlc:→])
(reuse inst #:from "sysf.rkt")
(require (only-in "ext-stlc.rkt" → →?))
@@ -22,17 +22,36 @@
(require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list)))
(require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup)))
-(module+ test
- (require (for-syntax rackunit)))
-
-(provide → →/test match2 define-type)
-
;; ML-like language
;; - top level recursive functions
;; - user-definable algebraic datatypes
;; - pattern matching
;; - (local) type inference
+(module+ test
+ (require (for-syntax rackunit)))
+
+(provide → →/test match2 define-type
+ ; redefine these to use lifted →
+ (typed-out [+ : (→ Int Int Int)]
+ [- : (→ Int Int Int)]
+ [* : (→ Int Int Int)]
+ [max : (→ Int Int Int)]
+ [min : (→ Int Int Int)]
+ [void : (→ Unit)]
+ [= : (→ Int Int Bool)]
+ [<= : (→ Int Int Bool)]
+ [< : (→ Int Int Bool)]
+ [> : (→ Int Int Bool)]
+ [modulo : (→ Int Int Int)]
+ [zero? : (→ Int Bool)]
+ [sub1 : (→ Int Int)]
+ [add1 : (→ Int Int)]
+ [not : (→ Bool Bool)]
+ [abs : (→ Int Int)]
+ [even? : (→ Int Bool)]
+ [odd? : (→ Int Bool)]))
+
;; creating possibly polymorphic types
;; ?∀ only wraps a type in a forall if there's at least one type variable
(define-syntax ?∀
@@ -811,26 +830,6 @@
#:with Xs (compute-tyvars #'rst)
#'(?∀ Xs (ext-stlc:→ . rst))]))
-; redefine these to use lifted →
-(define-primop + : (→ Int Int Int))
-(define-primop - : (→ Int Int Int))
-(define-primop * : (→ Int Int Int))
-(define-primop max : (→ Int Int Int))
-(define-primop min : (→ Int Int Int))
-(define-primop void : (→ Unit))
-(define-primop = : (→ Int Int Bool))
-(define-primop <= : (→ Int Int Bool))
-(define-primop < : (→ Int Int Bool))
-(define-primop > : (→ Int Int Bool))
-(define-primop modulo : (→ Int Int Int))
-(define-primop zero? : (→ Int Bool))
-(define-primop sub1 : (→ Int Int))
-(define-primop add1 : (→ Int Int))
-(define-primop not : (→ Bool Bool))
-(define-primop abs : (→ Int Int))
-(define-primop even? : (→ Int Bool))
-(define-primop odd? : (→ Int Bool))
-
; all λs have type (?∀ (X ...) (→ τ_in ... τ_out))
(define-typed-syntax λ
[(λ (x:id ...) body)
@@ -932,11 +931,10 @@
#:with (th- (~?∀ () (~ext-stlc:→ τ_out))) (infer+erase #'th)
(⊢ (thread- th-) : Thread)])
-(define-primop random : (→ Int Int))
-(define-primop integer->char : (→ Int Char))
-(define-primop string->list : (→ String (List Char)))
-(define-primop string->number : (→ String Int))
-;(define-primop number->string : (→ Int String))
+(provide (typed-out [random : (→ Int Int)]
+ [integer->char : (→ Int Char)]
+ [string->list : (→ String (List Char))]
+ [string->number : (→ String Int)]))
(define-typed-syntax number->string
[f:id (assign-type #'number->string- #'(→ Int String))]
[(number->string n)
@@ -944,10 +942,10 @@
[(number->string n rad)
#:with args- (⇑s (n rad) as Int)
(⊢ (number->string- . args-) : String)])
-(define-primop string : (→ Char String))
-(define-primop sleep : (→ Int Unit))
-(define-primop string=? : (→ String String Bool))
-(define-primop string<=? : (→ String String Bool))
+(provide (typed-out [string : (→ Char String)]
+ [sleep : (→ Int Unit)]
+ [string=? : (→ String String Bool)]
+ [string<=? : (→ String String Bool)]))
(define-typed-syntax string-append
[(string-append . strs)
@@ -1115,7 +1113,7 @@
[(displayln e)
#:with [e- _] (infer+erase #'e)
(⊢ (displayln- e-) : Unit)])
-(define-primop newline : (→ Unit))
+(provide (typed-out [newline : (→ Unit)]))
(define-typed-syntax list->vector
[(list->vector e)
@@ -1207,9 +1205,9 @@
(define-base-type String-Port)
(define-base-type Input-Port)
-(define-primop open-output-string : (→ String-Port))
-(define-primop get-output-string : (→ String-Port String))
-(define-primop string-upcase : (→ String String))
+(provide (typed-out [open-output-string : (→ String-Port)]
+ [get-output-string : (→ String-Port String)]
+ [string-upcase : (→ String String)]))
(define-typed-syntax write-string
[(write-string str out)
@@ -1225,9 +1223,9 @@
[(string-length str)
#:with str- (⇑ str as String)
(⊢ (string-length- str-) : Int)])
-(define-primop make-string : (→ Int String))
-(define-primop string-set! : (→ String Int Char Unit))
-(define-primop string-ref : (→ String Int Char))
+(provide (typed-out [make-string : (→ Int String)]
+ [string-set! : (→ String Int Char Unit)]
+ [string-ref : (→ String Int Char)]))
(define-typed-syntax string-copy!
[(string-copy! dest dest-start src)
#'(string-copy!
@@ -1240,17 +1238,17 @@
#:with src-end- (⇑ src-end as Int)
(⊢ (string-copy!- dest- dest-start- src- src-start- src-end-) : Unit)])
-(define-primop fl+ : (→ Float Float Float))
-(define-primop fl- : (→ Float Float Float))
-(define-primop fl* : (→ Float Float Float))
-(define-primop fl/ : (→ Float Float Float))
-(define-primop flsqrt : (→ Float Float))
-(define-primop flceiling : (→ Float Float))
-(define-primop inexact->exact : (→ Float Int))
-(define-primop exact->inexact : (→ Int Float))
-(define-primop char->integer : (→ Char Int))
-(define-primop real->decimal-string : (→ Float Int String))
-(define-primop fx->fl : (→ Int Float))
+(provide (typed-out [fl+ : (→ Float Float Float)]
+ [fl- : (→ Float Float Float)]
+ [fl* : (→ Float Float Float)]
+ [fl/ : (→ Float Float Float)]
+ [flsqrt : (→ Float Float)]
+ [flceiling : (→ Float Float)]
+ [inexact->exact : (→ Float Int)]
+ [exact->inexact : (→ Int Float)]
+ [char->integer : (→ Char Int)]
+ [real->decimal-string : (→ Float Int String)]
+ [fx->fl : (→ Int Float)]))
(define-typed-syntax quotient+remainder
[(quotient+remainder x y)
#:with x- (⇑ x as Int)
@@ -1258,7 +1256,7 @@
(⊢ (let-values- ([[a b] (quotient/remainder- x- y-)])
(list- a b))
: (stlc+rec-iso:× Int Int))])
-(define-primop quotient : (→ Int Int Int))
+(provide (typed-out [quotient : (→ Int Int Int)]))
(define-typed-syntax set!
[(set! x:id e)
@@ -1270,7 +1268,7 @@
(define-typed-syntax provide-type [(provide-type ty ...) #'(provide- ty ...)])
-(define-typed-syntax provide
+(define-typed-syntax mlish-provide #:export-as provide
[(provide x:id ...)
#:with ([x- ty_x] ...) (infers+erase #'(x ...))
; TODO: use hash-code to generate this tmp
@@ -1288,8 +1286,8 @@
(define-syntax x (make-rename-transformer (assign-type #'y #'x-ty))) ...)])
(define-base-type Regexp)
-(define-primop regexp-match : (→ Regexp String (List String)))
-(define-primop regexp : (→ String Regexp))
+(provide (typed-out [regexp-match : (→ Regexp String (List String))]
+ [regexp : (→ String Regexp)]))
(define-typed-syntax equal?
[(equal? e1 e2)
diff --git a/macrotypes/examples/stlc+lit.rkt b/macrotypes/examples/stlc+lit.rkt
@@ -10,9 +10,9 @@
;; - numeric literals
;; - prim +
-(define-base-type Int)
+(provide (typed-out [+ : (→ Int Int Int)]))
-(define-primop + : (→ Int Int Int))
+(define-base-type Int)
(define-typed-syntax #%datum #:literals (#%datum)
[(#%datum . n:integer) (⊢ #,(syntax/loc stx (#%datum- . n)) : Int)]
diff --git a/macrotypes/examples/stlc+occurrence.rkt b/macrotypes/examples/stlc+occurrence.rkt
@@ -1,6 +1,6 @@
#lang s-exp macrotypes/typecheck
(extends "stlc+sub.rkt" #:except #%datum)
-(extends "stlc+cons.rkt" #:except + #%datum and tup × proj ~× list)
+(extends "stlc+cons.rkt" #:except + * #%datum and tup × proj ~× list)
(reuse tup × proj #:from "stlc+tup.rkt")
(require (only-in "stlc+tup.rkt" ~×))
diff --git a/macrotypes/examples/stlc+reco+sub.rkt b/macrotypes/examples/stlc+reco+sub.rkt
@@ -1,6 +1,6 @@
#lang s-exp macrotypes/typecheck
(extends "stlc+sub.rkt" #:except #%datum)
-(extends "stlc+reco+var.rkt" #:except #%datum +)
+(extends "stlc+reco+var.rkt" #:except #%datum + *)
;; Simply-Typed Lambda Calculus, plus subtyping, plus records
;; Types:
diff --git a/macrotypes/examples/stlc+sub.rkt b/macrotypes/examples/stlc+sub.rkt
@@ -20,10 +20,10 @@
;; - also *
;; Other: sub? current-sub?
-(define-base-types Top Num Nat)
+(provide (typed-out [+ : (→ Num Num Num)]
+ [* : (→ Num Num Num)]))
-(define-primop + : (→ Num Num Num))
-(define-primop * : (→ Num Num Num))
+(define-base-types Top Num Nat)
(define-typed-syntax #%datum
[(#%datum . n:nat) (⊢ (#%datum- . n) : Nat)]
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
@@ -6,11 +6,16 @@
(postfix-in - racket/match)
(postfix-in - racket/promise)
(for-syntax (except-in racket extends)
- syntax/parse racket/syntax syntax/stx racket/stxparam syntax/parse/define
+ syntax/parse racket/syntax syntax/stx racket/stxparam
+ syntax/parse/define
+ (only-in racket/provide-transform
+ make-provide-pre-transformer pre-expand-export)
"stx-utils.rkt")
- (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
+ (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx
+ "stx-utils.rkt")
(for-meta 3 racket/base syntax/parse racket/syntax)
- racket/bool racket/provide racket/require racket/match racket/promise syntax/parse/define)
+ racket/bool racket/provide racket/require racket/match racket/promise
+ syntax/parse/define)
(provide
postfix-in
symbol=?- match- delay-
@@ -20,6 +25,7 @@
(rename-out [define-syntax-category define-stx-category])
(for-syntax
(all-from-out racket syntax/parse racket/syntax syntax/stx
+ racket/provide-transform
"stx-utils.rkt"))
(for-meta 2 (all-from-out racket/base syntax/parse racket/syntax)))
@@ -867,22 +873,32 @@
;; pre-declare all type-related functions and forms
(define-syntax-category type)
+(define-syntax typed-out
+ (make-provide-pre-transformer
+ (lambda (stx modes)
+ (syntax-parse stx #:datum-literals (:)
+ ;; cannot write ty:type bc provides might precede type def
+ [(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x #'out-x))
+ [[x:id (~optional :) ty] out-x:id])) ...)
+ #:with (x/tc ...) (generate-temporaries #'(x ...))
+ #:when (stx-map
+ syntax-local-lift-module-end-declaration
+ ;; use define-primop to validate type
+ #'((define-primop x/tc x ty) ...))
+ (pre-expand-export (syntax/loc stx (rename-out [x/tc out-x] ...))
+ modes)]))))
+
+;; colon is optional to make it easier to use define-primop in macros
(define-syntax define-primop
(syntax-parser #:datum-literals (:)
- [(define-primop op:id : τ #:no-provide)
- #:with op/tc (generate-temporary #'op)
- #'(define-primop op/tc op : τ)]
- [(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 op:id (~optional :) τ)
+ #:with op- (format-id #'op "~a-" #'op)
+ #'(define-primop op op- τ)]
+ [(define-primop op/tc:id (~optional #:as) op:id (~optional :) τ:type)
+ ; 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
diff --git a/turnstile/examples/ext-stlc.rkt b/turnstile/examples/ext-stlc.rkt
@@ -1,6 +1,5 @@
#lang turnstile/lang
(extends "stlc+lit.rkt" #:except #%datum)
-(provide ⊔ (for-syntax current-join))
;; Simply-Typed Lambda Calculus, plus extensions (TAPL ch11)
;; Types:
@@ -17,10 +16,21 @@
;; - ascription (ann)
;; - let, let*, letrec
-(define-base-type Bool)
-(define-base-type String)
-(define-base-type Float)
-(define-base-type Char)
+(provide (for-syntax current-join)
+ ⊔ zero? =
+ (rename-out [typed- -] [typed* *])
+ (typed-out [add1 (→ Int Int)]
+ [sub1 : (→ Int Int)]
+ [[not- (→ Bool Bool)] not]
+ [[void- : (→ Unit)] void]))
+
+(define-base-types Bool String Float Char Unit)
+
+;; test all variations of define-primop and typed-out
+(define-primop zero? (→ Int Bool))
+(define-primop = : (→ Int Int Bool))
+(define-primop typed- - (→ Int Int Int))
+(define-primop typed* * : (→ Int Int Int))
(define-typed-syntax #%datum
[(_ . b:boolean) ≫
@@ -40,14 +50,6 @@
--------
[≻ (stlc+lit:#%datum . x)]])
-(define-primop zero? : (→ Int Bool))
-(define-primop = : (→ Int Int Bool))
-(define-primop - : (→ Int Int Int))
-(define-primop * : (→ Int Int Int))
-(define-primop add1 : (→ Int Int))
-(define-primop sub1 : (→ Int Int))
-(define-primop not : (→ Bool Bool))
-
(define-typed-syntax (and e ...) ≫
[⊢ e ≫ e- ⇐ Bool] ...
--------
@@ -89,9 +91,6 @@
--------
[⊢ (if- e_tst- e1- e2-) ⇒ (⊔ τ1 τ2)]])
-(define-base-type Unit)
-(define-primop void : (→ Unit))
-
(define-typed-syntax begin
[(_ e_unit ... e) ⇐ τ_expected ≫
[⊢ e_unit ≫ e_unit- ⇒ _] ...
diff --git a/turnstile/examples/fsub.rkt b/turnstile/examples/fsub.rkt
@@ -14,7 +14,7 @@
;; - current-promote, expose
;; - extend current-sub? to call current-promote
-(define-primop + : (→ Nat Nat Nat))
+(provide (typed-out [+ : (→ Nat Nat Nat)]))
; can't just call expose in type-eval,
; otherwise typevars will have bound as type, rather than instantiated type
diff --git a/turnstile/examples/mlish+adhoc.rkt b/turnstile/examples/mlish+adhoc.rkt
@@ -782,25 +782,25 @@
#'(∀ Xs (=> TC ... (ext-stlc:→ . tys_arr)))]))
; redefine these to use lifted →
-(define-primop + : (→ Int Int Int))
-(define-primop - : (→ Int Int Int))
-(define-primop * : (→ Int Int Int))
-(define-primop max : (→ Int Int Int))
-(define-primop min : (→ Int Int Int))
-(define-primop void : (→ Unit))
-(define-primop = : (→ Int Int Bool))
-(define-primop <= : (→ Int Int Bool))
-(define-primop >= : (→ Int Int Bool))
-(define-primop < : (→ Int Int Bool))
-(define-primop > : (→ Int Int Bool))
-(define-primop modulo : (→ Int Int Int))
-(define-primop zero? : (→ Int Bool))
-(define-primop sub1 : (→ Int Int))
-(define-primop add1 : (→ Int Int))
-(define-primop not : (→ Bool Bool))
-(define-primop abs : (→ Int Int))
-(define-primop even? : (→ Int Bool))
-(define-primop odd? : (→ Int Bool))
+(provide (typed-out [+ : (→ Int Int Int)]
+ [- : (→ Int Int Int)]
+ [* : (→ Int Int Int)]
+ [max : (→ Int Int Int)]
+ [min : (→ Int Int Int)]
+ [void : (→ Unit)]
+ [= : (→ Int Int Bool)]
+ [<= : (→ Int Int Bool)]
+ [>= : (→ Int Int Bool)]
+ [< : (→ Int Int Bool)]
+ [> : (→ Int Int Bool)]
+ [modulo : (→ Int Int Int)]
+ [zero? : (→ Int Bool)]
+ [sub1 : (→ Int Int)]
+ [add1 : (→ Int Int)]
+ [not : (→ Bool Bool)]
+ [abs : (→ Int Int)]
+ [even? : (→ Int Bool)]
+ [odd? : (→ Int Bool)]))
;; λ --------------------------------------------------------------------------
@@ -1128,10 +1128,10 @@
--------
[⊢ (thread- th-) ⇒ Thread])
-(define-primop random : (→ Int Int))
-(define-primop integer->char : (→ Int Char))
-(define-primop string->list : (→ String (List Char)))
-(define-primop string->number : (→ String Int))
+(provide (typed-out [random : (→ Int Int)]
+ [integer->char : (→ Int Char)]
+ [string->list : (→ String (List Char))]
+ [string->number : (→ String Int)]))
(define-typed-syntax number->string
[_:id ≫
--------
@@ -1145,18 +1145,18 @@
--------
[⊢ (number->string- n rad) ⇒ String]])
-(define-primop string : (→ Char String))
-(define-primop sleep : (→ Int Unit))
-(define-primop string=? : (→ String String Bool))
-(define-primop string<? : (→ String String Bool))
-(define-primop string<=? : (→ String String Bool))
-(define-primop string>? : (→ String String Bool))
-(define-primop string>=? : (→ String String Bool))
-(define-primop char=? : (→ Char Char Bool))
-(define-primop char<? : (→ Char Char Bool))
-(define-primop char<=? : (→ Char Char Bool))
-(define-primop char>? : (→ Char Char Bool))
-(define-primop char>=? : (→ Char Char Bool))
+(provide (typed-out [string : (→ Char String)]
+ [sleep : (→ Int Unit)]
+ [string=? : (→ String String Bool)]
+ [string<? : (→ String String Bool)]
+ [string<=? : (→ String String Bool)]
+ [string>? : (→ String String Bool)]
+ [string>=? : (→ String String Bool)]
+ [char=? : (→ Char Char Bool)]
+ [char<? : (→ Char Char Bool)]
+ [char<=? : (→ Char Char Bool)]
+ [char>? : (→ Char Char Bool)]
+ [char>=? : (→ Char Char Bool)]))
(define-typed-syntax string-append
[(_ str ...) ≫
@@ -1344,7 +1344,7 @@
[⊢ e ≫ e- ⇒ _]
--------
[⊢ (displayln- e-) ⇒ Unit])
-(define-primop newline : (→ Unit))
+(provide (typed-out [newline : (→ Unit)]))
(define-typed-syntax list->vector
[(_ e) ⇐ (~Vector ty) ≫
@@ -1438,9 +1438,9 @@
(define-base-type String-Port)
(define-base-type Input-Port)
-(define-primop open-output-string : (→ String-Port))
-(define-primop get-output-string : (→ String-Port String))
-(define-primop string-upcase : (→ String String))
+(provide (typed-out [open-output-string : (→ String-Port)]
+ [get-output-string : (→ String-Port String)]
+ [string-upcase : (→ String String)]))
(define-typed-syntax write-string
[(_ str out) ≫
@@ -1458,9 +1458,9 @@
[⊢ str ≫ str- ⇐ String]
--------
[⊢ (string-length- str-) ⇒ Int])
-(define-primop make-string : (→ Int String))
-(define-primop string-set! : (→ String Int Char Unit))
-(define-primop string-ref : (→ String Int Char))
+(provide (typed-out [make-string : (→ Int String)]
+ [string-set! : (→ String Int Char Unit)]
+ [string-ref : (→ String Int Char)]))
(define-typed-syntax string-copy!
[(_ dest dest-start src) ≫
--------
@@ -1475,18 +1475,18 @@
--------
[⊢ (string-copy!- dest- dest-start- src- src-start- src-end-) ⇒ Unit]])
-(define-primop fl+ : (→ Float Float Float))
-(define-primop fl- : (→ Float Float Float))
-(define-primop fl* : (→ Float Float Float))
-(define-primop fl/ : (→ Float Float Float))
-(define-primop fl= : (→ Float Float Bool))
-(define-primop flsqrt : (→ Float Float))
-(define-primop flceiling : (→ Float Float))
-(define-primop inexact->exact : (→ Float Int))
-(define-primop exact->inexact : (→ Int Float))
-(define-primop char->integer : (→ Char Int))
-(define-primop real->decimal-string : (→ Float Int String))
-(define-primop fx->fl : (→ Int Float))
+(provide (typed-out [fl+ : (→ Float Float Float)]
+ [fl- : (→ Float Float Float)]
+ [fl* : (→ Float Float Float)]
+ [fl/ : (→ Float Float Float)]
+ [fl= : (→ Float Float Bool)]
+ [flsqrt : (→ Float Float)]
+ [flceiling : (→ Float Float)]
+ [inexact->exact : (→ Float Int)]
+ [exact->inexact : (→ Int Float)]
+ [char->integer : (→ Char Int)]
+ [real->decimal-string : (→ Float Int String)]
+ [fx->fl : (→ Int Float)]))
(define-typed-syntax (quotient+remainder x y) ≫
[⊢ x ≫ x- ⇐ Int]
[⊢ y ≫ y- ⇐ Int]
@@ -1494,7 +1494,7 @@
[⊢ (let-values- ([[a b] (quotient/remainder- x- y-)])
(list- a b))
⇒ (stlc+rec-iso:× Int Int)])
-(define-primop quotient : (→ Int Int Int))
+(provide (typed-out [quotient : (→ Int Int Int)]))
(define-typed-syntax (set! x:id e) ≫
[⊢ x ≫ x- ⇒ ty_x]
@@ -1506,15 +1506,16 @@
--------
[≻ (provide- ty ...)])
-(define-typed-syntax (provide x:id ...) ≫
- [⊢ x ≫ x- ⇒ ty_x] ...
- ; TODO: use hash-code to generate this tmp
- #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))
- --------
- [≻ (begin-
- (provide- x ...)
- (stlc+rec-iso:define-type-alias x-ty ty_x) ...
- (provide- x-ty ...))])
+(define-typed-syntax mlish-provide #:export-as provide
+ [(_ x:id ...) ≫
+ [⊢ x ≫ x- ⇒ ty_x] ...
+ ; TODO: use hash-code to generate this tmp
+ #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))
+ --------
+ [≻ (begin-
+ (provide- x ...)
+ (stlc+rec-iso:define-type-alias x-ty ty_x) ...
+ (provide- x-ty ...))]])
(define-typed-syntax (require-typed x:id ... #:from mod) ≫
#:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))
#:with (y ...) (generate-temporaries #'(x ...))
@@ -1524,8 +1525,8 @@
(define-syntax x (make-rename-transformer (assign-type #'y #'x-ty))) ...)])
(define-base-type Regexp)
-(define-primop regexp-match : (→ Regexp String (List String)))
-(define-primop regexp : (→ String Regexp))
+(provide (typed-out [regexp-match : (→ Regexp String (List String))]
+ [regexp : (→ String Regexp)]))
(define-typed-syntax (equal? e1 e2) ≫
[⊢ e1 ≫ e1- ⇒ ty1]
diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt
@@ -809,24 +809,24 @@
#'(?∀ Xs (ext-stlc:→ . rst))]))
; redefine these to use lifted →
-(define-primop + : (→ Int Int Int))
-(define-primop - : (→ Int Int Int))
-(define-primop * : (→ Int Int Int))
-(define-primop max : (→ Int Int Int))
-(define-primop min : (→ Int Int Int))
-(define-primop void : (→ Unit))
-(define-primop = : (→ Int Int Bool))
-(define-primop <= : (→ Int Int Bool))
-(define-primop < : (→ Int Int Bool))
-(define-primop > : (→ Int Int Bool))
-(define-primop modulo : (→ Int Int Int))
-(define-primop zero? : (→ Int Bool))
-(define-primop sub1 : (→ Int Int))
-(define-primop add1 : (→ Int Int))
-(define-primop not : (→ Bool Bool))
-(define-primop abs : (→ Int Int))
-(define-primop even? : (→ Int Bool))
-(define-primop odd? : (→ Int Bool))
+(provide (typed-out [+ : (→ Int Int Int)]
+ [- : (→ Int Int Int)]
+ [* : (→ Int Int Int)]
+ [max : (→ Int Int Int)]
+ [min : (→ Int Int Int)]
+ [void : (→ Unit)]
+ [= : (→ Int Int Bool)]
+ [<= : (→ Int Int Bool)]
+ [< : (→ Int Int Bool)]
+ [> : (→ Int Int Bool)]
+ [modulo : (→ Int Int Int)]
+ [zero? : (→ Int Bool)]
+ [sub1 : (→ Int Int)]
+ [add1 : (→ Int Int)]
+ [not : (→ Bool Bool)]
+ [abs : (→ Int Int)]
+ [even? : (→ Int Bool)]
+ [odd? : (→ Int Bool)]))
; all λs have type (?∀ (X ...) (→ τ_in ... τ_out))
(define-typed-syntax λ #:datum-literals (:)
@@ -951,11 +951,10 @@
--------
[⊢ [_ ≫ (thread- th-) ⇒ : Thread]]])
-(define-primop random : (→ Int Int))
-(define-primop integer->char : (→ Int Char))
-(define-primop string->list : (→ String (List Char)))
-(define-primop string->number : (→ String Int))
-;(define-primop number->string : (→ Int String))
+(provide (typed-out [random : (→ Int Int)]
+ [integer->char : (→ Int Char)]
+ [string->list : (→ String (List Char))]
+ [string->number : (→ String Int)]))
(define-typed-syntax number->string
[number->string:id ≫
--------
@@ -968,10 +967,10 @@
[⊢ [rad ≫ rad- ⇐ : Int]]
--------
[⊢ [_ ≫ (number->string- n rad) ⇒ : String]]])
-(define-primop string : (→ Char String))
-(define-primop sleep : (→ Int Unit))
-(define-primop string=? : (→ String String Bool))
-(define-primop string<=? : (→ String String Bool))
+(provide (typed-out [string : (→ Char String)]
+ [sleep : (→ Int Unit)]
+ [string=? : (→ String String Bool)]
+ [string<=? : (→ String String Bool)]))
(define-typed-syntax string-append
[(string-append str ...) ≫
@@ -1182,7 +1181,7 @@
[⊢ [e ≫ e- ⇒ : _]]
--------
[⊢ [_ ≫ (displayln- e-) ⇒ : Unit]]])
-(define-primop newline : (→ Unit))
+(provide (typed-out [newline : (→ Unit)]))
(define-typed-syntax list->vector
[(list->vector e) ⇐ : (~Vector ty) ≫
@@ -1281,9 +1280,9 @@
(define-base-type String-Port)
(define-base-type Input-Port)
-(define-primop open-output-string : (→ String-Port))
-(define-primop get-output-string : (→ String-Port String))
-(define-primop string-upcase : (→ String String))
+(provide (typed-out [open-output-string : (→ String-Port)]
+ [get-output-string : (→ String-Port String)]
+ [string-upcase : (→ String String)]))
(define-typed-syntax write-string
[(write-string str out) ≫
@@ -1302,9 +1301,9 @@
[⊢ [str ≫ str- ⇐ : String]]
--------
[⊢ [_ ≫ (string-length- str-) ⇒ : Int]]])
-(define-primop make-string : (→ Int String))
-(define-primop string-set! : (→ String Int Char Unit))
-(define-primop string-ref : (→ String Int Char))
+(provide (typed-out [make-string : (→ Int String)]
+ [string-set! : (→ String Int Char Unit)]
+ [string-ref : (→ String Int Char)]))
(define-typed-syntax string-copy!
[(string-copy! dest dest-start src) ≫
--------
@@ -1319,17 +1318,17 @@
--------
[⊢ [_ ≫ (string-copy!- dest- dest-start- src- src-start- src-end-) ⇒ : Unit]]])
-(define-primop fl+ : (→ Float Float Float))
-(define-primop fl- : (→ Float Float Float))
-(define-primop fl* : (→ Float Float Float))
-(define-primop fl/ : (→ Float Float Float))
-(define-primop flsqrt : (→ Float Float))
-(define-primop flceiling : (→ Float Float))
-(define-primop inexact->exact : (→ Float Int))
-(define-primop exact->inexact : (→ Int Float))
-(define-primop char->integer : (→ Char Int))
-(define-primop real->decimal-string : (→ Float Int String))
-(define-primop fx->fl : (→ Int Float))
+(provide (typed-out [fl+ : (→ Float Float Float)]
+ [fl- : (→ Float Float Float)]
+ [fl* : (→ Float Float Float)]
+ [fl/ : (→ Float Float Float)]
+ [flsqrt : (→ Float Float)]
+ [flceiling : (→ Float Float)]
+ [inexact->exact : (→ Float Int)]
+ [exact->inexact : (→ Int Float)]
+ [char->integer : (→ Char Int)]
+ [real->decimal-string : (→ Float Int String)]
+ [fx->fl : (→ Int Float)]))
(define-typed-syntax quotient+remainder
[(quotient+remainder x y) ≫
[⊢ [x ≫ x- ⇐ : Int]]
@@ -1338,7 +1337,7 @@
[⊢ [_ ≫ (let-values- ([[a b] (quotient/remainder- x- y-)])
(list- a b))
⇒ : (stlc+rec-iso:× Int Int)]]])
-(define-primop quotient : (→ Int Int Int))
+(provide (typed-out [quotient : (→ Int Int Int)]))
(define-typed-syntax set!
[(set! x:id e) ≫
@@ -1352,7 +1351,7 @@
--------
[_ ≻ (provide- ty ...)]])
-(define-typed-syntax provide
+(define-typed-syntax mlish-provide #:export-as provide
[(provide x:id ...) ≫
[⊢ [x ≫ x- ⇒ : ty_x] ...]
; TODO: use hash-code to generate this tmp
@@ -1372,8 +1371,8 @@
(define-syntax x (make-rename-transformer (assign-type #'y #'x-ty))) ...)]])
(define-base-type Regexp)
-(define-primop regexp-match : (→ Regexp String (List String)))
-(define-primop regexp : (→ String Regexp))
+(provide (typed-out [regexp-match : (→ Regexp String (List String))]
+ [regexp : (→ String Regexp)]))
(define-typed-syntax equal?
[(equal? e1 e2) ≫
diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
@@ -21,25 +21,26 @@
--------
[⊢ [_ ≫ (bv:BV e-) ⇒ : CUnit]]])
-(define-primop bv : (Ccase-> (C→ CInt CBV)
- (C→ CInt CBVPred CBV)
- (C→ CInt CPosInt CBV)))
-(define-primop bv* : (Ccase-> (C→ BV)
- (C→ CBVPred BV)))
-
+(provide (typed-out [bv : (Ccase-> (C→ CInt CBV)
+ (C→ CInt CBVPred CBV)
+ (C→ CInt CPosInt CBV))]
+ [bv* : (Ccase-> (C→ BV)
+ (C→ CBVPred BV))]
+ [bvredor : (C→ BV BV)]
+ [bvredand : (C→ BV BV)]))
(define-syntax-rule (bv:bool->bv b)
(ro:if b
(bv (rosette2:#%datum . 1))
(bv (rosette2:#%datum . 0))))
-(define-primop bvredor : (C→ BV BV))
-(define-primop bvredand : (C→ BV BV))
(define-simple-macro (define-comparators id ...)
#:with (op ...) (stx-map (lambda (o) (format-id o "ro:~a" o)) #'(id ...))
+ #:with (id/tc ...) (generate-temporaries #'(id ...))
(begin-
(define- (id x y) (bv:bool->bv (ro:#%app op x y))) ...
- (define-primop id : (C→ BV BV BV)) ...))
+ (provide (rename-out [id/tc id] ...))
+ (define-primop id/tc id (C→ BV BV BV)) ...))
(define-comparators bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge)
diff --git a/turnstile/examples/rosette/fsm.rkt b/turnstile/examples/rosette/fsm.rkt
@@ -47,11 +47,11 @@
[⊢ [_ ≫ (fsm:automaton init-state-
[state- : (label arr target-) ...] ...) ⇒ : FSM]]])
-(define-primop reject : State)
+(provide (typed-out [reject : State]
+ [verify-automaton : (→ FSM Regexp (List Symbol))]
+ [debug-automaton : (→ FSM Regexp (List Symbol) Pict)]
+ [synthesize-automaton : (→ FSM Regexp Unit)]))
;; (define (apply-FSM f v) (f v))
;; (define-primop apply-FSM : (→ FSM (List Symbol) Bool))
-(define-primop verify-automaton : (→ FSM Regexp (List Symbol)))
-(define-primop debug-automaton : (→ FSM Regexp (List Symbol) Pict))
-(define-primop synthesize-automaton : (→ FSM Regexp Unit))
diff --git a/turnstile/examples/rosette/ifc.rkt b/turnstile/examples/rosette/ifc.rkt
@@ -11,23 +11,31 @@
(define-base-types Prog Instr Machine Witness)
-(define-primop Halt : Instr)
-(define-primop Noop : Instr)
-(define-primop Push : Instr)
-(define-primop Pop : Instr)
-(define-primop Load* : Instr)
-(define-primop Store*AB : Instr)
-(define-primop Store*B : Instr)
-(define-primop Add* : Instr)
-(define-primop Load : Instr)
-(define-primop Store : Instr)
-(define-primop Add : Instr)
+(provide (typed-out [Halt : Instr]
+ [Noop : Instr]
+ [Push : Instr]
+ [Pop : Instr]
+ [Load* : Instr]
+ [Store*AB : Instr]
+ [Store*B : Instr]
+ [Add* : Instr]
+ [Load : Instr]
+ [Store : Instr]
+ [Add : Instr]
-(define-primop init : (→ Prog Machine))
-(define-primop halted? : (→ Machine Bool))
-(define-primop mem≈ : (→ Machine Machine Bool))
+ [init : (→ Prog Machine)]
+ [halted? : (→ Machine Bool)]
+ [mem≈ : (→ Machine Machine Bool)]
+
+ [program : (→ Int (List Instr) Prog)]
+
+ [verify-EENI* : (→ (→ Prog Machine)
+ (→ Machine Bool)
+ (→ Machine Machine Bool)
+ Prog Bool
+ Witness)]
+ [EENI-witness? : (→ Witness Bool)]))
-(define-primop program : (→ Int (List Instr) Prog))
#;(define-typed-syntax program
[(_ n procs) ≫
[⊢ [n ≫ n- ⇐ : Int]]
@@ -35,9 +43,3 @@
--------
[⊢ [_ ≫ (ifc:program n- procs-) ⇒ : Prog]]])
-(define-primop verify-EENI* : (→ (→ Prog Machine)
- (→ Machine Bool)
- (→ Machine Machine Bool)
- Prog Bool
- Witness))
-(define-primop EENI-witness? : (→ Witness Bool))
diff --git a/turnstile/examples/rosette/lib/synthax.rkt b/turnstile/examples/rosette/lib/synthax.rkt
@@ -1,9 +1,10 @@
#lang turnstile
(require
+ (only-in "../rosette2.rkt" rosette-typed-out)
(prefix-in t/ro: (only-in "../rosette2.rkt" Int Bool C→ CSolution Unit))
(prefix-in ro: rosette/lib/synthax))
-(provide print-forms)
+(provide (rosette-typed-out [print-forms : (t/ro:C→ t/ro:CSolution t/ro:Unit)]))
(define-typed-syntax ??
[(qq) ≫
@@ -15,7 +16,3 @@
[⊢ [pred ≫ pred- ⇐ : (t/ro:C→ ty.norm t/ro:Bool)]]
--------
[⊢ [_ ≫ (??/progsrc pred-) ⇒ : ty.norm]]])
-
-(define-syntax print-forms
- (make-variable-like-transformer
- (assign-type #'ro:print-forms #'(t/ro:C→ t/ro:CSolution t/ro:Unit))))
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
@@ -7,14 +7,18 @@
(require (prefix-in ro: rosette/lib/synthax))
(provide BVPred (rename-out [ro:#%module-begin #%module-begin]))
-(define-simple-macro (define-rosette-primop op:id : ty)
- (begin
- (require (only-in rosette [op op]))
- (define-primop op : ty)))
-(define-simple-macro (define-rosette-primop* op1:id op2:id : ty)
- (begin
- (require (only-in rosette [op1 op2]))
- (define-primop op2 : ty)))
+(define-for-syntax (mk-ro:-id id) (format-id id "ro:~a" id))
+
+(define-syntax rosette-typed-out
+ (make-provide-pre-transformer
+ (lambda (stx modes)
+ (syntax-parse stx #:datum-literals (:)
+ ;; cannot write ty:type bc provides might precede type def
+ [(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x #'out-x))
+ [[x:id (~optional :) ty] out-x:id])) ...)
+ #:with (ro-x ...) (stx-map mk-ro:-id #'(x ...))
+ (pre-expand-export (syntax/loc stx (typed-out [[ro-x ty] out-x] ...))
+ modes)]))))
;; ----------------------------------------------------------------------------
;; Rosette stuff
@@ -92,24 +96,24 @@
(define-type-constructor Param #:arity = 1)
-(define-rosette-primop boolean? : (→ Bool Bool))
-(define-rosette-primop integer? : (→ Int Bool))
-(define-rosette-primop string? : (→ String Bool))
-(define-rosette-primop pregexp : (→ String Regexp))
+(provide (rosette-typed-out [boolean? : (→ Bool Bool)]
+ [integer? : (→ Int Bool)]
+ [string? : (→ String Bool)]
+ [pregexp : (→ String Regexp)]
-(define-rosette-primop add1 : (case-> (→ NegInt (U NegInt Zero))
- (→ Zero PosInt)
- (→ PosInt PosInt)
- (→ Nat PosInt)
- (→ Int Int)))
-(define-rosette-primop sub1 : (case-> (→ NegInt NegInt)
- (→ Zero NegInt)
- (→ PosInt Nat)
- (→ Nat Int)
- (→ Int Int)))
-(define-rosette-primop + : (case-> (→ Nat Nat Nat)
- (→ Int Int Int)
- (→ Num Num Num)))
+ [add1 : (case-> (→ NegInt (U NegInt Zero))
+ (→ Zero PosInt)
+ (→ PosInt PosInt)
+ (→ Nat PosInt)
+ (→ Int Int))]
+ [sub1 : (case-> (→ NegInt NegInt)
+ (→ Zero NegInt)
+ (→ PosInt Nat)
+ (→ Nat Int)
+ (→ Int Int))]
+ [+ : (case-> (→ Nat Nat Nat)
+ (→ Int Int Int)
+ (→ Num Num Num))]))
(define-typed-syntax equal?
[(equal? e1 e2) ≫
@@ -168,29 +172,25 @@
(define-named-type-alias BVPred (→ BV Bool))
;; support higher order case with case-> types
-(define-rosette-primop bv : (case-> (→ Int BVPred BV)
- (→ Int PosInt BV)))
-
-(define-rosette-primop bv? : (→ BV Bool))
-(define-rosette-primop bitvector : (→ PosInt BVPred))
-(define-rosette-primop bitvector? : (→ BVPred Bool))
-(define-rosette-primop* bitvector bvpred : (→ PosInt BVPred))
-(define-rosette-primop* bitvector? bvpred? : (→ BVPred Bool))
-(define-rosette-primop bitvector-size : (→ BVPred PosInt))
-(define-rosette-primop* bitvector-size bvpred-size : (→ BVPred PosInt))
-
-(define-rosette-primop bveq : (→ BV BV Bool))
-(define-rosette-primop bvslt : (→ BV BV Bool))
-(define-rosette-primop bvult : (→ BV BV Bool))
-(define-rosette-primop bvsle : (→ BV BV Bool))
-(define-rosette-primop bvule : (→ BV BV Bool))
-(define-rosette-primop bvsgt : (→ BV BV Bool))
-(define-rosette-primop bvugt : (→ BV BV Bool))
-(define-rosette-primop bvsge : (→ BV BV Bool))
-(define-rosette-primop bvuge : (→ BV BV Bool))
-
-(define-rosette-primop bvnot : (→ BV BV))
-
+(provide (rosette-typed-out [bv : (case-> (→ Int BVPred BV)
+ (→ Int PosInt BV))]
+ [bv? : (→ BV Bool)]
+ [bitvector : (→ PosInt BVPred)]
+ [bitvector? : (→ BVPred Bool)]
+ [[bitvector : (→ PosInt BVPred)] bvpred]
+ [[bitvector? : (→ BVPred Bool)] bvpred?]
+ [bitvector-size : (→ BVPred PosInt)]
+ [[bitvector-size : (→ BVPred PosInt)] bvpred-size]
+ [bveq : (→ BV BV Bool)]
+ [bvslt : (→ BV BV Bool)]
+ [bvult : (→ BV BV Bool)]
+ [bvsle : (→ BV BV Bool)]
+ [bvule : (→ BV BV Bool)]
+ [bvsgt : (→ BV BV Bool)]
+ [bvugt : (→ BV BV Bool)]
+ [bvsge : (→ BV BV Bool)]
+ [bvuge : (→ BV BV Bool)]
+ [bvnot : (→ BV BV)]))
(define-typed-syntax bvand
[f:id ≫ ; TODO: implement variable arity types
@@ -217,10 +217,10 @@
--------
[⊢ [_ ≫ (ro:bvxor e- ...) ⇒ : BV]]])
-(define-rosette-primop bvshl : (→ BV BV BV))
-(define-rosette-primop bvlshr : (→ BV BV BV))
-(define-rosette-primop bvashr : (→ BV BV BV))
-(define-rosette-primop bvneg : (→ BV BV))
+(provide (rosette-typed-out [bvshl : (→ BV BV BV)]
+ [bvlshr : (→ BV BV BV)]
+ [bvashr : (→ BV BV BV)]
+ [bvneg : (→ BV BV)]))
(define-typed-syntax bvadd
[f:id ≫ ; TODO: implement variable arity types
@@ -247,11 +247,11 @@
--------
[⊢ [_ ≫ (ro:bvmul e- ...) ⇒ : BV]]])
-(define-rosette-primop bvsdiv : (→ BV BV BV))
-(define-rosette-primop bvudiv : (→ BV BV BV))
-(define-rosette-primop bvsrem : (→ BV BV BV))
-(define-rosette-primop bvurem : (→ BV BV BV))
-(define-rosette-primop bvsmod : (→ BV BV BV))
+(provide (rosette-typed-out [bvsdiv : (→ BV BV BV)]
+ [bvudiv : (→ BV BV BV)]
+ [bvsrem : (→ BV BV BV)]
+ [bvurem : (→ BV BV BV)]
+ [bvsmod : (→ BV BV BV)]))
(define-typed-syntax concat
[(_ e ...+) ≫
@@ -259,11 +259,10 @@
--------
[⊢ [_ ≫ (ro:concat e- ...) ⇒ : BV]]])
-(define-rosette-primop extract : (→ Int Int BV BV))
-;; TODO: additionally support union in 2nd arg
-(define-rosette-primop sign-extend : (→ BV BVPred BV))
-(define-rosette-primop zero-extend : (→ BV BVPred BV))
-
-(define-rosette-primop bitvector->integer : (→ BV Int))
-(define-rosette-primop bitvector->natural : (→ BV Int))
-(define-rosette-primop integer->bitvector : (→ Int BVPred BV))
+(provide (rosette-typed-out [extract : (→ Int Int BV BV)]
+ ;; TODO: support union in 2nd arg
+ [sign-extend : (→ BV BVPred BV)]
+ [zero-extend : (→ BV BVPred BV)]
+ [bitvector->integer : (→ BV Int)]
+ [bitvector->natural : (→ BV Int)]
+ [integer->bitvector : (→ Int BVPred BV)]))
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -42,10 +42,19 @@
(rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?]))
;; copied from rosette.rkt
-(define-simple-macro (define-rosette-primop op:id : ty)
- (begin-
- (require (only-in rosette [op op]))
- (define-primop op : ty)))
+(provide rosette-typed-out)
+(define-for-syntax (mk-ro:-id id) (format-id id "ro:~a" id))
+
+(define-syntax rosette-typed-out
+ (make-provide-pre-transformer
+ (lambda (stx modes)
+ (syntax-parse stx #:datum-literals (:)
+ ;; cannot write ty:type bc provides might precede type def
+ [(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x #'out-x))
+ [[x:id (~optional :) ty] out-x:id])) ...)
+ #:with (ro-x ...) (stx-map mk-ro:-id #'(x ...))
+ (pre-expand-export (syntax/loc stx (typed-out [[ro-x ty] out-x] ...))
+ modes)]))))
;; ---------------------------------
;; Concrete and Symbolic union types
@@ -397,113 +406,110 @@
#'(CIVectorof (CU τ ...))
#'(CIVectorof (U τ ...)))]]])
;; ---------------------------------
-;; IO
-
-(define-rosette-primop printf : (Ccase-> (C→ CString CUnit)
- (C→ CString Any CUnit)
- (C→ CString Any Any CUnit)))
-(define-rosette-primop error : (C→ (CU CString CSymbol) Nothing))
-(define-rosette-primop void : (C→ CUnit))
-
-;; ---------------------------------
-;; Types for built-in operations
-
-(define-rosette-primop equal? : (C→ Any Any Bool))
-(define-rosette-primop eq? : (C→ Any Any Bool))
-
-(define-rosette-primop pi : CNum)
-
-(define-rosette-primop add1 : (Ccase-> (C→ CNegInt (CU CNegInt CZero))
- (C→ NegInt (U NegInt Zero))
- (C→ CZero CPosInt)
- (C→ Zero PosInt)
- (C→ CPosInt CPosInt)
- (C→ PosInt PosInt)
- (C→ CNat CPosInt)
- (C→ Nat PosInt)
- (C→ CInt CInt)
- (C→ Int Int)))
-(define-rosette-primop sub1 : (Ccase-> (C→ CNegInt CNegInt)
- (C→ NegInt NegInt)
- (C→ CZero CNegInt)
- (C→ Zero NegInt)
- (C→ CPosInt CNat)
- (C→ PosInt Nat)
- (C→ CNat CInt)
- (C→ Nat Int)
- (C→ CInt CInt)
- (C→ Int Int)))
-(define-rosette-primop + : (Ccase-> (C→ CNat CNat CNat)
- (C→ CNat CNat CNat CNat)
- (C→ CNat CNat CNat CNat CNat)
- (C→ Nat Nat Nat)
- (C→ Nat Nat Nat Nat)
- (C→ Nat Nat Nat Nat Nat)
- (C→ CInt CInt CInt)
- (C→ CInt CInt CInt CInt)
- (C→ CInt CInt CInt CInt CInt)
- (C→ Int Int Int)
- (C→ Int Int Int Int)
- (C→ Int Int Int Int Int)
- (C→ CNum CNum CNum)
- (C→ CNum CNum CNum CNum)
- (C→ CNum CNum CNum CNum CNum)
- (C→ Num Num Num)
- (C→ Num Num Num Num)
- (C→ Num Num Num Num Num)))
-(define-rosette-primop * : (Ccase-> (C→ CNat CNat CNat)
- (C→ CNat CNat CNat CNat)
- (C→ CNat CNat CNat CNat CNat)
- (C→ Nat Nat Nat)
- (C→ Nat Nat Nat Nat)
- (C→ Nat Nat Nat Nat Nat)
- (C→ CInt CInt CInt)
- (C→ CInt CInt CInt CInt)
- (C→ CInt CInt CInt CInt CInt)
- (C→ Int Int Int)
- (C→ Int Int Int Int)
- (C→ Int Int Int Int Int)
- (C→ CNum CNum CNum)
- (C→ CNum CNum CNum CNum)
- (C→ CNum CNum CNum CNum CNum)
- (C→ Num Num Num)
- (C→ Num Num Num Num)
- (C→ Num Num Num Num Num)))
-(define-rosette-primop = : (Ccase-> (C→ CNum CNum CBool)
- (C→ Num Num Bool)))
-(define-rosette-primop < : (Ccase-> (C→ CNum CNum CBool)
- (C→ Num Num Bool)))
-(define-rosette-primop > : (Ccase-> (C→ CNum CNum CBool)
- (C→ Num Num Bool)))
-(define-rosette-primop <= : (Ccase-> (C→ CNum CNum CBool)
- (C→ Num Num Bool)))
-(define-rosette-primop >= : (Ccase-> (C→ CNum CNum CBool)
- (C→ Num Num Bool)))
-
-(define-rosette-primop abs : (Ccase-> (C→ CPosInt CPosInt)
- (C→ PosInt PosInt)
- (C→ CZero CZero)
- (C→ Zero Zero)
- (C→ CNegInt CPosInt)
- (C→ NegInt PosInt)
- (C→ CInt CInt)
- (C→ Int Int)
- (C→ CNum CNum)
- (C→ Num Num)))
-
-(define-rosette-primop not : (C→ Any Bool))
-(define-rosette-primop false? : (C→ Any Bool))
-
-;; TODO: fix types of these predicates
-(define-rosette-primop boolean? : (C→ Any Bool))
-(define-rosette-primop integer? : (C→ Any Bool))
-(define-rosette-primop real? : (C→ Any Bool))
-(define-rosette-primop positive? : (Ccase-> (C→ CNum CBool)
- (C→ Num Bool)))
-
-;; rosette-specific
-(define-rosette-primop asserts : (C→ (CListof Bool)))
-(define-rosette-primop clear-asserts! : (C→ CUnit))
+;; IO and other built-in ops
+
+(provide (rosette-typed-out [printf : (Ccase-> (C→ CString CUnit)
+ (C→ CString Any CUnit)
+ (C→ CString Any Any CUnit))]
+ [error : (C→ (CU CString CSymbol) Nothing)]
+ [void : (C→ CUnit)]
+
+ [equal? : (C→ Any Any Bool)]
+ [eq? : (C→ Any Any Bool)]
+
+ [pi : CNum]
+
+ [add1 : (Ccase-> (C→ CNegInt (CU CNegInt CZero))
+ (C→ NegInt (U NegInt Zero))
+ (C→ CZero CPosInt)
+ (C→ Zero PosInt)
+ (C→ CPosInt CPosInt)
+ (C→ PosInt PosInt)
+ (C→ CNat CPosInt)
+ (C→ Nat PosInt)
+ (C→ CInt CInt)
+ (C→ Int Int))]
+ [sub1 : (Ccase-> (C→ CNegInt CNegInt)
+ (C→ NegInt NegInt)
+ (C→ CZero CNegInt)
+ (C→ Zero NegInt)
+ (C→ CPosInt CNat)
+ (C→ PosInt Nat)
+ (C→ CNat CInt)
+ (C→ Nat Int)
+ (C→ CInt CInt)
+ (C→ Int Int))]
+ [+ : (Ccase-> (C→ CNat CNat CNat)
+ (C→ CNat CNat CNat CNat)
+ (C→ CNat CNat CNat CNat CNat)
+ (C→ Nat Nat Nat)
+ (C→ Nat Nat Nat Nat)
+ (C→ Nat Nat Nat Nat Nat)
+ (C→ CInt CInt CInt)
+ (C→ CInt CInt CInt CInt)
+ (C→ CInt CInt CInt CInt CInt)
+ (C→ Int Int Int)
+ (C→ Int Int Int Int)
+ (C→ Int Int Int Int Int)
+ (C→ CNum CNum CNum)
+ (C→ CNum CNum CNum CNum)
+ (C→ CNum CNum CNum CNum CNum)
+ (C→ Num Num Num)
+ (C→ Num Num Num Num)
+ (C→ Num Num Num Num Num))]
+ [* : (Ccase-> (C→ CNat CNat CNat)
+ (C→ CNat CNat CNat CNat)
+ (C→ CNat CNat CNat CNat CNat)
+ (C→ Nat Nat Nat)
+ (C→ Nat Nat Nat Nat)
+ (C→ Nat Nat Nat Nat Nat)
+ (C→ CInt CInt CInt)
+ (C→ CInt CInt CInt CInt)
+ (C→ CInt CInt CInt CInt CInt)
+ (C→ Int Int Int)
+ (C→ Int Int Int Int)
+ (C→ Int Int Int Int Int)
+ (C→ CNum CNum CNum)
+ (C→ CNum CNum CNum CNum)
+ (C→ CNum CNum CNum CNum CNum)
+ (C→ Num Num Num)
+ (C→ Num Num Num Num)
+ (C→ Num Num Num Num Num))]
+ [= : (Ccase-> (C→ CNum CNum CBool)
+ (C→ Num Num Bool))]
+ [< : (Ccase-> (C→ CNum CNum CBool)
+ (C→ Num Num Bool))]
+ [> : (Ccase-> (C→ CNum CNum CBool)
+ (C→ Num Num Bool))]
+ [<= : (Ccase-> (C→ CNum CNum CBool)
+ (C→ Num Num Bool))]
+ [>= : (Ccase-> (C→ CNum CNum CBool)
+ (C→ Num Num Bool))]
+
+ [abs : (Ccase-> (C→ CPosInt CPosInt)
+ (C→ PosInt PosInt)
+ (C→ CZero CZero)
+ (C→ Zero Zero)
+ (C→ CNegInt CPosInt)
+ (C→ NegInt PosInt)
+ (C→ CInt CInt)
+ (C→ Int Int)
+ (C→ CNum CNum)
+ (C→ Num Num))]
+
+ [not : (C→ Any Bool)]
+ [false? : (C→ Any Bool)]
+
+ ;; TODO: fix types of these predicates
+ [boolean? : (C→ Any Bool)]
+ [integer? : (C→ Any Bool)]
+ [real? : (C→ Any Bool)]
+ [positive? : (Ccase-> (C→ CNum CBool)
+ (C→ Num Bool))]
+
+ ;; rosette-specific
+ [asserts : (C→ (CListof Bool))]
+ [clear-asserts! : (C→ CUnit)]))
;; ---------------------------------
;; BV Types and Operations
@@ -522,63 +528,63 @@
--------
[⊢ [_ ≫ (ro:current-bitwidth e-) ⇒ : CUnit]]])
-(define-named-type-alias BV (add-predm (U CBV) bv?))
+(define-named-type-alias BV (add-predm (U CBV) ro:bv?))
(define-symbolic-named-type-alias BVPred (C→ BV Bool) #:pred lifted-bitvector?)
-(define-rosette-primop bv : (Ccase-> (C→ CInt CBVPred CBV)
- (C→ CInt CPosInt CBV)))
-(define-rosette-primop bv? : (C→ Any Bool))
-(define-rosette-primop bitvector : (C→ CPosInt CBVPred))
-(define-rosette-primop bitvector? : (C→ Any Bool))
+(provide (rosette-typed-out [bv : (Ccase-> (C→ CInt CBVPred CBV)
+ (C→ CInt CPosInt CBV))]
+ [bv? : (C→ Any Bool)]
+ [bitvector : (C→ CPosInt CBVPred)]
+ [bitvector? : (C→ Any Bool)]
-(define-rosette-primop bveq : (C→ BV BV Bool))
-(define-rosette-primop bvslt : (C→ BV BV Bool))
-(define-rosette-primop bvult : (C→ BV BV Bool))
-(define-rosette-primop bvsle : (C→ BV BV Bool))
-(define-rosette-primop bvule : (C→ BV BV Bool))
-(define-rosette-primop bvsgt : (C→ BV BV Bool))
-(define-rosette-primop bvugt : (C→ BV BV Bool))
-(define-rosette-primop bvsge : (C→ BV BV Bool))
-(define-rosette-primop bvuge : (C→ BV BV Bool))
+ [bveq : (C→ BV BV Bool)]
+ [bvslt : (C→ BV BV Bool)]
+ [bvult : (C→ BV BV Bool)]
+ [bvsle : (C→ BV BV Bool)]
+ [bvule : (C→ BV BV Bool)]
+ [bvsgt : (C→ BV BV Bool)]
+ [bvugt : (C→ BV BV Bool)]
+ [bvsge : (C→ BV BV Bool)]
+ [bvuge : (C→ BV BV Bool)]
-(define-rosette-primop bvnot : (C→ BV BV))
+ [bvnot : (C→ BV BV)]
-(define-rosette-primop bvand : (C→ BV BV BV))
-(define-rosette-primop bvor : (C→ BV BV BV))
-(define-rosette-primop bvxor : (C→ BV BV BV))
+ [bvand : (C→ BV BV BV)]
+ [bvor : (C→ BV BV BV)]
+ [bvxor : (C→ BV BV BV)]
-(define-rosette-primop bvshl : (C→ BV BV BV))
-(define-rosette-primop bvlshr : (C→ BV BV BV))
-(define-rosette-primop bvashr : (C→ BV BV BV))
-(define-rosette-primop bvneg : (C→ BV BV))
+ [bvshl : (C→ BV BV BV)]
+ [bvlshr : (C→ BV BV BV)]
+ [bvashr : (C→ BV BV BV)]
+ [bvneg : (C→ BV BV)]
-(define-rosette-primop bvadd : (C→ BV BV BV))
-(define-rosette-primop bvsub : (C→ BV BV BV))
-(define-rosette-primop bvmul : (C→ BV BV BV))
+ [bvadd : (C→ BV BV BV)]
+ [bvsub : (C→ BV BV BV)]
+ [bvmul : (C→ BV BV BV)]
-(define-rosette-primop bvsdiv : (C→ BV BV BV))
-(define-rosette-primop bvudiv : (C→ BV BV BV))
-(define-rosette-primop bvsrem : (C→ BV BV BV))
-(define-rosette-primop bvurem : (C→ BV BV BV))
-(define-rosette-primop bvsmod : (C→ BV BV BV))
+ [bvsdiv : (C→ BV BV BV)]
+ [bvudiv : (C→ BV BV BV)]
+ [bvsrem : (C→ BV BV BV)]
+ [bvurem : (C→ BV BV BV)]
+ [bvsmod : (C→ BV BV BV)]
-(define-rosette-primop concat : (C→ BV BV BV))
-(define-rosette-primop extract : (C→ Int Int BV BV))
-(define-rosette-primop sign-extend : (C→ BV CBVPred BV))
-(define-rosette-primop zero-extend : (C→ BV BVPred BV))
+ [concat : (C→ BV BV BV)]
+ [extract : (C→ Int Int BV BV)]
+ [sign-extend : (C→ BV CBVPred BV)]
+ [zero-extend : (C→ BV BVPred BV)]
-(define-rosette-primop bitvector->integer : (C→ BV Int))
-(define-rosette-primop bitvector->natural : (C→ BV Nat))
-(define-rosette-primop integer->bitvector : (C→ Int BVPred BV))
+ [bitvector->integer : (C→ BV Int)]
+ [bitvector->natural : (C→ BV Nat)]
+ [integer->bitvector : (C→ Int BVPred BV)]
-(define-rosette-primop bitvector-size : (C→ CBVPred CPosInt))
+ [bitvector-size : (C→ CBVPred CPosInt)]
;; ---------------------------------
;; Logic operators
-(define-rosette-primop ! : (C→ Bool Bool))
-(define-rosette-primop <=> : (C→ Bool Bool Bool))
+ [! : (C→ Bool Bool)]
+ [<=> : (C→ Bool Bool Bool)]))
(define-typed-syntax &&
[(_ e ...) ≫
@@ -596,13 +602,13 @@
(define-base-types CSolution CPict)
-(define-rosette-primop core : (C→ Any Any))
-(define-rosette-primop sat? : (C→ Any Bool))
-(define-rosette-primop unsat? : (C→ Any Bool))
-(define-rosette-primop unsat : (Ccase-> (C→ CSolution)
- (C→ (CListof Bool) CSolution)))
-(define-rosette-primop forall : (C→ (CListof Any) Bool Bool))
-(define-rosette-primop exists : (C→ (CListof Any) Bool Bool))
+(provide (rosette-typed-out [core : (C→ Any Any)]
+ [sat? : (C→ Any Bool)]
+ [unsat? : (C→ Any Bool)]
+ [unsat : (Ccase-> (C→ CSolution)
+ (C→ (CListof Bool) CSolution))]
+ [forall : (C→ (CListof Any) Bool Bool)]
+ [exists : (C→ (CListof Any) Bool Bool)]))
(define-typed-syntax verify
[(_ e) ≫
diff --git a/turnstile/examples/stlc+lit.rkt b/turnstile/examples/stlc+lit.rkt
@@ -1,5 +1,6 @@
#lang turnstile/lang
(extends "stlc.rkt")
+(provide (typed-out [+ : (→ Int Int Int)]))
;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
;; Types:
@@ -12,8 +13,6 @@
(define-base-type Int)
-(define-primop + : (→ Int Int Int))
-
(define-typed-syntax #%datum
[(_ . n:integer) ≫
--------
diff --git a/turnstile/examples/stlc+sub.rkt b/turnstile/examples/stlc+sub.rkt
@@ -20,12 +20,10 @@
;; - also *
;; Other: sub? current-sub?
-(define-base-type Top)
-(define-base-type Num)
-(define-base-type Nat)
+(provide (typed-out [+ : (→ Num Num Num)]
+ [* : (→ Num Num Num)]))
-(define-primop + : (→ Num Num Num))
-(define-primop * : (→ Num Num Num))
+(define-base-types Top Num Nat)
(define-typed-syntax #%datum
[(_ . n:nat) ≫
diff --git a/turnstile/examples/stlc+union+case.rkt b/turnstile/examples/stlc+union+case.rkt
@@ -13,16 +13,17 @@
;; - terms from stlc+union.rkt
;; Other: updated current-sub?
+(provide (typed-out [add1 : (case→ (→ Nat Nat)
+ (→ Int Int))]
+ [sub1 : (case→ (→ Zero NegInt)
+ (→ PosInt Nat)
+ (→ NegInt NegInt)
+ (→ Nat Nat)
+ (→ Int Int))]))
+
(define-type-constructor case-> #:arity > 0)
(define-syntax case→ (make-rename-transformer #'case->))
-(define-primop add1 : (case→ (→ Nat Nat)
- (→ Int Int)))
-(define-primop sub1 : (case→ (→ Zero NegInt)
- (→ PosInt Nat)
- (→ NegInt NegInt)
- (→ Nat Nat)
- (→ Int Int)))
(define-typed-syntax app #:export-as #%app
[(_ e_fn e_arg ...) ≫
diff --git a/turnstile/examples/stlc+union.rkt b/turnstile/examples/stlc+union.rkt
@@ -3,9 +3,6 @@
#:except #%app #%datum + add1 sub1 *
Int Int? ~Int Float Float? ~Float Bool ~Bool Bool?)
(reuse define-type-alias #:from "stlc+reco+var.rkt")
-(provide Int Num Nat U Bool
- define-named-type-alias
- (for-syntax current-sub? prune+sort))
;; Simply-Typed Lambda Calculus, plus union types
;; Types:
@@ -23,6 +20,14 @@
;; - also *
;; Other: sub? current-sub?
+(provide Int Num Nat U Bool
+ define-named-type-alias
+ (for-syntax current-sub? prune+sort)
+ (typed-out [+ : (→ Num Num Num)]
+ [* : (→ Num Num Num)]
+ [add1 : (→ Int Int)]
+ [sub1 : (→ Int Int)]))
+
(define-syntax define-named-type-alias
(syntax-parser
[(define-named-type-alias Name:id τ:type)
@@ -66,11 +71,6 @@
(define-syntax Num
(make-variable-like-transformer (add-orig #'(U Float Int) #'Num)))
-(define-primop + : (→ Num Num Num))
-(define-primop * : (→ Num Num Num))
-(define-primop add1 : (→ Int Int))
-(define-primop sub1 : (→ Int Int))
-
(define-typed-syntax datum #:export-as #%datum
[(_ . b:boolean) ≫
#:with ty_out (if (syntax-e #'b) #'True #'False)
diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl
@@ -117,10 +117,15 @@ A @racket[define-typed-syntax] definition is automatically provided, either usin
the given name, or with a specified @racket[#:export-as] name.
}
-@defform[(define-primop op-id : τ)]{
-Attaches type @racket[τ] to identifier @racket[op-id], e.g.
- @racket[(define-primop + : (→ Int Int))].
-Automatically provides the new @racket[op-id].}
+@defform*[((define-primop op-id τ)
+ (define-primop op-id : τ)
+ (define-primop typed-op-id op-id τ)
+ (define-primop typed-op-id op-id : τ))]{
+Defines @racket[typed-op-id] by attaching type @racket[τ] to (untyped)
+identifier @racket[op-id], e.g. @racket[(define-primop typed+ + : (→ Int Int))].
+
+When not specified, @racket[typed-op-id] is @racket[op-id] suffixed with
+@litchar{-} (see @secref{racket-}).}
@defform[(define-syntax-category name-id)]{
Defines a new "category" of syntax by defining a series of forms and functions.
@@ -224,7 +229,23 @@ equality, but includes alpha-equivalence.
]
}
-@section{@racket[require] and @racket[provide]-like Forms}
+@section{@racket[require] and @racket[provide]-related Forms}
+
+@defform[(typed-out x+ty+maybe-rename ...)
+ #:grammar
+ ([x+ty+maybe-rename
+ (code:line [x ty])
+ (code:line [x : ty])
+ (code:line [[x ty] out-x])
+ (code:line [[x : ty] out-x])]
+ [x identifier?]
+ [out-x identifier?]
+ [ty type?])]{
+A provide-spec that adds type @racket[ty] to untyped @racket[x] and provides
+that typed identifier as either @racket[x], or @racket[out-x] if it's specified.
+
+Equivalent to a @racket[define-primop] that automatically provides its
+definition.}
@defform[(extends base-lang option ...)
#:grammar
@@ -240,6 +261,12 @@ The imported names are available for use in the current module, with a
[old new]])]{
Reuses @racket[name]s from @racket[base-lang].}
+@section[#:tag "racket-"]{Suffixed Racket bindings}
+
+To help avoid name conflicts, Turnstile re-provides all Racket bindings with a
+@litchar{-} suffix. These bindings are automatically used in some cases, e.g.,
+@racket[define-primop].
+
@section{Lower-level Functions}
This section describes lower-level functions and parameters. It's usually not
