why3 1.3.2 · OCaml Package

why3

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 -> symbol

type (!_, !_) trans_typ =

| Ttrans : (Task.task Trans.trans, Task.task) trans_typ
| Ttrans_l : (Task.task Trans.tlist, Task.task list) trans_typ
| Tenvtrans : (Env.env -> Task.task Trans.trans, Task.task) trans_typ
| Tenvtrans_l : (Env.env -> Task.task Trans.tlist, Task.task list) trans_typ
| Tstring : ('a, 'b) trans_typ -> (string -> 'a, 'b) trans_typ
| Tint : ('a0, 'b0) trans_typ -> (int -> 'a0, 'b0) trans_typ
| Tty : ('a1, 'b1) trans_typ -> (Ty.ty -> 'a1, 'b1) trans_typ
| Ttysymbol : ('a2, 'b2) trans_typ -> (Ty.tysymbol -> 'a2, 'b2) trans_typ
| Tprsymbol : ('a3, 'b3) trans_typ -> (Decl.prsymbol -> 'a3, 'b3) trans_typ
| Tprlist : ('a4, 'b4) trans_typ -> (Decl.prsymbol list -> 'a4, 'b4) trans_typ
| Tlsymbol : ('a5, 'b5) trans_typ -> (Term.lsymbol -> 'a5, 'b5) trans_typ
| Tsymbol : ('a6, 'b6) trans_typ -> (symbol -> 'a6, 'b6) trans_typ
| Tlist : ('a7, 'b7) trans_typ -> (symbol list -> 'a7, 'b7) trans_typ
| Tidentlist : ('a8, 'b8) trans_typ -> (string list -> 'a8, 'b8) trans_typ
| Ttermlist : ('a9, 'b9) trans_typ -> (Term.term list -> 'a9, 'b9) trans_typ
| Ttermlist_same : int * ('a10, 'b10) trans_typ -> (Term.term list -> 'a10, 'b10) trans_typ
| Tterm : ('a11, 'b11) trans_typ -> (Term.term -> 'a11, 'b11) trans_typ
| Tformula : ('a12, 'b12) trans_typ -> (Term.term -> 'a12, 'b12) trans_typ
| Ttheory : ('a13, 'b13) trans_typ -> (Theory.theory -> 'a13, 'b13) trans_typ
| Topt : string * ('a14 -> 'c, 'b14) trans_typ -> ('a14 option -> 'c, 'b14) trans_typ
| Toptbool : string * ('a15, 'b15) trans_typ -> (bool -> 'a15, 'b15) trans_typ

val wrap_l : ('a, Task.task list) trans_typ -> 'a -> Trans.trans_with_args_l

val wrap : ('a, Task.task) trans_typ -> 'a -> Trans.trans_with_args

val wrap_and_register : 
  desc:Pp.formatted ->
  string ->
  ('a, 'b) trans_typ ->
  'a ->
  unit

val set_argument_parsing_functions : 
  Env.fformat ->
  parse_term:(Trans.naming_table -> Lexing.lexbuf -> Ptree.term) ->
  parse_term_list:(Trans.naming_table -> Lexing.lexbuf -> Ptree.term list) ->
  parse_qualid:(Lexing.lexbuf -> Ptree.qualid) ->
  parse_list_qualid:(Lexing.lexbuf -> Ptree.qualid list) ->
  parse_list_ident:(Lexing.lexbuf -> Ptree.ident list) ->
  unit

package why3