diff --git a/stage0/src/Init/Data/Option/Basic.lean b/stage0/src/Init/Data/Option/Basic.lean
index bf36b23cbe..ae88231c3a 100644
--- a/stage0/src/Init/Data/Option/Basic.lean
+++ b/stage0/src/Init/Data/Option/Basic.lean
@@ -64,10 +64,9 @@ instance : Monad Option := {
/- Remark: when using the polymorphic notation `a <|> b` is not a `[macroInline]`.
Thus, `a <|> b` will make `Option.orelse` to behave like it was marked as `[inline]`. -/
-instance : Alternative Option := {
- failure := none,
+instance : Alternative Option where
+ failure := none
orElse := Option.orElse
-}
@[inline] protected def lt (r : α → α → Prop) : Option α → Option α → Prop
| none, some x => True
@@ -82,22 +81,8 @@ instance (r : α → α → Prop) [s : DecidableRel r] : DecidableRel (Option.lt
end Option
-instance [DecidableEq α] : DecidableEq (Option α) := fun a b =>
- match a, b with
- | none, none => isTrue rfl
- | none, (some v₂) => isFalse (fun h => Option.noConfusion h)
- | (some v₁), none => isFalse (fun h => Option.noConfusion h)
- | (some v₁), (some v₂) =>
- match decEq v₁ v₂ with
- | (isTrue e) => isTrue (congrArg (@some α) e)
- | (isFalse n) => isFalse (fun h => Option.noConfusion h (fun e => absurd e n))
-
-instance [BEq α] : BEq (Option α) where
- beq
- | none, none => true
- | none, (some v₂) => false
- | (some v₁), none => false
- | (some v₁), (some v₂) => v₁ == v₂
+deriving instance DecidableEq for Option
+deriving instance BEq for Option
instance [HasLess α] : HasLess (Option α) := {
Less := Option.lt (· < ·)
diff --git a/stage0/src/Lean/Data/Position.lean b/stage0/src/Lean/Data/Position.lean
index b1032256da..f351dcd5c1 100644
--- a/stage0/src/Lean/Data/Position.lean
+++ b/stage0/src/Lean/Data/Position.lean
@@ -10,19 +10,9 @@ namespace Lean
structure Position where
line : Nat
column : Nat
- deriving Inhabited
+ deriving Inhabited, DecidableEq
namespace Position
-instance : DecidableEq Position :=
- fun ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ =>
- if h₁ : l₁ = l₂ then
- if h₂ : c₁ = c₂ then
- isTrue $ by subst h₁; subst h₂; rfl
- else
- isFalse fun contra => Position.noConfusion contra (fun e₁ e₂ => absurd e₂ h₂)
- else
- isFalse fun contra => Position.noConfusion contra (fun e₁ e₂ => absurd e₁ h₁)
-
protected def lt : Position → Position → Bool
| ⟨l₁, c₁⟩, ⟨l₂, c₂⟩ => (l₁, c₁) < (l₂, c₂)
diff --git a/stage0/src/Lean/Elab/Deriving/DecEq.lean b/stage0/src/Lean/Elab/Deriving/DecEq.lean
index 73237d8581..8b7c36d861 100644
--- a/stage0/src/Lean/Elab/Deriving/DecEq.lean
+++ b/stage0/src/Lean/Elab/Deriving/DecEq.lean
@@ -23,15 +23,17 @@ def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunNam
where
mkSameCtorRhs : List (Syntax × Syntax × Bool) → TermElabM Syntax
| [] => `(isTrue rfl)
- | (a, b, false) :: todo => withFreshMacroScope do
- `(if h : $a = $b then
- by subst h; exact $(← mkSameCtorRhs todo):term
- else
- isFalse (by intro n; injection n; apply h _; assumption))
- | (a, b, true) :: todo => withFreshMacroScope do
- `(@dite _ _ ($(mkIdent auxFunName) $a $b)
- (fun h => by subst h; exact $(← mkSameCtorRhs todo):term)
- (fun h => isFalse (by intro n; injection n; apply h _; assumption)))
+ | (a, b, recField) :: todo => withFreshMacroScope do
+ let rhs ←
+ `(if h : $a = $b then
+ by subst h; exact $(← mkSameCtorRhs todo):term
+ else
+ isFalse (by intro n; injection n; apply h _; assumption))
+ if recField then
+ -- add local instance for `a = b` using the function being defined `auxFunName`
+ `(let inst := $(mkIdent auxFunName) $a $b; $rhs)
+ else
+ return rhs
mkAlts : TermElabM (Array Syntax) := do
let mut alts := #[]
diff --git a/stage0/src/Lean/Elab/Quotation.lean b/stage0/src/Lean/Elab/Quotation.lean
index cd00890d32..674b7bd8d5 100644
--- a/stage0/src/Lean/Elab/Quotation.lean
+++ b/stage0/src/Lean/Elab/Quotation.lean
@@ -258,9 +258,7 @@ private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : T
| _, [] => throwError "non-exhaustive 'match_syntax'"
| discr::discrs, alts => do
let alts := (alts.map getHeadInfo).zip alts;
- -- Choose a most specific pattern, ie. a minimal element according to `generalizes`.
- -- If there are multiple minimal elements, the choice does not matter.
- let (info, alt) := alts.tail!.foldl (fun (min : HeadInfo × Alt) (alt : HeadInfo × Alt) => if min.1.generalizes alt.1 then alt else min) alts.head!;
+ let (info, alt) := alts.head!
-- introduce pattern matches on the discriminant's children if there are any nested patterns
let newDiscrs ← match info with
| basic { argPats := some pats, .. } => (List.range pats.size).mapM fun i => `(Syntax.getArg discr $(quote i))
diff --git a/stage0/src/library/compiler/ir_interpreter.cpp b/stage0/src/library/compiler/ir_interpreter.cpp
index bc4f6d8d2d..33161bc0d1 100644
--- a/stage0/src/library/compiler/ir_interpreter.cpp
+++ b/stage0/src/library/compiler/ir_interpreter.cpp
@@ -298,7 +298,7 @@ void * lookup_symbol_in_cur_exe(char const * sym) {
}
class interpreter;
-static interpreter & get_interpreter();
+LEAN_THREAD_PTR(interpreter, g_interpreter);
class interpreter {
// stack of IR variable slots
@@ -314,8 +314,8 @@ class interpreter {
frame(name const & mFn, size_t mArgBp, size_t mJpBp) : m_fn(mFn), m_arg_bp(mArgBp), m_jp_bp(mJpBp) {}
};
std::vector m_call_stack;
- environment const * m_env;
- options const * m_opts;
+ environment const & m_env;
+ options const & m_opts;
// if `false`, use IR code where possible
bool m_prefer_native;
struct constant_cache_entry {
@@ -353,30 +353,18 @@ class interpreter {
public:
template
static inline T with_interpreter(environment const & env, options const & opts, std::function const & f) {
- interpreter & interp = get_interpreter();
- if (interp.m_env && is_eqp(*interp.m_env, env) && interp.m_opts && is_eqp(*interp.m_opts, opts)) {
- return f(interp);
+ if (g_interpreter && is_eqp(g_interpreter->m_env, env) && is_eqp(g_interpreter->m_opts, opts)) {
+ return f(*g_interpreter);
} else {
// We changed threads or the closure was stored and called in a different context.
time_task t("interpretation",
message_builder(env, get_global_ios(), "foo", pos_info(), message_severity::INFORMATION));
abstract_type_context trace_ctx(opts);
scope_trace_env scope_trace(env, opts, trace_ctx);
- flet fl1(interp.m_env, &env);
- flet fl2(interp.m_opts, &opts);
- flet fl3(interp.m_prefer_native, opts.get_bool(*g_interpreter_prefer_native, LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE));
- if (interp.m_env) {
- // both these caches contain data from the Environment, so we cannot reuse them when changing it
- flet> fl4(interp.m_constant_cache, {});
- flet> fl5(interp.m_symbol_cache, {});
- return f(interp);
- } else {
- // if there is no outer interpreter, might as well leave the caches around; maybe the next call is for
- // the same Environment
- interp.m_constant_cache = {};
- interp.m_symbol_cache = {};
- return f(interp);
- }
+ // the caches contain data from the Environment, so we cannot reuse them when changing it
+ interpreter interp(env, opts);
+ flet fl(g_interpreter, &interp);
+ return f(interp);
}
}
@@ -412,8 +400,8 @@ private:
object * mk_stub_closure(decl const & d, unsigned n, object ** args) {
unsigned cls_size = 3 + decl_params(d).size();
object * cls = alloc_closure(get_stub(cls_size), cls_size, 3 + n);
- closure_set(cls, 0, m_env->to_obj_arg());
- closure_set(cls, 1, m_opts->to_obj_arg());
+ closure_set(cls, 0, m_env.to_obj_arg());
+ closure_set(cls, 1, m_opts.to_obj_arg());
closure_set(cls, 2, d.to_obj_arg());
for (unsigned i = 0; i < n ; i++)
closure_set(cls, 3 + i, args[i]);
@@ -741,7 +729,7 @@ private:
return *e;
} else {
symbol_cache_entry e_new { get_decl(fn), nullptr, false };
- if (m_prefer_native || decl_tag(e_new.m_decl) == decl_kind::Extern || has_init_attribute(*m_env, fn)) {
+ if (m_prefer_native || decl_tag(e_new.m_decl) == decl_kind::Extern || has_init_attribute(m_env, fn)) {
string_ref mangled = name_mangle(fn, *g_mangle_prefix);
string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw()));
// check for boxed version first
@@ -760,7 +748,7 @@ private:
/** \brief Retrieve Lean declaration from environment. */
decl get_decl(name const & fn) {
- option_ref d = find_ir_decl(*m_env, fn);
+ option_ref d = find_ir_decl(m_env, fn);
if (!d) {
throw exception(sstream() << "unknown declaration '" << fn << "'");
}
@@ -780,7 +768,7 @@ private:
return *o;
}
- if (get_regular_init_fn_name_for(*m_env, fn)) {
+ if (get_regular_init_fn_name_for(m_env, fn)) {
// We don't know whether `[init]` decls can be re-executed, so let's not.
throw exception(sstream() << "cannot evaluate `[init]` declaration '" << fn << "' in the same module");
}
@@ -917,6 +905,10 @@ private:
}
}
public:
+ explicit interpreter(environment const & env, options const & opts) : m_env(env), m_opts(opts) {
+ m_prefer_native = opts.get_bool(*g_interpreter_prefer_native, LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE);
+ }
+
~interpreter() {
for_each(m_constant_cache, [](name const &, constant_cache_entry const & e) {
if (!e.m_is_scalar) {
@@ -944,7 +936,7 @@ public:
} else {
// `lookup_symbol` does not prefer the boxed version for interpreted functions, so check manually.
decl d = e.m_decl;
- if (option_ref d_boxed = find_ir_decl(*m_env, fn + *g_boxed_suffix)) {
+ if (option_ref d_boxed = find_ir_decl(m_env, fn + *g_boxed_suffix)) {
d = *d_boxed.get();
}
r = mk_stub_closure(d, 0, nullptr);
@@ -1014,8 +1006,6 @@ public:
}
};
-MK_THREAD_LOCAL_GET_DEF(interpreter, get_interpreter);
-
object * run_boxed(environment const & env, options const & opts, name const & fn, unsigned n, object **args) {
return interpreter::with_interpreter