diff --git a/macrotypes/examples/ext-stlc.rkt b/macrotypes/examples/ext-stlc.rkt index 5b8f44e..48e5774 100644 --- 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 index d73f646..1fe99cc 100644 --- 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 index 370e5d1..c7e388f 100644 --- 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 index 58212ca..4c27507 100644 --- 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 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)] + [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 index 2dd024a..d88f3ec 100644 --- 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 index 5973b25..ba7fe66 100644 --- 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 index 756daa0..221129f 100644 --- 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 index 0e2bd1c..9ef03a8 100644 --- 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 index 6e9c3b2..e206b6e 100644 --- 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 index 4b7293b..fbff9bb 100644 --- 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 index 0daba41..58b73a0 100644 --- 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 index bcd43f2..0deaa11 100644 --- 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 index 348e717..1a9fc0b 100644 --- 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 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)] + [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 index 59b372d..3212d37 100644 --- 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 index d524fdc..9e0d774 100644 --- 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 index dec8358..83a011f 100644 --- 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 index bb5a3d1..a956bc2 100644 --- 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 index 8ad425b..bd09473 100644 --- 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 index 73f707f..751ae7f 100644 --- 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 index a1f9783..25cb23b 100644 --- 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 +;; IO and other built-in ops -(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)) +(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)] -;; --------------------------------- -;; Types for built-in operations + [equal? : (C→ Any Any Bool)] + [eq? : (C→ Any Any Bool)] -(define-rosette-primop equal? : (C→ Any Any Bool)) -(define-rosette-primop eq? : (C→ Any Any Bool)) + [pi : CNum] -(define-rosette-primop 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))] -(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))) + [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 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)] -(define-rosette-primop not : (C→ Any Bool)) -(define-rosette-primop 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))] -;; 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)) + ;; 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 index 9c4c0d5..e058eb2 100644 --- 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 index d2f349d..4d24c90 100644 --- 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 index 50018f5..297808e 100644 --- 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 index 2d66c41..ddc6f68 100644 --- 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 index 120ba1f..8de98dc 100644 --- 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