lambdapi 2.0.0 · OCaml Package

Calling a prover using Why3.

val log_why3 : 'a Lplib.Base.outfmt -> 'a

val default_prover : string Timed.ref

default_prover contains the name of the current prover. Note that it can be changed by using the "set prover <string>" command.

val timeout : int Timed.ref

timeout is the current time limit (in seconds) for a Why3 prover to find a proof. It can be changed with "set prover <int>".

val why3_config : Why3.Whyconf.config

why3_config is the Why3 configuration read from the configuration file ("~/.why3.conf" usually). For more information, visit the Why3 documentation at http://why3.lri.fr/api/Whyconf.html.

val why3_main : Why3.Whyconf.main

why3_main is the main section of the Why3 configuration.

val why3_env : Why3.Env.env

why3_env is the initialized Why3 environment.

type config = {

symb_P : Core.Term.sym;
(*
Encoding of propositions.
*)
symb_T : Core.Term.sym;
(*
Encoding of types.
*)
symb_or : Core.Term.sym;
(*
Disjunction(∨) symbol.
*)
symb_and : Core.Term.sym;
(*
Conjunction(∧) symbol.
*)
symb_imp : Core.Term.sym;
(*
Implication(⇒) symbol.
*)
symb_bot : Core.Term.sym;
(*
Bot(⊥) symbol.
*)
symb_top : Core.Term.sym;
(*
Top(⊤) symbol.
*)
symb_not : Core.Term.sym;
(*
Not(¬) symbol.
*)

}

Builtin configuration for propositional logic.

val get_config : Core.Sig_state.t -> Common.Pos.popt -> config

get_config ss pos build the configuration using ss.

type cnst_table = (Core.Term.term * Why3.Term.lsymbol) list

A map from lambdapi terms to Why3 constants.

val new_axiom_name : unit -> string

new_axiom_name () generates a fresh axiom name.

val translate_term : 
  config ->
  cnst_table ->
  Core.Term.term ->
  (cnst_table * Why3.Term.term) option

translate_term cfg tbl t translates the given lambdapi term t into the correspondig Why3 term, using the configuration cfg and constants in the association list tbl.

val encode : 
  Core.Sig_state.t ->
  Common.Pos.popt ->
  Core.Env.env ->
  Core.Term.term ->
  Why3.Task.task

encode ss pos hs g translates the hypotheses hs and the goal g into Why3 terms, to construct a Why3 task.

val run_task : Why3.Task.task -> Common.Pos.popt -> string -> bool

run_task tsk pos prover_name Run the task tsk with the specified prover named prover_name and return the answer of the prover.

val handle : 
  Core.Sig_state.t ->
  Common.Pos.popt ->
  string option ->
  Proof.goal_typ ->
  Core.Term.term

handle ss pos ps prover_name g runs the Why3 prover corresponding to the name prover_name (if given or a default one otherwise) on the goal g. If the prover succeeded to prove the goal, then this is reflected by a new axiom that is added to signature ss.

package lambdapi