Enum agda_mode::cmd::Cmd

pub enum Cmd {
    Load {
        path: String,
        flags: Vec<String>,
    },
    Compile {
        backend: String,
        path: String,
        flags: Vec<String>,
    },
    Constraints,
    Metas,
    ShowModuleContentsToplevel {
        rewrite: Rewrite,
        search: String,
    },
    SearchAboutToplevel {
        rewrite: Rewrite,
        search: String,
    },
    SolveAll(Rewrite),
    SolveOne(InputWithRewrite),
    AutoOne(GoalInput),
    AutoAll,
    InferToplevel {
        rewrite: Rewrite,
        code: String,
    },
    ComputeToplevel {
        compute_mode: ComputeMode,
        code: String,
    },
    LoadHighlightingInfo {
        path: String,
    },
    TokenHighlighting {
        path: String,
        remove: Remove,
    },
    Highlight(GoalInput),
    ShowImplicitArgs(bool),
    ToggleImplicitArgs,
    Give {
        force: UseForce,
        input: GoalInput,
    },
    Refine(GoalInput),
    Intro {
        dunno: bool,
        input: GoalInput,
    },
    RefineOrIntro {
        dunno: bool,
        input: GoalInput,
    },
    Context(InputWithRewrite),
    HelperFunction(InputWithRewrite),
    Infer(InputWithRewrite),
    GoalType(InputWithRewrite),
    ElaborateGive(InputWithRewrite),
    GoalTypeContext(InputWithRewrite),
    GoalTypeContextInfer(InputWithRewrite),
    GoalTypeContextCheck(InputWithRewrite),
    ShowModuleContents(InputWithRewrite),
    MakeCase(GoalInput),
    Compute {
        compute_mode: ComputeMode,
        input: GoalInput,
    },
    WhyInScope(GoalInput),
    WhyInScopeToplevel(String),
    ShowVersion,
    Abort,
}

Variants

Load

Loads the module in file path, using flags as the command-line options.

Fields of Load

path: Stringflags: Vec<String>

Compile

Compiles the module in file path using the backend backend, using flags as the command-line options.

Fields of Compile

backend: Stringpath: Stringflags: Vec<String>

Constraints

Metas

Show unsolved metas. If there are no unsolved metas but unsolved constraints, show those instead.

ShowModuleContentsToplevel

Shows all the top-level names in the given module, along with their types. Uses the top-level scope.

Fields of ShowModuleContentsToplevel

rewrite: Rewritesearch: String

SearchAboutToplevel

Shows all the top-level names in scope which mention all the given identifiers in their type.

Fields of SearchAboutToplevel

rewrite: Rewritesearch: String

SolveAll(Rewrite)

Solve all goals whose values are determined by the constraints.

SolveOne(InputWithRewrite)

Solve the goal at point whose value is determined by the constraints.

AutoOne(GoalInput)

Solve the goal at point by using Auto.

AutoAll

Solve all goals by using Auto.

InferToplevel

Parse the given expression (as if it were defined at the

Fields of InferToplevel

rewrite: Rewrite

Normalise the type?

code: String

ComputeToplevel

Parse and type check the given expression (as if it were defined at the top-level of the current module) and normalise it.

Fields of ComputeToplevel

compute_mode: ComputeModecode: String

LoadHighlightingInfo

loads syntax highlighting information for the module in path, and asks Emacs to apply highlighting info from this file.

If the module does not exist, or its module name is malformed or cannot be determined, or the module has not already been visited, or the cached info is out of date, then no highlighting information is printed.

This command is used to load syntax highlighting information when a new file is opened, and it would probably be annoying if jumping to the definition of an identifier reset the proof state, so this command tries not to do that. One result of this is that the command uses the current include directories, whatever they happen to be.

Fields of LoadHighlightingInfo

path: String

TokenHighlighting

Tells Agda to compute token-based highlighting information for the file.

This command works even if the file's module name does not match its location in the file system, or if the file is not scope-correct. Furthermore no file names are put in the generated output. Thus it is fine to put source code into a temporary file before calling this command. However, the file extension should be correct.

If the second argument is 'Remove', then the (presumably temporary) file is removed after it has been read.

Fields of TokenHighlighting

path: Stringremove: Remove

Highlight(GoalInput)

Tells Agda to compute highlighting information for the expression just spliced into an interaction point.

ShowImplicitArgs(bool)

Tells Agda whether or not to show implicit arguments.

ToggleImplicitArgs

Toggle display of implicit arguments.

Give

If the range is 'noRange', then the string comes from the minibuffer rather than the goal.

Fields of Give

force: UseForceinput: GoalInput

Refine(GoalInput)

Intro

Fields of Intro

dunno: boolinput: GoalInput

RefineOrIntro

Fields of RefineOrIntro

dunno: boolinput: GoalInput

Context(InputWithRewrite)

HelperFunction(InputWithRewrite)

Infer(InputWithRewrite)

GoalType(InputWithRewrite)

ElaborateGive(InputWithRewrite)

Grabs the current goal's type and checks the expression in the hole against it. Returns the elaborated term.

GoalTypeContext(InputWithRewrite)

Displays the current goal and context.

GoalTypeContextInfer(InputWithRewrite)

Displays the current goal and context and infers the type of an expression.

GoalTypeContextCheck(InputWithRewrite)

Grabs the current goal's type and checks the expression in the hole against it

ShowModuleContents(InputWithRewrite)

Shows all the top-level names in the given module, along with their types. Uses the scope of the given goal.

MakeCase(GoalInput)

Compute

Fields of Compute

compute_mode: ComputeModeinput: GoalInput

WhyInScope(GoalInput)

WhyInScopeToplevel(String)

ShowVersion

Displays version of the running Agda

Abort

Abort the current computation. Does nothing if no computation is in progress.

Methods

impl Cmd

pub fn load_simple(path: String) -> Self

pub fn goal_type(input: GoalInput) -> Self

Produces CurrentGoal.

pub fn context(input: GoalInput) -> Self

pub fn split(input: GoalInput) -> Self

pub fn search_module(search: String) -> Self

pub fn infer(input: GoalInput) -> Self

Produces InferredType.

pub fn give(input: GoalInput) -> Self

Trait Implementations

impl Clone for Cmd

fn clone(&self) -> Cmd

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Display for Cmd

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

Formats the value using the given formatter.

impl Debug for Cmd

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

Formats the value using the given formatter.