package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a
doc/lambdapi.handle/Handle/Command/index.html
Module Handle.Command
Source
Handling of commands.
too_long
indicates the duration after which a warning should be given to indicate commands that take too long to execute.
Type alias for a function that compiles a Lambdapi module.
type proof_data = {
pdata_sym_pos : Common.Pos.popt;
(*Position of the declared symbol.
*)pdata_state : Proof.proof_state;
(*Proof state.
*)pdata_proof : Parsing.Syntax.p_proof;
(*Proof script.
*)pdata_finalize : Core.Sig_state.sig_state -> Proof.proof_state -> Core.Sig_state.sig_state;
(*Finalizer.
*)pdata_end_pos : Common.Pos.popt;
(*Position of the proof's terminator.
*)pdata_prv : bool;
(*
*)true
iff private symbols are allowed.
}
Representation of a yet unchecked proof. The structure is initialized when the proof mode is entered, and its finalizer is called when the proof mode is exited (i.e., when a terminator like “end” is used).
Representation of a command output.
val get_proof_data :
compiler ->
Core.Sig_state.sig_state ->
Parsing.Syntax.p_command ->
cmd_output
get_proof_data compile ss cmd
tries to handle the command cmd
with ss
as the signature state and compile
as the main compilation function processing lambdapi modules (it is passed as argument to avoid cyclic dependencies). On success, an updated signature state is returned. When cmd
leads to entering the proof mode, a proof_data
is also returned. This structure contains the list of the tactics to be executed, as well as the initial state of the proof. The checking of the proof is then handled separately. Note that Fatal
is raised in case of an error.
val handle :
compiler ->
Core.Sig_state.sig_state ->
Parsing.Syntax.p_command ->
Core.Sig_state.sig_state
handle compile_mod ss cmd
retrieves proof data from cmd
(with get_proof_data
) and handles proofs using functions from Tactic
The function compile_mod
is used to compile required modules recursively.