Module Weight.Weight_as_DepthSource

The type of weight

pp fmt w pretty prints the weight w on the formatter fmt.

an initial value for the weight (somehow a unit of the ring of weights)

is better w1 w2 returns true if w1 is strictly better (in the sense implemented by the module) than w2

is better w1 w2 returns true if w1 = w2

up w v returns the new weight computed from w and from v (the label of the current node, before moving up in the tree).

down w v returns the new weight computed from w and from v (the label of the current node, before moving down in the tree).

right w v returns the new weight computed from w and from v (the label parent node of the current node.

This module implements a map from weights to lists of computational states of same weight.