Struct kocheck::Opt

pub struct Opt {
    pub eta: bool,
    pub omit: Option<Stage>,
    pub channel_capacity: Option<Option<usize>>,
    pub jobs: Option<Option<usize>>,
    pub files: Vec<PathBuf>,
}

A typechecker for the lambda-Pi calculus modulo rewriting

Fields

eta: bool

Reduce terms modulo eta

When this is enabled, x => t and u are convertible if x => t and y => u y are convertible.

omit: Option<Stage>

Perform only operations until (excluding) the given stage.

channel_capacity: Option<Option<usize>>

Parse N commands in advance (∞ if argument omitted)

If this option is used, commands are parsed and checked simultaneously. If this option is given with a number N, then maximally N commands are parsed in advance. If this option is given without an extra argument, then the number of commands parsed in advance is unbounded.

Note that unbounded parsing can lead to high memory usage!

jobs: Option<Option<usize>>

Typecheck up to N commands concurrently (∞ if argument omitted)

If this option is used, type checking tasks are executed in parallel. If this option is given with a number N, then at most N type checking tasks are executed concurrently. If this option is given without an extra argument, then the number of concurrently executed tasks is determined automatically from the number of CPUs.

files: Vec<PathBuf>

Files to process (cumulative)

Every file is wrapped in a module corresponding to the file path. To read from standard input, use “-” as file name.

Implementations

impl Opt

pub fn omits(&self, stage: Stage) -> bool

Trait Implementations

impl Args for Opt

fn group_id() -> Option<Id>

Report the [ArgGroup::id][crate::ArgGroup::id] for this set of arguments

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

Append to [Command] so it can instantiate Self.

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

Append to [Command] so it can update self.

impl Clone for Opt

fn clone(&self) -> Opt

Returns a copy of the value.

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

Performs copy-assignment from source.

impl CommandFactory for Opt

fn command<'b>() -> Command

Build a [Command] that can instantiate Self.

fn command_for_update<'b>() -> Command

Build a [Command] that can update self.

impl Debug for Opt

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

Formats the value using the given formatter.

impl FromArgMatches for Opt

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( &mut self, __clap_arg_matches: &mut ArgMatches ) -> Result<(), Error>

Assign values from ArgMatches to self.

impl Parser for Opt

fn parse() -> Self

Parse from std::env::args_os(), exit on error

fn try_parse() -> Result<Self, Error>

Parse from std::env::args_os(), return Err on error.

fn parse_from<I, T>(itr: I) -> Self

where I: IntoIterator<Item = T>, T: Into<OsString> + Clone,

Parse from iterator, exit on error

fn try_parse_from<I, T>(itr: I) -> Result<Self, Error>

where I: IntoIterator<Item = T>, T: Into<OsString> + Clone,

Parse from iterator, return Err on error.

fn update_from<I, T>(&mut self, itr: I)

where I: IntoIterator<Item = T>, T: Into<OsString> + Clone,

Update from iterator, exit on error

fn try_update_from<I, T>(&mut self, itr: I) -> Result<(), Error>

where I: IntoIterator<Item = T>, T: Into<OsString> + Clone,

Update from iterator, return Err on error.