1signature HolKernelDoc =
2sig
3  (* This signature file is for documentation purposes only *)
4
5  type term = Term.term
6  type hol_type = Type.hol_type
7  type 'a set = 'a HOLset.set
8  type ('a,'b) subst = ('a,'b) Lib.subst
9
10  val gen_find_term: (term list * term -> 'a option) -> term -> 'a option
11  val gen_find_terms: (term list * term -> 'a option) -> term -> 'a list
12  val bvk_find_term:
13     (term list * term -> bool) -> (term -> 'a) -> term -> 'a option
14  val dest_binder: term -> exn -> term -> term * term
15  val dest_binop: term -> exn -> term -> term * term
16  val dest_monop: term -> exn -> term -> term
17  val dest_quadop: term -> exn -> term -> term * term * term * term
18  val dest_triop: term -> exn -> term -> term * term * term
19  val disch: term * term list -> term list
20  val find_maximal_terms: (term -> bool) -> term -> term set
21  val find_term: (term -> bool) -> term -> term
22  val find_terms: (term -> bool) -> term -> term list
23  val ho_match_term0:
24     hol_type list -> term set -> term -> term ->
25     {redex: term, residue: int} list *
26     {redex: term, residue: term} list *
27     ((hol_type, hol_type) subst * hol_type list)
28  val ho_match_term:
29     hol_type list -> term set -> term -> term ->
30     {redex: term, residue: term} list * (hol_type, hol_type) subst
31  val list_mk_fun: hol_type list * hol_type -> hol_type
32  val list_mk_icomb: term -> term list -> term
33  val list_mk_lbinop: ('a -> 'a -> 'a) -> 'a list -> 'a
34  val list_mk_rbinop: ('a -> 'a -> 'a) -> 'a list -> 'a
35  val lspine_binop: ('a -> ('a * 'a) option) -> 'a -> 'a list
36  val mk_binder: term -> string -> term * term -> term
37  val mk_binop: term -> term * term -> term
38  val mk_monop: term -> term -> term
39  val mk_quadop: term -> term * term * term * term -> term
40  val mk_triop: term -> term * term * term -> term
41  val sdest_binder: string * string -> exn -> term -> term * term
42  val sdest_binop: string * string -> exn -> term -> term * term
43  val sdest_monop: string * string -> exn -> term -> term
44  val spine_binop: ('a -> ('a * 'a) option) -> 'a -> 'a list
45  val strip_binop: ('a -> ('a * 'a) option) -> 'a -> 'a list
46  val strip_comb: term -> term * term list
47  val strip_fun: hol_type -> hol_type list * hol_type
48  val strip_gen_right_opt: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
49  val strip_gen_right: ('a -> 'a * 'b) -> 'a -> 'a * 'b list
50  val strip_gen_left_opt: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
51  val strip_gen_left: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
52  val sort_vars: string list -> term list -> term list
53  val subst_occs:
54     int list list -> {redex: term, residue: term} list -> term -> term
55  val syntax_fns:
56     {n: int, make: term -> 'a -> term, dest: term -> exn -> term -> 'b} ->
57     string -> string -> term * ('a -> term) * (term -> 'b) * (term -> bool)
58  val syntax_fns1:
59     string -> string -> term * (term -> term) * (term -> term) * (term -> bool)
60  val syntax_fns2:
61     string -> string ->
62     term * (term * term -> term) * (term -> term * term) * (term -> bool)
63  val syntax_fns3:
64     string -> string ->
65     term * (term * term * term -> term) * (term -> term * term * term) * (term -> bool)
66  val syntax_fns4:
67     string -> string ->
68     term * (term * term * term * term -> term) * (term -> term * term * term * term) * (term -> bool)
69  val term_size: term -> int
70
71end
72