From cdedc4b5562d678c8cab9218433d1602991998f5 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 9 Nov 2016 17:03:46 -0500
Subject: [PATCH] working with app snippet tests: assignment, vectors,
 pointers, selectors, procedures

---
 turnstile/examples/rosette/synthcl3.rkt       | 325 ++++++++++++++++--
 .../tests/rosette/rosette3/synthcl3-tests.rkt | 136 +++++---
 2 files changed, 393 insertions(+), 68 deletions(-)

diff --git a/turnstile/examples/rosette/synthcl3.rkt b/turnstile/examples/rosette/synthcl3.rkt
index bab15ae..be0f1c7 100644
--- a/turnstile/examples/rosette/synthcl3.rkt
+++ b/turnstile/examples/rosette/synthcl3.rkt
@@ -1,11 +1,18 @@
 #lang turnstile
-(extends "rosette3.rkt" #:except ! #%app || && void = +) ; typed rosette
+(extends "rosette3.rkt" #:except ! #%app || && void = + #%datum if) ; typed rosette
 (require ;(prefix-in ro: (except-in rosette verify sqrt range print)) ; untyped 
+ racket/stxparam
   (prefix-in ro: rosette)
 ;             define-symbolic* #%datum define if ! = number? boolean? cond ||))
+  (prefix-in cl: sdsl/synthcl/lang/forms)
+  (prefix-in cl: sdsl/synthcl/model/reals)
   (prefix-in cl: sdsl/synthcl/model/operators)
   (prefix-in cl: sdsl/synthcl/model/errors)
-  (prefix-in cl: sdsl/synthcl/model/memory))
+  (prefix-in cl: sdsl/synthcl/model/memory)
+  (prefix-in cl: sdsl/synthcl/model/runtime)
+  (prefix-in cl: sdsl/synthcl/model/work)
+  (prefix-in cl: sdsl/synthcl/model/pointers)
+  (for-syntax (prefix-in cl: sdsl/synthcl/lang/util)))
 
 (begin-for-syntax
   (define (mk-cl id) (format-id id "cl:~a" id))
@@ -13,20 +20,25 @@
 
 ;(define-base-types)
 
-(provide (rename-out 
+(provide (rename-out
           [synth-app #%app]
 ;          [rosette3:Bool bool] ; symbolic
 ;          [rosette3:Int int]   ; symbolic
 ;          [rosette3:Num float] ; symbolic
-          [rosette3:CString char*]) ; always concrete
-         bool int float float3 int16 void void*
-         : ! ?: == +
+          #;[rosette3:CString char*]) ; always concrete
+         procedure kernel
+         #%datum if range for
+         bool int int2 int3 int4 float float3 int16 void
+         void* char* int* int16*
+         : ! ?: == + %
          ;; assignment ops
-         = +=
+         = += %=
          (typed-out
           ;; need the concrete cases for literals;
           ;; alternative is to redefine #%datum to give literals symbolic type
-          [% : (Ccase-> (C→ CInt CInt CInt)
+          [malloc : (C→ int void*)]
+          [get_work_dim : (C→ int)]
+           #;[% : (Ccase-> (C→ CInt CInt CInt)
                         (C→ Int Int Int))]
           [!= : (Ccase-> (C→ CNum CNum CBool)
                          (C→ CNum CNum CNum CBool)
@@ -45,7 +57,11 @@
   (define (typecheck/un? t1 t2)
     (typecheck? ((current-type-eval) t1)
                 ((current-type-eval) t2)))
-  (define (real-type? t) (not (typecheck/un? t #'bool)))
+  (define (real-type? t)
+    (and (not (typecheck/un? t #'bool))
+         (not (pointer-type? t))))
+  (define (pointer-type? t)
+    (regexp-match #px"\\*$" (type->str t)))
   (define (type-base t)
     (datum->syntax t
      (string->symbol
@@ -78,12 +94,12 @@
   ;; copied from check-implicit-conversion in lang/types.rkt
   ;; TODO: this should not exception since it is used in stx-parse
   ;; clauses that may want to backtrack
-  (define (cast-ok? from to expr [subexpr #f])
+  (define (cast-ok? from to [expr #f] [subexpr #f])
     (unless (if #t #;(type? to)
               (or (typecheck/un? from to)
                   (and (scalar-type? from) (scalar-type? to))
                   (and (scalar-type? from) (vector-type? to))
-                  #;(and (pointer-type? from) (pointer-type? to))
+                  (and (pointer-type? from) (pointer-type? to))
                   #;(and (equal? from cl_mem) (pointer-type? to)))
               (to from))
       (raise-syntax-error 
@@ -99,6 +115,10 @@
     (set-stx-prop/preserved stx 'convert fn))
   (define (get-convert stx)
     (syntax-property stx 'convert))
+  (define (add-construct stx fn)
+    (set-stx-prop/preserved stx 'construct fn))
+  (define (get-construct stx)
+    (syntax-property stx 'construct))
   (define (ty->len ty)
     (regexp-match #px"([a-z]+)([0-9]+)" (type->str ty)))
   (define (get-base ty [ctx #'here])
@@ -106,12 +126,15 @@
      (datum->syntax ctx
       (string->symbol (car (regexp-match #px"[a-z]+" (type->str ty)))))))
   (define (vector-type? ty)
+    ;; TODO: and not pointer-type?
     (ty->len ty))
   (define (scalar-type? ty)
     (not (vector-type? ty))))
 
 (define-syntax-parser add-convertm
   [(_ stx fn) (add-convert #'stx #'fn)])
+(define-syntax-parser add-constructm
+  [(_ stx fn) (add-construct #'stx #'fn)])
 
 ;; TODO: reuse impls in model/reals.rkt ?
 (ro:define (to-bool v)
@@ -139,6 +162,45 @@
     (ro:apply ro:vector-immutable
       (ro:for/list ([i 3]) (to-float (ro:vector-ref v i))))]
    [else (ro:apply ro:vector-immutable (ro:make-list 3 (to-float v)))]))
+(ro:define (to-int2 v)
+  (ro:cond
+   [(ro:list? v)
+    (ro:apply ro:vector-immutable
+      (ro:for/list ([i 2]) (to-int (ro:list-ref v i))))]
+   [(ro:vector? v)
+    (ro:apply ro:vector-immutable
+      (ro:for/list ([i 2]) (to-int (ro:vector-ref v i))))]
+   [else
+    (ro:apply ro:vector-immutable
+      (ro:make-list 2 (to-int v)))]))
+(ro:define (to-int3 v)
+  (ro:cond
+   [(ro:list? v)
+    (ro:apply ro:vector-immutable
+      (ro:for/list ([i 3]) (to-int (ro:list-ref v i))))]
+   [(ro:vector? v)
+    (ro:apply ro:vector-immutable
+      (ro:for/list ([i 3]) (to-int (ro:vector-ref v i))))]
+   [else
+    (ro:apply ro:vector-immutable
+      (ro:make-list 3 (to-int v)))]))
+(ro:define (to-int4 v)
+  (ro:cond
+   [(ro:list? v)
+    (ro:apply ro:vector-immutable
+      (ro:for/list ([i 4]) (to-int (ro:list-ref v i))))]
+   [(ro:vector? v)
+    (ro:apply ro:vector-immutable
+      (ro:for/list ([i 4]) (to-int (ro:vector-ref v i))))]
+   [else
+    (ro:apply ro:vector-immutable
+      (ro:make-list 4 (to-int v)))]))
+(ro:define (mk-int2 x y)
+  (ro:#%app ro:vector-immutable (to-int x) (to-int y)))
+(ro:define (mk-int3 x y z)
+  (ro:#%app ro:vector-immutable (to-int x) (to-int y) (to-int z)))
+(ro:define (mk-int4 w x y z)
+  (ro:#%app ro:vector-immutable (to-int w) (to-int x) (to-int y) (to-int z)))
 (ro:define (to-int16 v)
   (ro:cond
    [(ro:list? v)
@@ -150,6 +212,8 @@
    [else
     (ro:apply ro:vector-immutable
       (ro:make-list 16 (to-int v)))]))
+(ro:define (to-int16* v)
+ (cl:pointer-cast v cl:int16))
 
 (define-named-type-alias bool
   (add-convertm rosette3:Bool to-bool))
@@ -157,11 +221,30 @@
   (add-convertm rosette3:Int to-int))
 (define-named-type-alias float
   (add-convertm rosette3:Num to-float))
+(define-named-type-alias char* rosette3:CString)
 
 (define-named-type-alias float3
   (add-convertm
    (rosette3:CVector rosette3:Num rosette3:Num rosette3:Num)
    to-float3))
+(define-named-type-alias int2
+  (add-constructm
+   (add-convertm
+    (rosette3:CVector rosette3:Int rosette3:Int)
+    to-int2)
+   mk-int2))
+(define-named-type-alias int3
+  (add-constructm
+   (add-convertm
+    (rosette3:CVector rosette3:Int rosette3:Int rosette3:Int)
+    to-int3)
+   mk-int3))
+(define-named-type-alias int4
+  (add-constructm
+   (add-convertm
+    (rosette3:CVector rosette3:Int rosette3:Int rosette3:Int rosette3:Int)
+    to-int4)
+   mk-int4))
 (define-named-type-alias int16
   (add-convertm
    (rosette3:CVector rosette3:Int rosette3:Int rosette3:Int rosette3:Int
@@ -169,8 +252,13 @@
                      rosette3:Int rosette3:Int rosette3:Int rosette3:Int
                      rosette3:Int rosette3:Int rosette3:Int rosette3:Int)
    to-int16))
-(define-named-type-alias void* rosette3:Unit)
+(define-type-constructor Pointer #:arity = 1)
 (define-named-type-alias void rosette3:CUnit)
+(define-named-type-alias void* (Pointer rosette3:CUnit))
+(define-named-type-alias int*
+  (Pointer int))
+(define-named-type-alias int16*
+  (add-convertm (Pointer int16) to-int16*))
 
 (define-typed-syntax synth-app
   [(_ (ty:type) e) ≫ ; cast
@@ -183,11 +271,146 @@
                  (format "cannot cast ~a to ~a: conversion fn not found"
                          (type->str #'ty-e) (type->str #'ty.norm))
    --------
-   [⊢ (convert e-) ⇒ ty.norm]]
+   [⊢ (ro:#%app convert e-) ⇒ ty.norm]]
+  [(_ ty:type e ...) ≫ ; construct
+   [⊢ e ≫ e- ⇒ ty-e] ...
+   ;; #:fail-unless (cast-ok? #'ty-e #'ty.norm #'e)
+   ;;               (format "cannot cast ~a to ~a"
+   ;;                       (type->str #'ty-e) (type->str #'ty.norm))
+   #:with construct (get-construct #'ty.norm)
+   #:fail-unless (syntax-e #'construct)
+                 (format "no constructor found for ~a type"
+                         (type->str #'ty.norm))
+   --------
+   [⊢ (ro:#%app construct e- ...) ⇒ ty.norm]]
+  [(_ ptr sel) ≫ ; applying ptr to one arg is selector
+   [⊢ ptr ≫ ptr- ⇒ ty-ptr]
+   #:when (pointer-type? #'ty-ptr)
+   #:do [(define split-ty (ty->len #'ty-ptr))]
+   #:when (and split-ty (= 3 (length split-ty)))
+   #:do [(define base-str (cadr split-ty))
+         (define len-str (caddr split-ty))]
+   #:with e-out #'(cl:pointer-ref ptr- sel)
+   #:with ty-out ((current-type-eval)
+                  (format-id #'here "~a~a"
+                             base-str len-str))
+;   #:with convert (get-convert #'ty-out)
+   --------
+   [⊢ e-out ⇒ ty-out]]
+  [(_ vec sel) ≫ ; applying vector to one arg is selector
+   [⊢ vec ≫ vec- ⇒ ty-vec]
+   #:when (vector-type? #'ty-vec)
+   #:with selector (cl:parse-selector #t #'sel stx)
+   #:do [(define split-ty (ty->len #'ty-vec))]
+   #:when (and split-ty (= 3 (length split-ty)))
+   #:do [(define base-str (cadr split-ty))
+         (define len-str (caddr split-ty))]
+   #:do [(define sels (length (stx->list #'selector)))]
+   #:with e-out (if (= sels 1)
+                    #'(ro:vector-ref vec- (ro:car 'selector))
+                    #'(for/list ([idx 'selector])
+                        (ro:vector-ref vec- idx)))
+   #:with ty-out ((current-type-eval)
+                  (if (= sels 1)
+                      (format-id #'here "~a" base-str)
+                      (format-id #'here "~a~a"
+                                 base-str (length (stx->list #'selector)))))
+   #:with convert (get-convert #'ty-out)
+   --------
+   [⊢ (ro:#%app convert e-out) ⇒ ty-out]]
+  [(_ f e ...) ≫
+   [⊢ f ≫ f- ⇒ (~C→ ty-in ... ty-out)]
+   [⊢ e ≫ e- ⇒ ty-e] ...
+   #:when (stx-andmap cast-ok? #'(ty-e ...) #'(ty-in ...))
+   --------
+   [⊢ (ro:#%app f- e- ...) ⇒ ty-out]]
   [(_ . es) ≫
    --------
    [≻ (rosette3:#%app . es)]])
 
+(define-syntax (⊢m stx)
+  (syntax-parse stx #:datum-literals (:)
+   [(_ e : τ) (assign-type #`e #`τ)]
+   [(_ e τ) (assign-type #`e #`τ)]))
+
+;; top-level fns --------------------------------------------------
+(define-typed-syntax procedure
+  [(_ ty-out:type (f [ty:type x:id] ...) e ...) ≫
+   #:with col (datum->syntax #f ':)
+   #:with arr (datum->syntax #f '->)
+   #:with (conv ...) (stx-map get-convert #'(ty.norm ...))
+   --------
+   [≻ #,(if (typecheck/un? #'ty-out #'void)
+            #'(rosette3:define (f [x col ty] ... arr ty-out)
+                               ;; TODO: this is deviating from rosette's impl
+                               ;; but I think it's a bug in rosette
+                               ;; otherwise it's unsound
+;                               (⊢ (ro:set! x (ro:a conv x)) void) ...
+                               (⊢m (ro:let ([x (ro:#%app conv x)] ...)
+                                     e ...
+                                     (rosette3:#%app rosette3:void))
+                                   ty-out))
+            #'(rosette3:define (f [x col ty] ... arr ty-out)
+;                               (⊢ (ro:set! x (ro:a conv x)) void) ...
+                               (⊢m (ro:let ([x (ro:#%app conv x)] ...)
+                                     (rosette3:#%app rosette3:void)
+                                     e ...)
+                                   ty-out)))]])
+(define-typed-syntax kernel
+  [(_ ty-out:type (f [ty:type x:id] ...) e ...) ≫
+   --------
+   [≻ (procedure ty-out (f [ty x] ...) e ...)]])
+   
+;; for and if statement --------------------------------------------------
+(define-typed-syntax if
+  [(_ test {then ...}  {else ...}) ≫
+   --------
+   [⊢ (ro:if (to-bool test)
+             (ro:let () then ... (ro:void)) 
+             (ro:let () else ... (ro:void))) ⇒ void]]
+  [(_ test {then ...}) ≫
+   --------
+   [≻ (if test {then ...} {})]])
+
+;(define-syntax-parameter range (syntax-rules ()))
+(define-typed-syntax (range e ...) ≫
+  [⊢ e ≫ e- ⇐ int] ...
+  --------
+  [⊢ (ro:#%app ro:in-range e- ...) ⇒ int]) 
+(define-typed-syntax for
+  [(_ [((~literal :) ty:type var:id (~datum in) rangeExpr) ...] e ...) ≫
+;   [⊢ rangeExpr ≫ rangeExpr- ⇒ _] ...
+   [[var ≫ var- : ty.norm] ... ⊢ [e ≫ e- ⇒ ty-e] ...]
+   --------
+   [⊢ (ro:for* ([var- rangeExpr] ...)
+               e- ... (ro:void)) ⇒ void]])
+
+
+;; need to redefine #%datum because rosette3:#%datum is too precise
+(define-typed-syntax #%datum
+  [(_ . b:boolean) ≫
+;   #:with ty_out (if (syntax-e #'b) #'True #'False)
+   --------
+   [⊢ (ro:#%datum . b) ⇒ bool]]
+  [(_ . n:integer) ≫
+   ;; #:with ty_out (let ([m (syntax-e #'n)])
+   ;;                 (cond [(zero? m) #'Zero]
+   ;;                       [(> m 0) #'PosInt]
+   ;;                       [else #'NegInt]))
+   --------
+   [⊢ (ro:#%datum . n) ⇒ int]]
+  [(#%datum . n:number) ≫
+   #:when (real? (syntax-e #'n))
+   --------
+   [⊢ (ro:#%datum . n) ⇒ float]]
+  [(_ . s:str) ≫
+   --------
+   [⊢ (ro:#%datum . s) ⇒ char*]]
+  [(_ . x) ≫
+   --------
+   [_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
+
+
 ;; : --------------------------------------------------
 (define-typed-syntax :
   [(_ ty:type x:id ...) ≫ ; special String case
@@ -201,6 +424,7 @@
   ;; TODO: vector types need a better representation
   ;; currently dissecting the identifier
   [(_ ty:type x:id ...) ≫
+   #:when (real-type? #'ty.norm)
    #:do [(define split-ty (ty->len #'ty))]
    #:when (and split-ty (= 3 (length split-ty)))
    #:do [(define base-str (cadr split-ty))
@@ -217,8 +441,9 @@
         (ro:define x- (ro:apply ro:vector-immutable x--)) ...
         (define-syntax- x
           (make-rename-transformer (assign-type #'x- #'ty.norm))) ...)]]
-  ;; scalar (ie non-vector) types
+  ;; real, scalar (ie non-vector) types
   [(_ ty:type x:id ...) ≫
+   #:when (real-type? #'ty.norm)
    #:with pred (get-pred #'ty.norm)
    #:fail-unless (syntax-e #'pred)
                  (format "no pred for ~a" (type->str #'ty))
@@ -227,7 +452,16 @@
    [≻ (begin-
         (define-syntax- x
           (make-rename-transformer (assign-type #'x- #'ty.norm))) ...
-        (ro:define-symbolic* x- pred) ...)]])
+        (ro:define-symbolic* x- pred) ...)]]
+  ;; else init to NULLs
+  [(_ ty:type x:id ...) ≫
+;   #:when (not (real-type? #'ty.norm))
+   #:with (x- ...) (generate-temporaries #'(x ...))
+   --------
+   [≻ (begin-
+        (define-syntax- x
+          (make-rename-transformer (assign-type #'x- #'ty.norm))) ...
+        (ro:define x- cl:NULL) ...)]])
 
 ;; ?: --------------------------------------------------
 (define-typed-syntax ?:
@@ -280,16 +514,24 @@
                  (format "cannot cast ~a to ~a"
                          (type->str #'ty-e) (type->str #'ty-x))
    --------
-   [⊢ (ro:set! x- (synth-app (ty-x) e-)) ⇒ void]])
-(define-typed-syntax +=
-  [(_ x:id e) ≫
+   [⊢ (ro:set! x- (synth-app (ty-x) e-)) ⇒ void]]
+  ;; selector can be list of numbers or up to wxyz for vectors of length <=4
+  [(_ [x:id sel] e) ≫
    [⊢ x ≫ x- ⇒ ty-x]
    [⊢ e ≫ e- ⇒ ty-e]
-   #:fail-unless (cast-ok? #'ty-e #'ty-x stx)
-                 (format "cannot cast ~a to ~a"
-                         (type->str #'ty-e) (type->str #'ty-x))
+   #:with out-e (if (pointer-type? #'ty-x)
+                    #'(ro:begin
+                       (cl:pointer-set! x- sel e-)
+                       x-)
+                    (with-syntax ([selector (cl:parse-selector #f #'sel stx)])
+                    #`(ro:let ([out (ro:vector-copy x-)])
+                      #,(if (= 1 (length (stx->list #'selector)))
+                            #`(ro:vector-set! out (car 'selector) e-)
+                            #'(ro:for ([idx 'selector] [v e-])
+                                (ro:vector-set! out idx v)))
+                      out)))
    --------
-   [⊢ (ro:set! x- (+ x- (synth-app (ty-x) e-))) ⇒ void]])
+   [⊢ (ro:set! x- out-e) ⇒ void]])
 
 (define-typed-syntax !
   [(_ e) ≫
@@ -357,8 +599,45 @@
             #'(convert
                (ro:let ([a (convert e1-)][b (convert e2-)])
                  (ro:for/list ([v1 a][v2 b])
-                   (base-convert (ro:+ v1 v2)))))) ⇒ ty-out]])
+                   (base-convert (cl:+ v1 v2)))))) ⇒ ty-out]])
 
+(define-typed-syntax +=
+  [(_ x e) ≫
+   --------
+   [≻ (= x (+ x e))]])
+   
+(define-typed-syntax %
+  [(_ e1 e2) ≫
+   [⊢ e1 ≫ e1- ⇒ ty1]
+   [⊢ e2 ≫ e2- ⇒ ty2]
+   ;; #:when (real-type? #'ty1)
+   ;; #:when (real-type? #'ty2)
+   #:with ty-out (common-real-type #'ty1 #'ty2)
+   #:with convert (get-convert #'ty-out)
+   #:with ty-base (get-base #'ty-out)
+   #:with base-convert (get-convert #'ty-base)
+   --------
+   [⊢ #,(if (scalar-type? #'ty-out)
+            #'(convert (cl:% (synth-app (ty-out) e1-)
+                             (synth-app (ty-out) e2-)))
+            #'(convert
+               (ro:let ([a (convert e1-)][b (convert e2-)])
+                 (ro:for/list ([v1 a][v2 b])
+                   (base-convert (cl:% v1 v2)))))) ⇒ ty-out]])
+
+(define-typed-syntax %=
+  [(_ x e) ≫
+   --------
+   [≻ (= x (% x e))]])
+#;(define-typed-syntax %=
+  [(_ x:id e) ≫
+   [⊢ x ≫ x- ⇒ ty-x]
+   [⊢ e ≫ e- ⇒ ty-e]
+   #:fail-unless (cast-ok? #'ty-e #'ty-x stx)
+                 (format "cannot cast ~a to ~a"
+                         (type->str #'ty-e) (type->str #'ty-x))
+   --------
+   [⊢ (ro:set! x- (% x- (synth-app (ty-x) e-))) ⇒ void]])
 
 #;(define-typed-syntax &&
   [(_ e1 e2) ≫
diff --git a/turnstile/examples/tests/rosette/rosette3/synthcl3-tests.rkt b/turnstile/examples/tests/rosette/rosette3/synthcl3-tests.rkt
index ce01be7..cd9307a 100644
--- a/turnstile/examples/tests/rosette/rosette3/synthcl3-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette3/synthcl3-tests.rkt
@@ -15,9 +15,9 @@
 ;; (check-type (expression? x) : CBool -> #f)
 ;; (check-type (constant? x) : CBool -> #t)
 
-;; (assert (+ x 1))
-;; (assert (% (+ x 2) 3))
-;; (assert (!= x 2))
+(assert (+ x 1))
+(assert (% (+ x 2) 3))
+(assert (!= x 2))
 
 (check-type "" : char*)
 (: char* y)
@@ -76,9 +76,10 @@
      (ro:a ro:integer->real x)
      (ro:a ro:integer->real x)))
 
-(: int16 u)
-
+(: int16 u u2)
+(= u2 u)
 (check-type u : int16 -> u)
+(check-type u2 : int16 -> u)
 
 (check-type NULL : void* -> NULL)
 (check-type ((int16) v) : int16
@@ -110,58 +111,103 @@
  ;;     (ro:a ro:+ 2.0 (ro:a ro:vector-ref z 1))
  ;;     (ro:a ro:+ 2.0 (ro:a ro:vector-ref z 2))))
 
-;; (%= x 3)
-;; x
+(%= x 3)
+(check-type x : int -> 0)
 
-;; (int3 4 5 6)
-;; (= [u xyz] (int3 4 5 6))
-;; u
+(check-type (int3 4 5 6) : int3
+ -> (ro:a ro:vector-immutable 4 5 6))
 
-;; (+ (int3 1 2 3) 4)
+(= [u xyz] (int3 4 5 6))
 
-;; ((int4 5 6 7 8) s03)
+(check-type u : int16
+ -> (ro:let ([out (ro:a ro:vector-copy u2)])
+            (ro:a ro:vector-set! out 0 4)
+            (ro:a ro:vector-set! out 1 5)
+            (ro:a ro:vector-set! out 2 6)
+            out))
 
-;; (if x {}{})
+(check-type (+ (int3 1 2 3) 4) : int3
+ -> (ro:a ro:vector-immutable 5 6 7))
 
-;; (if x 
-;;     { (= [u sf] 10) }
-;;     { (= [u sf] 9) }
-;; )
-;; u
+(check-type ((int4 5 6 7 8) s03) : int2
+ -> (ro:a ro:vector-immutable 5 8))
 
-;; (if (! x) 
-;;     { (: int g) (= g 3) (= [u sf] g) }
-;;     { (= [u sf] 9) }
-;; )
-;; u
+(check-type (if x {}{}) : void -> (= x x))
 
-;; (for [(: int i in (range 0 4 1))] )
-;; (for [(: int i in (range 0 4 1))] 
-;;   (if (! x)
-;;       { (: int g) (= g i) (+= [u sf] g)} )
-;;   )
-;; u
+(= u2 u)
+(if x 
+    { (= [u sf] 10) }
+    { (= [u sf] 9) }
+)
+(check-type u : int16
+ -> (ro:let ([out (ro:a ro:vector-copy u2)])
+            (ro:a ro:vector-set! out 15 9)
+            out))
+
+(if (! x) 
+    { (: int g) (= g 3) (= [u sf] g) }
+    { (= [u sf] 9) }
+)
+(check-type u : int16
+ -> (ro:let ([out (ro:a ro:vector-copy u2)])
+            (ro:a ro:vector-set! out 15 3)
+            out))
 
 
-;; (: int16* w)
-;; (= w ((int16*) (malloc 32)))
-;; (= [w 0] 1)
-;; (= [w 1] 2)
-;; w
-;; [w 0]
-;; [w 1]
+(check-type (for [(: int i in (range 0 4 1))] ) : void -> (= x x))
 
-;; (get_work_dim)
+(check-type (! x) : bool -> #t)
+(: int g1)
+(= g1 3)
+(check-type (u sf) : int -> 3)
+(+= [u sf] g1)
+(check-type u : int16
+ -> (ro:let ([out (ro:a ro:vector-copy u2)])
+            (ro:a ro:vector-set! out 15 6)
+            out))
+(= [u sf] 3)
 
-;; (procedure void (nop1))
-;; (nop1)
-;; (kernel void (nop2))
-;; (nop2)
+(for [(: int i in (range 0 4 1))]
+  (if (! x)
+      { (: int g) (= g i) (+= [u sf] g)} )
+  )
+(check-type u : int16
+ -> (ro:let ([out (ro:a ro:vector-copy u2)])
+            (ro:a ro:vector-set! out 15 9)
+            out))
 
-;; (procedure int (int_iden [int x]) x)
-;; (int_iden ((int) 4.5))
-;; (int_iden #t)
-;; (int_iden 4.5)
+(: int16* w)
+(check-type w : int16* -> NULL)
+(check-type (malloc 32) : void*)
+(= w ((int16*) (malloc 32)))
+; TODO: how to check this?
+;#x0#(0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)
+(check-type w : int16*)
+(= [w 0] 1)
+;#x0#(1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)
+(= [w 1] 2)
+;#x0#(1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2)
+(check-type [w 0] : int16
+ -> (ro:a ro:vector-immutable 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1))
+(check-type [w 1] : int16
+ -> (ro:a ro:vector-immutable 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2))
+
+(check-type (get_work_dim) : int -> 0)
+
+(procedure void (nop1))
+(check-type (nop1) : void -> (= x x))
+(kernel void (nop2))
+(check-type (nop2) : void -> (= x x))
+
+(procedure int (int_iden [int x]) x)
+;; huh? these are unsound?
+;; but match rosette's implementation
+;; specifically, procedure does not coerce (but kernel does)
+(check-type (int_iden ((int) 4.5)) : int -> 4)
+;; (check-type (int_iden #t) : int -> #t)
+;; (check-type (int_iden 4.5) : int -> 4.5)
+(check-type (int_iden #t) : int -> 1)
+(check-type (int_iden 4.5) : int -> 4)