#
8dec49fd |
|
21-Jan-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update to patriciaLib code. Following these updates, most conversions are now faster. ** Note that PTREE_TRANSFORM_CONV, PTREE_EVERY_LEAF_CONV and PTREE_EXISTS_LEAF_CONV now take a conversion as an extra argument. ** The reference is_ptree_term_size_limit has been removed. Instead, there are now two functions: Define_mk_ptree and Define_mk_ptree_with_is_ptree. The latter returns an IS_PTREE theorem for the new constant. In this case the IS_PTREE theorem is proven in a more efficient manner, however it can still be time consuming, e.g. on a fast machine it takes 3 minutes to prove for a tree with around 49 thousand elements. Smaller trees are more manageable, e.g. 1.6s for a tree with a thousand elements.
|
#
8305d6d4 |
|
29-Aug-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A Patricia tree implementation of finite maps, with datatypes ``: 'a pree`` and ``: ('a, 'b) word_ptree``. These provide support for finite maps num |-> 'a 'a word |-> 'b string |-> 'a For example: - load "patriciaLib"; - EVAL ``(Empty |+ (1, 1) |+ (2,2)) ' 1``; > val it = |- (<{}> |+ (1,1) |+ (2,2)) ' 1 = SOME 1 : thm There is also support for representing sets i.e. num set, 'a word set and string set. For example: - load "patricia_castsLib"; - EVAL ``32w:word32 IN_PTREEw +{16w; 12w; 32w; 8w}+``; > val it = |- 32w IN_PTREEw +{16w; 12w; 32w; 8w}+ = T : thm - EVAL ``KEYSs -{"world"; "hello"}-``; > val it = |- KEYSs -{"world"; "hello"}- = ["hello"; "world"] : thm - EVAL ``NUMSET_OF_PTREE <{2; 4; 6; 2}>``; > val it = |- NUMSET_OF_PTREE <{2; 4; 6; 2}> = {6; 2; 4} : thm It is also possible to work with large trees by constructing them in ML. For example: - val tree = patriciaLib.ptree_of_ints (2::l); /* very long list of ints */ - Globals.max_print_depth := 10; /* tree is too big to print in full */ - val tree_def = patriciaLib.Define_mk_ptree "tree" tree; - EVAL ``2 IN_PTREE tree``; > val it = |- 2 IN_PTREE tree = T : thm - EVAL ``tree \\ 2``; > val it = |- tree \\ 2 = tree \\ 2 : thm - EVAL ``2 IN_PTREE (tree \\ 2)``; > val it = |- 2 IN_PTREE tree \\ 2 = F : thm All of this happens fairly quickly, even when there are a few thousand elements in the tree -- that is, when adding tree_def to the compset would make things grind to a halt.
|