Andor (p.lrgrep.0.9.doc.kernel.Kernel.Coverage.Andor)

Sourcetype ('g, 'lrc, 'n) node = {

lrc : 'lrc Fix.Indexing.index;
rpos : 'g Redpos.t Fix.Indexing.Opt.n Fix.Indexing.index;
active : 'g Info.terminal Utils.Misc.indexset;
mutable successors : ('g Info.terminal Utils.Misc.indexset * 'n Fix.Indexing.index) array;

}

Non-deterministic AND-OR graph for coverability analysis. OR nodes represent choice points where multiple reductions may fire. AND nodes represent deterministic stack consumption during a reduction.

Sourcetype ('g, 'lrc, 'n) _graph = {

initials : ('lrc, 'g Info.terminal Utils.Misc.indexset * 'n Fix.Indexing.index) Utils.Misc.indexmap;
nodes : ('n, ('g, 'lrc, 'n) node) Fix.Indexing.vector;

}

Sourcetype ('g, 'lrc) graph =

| Graph : ('g, 'lrc, 'n) _graph -> ('g, 'lrc) graph

Sourceval is_or_node : 'a Redpos.table -> ('a, 'b, 'c) node -> bool

Returns true when the node is an OR node, i.e., at a reduction choice point: either between reductions (rpos = None) or at the start of a reduction (rpos at position zero).

Source

val top_state : 
  'a Kernel__Info.grammar ->
  ('a, 'b) Automata.stacks ->
  'a Redpos.table ->
  ('a, 'b, 'c) node ->
  'a Info.lr1 Fix.Indexing.index

Returns the top LR(1) state on the stack for a given node. For OR nodes (rpos = None), this is the label of the LRC state. For AND nodes mid-reduction on a nonterminal, this is the goto target from the LRC's label state.

Source

val make : 
  'g Info.grammar ->
  ('g Info.lr1, 'g Redgraph.reduction_closure) Fix.Indexing.vector ->
  ('g, 'lrc) Automata.stacks ->
  'g Redpos.table ->
  ('g, 'lrc) graph

Build the AND-OR graph by fixpoint iteration. Starting from each LRC state with all regular terminals as active lookahead, the graph explores reductions and stack pops. OR nodes branch into all applicable reductions; AND nodes chain through right-to-left consumption of production RHS symbols.