		Search-engine friendly clone of the ACL2 documentation.

Htclient

Post

Issue an HTTP/HTTPS POST command.

Signature
(post url data state) → (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).
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

(defun post (url data state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard (and (stringp url) (alistp data))))
       (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 url data state)))
            (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 url data state)))
                     (state-p1 state)))
        :rule-classes :rewrite)