From 8e2710e133449b04b4a5297999e612fff9f30449 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 4 Nov 2016 17:14:22 -0400
Subject: [PATCH] synth3: start assignment

---
 turnstile/examples/rosette/synthcl3.rkt       | 72 ++++++++++++++++---
 .../tests/rosette/rosette3/synthcl3-tests.rkt | 39 +++++++---
 2 files changed, 93 insertions(+), 18 deletions(-)

diff --git a/turnstile/examples/rosette/synthcl3.rkt b/turnstile/examples/rosette/synthcl3.rkt
index f7677f6..bab15ae 100644
--- a/turnstile/examples/rosette/synthcl3.rkt
+++ b/turnstile/examples/rosette/synthcl3.rkt
@@ -1,10 +1,11 @@
 #lang turnstile
-(extends "rosette3.rkt" #:except ! #%app || &&) ; typed rosette
+(extends "rosette3.rkt" #:except ! #%app || && void = +) ; typed rosette
 (require ;(prefix-in ro: (except-in rosette verify sqrt range print)) ; untyped 
   (prefix-in ro: rosette)
 ;             define-symbolic* #%datum define if ! = number? boolean? cond ||))
   (prefix-in cl: sdsl/synthcl/model/operators)
-  (prefix-in cl: sdsl/synthcl/model/errors))
+  (prefix-in cl: sdsl/synthcl/model/errors)
+  (prefix-in cl: sdsl/synthcl/model/memory))
 
 (begin-for-syntax
   (define (mk-cl id) (format-id id "cl:~a" id))
@@ -18,8 +19,10 @@
 ;          [rosette3:Int int]   ; symbolic
 ;          [rosette3:Num float] ; symbolic
           [rosette3:CString char*]) ; always concrete
-         bool int float float3 int16
-         : ! ?: ==
+         bool int float float3 int16 void void*
+         : ! ?: == +
+         ;; assignment ops
+         = +=
          (typed-out
           ;; need the concrete cases for literals;
           ;; alternative is to redefine #%datum to give literals symbolic type
@@ -29,6 +32,7 @@
                          (C→ CNum CNum CNum CBool)
                          (C→ Num Num Bool)
                          (C→ Num Num Num Bool))]
+          [NULL : void*]
           #;[== : (Ccase-> (C→ CNum CNum CBool)
                          (C→ CNum CNum CNum CBool)
                          (C→ Num Num Bool)
@@ -97,6 +101,10 @@
     (syntax-property stx 'convert))
   (define (ty->len ty)
     (regexp-match #px"([a-z]+)([0-9]+)" (type->str ty)))
+  (define (get-base ty [ctx #'here])
+    ((current-type-eval)
+     (datum->syntax ctx
+      (string->symbol (car (regexp-match #px"[a-z]+" (type->str ty)))))))
   (define (vector-type? ty)
     (ty->len ty))
   (define (scalar-type? ty)
@@ -131,15 +139,17 @@
     (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-int16 v) v
-           #;(ro:cond
+(ro:define (to-int16 v)
+  (ro:cond
    [(ro:list? v)
     (ro:apply ro:vector-immutable
       (ro:for/list ([i 16]) (to-int (ro:list-ref v i))))]
    [(ro:vector? v)
     (ro:apply ro:vector-immutable
       (ro:for/list ([i 16]) (to-int (ro:vector-ref v i))))]
-   [else (ro:apply ro:vector-immutable (ro:make-list 16 (to-float v)))]))
+   [else
+    (ro:apply ro:vector-immutable
+      (ro:make-list 16 (to-int v)))]))
 
 (define-named-type-alias bool
   (add-convertm rosette3:Bool to-bool))
@@ -159,6 +169,8 @@
                      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-named-type-alias void rosette3:CUnit)
 
 (define-typed-syntax synth-app
   [(_ (ty:type) e) ≫ ; cast
@@ -175,7 +187,8 @@
   [(_ . es) ≫
    --------
    [≻ (rosette3:#%app . es)]])
-   
+
+;; : --------------------------------------------------
 (define-typed-syntax :
   [(_ ty:type x:id ...) ≫ ; special String case
    #:when (rosette3:CString? #'ty.norm)
@@ -216,6 +229,7 @@
           (make-rename-transformer (assign-type #'x- #'ty.norm))) ...
         (ro:define-symbolic* x- pred) ...)]])
 
+;; ?: --------------------------------------------------
 (define-typed-syntax ?:
   [(_ e e1 e2) ≫
    [⊢ e ≫ e- ⇐ bool]
@@ -245,7 +259,6 @@
                 (base-convert (ro:vector-ref c idx))))))
       ⇒ ty-out]]
   [(_ e e1 e2) ≫ ; should be scalar
-   #:when (displayln 1)
    [⊢ e ≫ e- ⇒ ty]
    #:fail-unless (cast-ok? #'ty #'bool #'e)
                  (format "cannot cast ~a to bool" (type->str #'ty))
@@ -257,6 +270,27 @@
              (synth-app (ty-out) e1-)
              (synth-app (ty-out) e2-)) ⇒ ty-out]])
 
+;; = --------------------------------------------------
+;; assignment
+(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- (synth-app (ty-x) e-)) ⇒ void]])
+(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 !
   [(_ e) ≫
    [⊢ e ≫ e- ⇐ bool]
@@ -306,6 +340,26 @@
    --------
    [⊢ (to-int (cl:== e1- e2-)) ⇒ int]])
 
+(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 (ro:+ v1 v2)))))) ⇒ ty-out]])
+
+
 #;(define-typed-syntax &&
   [(_ e1 e2) ≫
    [⊢ e1 ≫ e1- ⇐ bool]
diff --git a/turnstile/examples/tests/rosette/rosette3/synthcl3-tests.rkt b/turnstile/examples/tests/rosette/rosette3/synthcl3-tests.rkt
index 3f314e0..ce01be7 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)
@@ -80,14 +80,35 @@
 
 (check-type u : int16 -> u)
 
-;; NULL
-;; ((int16) v)
+(check-type NULL : void* -> NULL)
+(check-type ((int16) v) : int16
+ ->
+ (ro:a ro:vector-immutable
+  (ro:a ro:real->integer v) (ro:a ro:real->integer v) (ro:a ro:real->integer v)
+  (ro:a ro:real->integer v) (ro:a ro:real->integer v) (ro:a ro:real->integer v)
+  (ro:a ro:real->integer v) (ro:a ro:real->integer v) (ro:a ro:real->integer v)
+  (ro:a ro:real->integer v) (ro:a ro:real->integer v) (ro:a ro:real->integer v)
+  (ro:a ro:real->integer v) (ro:a ro:real->integer v) (ro:a ro:real->integer v)
+  (ro:a ro:real->integer v)))
 
-;; (= x 3.4)
-;; x
+(= x 3.4)
+(check-type x : int -> 3)
 
-;; (+= z 2)
-;; z
+(check-type ((float3) 2) : float3 -> (ro:a ro:vector-immutable 2.0 2.0 2.0))
+
+;; vector addition
+(check-type (+ z 2) : float3
+ -> (ro:a ro:vector-immutable
+     (ro:a ro:+ 2.0 (ro:a ro:vector-ref z 0))
+     (ro:a ro:+ 2.0 (ro:a ro:vector-ref z 1))
+     (ro:a ro:+ 2.0 (ro:a ro:vector-ref z 2))))
+
+(+= z 2)
+(check-type z : float3 -> z)
+ ;; -> (ro:a ro:vector-immutable
+ ;;     (ro:a ro:+ 2.0 (ro:a ro:vector-ref z 0))
+ ;;     (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