sig
  exception Parse_error of string
  exception Arg_expected of string * string
  exception Arg_theory_not_found of string
  exception Arg_expected_none of string
  exception Arg_pr_not_found of Why3.Decl.prsymbol
  exception Arg_qid_not_found of Why3.Ptree.qualid
  exception Arg_error of string
  exception Arg_parse_type_error of Why3.Loc.position * string * exn
  val build_naming_tables : Why3.Task.task -> Why3.Trans.naming_table
  type symbol =
      Tstysymbol of Why3.Ty.tysymbol
    | Tsprsymbol of Why3.Decl.prsymbol
    | Tslsymbol of Why3.Term.lsymbol
  val find_symbol : string -> Why3.Trans.naming_table -> Args_wrapper.symbol
  type (_, _) trans_typ =
      Ttrans :
        (Why3.Task.task Why3.Trans.trans, Why3.Task.task)
        Args_wrapper.trans_typ
    | Ttrans_l :
        (Why3.Task.task Why3.Trans.tlist, Why3.Task.task list)
        Args_wrapper.trans_typ
    | Tenvtrans :
        (Why3.Env.env -> Why3.Task.task Why3.Trans.trans, Why3.Task.task)
        Args_wrapper.trans_typ
    | Tenvtrans_l :
        (Why3.Env.env -> Why3.Task.task Why3.Trans.tlist,
         Why3.Task.task list)
        Args_wrapper.trans_typ
    | Tstring :
        ('a, 'b) Args_wrapper.trans_typ -> (string -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tint :
        ('a, 'b) Args_wrapper.trans_typ -> (int -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tty :
        ('a, 'b) Args_wrapper.trans_typ -> (Why3.Ty.ty -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Ttysymbol :
        ('a, 'b) Args_wrapper.trans_typ -> (Why3.Ty.tysymbol -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tprsymbol :
        ('a, 'b) Args_wrapper.trans_typ -> (Why3.Decl.prsymbol -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tprlist :
        ('a, 'b) Args_wrapper.trans_typ -> (Why3.Decl.prsymbol list -> 'a,
                                            'b)
                                           Args_wrapper.trans_typ
    | Tlsymbol :
        ('a, 'b) Args_wrapper.trans_typ -> (Why3.Term.lsymbol -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tsymbol :
        ('a, 'b) Args_wrapper.trans_typ -> (Args_wrapper.symbol -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tlist :
        ('a, 'b) Args_wrapper.trans_typ -> (Args_wrapper.symbol list -> 'a,
                                            'b)
                                           Args_wrapper.trans_typ
    | Tidentlist :
        ('a, 'b) Args_wrapper.trans_typ -> (string list -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Ttermlist :
        ('a, 'b) Args_wrapper.trans_typ -> (Why3.Term.term list -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Ttermlist_same : int *
        ('a, 'b) Args_wrapper.trans_typ -> (Why3.Term.term list -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tterm :
        ('a, 'b) Args_wrapper.trans_typ -> (Why3.Term.term -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tformula :
        ('a, 'b) Args_wrapper.trans_typ -> (Why3.Term.term -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Ttheory :
        ('a, 'b) Args_wrapper.trans_typ -> (Why3.Theory.theory -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Topt : string *
        ('a -> 'c, 'b) Args_wrapper.trans_typ -> ('a option -> 'c, 'b)
                                                 Args_wrapper.trans_typ
    | Toptbool : string *
        ('a, 'b) Args_wrapper.trans_typ -> (bool -> 'a, 'b)
                                           Args_wrapper.trans_typ
  val wrap_l :
    ('a, Why3.Task.task list) Args_wrapper.trans_typ ->
    'a -> Why3.Trans.trans_with_args_l
  val wrap :
    ('a, Why3.Task.task) Args_wrapper.trans_typ ->
    'a -> Why3.Trans.trans_with_args
  val wrap_and_register :
    desc:Why3.Pp.formatted ->
    string -> ('a, 'b) Args_wrapper.trans_typ -> 'a -> unit
  type packed_trans_typ =
      Pack : ('a, 'b) Args_wrapper.trans_typ -> Args_wrapper.packed_trans_typ
  val get_trans_typ : string -> Args_wrapper.packed_trans_typ option
  val parse_and_type_list :
    lang:string ->
    as_fmla:bool -> string -> Why3.Trans.naming_table -> Why3.Term.term list
  val set_argument_parsing_functions :
    Why3.Env.fformat ->
    parse_term:(Why3.Trans.naming_table ->
                Stdlib.Lexing.lexbuf -> Why3.Ptree.term) ->
    parse_term_list:(Why3.Trans.naming_table ->
                     Stdlib.Lexing.lexbuf -> Why3.Ptree.term list) ->
    parse_qualid:(Stdlib.Lexing.lexbuf -> Why3.Ptree.qualid) ->
    parse_list_qualid:(Stdlib.Lexing.lexbuf -> Why3.Ptree.qualid list) ->
    parse_list_ident:(Stdlib.Lexing.lexbuf -> Why3.Ptree.ident list) -> unit
end