#lang rosette/safe

(require rosette/lib/synthax)
(current-bitwidth #f)

; define our grammar
(define-grammar (expr x y)
   [exp (choose
          x y (??)
          ((choose + - *) (exp) (exp))
         )
   ]
)

(define (targetexpr x y)
  (expr x y #:depth 3))

; --------
; let's do our I/O examples from last class

(print-forms
 (synthesize
  #:forall '()
  #:guarantee (assert (&&
                       (equal? (targetexpr 3 7) 23)
                       (equal? (targetexpr 4 4) 19)
                       (equal? (targetexpr 2 12) 31)))))

; --------
; let's do a logical specification

(define-symbolic x y integer?)
(print-forms
 (synthesize
  #:forall (list x y)
  #:guarantee (assert (equal? (targetexpr x y) (+ x y)))))

; --------
; ACTIVITY 1:
; what if we want a program that raises the input to the third power?
; note: in racket, you use expt for raising to power

(define (targetexpr2 x y)
  (expr x y #:depth 2))

(print-forms
 (synthesize
  #:forall (list x y)
  #:guarantee (assert (equal? (targetexpr2 x y) (expt x 3)))))

; --------
; ACTIVITY 2:
; now make any variant that uses a function you've defined

(define (add-2 x y)
  (+ x y 2))

; a new grammar
(define-grammar (expr2 x y)
   [exp (choose
          x y (??)
          ((choose + - * add-2) (exp) (exp))
         )
   ]
)

(define (targetexpr3 x y)
  (expr2 x y #:depth 1))

(print-forms
 (synthesize
  #:forall (list x y)
  #:guarantee (assert (equal? (targetexpr3 x y) (+ x y 2)))))

; --------
; ACTIVITY 3:
; now make a variant that can use + and - but also square
; remove access to * !

; a new grammar
(define-grammar (expr3 x y)
   [exp (choose
          x y (??)
          (expt (exp) 2)
          ((choose + -) (exp) (exp))
         )
   ]
)

(define (targetexpr4 x y)
  (expr3 x y #:depth 2))

(print-forms
 (synthesize
  #:forall (list x y)
  #:guarantee (assert (equal? (targetexpr4 x y) (expt x 2)))))