module Proof: sig
.. end
Proof Script Database
val scriptbase : (String.t, String.t list * string) Hashtbl.t
val scriptfile : Wp_parameters.Script.t option Pervasives.ref
val needback : bool Pervasives.ref
val needsave : bool Pervasives.ref
val needwarn : bool Pervasives.ref
val clear : unit -> unit
val sanitize : string -> bool
val register_script : String.t -> String.t list -> string -> unit
val delete_script : String.t -> unit
val is_empty : string -> bool
val parse_coqproof : string -> string option
parse_coqproof f
parses a coq-file f
and fetch the first proof.
val collect_scripts : Script.input -> unit
val parse_scripts : string -> unit
parse_scripts f
parses all scripts from file f
and put them in the database.
val dump_scripts : string -> unit
dump_scripts f
saves all scripts from the database into file f
.
val choose : int -> string
val savescripts : unit -> unit
If necessary, dump the scripts database into the file
specified by -wp-script f
.
val loadscripts : unit -> unit
Load scripts from -wp-script f
. Automatically invoked by find_xxx
unless
loadscripts
flags is unset.
val find_script_for_goal : String.t -> string option
Retrieve script file for one specific goal.
The file specified by -wp-script f
is loaded if necessary.
val update_hints_for_goal : String.t -> String.t list -> unit
Update the hints for one specific goal. The script file will be saved if hints
are different.
val matches : int -> String.t list -> String.t list -> int
val filter : String.t list -> String.t list -> String.t list
val most_suitable : int * 'a * 'b -> int * 'c * 'd -> int
val find_script_with_hints : String.t list -> String.t list -> (int * String.t * string) list
Retrieve matchable script files for w.r.t provided required and hints keywords.
Most suitable scripts comes first, with format (n,g,p)
where p
is a script
matching n
hints from possibly deprecated goal g
.
val add_script : String.t -> String.t list -> string -> unit
new_script goal keys proof
registers the script proof
for goal goal
and keywords keys
val script_for : pid:WpPropId.prop_id -> gid:String.t -> string option
val head : int -> 'a list -> 'a list
val hints_for : pid:WpPropId.prop_id -> (string * string) list
val script_for_ide : pid:WpPropId.prop_id -> gid:String.t -> string