1signature Absyn =
2sig
3  type term = Term.term
4  type pretype = Pretype.pretype
5  type 'a quotation = 'a Portable.quotation
6
7  datatype vstruct = datatype Absyn_dtype.vstruct
8  datatype absyn = datatype Absyn_dtype.absyn
9
10  val locn_of_absyn   : absyn -> locn.locn
11  val locn_of_vstruct : vstruct -> locn.locn
12
13  val traverse : (absyn -> bool) ->
14                 ((absyn -> absyn) -> (absyn -> absyn)) ->
15                 absyn -> absyn
16
17  val to_vstruct : absyn -> vstruct
18
19  val mk_AQ    : term -> absyn
20  val mk_ident : string -> absyn
21  val mk_app   : absyn * absyn -> absyn
22  val mk_lam   : vstruct * absyn -> absyn
23  val mk_typed : absyn * pretype -> absyn
24
25  val mk_eq      : absyn * absyn -> absyn
26  val mk_conj    : absyn * absyn -> absyn
27  val mk_disj    : absyn * absyn -> absyn
28  val mk_imp     : absyn * absyn -> absyn
29  val mk_pair    : absyn * absyn -> absyn
30  val mk_forall  : vstruct * absyn -> absyn
31  val mk_exists  : vstruct * absyn -> absyn
32  val mk_exists1 : vstruct * absyn -> absyn
33  val mk_select  : vstruct * absyn -> absyn
34  val mk_binder  : string -> vstruct * absyn -> absyn
35
36  val dest_AQ      : absyn -> term
37  val dest_ident   : absyn -> string
38  val dest_app     : absyn -> absyn * absyn
39  val dest_lam     : absyn -> vstruct * absyn
40  val dest_typed   : absyn -> absyn * pretype
41  val dest_eq      : absyn -> absyn * absyn
42  val dest_conj    : absyn -> absyn * absyn
43  val dest_disj    : absyn -> absyn * absyn
44  val dest_imp     : absyn -> absyn * absyn
45  val dest_pair    : absyn -> absyn * absyn
46  val dest_forall  : absyn -> vstruct * absyn
47  val dest_exists  : absyn -> vstruct * absyn
48  val dest_exists1 : absyn -> vstruct * absyn
49  val dest_select  : absyn -> vstruct * absyn
50  val dest_binder  : string -> absyn -> vstruct * absyn
51  val dest_binop   : string -> absyn -> absyn * absyn
52
53  val list_mk_app     : absyn * absyn list -> absyn
54  val list_mk_lam     : vstruct list * absyn -> absyn
55  val list_mk_conj    : absyn list -> absyn
56  val list_mk_disj    : absyn list -> absyn
57  val list_mk_imp     : absyn list -> absyn
58  val list_mk_pair    : absyn list -> absyn
59  val list_mk_forall  : vstruct list * absyn -> absyn
60  val list_mk_exists  : vstruct list * absyn -> absyn
61  val list_mk_exists1 : vstruct list * absyn -> absyn
62  val list_mk_select  : vstruct list * absyn -> absyn
63
64  val strip_app     : absyn -> absyn * absyn list
65  val strip_lam     : absyn -> vstruct list * absyn
66  val strip_conj    : absyn -> absyn list
67  val strip_disj    : absyn -> absyn list
68  val strip_imp     : absyn -> absyn list
69  val strip_pair    : absyn -> absyn list
70  val strip_forall  : absyn -> vstruct list * absyn
71  val strip_exists  : absyn -> vstruct list * absyn
72  val strip_exists1 : absyn -> vstruct list * absyn
73  val strip_select  : absyn -> vstruct list * absyn
74
75  val is_ident   : absyn -> bool
76  val is_app     : absyn -> bool
77  val is_lam     : absyn -> bool
78  val is_AQ      : absyn -> bool
79  val is_typed   : absyn -> bool
80  val is_eq      : absyn -> bool
81  val is_conj    : absyn -> bool
82  val is_disj    : absyn -> bool
83  val is_imp     : absyn -> bool
84  val is_pair    : absyn -> bool
85  val is_forall  : absyn -> bool
86  val is_exists  : absyn -> bool
87  val is_exists1 : absyn -> bool
88  val is_select  : absyn -> bool
89end
90