----------------------------------------------------------------------
PTREE_CONV                                               (patriciaLib)
----------------------------------------------------------------------
PTREE_CONV : conv

SYNOPSIS
Conversion for evaluating Patricia tree operations.

DESCRIBE
The conversion {PTREE_CONV} evaluates Patricia tree operations such as {ADD}, {ADD_LIST}, {REMOVE}, {SIZE}, {PEEK} and {FIND}.  These evaluations work for constants that are defined using {Define_mk_ptree}.  When adding to, or removing from, a Patricia tree a new contant will be defined after {patriciaLib.ptree_new_defn_depth} operations.  By default {ptree_new_defn_depth} is {~1}, which means that new constants are never defined.

EXAMPLE
Consider the following Patricia tree:

val ptree = Define_mk_ptree "ptree" (int_ptree_of_list [(1,``1``), (2, ``2``)]);
<<HOL message: Saved IS_PTREE theorem for new constant "ptree">>
val ptree = |- ptree = Branch 0 0 (Leaf 1 1) (Leaf 2 2): thm


Adding a list of updates expands into applications of {ADD}:

> real_time PTREE_CONV ``ptree |++ [(3,3); (4,4); (5,5); (6,6); (7,7)]``;
realtime: 0.000s
val it =
   |- ptree |++ [(3,3); (4,4); (5,5); (6,6); (7,7)] =
   ptree |+ (3,3) |+ (4,4) |+ (5,5) |+ (6,6) |+ (7,7):
   thm


However, setting {ptree_new_defn_depth} will cause new definitions to be made:

> ptree_new_defn_depth := 2;
val it = (): unit
> real_time PTREE_CONV ``ptree |++ [(3,3); (4,4); (5,5); (6,6); (7,7)]``;
<<HOL message: Defined new ptree: ptree1>>
<<HOL message: Defined new ptree: ptree2>>
realtime: 0.006s
val it = |- ptree |++ [(3,3); (4,4); (5,5); (6,6); (7,7)] = ptree2 |+ (7,7):
   thm


New definitions will also be made when removing elements:

> real_time PTREE_CONV ``ptree2 \\ 6 \\ 5``;
<<HOL message: Defined new ptree: ptree3>>
realtime: 0.001s
val it = |- ptree2 \\ 6 \\ 5 = ptree3: thm


Here, the conversion is not smart enough to work out that {ptree3} is the same as {ptree1}.

> (DEPTH_CONV PTREE_DEFN_CONV THENC EVAL) ``ptree1 = ptree3``;
val it = |- (ptree1 = ptree3) <=> T: thm


Look-up behaves as expected:

> real_time PTREE_CONV ``ptree1 ' 2``;
realtime: 0.001s
val it = |- ptree1 ' 2 = SOME 2: thm
> real_time PTREE_CONV ``ptree1 ' 5``;
realtime: 0.001s
val it = |- ptree1 ' 5 = NONE: thm


COMMENTS
The conversion {PTREE_CONV} is automatically added to the standard {compset}.  Thus, {EVAL} will have the same behaviour when {patriciaLib} is loaded.

Run-times should be respectable when working with large Patricia trees.  However, this is predicated on the assumption that relatively small numbers of updates are made following an initial application of {Define_mk_ptree}.  In this sense, the Patricia tree development is best suited to situations where users require fast "read-only" look-up; where the work of building the look-up tree can be performed outside of the logic (i.e. in ML).

SEEALSO
patriciaLib.Define_mk_ptree, patriciaLib.PTREE_DEFN_CONV.

----------------------------------------------------------------------