Coverage.ReportSourceFormats and emits coverage results for user-facing output. Provides local (per-state) and global (cross-state) reporting modes, with sentence deduplication and cost-based ordering.
val cleanup_sentences :
'term Utils.Misc.indexset ->
'a ->
('tactic * int * 'term Utils.Misc.indexset) list ->
('tactic * int * 'term Utils.IndexSet.t * 'a) listDeduplicate and filter sentences for a single LR(0) state. Sentences are sorted by cost, and lookaheads already covered by earlier sentences are removed. Only sentences contributing new uncovered lookaheads are retained.
val emit_local :
('lr0, 'term Utils.Misc.indexset) Fix.Indexing.vector ->
('lr0 Fix.Indexing.index -> ('tactic * int * 'term Utils.Misc.indexset) list) ->
('lr0 Fix.Indexing.index * ('tactic * 'term Utils.Misc.indexset) Stdlib.Seq.t)
Stdlib.Seq.tEmit local (per-state) coverage results. For each LR(0) state with uncovered lookaheads, returns a sequence of sentences sorted by cost. States with no remaining goals are omitted.
val emit_global :
('lr0, 'term Utils.Misc.indexset) Fix.Indexing.vector ->
('lr0 Fix.Indexing.index -> ('tactic * int * 'term Utils.Misc.indexset) list) ->
('lr0 Fix.Indexing.index * 'tactic * 'term Utils.Misc.indexset) Stdlib.Seq.tEmit global coverage results using a priority queue. Sentences from all LR(0) states are merged into a single cost-ordered sequence, so the most relevant counterexamples appear first regardless of which state they belong to.
val emit_all :
goals:'goal Fix.Indexing.cardinal ->
graph:('n, 'term) Enum._graph ->
maximals:('n Fix.Indexing.index list * 'term Utils.Misc.indexset) list array ->
globals:('n Fix.Indexing.index list * 'term Utils.Misc.indexset) list array ->
reached:('n Fix.Indexing.index -> 'goal Utils.Misc.indexset) ->
('goal Fix.Indexing.index
* ('n Fix.Indexing.index list * 'term Utils.Misc.indexset) Stdlib.Seq.t)
Stdlib.Seq.t
* ('goal Fix.Indexing.index
* ('n Fix.Indexing.index list * 'term Utils.Misc.indexset) Stdlib.Seq.t)
Stdlib.Seq.tEmit both local and global coverage results. Populates goal-to-sentence mappings from maximal and global prefix arrays, then expands paths by following predecessor links and committing coverage decisions (removing lookaheads already accounted for by earlier sentences). Returns a pair of (local, global) result sequences.