refactor(library/init/core): rename out_param => inout_param

It is really input/output.

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

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

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() {

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

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; }

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

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

src/library/type_context.cpp

@@ -3660,10 +3660,10 @@ static bool depends_on_mvar(expr const & e, buffer<expr> 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());

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

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

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)
 

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 :=