Module WpReport

module WpReport: sig .. end
start chapter stats

Export Statistics.

Patterns for formatting:

Patterns in fct: Patterns in main: 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 = {
   main : stats;
   prover : (VCS.prover, stats) Hashtbl.t;
}
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 = {
   dstats : pstats;
   dcoverage : coverage;
   mutable dmap : pstats Property.Map.t;
}
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
type t = WpReport.entry 
val compare : WpReport.entry -> WpReport.entry -> int
end)
type fcstat = {
   global : pstats;
   gcoverage : coverage;
   mutable dsmap : dstats Smap.t;
}
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 = {
   fcstat : fcstat;
   chapters : (string * (entry * dstats) list) list;
}
val start_stat4chap : fcstat -> istat option
start chapter stats
val next_stat4chap : istat -> istat option
next chapters stats
type cistat = {
   cfcstat : fcstat;
   chapter : string;
   sections : (entry * dstats) list;
}
val start_stat4sect : istat -> cistat option
start section stats of a chapter
val next_stat4sect : cistat -> cistat option
next section stats
type sistat = {
   sfcstat : fcstat;
   schapter : string;
   section : entry * dstats;
   properties : (Property.t * pstats) list;
}
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