package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 =
  1. | Tstysymbol of Ty.tysymbol
  2. | Tsprsymbol of Decl.prsymbol
  3. | Tslsymbol of Term.lsymbol
val find_symbol : string -> Trans.naming_table -> symbol
type (!_, !_) trans_typ =
  1. | Ttrans : (Task.task Trans.trans, Task.task) trans_typ
  2. | Ttrans_l : (Task.task Trans.tlist, Task.task list) trans_typ
  3. | Tenvtrans : (Env.env -> Task.task Trans.trans, Task.task) trans_typ
  4. | Tenvtrans_l : (Env.env -> Task.task Trans.tlist, Task.task list) trans_typ
  5. | Tstring : ('a, 'b) trans_typ -> (string -> 'a, 'b) trans_typ
  6. | Tint : ('a0, 'b0) trans_typ -> (int -> 'a0, 'b0) trans_typ
  7. | Tty : ('a1, 'b1) trans_typ -> (Ty.ty -> 'a1, 'b1) trans_typ
  8. | Ttysymbol : ('a2, 'b2) trans_typ -> (Ty.tysymbol -> 'a2, 'b2) trans_typ
  9. | Tprsymbol : ('a3, 'b3) trans_typ -> (Decl.prsymbol -> 'a3, 'b3) trans_typ
  10. | Tprlist : ('a4, 'b4) trans_typ -> (Decl.prsymbol list -> 'a4, 'b4) trans_typ
  11. | Tlsymbol : ('a5, 'b5) trans_typ -> (Term.lsymbol -> 'a5, 'b5) trans_typ
  12. | Tsymbol : ('a6, 'b6) trans_typ -> (symbol -> 'a6, 'b6) trans_typ
  13. | Tlist : ('a7, 'b7) trans_typ -> (symbol list -> 'a7, 'b7) trans_typ
  14. | Tidentlist : ('a8, 'b8) trans_typ -> (string list -> 'a8, 'b8) trans_typ
  15. | Ttermlist : ('a9, 'b9) trans_typ -> (Term.term list -> 'a9, 'b9) trans_typ
  16. | Ttermlist_same : int * ('a10, 'b10) trans_typ -> (Term.term list -> 'a10, 'b10) trans_typ
  17. | Tterm : ('a11, 'b11) trans_typ -> (Term.term -> 'a11, 'b11) trans_typ
  18. | Tformula : ('a12, 'b12) trans_typ -> (Term.term -> 'a12, 'b12) trans_typ
  19. | Ttheory : ('a13, 'b13) trans_typ -> (Theory.theory -> 'a13, 'b13) trans_typ
  20. | Topt : string * ('a14 -> 'c, 'b14) trans_typ -> ('a14 option -> 'c, 'b14) trans_typ
  21. | 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
OCaml

Innovation. Community. Security.