diff --git a/racket/typed/prim.rkt b/racket/typed/prim.rkt new file mode 100644 index 0000000..b557d59 --- /dev/null +++ b/racket/typed/prim.rkt @@ -0,0 +1,93 @@ +#lang turnstile + +(provide (all-defined-out) + (for-syntax (all-defined-out))) + +(require "core-types.rkt") +(require (rename-in racket/math [exact-truncate exact-truncate-])) +(require (postfix-in - (only-in racket/format ~a))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Primitives +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; hmmm +(define-primop + (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns)))) +(define-primop - (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns)))) +(define-primop * (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns)))) +(define-primop or (→ Bool Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) +(define-primop not (→ Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) +(define-primop < (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) +(define-primop > (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) +(define-primop <= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) +(define-primop >= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) +(define-primop = (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) + +(define-primop bytes->string/utf-8 (→ ByteString (Computation (Value String) (Endpoints) (Roles) (Spawns)))) +(define-primop string->bytes/utf-8 (→ String (Computation (Value ByteString) (Endpoints) (Roles) (Spawns)))) +(define-primop gensym (→ Symbol (Computation (Value Symbol) (Endpoints) (Roles) (Spawns)))) +(define-primop symbol->string (→ Symbol (Computation (Value String) (Endpoints) (Roles) (Spawns)))) +(define-primop string->symbol (→ String (Computation (Value Symbol) (Endpoints) (Roles) (Spawns)))) + +(define-typed-syntax (/ e1 e2) ≫ + [⊢ e1 ≫ e1- (⇐ : Int)] + [⊢ e2 ≫ e2- (⇐ : Int)] + #:fail-unless (pure? #'e1-) "expression not allowed to have effects" + #:fail-unless (pure? #'e2-) "expression not allowed to have effects" + ------------------------ + [⊢ (exact-truncate- (/- e1- e2-)) (⇒ : Int)]) + +;; for some reason defining `and` as a prim op doesn't work +(define-typed-syntax (and e ...) ≫ + [⊢ e ≫ e- (⇐ : Bool)] ... + #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects" + ------------------------ + [⊢ (and- e- ...) (⇒ : Bool)]) + +(define-typed-syntax (equal? e1:expr e2:expr) ≫ + [⊢ e1 ≫ e1- (⇒ : τ1)] + #:fail-unless (flat-type? #'τ1) + (format "equality only available on flat data; got ~a" (type->str #'τ1)) + [⊢ e2 ≫ e2- (⇐ : τ1)] + #:fail-unless (pure? #'e1-) "expression not allowed to have effects" + #:fail-unless (pure? #'e2-) "expression not allowed to have effects" + --------------------------------------------------------------------------- + [⊢ (equal?- e1- e2-) (⇒ : Bool)]) + +(define-typed-syntax (displayln e:expr) ≫ + [⊢ e ≫ e- (⇒ : τ)] + #:fail-unless (pure? #'e-) "expression not allowed to have effects" + --------------- + [⊢ (displayln- e-) (⇒ : ★/t)]) + +(define-typed-syntax (printf e ...+) ≫ + [⊢ e ≫ e- (⇒ : τ)] ... + #:fail-unless (stx-andmap pure? #'(e- ...)) "expression not allowed to have effects" + --------------- + [⊢ (printf- e- ...) (⇒ : ★/t)]) + +(define-typed-syntax (~a e ...) ≫ + [⊢ e ≫ e- (⇒ : τ)] ... + #:fail-unless (stx-andmap flat-type? #'(τ ...)) + "expressions must be string-able" + -------------------------------------------------- + [⊢ (~a- e- ...) (⇒ : String)]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Basic Values +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-typed-syntax #%datum + [(_ . n:integer) ≫ + ---------------- + [⊢ (#%datum- . n) (⇒ : Int)]] + [(_ . b:boolean) ≫ + ---------------- + [⊢ (#%datum- . b) (⇒ : Bool)]] + [(_ . s:string) ≫ + ---------------- + [⊢ (#%datum- . s) (⇒ : String)]]) + +(define-typed-syntax (typed-quote x:id) ≫ + ------------------------------- + [⊢ (quote- x) (⇒ : Symbol)]) diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 58c8e11..1fd97a5 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -15,7 +15,7 @@ Computation Value Endpoints Roles Spawns ;; Statements let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do - when unless send! + when unless send! define ;; Derived Forms during define/query-value define/query-set ;; endpoints @@ -30,9 +30,7 @@ ;; patterns bind discard ;; primitives - + - * / and or not > < >= <= = equal? displayln printf define - gensym symbol->string string->symbol bytes->string/utf-8 string->bytes/utf-8 - ~a + (all-from-out "prim.rkt") ;; lists (all-from-out "list.rkt") ;; sets @@ -50,6 +48,7 @@ (require "core-types.rkt") (require "list.rkt") (require "set.rkt") +(require "prim.rkt") (require (prefix-in syndicate: syndicate/actor-lang)) @@ -57,12 +56,9 @@ (require (for-syntax turnstile/examples/util/filter-maximal)) (require (for-syntax racket/struct-info)) (require macrotypes/postfix-in) -(require (rename-in racket/math [exact-truncate exact-truncate-])) (require (postfix-in - racket/list)) (require (postfix-in - racket/set)) (require (postfix-in - racket/match)) -(require (postfix-in - (only-in racket/format ~a))) - (module+ test (require rackunit) @@ -554,91 +550,6 @@ ----------------------------------------------------------------------------------- [⊢ (syndicate:run-ground s- ...) (⇒ : (AssertionSet τ-c))]) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Primitives -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; hmmm -(define-primop + (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns)))) -(define-primop - (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns)))) -(define-primop * (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns)))) -#;(define-primop and (→ Bool Bool Bool)) -(define-primop or (→ Bool Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) -(define-primop not (→ Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) -(define-primop < (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) -(define-primop > (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) -(define-primop <= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) -(define-primop >= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) -(define-primop = (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) - -(define-primop bytes->string/utf-8 (→ ByteString (Computation (Value String) (Endpoints) (Roles) (Spawns)))) -(define-primop string->bytes/utf-8 (→ String (Computation (Value ByteString) (Endpoints) (Roles) (Spawns)))) -(define-primop gensym (→ Symbol (Computation (Value Symbol) (Endpoints) (Roles) (Spawns)))) -(define-primop symbol->string (→ Symbol (Computation (Value String) (Endpoints) (Roles) (Spawns)))) -(define-primop string->symbol (→ String (Computation (Value Symbol) (Endpoints) (Roles) (Spawns)))) - -(define-typed-syntax (/ e1 e2) ≫ - [⊢ e1 ≫ e1- (⇐ : Int)] - [⊢ e2 ≫ e2- (⇐ : Int)] - #:fail-unless (pure? #'e1-) "expression not allowed to have effects" - #:fail-unless (pure? #'e2-) "expression not allowed to have effects" - ------------------------ - [⊢ (exact-truncate- (/- e1- e2-)) (⇒ : Int)]) - -;; for some reason defining `and` as a prim op doesn't work -(define-typed-syntax (and e ...) ≫ - [⊢ e ≫ e- (⇐ : Bool)] ... - #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects" - ------------------------ - [⊢ (and- e- ...) (⇒ : Bool)]) - -(define-typed-syntax (equal? e1:expr e2:expr) ≫ - [⊢ e1 ≫ e1- (⇒ : τ1)] - #:fail-unless (flat-type? #'τ1) - (format "equality only available on flat data; got ~a" (type->str #'τ1)) - [⊢ e2 ≫ e2- (⇐ : τ1)] - #:fail-unless (pure? #'e1-) "expression not allowed to have effects" - #:fail-unless (pure? #'e2-) "expression not allowed to have effects" - --------------------------------------------------------------------------- - [⊢ (equal?- e1- e2-) (⇒ : Bool)]) - -(define-typed-syntax (displayln e:expr) ≫ - [⊢ e ≫ e- (⇒ : τ)] - #:fail-unless (pure? #'e-) "expression not allowed to have effects" - --------------- - [⊢ (displayln- e-) (⇒ : ★/t)]) - -(define-typed-syntax (printf e ...+) ≫ - [⊢ e ≫ e- (⇒ : τ)] ... - #:fail-unless (stx-andmap pure? #'(e- ...)) "expression not allowed to have effects" - --------------- - [⊢ (printf- e- ...) (⇒ : ★/t)]) - -(define-typed-syntax (~a e ...) ≫ - [⊢ e ≫ e- (⇒ : τ)] ... - #:fail-unless (stx-andmap flat-type? #'(τ ...)) - "expressions must be string-able" - -------------------------------------------------- - [⊢ (~a- e- ...) (⇒ : String)]) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Basic Values -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(define-typed-syntax #%datum - [(_ . n:integer) ≫ - ---------------- - [⊢ (#%datum- . n) (⇒ : Int)]] - [(_ . b:boolean) ≫ - ---------------- - [⊢ (#%datum- . b) (⇒ : Bool)]] - [(_ . s:string) ≫ - ---------------- - [⊢ (#%datum- . s) (⇒ : String)]]) - -(define-typed-syntax (typed-quote x:id) ≫ - ------------------------------- - [⊢ (quote- x) (⇒ : Symbol)]) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Utilities diff --git a/racket/typed/set.rkt b/racket/typed/set.rkt index d96e61e..52c1bff 100644 --- a/racket/typed/set.rkt +++ b/racket/typed/set.rkt @@ -103,7 +103,8 @@ ----------------------- [⊢ (set->list- s-) ⇒ (List τ)]) -#;(module+ test +(module+ test + (require "prim.rkt") (check-type (set 1 2 3) : (Set Int) -> (set- 2 3 1))