From 7ef84a313d4ca5df4c9ef722e0dec703b2a66289 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Thu, 1 Sep 2016 16:33:55 -0400 Subject: [PATCH] support symbolic Listof; add letrec, remaining sec2 tests --- turnstile/examples/rosette/rosette2.rkt | 104 ++++++++++++------ .../rosette/rosette-guide-sec2-tests.rkt | 50 +++++++++ .../rosette/rosette-guide-sec3-tests.rkt | 2 + 3 files changed, 121 insertions(+), 35 deletions(-) diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index 8be107b..1ea4069 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -4,7 +4,9 @@ (reuse #%datum define-type-alias define-named-type-alias #:from "../stlc+union.rkt") -(provide (rename-out [ro:#%module-begin #%module-begin]) +(provide (rename-out [ro:#%module-begin #%module-begin] + [stlc:λ lambda] + [first car] [rest cdr]) Any Nothing CU U C→ → (for-syntax ~C→ C→?) @@ -142,6 +144,7 @@ (define-named-type-alias Unit (add-predm (U CUnit) ro:void?)) (define-named-type-alias (CParamof X) (Ccase-> (C→ X) (C→ X CUnit))) +(define-named-type-alias (Listof X) (U (CListof X))) (define-syntax → (syntax-parser @@ -259,6 +262,9 @@ [(_ x:id) ≫ -------- [⊢ [_ ≫ (quote- x) ⇒ : CSymbol]]] + [(_ (x:integer ...)) ≫ + -------- + [⊢ [_ ≫ (quote- (x ...)) ⇒ : (CListof CInt)]]] [(_ (x:id ...)) ≫ -------- [⊢ [_ ≫ (quote- (x ...)) ⇒ : (CListof CSymbol)]]]) @@ -377,6 +383,18 @@ -------- [_ ≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body ...))]]) +(define-typed-syntax letrec + [(letrec ([b:type-bind e] ...) e_body ...) ⇐ : τ_expected ≫ + [() ([b.x ≫ x- : b.type] ...) + ⊢ [e ≫ e- ⇐ : b.type] ... [(begin e_body ...) ≫ e_body- ⇐ : τ_expected]] + -------- + [⊢ [_ ≫ (ro:letrec ([x- e-] ...) e_body-) ⇐ : _]]] + [(letrec ([b:type-bind e] ...) e_body ...) ≫ + [() ([b.x ≫ x- : b.type] ...) + ⊢ [e ≫ e- ⇐ : b.type] ... [(begin e_body ...) ≫ e_body- ⇒ : τ_body]] + -------- + [⊢ [_ ≫ (ro:letrec ([x- e-] ...) e_body-) ⇒ : τ_body]]]) + ;; -------------------- ;; begin @@ -424,6 +442,11 @@ ;; --------------------------------- ;; lists +(define-rosette-primop null? : (Ccase-> (C→ (CListof Any) CBool) + (C→ (Listof Any) Bool))) +(define-rosette-primop empty? : (Ccase-> (C→ (CListof Any) CBool) + (C→ (Listof Any) Bool))) + (define-typed-syntax list [(_ e ...) ≫ [⊢ [e ≫ e- ⇒ : τ] ...] @@ -433,82 +456,93 @@ (define-typed-syntax cons [_:id ≫ ;; TODO: use polymorphism -------- - [⊢ [_ ≫ ro:cons ⇒ : (C→ Any (CListof Any) (CListof Any))]]] + [⊢ [_ ≫ ro:cons ⇒ : (Ccase-> (C→ Any (CListof Any) (CListof Any)) + (C→ Any (Listof Any) (Listof Any)))]]] [(_ e1 e2) ≫ [⊢ [e2 ≫ e2- ⇒ : (~CListof τ)]] [⊢ [e1 ≫ e1- ⇐ : τ]] -------- [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CListof τ)]]] + [(_ e1 e2) ≫ + [⊢ [e2 ≫ e2- ⇒ : (~U* (~CListof τ) ...)]] + [⊢ [e1 ≫ e1- ⇒ : τ1]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CListof (U τ1 τ)) ...)]]] [(_ e1 e2) ≫ [⊢ [e1 ≫ e1- ⇒ : τ1]] [⊢ [e2 ≫ e2- ⇒ : (~CList τ ...)]] -------- - [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CList τ1 τ ...)]]]) - -(define-typed-syntax car - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:car ⇒ : (C→ (CListof Any) Any)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : τ]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : τ1]]]) - -(define-typed-syntax cdr - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:cdr ⇒ : (C→ (CListof Any) (CListof Any))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CListof τ)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CList τ ...)]]]) + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CList τ1 τ ...)]]] + [(_ e1 e2) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : (~U* (~CList τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CList τ1 τ ...) ...)]]]) +;; in typed rosette, car and cdr are the same as first and rest? (define-typed-syntax first [_:id ≫ ;; TODO: use polymorphism -------- - [⊢ [_ ≫ ro:first ⇒ : (C→ (CListof Any) Any)]]] + [⊢ [_ ≫ ro:first ⇒ : (C→ (Listof Any) Any)]]] [(_ e) ≫ [⊢ [e ≫ e- ⇒ : (~CListof τ)]] -------- [⊢ [_ ≫ (ro:first e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:first e-) ⇒ : (U τ ...)]]] [(_ e) ≫ [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] -------- - [⊢ [_ ≫ (ro:first e-) ⇒ : τ1]]]) + [⊢ [_ ≫ (ro:first e-) ⇒ : τ1]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:first e-) ⇒ : (U τ1 ...)]]]) (define-typed-syntax rest [_:id ≫ ;; TODO: use polymorphism -------- - [⊢ [_ ≫ ro:rest ⇒ : (C→ (CListof Any) (CListof Any))]]] + [⊢ [_ ≫ ro:rest ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) + (C→ (Listof Any) (Listof Any)))]]] [(_ e) ≫ [⊢ [e ≫ e- ⇒ : (~CListof τ)]] -------- [⊢ [_ ≫ (ro:rest e-) ⇒ : (CListof τ)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:rest e-) ⇒ : (U (CListof τ) ...)]]] [(_ e) ≫ [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] -------- - [⊢ [_ ≫ (ro:rest e-) ⇒ : (CList τ ...)]]]) + [⊢ [_ ≫ (ro:rest e-) ⇒ : (CList τ ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:rest e-) ⇒ : (U (CList τ ...) ...)]]]) (define-typed-syntax second [_:id ≫ ;; TODO: use polymorphism -------- - [⊢ [_ ≫ ro:second ⇒ : (C→ (CListof Any) Any)]]] + [⊢ [_ ≫ ro:second ⇒ : (C→ (Listof Any) Any)]]] [(_ e) ≫ [⊢ [e ≫ e- ⇒ : (~CListof τ)]] -------- [⊢ [_ ≫ (ro:second e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:second e-) ⇒ : (U τ ...)]]] [(_ e) ≫ [⊢ [e ≫ e- ⇒ : (~CList τ1 τ2 τ ...)]] -------- - [⊢ [_ ≫ (ro:second e-) ⇒ : τ2]]]) + [⊢ [_ ≫ (ro:second e-) ⇒ : τ2]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ2 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:second e-) ⇒ : (U τ2 ...)]]]) ;; --------------------------------- ;; IO and other built-in ops diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt index f3b4373..3245239 100644 --- a/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt @@ -182,3 +182,53 @@ (check-type sol3 : CSolution) (check-type (sat? sol3) : Bool -> #t) (check-type (evaluate y1 sol3) : Num -> 0.0) + +;; these examples uses symbolic lists +(check-type + (letrec ([[ones : (C→ Int (Listof Int))] + (lambda ([n : Int]) + (if (<= n 0) + (list) + (cons 1 (ones (- n 1)))))]) + (printf "~a" (ones 3)) + (printf "~a" (ones x))) + : Unit) + +(check-type + (letrec ([[ones : (C→ Int (Listof Int))] + (lambda ([n : Int]) + (if (<= n 0) + (list) + (cons 1 (ones (- n 1)))))]) + (ones 3)) + : (Listof Int) -> (list 1 1 1)) + +;; inf loop +(check-type + (letrec ([[ones : (C→ Int (Listof Int))] + (lambda ([n : Int]) + (if (<= n 0) + (list) + (cons 1 (ones (- n 1)))))]) + (ones x)) + : (Listof Int)) + +;; drop lambda annotation +(check-type + (letrec ([[ones : (C→ Int (Listof Int))] + (lambda (n) + (if (<= n 0) + (list) + (cons 1 (ones (- n 1)))))]) + (printf "~a" (ones 3)) + (printf "~a" (ones x))) + : Unit) + +(check-type + (letrec ([[adder : (C→ (CListof Int) Int (CListof Int))] + (lambda (vs n) + (if (null? vs) + (list) + (cons (+ (car vs) n) (adder (cdr vs) n))))]) + (adder '(1 2 3) x)) + : (CListof Int) -> (list (+ 1 x) (+ 2 x) (+ 3 x))) diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt index b3d4d94..9bbe5e9 100644 --- a/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt @@ -33,6 +33,8 @@ (check-type res : (CList Bool Nat)) (check-type (second res) : Nat -> (if (first res) 0 3)) +;; use car and cdr instead +(check-type (car (cdr res)) : Nat -> (if (car res) 0 3)) ;; 3.2 Solver-Aided Forms