SharedForest.SharedForestThis type is the type of addresses of forests. It is a list of (position in the forest,position as a child).
type relative_path = int * addressThis is the type of relative path from one forest to another one. The first argument is the number of steps to move up, then second argument is the address to reach from this point.
val diff : address -> address -> relative_pathdiff add add' returns the relative path to go from the forest (subtree) wich occurs at address add to the forest (subtree) wich occurs at address add'.
val pp_path : Stdlib.Format.formatter -> relative_path -> unitpp_path fmt p pretty prints the path p on the formatter fmt.
val pp_address : Stdlib.Format.formatter -> address -> unitpp_path fmt add pretty prints the address add on the formatter fmt.
type weight = Weight.Weight_as_Depth_and_Size.wThis type is the type for weights of trees. It is used to enumerate trees in the resumptions in the order specified by W
val pp_weight : Stdlib.Format.formatter -> weight -> unitpp_path fmt w pretty prints the weight w on the formatter fmt.
type !'a forest = 'a forest_tree listand !'a forest_tree = 'a Make(Weight.Weight_as_Depth_and_Size).forest_tree = | Node of 'a * 'a child listand !'a child = 'a Make(Weight.Weight_as_Depth_and_Size).child = | Forest of 'a forest| Link_to of relative_pathThe type of the forests, made of the type of their nodes and the type of their children
*)type !'a childList_context =
'a Make(Weight.Weight_as_Depth_and_Size).childList_context =
{siblings : 'a child ListContext.focused_list;parent_label : 'a;focus : 'a child;}The type of the context for child lists (cannot be straightforwadly list context because elements can be either forests or links to other places in the shared forest
type !'a forest_context_info =
'a Make(Weight.Weight_as_Depth_and_Size).forest_context_info =
{label : 'a;children : 'a child ListContext.focused_list;alternatives : 'a forest_tree ListContext.focused_list;alt_num : int;context : 'a forest_context;suspended_computation : (('a forest_context * 'a forest_tree)
* 'a childList_context)
option;address : address;}and !'a forest_context =
'a Make(Weight.Weight_as_Depth_and_Size).forest_context =
| Top of 'a forest_tree ListContext.focused_list
* int
* (('a forest_context * 'a forest_tree) * 'a childList_context) option| Zip of 'a forest_context_infoThe type for shared forest contexts. Using a record to better distinguish the different components
*)module Resumptions : sig ... endA resumption store module for the weighting scheme being used
val init :
alt_max:int ->
(Stdlib.Format.formatter -> 'a -> unit) ->
'a forest_tree list ->
'a Resumptions.resumptionsinit ~alt_max ppf forest builds the resumptions with a focused forest focusing on each of the tree of forest. 10^alt_max is the max number of delayed computations before moving to non-regular sorting. ppf is a pretty printer for 'a type values.
val resume :
'a Resumptions.resumptions ->
('a TreeContext.Tree.tree * Weight.Weight_as_Depth_and_Size.w) option
* 'a Resumptions.resumptionsresume resumptions returns a pair (Some (t,n),resumptions') where t of size n is extracted from resumptions, the latter being updated with possible alternatives met in building t to produce resumptions'. It returns (None,[]) if no tree can be extracted
val pp_trees :
(Stdlib.Format.formatter -> 'a -> unit) ->
Stdlib.Format.formatter ->
'a Resumptions.resumptions ->
unitpp_tree pp fmt r pretty prints all the trees by generated by the resumptions on the formatter fmt using the pretty printer for tree nodes pp
val pp_forest :
(Stdlib.Format.formatter -> 'a -> unit) ->
Stdlib.Format.formatter ->
'a forest ->
unitpp_tree pp fmt f pretty prints the forest f (with actual link-to node) on the formatter fmt using the pretty printer for tree nodes pp