(in-package "ACL2")

(defun expand-defproperty/make-conjecture (hyps body)
  (cond
   ((endp hyps) body)
   ((endp (cdr hyps)) `(implies ,(car hyps) ,body))
   (else `(implies (and ,@hyps) ,body))))

(defun expand-defproperty/trivial-hypothesis? (hyp)
  (equal hyp t))

(defun expand-defproperty/add-hypothesis (hyp hyps)
  (if (expand-defproperty/trivial-hypothesis? hyp) hyps (cons hyp hyps)))

(defun expand-defproperty/bindings->hypotheses (bindings)
  (cond
   ((endp bindings) nil)
   ((consp bindings)
    (expand-defproperty/add-hypothesis
     (cadar bindings)
     (expand-defproperty/bindings->hypotheses (cdr bindings))))))

(defmacro defproperty (name bindings body &rest rest)
  `(defthm ,name
     ,(expand-defproperty/make-conjecture
       (expand-defproperty/bindings->hypotheses bindings)
       body)
     ,@rest))

(defmacro defrandom (name args body)
  `(encapsulate () (program) (defun ,name ,args ,body)))

(defrandom random-boolean () t)
(defrandom random-symbol () 'symbol)
(defrandom random-char () #\c)
(defrandom random-string () "string")
(defrandom random-number () 0)
(defrandom random-rational () 0)
(defrandom random-integer () 0)
(defrandom random-natural () 0)
(defrandom random-data-size () 1)
(defrandom random-between (lo hi) lo)
(defrandom random-atom () nil)
(defrandom random-sexp () (cons 'sexp nil))

(defmacro random-case (first second &rest rest)
  (declare (ignore rest))
  `(if (random-boolean) ,first ,second))

(defmacro random-sexp-of (atom &key size)
  (declare (ignore size))
  `(if (random-boolean) (cons ,atom ,atom) ,atom))

(defmacro random-list-of (elem &key size)
  (declare (ignore size))
  `(if (random-boolean) (list ,elem) nil))

(defun check-properties () t)