glcp-geval

(in-package "GL")

(include-book "generic-geval")

(include-book "symbolic-arithmetic")

(include-book "shape-spec-defs")

(include-book "gl-mbe")

(defun gl-cp-hint (x) (declare (ignore x)) t)

(in-theory (disable gl-cp-hint
    (:type-prescription gl-cp-hint)
    (gl-cp-hint)))

(def-eval-g glcp-generic-geval
  (logtail$inline logapp
    int-set-sign
    maybe-integer
    cons
    car
    cdr
    consp
    if
    not
    equal
    nth
    len
    iff
    shape-spec-slice-to-env
    ss-append-envs
    shape-spec-obj-in-range-iff
    shape-spec-obj-in-range
    shape-spec-env-slice
    shape-spec-iff-env-slice
    logcons$inline
    if
    gl-cp-hint
    shape-spec-obj-in-range
    return-last
    use-by-hint
    equal
    typespec-check
    implies
    iff
    not
    cons
    gl-aside
    gl-ignore
    gl-error
    gl-hide
    binary-*
    binary-+
    pkg-witness
    unary--
    complex-rationalp
    acl2-numberp
    symbol-package-name
    intern-in-package-of-symbol
    code-char
    denominator
    cdr
    car
    consp
    symbol-name
    char-code
    imagpart
    symbolp
    realpart
    numerator
    equal
    stringp
    rationalp
    cons
    integerp
    characterp
    <
    coerce
    booleanp
    logbitp
    binary-logand
    binary-logior
    binary-logxor
    binary-logeqv
    lognot
    ash
    integer-length
    floor
    mod
    truncate
    rem
    bool-fix$inline
    not
    implies
    eq
    atom
    eql
    =
    /=
    null
    endp
    zerop
    plusp
    minusp
    listp
    logapp
    int-set-sign
    maybe-integer
    gl-force-check-fn
    binary-minus-for-gl
    o<
    o-p))

(in-theory (disable glcp-generic-geval))

(defund glcp-generic-geval-alist
  (al env)
  (declare (xargs :guard (consp env)))
  (if (atom al)
    nil
    (if (consp (car al))
      (cons (cons (caar al)
          (glcp-generic-geval (cdar al) env))
        (glcp-generic-geval-alist (cdr al) env))
      (glcp-generic-geval-alist (cdr al) env))))