diff --git a/library/init/core.lean b/library/init/core.lean index 49d61f0dbc..0e937d6e1d 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -85,9 +85,9 @@ universes u v w α /-- Gadget for marking output parameters in type classes. -/ -@[reducible] def out_param (α : Sort u) : Sort u := α +@[reducible] def inout_param (α : Sort u) : Sort u := α -notation `inout`:1024 a:0 := out_param a +notation `inout`:1024 a:0 := inout_param a inductive punit : Sort u | star : punit diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 9944c513c4..38d05e595d 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -300,7 +300,7 @@ bool elaborator::ready_to_synthesize(expr inst_type) { if (!is_pi(it)) return false; /* failed */ expr const & d = binding_domain(it); - if (has_expr_metavar(C_arg) && !is_class_out_param(d)) + if (has_expr_metavar(C_arg) && !is_class_inout_param(d)) return false; it = binding_body(it); } diff --git a/src/library/class.cpp b/src/library/class.cpp index 28de589230..c371ae4120 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -256,8 +256,8 @@ bool is_anonymous_inst_name(name const & n) { strlen(g_anonymous_inst_name_prefix->get_string())) == 0; } -bool is_class_out_param(expr const & e) { - return is_app_of(e, get_out_param_name(), 1); +bool is_class_inout_param(expr const & e) { + return is_app_of(e, get_inout_param_name(), 1); } void initialize_class() { diff --git a/src/library/class.h b/src/library/class.h index cdeb12b234..bffaa672eb 100644 --- a/src/library/class.h +++ b/src/library/class.h @@ -33,8 +33,8 @@ name const & get_anonymous_instance_prefix(); name mk_anonymous_inst_name(unsigned idx); bool is_anonymous_inst_name(name const & n); -/** \brief Return true iff e is of the form (out_param a) */ -bool is_class_out_param(expr const & e); +/** \brief Return true iff e is of the form (inout_param a) */ +bool is_class_inout_param(expr const & e); void initialize_class(); void finalize_class(); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index ff92a9bf95..91bda07730 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -284,7 +284,7 @@ name const * g_of_eq_true = nullptr; name const * g_of_iff_true = nullptr; name const * g_opt_param = nullptr; name const * g_or = nullptr; -name const * g_out_param = nullptr; +name const * g_inout_param = nullptr; name const * g_punit = nullptr; name const * g_punit_star = nullptr; name const * g_pos_num_bit0 = nullptr; @@ -655,7 +655,7 @@ void initialize_constants() { g_of_iff_true = new name{"of_iff_true"}; g_opt_param = new name{"opt_param"}; g_or = new name{"or"}; - g_out_param = new name{"out_param"}; + g_inout_param = new name{"inout_param"}; g_punit = new name{"punit"}; g_punit_star = new name{"punit", "star"}; g_pos_num_bit0 = new name{"pos_num", "bit0"}; @@ -1027,7 +1027,7 @@ void finalize_constants() { delete g_of_iff_true; delete g_opt_param; delete g_or; - delete g_out_param; + delete g_inout_param; delete g_punit; delete g_punit_star; delete g_pos_num_bit0; @@ -1398,7 +1398,7 @@ name const & get_of_eq_true_name() { return *g_of_eq_true; } name const & get_of_iff_true_name() { return *g_of_iff_true; } name const & get_opt_param_name() { return *g_opt_param; } name const & get_or_name() { return *g_or; } -name const & get_out_param_name() { return *g_out_param; } +name const & get_inout_param_name() { return *g_inout_param; } name const & get_punit_name() { return *g_punit; } name const & get_punit_star_name() { return *g_punit_star; } name const & get_pos_num_bit0_name() { return *g_pos_num_bit0; } diff --git a/src/library/constants.h b/src/library/constants.h index 360179ccf7..715f8c6df2 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -286,7 +286,7 @@ name const & get_of_eq_true_name(); name const & get_of_iff_true_name(); name const & get_opt_param_name(); name const & get_or_name(); -name const & get_out_param_name(); +name const & get_inout_param_name(); name const & get_punit_name(); name const & get_punit_star_name(); name const & get_pos_num_bit0_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index a0f729e2e2..56c71c50a5 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -279,7 +279,7 @@ of_eq_true of_iff_true opt_param or -out_param +inout_param punit punit.star pos_num.bit0 diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 7e5f00dd74..992ecdd3cc 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -3660,10 +3660,10 @@ static bool depends_on_mvar(expr const & e, buffer const & mvars) { } /* -Type class parameters can be annotated with out_param annotations. +Type class parameters can be annotated with inout_param annotations. Given (C a_1 ... a_n), we replace a_i with a temporary metavariable ?m_i IF -1- a_i is an out_param and it contains metavariables. +1- a_i is an inout_param and it contains metavariables. 2- a_i depends on a_j for j < i, and a_j was replaced with a temporary metavariable ?m_j. This case is needed to make sure the new C-application is type correct. @@ -3710,7 +3710,7 @@ expr type_context::preprocess_class(expr const & type, if (!is_pi(it2)) return type; /* failed */ expr const & d = binding_domain(it2); - if ((is_class_out_param(d) && has_expr_metavar(C_arg)) || + if ((is_class_inout_param(d) && has_expr_metavar(C_arg)) || (depends_on_mvar(d, new_mvars))) { expr new_mvar = mk_tmp_mvar(locals.mk_pi(d)); expr new_arg = mk_app(new_mvar, locals.as_buffer()); diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index 7020b9d7ae..678931ee2f 100644 --- a/tests/lean/run/check_constants.lean +++ b/tests/lean/run/check_constants.lean @@ -284,7 +284,7 @@ run_cmd script_check_id `of_eq_true run_cmd script_check_id `of_iff_true run_cmd script_check_id `opt_param run_cmd script_check_id `or -run_cmd script_check_id `out_param +run_cmd script_check_id `inout_param run_cmd script_check_id `punit run_cmd script_check_id `punit.star run_cmd script_check_id `pos_num.bit0 diff --git a/tests/lean/run/mvar_backtrack.lean b/tests/lean/run/mvar_backtrack.lean index 4c77fe8855..1aff48110e 100644 --- a/tests/lean/run/mvar_backtrack.lean +++ b/tests/lean/run/mvar_backtrack.lean @@ -1,11 +1,11 @@ namespace foo open nat -class lt (n : out_param ℕ) (m : ℕ) +class lt (n : inout ℕ) (m : ℕ) instance succ_lt_succ_of_lt (n m) [lt n m] : lt (succ n) (succ m) := by constructor instance zero_lt_succ (m) : lt 0 (succ m) := by constructor -class foo (n : out_param ℕ) (m : ℕ) +class foo (n : inout ℕ) (m : ℕ) instance (n m) [lt n 10] [lt m n] : foo n m := by constructor def bar {n} (m) [foo n m] := n diff --git a/tests/lean/run/quote_bas.lean b/tests/lean/run/quote_bas.lean index ccef44518d..9c42f2764f 100644 --- a/tests/lean/run/quote_bas.lean +++ b/tests/lean/run/quote_bas.lean @@ -58,7 +58,7 @@ begin { simp_using_hs } end -class Quote {V : out_param (Type u)} (l : out_param (Env V)) (n : Value) {V' : out_param (Type v)} (r : out_param (Env V')) := +class Quote {V : inout Type u} (l : inout Env V) (n : Value) {V' : inout Type v} (r : inout Env V') := (quote : Expr (sum V V')) (eval_quote : evalExpr (merge l r) quote = n) diff --git a/tests/lean/run/tc_inout1.lean b/tests/lean/run/tc_inout1.lean index 858511ce0d..6d1582ef83 100644 --- a/tests/lean/run/tc_inout1.lean +++ b/tests/lean/run/tc_inout1.lean @@ -17,7 +17,7 @@ We also fail if ?m_i is not assigned. Remark: we do not cache results when temporary metavariables ?m_i are used. -/ -class is_monoid (α : Type) (op : out_param (α → α → α)) (e : out_param α) := +class is_monoid (α : Type) (op : inout α → α → α) (e : inout α) := (op_assoc : associative op) (left_neutral : ∀ a : α, op e a = a) (right_neutral : ∀ a : α, op a e = a) @@ -58,7 +58,7 @@ assoc a b c end section -class has_mem2 (α : out_param (Type u)) (γ : Type v) := +class has_mem2 (α : inout Type u) (γ : Type v) := (mem : α → γ → Prop) def mem2 {α : Type u} {γ : Type v} [has_mem2 α γ] : α → γ → Prop :=