fty-list

(in-package "FTY")

(include-book "database")

(include-book "fty-parseutils")

(include-book "std/lists/list-defuns" :dir :system)

(program)

(defconst *flexlist-keywords*
  '(:pred :fix :equiv :count :elt-type :non-emptyp :measure :measure-debug :xvar :true-listp :elementp-of-nil :cheap :parents :short :long :no-count :prepwork :post-pred-events :post-fix-events :post-events :enable-rules :verbosep))

(define parse-flexlist
  (x xvar
    our-fixtypes
    fixtypes
    state)
  (b* (((cons name args) x) ((unless (symbolp name)) (raise "Malformed flexlist: ~x0: name must be a symbol"
          x))
      ((mv pre-/// post-///) (split-/// name args))
      ((mv kwd-alist rest) (extract-keywords name
          *flexlist-keywords*
          pre-///
          nil))
      (kwd-alist (append kwd-alist
          (table-alist 'deflist-defaults
            (w state))))
      ((when rest) (raise "Malformed flexlist: ~x0: after kind should be a keyword/value list."
          name))
      (elt-type (getarg :elt-type nil kwd-alist))
      ((unless (and (symbolp elt-type) elt-type)) (raise "Bad flexlist ~x0: Element type must be a symbol"
          name))
      ((mv elt-type
         elt-fix
         elt-equiv
         recp) (get-pred/fix/equiv (getarg :elt-type nil kwd-alist)
          our-fixtypes
          fixtypes))
      (pred (getarg! :pred (intern-in-package-of-symbol (cat (symbol-name name) "-P")
            name)
          kwd-alist))
      (fix (getarg! :fix (intern-in-package-of-symbol (cat (symbol-name name) "-FIX")
            name)
          kwd-alist))
      (equiv (getarg! :equiv (intern-in-package-of-symbol (cat (symbol-name name) "-EQUIV")
            name)
          kwd-alist))
      (non-emptyp (getarg :non-emptyp nil kwd-alist))
      (elementp-of-nil (getarg :elementp-of-nil :unknown kwd-alist))
      (cheap (getarg :cheap nil kwd-alist))
      (count (flextype-get-count-fn name kwd-alist))
      (xvar (or (getarg :xvar xvar kwd-alist)
          (car (find-symbols-named-x (getarg :measure nil kwd-alist)))
          (intern-in-package-of-symbol "X" name)))
      (measure (getarg! :measure `(acl2-count ,FTY::XVAR)
          kwd-alist))
      ((mv already-defined true-listp) (check-flexlist-already-defined pred
          kwd-alist
          our-fixtypes
          'deflist
          state))
      (fix-already-defined (check-flexlist-fix-already-defined fix
          kwd-alist
          our-fixtypes
          'deflist
          state)))
    (make-flexlist :name name
      :pred pred
      :fix fix
      :equiv equiv
      :count count
      :elt-type elt-type
      :elt-fix elt-fix
      :elt-equiv elt-equiv
      :true-listp true-listp
      :elementp-of-nil elementp-of-nil
      :cheap cheap
      :measure measure
      :non-emptyp non-emptyp
      :kwd-alist (if post-///
        (cons (cons :///-events post-///) kwd-alist)
        kwd-alist)
      :xvar xvar
      :recp recp
      :already-definedp already-defined
      :fix-already-definedp fix-already-defined)))

(define flexlist-fns
  (x)
  (b* (((flexlist x)))
    (list x.pred x.fix)))

(define flexlist-collect-fix/pred-pairs
  (x)
  (b* (((flexlist x)))
    (and x.elt-type
      x.elt-fix
      (list (cons x.elt-fix x.elt-type)))))

(define flexlist-predicate-def
  (x)
  (b* (((flexlist x)) (stdx (intern-in-package-of-symbol "X" x.pred)))
    `(,@(IF FTY::X.ALREADY-DEFINEDP
      '(PROGN)
      `(FTY::DEFINE ,FTY::X.PRED (,FTY::X.XVAR) :PARENTS NIL :PROGN T :MEASURE
        ,FTY::X.MEASURE
        ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::X.KWD-ALIST)
               `(:MEASURE-DEBUG T))
        ,(IF FTY::X.NON-EMPTYP
             `(AND (CONSP ,FTY::X.XVAR) (,FTY::X.ELT-TYPE (CAR ,FTY::X.XVAR))
                   (LET ((,FTY::X.XVAR (CDR ,FTY::X.XVAR)))
                     (IF (ATOM ,FTY::X.XVAR)
                         ,(IF FTY::X.TRUE-LISTP
                              `(EQ ,FTY::X.XVAR NIL)
                              T)
                         (,FTY::X.PRED ,FTY::X.XVAR))))
             `(IF (ATOM ,FTY::X.XVAR)
                  ,(IF FTY::X.TRUE-LISTP
                       `(EQ ,FTY::X.XVAR NIL)
                       T)
                  (AND (,FTY::X.ELT-TYPE (CAR ,FTY::X.XVAR))
                       (,FTY::X.PRED (CDR ,FTY::X.XVAR)))))
        ///)) (local (in-theory (disable ,FTY::X.PRED)))
      (deflist ,FTY::X.PRED
        (,FTY::STDX)
        :parents (,FTY::X.NAME)
        (,FTY::X.ELT-TYPE ,FTY::STDX)
        :already-definedp t
        ,@(AND (NOT (EQ FTY::X.ELEMENTP-OF-NIL :UNKNOWN))
       `(:ELEMENTP-OF-NIL ,FTY::X.ELEMENTP-OF-NIL))
        :true-listp ,FTY::X.TRUE-LISTP
        :non-emptyp ,FTY::X.NON-EMPTYP
        :cheap ,FTY::X.CHEAP))))

(define flexlist-fix-def
  (x flagp)
  (b* (((flexlist x)))
    (if x.fix-already-definedp
      '(progn)
      `(define ,FTY::X.FIX
        ((,FTY::X.XVAR ,FTY::X.PRED))
        :parents (,FTY::X.NAME)
        :short ,(FTY::CAT "@(call " (XDOC::FULL-ESCAPE-SYMBOL FTY::X.FIX)
  ") is a usual @(see fty::fty) list fixing function.")
        :long ,(FTY::CAT "<p>In the logic, we apply @(see? "
  (XDOC::FULL-ESCAPE-SYMBOL FTY::X.ELT-FIX)
  ") to each member of the x.  In the execution, none of
                    that is actually necessary and this is just an inlined
                    identity function.</p>")
        :measure ,FTY::X.MEASURE
        ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::X.KWD-ALIST) `(:MEASURE-DEBUG T))
        ,@(AND FTY::FLAGP `(:FLAG ,FTY::X.NAME))
        :returns (newx ,FTY::X.PRED
          :hints (,@(AND (NOT FTY::FLAGP) `(("goal" :INDUCT (,FTY::X.FIX ,FTY::X.XVAR)))) '(:in-theory (disable ,FTY::X.FIX ,FTY::X.PRED)
              :expand ((,FTY::X.FIX ,FTY::X.XVAR) (:free (a b) (,FTY::X.PRED (cons a b)))
                (,FTY::X.PRED ,FTY::X.XVAR)
                (,FTY::X.PRED nil)))))
        :verify-guards nil
        :progn t
        :inline t
        (mbe :logic ,(IF FTY::X.NON-EMPTYP
     `(IF (CONSP (CDR ,FTY::X.XVAR))
          (CONS (,FTY::X.ELT-FIX (CAR ,FTY::X.XVAR))
                (,FTY::X.FIX (CDR ,FTY::X.XVAR)))
          (CONS (,FTY::X.ELT-FIX (CAR ,FTY::X.XVAR))
                ,(IF FTY::X.TRUE-LISTP
                     NIL
                     `(CDR ,FTY::X.XVAR))))
     `(IF (ATOM ,FTY::X.XVAR)
          ,(IF FTY::X.TRUE-LISTP
               NIL
               FTY::X.XVAR)
          (CONS (,FTY::X.ELT-FIX (CAR ,FTY::X.XVAR))
                (,FTY::X.FIX (CDR ,FTY::X.XVAR)))))
          :exec ,FTY::X.XVAR)
        ///))))

(define flexlist-fix-postevents
  (x)
  (b* (((flexlist x)) (stdx (intern-in-package-of-symbol "X" x.pred))
      (stda (intern-in-package-of-symbol "A" x.pred))
      (consp-of-foo-fix (intern-in-package-of-symbol (cat "CONSP-OF-" (symbol-name x.fix))
          x.fix))
      (consp-cdr-of-foo-fix (intern-in-package-of-symbol (cat "CONSP-CDR-OF-" (symbol-name x.fix))
          x.fix))
      (car-of-foo-fix (intern-in-package-of-symbol (cat "CAR-OF-" (symbol-name x.fix))
          x.fix))
      (foo-fix-under-iff (intern-in-package-of-symbol (cat (symbol-name x.fix) "-UNDER-IFF")
          x.fix))
      (foo-fix-of-cons (intern-in-package-of-symbol (cat (symbol-name x.fix) "-OF-CONS")
          x.fix))
      (len-of-foo-fix (intern-in-package-of-symbol (cat "LEN-OF-" (symbol-name x.fix))
          x.fix))
      (foo-fix-of-append (intern-in-package-of-symbol (cat (symbol-name x.fix) "-OF-APPEND")
          x.fix))
      (foo-fix-of-repeat (intern-in-package-of-symbol (cat (symbol-name x.fix) "-OF-REPEAT")
          x.fix))
      (nth-of-foo-fix (intern-in-package-of-symbol (cat "NTH-OF-" (symbol-name x.fix))
          x.fix))
      (list-equiv-refines-foo-equiv (intern-in-package-of-symbol (cat "LIST-EQUIV-REFINES-" (symbol-name x.equiv))
          x.equiv))
      (foo-equiv-implies-foo-equiv-append-1 (intern-in-package-of-symbol (cat (symbol-name x.equiv)
            "-IMPLIES-"
            (symbol-name x.equiv)
            "-APPEND-1")
          x.equiv))
      (foo-equiv-implies-foo-equiv-append-2 (intern-in-package-of-symbol (cat (symbol-name x.equiv)
            "-IMPLIES-"
            (symbol-name x.equiv)
            "-APPEND-2")
          x.equiv)))
    `((deffixcong ,FTY::X.EQUIV
       ,FTY::X.ELT-EQUIV
       (car x)
       x
       :pkg ,FTY::X.EQUIV
       :hints (("goal" :expand ((,FTY::X.FIX x))
          :in-theory (enable default-car)))) (deffixcong ,FTY::X.EQUIV
        ,FTY::X.EQUIV
        (cdr x)
        x
        :pkg ,FTY::X.EQUIV
        :hints (("goal" :expand ((,FTY::X.FIX x) ,@(AND FTY::X.NON-EMPTYP `((,FTY::X.FIX (CDR FTY::X)))))
           ,@(AND FTY::X.NON-EMPTYP '(:IN-THEORY (FTY::ENABLE FTY::DEFAULT-CAR))))))
      (deffixcong ,FTY::X.ELT-EQUIV
        ,FTY::X.EQUIV
        (cons x y)
        x
        :pkg ,FTY::X.EQUIV
        :hints (("goal" :expand ((:free (a b) (,FTY::X.FIX (cons a b)))))))
      ,@(AND (NOT FTY::X.NON-EMPTYP)
       `((FTY::DEFFIXCONG ,FTY::X.EQUIV ,FTY::X.EQUIV (CONS FTY::X FTY::Y)
          FTY::Y :PKG ,FTY::X.EQUIV :HINTS
          (("goal" :EXPAND
            ((:FREE (FTY::A FTY::B) (,FTY::X.FIX (CONS FTY::A FTY::B)))))))))
      (defthm ,FTY::CONSP-OF-FOO-FIX
        ,(IF FTY::X.NON-EMPTYP
     `(CONSP (,FTY::X.FIX FTY::X))
     `(EQUAL (CONSP (,FTY::X.FIX FTY::X)) (CONSP FTY::X)))
        :hints (("goal" :expand ((,FTY::X.FIX x)))))
      ,@(AND FTY::X.NON-EMPTYP
       `((FTY::DEFTHM ,FTY::CONSP-CDR-OF-FOO-FIX
          (EQUAL (CONSP (CDR (,FTY::X.FIX FTY::X))) (CONSP (CDR FTY::X)))
          :HINTS (("goal" :EXPAND ((,FTY::X.FIX FTY::X)))))
         (FTY::DEFTHM ,FTY::CAR-OF-FOO-FIX
          (EQUAL (CAR (,FTY::X.FIX FTY::X)) (,FTY::X.ELT-FIX (CAR FTY::X)))
          :HINTS (("goal" :EXPAND ((,FTY::X.FIX FTY::X)))))))
      ,@(AND (OR FTY::X.TRUE-LISTP FTY::X.NON-EMPTYP)
       `((FTY::DEFTHM ,FTY::FOO-FIX-UNDER-IFF
          ,(IF FTY::X.NON-EMPTYP
               `(,FTY::X.FIX FTY::X)
               `(FTY::IFF (,FTY::X.FIX FTY::X) (CONSP FTY::X)))
          :HINTS (("goal" :EXPAND ((,FTY::X.FIX FTY::X)))))))
      (defthm ,FTY::FOO-FIX-OF-CONS
        (equal (,FTY::X.FIX (cons ,FTY::STDA ,FTY::STDX))
          (cons (,FTY::X.ELT-FIX ,FTY::STDA)
            ,(IF FTY::X.NON-EMPTYP
     (IF FTY::X.TRUE-LISTP
         `(AND (CONSP ,FTY::STDX) (,FTY::X.FIX ,FTY::STDX))
         `(IF (CONSP ,FTY::STDX)
              (,FTY::X.FIX ,FTY::STDX)
              ,FTY::STDX))
     `(,FTY::X.FIX ,FTY::STDX))))
        :hints (("goal" :expand ((:free (a b) (,FTY::X.FIX (cons a b)))))))
      (defthm ,FTY::LEN-OF-FOO-FIX
        (equal (len (,FTY::X.FIX x))
          ,(IF FTY::X.NON-EMPTYP
     `(MAX 1 (FTY::LEN FTY::X))
     `(FTY::LEN FTY::X)))
        :hints (("goal" :induct (len x)
           :expand ((,FTY::X.FIX x))
           :in-theory (enable len))))
      ,@(AND (NOT FTY::X.NON-EMPTYP)
       `((FTY::DEFTHM ,FTY::FOO-FIX-OF-APPEND
          (EQUAL (,FTY::X.FIX (APPEND STD::A STD::B))
                 (APPEND (,FTY::X.FIX STD::A) (,FTY::X.FIX STD::B)))
          :HINTS
          (("goal" :INDUCT (APPEND STD::A STD::B) :EXPAND
            ((,FTY::X.FIX STD::A)
             (:FREE (FTY::A FTY::B) (,FTY::X.FIX (CONS FTY::A FTY::B)))
             (,FTY::X.FIX NIL) (:FREE (FTY::B) (APPEND STD::A FTY::B))
             (:FREE (FTY::B) (APPEND NIL FTY::B))
             (:FREE (FTY::A FTY::B FTY::C)
              (APPEND (CONS FTY::A FTY::B) FTY::C)))
            :IN-THEORY (FTY::ENABLE (:I APPEND)))))))
      ,@(AND (NOT FTY::X.NON-EMPTYP)
       `((FTY::DEFTHM ,FTY::FOO-FIX-OF-REPEAT
          (EQUAL (,FTY::X.FIX (FTY::REPEAT FTY::N FTY::X))
                 (FTY::REPEAT FTY::N (,FTY::X.ELT-FIX FTY::X)))
          :HINTS
          (("goal" :INDUCT (FTY::REPEAT FTY::N FTY::X) :EXPAND
            ((FTY::REPEAT FTY::N FTY::X)
             (FTY::REPEAT FTY::N (,FTY::X.ELT-FIX FTY::X))
             (:FREE (FTY::A FTY::B) (,FTY::X.FIX (CONS FTY::A FTY::B))))
            :IN-THEORY (FTY::ENABLE (:I FTY::REPEAT)))))))
      ,@(AND FTY::X.TRUE-LISTP (NOT FTY::X.NON-EMPTYP)
       `((FTY::DEFTHM ,FTY::LIST-EQUIV-REFINES-FOO-EQUIV
          (FTY::IMPLIES (FTY::LIST-EQUIV FTY::X FTY::Y)
           (,FTY::X.EQUIV FTY::X FTY::Y))
          :HINTS
          (("Goal" :INDUCT (FAST-LIST-EQUIV FTY::X FTY::Y) :IN-THEORY
            (FTY::ENABLE ,FTY::X.FIX FAST-LIST-EQUIV LIST-EQUIV TRUE-LIST-FIX)
            :EXPAND
            ((TRUE-LIST-FIX FTY::X) (TRUE-LIST-FIX FTY::Y) (,FTY::X.FIX FTY::X)
             (,FTY::X.FIX FTY::Y))))
          :RULE-CLASSES :REFINEMENT)))
      ,@(AND (NOT FTY::X.NON-EMPTYP)
       `((FTY::DEFTHM ,FTY::NTH-OF-FOO-FIX
          (EQUAL (NTH FTY::N (,FTY::X.FIX FTY::X))
                 (IF (< (FTY::NFIX FTY::N) (FTY::LEN FTY::X))
                     (,FTY::X.ELT-FIX (NTH FTY::N FTY::X))
                     NIL))
          :HINTS
          (("goal" :INDUCT (NTH FTY::N FTY::X) :EXPAND ((,FTY::X.FIX FTY::X))
            :IN-THEORY (FTY::ENABLE NTH FTY::LEN FTY::NFIX))))
         (FTY::DEFTHM ,FTY::FOO-EQUIV-IMPLIES-FOO-EQUIV-APPEND-1
          (FTY::IMPLIES (,FTY::X.EQUIV FTY::X FTY::X-EQUIV)
           (,FTY::X.EQUIV (APPEND FTY::X FTY::Y) (APPEND FTY::X-EQUIV FTY::Y)))
          :RULE-CLASSES (:CONGRUENCE) :HINTS
          (("goal" :IN-THEORY (FTY::ENABLE ,FTY::X.EQUIV ,FTY::X.FIX APPEND)
            :INDUCT (APPEND FTY::X FTY::Y))))
         (FTY::DEFTHM ,FTY::FOO-EQUIV-IMPLIES-FOO-EQUIV-APPEND-2
          (FTY::IMPLIES (,FTY::X.EQUIV FTY::Y FTY::Y-EQUIV)
           (,FTY::X.EQUIV (APPEND FTY::X FTY::Y) (APPEND FTY::X FTY::Y-EQUIV)))
          :RULE-CLASSES (:CONGRUENCE) :HINTS
          (("goal" :IN-THEORY (FTY::ENABLE ,FTY::X.EQUIV ,FTY::X.FIX APPEND)
            :INDUCT (APPEND FTY::X FTY::Y))))
         (FTY::DEFCONG ,FTY::X.EQUIV ,FTY::X.EQUIV (NTHCDR FTY::N FTY::L) 2
          :HINTS
          (("goal" :IN-THEORY (FTY::ENABLE ,FTY::X.EQUIV ,FTY::X.FIX NTHCDR)
            :INDUCT T :EXPAND
            ((,FTY::X.FIX FTY::L) (,FTY::X.FIX FTY::L-EQUIV)))))
         (FTY::DEFCONG ,FTY::X.EQUIV ,FTY::X.EQUIV (FTY::TAKE FTY::N FTY::L) 2
          :HINTS
          (("goal" :IN-THEORY
            (FTY::ENABLE ,FTY::X.EQUIV ,FTY::X.FIX FTY::TAKE FTY::CONS-EQUAL
             FTY::DEFAULT-CAR)
            :INDUCT T :EXPAND
            ((,FTY::X.FIX FTY::L) (,FTY::X.FIX FTY::L-EQUIV))))))))))

(define flexlist-fix-when-pred-thm
  (x flagp)
  (b* (((flexlist x)) (foo-fix-when-foo-p (intern-in-package-of-symbol (cat (symbol-name x.fix)
            "-WHEN-"
            (symbol-name x.pred))
          x.fix)))
    `(defthm ,FTY::FOO-FIX-WHEN-FOO-P
      (implies (,FTY::X.PRED ,FTY::X.XVAR)
        (equal (,FTY::X.FIX ,FTY::X.XVAR) ,FTY::X.XVAR))
      :hints (,@(AND (NOT FTY::FLAGP) `(("goal" :INDUCT (,FTY::X.FIX ,FTY::X.XVAR)))) '(:expand ((,FTY::X.PRED ,FTY::X.XVAR) (,FTY::X.FIX ,FTY::X.XVAR))
          :in-theory (disable ,FTY::X.FIX ,FTY::X.PRED))) . ,(AND FTY::FLAGP `(:FLAG ,FTY::X.NAME)))))

(defun flexlist-count
  (x types)
  (b* (((flexlist x)) ((unless x.count) nil)
      (eltcount (flextypes-find-count-for-pred x.elt-type
          types)))
    `((define ,FTY::X.COUNT
       ((,FTY::X.XVAR ,FTY::X.PRED))
       :returns (count natp
         :rule-classes :type-prescription :hints ('(:expand (,FTY::X.COUNT ,FTY::X.XVAR)
            :in-theory (disable ,FTY::X.COUNT))))
       :measure (let ((,FTY::X.XVAR (,FTY::X.FIX ,FTY::X.XVAR)))
         ,FTY::X.MEASURE)
       ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::X.KWD-ALIST) `(:MEASURE-DEBUG T))
       :verify-guards nil
       :progn t
       ,(IF FTY::X.NON-EMPTYP
     `(IF (CONSP (CDR ,FTY::X.XVAR))
          (+ 1 ,@(AND FTY::ELTCOUNT `((,FTY::ELTCOUNT (CAR ,FTY::X.XVAR))))
             (,FTY::X.COUNT (CDR ,FTY::X.XVAR)))
          (+ 1 ,@(AND FTY::ELTCOUNT `((,FTY::ELTCOUNT (CAR ,FTY::X.XVAR))))))
     `(IF (ATOM ,FTY::X.XVAR)
          1
          (+ 1 ,@(AND FTY::ELTCOUNT `((,FTY::ELTCOUNT (CAR ,FTY::X.XVAR))))
             (,FTY::X.COUNT (CDR ,FTY::X.XVAR)))))))))

