properties

(defun gen-property-accessors-updators
  (tbl a)
  (if (endp a)
    nil
    (b* ((`((,ACL2S::KEY . &) . &) a) (acc (make-symbl `(get- ,ACL2S::TBL - ,ACL2S::KEY)
            "ACL2S"))
        (upd (make-symbl `(set- ,ACL2S::TBL - ,ACL2S::KEY)
            "ACL2S")))
      (list* `(defmacro ,ACL2S::ACC
          nil
          (tbl-get-fn ',ACL2S::TBL ,ACL2S::KEY))
        `(defmacro ,ACL2S::UPD
          (x)
          (tbl-set-fn ',ACL2S::TBL ,ACL2S::KEY x))
        (gen-property-accessors-updators tbl
          (cdr a))))))

(defun parse-property
  (args state)
  (declare (xargs :mode :program :stobjs (state)))
  (b* ((pkg (current-package state)) (wrld (w state))
      (tbl (table-alist 'type-metadata-table wrld))
      (atbl (table-alist 'type-alias-table wrld))
      (ctx 'property)
      (name? (legal-variablep (car args)))
      (name (and name? (car args)))
      (args (if name?
          (cdr args)
          args))
      (pt (acl2s-property-table wrld))
      (pt (remove1-assoc-eq-lst (filter-keywords args)
          pt))
      ((mv kwd-alist prop-rest) (extract-keywords ctx
          *property-keywords*
          args
          pt
          nil))
      (debug? (get1 :debug? kwd-alist))
      (debug-all? (== debug? :all))
      (- (cw? debug-all?
          "~%**prop-rest is: ~x0~%"
          prop-rest))
      (- (cw? debug-all?
          "~|**kwd-alist is: ~x0~%"
          kwd-alist))
      (vars? (assoc :vars kwd-alist))
      (- (cw? debug-all?
          "~|**vars? is: ~x0~%"
          vars?))
      ((when (and (! vars?)
           (! (proper-argsp (car prop-rest))))) (ecw "~%**ERROR: The argument list: ~x0 is not well-formed."
          (car prop-rest)
          nil))
      (ivars? (and (! vars?)
          (cons :vars (process-typed-args (car prop-rest)))))
      (vars? (or vars? ivars?))
      (- (cw? debug-all?
          "~|**vars? is: ~x0~%"
          vars?))
      (prop-rest (if ivars?
          (cdr prop-rest)
          prop-rest))
      (hyps? (assoc :hyps kwd-alist))
      (hyps? (or hyps? (assoc :h kwd-alist)))
      (body? (assoc :body kwd-alist))
      (body? (or body? (assoc :b kwd-alist)))
      (check-contracts? (get1 :check-contracts? kwd-alist))
      (test-contracts? (get1 :test-contracts? kwd-alist))
      (body (cond (body? (or (get1 :body kwd-alist)
              (get1 :b kwd-alist)))
          (hyps? (car prop-rest))
          (t (extract-body (car prop-rest)))))
      (hyps-list (cond (hyps? (hyps-list-from-hyps (or (get1 :hyps kwd-alist)
                (get1 :h kwd-alist))))
          (body? nil)))
      ((mv erp pt-hyps-list) (if (or hyps? body?)
          (mv nil nil)
          (pseudo-translate (car prop-rest) nil wrld)))
      ((when erp) (ecw "~%**ERROR: The translation of hyps: ~
              ~x0 ~
              resulted in an error."
          (car prop-rest)
          nil))
      (hyps-list (if pt-hyps-list
          (extract-hyps pt-hyps-list)
          hyps-list))
      (find-duplicate-hyp (find-first-duplicate hyps-list))
      (- (cw? find-duplicate-hyp
          "~%**Warning: Your property has a duplicate hypothesis, ~x0. ~
                ~%**This may indicate an error.~%"
          find-duplicate-hyp))
      (hyps-list (remove-dups hyps-list))
      (user-var-list (cdr vars?))
      (user-vars (evens user-var-list))
      (user-types (odds user-var-list))
      (user-types (map-intern-types user-types pkg))
      (- (cw? debug-all?
          "~|**user-types is: ~x0~%"
          user-types))
      (user-preds (map-preds user-types tbl atbl))
      (- (cw? debug-all?
          "~|**user-preds is: ~x0~%"
          user-preds))
      (bad-type (find-bad-d-arg-types user-types
          user-preds))
      ((when bad-type) (ecw "~%**ERROR: One of the argument types, ~x0, is not a type."
          bad-type
          nil))
      (type-list1 (make-input-contract user-vars
          user-preds))
      (type-list (hyps-list-from-hyps type-list1))
      (type-hyps-list (append type-list hyps-list))
      (- (cw? debug-all?
          "~|**type-hyps-list is: ~x0~%"
          type-hyps-list))
      (prop (cond ((endp type-hyps-list) body)
          ((endp (cdr type-hyps-list)) `(implies ,(CAR ACL2S::TYPE-HYPS-LIST) ,ACL2S::BODY))
          (t `(implies (and ,@ACL2S::TYPE-HYPS-LIST) ,ACL2S::BODY))))
      ((mv erp trans-prop) (pseudo-translate prop nil wrld))
      (all-vars (all-vars trans-prop))
      (vars (if vars?
          user-vars
          all-vars))
      (- (cw? debug-all?
          "~|**vars is: ~x0~%"
          vars))
      (- (cw? debug-all?
          "~|**all-vars is: ~x0~%"
          all-vars))
      (var-diff (sym-diff vars all-vars))
      (- (cw? debug-all?
          "~|**prop is: ~x0~%"
          prop))
      (- (cw? debug-all?
          "~|**trans-prop is: ~x0~%"
          trans-prop))
      (parsed (list name? name prop kwd-alist))
      ((when erp) (ecw "~%**ERROR: The translation of prop: ~
              ~x0 ~
              resulted in an error."
          prop
          parsed))
      ((unless (or (consp prop-rest) body?)) (ecw "~%**ERROR: Empty properties are not allowed."
          parsed))
      ((when var-diff) (ecw "~%**ERROR: The :vars provided do not match the actual variables ~
                appearing in the property. An example is ~x0."
          (car var-diff)
          parsed))
      (gprop (sublis-fn-simple '((implies . impliez))
          trans-prop))
      (- (cw? debug-all?
          "~|**gprop is: ~x0~%"
          gprop))
      ((mv gc-erp val) (if check-contracts?
          (guard-obligation gprop
            nil
            nil
            t
            ctx
            state)
          (guard-obligation t
            nil
            nil
            t
            ctx
            state)))
      ((list* & cl &) val)
      (gc-guards (if gc-erp
          t
          (prettyify-clause-set cl nil wrld)))
      (check-guards (if (and check-contracts? (not gc-erp))
          gc-guards
          t))
      ((mv gt-erp val) (if test-contracts?
          (guard-obligation-testing gprop
            nil
            nil
            t
            ctx
            state)
          (guard-obligation t
            nil
            nil
            t
            ctx
            state)))
      ((when gt-erp) (ecw "~%**ERROR Determining Contract Checking Proof Obligation.** ~
              ~%**val is: ~x0"
          val
          parsed))
      ((list* & cl &) val)
      (gt-guards (prettyify-clause-set cl nil wrld))
      (test-guards (if test-contracts?
          gt-guards
          t))
      (- (cw? debug?
          "~|**The Original Contract Checking Proof Obligation is: ~x0~%"
          gc-guards))
      (- (cw? debug?
          "~|**The Original Contract Testing Proof Obligation is: ~x0~%"
          gt-guards))
      (- (cw? debug?
          "~|**The Contract Checking Proof Obligation is: ~x0~%"
          check-guards))
      (- (cw? debug?
          "~|**The Contract Testing Proof Obligation is: ~x0~%"
          test-guards))
      (proof-timeout (get1 :proof-timeout kwd-alist))
      (testing-timeout (get1 :testing-timeout kwd-alist))
      (- (cw? (and check-contracts? (not gc-erp))
          "~%Form:  ( CONTRACT-CHECKING PROPERTY ...)"))
      (- (cw "~%"))
      ((mv te-thm-erp val state) (if (and check-contracts? (not gc-erp))
          (with-time-limit proof-timeout
            (trans-eval `(with-output ,@(IF ACL2S::DEBUG?
      '(:ON :ALL :SUMMARY-ON :ALL :GAG-MODE NIL :OFF
        (ACL2S::PROOF-BUILDER ACL2S::PROOF-TREE))
      (IF ACL2S::CHECK-CONTRACTS?
          '(:OFF :ALL :ON (ACL2S::SUMMARY ACL2S::COMMENT) :SUMMARY-ON :ALL
            :SUMMARY-OFF (:OTHER-THAN TIME))
          '(:OFF :ALL :SUMMARY-OFF :ALL :ON ACL2S::COMMENT)))
                (thm-no-test ,ACL2S::CHECK-GUARDS))
              ctx
              state
              t))
          (mv nil nil state)))
      ((list* & thm-erp &) val)
      (- (cw? debug-all?
          "~|**te-thm-erp is: ~x0~%"
          te-thm-erp))
      (- (cw? debug-all?
          "~|**val is: ~x0~%"
          val))
      (- (cw? debug-all?
          "~|**thm-erp is: ~x0~%"
          thm-erp))
      (- (cw? thm-erp
          "~%**ERROR During Contract Checking.** ~
              ~|**The Contract Checking Proof Obligation is: ~x0"
          check-guards))
      (- (cw? (and test-contracts?
            (or thm-erp
              gc-erp
              (not check-contracts?)))
          "~%Form:  ( TESTING PROPERTY CONTRACTS ...)"))
      ((mv te-test-erp val state) (if (and test-contracts?
            (or thm-erp
              gc-erp
              (not check-contracts?)))
          (with-time-limit testing-timeout
            (trans-eval `(with-output ,@(IF ACL2S::DEBUG?
      '(:ON :ALL :OFF (ACL2S::PROOF-BUILDER ACL2S::PROOF-TREE) :GAG-MODE NIL)
      '(:OFF :ALL :ON (ERROR ACL2S::COMMENT)))
                (test? ,ACL2S::TEST-GUARDS
                  ,@(IF ACL2S::DEBUG?
      'NIL
      '(:PRINT-CGEN-SUMMARY NIL :NUM-WITNESSES 0))))
              ctx
              state
              t))
          (mv nil nil state)))
      ((list* & test-erp &) val)
      (- (cw? debug-all?
          "~|**te-test-erp is: ~x0~%"
          te-test-erp))
      (- (cw? debug-all?
          "~|**val is: ~x0~%"
          val))
      (- (cw? debug-all?
          "~|**test-erp is: ~x0~%"
          test-erp))
      ((when gc-erp) (ecw "~%**ERROR Determining Contract Checking Proof Obligation.** ~
              ~%**val is: ~x0"
          val
          parsed))
      ((when test-erp) (ecw "~%**Contract Testing Error. The hypotheses of your property must imply:~
~%  ~x0.~
~%The counterexample above shows that this is not the case."
          test-guards
          parsed))
      ((when thm-erp) (ecw "~%**Contract Checking Error. The hypotheses of your property must imply:~
~%  ~x0."
          check-guards
          parsed)))
    (value parsed)))

(defun contract-check
  (form kwd-val-lst state)
  (declare (xargs :mode :program :stobjs (state)))
  (b* ((wrld (w state)) (ctx 'contract-check)
      (prop form)
      (- (cw? t "~%**Property is: ~x0~%" prop))
      (gprop (sublis-fn-simple '((implies . impliez))
          prop))
      ((mv erp val) (guard-obligation gprop
          nil
          nil
          t
          ctx
          state))
      ((when erp) (er soft
          ctx
          "~|**ERROR During Contract Checking.**"))
      ((list* & cl &) val)
      (guards (prettyify-clause-set cl nil wrld))
      (- (cw? t
          "~|**The Contract Completion Proof Obligation is: ~x0~%"
          guards))
      (- (cw? t
          "~%Form:  ( CONTRACT-CHECKING PROPERTY ...)~%"))
      (cgen-state (make-cgen-state-fn form
          (cons :user-defined ctx)
          kwd-val-lst
          (w state)))
      (timeout (cget cgen-timeout))
      ((mv te-thm-erp val state) (with-time-limit timeout
          (trans-eval `(with-output :off :all :on (summary comment)
              :summary-off (:other-than time)
              :gag-mode nil
              (encapsulate nil
                (with-output :off :all :on comment
                  (thm-no-test ,ACL2S::GUARDS))))
            ctx
            state
            t)))
      ((list* & thm-erp &) val)
      (- (cw? t
          "~|**trans-eval-thm-erp is: ~x0~%"
          te-thm-erp))
      (- (cw? t "~|**val is: ~x0~%" val))
      (- (cw? t "~|**thm-erp is: ~x0~%" thm-erp))
      (- (cw? thm-erp
          "~|Form:  ( TESTING PROPERTY CONTRACTS ...)"))
      ((mv te-test-erp val state) (if thm-erp
          (with-time-limit timeout
            (trans-eval `(with-output :off :all :on (error comment)
                (test? ,ACL2S::GUARDS
                  :print-cgen-summary nil
                  :num-witnesses 0))
              ctx
              state
              t))
          (mv nil nil state)))
      ((list* & test-erp &) val)
      (- (cw? t
          "~|**trans-eval-test-erp is: ~x0~%"
          te-test-erp))
      (- (cw? t "~|**val is: ~x0~%" val))
      (- (cw? t "~|**test-erp is: ~x0~%" test-erp))
      ((when test-erp) (er soft
          ctx
          "~%**Contract Completion Error. The hypotheses of your property must imply:~
~%  ~x0.~
~%The counterexample above shows that this is not the case."
          guards))
      ((when thm-erp) (er soft
          ctx
          "~%**Contract Completion Error. The hypotheses of your property must imply:~
~%  ~x0."
          guards)))
    (value t)))

(defun property-core
  (parsed)
  (declare (xargs :mode :program))
  (b* (((list name? name prop kwd-alist) parsed) (proofs? (get1 :proofs? kwd-alist))
      (testing? (get1 :testing? kwd-alist))
      (debug? (get1 :debug? kwd-alist))
      (debug-all? (== debug? :all))
      (proof-timeout (get1 :proof-timeout kwd-alist))
      (testing-timeout (get1 :testing-timeout kwd-alist))
      (prove (cond ((and name? testing?) 'defthm)
          (name? 'defthm-no-test)
          (testing? 'thm)
          (t 'thm-no-test)))
      (other-kwds (remove1-assoc-eq-lst (append (if name?
              nil
              *property-just-defthm-keywords*)
            *property-core-keywords*
            *property-conjecture-keywords*)
          kwd-alist))
      (- (cw? debug-all?
          "~|Kwd-alist: ~x0~%"
          kwd-alist))
      (- (cw? debug-all?
          "~|Other-kwds: ~x0~%"
          other-kwds))
      (flat-kwds (gen-other-keywords other-kwds))
      (- (cw? debug-all?
          "~|Flat-kwds: ~x0~%"
          flat-kwds))
      (args (if name?
          (list* name prop flat-kwds)
          (list* prop flat-kwds)))
      ((when proofs?) `(with-output :off :all :on (comment summary)
          :summary-on :all :summary-off (:other-than time)
          (encapsulate nil
            (value-triple (cw "~|Form:  ( PROVING PROPERTY )~%"))
            (with-time-limit ,ACL2S::PROOF-TIMEOUT
              (with-output ,@(IF ACL2S::DEBUG?
      '(:ON :ALL :OFF (ACL2S::PROOF-BUILDER ACL2S::PROOF-TREE) :SUMMARY-ON :ALL
        :GAG-MODE NIL)
      '(:STACK :POP :ON (ERROR ACL2S::SUMMARY ACL2S::COMMENT) :SUMMARY-ON :ALL
        :SUMMARY-OFF (:OTHER-THAN TIME ACL2S::RULES ACL2S::WARNINGS)))
                (,ACL2S::PROVE ,@ACL2S::ARGS)))
            (value-triple (cw "~|Form:  ( ACCEPTED PROPERTY AS THEOREM )~%")))))
      ((when (and testing? name?)) `(with-output :off :all :on (comment summary)
          :summary-on :all :summary-off (:other-than time)
          (encapsulate nil
            (value-triple (cw "~|Form:  ( TESTING PROPERTY )~%"))
            (with-time-limit ,ACL2S::TESTING-TIMEOUT
              (with-output ,@(IF ACL2S::DEBUG?
      '(:ON :ALL :OFF (ACL2S::PROOF-BUILDER ACL2S::PROOF-TREE) :SUMMARY-ON :ALL
        :GAG-MODE NIL)
      '(:STACK :POP :ON (ERROR ACL2S::SUMMARY ACL2S::COMMENT) :SUMMARY-ON :ALL
        :SUMMARY-OFF (:OTHER-THAN TIME ACL2S::RULES ACL2S::WARNINGS)))
                (defthm-test-no-proof ,@ACL2S::ARGS)))
            (value-triple (cw "~|Form:  ( ACCEPTED PROPERTY AS A THEOREM WITHOUT PROOF )~%")))))
      ((when testing?) `(with-output :off :all :on (comment summary)
          :summary-on :all :summary-off (:other-than time)
          (encapsulate nil
            (value-triple (cw "~|Form:  ( TESTING PROPERTY )~%"))
            (with-time-limit ,ACL2S::TESTING-TIMEOUT
              (with-output ,@(IF ACL2S::DEBUG?
      '(:ON :ALL :OFF (ACL2S::PROOF-BUILDER ACL2S::PROOF-TREE) :SUMMARY-ON :ALL
        :GAG-MODE NIL)
      '(:OFF :ALL :ON (ERROR ACL2S::COMMENT)))
                (test? ,@ACL2S::ARGS)))
            (value-triple (cw "~|Form:  ( PROPERTY PASSED TESTING )~%")))))
      ((when name?) `(with-output :off :all :on (comment summary)
          :summary-on :all :summary-off (:other-than time)
          (encapsulate nil
            (value-triple (cw "~|Form:  ( ANALYZING PROPERTY )~%"))
            (with-time-limit ,ACL2S::PROOF-TIMEOUT
              (with-output ,@(IF ACL2S::DEBUG?
      '(:ON :ALL :OFF (ACL2S::PROOF-BUILDER ACL2S::PROOF-TREE) :SUMMARY-ON :ALL
        :GAG-MODE NIL)
      '(:STACK :POP :ON (ERROR ACL2S::SUMMARY ACL2S::COMMENT) :SUMMARY-ON :ALL
        :SUMMARY-OFF (:OTHER-THAN TIME ACL2S::WARNINGS)))
                (defthmskipall ,@ACL2S::ARGS)))
            (value-triple (cw "~|Form:  ( ACCEPTED PROPERTY AS A THEOREM WITHOUT PROOF )~%"))))))
    `(value-triple :passed)))

(defun property-fn
  (args state)
  (declare (xargs :mode :program :stobjs (state)))
  (b* (((mv erp parsed state) (parse-property args state)) ((list - - - kwd-alist) parsed)
      (debug? (get1 :debug? kwd-alist))
      (debug-hint (if debug?
          ""
          " To debug, add ":debug? t" at the end of your property.~%"))
      ((when erp) (ecw "~%~|******** PROPERTY FAILED ********~% ~@0"
          debug-hint
          nil)))
    (value `(make-event ',(ACL2S::PROPERTY-CORE ACL2S::PARSED)))))