use crate::{
ElicitCommunicator, ElicitIntrospect, ElicitResult, Elicitation, ElicitationPattern,
PatternDetails, Prompt, TypeMetadata,
};
use reqwest::{Client, Request, RequestBuilder};
use url::Url;
crate::default_style!(RequestBuilder => RequestBuilderStyle);
impl Prompt for RequestBuilder {
fn prompt() -> Option<&'static str> {
Some(
"Construct an HTTP request builder — provide the method and target URL. \
Additional configuration (headers, body, timeout) can be applied via \
subsequent builder method calls.",
)
}
}
impl Elicitation for RequestBuilder {
type Style = RequestBuilderStyle;
#[tracing::instrument(skip(communicator))]
async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
tracing::debug!("Eliciting reqwest::RequestBuilder");
let method = reqwest::Method::elicit(communicator).await?;
tracing::debug!(?method, "Method selected");
let url = Url::elicit(communicator).await?;
tracing::debug!(%url, "URL selected");
let request = Request::new(method, url);
Ok(RequestBuilder::from_parts(Client::new(), request))
}
fn kani_proof() -> proc_macro2::TokenStream {
crate::verification::proof_helpers::kani_trusted_opaque("request_builder")
}
fn verus_proof() -> proc_macro2::TokenStream {
crate::verification::proof_helpers::verus_trusted_opaque("request_builder")
}
fn creusot_proof() -> proc_macro2::TokenStream {
crate::verification::proof_helpers::creusot_trusted_opaque("request_builder")
}
}
impl ElicitIntrospect for RequestBuilder {
fn pattern() -> ElicitationPattern {
ElicitationPattern::Survey
}
fn metadata() -> TypeMetadata {
TypeMetadata {
type_name: "reqwest::RequestBuilder",
description: Self::prompt(),
details: PatternDetails::Survey {
fields: vec![
crate::FieldInfo {
name: "method",
type_name: "reqwest::Method",
prompt: Some("HTTP method (GET, POST, …)"),
},
crate::FieldInfo {
name: "url",
type_name: "url::Url",
prompt: Some("Target URL"),
},
],
},
}
}
}