From 1bdb9b78207e8f369247e5993fecbf23874bb55f Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Thu, 9 May 2019 10:23:15 -0400 Subject: [PATCH] move definition of primitive base types --- racket/typed/core-types.rkt | 15 +++++++++++++-- racket/typed/hash.rkt | 1 + racket/typed/list.rkt | 1 + racket/typed/prim.rkt | 2 ++ racket/typed/roles.rkt | 2 +- racket/typed/sequence.rkt | 1 + racket/typed/set.rkt | 4 +++- 7 files changed, 22 insertions(+), 4 deletions(-) diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt index b17dcda..4b17fdc 100644 --- a/racket/typed/core-types.rkt +++ b/racket/typed/core-types.rkt @@ -207,7 +207,7 @@ (define-type-constructor Spawns #:arity >= 0) -(define-base-types Int Bool String Discard ★/t FacetName ByteString Symbol) +(define-base-types Discard ★/t FacetName) (define-for-syntax (type-eval t) ((current-type-eval) t)) @@ -262,7 +262,18 @@ #'(~→ ty-in ... (~Computation (~Value ty-out) (~Endpoints) (~Roles) - (~Spawns)))])))) + (~Spawns)))]))) + + ;; matching possibly polymorphic types + (define-syntax ~?∀ + (pattern-expander + (lambda (stx) + (syntax-case stx () + [(?∀ vars-pat body-pat) + #'(~or (~∀ vars-pat body-pat) + (~and (~not (~∀ _ _)) + (~parse vars-pat #'()) + body-pat))]))))) ;; for looking at the "effects" (begin-for-syntax diff --git a/racket/typed/hash.rkt b/racket/typed/hash.rkt index 586fdbd..8433eb7 100644 --- a/racket/typed/hash.rkt +++ b/racket/typed/hash.rkt @@ -19,6 +19,7 @@ (require "core-types.rkt") (require (only-in "list.rkt" List)) +(require (only-in "prim.rkt" Int Bool)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Immutable Hash Tables diff --git a/racket/typed/list.rkt b/racket/typed/list.rkt index c6cba1f..85cc8a9 100644 --- a/racket/typed/list.rkt +++ b/racket/typed/list.rkt @@ -11,6 +11,7 @@ reverse) (require "core-types.rkt") +(require (only-in "prim.rkt" Bool)) (require (postfix-in - racket/list)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/racket/typed/prim.rkt b/racket/typed/prim.rkt index 83a8e74..0a1b782 100644 --- a/racket/typed/prim.rkt +++ b/racket/typed/prim.rkt @@ -11,6 +11,8 @@ ;; Primitives ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(define-base-types Int Bool String ByteString Symbol) + ;; hmmm (define-primop + (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns)))) (define-primop - (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns)))) diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 5ddb407..75e08b6 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -8,7 +8,7 @@ ;; Start dataspace programs run-ground-dataspace ;; Types - Int Bool String Tuple Bind Discard → ∀ ByteString Symbol + Tuple Bind Discard → ∀ Role Reacts Shares Know ¬Know Message OnDataflow Stop OnStart OnStop FacetName Field ★/t Observe Inbound Outbound Actor U diff --git a/racket/typed/sequence.rkt b/racket/typed/sequence.rkt index 62ca918..ea8eef4 100644 --- a/racket/typed/sequence.rkt +++ b/racket/typed/sequence.rkt @@ -22,6 +22,7 @@ (require "core-types.rkt") (require (only-in "list.rkt" List)) (require (only-in "set.rkt" Set)) +(require (only-in "prim.rkt" Int Bool)) #;(require (postfix-in - racket/sequence)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/racket/typed/set.rkt b/racket/typed/set.rkt index 52c1bff..3bfc84b 100644 --- a/racket/typed/set.rkt +++ b/racket/typed/set.rkt @@ -14,13 +14,15 @@ set->list) (require "core-types.rkt") +(require (only-in "prim.rkt" Int)) (require (only-in "list.rkt" ~List)) (require (postfix-in - racket/set)) (module+ test (require rackunit) - (require rackunit/turnstile)) + (require rackunit/turnstile) + ) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Sets