From efbf03c258fe98ad5201c6ac0ae2f372fab3d25f Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 26 Jul 2016 16:32:42 -0400 Subject: [PATCH] start stlc+union --- macrotypes/stx-utils.rkt | 6 +- turnstile/examples/stlc+union.rkt | 86 +++++++++++++++++++ .../tests/rosette/run-all-rosette-tests.rkt | 3 +- turnstile/examples/tests/stlc+union.rkt | 81 +++++++++++++++++ 4 files changed, 172 insertions(+), 4 deletions(-) create mode 100644 turnstile/examples/stlc+union.rkt create mode 100644 turnstile/examples/tests/stlc+union.rkt diff --git a/macrotypes/stx-utils.rkt b/macrotypes/stx-utils.rkt index e03f967..ab7268c 100644 --- a/macrotypes/stx-utils.rkt +++ b/macrotypes/stx-utils.rkt @@ -1,5 +1,5 @@ #lang racket/base -(require syntax/stx syntax/parse racket/list version/utils) +(require syntax/stx syntax/parse racket/list racket/format version/utils) (provide (all-defined-out)) (define (stx-cadr stx) (stx-car (stx-cdr stx))) @@ -44,8 +44,8 @@ (string=? (syntax-e s1) (syntax-e s2))) (define (stx-sort stx - #:cmp [cmp (lambda (x y) (string<=? (symbol->string (syntax->datum x)) - (symbol->string (syntax->datum y))))] + #:cmp [cmp (lambda (x y) (string<=? (~a (syntax->datum x)) + (~a (syntax->datum y))))] #:key [key-fn (λ (x) x)]) (sort (stx->list stx) cmp #:key key-fn)) diff --git a/turnstile/examples/stlc+union.rkt b/turnstile/examples/stlc+union.rkt new file mode 100644 index 0000000..84f3688 --- /dev/null +++ b/turnstile/examples/stlc+union.rkt @@ -0,0 +1,86 @@ +#lang turnstile +(extends "ext-stlc.rkt" #:except #%datum + add1 * Int Int? ~Int Float Float? ~Float) +(reuse define-type-alias #:from "stlc+reco+var.rkt") +(provide Int Num U) + +;; Simply-Typed Lambda Calculus, plus union types +;; Types: +;; - types from and ext+stlc.rkt +;; - Top, Num, Nat +;; - U +;; Type relations: +;; - sub? +;; - Any <: Top +;; - Nat <: Int +;; - Int <: Num +;; - → +;; Terms: +;; - terms from stlc+lit.rkt, except redefined: datum and + +;; - also * +;; Other: sub? current-sub? + +(define-base-types Nat NegInt Float) +(define-type-constructor U* #:arity > 0) +(define-for-syntax (prune+sort tys) + (define ts (stx->list tys)) + (stx-sort (remove-duplicates (stx->list tys) typecheck?))) + + +(define-syntax (U stx) + (syntax-parse stx + [(_ . tys) + #:with ((~or (~U* ty1- ...) ty2-) ...) (stx-map (current-type-eval) #'tys) + #:with tys- (prune+sort #'(ty1- ... ... ty2- ...)) + (if (= 1 (stx-length #'tys-)) + (stx-car #'tys) + #'(U* . tys-))])) +(define-syntax Int + (make-variable-like-transformer (add-orig #'(U Nat NegInt) #'Int))) +(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-typed-syntax #%datum + [(#%datum . n:nat) ≫ + -------- + [⊢ [_ ≫ (#%datum- . n) ⇒ : Nat]]] + [(#%datum . n:integer) ≫ + -------- + [⊢ [_ ≫ (#%datum- . n) ⇒ : NegInt]]] + [(#%datum . n:number) ≫ + #:when (real? (syntax-e #'n)) + -------- + [⊢ [_ ≫ (#%datum- . n) ⇒ : Float]]] + [(#%datum . x) ≫ + -------- + [_ ≻ (ext-stlc:#%datum . x)]]) + +(begin-for-syntax + (define (sub? t1 t2) + ; need this because recursive calls made with unexpanded types + ;; (define τ1 ((current-type-eval) t1)) + ;; (define τ2 ((current-type-eval) t2)) + ;; (printf "t1 = ~a\n" (syntax->datum t1)) + ;; (printf "t2 = ~a\n" (syntax->datum t2)) + (or + ((current-type=?) t1 t2) + (syntax-parse (list t1 t2) + [((~U* . tys1) (~U* . tys2)) + (for/and ([t (stx->list #'tys1)]) + ((current-sub?) t t2))] + [(ty (~U* . tys)) + (for/or ([t (stx->list #'tys)]) + ((current-sub?) #'ty t))] + [_ #f]))) + (define current-sub? (make-parameter sub?)) + (current-typecheck-relation sub?) + (define (subs? τs1 τs2) + (and (stx-length=? τs1 τs2) + (stx-andmap (current-sub?) τs1 τs2))) + + (define (join t1 t2) #`(U #,t1 #,t2)) + (current-join join)) + diff --git a/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt b/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt index 1e24334..9a2730a 100644 --- a/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt +++ b/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt @@ -3,4 +3,5 @@ (require "bv-tests.rkt") ;(require "bv-ref-tests.rkt") ; visit but dont instantiate, o.w. will get unsat -(dynamic-require "fsm-test.rkt" (void)) +;(dynamic-require "fsm-test.rkt" #f) +(require "ifc-tests.rkt") diff --git a/turnstile/examples/tests/stlc+union.rkt b/turnstile/examples/tests/stlc+union.rkt new file mode 100644 index 0000000..81a53e9 --- /dev/null +++ b/turnstile/examples/tests/stlc+union.rkt @@ -0,0 +1,81 @@ +#lang s-exp "../stlc+union.rkt" +(require "rackunit-typechecking.rkt") + +(check-type 1 : Nat) +(check-type -1 : NegInt) +(check-type 1.1 : Float) +(check-type (+ 1 1.1) : Num -> 2.1) +(check-type (+ 1.1 1) : Num -> 2.1) +(typecheck-fail (+ "1" 1) #:with-msg "expected Num, given String") + +;; Alex's example +;; illustrates flattening +(define-type-alias A Int) +(define-type-alias B String) +(define-type-alias C Bool) +(define-type-alias AC (U A C)) +(define-type-alias BC (U B C)) +(define-type-alias A-BC (U A BC)) +(define-type-alias B-AC (U B AC)) +(check-type ((λ ([x : A-BC]) x) ((λ ([x : B-AC]) x) "1")) : A-BC -> "1") + +; check pruning and collapsing +(define-type-alias NN (U Nat Nat)) +(check-type ((λ ([x : NN]) x) 1) : Nat -> 1) +(define-type-alias NNN (U (U Nat Nat) (U (U Nat Nat Nat) (U Nat Nat)))) +(check-type ((λ ([x : NNN]) x) 1) : Nat -> 1) + + +;; tests from stlc+sub --------------------- +(check-type 1 : Num) +(check-type 1 : Int) +(check-type -1 : Num) +(check-type -1 : Int) +(check-not-type -1 : Nat) +(check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1) +(check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1) +(typecheck-fail ((λ ([x : Nat]) x) -1) #:with-msg "expected Nat, given NegInt") +(check-type (λ ([x : Int]) x) : (→ Int Int)) +; TODO: no function subtypes for now +;(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output +(check-not-type (λ ([x : Int]) x) : (→ Int Nat)) +;(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input +(check-not-type (λ ([x : Int]) x) : (→ Num Int)) + +(check-type ((λ ([f : (→ Int Int)]) (f -1)) add1) : Int ⇒ 0) +; (check-type ((λ ([f : (→ Nat Int)]) (f 1)) add1) : Int ⇒ 2) +(typecheck-fail ((λ ([f : (→ Num Int)]) (f 1.1)) add1)) +;(check-type ((λ ([f : (→ Nat Num)]) (f 1)) add1) : Num ⇒ 2) +(typecheck-fail ((λ ([f : (→ Num Num)]) (f 1.1)) add1)) + +(check-type + : (→ Num Num Num)) +;(check-type + : (→ Int Num Num)) +;(check-type + : (→ Int Int Num)) +;(check-not-type + : (→ Top Int Num)) +(check-not-type + : (→ Int Int Int)) +;(check-type + : (→ Nat Int Top)) + +;; previous tests ------------------------------------------------------------- +;; some change due to more specific types +(check-not-type 1 : (→ Int Int)) +(check-type "one" : String) +(check-type #f : Bool) +(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) +(check-type ((λ ([x : Int] [y : Int]) x) -1 1) : Int -> -1) +(check-not-type (λ ([x : Int]) x) : Int) +(check-type (λ ([x : Int]) x) : (→ Int Int)) +(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Nat)) +(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) +(typecheck-fail ((λ ([x : Sym]) x) 1)) ; Sym is not valid type +(typecheck-fail (λ ([x : Sym]) x)) ; Sym is not valid type +(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type +(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + : (→ (→ Int Int Int) Int Int Int)) +(check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 3) +(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int +(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int +(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args +(check-type ((λ ([x : Int]) (+ x x)) 10) : Num ⇒ 20) + +(check-not-type (λ ([x : Int] [y : Int]) x) : (→ Int Int)) +(check-not-type (λ ([x : Int]) x) : (→ Int Int Int Int))