fix typed `or`

This commit is contained in:
Sam Caldwell 2020-02-24 15:10:52 -05:00
parent 0074fcb566
commit 99e53d9729
2 changed files with 34 additions and 2 deletions

View File

@ -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)]

View File

@ -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)