use crate::Stage;
use clap::Parser;
use std::path::PathBuf;

#[derive(Clone, Debug, Parser)]
#[clap(version)]
/// A typechecker for the lambda-Pi calculus modulo rewriting
pub struct Opt {
    /// Reduce terms modulo eta
    ///
    /// When this is enabled,
    /// `x => t` and `u` are convertible if
    /// `x => t` and `y => u y` are convertible.
    #[clap(long)]
    pub eta: bool,

    /// Perform only operations until (excluding) the given stage.
    #[clap(long, value_name = "STAGE", arg_enum)]
    pub omit: Option<Stage>,

    /// 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!
    #[clap(long, short = 'c', value_name = "N")]
    pub channel_capacity: 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.
    #[clap(long, short = 'j', value_name = "N")]
    pub jobs: Option<Option<usize>>,

    /// 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.
    #[clap(name = "FILE", required = true)]
    pub files: Vec<PathBuf>,
}

impl Opt {
    pub fn omits(&self, stage: Stage) -> bool {
        self.omit == Some(stage)
    }
}
