Module Handle.Why3_tacticSource

Calling a prover using Why3.

Sourceval log_why3 : 'a Lplib.Base.outfmt -> 'a
Sourceval 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.

Sourceval 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>".

Sourceval 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.

Sourceval why3_main : Why3.Whyconf.main

why3_main is the main section of the Why3 configuration.

Sourceval why3_env : Why3.Env.env

why3_env is the initialized Why3 environment.

Sourcetype config = {
  1. symb_P : Core.Term.sym;
    (*

    Encoding of propositions.

    *)
  2. symb_T : Core.Term.sym;
    (*

    Encoding of types.

    *)
  3. symb_or : Core.Term.sym;
    (*

    Disjunction(∨) symbol.

    *)
  4. symb_and : Core.Term.sym;
    (*

    Conjunction(∧) symbol.

    *)
  5. symb_imp : Core.Term.sym;
    (*

    Implication(⇒) symbol.

    *)
  6. symb_bot : Core.Term.sym;
    (*

    Bot(⊥) symbol.

    *)
  7. symb_top : Core.Term.sym;
    (*

    Top(⊤) symbol.

    *)
  8. symb_not : Core.Term.sym;
    (*

    Not(¬) symbol.

    *)
}

Builtin configuration for propositional logic.

get_config ss pos build the configuration using ss.

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

A map from lambdapi terms to Why3 constants.

Sourceval new_axiom_name : unit -> string

new_axiom_name () generates a fresh axiom name.

Sourceval 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.

Sourceval 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.

Sourceval 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.

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.