1signature Parse_support =
2sig
3  type pretype = Pretype.pretype
4  type preterm = Preterm.preterm
5  type term    = Term.term
6
7  type env            = Parse_supportENV.env
8  type preterm_in_env = preterm Parse_supportENV.PSM
9  type bvar_in_env    = env -> (preterm -> preterm) * env
10  type overload_info  = term_grammar.overload_info
11
12  val gen_overloaded_const  : overload_info -> locn.locn -> string ->
13                              preterm_in_env
14  val make_preterm          : preterm_in_env -> preterm Pretype.in_env
15  val make_aq               : locn.locn -> term -> preterm_in_env
16  val make_binding_occ      : locn.locn -> string -> bvar_in_env
17  val make_aq_binding_occ   : locn.locn -> term -> bvar_in_env
18  val make_atom             : overload_info -> locn.locn ->
19                              string -> preterm_in_env
20  val make_qconst           : locn.locn -> string * string -> preterm_in_env
21  val list_make_comb        : locn.locn -> preterm_in_env list -> preterm_in_env
22  val bind_term             : locn.locn -> bvar_in_env list ->
23                              preterm_in_env -> preterm_in_env
24  val make_vstruct          : overload_info -> locn.locn -> bvar_in_env list ->
25                              pretype option -> bvar_in_env
26  val make_constrained      : locn.locn -> preterm_in_env -> pretype ->
27                              preterm_in_env
28  val make_let              : overload_info -> locn.locn ->
29                              (bvar_in_env list * preterm_in_env) list ->
30                              preterm_in_env -> preterm_in_env
31  val make_set_abs          : overload_info -> locn.locn ->
32                              preterm_in_env * preterm_in_env ->
33                              preterm_in_env
34
35  val make_case_arrow       : overload_info -> locn.locn ->
36                              preterm_in_env -> preterm_in_env ->
37                              preterm_in_env
38
39  val binder_restrictions   : unit -> (string * string) list
40  val associate_restriction : locn.locn -> string * string -> unit
41  val delete_restriction    : locn.locn -> string -> unit
42
43end
44