sig
  val check_tp : string -> Term.term -> bool
  exception DECODE of string
  exception TOPLEVEL_ERROR of string * Term.term option
  val code_list :
    Term.term array -> ('a -> Term.term) -> 'a list -> Term.term
  val decode_list :
    normalized:bool -> (Term.term -> 'a) -> Term.term -> 'a list
  val decode_list_opt : (Term.term -> 'a) -> Term.term -> 'a list option
  val code_hlist : ('a -> Term.term) -> 'a list -> Term.term
  val decode_hlist :
    normalized:bool -> (Term.term -> 'a) -> Term.term -> 'a list
  val decode_hlist_opt : (Term.term -> 'a) -> Term.term -> 'a list option
  val int_to_bits : int -> int list
  val bits_to_int : int list -> int
  val code_bit : int -> Term.term
  val decode_bit : normalized:bool -> Term.term -> int
  val decode_bit_list : normalized:bool -> Term.term -> int
  val code_char : char -> Term.term
  val decode_char : normalized:bool -> Term.term -> char
  val code_string : ?value_prefix:bool -> string -> Term.term
  val decode_string : normalized:bool -> Term.term -> string
  val decode_string_opt : Term.term -> string option
  val code_bool : bool -> Term.term
  val decode_bool : normalized:bool -> Term.term -> bool
  val code_term : Term.term -> Term.term
  val code_term_incr_vars : Term.term -> Term.term
  val decode_term : normalized:bool -> Term.term -> Term.term
  val unpack_te : Term.term -> Term.term
  type rewrite_rule = bool * Term.term * Term.term
  val code_rewrite_rule : Coding.rewrite_rule -> Term.term
  val decode_rewrite_rule :
    normalized:bool -> Term.term -> Coding.rewrite_rule
  val code_input_rewrite_rule : Coding.rewrite_rule -> Term.term
  val decode_input_rewrite_rule :
    normalized:bool -> Term.term -> Coding.rewrite_rule
  val code_priority_input_rewrite_rule : Coding.rewrite_rule -> Term.term
  val decode_priority_input_rewrite_rule :
    normalized:bool -> Term.term -> Coding.rewrite_rule
  type fun_definition = string * Term.term list * Term.term
  val code_fun_definition : Coding.fun_definition -> Term.term
  val decode_fun_definition :
    normalized:bool -> Term.term -> Coding.fun_definition
  val decode_syntax_element :
    normalized:bool -> Term.term -> SyntaxDef.syntax_elem
  val code_syntax_element_list : SyntaxDef.syntax_elem list -> Term.term
  val decode_syntax_element_list :
    normalized:bool -> Term.term -> SyntaxDef.syntax_elem list
  val code_syntax_definition : SyntaxDef.syntax_def -> Term.term
  val decode_syntax_definition :
    normalized:bool -> Term.term -> SyntaxDef.syntax_def
  val func_sd_of_sd : SyntaxDef.syntax_def -> SyntaxDef.syntax_def option
  val matches :
    (string * Term.term) list Pervasives.ref -> Term.term * Term.term -> bool
  val apply_s : (string * Term.term) list -> Term.term -> Term.term
  val display_term :
    ?sdefs:(string * SyntaxDef.syntax_def) list ->
    ?full:[ `Full | `HeadType | `NoSupercl | `NoTypes ] ->
    Term.term -> string
  val display_super :
    (string * SyntaxDef.syntax_def) list option ->
    [ `Full | `HeadType | `NoSupercl | `NoTypes ] ->
    Term.term array -> string
  val display_term_bracketed : Term.term -> string
  val display_shortly_bracketed : Term.term -> string
  val display_hterm :
    ?types:bool ->
    ?bracketed:bool ->
    ?sdefs:(string * SyntaxDef.syntax_def) list ->
    Term.decls_set -> Term.term -> string
  val display_term_xml : Term.term -> string
  val term_to_string : Term.term -> string
  val parse_term : Aux.split_result list -> Term.term * Aux.split_result list
  val term_of_string : string -> Term.term
  val short_term : Term.term -> string
  val split_sdef_name : string -> string option list
  val pretty_print_sd : SyntaxDef.syntax_def -> string
  val brackets_rules : (bool * Term.term * Term.term) list
  val verbatim_rules : (bool * Term.term * Term.term) list
  val if_then_else_rules : (bool * Term.term * Term.term) list
  val additional_xslt_rules : (bool * Term.term * Term.term) list
  val string_quote_rules : (bool * Term.term * Term.term) list
end