From 99e53d97294db2ad6420eeff3881e97530e15067 Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Mon, 24 Feb 2020 15:10:52 -0500 Subject: [PATCH] fix typed `or` --- racket/typed/prim.rkt | 9 +++++++-- racket/typed/tests/primitives.rkt | 27 +++++++++++++++++++++++++++ 2 files changed, 34 insertions(+), 2 deletions(-) create mode 100644 racket/typed/tests/primitives.rkt diff --git a/racket/typed/prim.rkt b/racket/typed/prim.rkt index 3d651d4..71b1465 100644 --- a/racket/typed/prim.rkt +++ b/racket/typed/prim.rkt @@ -17,7 +17,6 @@ (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)))) @@ -48,13 +47,19 @@ ------------------------ [⊢ (#%app- exact-truncate- (#%app- /- e1- e2-)) (⇒ : Int)]) -;; for some reason defining `and` as a prim op doesn't work +;; I think defining `and` and `or` as primops doesn't work because they're syntax (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 (or e ...) ≫ + [⊢ e ≫ e- (⇐ : Bool)] ... + #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects" + ------------------------ + [⊢ (or- e- ...) (⇒ : Bool)]) + (define-typed-syntax (equal? e1:expr e2:expr) ≫ [⊢ e1 ≫ e1- (⇒ : τ1)] [⊢ e2 ≫ e2- (⇒ : τ2)] diff --git a/racket/typed/tests/primitives.rkt b/racket/typed/tests/primitives.rkt new file mode 100644 index 0000000..10cff18 --- /dev/null +++ b/racket/typed/tests/primitives.rkt @@ -0,0 +1,27 @@ +#lang typed/syndicate/roles + +(require rackunit/turnstile) + +(check-type (or #f #t) + : Bool + ⇒ #t) + +(check-type (and #t #f) + : Bool + ⇒ #f) + +(check-type (or) + : Bool + ⇒ #f) + +(check-type (and) + : Bool + ⇒ #t) + +(check-type (or #f #f #f #f #f #t) + : Bool + ⇒ #t) + +(check-type (and #t #t #t #t #t #f) + : Bool + ⇒ #f)