michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(api): annotate which procedures in the API may throw high-level exceptions

Browse source 
We say an exception is low-level (non high-level) when it is related to
memory exhaustion, system errors, and interruptions.
This commit is contained in:
Leonardo de Moura 2015-09-23 18:36:45 -07:00
parent 86e8508711
commit 97cf839665
12 changed files with 118 additions and 66 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/api/lean_decl.h
View file

@ -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);

12
src/api/lean_env.h
View file

@ -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. */

8
src/api/lean_exception.h
View file

@ -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 <tt>lean_exception * ex</tt> 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

54
src/api/lean_expr.h
View file

@ -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);
/*@}*/

9
src/api/lean_inductive.h
View file

@ -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,

12
src/api/lean_ios.h
View file

@ -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 */

6
src/api/lean_module.h
View file

@ -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 */

22
src/api/lean_name.h
View file

@ -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 <tt>pre.i</tt>.
\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);
/*@}*/

10
src/api/lean_options.h
View file

@ -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);
/*@}*/

9
src/api/lean_parser.h
View file

@ -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);
/*@}*/

12
src/api/lean_type_checker.h
View file

@ -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);
/*@}*/

18
src/api/lean_univ.h
View file

@ -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 <tt>ns</tt> with <tt>us</tt> 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);
/*@}*/