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        + Eq
23        + PartialEq
24);
25
26trait_alias!(SubcommandExtensionPoint = ExtensionPoint + clap::Subcommand);
27trait_alias!(ArgsExtensionPoint = ExtensionPoint + clap::Args);
28
29#[derive_group(Serializers)]
30#[derive(JsonSchema, Parser, Debug, Clone, Eq, PartialEq)]
31pub struct EmptyArgsExtension {}
32
33#[derive_group(Serializers)]
34#[derive(JsonSchema, Subcommand, Debug, Clone, Eq, PartialEq)]
35pub enum EmptySubcommandExtension {}
36
37pub trait Extension: 'static {
38    type Options: ArgsExtensionPoint;
39    type Command: SubcommandExtensionPoint;
40    type BackendOptions: ArgsExtensionPoint;
41    type FStarOptions: ArgsExtensionPoint;
42    type LeanOptions: ArgsExtensionPoint;
43}
44
45impl Extension for () {
46    type Options = EmptyArgsExtension;
47    type Command = EmptySubcommandExtension;
48    type BackendOptions = EmptyArgsExtension;
49    type FStarOptions = EmptyArgsExtension;
50    type LeanOptions = EmptyArgsExtension;
51}
hax_types/cli_options/extension.rs

hax_types/cli_options/
extension.rs
