lambdapi 2.2.0 · OCaml Package

Interface to LSP.

module Command : sig ... end

Abstract representation of a command (top-level item).

val rangemap : Command.t list -> Core.Term.qident Lplib.RangeMap.t

module Tactic : sig ... end

Abstract representation of a tactic (proof item).

module ProofTree : sig ... end

Abstract representation of a proof.

type state

Representation of the state when at the toplevel.

type proof_state

Representation of the state when in a proof.

exception Parse_error of Common.Pos.pos * string

Exception raised by parse_text.

val parse_text : state -> fname:string -> string -> Command.t list * state

parse_text st ~fname contents runs the parser on the string contents as if it were a file named fname. The action takes place in the state st, and an updated state is returned. The function may raise Parse_error.

type conclusion =

| Typ of string * string
(*
Metavariable name and type.
*)
| Unif of string * string
(*
LHS and RHS of the unification goal.
*)

A goal is given by a list of assumptions and a conclusion. Each assumption has a name and a type.

type goal = (string * string) list * conclusion

val current_goals : proof_state -> goal list

current_goals s returns the list of open goals for proof state s.

type command_result =

| Cmd_OK of state * string option
(*
Command is done.
*)
| Cmd_Proof of proof_state * ProofTree.t * Common.Pos.popt * Common.Pos.popt
(*
Enter proof mode (positions are for statement and qed).
*)
| Cmd_Error of Common.Pos.popt option * string
(*
Error report.
*)

Result type of the handle_command function.

type tactic_result =

| Tac_OK of proof_state * string option
| Tac_Error of Common.Pos.popt option * string

Result type of the handle_tactic function.

val initial_state : string -> state

initial_state fname gives an initial state for working with the (source) file fname. The resulting state can be used by handle_command.

val handle_command : state -> Command.t -> command_result

handle_command st cmd evaluates the command cmd in state st, giving one of three possible results: the command is fully handled (corresponding to the Cmd_OK constructor, the command starts a proof (corresponding to the Cmd_Proof constructor), or the command fails (corresponding to the Cmd_Error constuctor).

val handle_tactic : proof_state -> Tactic.t -> int -> tactic_result

handle_tactic ps tac n evaluates the tactic tac with n subproofs in proof state ps, returning a new proof state (with Tac_OK) or an error (with Tac_Error).

val end_proof : proof_state -> command_result

end_proof st finalises the proof which state is st, returning a result at the command level for the whole theorem. This function should be called when all the tactics have been handled with handle_tactic. Note that the value returned by this function cannot be Cmd_Proof.

val get_symbols : state -> Core.Term.sym Lplib.Extra.StrMap.t

get_symbols st returns all the symbols defined in the signature at state st. This can be used for displaying the type of symbols.

val set_initial_time : unit -> unit

set_initial_time () records the current imperative state as the rollback "time" for the initial_state function. This is only useful to initialise or reinitialise the pure interface.

package lambdapi