fixtype - ACL2 Book

other

(in-package "FTY")

other

(include-book "xdoc/top" :dir :system)

other

(include-book "std/util/da-base" :dir :system)

other

(program)

other

(set-state-ok t)

other

(def-primitive-aggregate fixtype
  (name pred
    fix
    equiv
    executablep
    equiv-means-fixes-equal
    inline
    equal
    topic))

other

(table fixtypes)

get-fixtypes-alistfunction

(defun get-fixtypes-alist
  (world)
  (cdr (assoc 'fixtype-alist
      (table-alist 'fixtypes world))))

deffixtype-fnfunction

(defun deffixtype-fn
  (name predicate
    fix
    equiv
    executablep
    definep
    inline
    equal
    no-rewrite-quoted-constant
    topic
    verbosep
    hints
    forward)
  (if definep
    `(with-output ,@(AND (NOT FTY::VERBOSEP) '(:OFF :ALL :ON ERROR))
      :stack :push (encapsulate nil
        (logic)
        (local (make-event '(:or (with-output :stack :pop (defthm tmp-deffixtype-idempotent
                  (equal (,FTY::FIX (,FTY::FIX x)) (,FTY::FIX x))))
              (value-triple (er hard?
                  'deffixtype
                  "Failed to prove that ~x0 is idempotent.~%"
                  ',FTY::FIX)))))
        (,(COND ((NOT FTY::EXECUTABLEP) 'FTY::DEFUN-NX) ((NOT INLINE) 'DEFUN)
       (T 'FTY::DEFUN-INLINE)) ,FTY::EQUIV
          (x y)
          (declare (xargs :normalize nil
              ,@(AND FTY::EXECUTABLEP
       `(:GUARD (AND (,FTY::PREDICATE FTY::X) (,FTY::PREDICATE FTY::Y))))
              :verify-guards ,FTY::EXECUTABLEP))
          (,EQUAL (,FTY::FIX x) (,FTY::FIX y)))
        (local (in-theory '(,FTY::EQUIV tmp-deffixtype-idempotent
              booleanp-compound-recognizer)))
        (defequiv ,FTY::EQUIV :package :legacy)
        (defcong ,FTY::EQUIV
          equal
          (,FTY::FIX x)
          1
          :package :legacy)
        (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME FTY::FIX) "-UNDER-"
               (SYMBOL-NAME FTY::EQUIV))
  FTY::EQUIV)
          (,FTY::EQUIV (,FTY::FIX x) x)
          :rule-classes (:rewrite . ,(AND (NOT FTY::NO-REWRITE-QUOTED-CONSTANT) '(:REWRITE-QUOTED-CONSTANT))))
        ,@(AND FTY::FORWARD
       `((FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (CONCATENATE 'STRING "EQUAL-OF-" (SYMBOL-NAME FTY::FIX)
                         "-1-FORWARD-TO-" (SYMBOL-NAME FTY::EQUIV))
            FTY::EQUIV)
          (FTY::IMPLIES (EQUAL (,FTY::FIX FTY::X) FTY::Y)
           (,FTY::EQUIV FTY::X FTY::Y))
          :RULE-CLASSES :FORWARD-CHAINING)
         (FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (CONCATENATE 'STRING "EQUAL-OF-" (SYMBOL-NAME FTY::FIX)
                         "-2-FORWARD-TO-" (SYMBOL-NAME FTY::EQUIV))
            FTY::EQUIV)
          (FTY::IMPLIES (EQUAL FTY::X (,FTY::FIX FTY::Y))
           (,FTY::EQUIV FTY::X FTY::Y))
          :RULE-CLASSES :FORWARD-CHAINING)
         (FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (CONCATENATE 'STRING (SYMBOL-NAME FTY::EQUIV) "-OF-"
                         (SYMBOL-NAME FTY::FIX) "-1-FORWARD")
            FTY::EQUIV)
          (FTY::IMPLIES (,FTY::EQUIV (,FTY::FIX FTY::X) FTY::Y)
           (,FTY::EQUIV FTY::X FTY::Y))
          :RULE-CLASSES :FORWARD-CHAINING)
         (FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (CONCATENATE 'STRING (SYMBOL-NAME FTY::EQUIV) "-OF-"
                         (SYMBOL-NAME FTY::FIX) "-2-FORWARD")
            FTY::EQUIV)
          (FTY::IMPLIES (,FTY::EQUIV FTY::X (,FTY::FIX FTY::Y))
           (,FTY::EQUIV FTY::X FTY::Y))
          :RULE-CLASSES :FORWARD-CHAINING)))
        (table fixtypes
          'fixtype-alist
          (cons (cons ',FTY::NAME
              ',(FTY::MAKE-FIXTYPE :NAME FTY::NAME :PRED FTY::PREDICATE :FIX FTY::FIX :EQUIV
  FTY::EQUIV :EXECUTABLEP FTY::EXECUTABLEP :EQUIV-MEANS-FIXES-EQUAL
  (IF (AND FTY::EXECUTABLEP INLINE)
      (FTY::INTERN-IN-PACKAGE-OF-SYMBOL
       (CONCATENATE 'STRING (SYMBOL-NAME FTY::EQUIV) "$INLINE") FTY::EQUIV)
      FTY::EQUIV)
  :INLINE INLINE :EQUAL EQUAL :TOPIC FTY::TOPIC))
            (get-fixtypes-alist world)))))
    (b* ((thmname (intern-in-package-of-symbol (concatenate 'string
             "__DEFFIXTYPE-"
             (symbol-name equiv)
             "-MEANS-EQUAL-OF-"
             (symbol-name fix))
           'fty)))
      `(with-output ,@(AND (NOT FTY::VERBOSEP) '(:OFF :ALL))
        :stack :push (progn (make-event '(:or (encapsulate nil
                (logic)
                (with-output :stack :pop (defthm ,FTY::THMNAME
                    (implies (,FTY::EQUIV x y)
                      (equal (,FTY::FIX x) (,FTY::FIX y)))
                    :hints ,FTY::HINTS
                    :rule-classes nil)))
              (with-output :on (error)
                (value-triple (er hard?
                    'deffixtype
                    "Failed to prove that ~x0 implies equality of ~x1.  ~
                           You may provide :hints to help."
                    ',FTY::EQUIV
                    ',FTY::FIX)))))
          (table fixtypes
            'fixtype-alist
            (cons (cons ',FTY::NAME
                ',(FTY::MAKE-FIXTYPE :NAME FTY::NAME :PRED FTY::PREDICATE :FIX FTY::FIX :EQUIV
  FTY::EQUIV :EXECUTABLEP FTY::EXECUTABLEP :EQUIV-MEANS-FIXES-EQUAL
  FTY::THMNAME :INLINE INLINE :EQUAL EQUAL :TOPIC FTY::TOPIC))
              (get-fixtypes-alist world))))))))

deffixtypemacro

(defmacro deffixtype
  (name &key
    pred
    fix
    equiv
    (executablep 't)
    define
    verbosep
    hints
    forward
    (no-rewrite-quoted-constant 'nil)
    (inline 't)
    (equal 'equal)
    (topic 'nil topic-p))
  (declare (xargs :guard (and pred fix equiv)))
  (deffixtype-fn name
    pred
    fix
    equiv
    executablep
    define
    inline
    equal
    no-rewrite-quoted-constant
    (if topic-p
      topic
      name)
    verbosep
    hints
    forward))

find-fixtype-for-predfunction

(defun find-fixtype-for-pred
  (pred alist)
  (if (atom alist)
    nil
    (let* ((fixtype (cdar alist)))
      (if (eq (fixtype->pred fixtype) pred)
        fixtype
        (find-fixtype-for-pred pred (cdr alist))))))

find-fixtype-for-equivfunction

(defun find-fixtype-for-equiv
  (equiv alist)
  (if (atom alist)
    nil
    (let* ((fixtype (cdar alist)))
      (if (eq (fixtype->equiv fixtype) equiv)
        fixtype
        (find-fixtype-for-equiv equiv (cdr alist))))))

find-fixtype-for-typenamefunction

(defun find-fixtype-for-typename
  (name alist)
  (cdr (assoc name alist)))

find-fixtypefunction

(defun find-fixtype
  (typename alist)
  (or (find-fixtype-for-typename typename alist)
    (find-fixtype-for-pred typename alist)))

other

(defconst *deffixequiv-basic-keywords*
  '(:hints :skip-const-thm :skip-cong-thm :skip-ok :verbosep :out-equiv :other-var :thm-suffix :basename :pkg))

other

(def-primitive-aggregate fixequiv
  (form arg
    type
    kwd-alist
    fix-body
    fix-thm
    const-thm
    cong-thm))

deffixequiv-basic-parsefunction

(defun deffixequiv-basic-parse
  (form arg type keys state)
  (declare (xargs :mode :program :stobjs state))
  (b* ((__function__ 'deffixequiv-basic-parse) (world (w state))
      ((mv kwd-alist rest) (extract-keywords 'deffixequiv-basic
          *deffixequiv-basic-keywords*
          keys
          nil))
      ((when rest) (raise "Bad args: ~x0~%" rest))
      (fixtype-al (get-fixtypes-alist world))
      (stobjname (and (fgetprop arg 'stobj nil world)
          (congruent-stobj-rep arg world)))
      (fixtype (or (find-fixtype-for-typename type fixtype-al)
          (find-fixtype-for-pred type fixtype-al)
          (find-fixtype-for-typename stobjname
            fixtype-al)))
      (skip-ok (cdr (assoc :skip-ok kwd-alist)))
      ((unless fixtype) (if skip-ok
          (prog2$ (cw "Note: skipping ~x0 since its type ~x1 was not a ~
                         fixtype name or predicate~%"
              arg
              type)
            nil)
          (raise "Not a fixtype name or predicate: ~x0" type)))
      (fix (fixtype->fix fixtype))
      (equiv (fixtype->equiv fixtype))
      (hints (getarg :hints nil kwd-alist))
      (skip-cong-thm (getarg :skip-cong-thm nil kwd-alist))
      ((unless (and (consp form) (symbolp (car form)))) (raise "Form should be a function call term, but it's ~x0"
          form))
      (basename (getarg :basename (car form) kwd-alist))
      (pkg (or (getarg :pkg nil kwd-alist) basename))
      (pkg (if (equal (symbol-package-name pkg) "COMMON-LISP")
          'foo
          pkg))
      (out-equiv (getarg :out-equiv 'equal kwd-alist))
      (out-equiv-equiv-rune (equivalence-rune (deref-macro-name out-equiv
            (macro-aliases world))
          world))
      ((unless out-equiv-equiv-rune) (raise "Expected ~s0 to be a known equivalence relation"
          out-equiv))
      (under-out-equiv (if (eq out-equiv 'equal)
          ""
          (concatenate 'string "-UNDER-" (symbol-name out-equiv))))
      (suffix (getarg :thm-suffix "" kwd-alist))
      (fix-thmname (intern-in-package-of-symbol (concatenate 'string
            (symbol-name basename)
            "-OF-"
            (symbol-name fix)
            "-"
            (symbol-name arg)
            under-out-equiv
            suffix)
          pkg))
      (congruence-thmname (intern-in-package-of-symbol (concatenate 'string
            (symbol-name basename)
            "-"
            (symbol-name equiv)
            "-CONGRUENCE-ON-"
            (symbol-name arg)
            under-out-equiv
            suffix)
          pkg))
      (argequiv (or (getarg :other-var nil kwd-alist)
          (intern-in-package-of-symbol (concatenate 'string (symbol-name arg) "-EQUIV")
            pkg)))
      ((mv err tr-form) (translate-cmp form
          t
          nil
          nil
          'deffixequiv-basic-parse
          world
          (default-state-vars t)))
      ((when err) (raise "Error translating form: ~@0" tr-form))
      (vars (all-vars tr-form))
      ((unless (and (symbolp arg) (member arg vars))) (raise "Expected ~x0 to be among variables of ~x1"
          arg
          form))
      (subst-alist `((,FTY::ARG ,FTY::FIX ,FTY::ARG)))
      (fix-body `(,FTY::OUT-EQUIV ,(SUBLIS-VAR FTY::SUBST-ALIST FTY::FORM)
          ,FTY::FORM))
      (fix-thm `(defthm ,FTY::FIX-THMNAME
          ,FTY::FIX-BODY
          :hints ,FTY::HINTS))
      (cong-thm (and (not skip-cong-thm)
          `(defthm ,FTY::CONGRUENCE-THMNAME
            (implies (,FTY::EQUIV ,FTY::ARG ,FTY::ARGEQUIV)
              (,FTY::OUT-EQUIV ,FTY::FORM
                ,(SUBLIS-VAR `((,FTY::ARG . ,FTY::ARGEQUIV)) FTY::FORM)))
            :hints (("Goal" :in-theory nil
               :do-not '(preprocess)
               :use ((:instance ,FTY::FIX-THMNAME) (:instance ,FTY::FIX-THMNAME (,FTY::ARG ,FTY::ARGEQUIV))
                 (:instance ,(FTY::FIXTYPE->EQUIV-MEANS-FIXES-EQUAL FTY::FIXTYPE)
                   (x ,FTY::ARG)
                   (y ,FTY::ARGEQUIV)))))
            :rule-classes :congruence))))
    (make-fixequiv :form form
      :arg arg
      :type type
      :kwd-alist kwd-alist
      :fix-body fix-body
      :fix-thm fix-thm
      :cong-thm cong-thm)))

fixequiv-eventsfunction

(defun fixequiv-events
  (fixequiv)
  (b* (((unless fixequiv) '(value-triple :skipped)) ((fixequiv x) fixequiv))
    `(progn (with-output :stack :pop ,FTY::X.FIX-THM)
      ,@(AND FTY::X.CONST-THM `((FTY::WITH-OUTPUT :ON (ERROR) ,FTY::X.CONST-THM)))
      ,@(AND FTY::X.CONG-THM
       `((FTY::MAKE-EVENT
          '(:OR (FTY::WITH-OUTPUT :ON (ERROR) ,FTY::X.CONG-THM)
            (FTY::WITH-OUTPUT :ON (ERROR)
             (FTY::VALUE-TRIPLE
              (FTY::ER FTY::HARD? 'FTY::FIXEQUIV
               "The congruence theorem failed: this is unexpected because ~
                  this should be automatic once the fixing theorem succeeds.  ~
                  Please try again with :verbosep t to diagnose the problem."))))))))))

deffixequiv-basicmacro

(defmacro deffixequiv-basic
  (fn arg type &rest keys)
  (b* ((verbosep (let ((lst (member :verbosep keys)))
         (and lst (cadr lst)))))
    `(with-output ,@(AND (NOT FTY::VERBOSEP) '(:OFF :ALL))
      :stack :push (make-event (let ((formals (fgetprop ',FTY::FN 'formals :none (w state))))
          (fixequiv-events (deffixequiv-basic-parse (cons ',FTY::FN formals)
              ',FTY::ARG
              ',TYPE
              (cons (cons :pkg ',FTY::FN) ',FTY::KEYS)
              state)))))))

deffixcong-parsefunction

(defun deffixcong-parse
  (in-equiv out-equiv
    form
    var
    keys
    state)
  (b* ((fixtypes (get-fixtypes-alist (w state))) (in-fixtype (find-fixtype-for-equiv in-equiv fixtypes)))
    (deffixequiv-basic-parse form
      var
      (fixtype->name in-fixtype)
      (list* :out-equiv out-equiv keys)
      state)))

deffixcongmacro

(defmacro deffixcong
  (in-equiv out-equiv
    form
    var
    &rest
    keys)
  (b* ((verbosep (let ((lst (member :verbosep keys)))
         (and lst (cdr lst)))))
    `(with-output ,@(AND (NOT FTY::VERBOSEP) '(:OFF :ALL))
      :stack :push (make-event (fixequiv-events (deffixcong-parse ',FTY::IN-EQUIV
            ',FTY::OUT-EQUIV
            ',FTY::FORM
            ',FTY::VAR
            ',FTY::KEYS
            state))))))