common.rkt

#lang rosette

(require rosette/lib/synthax
         (only-in rosette/base/util/array reshape))

(provide generate-symbolic define-synthax-rule
         (all-from-out rosette/lib/synthax))

;; Fundamental. If you want bitvectors, use the bv explicit types
(current-bitwidth #f)

;; Instead of (define (get-sym) (define-symbolic* x <type>) x)
;; Use (generate-symbolic <type>)
;;
;; also works with (generate-symbolic <type> [dim ...]) for multidimensional lists
;; just like define-symbolic. Yes that's a thing you can do. Undocumented of course.
;;
(define-syntax (generate-symbolic stx)
  (syntax-case stx ()
    [(_ type)
     (syntax/loc stx
       (with-syntax ([(var) (generate-temporaries #'(gen))])
         (constant (list #'var ((current-oracle) #'var)) type)))]
    [(_ type [ k ... ])
     (syntax/loc stx
       (with-syntax ([(var) (generate-temporaries #'(gen))])
         (reshape (list k ...) (for/list ([i (in-range (* k ...))])
                                 (generate-symbolic type)))))]))

;; (define-synthax ...) has a confusing number of parens.
;; This allows you to not need nearly as many when your rule only has one pattern.
(define-syntax-rule (define-synthax-rule (id pats ...) expr)
  (define-synthax id
    ([(_ pats ...) expr])))