Enum Command 

pub enum Command<E: Extension> {
    Backend(BackendOptions<E>),
    JSON {
        output_file: PathOrDash,
        kind: Vec<ExportBodyKind>,
        use_ids: bool,
        include_extra: bool,
    },
    Serialize {
        kind: Vec<ExportBodyKind>,
        backend: Option<BackendName>,
    },
    CliExtension(E::Command),
}

Variants

Backend(BackendOptions<E>)

Translate to a backend. The translated modules will be written under the directory <PKG>/proofs/<BACKEND>/extraction, where <PKG> is the translated cargo package name and <BACKEND> the name of the backend.

JSON

Export directly as a JSON file

Fields

output_file: PathOrDash

Path to the output JSON file, “-” denotes stdout.

kind: Vec<ExportBodyKind>

Whether the bodies are exported as THIR, built MIR, const MIR, or a combination. Repeat this option to extract a combination (e.g. -k thir -k mir-built). Pass --kind alone with no value to disable body extraction.

use_ids: bool

By default, cargo hax json outputs a JSON where every piece of information is inlined. This however creates very large JSON files. This flag enables the use of unique IDs and outputs a map from IDs to actual objects.

include_extra: bool

Whether to include extra informations about DefIds.

Serialize

Serialize to a haxmeta file, the internal binary format used by hax to store the ASTs produced by the hax exporter.

Fields

kind: Vec<ExportBodyKind>

Whether the bodies are exported as THIR, built MIR, const MIR, or a combination. Repeat this option to extract a combination (e.g. -k thir -k mir-built). Pass --kind alone with no value to disable body extraction.

backend: Option<BackendName>

When extracting to a given backend, the exporter is called with different cfg options. This option allows to set the same flags as cargo hax into would pick.

CliExtension(E::Command)

Implementations

impl<E: Extension> Command<E>

pub fn body_kinds(&self) -> Vec<ExportBodyKind>

pub fn backend_name(&self) -> Option<BackendName>

Trait Implementations

impl<E: Clone + Extension> Clone for Command<E>

where E::Command: Clone,

fn clone(&self) -> Command<E>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<E: Debug + Extension> Debug for Command<E>

where E::Command: Debug,

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de, E> Deserialize<'de> for Command<E>

where E: Deserialize<'de> + Extension, E::Command: Deserialize<'de>,

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl<E: Extension> FromArgMatches for Command<E>

fn from_arg_matches(__clap_arg_matches: &ArgMatches) -> Result<Self, Error>

Instantiate Self from ArgMatches, parsing the arguments as needed.

fn from_arg_matches_mut( __clap_arg_matches: &mut ArgMatches, ) -> Result<Self, Error>

Instantiate Self from ArgMatches, parsing the arguments as needed.

fn update_from_arg_matches( &mut self, __clap_arg_matches: &ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

fn update_from_arg_matches_mut<'b>( &mut self, __clap_arg_matches: &mut ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

impl<E: Extension + JsonSchema> JsonSchema for Command<E>

fn schema_name() -> String

The name of the generated JSON Schema.

fn schema_id() -> Cow<'static, str>

Returns a string that uniquely identifies the schema produced by this type.

fn json_schema(generator: &mut SchemaGenerator) -> Schema

Generates a JSON Schema for this type.

fn is_referenceable() -> bool

Whether JSON Schemas generated for this type should be re-used where possible using the $ref keyword.

impl<E: Extension> NormalizePaths for Command<E>

fn normalize_paths(&mut self)

impl<E> Serialize for Command<E>

where E: Serialize + Extension, E::Command: Serialize,

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl<E: Extension> Subcommand for Command<E>

fn augment_subcommands<'b>(__clap_app: Command) -> Command

Append to Command so it can instantiate Self via FromArgMatches::from_arg_matches_mut

fn augment_subcommands_for_update<'b>(__clap_app: Command) -> Command

Append to Command so it can instantiate self via FromArgMatches::update_from_arg_matches_mut

fn has_subcommand(__clap_name: &str) -> bool

Test whether Self can parse a specific subcommand