build-enumcalls

(in-package "CGEN")

(include-book "basis")

(include-book "utilities")

(include-book "type")

(include-book "infer-enum-shape")

(defrec enum-info%
  (domain-size category
    expr
    expr2
    min-rec-depth
    max-rec-depth)
  nil)

(defun enum-info%-p
  (v)
  (declare (xargs :guard t))
  (case-match v
    (('enum-info% domain-size
       category
       expr
       expr2
       min-rec-depth
       max-rec-depth) (and (fixnump domain-size)
        (fixnump min-rec-depth)
        (fixnump max-rec-depth)
        (member-eq category
          '(:singleton :function :defconst :numeric-range :empty))
        (pseudo-termp expr)
        (pseudo-termp expr2)))))

(defun abs/complex
  (c)
  (declare (xargs :guard (complex/complex-rationalp c)))
  (complex (abs (realpart c)) (abs (imagpart c))))

(defun abs/acl2-number
  (x)
  (declare (xargs :guard (acl2-numberp x)))
  (if (complex/complex-rationalp x)
    (abs/complex x)
    (abs x)))

(defun mod/complex
  (c m)
  (declare (xargs :guard (and (rationalp m)
        (> m 0)
        (complex/complex-rationalp c))))
  (complex (mod (realpart c) m)
    (imagpart c)))

(defun mod/acl2-number
  (x m)
  (declare (xargs :guard (and (acl2-numberp x)
        (rationalp m)
        (> m 0))))
  (if (complex/complex-rationalp x)
    (mod/complex x m)
    (mod x m)))

(defun make-numeric-range-enum-info
  (size exp exp2)
  (make enum-info%
    :domain-size size
    :min-rec-depth 0
    :max-rec-depth 30
    :category :numeric-range :expr exp
    :expr2 exp2))

(include-book "acl2s/defdata/builtin-combinators" :dir :system)

(def make-range-enum-info%
  (interval integer-p)
  (decl :sig ((non-empty-non-universal-interval-p booleanp) ->
      enum-info%-p)
    :doc "given tau-interval interval construct an enum-info% rec with appropriate enum calls")
  (b* ((lo (access tau-interval interval :lo)) (hi (access tau-interval interval :hi))
      (lo-rel (access tau-interval interval :lo-rel))
      (hi-rel (access tau-interval interval :hi-rel))
      (domain (if integer-p
          'integer
          'rational))
      (dom-size (if (and lo hi integer-p)
          (- (if hi-rel
              (1- hi)
              hi)
            (if lo-rel
              (1+ lo)
              lo))
          't)))
    (make-numeric-range-enum-info dom-size
      (make-enum-body-for-range 'r
        domain
        lo
        hi
        lo-rel
        hi-rel)
      (make-enum/acc-body-for-range 'r
        'seed.
        domain
        lo
        hi
        lo-rel
        hi-rel))))

(def get-enum-info%
  (type range vl wrld)
  (decl :sig ((possible-defdata-type-p tau-interval
       fixnum
       plist-world) ->
      enum-info%-p)
    :doc "to fill")
  (declare (xargs :verify-guards nil))
  (if (possible-constant-value-p type)
    (make enum-info%
      :domain-size 1
      :min-rec-depth 0
      :max-rec-depth 1
      :category :singleton :expr type
      :expr2 `(mv ',TYPE seed.))
    (let ((entry (assoc-eq type
           (table-alist 'type-metadata-table wrld))))
      (if entry
        (b* ((al (cdr entry)) (ti.test-enumerator (cdr (assoc-eq :enum/test al)))
            (ti.test-enumerator/acc (cdr (assoc-eq :enum/test/acc al)))
            (ti.enumerator (cdr (assoc-eq :enumerator al)))
            (ti.enum-uniform (cdr (assoc-eq :enum/acc al)))
            (ti.size (cdr (assoc-eq :domain-size al)))
            (ti.pred (cdr (assoc-eq :predicate al)))
            (ti.min (cdr (assoc-eq :min-rec-depth al)))
            (ti.max (cdr (assoc-eq :max-rec-depth al)))
            (ti.def (cdr (assoc-eq :def al)))
            ((when (equal 0 ti.size)) (prog2$ (cw? (verbose-stats-flag vl)
                  "~|Cgen/Error: size in type-info ~x0 is 0.~%"
                  (cdr entry))
                (make enum-info%
                  :domain-size 0
                  :min-rec-depth 0
                  :max-rec-depth 1
                  :category :empty :expr nil
                  :expr2 nil)))
            ((unless (or (eq 't ti.size) (natp ti.size))) (prog2$ (cw? (normal-output-flag vl)
                  "~|Cgen/Error: size in type-info ~x0 should be a natural number or T.~%"
                  (cdr entry))
                (make enum-info%
                  :domain-size 0
                  :min-rec-depth 0
                  :max-rec-depth 1
                  :category :empty :expr nil
                  :expr2 nil)))
            ((when (or (and (consp ti.def)
                   (eq 'range (car ti.def))
                   (range-subtype-p range
                     (get-tau-int (cadr ti.def)
                       (third ti.def))))
                 (and (subtype-p ti.pred
                     'acl2-numberp
                     wrld)
                   (non-empty-non-universal-interval-p range)))) (make-range-enum-info% range
                (subtype-p ti.pred 'integerp wrld))))
          (if ti.test-enumerator
            (cond ((allows-arity ti.test-enumerator
                 1
                 wrld) (make enum-info%
                  :domain-size 't
                  :min-rec-depth 0
                  :max-rec-depth 30
                  :category :function :expr (list ti.test-enumerator 'r)
                  :expr2 (list ti.test-enumerator/acc 'm 'seed.)))
              (t (prog2$ (cw? (normal-output-flag vl)
                    "~|Cgen/Error: ~x0 should be an enum function of arity 1.~%"
                    ti.test-enumerator)
                  (make enum-info%
                    :domain-size 0
                    :min-rec-depth 0
                    :max-rec-depth 0
                    :category :empty :expr nil
                    :expr2 nil))))
            (if (eq 't ti.size)
              (make enum-info%
                :domain-size ti.size
                :min-rec-depth ti.min
                :max-rec-depth ti.max
                :category :function :expr (list ti.enumerator 'r)
                :expr2 (list ti.enum-uniform 'm 'seed.))
              (let ((stored-defconst (acl2-getprop ti.enumerator 'const wrld)))
                (if stored-defconst
                  (b* ((values (second stored-defconst)) (len-v (len values))
                      ((unless (posp len-v)) (prog2$ (cw? (normal-output-flag vl)
                            "~|Cgen/Error: stored-defconst ~x0 has 0 values~%"
                            stored-defconst)
                          (make enum-info%
                            :domain-size 0
                            :min-rec-depth 0
                            :max-rec-depth 0
                            :category :empty :expr nil
                            :expr2 nil))))
                    (make enum-info%
                      :domain-size len-v
                      :min-rec-depth 0
                      :max-rec-depth 30
                      :category (if (= len-v 1)
                        :singleton :defconst)
                      :expr (if (= len-v 1)
                        `',(CAR VALUES)
                        `(nth (mod r ,CGEN::LEN-V) ,CGEN::TI.ENUMERATOR))
                      :expr2 (if (= len-v 1)
                        `(mv ',(CAR VALUES) seed.)
                        `(mv (nth (mod seed. ,CGEN::LEN-V) ,CGEN::TI.ENUMERATOR)
                          seed.))))
                  (if (allows-arity ti.enumerator 1 wrld)
                    (make enum-info%
                      :domain-size ti.size
                      :min-rec-depth ti.min
                      :max-rec-depth ti.max
                      :category :function :expr (list ti.enumerator 'r)
                      :expr2 (list ti.enum-uniform 'm 'seed.))
                    (prog2$ (cw? (normal-output-flag vl)
                        "~|Cgen/Error: ~x0 is neither one of constant, an enum function or a values defconst.~%"
                        ti.enumerator)
                      (make enum-info%
                        :domain-size 0
                        :category :empty :expr nil
                        :expr2 nil))))))))
        (let* ((vsym (modify-symbol "*" type "-VALUES*")) (values (second (acl2-getprop vsym 'const wrld))))
          (if values
            (let ((len-v (len values)))
              (make enum-info%
                :domain-size len-v
                :min-rec-depth 0
                :max-rec-depth 30
                :category (if (= len-v 1)
                  :singleton :defconst)
                :expr (if (= len-v 1)
                  `',(CAR VALUES)
                  `(nth (mod r ,CGEN::LEN-V) ,CGEN::VSYM))
                :expr2 (if (= len-v 1)
                  `(mv ',(CAR VALUES) seed.)
                  `(mv (nth (mod seed. ,CGEN::LEN-V) ,CGEN::VSYM)
                    seed.))))
            (let ((esym (modify-symbol "NTH-" type "")))
              (cond ((allows-arity esym 1 wrld) (make enum-info%
                    :domain-size t
                    :min-rec-depth 0
                    :max-rec-depth 30
                    :category :function :expr `(,CGEN::ESYM r)
                    :expr2 `(mv-let (r seed.)
                      (random-natural-seed seed.)
                      (mv (,CGEN::ESYM r) seed.))))
                (t (prog2$ (cw? (normal-output-flag vl)
                      "~|Cgen/Error: ~x0 doesnt appear to be a type.~%"
                      type)
                    (make enum-info%
                      :domain-size 0
                      :category :empty :expr nil
                      :expr2 nil)))))))))))

(defun symbol-unsigned-60bits-alistp
  (v)
  (declare (xargs :guard t))
  (if (atom v)
    (null v)
    (and (consp (car v))
      (symbolp (caar v))
      (unsigned-60bits-p (cdar v))
      (symbol-unsigned-60bits-alistp (cdr v)))))

(defthm symbol-unsigned-60bits-alistp-forwards-to-symbol-alistp
  (implies (symbol-unsigned-60bits-alistp x)
    (symbol-alistp x))
  :rule-classes :forward-chaining)

(defun |next BE args|
  (be.)
  "naive bounded exhaustive enumeration."
  (declare (xargs :guard (and (true-listp be.)
        (consp be.)
        (symbol-alistp be.))))
  (b* (((cons v m) (car be.)) (m~ (1+ (nfix m))))
    (append (cdr be.) (list (cons v m~)))))

(def make-guard-var-assoc-eq
  (vars alst)
  (decl :sig ((symbol-alistp symbol) -> all)
    :doc "helper function to make-next-sigma")
  (if (endp vars)
    nil
    (cons `(assoc-eq ',(CAR CGEN::VARS) ,CGEN::ALST)
      (make-guard-var-assoc-eq (cdr vars) alst))))

(def cs%-enumcalls-defdata
  (cs% vl wrld)
  (decl :sig ((cs%-p fixnump plist-worldp) ->
      (mv fixnum
        (cons pseudo-termp pseudo-termp)))
    :doc "see cs%-enumcalls")
  (declare (xargs :verify-guards nil))
  (case-match cs%
    (('cs% defdata-type
       &
       &
       range
       &
       &) (b* ((enum-info% (get-enum-info% defdata-type
             range
             vl
             wrld)))
        (mv (access enum-info% domain-size)
          (access enum-info% min-rec-depth)
          (access enum-info% max-rec-depth)
          (list (access enum-info% expr)
            (access enum-info% expr2)))))
    (& (prog2$ (cw? (normal-output-flag vl)
          "~|Cgen/Error: BAD record cs% passed to cs%-enumcalls")
        (mv 0 0 0 nil)))))

(def cs%-enumcalls
  (cs% vl wrld bound-vars)
  (decl :sig ((cs%-p fixnump
       plist-worldp
       symbol-listp) ->
      (mv fixnum
        (cons pseudo-termp pseudo-termp)))
    :doc "for each cs% record we translate it into the a (mv
  size min-rec-depth max-rec-depth (list enumcall enumcall2)), 
  where the enumcall is an expression
  that when evaluated gives a value (with random distribution) of
  correct type/constraint and size is the size of the type i.e the set
  of value satisfied by the constraint. enumcall2 is a similar
  expression but with the random seed accumulated/threaded
  uniformly. Return value of (mv 0 nil) stands for an error and is
  recognized by the caller function as such.")
  (declare (xargs :verify-guards nil))
  (case-match cs%
    (('cs% defdata-type
       &
       'empty-eq-constraint
       range
       'empty-mem-constraint
       &) (b* ((enum-info% (get-enum-info% defdata-type
             range
             vl
             wrld)))
        (mv (access enum-info% domain-size)
          (access enum-info% min-rec-depth)
          (access enum-info% max-rec-depth)
          (list (access enum-info% expr)
            (access enum-info% expr2)))))
    (('cs% defdata-type
       &
       eq-constraint
       range
       'empty-mem-constraint
       &) (b* ((?eq-vs (all-vars eq-constraint)) (?remaining (set-difference-eq eq-vs bound-vars)))
        (if remaining
          (b* ((enum-info% (get-enum-info% defdata-type
                 range
                 vl
                 wrld)))
            (mv (access enum-info% domain-size)
              (access enum-info% min-rec-depth)
              (access enum-info% max-rec-depth)
              (list (access enum-info% expr)
                (access enum-info% expr2))))
          (mv 1
            0
            1
            (list eq-constraint
              (list 'mv eq-constraint 'seed.))))))
    (('cs% defdata-type
       &
       'empty-eq-constraint
       range
       mem-constraint
       &) (b* ((mem-vs (all-vars mem-constraint)) (remaining (set-difference-eq mem-vs bound-vars))
          (enum-info% (get-enum-info% defdata-type
              range
              vl
              wrld)))
        (if remaining
          (mv (access enum-info% domain-size)
            (access enum-info% min-rec-depth)
            (access enum-info% max-rec-depth)
            (list (access enum-info% expr)
              (access enum-info% expr2)))
          (mv :mem 0
            30
            (list `(let ((len-v (len ,CGEN::MEM-CONSTRAINT)))
                (if (zp len-v)
                  ,(CGEN::ACCESS CGEN::ENUM-INFO% CGEN::EXPR)
                  (nth (mod r len-v) ,CGEN::MEM-CONSTRAINT)))
              `(let ((len-v (len ,CGEN::MEM-CONSTRAINT)))
                (if (zp len-v)
                  ,(CGEN::ACCESS CGEN::ENUM-INFO% CGEN::EXPR2)
                  (mv (nth (mod seed. len-v) ,CGEN::MEM-CONSTRAINT)
                    seed.))))))))
    (& (prog2$ (cw? (normal-output-flag vl)
          "~|Cgen/Error: BAD record cs% passed to cs%-enumcalls")
        (mv 0 0 0 nil)))))

(def make-next-sigma_mv-let
  (v-cs%-alst seen-vars
    n
    i
    use-fixers-p
    vl
    wrld
    body)
  (decl :sig ((symbol-alistp symbol-listp
       fixnum
       fixnum
       booleanp
       fixnum
       plist-worldp
       pseudo-termp) ->
      pseudo-termp)
    :doc "helper function to make-next-sigma")
  (declare (ignorable n i))
  (f* ((_mv-value (v min max exp exp2)
       `(case sampling-method
         (:uniform-random (b* (((mv ?m seed.) (choose-size ,MIN ,MAX seed.)) ((mv val seed.) ,CGEN::EXP2))
             (mv seed. be. val)))
         (:random (b* (((mv ?r seed.) (random-natural-seed seed.)))
             (mv seed. be. ,EXP)))
         (:be (b* ((?r (cdr (assoc-eq ',CGEN::V be.))))
             (mv seed. (|next BE args| be.) ,EXP)))
         (otherwise (mv seed. be. '0)))))
    (if (endp v-cs%-alst)
      body
      (b* (((cons var cs%) (car v-cs%-alst)) ((mv &
             min-rec-depth
             max-rec-depth
             (list exp exp2)) (if use-fixers-p
              (cs%-enumcalls-defdata cs% vl wrld)
              (cs%-enumcalls cs%
                vl
                wrld
                seen-vars))))
        `(mv-let (seed. be. ,CGEN::VAR)
          ,(CGEN::_MV-VALUE CGEN::VAR CGEN::MIN-REC-DEPTH CGEN::MAX-REC-DEPTH EXP
  CGEN::EXP2)
          (declare (ignorable ,CGEN::VAR))
          ,(CGEN::MAKE-NEXT-SIGMA_MV-LET (CDR CGEN::V-CS%-ALST)
  (CONS CGEN::VAR CGEN::SEEN-VARS) CGEN::N CGEN::I CGEN::USE-FIXERS-P CGEN::VL
  CGEN::WRLD CGEN::BODY))))))

(defun displayed-range
  (interval)
  (b* ((lo (access tau-interval interval :lo)) (hi (access tau-interval interval :hi))
      (lo-rel (access tau-interval interval :lo-rel))
      (hi-rel (access tau-interval interval :hi-rel)))
    (cond ((and lo hi) `(,CGEN::LO ,(IF CGEN::LO-REL
     '<
     '<=)
          '_
          ,(IF CGEN::HI-REL
     '<
     '<=)
          ,CGEN::HI))
      (lo `(,(IF CGEN::LO-REL
     '>
     '>=) ,CGEN::LO))
      (t `(,(IF CGEN::HI-REL
     '<
     '<=) ,CGEN::HI)))))

(def displayed-defdata-type/eq-constraint
  (cs% computed-vars)
  (decl :sig ((cs%-p symbol-listp) ->
      (mv fixnum pseudo-termp))
    :doc "for each cs% record we translate it to defdata-type or 
equality constraint that will be used for enumeration. it shadows cs%-enumcall")
  (case-match cs%
    (('cs% defdata-type
       &
       'empty-eq-constraint
       range
       'empty-mem-constraint
       &) (if (non-empty-non-universal-interval-p range)
        (list :type defdata-type
          :range (displayed-range range))
        defdata-type))
    (('cs% defdata-type
       &
       eq-constraint
       range
       'empty-mem-constraint
       &) (b* ((eq-vs (all-vars eq-constraint)) (remaining (set-difference-eq eq-vs computed-vars)))
        (if remaining
          (if (non-empty-non-universal-interval-p range)
            (list :type defdata-type
              :range (displayed-range range))
            defdata-type)
          eq-constraint)))
    (('cs% defdata-type
       &
       'empty-eq-constraint
       range
       mem-constraint
       &) (b* ((mem-vs (all-vars mem-constraint)) (remaining (set-difference-eq mem-vs computed-vars)))
        (if remaining
          (if (non-empty-non-universal-interval-p range)
            (list :type defdata-type
              :range (displayed-range range))
            defdata-type)
          (list :enum mem-constraint))))
    (& 'bad-type)))

(def displayed-enum-alist
  (v-cs%-alst ans.)
  (decl :sig ((symbol-cs%-alist symbol-alist) ->
      symbol-alist)
    :doc "given an alist mapping variables to cs% records (in dependency order),
  we walk down the alist, translating each type constraint to the corresponding
enumerator type/expr to be displayed in verbose mode")
  (if (endp v-cs%-alst)
    (reverse ans.)
    (b* (((cons x cs%) (car v-cs%-alst)) (type (displayed-defdata-type/eq-constraint cs%
            (strip-cars ans.))))
      (displayed-enum-alist (cdr v-cs%-alst)
        (cons (cons x type) ans.)))))