From 97cf839665b87a10ecbbcde2c5686887ddb587a6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Sep 2015 18:36:45 -0700 Subject: [PATCH] feat(api): annotate which procedures in the API may throw high-level exceptions We say an exception is low-level (non high-level) when it is related to memory exhaustion, system errors, and interruptions. --- src/api/lean_decl.h | 12 ++++++--- src/api/lean_env.h | 12 ++++++--- src/api/lean_exception.h | 8 ++++++ src/api/lean_expr.h | 54 ++++++++++++++++++++++++------------- src/api/lean_inductive.h | 9 ++++--- src/api/lean_ios.h | 12 ++++++--- src/api/lean_module.h | 6 +++-- src/api/lean_name.h | 22 ++++++++------- src/api/lean_options.h | 10 +++---- src/api/lean_parser.h | 9 ++++--- src/api/lean_type_checker.h | 12 ++++++--- src/api/lean_univ.h | 18 ++++++------- 12 files changed, 118 insertions(+), 66 deletions(-) diff --git a/src/api/lean_decl.h b/src/api/lean_decl.h index fbd523750..cae898c15 100644 --- a/src/api/lean_decl.h +++ b/src/api/lean_decl.h @@ -70,16 +70,20 @@ lean_bool lean_decl_get_univ_params(lean_decl d, lean_list_name * r, lean_except /** \brief Store in \c r the type of the given declaration. */ lean_bool lean_decl_get_type(lean_decl d, lean_expr * r, lean_exception * ex); /** \brief Store in \c r the value of the given theorem or definition. - \pre lean_decl_get_kind(d) == LEAN_DECL_THM || lean_decl_get_kind(d) == LEAN_DECL_DEF */ + \pre lean_decl_get_kind(d) == LEAN_DECL_THM || lean_decl_get_kind(d) == LEAN_DECL_DEF + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_decl_get_value(lean_decl d, lean_expr * r, lean_exception * ex); /** \brief Store in \c r the definitional height of the given theorem or definition. - \pre lean_decl_get_kind(d) == LEAN_DECL_THM || lean_decl_get_kind(d) == LEAN_DECL_DEF */ + \pre lean_decl_get_kind(d) == LEAN_DECL_THM || lean_decl_get_kind(d) == LEAN_DECL_DEF + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_decl_get_height(lean_decl d, unsigned * r, lean_exception * ex); /** \brief Store in \c r whether lazy unfolding is considered for the given definition. - \pre lean_decl_get_kind(d) == LEAN_DECL_DEF */ + \pre lean_decl_get_kind(d) == LEAN_DECL_DEF + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_decl_get_conv_opt(lean_decl d, lean_bool * r, lean_exception * ex); -/** \brief Create a certified declaration by type checking the given declaration with respect to the given environment */ +/** \brief Create a certified declaration by type checking the given declaration with respect to the given environment + \remark exceptions: LEAN_KERNEL_EXCEPTION */ lean_bool lean_decl_check(lean_env e, lean_decl d, lean_cert_decl * r, lean_exception * ex); /** \brief Delete/dispose the given certified declaration. */ void lean_cert_decl_del(lean_cert_decl d); diff --git a/src/api/lean_env.h b/src/api/lean_env.h index e787a0e10..d30cdae2c 100644 --- a/src/api/lean_env.h +++ b/src/api/lean_env.h @@ -30,14 +30,17 @@ lean_bool lean_env_mk_hott(unsigned t, lean_env * r, lean_exception * ex); /** Trust all macros implemented in Lean, and do no retype-check imported modules */ #define LEAN_TRUST_HIGH 100000 -/** \brief Add a new global universe with name \c u. */ +/** \brief Add a new global universe with name \c u. + \remark exceptions: LEAN_KERNEL_EXCEPTION */ lean_bool lean_env_add_univ(lean_env e, lean_name u, lean_env * r, lean_exception * ex); -/** \brief Create a new environment by adding the given certified declaration \c d to the environment \c e. */ +/** \brief Create a new environment by adding the given certified declaration \c d to the environment \c e. + \remark exceptions: LEAN_KERNEL_EXCEPTION */ lean_bool lean_env_add(lean_env e, lean_cert_decl d, lean_env * r, lean_exception * ex); /** \brief Replace the axiom with the name of the given certified theorem \c d with \c d. This procedure throws an exception if: - The theorem was certified in an environment which is not an ancestor of \c e. - - The environment does not contain an axiom with the given name. */ + - The environment does not contain an axiom with the given name. + \remark exceptions: LEAN_KERNEL_EXCEPTION */ lean_bool lean_env_replace(lean_env e, lean_cert_decl d, lean_env * r, lean_exception * ex); /** \brief Delete/dispose the given environment. */ @@ -54,7 +57,8 @@ lean_bool lean_env_impredicative(lean_env e); lean_bool lean_env_contains_univ(lean_env e, lean_name n); /** \brief Return true iff \c e contains a declaration with name \c n. */ lean_bool lean_env_contains_decl(lean_env e, lean_name n); -/** \brief Store in \c d the declaration with name \c n in \c e. */ +/** \brief Store in \c d the declaration with name \c n in \c e. + \remark exceptions: LEAN_KERNEL_EXCEPTION */ lean_bool lean_env_get_decl(lean_env e, lean_name n, lean_decl * d, lean_exception * ex); /** \brief Return true when \c e1 is a descendant of \c e2, that is, \c e1 was created by adding declarations to \c e2. */ diff --git a/src/api/lean_exception.h b/src/api/lean_exception.h index e00b08816..906806110 100644 --- a/src/api/lean_exception.h +++ b/src/api/lean_exception.h @@ -35,6 +35,14 @@ char const * lean_exception_get_message(lean_exception e); */ char const * lean_exception_get_detailed_message(lean_exception e); +/** \brief Exceptions and errors signed by the Lean API. + The first four (LEAN_NULL_EXCEPTION, LEAN_SYSTEM_EXCEPTION, LEAN_OUT_OF_MEMORY, LEAN_INTERRUPTED) + are considered to be low-level exceptions. + In principle, any procedure that has the argument lean_exception * ex may return one + of them. + The remaining ones can be viewed as "real" (or high-level) exceptions, and + we document the procedures that may throw them. +*/ typedef enum { LEAN_NULL_EXCEPTION, // null (aka there is no exception) LEAN_SYSTEM_EXCEPTION, // exception generated by the C++ runtime diff --git a/src/api/lean_expr.h b/src/api/lean_expr.h index d9ead0868..1b90f3629 100644 --- a/src/api/lean_expr.h +++ b/src/api/lean_expr.h @@ -100,52 +100,68 @@ lean_bool lean_expr_lt(lean_expr e1, lean_expr e2, lean_bool * b, lean_exception lean_bool lean_expr_quick_lt(lean_expr e1, lean_expr e2, lean_bool * b, lean_exception * ex); /** \brief Store in \c i the de-Brujin index of the given variable. - \pre lean_expr_get_kind(e) == LEAN_EXPR_VAR */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_VAR + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_var_idx(lean_expr e, unsigned * i, lean_exception * ex); /** \brief Stgore in \c u the universe of the given sort. - \pre lean_expr_get_kind(e) == LEAN_EXPR_SORT */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_SORT + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_sort_univ(lean_expr e, lean_univ * u, lean_exception * ex); /** \brief Store in \c n the name of the given constant. - \pre lean_expr_get_kind(e) == LEAN_EXPR_CONST */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_CONST + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_const_name(lean_expr e, lean_name * n, lean_exception * ex); /** \brief Store in \c us the universes parameters of the given constant. - \pre lean_expr_get_kind(e) == LEAN_EXPR_CONST */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_CONST + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_const_univs(lean_expr e, lean_list_univ * us, lean_exception * ex); /** \brief Store in \c f the function of the given function application. - \pre lean_expr_get_kind(e) == LEAN_EXPR_APP */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_APP + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_app_fun(lean_expr e, lean_expr * f, lean_exception * ex); /** \brief Store in \c a the argument of the given function application. - \pre lean_expr_get_kind(e) == LEAN_EXPR_APP */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_APP + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_app_arg(lean_expr e, lean_expr * a, lean_exception * ex); /** \brief Store in \c n the name the given local constant or meta-variable. - \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL || lean_expr_get_kind(e) == LEAN_EXPR_META */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL || lean_expr_get_kind(e) == LEAN_EXPR_META + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_mlocal_name(lean_expr e, lean_name * n, lean_exception * ex); /** \brief Store in \c t the type the given local constant or meta-variable. - \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL || lean_expr_get_kind(e) == LEAN_EXPR_META */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL || lean_expr_get_kind(e) == LEAN_EXPR_META + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_mlocal_type(lean_expr e, lean_expr * t, lean_exception * ex); /** \brief Store in \c n the pretty printing name the given local constant. - \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_local_pp_name(lean_expr e, lean_name * n, lean_exception * ex); /** \brief Store in \c k the binder_kind associated with the given local constant. - \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_local_binder_kind(lean_expr e, lean_binder_kind * k, lean_exception * ex); /** \brief Store in \c n the name associated with the given binding expression (i.e., lambda or Pi). - \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_binding_name(lean_expr e, lean_name * n, lean_exception * ex); /** \brief Store in \c d the domain of the given binding (i.e., lambda or Pi). - \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_binding_domain(lean_expr e, lean_expr * d, lean_exception * ex); /** \brief Store in \c b the body of the given binding (i.e., lambda or Pi). - \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_binding_body(lean_expr e, lean_expr * b, lean_exception * ex); /** \brief Store in \c k the binder_kind of the given binding (i.e., lambda or Pi). - \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_binding_binder_kind(lean_expr e, lean_binder_kind * k, lean_exception * ex); /** \brief Store in \c d the macro definition of the given macro application. - \pre lean_expr_get_kind(e) == LEAN_EXPR_MACRO */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_MACRO + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_macro_def(lean_expr e, lean_macro_def * d, lean_exception * ex); /** \brief Store in \c as the arguments of the given macro application. - \pre lean_expr_get_kind(e) == LEAN_EXPR_MACRO */ + \pre lean_expr_get_kind(e) == LEAN_EXPR_MACRO + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_expr_get_macro_args(lean_expr e, lean_list_expr * as, lean_exception * ex); /** \brief Create the empty list of exprs */ @@ -159,10 +175,12 @@ lean_bool lean_list_expr_is_cons(lean_list_expr l); /** \brief Return true in \c b iff the two given lists are equal */ lean_bool lean_list_expr_eq(lean_list_expr n1, lean_list_expr n2, lean_bool * b, lean_exception * ex); /** \brief Store in \c r the head of the given list - \pre lean_list_expr_is_cons(l) */ + \pre lean_list_expr_is_cons(l) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_list_expr_head(lean_list_expr l, lean_expr * r, lean_exception * ex); /** \brief Store in \c r the tail of the given list - \pre lean_list_expr_is_cons(l) */ + \pre lean_list_expr_is_cons(l) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_list_expr_tail(lean_list_expr l, lean_list_expr * r, lean_exception * ex); /*@}*/ diff --git a/src/api/lean_inductive.h b/src/api/lean_inductive.h index 289e447c3..bcc129bd6 100644 --- a/src/api/lean_inductive.h +++ b/src/api/lean_inductive.h @@ -26,7 +26,8 @@ LEAN_DEFINE_TYPE(lean_list_inductive_type); LEAN_DEFINE_TYPE(lean_inductive_decl); /** \brief Create a new inductive type with name \c n, type \c t, and constructors (aka introduction rules \c cs) - \remark \c cs must be a list of local constants. */ + \remark \c cs must be a list of local constants. + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_inductive_type_mk(lean_name n, lean_expr t, lean_list_expr cs, lean_inductive_type * r, lean_exception * ex); /** \brief Dispose/delete the given inductive type */ void lean_inductive_type_del(lean_inductive_type t); @@ -52,10 +53,12 @@ lean_bool lean_list_inductive_type_is_cons(lean_list_inductive_type l); /** \brief Return true in \c b iff the two given lists are equal */ lean_bool lean_list_inductive_type_eq(lean_list_inductive_type l1, lean_list_inductive_type l2, lean_bool * b, lean_exception * ex); /** \brief Store in \c r the head of the given list - \pre lean_list_inductive_type_is_cons(l) */ + \pre lean_list_inductive_type_is_cons(l) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_list_inductive_type_head(lean_list_inductive_type l, lean_inductive_type * r, lean_exception * ex); /** \brief Store in \c r the tail of the given list - \pre lean_list_inductive_type_is_cons(l) */ + \pre lean_list_inductive_type_is_cons(l) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_list_inductive_type_tail(lean_list_inductive_type l, lean_list_inductive_type * r, lean_exception * ex); /** \brief Create a mutually recursive inductive datatype declaration with universe parameters \c ps, diff --git a/src/api/lean_ios.h b/src/api/lean_ios.h index 8492441cf..c8c86ec4e 100644 --- a/src/api/lean_ios.h +++ b/src/api/lean_ios.h @@ -42,19 +42,23 @@ lean_bool lean_ios_set_options(lean_ios ios, lean_options o, lean_exception * ex lean_bool lean_ios_get_options(lean_ios ios, lean_options * r, lean_exception * ex); /** \brief Store in \c r the content of the regular output stream. - \pre !lean_ios_is_std(ios) */ + \pre !lean_ios_is_std(ios) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_ios_get_regular(lean_ios ios, char const ** r, lean_exception * ex); /** \brief Store in \c r the content of the diagnostic output stream. - \pre !lean_ios_is_std(ios) */ + \pre !lean_ios_is_std(ios) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_ios_get_diagnostic(lean_ios ios, char const ** r, lean_exception * ex); /** \brief Reset the regular output stream. - \pre !lean_ios_is_std(ios) */ + \pre !lean_ios_is_std(ios) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_ios_reset_regular(lean_ios ios, lean_exception * ex); /** \brief Reset the diagnostic output stream. - \pre !lean_ios_is_std(ios) */ + \pre !lean_ios_is_std(ios) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_ios_reset_diagnostic(lean_ios ios, lean_exception * ex); /** \brief Store in \c r a pretty printed representation of \c e */ diff --git a/src/api/lean_module.h b/src/api/lean_module.h index 8738724e2..0e97ab1c5 100644 --- a/src/api/lean_module.h +++ b/src/api/lean_module.h @@ -21,10 +21,12 @@ extern "C" { */ /*@{*/ -/** \brief Import the given modules (i.e., pre-compiled .olean files) */ +/** \brief Import the given modules (i.e., pre-compiled .olean files) + \remark exceptions: LEAN_KERNEL_EXCEPTION, LEAN_OTHER_EXCEPTION */ lean_bool lean_env_import(lean_env env, lean_ios ios, lean_list_name modules, lean_env * r, lean_exception * ex); -/** \brief Export to the given file name the declarations added to the environment */ +/** \brief Export to the given file name the declarations added to the environment + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_env_export(lean_env env, char const * fname, lean_exception * ex); /** \brief Store in \c r the LEAN_PATH */ diff --git a/src/api/lean_name.h b/src/api/lean_name.h index a0a0a3228..38f7583fb 100644 --- a/src/api/lean_name.h +++ b/src/api/lean_name.h @@ -29,7 +29,8 @@ lean_bool lean_name_mk_anonymous(lean_name * r, lean_exception * ex); lean_bool lean_name_mk_str(lean_name pre, char const * s, lean_name * r, lean_exception * ex); /** \brief Create the name pre.i. \pre !lean_name_is_anonymous(pre) - \remark \c r must be disposed using #lean_name_del */ + \remark \c r must be disposed using #lean_name_del + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_name_mk_idx(lean_name pre, unsigned i, lean_name * r, lean_exception * ex); /** \brief Delete/dispose the given hierarchical name */ void lean_name_del(lean_name n); @@ -41,29 +42,28 @@ lean_bool lean_name_is_str(lean_name n); lean_bool lean_name_is_idx(lean_name n); /** \brief Return true iff the two given hierarchical names are equal */ lean_bool lean_name_eq(lean_name n1, lean_name n2); -/** \brief Return the prefix of the given name. - \pre !lean_name_is_anonymous(n) -*/ /** \brief Return true if \c n1 is smaller than \c n2 in the internal total order. */ lean_bool lean_name_lt(lean_name n1, lean_name n2); /** \brief Return true if \c n1 is smaller than \c n2 in the internal total order. Similar to #lean_name_lt, but it is more efficient because it first compares the hashcodes associated with \c n1 and \c n2. */ lean_bool lean_name_quick_lt(lean_name n1, lean_name n2); +/** \brief Return the prefix of the given name. + \pre !lean_name_is_anonymous(n) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_name_get_prefix(lean_name n, lean_name * r, lean_exception * ex); /** \brief Store in \c r the suffix of the given name as a string. \pre lean_name_is_str(n) \remark \c r must be disposed using #lean_name_del -*/ + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_name_get_str(lean_name n, char const ** r, lean_exception * ex); /** \brief Store in \c r the suffix of the given name as a unsigned integer. \pre lean_name_is_idx(n) \remark \c r must be deleted using #lean_string_del -*/ + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_name_get_idx(lean_name n, unsigned * r, lean_exception * ex); /** \brief Store in \c r a string representation of the given hierarchical name. - \remark \c r must be deleted using #lean_string_del -*/ + \remark \c r must be deleted using #lean_string_del */ lean_bool lean_name_to_string(lean_name n, char const **r, lean_exception * ex); LEAN_DEFINE_TYPE(lean_list_name); @@ -79,10 +79,12 @@ lean_bool lean_list_name_is_cons(lean_list_name l); /** \brief Return true iff the two given lists are equal */ lean_bool lean_list_name_eq(lean_list_name n1, lean_list_name n2); /** \brief Store in \c r the head of the given list - \pre lean_list_name_is_cons(l) */ + \pre lean_list_name_is_cons(l) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_list_name_head(lean_list_name l, lean_name * r, lean_exception * ex); /** \brief Store in \c r the tail of the given list - \pre lean_list_name_is_cons(l) */ + \pre lean_list_name_is_cons(l) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_list_name_tail(lean_list_name l, lean_list_name * r, lean_exception * ex); /*@}*/ diff --git a/src/api/lean_options.h b/src/api/lean_options.h index 72e650175..e2cbe16e5 100644 --- a/src/api/lean_options.h +++ b/src/api/lean_options.h @@ -64,28 +64,28 @@ lean_bool lean_options_contains(lean_options o, lean_name n); /** \brief Store in \c r the value assigned to \c n in the options \c o. \pre lean_options_contains(o, n) \remark If the value associated with \c n is not a Boolean, the result is lean_false -*/ + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_options_get_bool(lean_options o, lean_name n, lean_bool * r, lean_exception * ex); /** \brief Store in \c r the value assigned to \c n in the options \c o. \pre lean_options_contains(o, n) \remark If the value associated with \c n is not a numeric value, the result is 0 -*/ + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_options_get_int(lean_options o, lean_name n, int * r, lean_exception * ex); /** \brief Store in \c r the value assigned to \c n in the options \c o. \pre lean_options_contains(o, n) \remark If the value associated with \c n is not a numeric value, the result is 0 -*/ + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_options_get_unsigned(lean_options o, lean_name n, unsigned * r, lean_exception * ex); /** \brief Store in \c r the value assigned to \c n in the options \c o. \pre lean_options_contains(o, n) \remark If the value associated with \c n is not a double, the result is 0.0 -*/ + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_options_get_double(lean_options o, lean_name n, double * r, lean_exception * ex); /** \brief Store in \c r the value assigned to \c n in the options \c o. \pre lean_options_contains(o, n) \remark If the value associated with \c n is not a double, the result is the empty string "" \remark \c r must be deleted using #lean_string_del. -*/ + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_options_get_string(lean_options o, lean_name n, char const ** r, lean_exception * ex); /*@}*/ diff --git a/src/api/lean_parser.h b/src/api/lean_parser.h index 39e67223f..683114487 100644 --- a/src/api/lean_parser.h +++ b/src/api/lean_parser.h @@ -23,16 +23,19 @@ extern "C" { /** \brief Parse the file \c fname using \c env and \c ios. Store the updated environment and ios at \c new_env and \c new_ios. - \remark We return a new ios object because Lean has commands for updating configuration options. */ + \remark We return a new ios object because Lean has commands for updating configuration options. + \remark exceptions: LEAN_KERNEL_EXCEPTION, LEAN_PARSER_EXCEPTION, LEAN_UNIFIER_EXCEPTION, LEAN_TACTIC_EXCEPTION, LEAN_OTHER_EXCEPTION */ lean_bool lean_parse_file(lean_env env, lean_ios ios, char const * fname, lean_env * new_env, lean_ios * new_ios, lean_exception * ex); /** \brief Parse the commands in the string \c str using \c env and \c ios. Store the updated environment and ios at \c new_env and \c new_ios. - \remark We return a new ios object because Lean has commands for updating configuration options. */ + \remark We return a new ios object because Lean has commands for updating configuration options. + \remark exceptions: LEAN_KERNEL_EXCEPTION, LEAN_PARSER_EXCEPTION, LEAN_UNIFIER_EXCEPTION, LEAN_TACTIC_EXCEPTION, LEAN_OTHER_EXCEPTION */ lean_bool lean_parse_commands(lean_env env, lean_ios ios, char const * str, lean_env * new_env, lean_ios * new_ios, lean_exception * ex); /** \brief Parse (and elaborate) the expression in the string \c str using \c env and \c ios. - Store the elaborated expression in \c new_expr, and automatically generated universe parameters in \c new_ps. */ + Store the elaborated expression in \c new_expr, and automatically generated universe parameters in \c new_ps. + \remark exceptions: LEAN_KERNEL_EXCEPTION, LEAN_PARSER_EXCEPTION, LEAN_UNIFIER_EXCEPTION, LEAN_TACTIC_EXCEPTION, LEAN_OTHER_EXCEPTION */ lean_bool lean_parse_expr(lean_env env, lean_ios ios, char const * str, lean_expr * new_expr, lean_list_name * new_ps, lean_exception * ex); /*@}*/ diff --git a/src/api/lean_type_checker.h b/src/api/lean_type_checker.h index 13bd7d20c..91ac1419a 100644 --- a/src/api/lean_type_checker.h +++ b/src/api/lean_type_checker.h @@ -34,19 +34,23 @@ void lean_type_checker_del(lean_type_checker t); void lean_cnstr_seq_del(lean_cnstr_seq s); /** \brief Infer the type of \c e using \c t. Store the result in \c r and any generated constraints in \c s. - \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR */ + \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR + \remark exceptions: LEAN_KERNEL_EXCEPTION */ lean_bool lean_type_checker_infer(lean_type_checker t, lean_expr e, lean_expr * r, lean_cnstr_seq * s, lean_exception * ex); /** \brief Type check and infer the type of \c e using \c t. Store the result in \c r and any generated constraints in \c s. - \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR */ + \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR + \remark exceptions: LEAN_KERNEL_EXCEPTION */ lean_bool lean_type_checker_check(lean_type_checker t, lean_expr e, lean_expr * r, lean_cnstr_seq * s, lean_exception * ex); /** \brief Compute the weak-head-normal-form of \c e using \c t. Store the result in \c r and any generated constraints in \c s. - \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR */ + \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR + \remark exceptions: LEAN_KERNEL_EXCEPTION */ lean_bool lean_type_checker_whnf(lean_type_checker t, lean_expr e, lean_expr * r, lean_cnstr_seq * s, lean_exception * ex); /** \brief Store true in \c r iff \c e1 and \c e2 are definitionally equal. Store any generated constraints in \c s. - \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR */ + \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR + \remark exceptions: LEAN_KERNEL_EXCEPTION */ lean_bool lean_type_checker_is_def_eq(lean_type_checker t, lean_expr e1, lean_expr e2, lean_bool * r, lean_cnstr_seq * s, lean_exception * ex); /*@}*/ diff --git a/src/api/lean_univ.h b/src/api/lean_univ.h index ceb67ff9c..ede9d7862 100644 --- a/src/api/lean_univ.h +++ b/src/api/lean_univ.h @@ -76,22 +76,21 @@ lean_bool lean_univ_geq(lean_univ u1, lean_univ u2, lean_bool * r, lean_exceptio /** \brief Store the predecessor universe of \c u in \c r. \pre lean_univ_get_kind(u) == LEAN_UNIV_SUCC -*/ + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_univ_get_pred(lean_univ u, lean_univ * r, lean_exception * ex); /** \brief Store the left-hand-side of the max/imax universe \c u in \c r. \pre lean_univ_get_kind(u) == LEAN_UNIV_MAX || lean_univ_get_kind(u) == LEAN_UNIV_IMAX -*/ - + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_univ_get_max_lhs(lean_univ u, lean_univ * r, lean_exception * ex); /** \brief Store the right-hand-side of the max/imax universe \c u in \c r. \pre lean_univ_get_kind(u) == LEAN_UNIV_MAX || lean_univ_get_kind(u) == LEAN_UNIV_IMAX -*/ + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_univ_get_max_rhs(lean_univ u, lean_univ * r, lean_exception * ex); /** \brief Store the name of the given universe in \c r. \pre lean_univ_get_kind(u) == LEAN_UNIV_PARAM || lean_univ_get_kind(u) == LEAN_UNIV_GLOBAL || lean_univ_get_kind(u) == LEAN_UNIV_META -*/ + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_univ_get_name(lean_univ u, lean_name * r, lean_exception * ex); /** \brief Store in \c r the normal for of the given universe */ lean_bool lean_univ_normalize(lean_univ u, lean_univ * r, lean_exception * ex); @@ -109,16 +108,17 @@ lean_bool lean_list_univ_is_cons(lean_list_univ l); /** \brief Store true in \c b iff the two given lists are equal */ lean_bool lean_list_univ_eq(lean_list_univ n1, lean_list_univ n2, lean_bool * b, lean_exception * ex); /** \brief Store in \c r the head of the given list - \pre lean_list_univ_is_cons(l) */ + \pre lean_list_univ_is_cons(l) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_list_univ_head(lean_list_univ l, lean_univ * r, lean_exception * ex); /** \brief Store in \c r the tail of the given list - \pre lean_list_univ_is_cons(l) */ + \pre lean_list_univ_is_cons(l) + \remark exceptions: LEAN_OTHER_EXCEPTION */ lean_bool lean_list_univ_tail(lean_list_univ l, lean_list_univ * r, lean_exception * ex); /** \brief Instantiate the universe parameters names in ns with us in \c u, and store the result in \c r. - \remark The given lists must have the same length. -*/ + \remark The given lists must have the same length. */ lean_bool lean_univ_instantiate(lean_univ u, lean_list_name ns, lean_list_univ us, lean_univ * r, lean_exception * ex); /*@}*/