hax_types/cli_options/
extension.rs

1/// This module defines a way to extend externally the CLI of hax, via
2/// the `Extension` trait. This trait defines one associated type per
3/// extension point.
4use crate::prelude::*;
5
6use clap::{Parser, Subcommand};
7
8macro_rules! trait_alias {
9    ($name:ident = $($base:tt)+) => {
10        pub trait $name: $($base)+ { }
11        impl<T: $($base)+> $name for T { }
12    };
13}
14
15trait_alias!(
16    ExtensionPoint =
17        std::fmt::Debug
18        + for<'a> serde::Deserialize<'a>
19        + serde::Serialize
20        + JsonSchema
21        + Clone
22);
23
24trait_alias!(SubcommandExtensionPoint = ExtensionPoint + clap::Subcommand);
25trait_alias!(ArgsExtensionPoint = ExtensionPoint + clap::Args);
26
27#[derive_group(Serializers)]
28#[derive(JsonSchema, Parser, Debug, Clone)]
29pub struct EmptyArgsExtension {}
30
31#[derive_group(Serializers)]
32#[derive(JsonSchema, Subcommand, Debug, Clone)]
33pub enum EmptySubcommandExtension {}
34
35pub trait Extension: 'static {
36    type Options: ArgsExtensionPoint;
37    type Command: SubcommandExtensionPoint;
38    type BackendOptions: ArgsExtensionPoint;
39    type FStarOptions: ArgsExtensionPoint;
40}
41
42impl Extension for () {
43    type Options = EmptyArgsExtension;
44    type Command = EmptySubcommandExtension;
45    type BackendOptions = EmptyArgsExtension;
46    type FStarOptions = EmptyArgsExtension;
47}
hax_types/cli_options/extension.rs

hax_types/cli_options/
extension.rs
