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