1signature EmitML =
2sig
3  include Abbrev
4
5  val reshape_thm_hook : (thm -> thm) ref
6  val pseudo_constr_rws : unit -> term list
7  val new_pseudo_constr : term * int -> unit
8  val is_int_literal_hook : (term -> bool) ref
9  val int_of_term_hook : (term -> Arbint.int) ref
10
11  datatype side = LEFT | RIGHT
12
13  val pp_type_as_ML     : hol_type PP.pprinter
14  val pp_term_as_ML     : string list -> side -> term PP.pprinter
15  val pp_defn_as_ML     : string list -> term PP.pprinter
16  val pp_datatype_as_ML : (string list * ParseDatatype.AST list) PP.pprinter
17
18  datatype elem = DEFN of thm
19                | DEFN_NOSIG of thm
20                | DATATYPE of hol_type quotation
21                | EQDATATYPE of string list * hol_type quotation
22                | ABSDATATYPE of string list * hol_type quotation
23                | OPEN of string list
24                | MLSIG of string
25                | MLSTRUCT of string
26
27  val MLSIGSTRUCT      : string list -> elem list
28
29  val sigSuffix        : string ref
30  val structSuffix     : string ref
31  val sigCamlSuffix    : string ref
32  val structCamlSuffix : string ref
33
34  val emitML   : string -> string * elem list -> unit
35  val emitCAML : string -> string * elem list -> unit
36
37  val eSML     : string -> elem list -> unit
38  val eCAML    : string -> elem list -> unit
39end
40