#
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.
|