(defun flexlist-count-post-events
  (x types)
  (b* (((flexlist x)) ((unless x.count) nil)
      (eltcount (flextypes-find-count-for-pred x.elt-type
          types))
      (foo-count-of-cons (intern-in-package-of-symbol (cat (symbol-name x.count) "-OF-CONS")
          x.count))
      (foo-count-of-cdr (intern-in-package-of-symbol (cat (symbol-name x.count) "-OF-CDR")
          x.count))
      (foo-count-of-car (intern-in-package-of-symbol (cat (symbol-name eltcount) "-OF-CAR")
          x.count)))
    `((defthm ,FTY::FOO-COUNT-OF-CONS
       ,(LET ((FTY::BODY
        `(> (,FTY::X.COUNT (CONS FTY::A FTY::B))
            ,(IF FTY::ELTCOUNT
                 `(+ (,FTY::ELTCOUNT FTY::A) (,FTY::X.COUNT FTY::B))
                 `(,FTY::X.COUNT FTY::B)))))
   (IF FTY::X.NON-EMPTYP
       `(FTY::IMPLIES (CONSP FTY::B) ,FTY::BODY)
       FTY::BODY))
       :hints (("goal" :expand ((:free (a b) (,FTY::X.COUNT (cons a b))))))
       :rule-classes :linear) ,@(AND FTY::ELTCOUNT
       `((FTY::DEFTHM ,FTY::FOO-COUNT-OF-CAR
          (FTY::IMPLIES
           ,(IF FTY::X.NON-EMPTYP
                T
                `(CONSP ,FTY::X.XVAR))
           (< (,FTY::ELTCOUNT (CAR ,FTY::X.XVAR))
              (,FTY::X.COUNT ,FTY::X.XVAR)))
          ,@(AND FTY::X.NON-EMPTYP
                 `(:HINTS (("goal" :EXPAND ((,FTY::X.COUNT ,FTY::X.XVAR))))))
          :RULE-CLASSES :LINEAR)))
      (defthm ,FTY::FOO-COUNT-OF-CDR
        (implies ,(IF FTY::X.NON-EMPTYP
     `(CONSP (CDR ,FTY::X.XVAR))
     `(CONSP ,FTY::X.XVAR))
          (< (,FTY::X.COUNT (cdr ,FTY::X.XVAR))
            (,FTY::X.COUNT ,FTY::X.XVAR)))
        :rule-classes :linear))))