1signature Rsyntax =
2sig
3  type hol_type = Type.hol_type
4  type term = Term.term
5  type thm = Thm.thm
6
7  val mk_type       : {Args:hol_type list, Tyop:string} -> hol_type
8  val mk_var        : {Name:string, Ty:hol_type} -> term
9  val mk_primed_var : {Name:string, Ty:hol_type} -> term
10  val mk_const      : {Name:string, Ty:hol_type} -> term
11  val mk_abs        : {Bvar:term, Body:term} -> term
12  val mk_comb       : {Rand:term, Rator:term} -> term
13  val mk_cond       : {cond:term, larm:term, rarm:term} -> term
14  val mk_conj       : {conj1:term, conj2:term} -> term
15  val mk_disj       : {disj1:term, disj2:term} -> term
16  val mk_eq         : {lhs:term, rhs:term} -> term
17  val mk_forall     : {Bvar:term, Body:term} -> term
18  val mk_exists     : {Bvar:term, Body:term} -> term
19  val mk_exists1    : {Bvar:term, Body:term} -> term
20  val mk_select     : {Bvar:term, Body:term} -> term
21  val mk_imp        : {ant:term, conseq:term} -> term
22  val mk_let        : {arg:term, func:term} -> term
23
24  val dest_type     : hol_type -> {Args:hol_type list, Tyop:string}
25  val dest_var      : term -> {Name:string, Ty:hol_type}
26  val dest_const    : term -> {Name:string, Ty:hol_type}
27  val dest_abs      : term -> {Body:term, Bvar:term}
28  val dest_comb     : term -> {Rand:term, Rator:term}
29  val dest_cond     : term -> {cond:term, larm:term, rarm:term}
30  val dest_conj     : term -> {conj1:term, conj2:term}
31  val dest_disj     : term -> {disj1:term, disj2:term}
32  val dest_eq       : term -> {lhs:term, rhs:term}
33  val dest_forall   : term -> {Bvar:term, Body:term}
34  val dest_exists   : term -> {Bvar:term, Body:term}
35  val dest_exists1  : term -> {Bvar:term, Body:term}
36  val dest_select   : term -> {Bvar:term, Body:term}
37  val dest_imp      : term -> {ant:term, conseq:term}
38  val dest_imp_only : term -> {ant:term, conseq:term}
39  val dest_let      : term -> {arg:term, func:term}
40
41  val new_type      : {Arity:int, Name:string} -> unit
42  val new_constant  : {Name:string, Ty:hol_type} -> unit
43  val new_infix     : {Name:string, Prec:int, Ty:hol_type} -> unit
44  val new_binder    : {Name:string, Ty:hol_type} -> unit
45  val new_specification : {name    : string,
46                           sat_thm : thm,
47                           consts  : {const_name : string,
48                                      fixity : Parse.fixity option} list} -> thm
49  datatype lambda
50     = VAR   of {Name:string, Ty:hol_type}
51     | CONST of {Name:string, Thy:string, Ty:hol_type}
52     | COMB  of {Rator:term, Rand:term}
53     | LAMB  of {Bvar:term, Body:term};
54
55  val dest_term : term -> lambda
56end
57