module WpReport: sig
.. end
start chapter stats
Export Statistics.
Patterns for formatting:
"%{cmd:arg}"
or "%cmd:arg"
"%{cmd}"
or "%cmd"
Patterns in
fct
:
"%kf"
or "%kf:name"
the name of the function.
"%kf:<s>"
the stats in format <s>
for the function.
"%<p>:<s>"
the stats in format <s>
for prover <p>
.
Patterns in
main
:
- "%<s>" the global statistics with format
<s>
.
Prover strings are
"wp"
,
"ergo"
,
"coq"
,
"z3"
and
"simplify"
.
Format strings are "100" (percents of valid upon total, default),
"total"
,
"valid"
and
"failed"
for respective number of verification conditions.
Zero is printed as
zero
. Percentages are printed in decimal
"dd.d"
.
val ladder : float array
type
res =
| |
VALID |
| |
UNSUCCESS |
| |
INCONCLUSIVE |
| |
NORESULT |
val result : VCS.result -> res
val best_result : res -> res -> res
type
stats = {
|
mutable valid : int ; |
|
mutable unsuccess : int ; |
|
mutable inconclusive : int ; |
|
mutable total : int ; |
|
mutable steps : int ; |
|
mutable time : float ; |
}
val stats : unit -> stats
val add_stat : res -> int -> float -> stats -> unit
val add_qedstat : float -> stats -> unit
type
pstats = {
}
val pstats : config:config ->
Format.formatter -> pstats -> string -> string -> unit
val get_prover : pstats -> VCS.prover -> stats
val add_results : pstats list -> Wpo.t -> unit
type
coverage = {
|
mutable covered : Property.Set.t ; |
|
mutable proved : Property.Set.t ; |
}
val coverage : unit -> coverage
val add_cover : coverage -> bool -> Property.Set.elt -> unit
type
dstats = {
}
val dstats : unit -> dstats
type
entry =
| |
Global of string |
| |
Axiom of string |
| |
Fun of Kernel_function.t |
val decode_chapter : entry -> string
module Smap: FCMap.Make
(
sig
end
)
type
fcstat = {
}
val get_section : fcstat -> Smap.key -> dstats
val get_property : dstats -> Property.Map.key -> pstats
val add_goal : fcstat -> Wpo.t -> unit
val fcstat : unit -> fcstat
type
istat = {
}
val start_stat4chap : fcstat -> istat option
start chapter stats
val next_stat4chap : istat -> istat option
next chapters stats
type
cistat = {
}
val start_stat4sect : istat -> cistat option
start section stats of a chapter
val next_stat4sect : cistat -> cistat option
next section stats
type
sistat = {
}
val start_stat4prop : cistat -> sistat option
start property stats of a section
val next_stat4prop : sistat -> sistat option
next property stats
val iter_stat : ?first:('a -> unit) ->
?sep:('a -> unit) ->
?last:(unit -> unit) ->
from:'b -> ('b -> 'a option) -> ('a -> 'a option) -> unit
generic iterator
type
config = {
|
mutable status_passed : string ; |
|
mutable status_failed : string ; |
|
mutable status_inconclusive : string ; |
|
mutable status_untried : string ; |
|
mutable global_prefix : string ; |
|
mutable lemma_prefix : string ; |
|
mutable axiomatic_prefix : string ; |
|
mutable function_prefix : string ; |
|
mutable property_prefix : string ; |
|
mutable global_section : string ; |
|
mutable axiomatic_section : string ; |
|
mutable function_section : string ; |
|
mutable console : bool ; |
|
mutable zero : string ; |
}
val pp_zero : config:config -> Format.formatter -> unit
val percent : config:config -> Format.formatter -> int -> int -> unit
val number : config:config -> Format.formatter -> int -> unit
val properties : config:config ->
Format.formatter -> coverage -> string -> unit
val stat : config:config ->
Format.formatter -> stats -> string -> unit
val pstats : config:config ->
Format.formatter -> pstats -> string -> string -> unit
val pcstats : config:config ->
Format.formatter ->
pstats * coverage -> string -> string -> unit
val env_toplevel : config:config ->
fcstat -> Format.formatter -> string -> string -> unit
val env_chapter : string -> Format.formatter -> string -> string -> unit
val env_section : config:config ->
name:string ->
cistat -> Format.formatter -> string -> string -> unit
val env_property : config:config ->
name:string ->
sistat -> Format.formatter -> string -> string -> unit
val print_property : sistat ->
config:config ->
name:string -> prop:string -> Format.formatter -> unit
val print_section : cistat ->
config:config ->
name:string -> sect:string -> prop:string -> Format.formatter -> unit
val print_chapter : istat ->
config:config ->
chap:string ->
sect:string ->
glob:string ->
axio:string -> func:string -> prop:string -> Format.formatter -> unit
val print : fcstat ->
config:config ->
head:string ->
tail:string ->
chap:string ->
sect:string ->
glob:string ->
axio:string -> func:string -> prop:string -> Format.formatter -> unit
type
section =
| |
END |
| |
HEAD |
| |
TAIL |
| |
CHAPTER |
| |
SECTION |
| |
GLOB_SECTION |
| |
AXIO_SECTION |
| |
FUNC_SECTION |
| |
PROPERTY |
val export : fcstat -> string -> unit