rewrite-code

(in-package "REWRITE-CODE")

(program)

(set-state-ok t)

(defun aug-natp
  (x)
  (or (natp x)
    (equal x 'inf)))

(defun aug-nat-<
  (x y)
  (and (not (eq x 'inf))
    (or (eq y 'inf)
      (< x y))))

(defun aug-nat-dec
  (x)
  (cond ((eq x 'inf) 'inf)
    ((zp x) 0)
    (t (1- x))))

(defun multiplicity-rangep
  (x)
  (or (null x)
    (and (consp x)
      (aug-natp (car x))
      (aug-natp (cdr x))
      (not (aug-nat-< (cdr x)
          (car x))))))

(defun multiplicity-range-dec
  (x)
  (if (or (endp x) (equal (cdr x) 0))
    nil
    (cons (aug-nat-dec (car x))
      (aug-nat-dec (cdr x)))))

(defun rev-prepend
  (torev onto)
  (if (endp torev)
    onto
    (rev-prepend (cdr torev)
      (cons (car torev) onto))))

(defun pop-push-n
  (n from to)
  (if (or (zp n)
      (endp from))
    (mv from to)
    (pop-push-n (1- n)
      (cdr from)
      (cons (car from) to))))

(defun update-alist
  (key val lst)
  (cond ((endp lst) (list (cons key val)))
    ((and (consp (car lst))
       (equal (caar lst) key)) (cons (cons key val)
        (cdr lst)))
    (t (cons (car lst)
        (update-alist key
          val
          (cdr lst))))))

(defun replace-assns
  (expr assn-alist)
  (if (consp expr)
    (cons (replace-assns (car expr)
        assn-alist)
      (replace-assns (cdr expr)
        assn-alist))
    (if (symbolp expr)
      (let ((assn (assoc-eq expr
             assn-alist)))
        (if (consp assn)
          (cdr assn)
          expr))
      expr)))

(defun merge-matches
  (a1 a2)
  (cond ((endp a1) a2)
    ((endp a2) a1)
    (t (let* ((sym (caar a1)) (binding2 (assoc-eq sym a2)))
        (if (consp binding2)
          (let ((val1 (cdar a1)) (val2 (cdr binding2)))
            (if (equal val1 val2)
              (merge-matches (cdr a1)
                a2)
              t))
          (merge-matches (cdr a1)
            (cons (car a1) a2)))))))

(defun match-pattern
  (expr pat vars)
  (cond ((member-eq pat
       vars) (list (cons pat expr)))
    ((and (consp pat) (consp expr)) (let ((car-result (match-pattern (car expr)
             (car pat)
             vars)) (cdr-result (match-pattern (cdr expr)
              (cdr pat)
              vars)))
        (if (or (equal car-result t)
            (equal cdr-result t))
          t
          (merge-matches car-result
            cdr-result))))
    ((equal pat expr) nil)
    (t t)))

(mutual-recursion (defun rewrite-defp
    (v)
    (declare (xargs :measure (acl2-count v)
        :hints (("Goal" :in-theory (disable (:definition multiplicity-rangep))))))
    (or (null v)
      (and (consp v)
        (rewrite-simul-defp (car v))
        (rewrite-defp (cdr v)))))
  (defun rewrite-simul-defp
    (v)
    (declare (xargs :measure (acl2-count v)))
    (or (null v)
      (and (consp v)
        (rewrite-entryp (car v))
        (rewrite-simul-defp (cdr v)))))
  (defun rewrite-entryp
    (v)
    (declare (xargs :measure (acl2-count v)))
    (and (consp v)
      (multiplicity-rangep (car v))
      (consp (cdr v))
      (rewrite-var-entry-lstp (cadr v))
      (consp (cddr v))
      (symbol-listp (caddr v))
      (consp (cdddr v))))
  (defun rewrite-var-entry-lstp
    (v)
    (declare (xargs :measure (acl2-count v)))
    (or (null v)
      (and (consp v)
        (rewrite-var-entryp (car v))
        (rewrite-var-entry-lstp (cdr v)))))
  (defun rewrite-var-entryp
    (v)
    (declare (xargs :measure (acl2-count v)))
    (and (consp v)
      (symbolp (car v))
      (rewrite-defp (cdr v)))))

(defmacro entry-multrng
  (v)
  `(car ,REWRITE-CODE::V))

(defmacro entry-alist
  (v)
  `(cadr ,REWRITE-CODE::V))

(defmacro entry-vars
  (v)
  `(caddr ,REWRITE-CODE::V))

(defmacro entry-pat
  (v)
  `(cadddr ,REWRITE-CODE::V))

(defmacro entry-repl
  (v)
  `(cddddr ,REWRITE-CODE::V))

(defun dec-entry
  (v)
  (cons (multiplicity-range-dec (car v))
    (cdr v)))

(defun update-entry-alist
  (v alist)
  (cons (car v)
    (cons alist (cddr v))))

(defun update-entry-alist-entry
  (v var def)
  (update-entry-alist v
    (update-alist var
      def
      (entry-alist v))))

(mutual-recursion (defun rewrite-seq
    (form seq-from
      seq-to)
    (declare (xargs :guard (and (rewrite-defp seq-from)
          (rewrite-defp seq-to))))
    (if (consp seq-from)
      (mv-let (form updated)
        (rewrite-simul form
          (car seq-from)
          nil)
        (rewrite-seq form
          (cdr seq-from)
          (cons updated seq-to)))
      (mv form
        (reverse seq-to))))
  (defun rewrite-simul
    (form simul-from
      simul-to)
    (declare (xargs :guard (and (rewrite-simul-defp simul-from)
          (rewrite-simul-defp simul-to))))
    (if (consp simul-from)
      (let* ((entry (car simul-from)) (assns-opt (match-pattern form
              (entry-pat entry)
              (entry-vars entry))))
        (if (eq 't assns-opt)
          (rewrite-simul form
            (cdr simul-from)
            (cons entry simul-to))
          (let* ((entry (dec-entry entry)) (simul-from (cons entry (cdr simul-from)))
              (idx (len simul-to)))
            (rewrite-assns (entry-repl entry)
              assns-opt
              idx
              (rev-prepend simul-to
                simul-from)))))
      (let ((simul-all (reverse simul-to)))
        (if (consp form)
          (mv-let (car-form simul-all)
            (rewrite-simul (car form)
              simul-all
              nil)
            (mv-let (cdr-form simul-all)
              (rewrite-simul (cdr form)
                simul-all
                nil)
              (mv (cons car-form cdr-form)
                simul-all)))
          (mv form
            simul-all)))))
  (defun rewrite-assns
    (repl assns
      entry-idx
      simul-all)
    (declare (xargs :guard (and (rewrite-simul-defp simul-all)
          (natp entry-idx)
          (< entry-idx
            (len simul-all))
          (symbol-alistp assns))))
    (cond ((consp repl) (mv-let (car-form simul-all)
          (rewrite-assns (car repl)
            assns
            entry-idx
            simul-all)
          (mv-let (cdr-form simul-all)
            (rewrite-assns (cdr repl)
              assns
              entry-idx
              simul-all)
            (mv (cons car-form cdr-form)
              simul-all))))
      ((symbolp repl) (let ((assn-opt (assoc-eq repl
               assns)))
          (if (consp assn-opt)
            (let* ((form (cdr assn-opt)) (entry (nth entry-idx simul-all))
                (non-rec-defs (entry-alist entry))
                (non-rec-def-opt (assoc-eq repl
                    non-rec-defs)))
              (if (consp non-rec-def-opt)
                (mv-let (form updated-def)
                  (rewrite-seq form
                    (cdr non-rec-def-opt)
                    nil)
                  (mv form
                    (update-nth entry-idx
                      (update-entry-alist-entry entry
                        repl
                        updated-def)
                      simul-all)))
                (if (and (symbolp (entry-pat entry))
                    (member-eq (entry-pat entry)
                      (entry-vars entry)))
                  (mv form
                    simul-all)
                  (rewrite-simul form
                    simul-all
                    nil))))
            (mv repl
              simul-all))))
      (t (mv repl
          simul-all)))))

(mutual-recursion (defun assert-zero-allowed-def
    (v state)
    (if (endp v)
      state
      (pprogn (assert-zero-allowed-simul-def (car v)
          state)
        (assert-zero-allowed-def (cdr v)
          state))))
  (defun assert-zero-allowed-simul-def
    (v state)
    (if (endp v)
      state
      (pprogn (assert-zero-allowed-entry (car v)
          state)
        (assert-zero-allowed-simul-def (cdr v)
          state))))
  (defun assert-zero-allowed-entry
    (v state)
    (if (or (endp v) (endp (cdr v)))
      state
      (let ((rng (car v)) (var-entries (cadr v)))
        (pprogn (if (or (endp rng)
              (not (equal (car rng) 0)))
            (pprogn (f-put-global 'erp t state)
              (fms (if (endp rng)
                  "Code rewrite entry used too many times:~%  ~xp -> ~xr~%"
                  "Code rewrite entry used too few times (at least ~xn applications remaining):~%  ~xp -> ~xr~%")
                `((#\p . ,(REWRITE-CODE::ENTRY-PAT REWRITE-CODE::V)) (#\r . ,(REWRITE-CODE::ENTRY-REPL REWRITE-CODE::V))
                  (#\n . ,(AND (CONSP REWRITE-CODE::RNG) (CAR REWRITE-CODE::RNG))))
                (standard-co state)
                state
                (abbrev-evisc-tuple state)))
            state)
          (assert-zero-allowed-entry-lst var-entries
            state)))))
  (defun assert-zero-allowed-entry-lst
    (v state)
    (if (endp v)
      state
      (pprogn (assert-zero-allowed-var-entry (car v)
          state)
        (assert-zero-allowed-entry-lst (cdr v)
          state))))
  (defun assert-zero-allowed-var-entry
    (v state)
    (if (endp v)
      state
      (assert-zero-allowed-def (cdr v)
        state))))

(defun er-if-zero-not-allowed-def
  (def state)
  (state-global-let* ((erp nil))
    (pprogn (assert-zero-allowed-def def
        state)
      (mv (@ erp)
        :invisible state))))

(defun rewrite-fn
  (form def state)
  (if (not (rewrite-defp def))
    (er soft
      'rewrite
      "Code rewrite definition illegal:~%~x0"
      def)
    (mv-let (result new-def)
      (rewrite-seq form
        def
        nil)
      (er-progn (er-if-zero-not-allowed-def new-def
          state)
        (value result)))))

(defun multiplicity-specp
  (x)
  (declare (xargs :guard t))
  (or (and (multiplicity-rangep x)
      (not (equal (car x) 'inf)))
    (equal x '*)
    (equal x '+)
    (natp x)))

(defun multiplicity-spec-to-noninf-range
  (x)
  (declare (xargs :guard (multiplicity-specp x)))
  (cond ((and (multiplicity-rangep x)
       (not (equal (car x) 'inf))) x)
    ((equal x '*) '(0 . inf))
    ((equal x '+) '(1 . inf))
    ((natp x) (cons x x))
    (t nil)))

(defmacro quote-rewrite-def
  (&rest v)
  (cond ((endp v) ''nil)
    ((and (consp (car v))
       (null (cdr v))) `(quote-rewrite-def . ,(CAR REWRITE-CODE::V)))
    ((eq ':seq (car v)) `(quote-rewrite-def-rest . ,(CDR REWRITE-CODE::V)))
    (t `(list (quote-rewrite-simul-def . ,REWRITE-CODE::V)))))

(defmacro quote-rewrite-def-rest
  (&rest v)
  (if (endp v)
    ''nil
    `(cons (quote-rewrite-simul-def . ,(CAR REWRITE-CODE::V))
      (quote-rewrite-def-rest . ,(CDR REWRITE-CODE::V)))))

(defmacro quote-rewrite-simul-def
  (&rest v)
  (cond ((endp v) ''nil)
    ((eq ':simul (car v)) `(quote-rewrite-simul-def-rest . ,(CDR REWRITE-CODE::V)))
    (t `(list (quote-rewrite-entry . ,REWRITE-CODE::V)))))

(defmacro quote-rewrite-simul-def-rest
  (&rest v)
  (if (endp v)
    ''nil
    `(cons (quote-rewrite-entry . ,(CAR REWRITE-CODE::V))
      (quote-rewrite-simul-def-rest . ,(CDR REWRITE-CODE::V)))))

(defun namep
  (v)
  (and (symbolp v)
    (not (null v))
    (not (keywordp v))))

(defun var-specp
  (v)
  (or (null v)
    (namep v)
    (and (consp v)
      (or (namep (car v))
        (and (consp (car v))
          (namep (caar v))))
      (var-specp (cdr v)))))

(defun recvar-specp
  (v)
  (or (null v)
    (namep v)
    (and (consp v)
      (namep (car v))
      (recvar-specp (cdr v)))))

(defun get-var-names
  (var-spec)
  (if (consp var-spec)
    (cons (if (consp (car var-spec))
        (caar var-spec)
        (car var-spec))
      (get-var-names (cdr var-spec)))
    (if (null var-spec)
      nil
      (list var-spec))))

(defun canonicalize-var-bindings
  (var-spec)
  (if (consp var-spec)
    (cons (if (consp (car var-spec))
        (car var-spec)
        (list (car var-spec)))
      (canonicalize-var-bindings (cdr var-spec)))
    (if (null var-spec)
      nil
      (list (list var-spec)))))

(defmacro quote-rewrite-entry
  (&key (pat 'nil patp)
    (carpat 'nil carpatp)
    (repl 'nil replp)
    (mult '*)
    (vars 'nil)
    (recvars 'nil))
  (declare (xargs :guard (and (multiplicity-specp mult)
        (var-specp vars)
        (recvar-specp recvars)
        (not (and patp carpatp))
        (or (and patp
            (not (member pat
                (get-var-names recvars))))
          (and carpatp
            (not (member carpat
                (get-var-names recvars)))))
        (not (intersectp-eq (get-var-names vars)
            (get-var-names recvars))))))
  (let* ((cdrvar '%cdr-reserved%) (nrcvar-names (get-var-names vars))
      (recvar-names (append (if carpatp
            (list cdrvar)
            'nil)
          (get-var-names recvars)))
      (var-names (append nrcvar-names
          recvar-names))
      (pat (if patp
          pat
          (cons carpat cdrvar)))
      (repl (if replp
          (if carpatp
            (cons repl cdrvar)
            repl)
          pat)))
    `(list* ',(REWRITE-CODE::MULTIPLICITY-SPEC-TO-NONINF-RANGE REWRITE-CODE::MULT)
      (quote-rewrite-var-entry-lst . ,(REWRITE-CODE::CANONICALIZE-VAR-BINDINGS REWRITE-CODE::VARS))
      ',REWRITE-CODE::VAR-NAMES
      ',REWRITE-CODE::PAT
      ',REWRITE-CODE::REPL)))

(defmacro quote-rewrite-var-entry-lst
  (&rest bindings)
  (if (endp bindings)
    ''nil
    `(cons (quote-rewrite-var-entry ,(CAR REWRITE-CODE::BINDINGS))
      (quote-rewrite-var-entry-lst . ,(CDR REWRITE-CODE::BINDINGS)))))

(defmacro quote-rewrite-var-entry
  (v)
  (declare (xargs :guard (and (consp v)
        (namep (car v)))))
  `(cons ',(CAR REWRITE-CODE::V)
    (quote-rewrite-def . ,(CDR REWRITE-CODE::V))))

(defmacro er-rewrite-form
  (form &rest def)
  `(rewrite-fn ,REWRITE-CODE::FORM
    (quote-rewrite-def . ,REWRITE-CODE::DEF)
    state))

(defun get-defun
  (name state)
  (let* ((ev-wrld (decode-logical-name name
         (w state))) (cltl-command (and ev-wrld
          (let ((cltl-cmd (getprop 'cltl-command
                 'global-value
                 nil
                 'current-acl2-world
                 ev-wrld)))
            (and (consp cltl-cmd)
              (equal (car cltl-cmd) 'defuns)
              (= (len cltl-cmd) 4)
              cltl-cmd)))))
    (and cltl-command
      (let* ((mode (second cltl-command)) (defuns-body (fourth cltl-command))
          (ll (cadr defuns-body))
          (tail (cddr defuns-body))
          (stobjs (remove nil
              (getprop name
                'stobjs-in
                nil
                'current-acl2-world
                ev-wrld)))
          (dec `(declare (xargs :mode ,REWRITE-CODE::MODE
                :stobjs ,REWRITE-CODE::STOBJS))))
        `(defun ,REWRITE-CODE::NAME
          ,REWRITE-CODE::LL
          ,REWRITE-CODE::DEC . ,REWRITE-CODE::TAIL)))))

(defun compute-copy-defun+rewrite
  (src dst
    rwdef
    defun-like
    state)
  (if (and (null rwdef)
      (eq src dst))
    (value '(value-triple :nothing-to-do))
    (let* ((src-defun (get-defun src
           state)))
      (if src-defun
        (value (let* ((tuple (cddr src-defun)) (bodycons (last tuple))
              (tuple-no-body (butlast tuple 1)))
            (if (null rwdef)
              (list* defun-like
                dst
                tuple)
              `(make-event (er-let* ((b2 (er-rewrite-form ',REWRITE-CODE::BODYCONS . ,REWRITE-CODE::RWDEF)))
                  (value `(,',REWRITE-CODE::DEFUN-LIKE ,',REWRITE-CODE::DST
                      ,@',REWRITE-CODE::TUPLE-NO-BODY . ,REWRITE-CODE::B2)))))))
        (er soft
          'compute-copy-defun+rewrite
          "Illegal or missing defun for ~x0."
          src)))))

(defmacro assert-include-defun-matches-certify-defun
  (name)
  (declare (xargs :guard (symbolp name)))
  `(make-event `(assert-event (let ((certify-time-defun ',(REWRITE-CODE::GET-DEFUN ',REWRITE-CODE::NAME REWRITE-CODE::STATE)) (include-time-defun (get-defun ',',REWRITE-CODE::NAME
              state)))
        (or (equal certify-time-defun
            include-time-defun)
          (cw "Certify time def: ~x0~%Include time def: ~x1~%"
            certify-time-defun
            include-time-defun)))
      :on-skip-proofs t)))

(defmacro copy-defun+rewrite
  (src dst
    &rest
    rewrite-spec)
  (declare (xargs :guard (and (symbolp src)
        (symbolp dst))))
  `(progn (assert-include-defun-matches-certify-defun ,REWRITE-CODE::SRC)
    (make-event (compute-copy-defun+rewrite ',REWRITE-CODE::SRC
        ',REWRITE-CODE::DST
        ',REWRITE-CODE::REWRITE-SPEC
        'defun
        state))))

(defmacro copy-defun
  (src dst)
  `(copy-defun+rewrite ,REWRITE-CODE::SRC
    ,REWRITE-CODE::DST))