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