		Search-engine friendly clone of the ACL2 documentation.

Htclient

Post

Issue an HTTP/HTTPS POST command.

Signature
(post url data state &key (connect-timeout '10) (read-timeout '10)) → (mv error val state)
Arguments: url — Address to send POST command to.
Guard (stringp url).; data — Alist of form keys and data, both as strings.
Guard (alistp data).; connect-timeout — Max seconds to wait for a connection.
Guard (atom connect-timeout).; read-timeout — Max seconds to wait for a reply.
Guard (atom read-timeout).
Returns: error — NIL on success or an error msg on failure.; val — On success: a string response.
Type (stringp val).; state — Type (state-p1 state), given (force (state-p1 state)).

In the logic this function reads from the ACL2 oracle. In the execution we send the http/https POST request to url.

Examples

(htclient::post "https://httpbin.org/post"
    '(("n" . "3") ("checkpoints" . "((ACL-NUMBERP A))")) state)

Definitions and Theorems

Function: post-fn

(defun post-fn (url data state connect-timeout read-timeout)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (stringp url)
                              (alistp data)
                              (atom connect-timeout)
                              (atom read-timeout))))
  (let ((__function__ 'post))
    (declare (ignorable __function__))
    (b* ((- (raise "Raw Lisp definition not installed?"))
         ((mv ?err1 val1 state)
          (read-acl2-oracle state))
         ((mv ?err2 val2 state)
          (read-acl2-oracle state))
         ((when val1) (mv val1 "" state)))
      (mv nil (acl2::str-fix val2) state))))

Theorem: stringp-of-post.val

(defthm stringp-of-post.val
  (b* (((mv common-lisp::?error ?val acl2::?state)
        (post-fn url data
                 state connect-timeout read-timeout)))
    (stringp val))
  :rule-classes :rewrite)

Theorem: state-p1-of-post.state

(defthm state-p1-of-post.state
  (implies (force (state-p1 state))
           (b* (((mv common-lisp::?error ?val acl2::?state)
                 (post-fn url data
                          state connect-timeout read-timeout)))
             (state-p1 state)))
  :rule-classes :rewrite)