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 Decl.prsymbol
exception Arg_qid_not_found of Ptree.qualid
exception Arg_error of string
exception Arg_parse_type_error of Loc.position * string * exn
val build_naming_tables : Task.task -> Trans.naming_table
type symbol =
Tstysymbol of Ty.tysymbol
| Tsprsymbol of Decl.prsymbol
| Tslsymbol of Term.lsymbol
val find_symbol : string -> Trans.naming_table -> Args_wrapper.symbol
type (_, _) trans_typ =
Ttrans : (Task.task Trans.trans, Task.task) Args_wrapper.trans_typ
| Ttrans_l :
(Task.task Trans.tlist, Task.task list) Args_wrapper.trans_typ
| Tenvtrans :
(Env.env -> Task.task Trans.trans, Task.task) Args_wrapper.trans_typ
| Tenvtrans_l :
(Env.env -> Task.task Trans.tlist, 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 -> (Ty.ty -> 'a, 'b)
Args_wrapper.trans_typ
| Ttysymbol :
('a, 'b) Args_wrapper.trans_typ -> (Ty.tysymbol -> 'a, 'b)
Args_wrapper.trans_typ
| Tprsymbol :
('a, 'b) Args_wrapper.trans_typ -> (Decl.prsymbol -> 'a, 'b)
Args_wrapper.trans_typ
| Tprlist :
('a, 'b) Args_wrapper.trans_typ -> (Decl.prsymbol list -> 'a, 'b)
Args_wrapper.trans_typ
| Tlsymbol :
('a, 'b) Args_wrapper.trans_typ -> (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 -> (Term.term list -> 'a, 'b)
Args_wrapper.trans_typ
| Ttermlist_same : int *
('a, 'b) Args_wrapper.trans_typ -> (Term.term list -> 'a, 'b)
Args_wrapper.trans_typ
| Tterm :
('a, 'b) Args_wrapper.trans_typ -> (Term.term -> 'a, 'b)
Args_wrapper.trans_typ
| Tformula :
('a, 'b) Args_wrapper.trans_typ -> (Term.term -> 'a, 'b)
Args_wrapper.trans_typ
| Ttheory :
('a, 'b) Args_wrapper.trans_typ -> (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, Task.task list) Args_wrapper.trans_typ ->
'a -> Trans.trans_with_args_l
val wrap :
('a, Task.task) Args_wrapper.trans_typ -> 'a -> Trans.trans_with_args
val wrap_and_register :
desc:Pp.formatted ->
string -> ('a, 'b) Args_wrapper.trans_typ -> 'a -> unit
val parse_and_type_list :
lang:string ->
as_fmla:bool -> string -> Trans.naming_table -> Term.term list
val set_argument_parsing_functions :
Env.fformat ->
parse_term:(Trans.naming_table -> Stdlib.Lexing.lexbuf -> Ptree.term) ->
parse_term_list:(Trans.naming_table ->
Stdlib.Lexing.lexbuf -> Ptree.term list) ->
parse_qualid:(Stdlib.Lexing.lexbuf -> Ptree.qualid) ->
parse_list_qualid:(Stdlib.Lexing.lexbuf -> Ptree.qualid list) ->
parse_list_ident:(Stdlib.Lexing.lexbuf -> Ptree.ident list) -> unit
end