1signature patriciaLib =
2sig
3
4  include Abbrev
5
6  type term_ptree
7  type num = Arbnum.num
8
9  val dest_ptree : term -> term_ptree
10  val mk_ptree   : term_ptree -> term
11  val is_ptree   : term -> bool
12
13  val Define_mk_ptree : string -> term_ptree -> thm
14  val Define_mk_ptree_with_is_ptree : string -> term_ptree -> thm * thm
15
16  val empty         : term_ptree
17  val peek          : term_ptree -> num -> term option
18  val add           : term_ptree -> (num * term) -> term_ptree
19  val add_list      : term_ptree -> (num * term) list -> term_ptree
20  val remove        : term_ptree -> num -> term_ptree
21  val traverse      : term_ptree -> num list
22  val keys          : term_ptree -> num list
23  val transform     : (term -> term) -> term_ptree -> term_ptree
24  val size          : term_ptree -> int
25  val depth         : term_ptree -> int
26  val every_leaf    : (num -> term -> bool) -> term_ptree -> bool
27  val tabulate      : int * (int -> num * term) -> term_ptree
28  val in_ptree      : num * term_ptree -> bool
29  val insert_ptree  : num * term_ptree -> term_ptree
30  val ptree_of_list : (num * term) list -> term_ptree
31  val list_of_ptree : term_ptree -> (num * term) list
32  val ptree_of_nums : num list -> term_ptree
33
34  val int_peek          : term_ptree -> int -> term option
35  val int_add           : term_ptree -> (int * term) -> term_ptree
36  val int_add_list      : term_ptree -> (int * term) list -> term_ptree
37  val int_remove        : term_ptree -> int -> term_ptree
38  val int_in_ptree      : int * term_ptree -> bool
39  val int_insert_ptree  : int * term_ptree -> term_ptree
40  val int_ptree_of_list : (int * term) list -> term_ptree
41  val ptree_of_ints     : int list -> term_ptree
42
43  val string_peek          : term_ptree -> string -> term option
44  val string_add           : term_ptree -> (string * term) -> term_ptree
45  val string_add_list      : term_ptree -> (string * term) list -> term_ptree
46  val string_remove        : term_ptree -> string -> term_ptree
47  val string_in_ptree      : string * term_ptree -> bool
48  val string_insert_ptree  : string * term_ptree -> term_ptree
49  val string_ptree_of_list : (string * term) list -> term_ptree
50  val ptree_of_strings     : string list -> term_ptree
51
52  val custom_pp_term_ptree :
53    bool PP.pprinter -> (num * term) PP.pprinter -> int ->
54    term_ptree PP.pprinter
55
56  val pp_term_ptree : term_ptree PP.pprinter
57
58  val PTREE_PEEK_CONV         : conv
59  val PTREE_ADD_CONV          : conv
60  val PTREE_REMOVE_CONV       : conv
61  val PTREE_SIZE_CONV         : conv
62  val PTREE_DEPTH_CONV        : conv
63  val PTREE_TRANSFORM_CONV    : conv -> conv
64  val PTREE_EVERY_LEAF_CONV   : conv -> conv
65  val PTREE_EXISTS_LEAF_CONV  : conv -> conv
66  val PTREE_IN_PTREE_CONV     : conv
67  val PTREE_IS_PTREE_CONV     : conv
68  val PTREE_INSERT_PTREE_CONV : conv
69  val PTREE_OF_NUMSET_CONV    : conv
70
71  val PTREE_CONV              : conv
72  val PTREE_DEFN_CONV         : conv
73
74  val ptree_new_defn_depth : int ref
75
76  val add_ptree_compset : computeLib.compset -> unit
77  val ptree_compset     : unit -> computeLib.compset
78
79end
80