From 62284c7f39375becc8df188b171008f2fc92e14a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 16 Mar 2019 07:54:41 -0700
Subject: [PATCH] feat(library/init/control): add `estate` monad
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Optimized `except_t ε (state_t σ id) α`
---
 library/init/control/estate.lean |  127 +++
 src/boot/CMakeLists.txt          |    2 +-
 src/boot/init/control/estate.cpp | 1547 ++++++++++++++++++++++++++++++
 3 files changed, 1675 insertions(+), 1 deletion(-)
 create mode 100644 library/init/control/estate.lean
 create mode 100644 src/boot/init/control/estate.cpp

diff --git a/library/init/control/estate.lean b/library/init/control/estate.lean
new file mode 100644
index 0000000000..d8d8f8b06f
--- /dev/null
+++ b/library/init/control/estate.lean
@@ -0,0 +1,127 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+The combined except and state monad that minimizes the number
+of memory allocations using the approach described in the paper
+"Counting immutable beans" by Sebastian and Leo
+-/
+prelude
+import init.control.state init.control.except
+universes u v
+
+namespace estate
+
+inductive result (ε σ α : Type u)
+| ok    {} : α → σ → result
+| error {} : ε → σ → result
+
+variables {ε σ α : Type u}
+
+inductive result.is_ok : result ε σ α → Prop
+| mk (a : α) (s : σ) : result.is_ok (result.ok a s)
+
+theorem not_is_ok_error {e : ε} {s : σ} (h : @result.is_ok _ _ α (result.error e s)) : false :=
+match h with end
+
+@[inline] def unreachable_error {β : Type v} {e : ε} {s : σ} (h : @result.is_ok _ _ α (result.error e s)) : β :=
+false.elim (not_is_ok_error h)
+
+abbrev result_ok (ε σ α : Type u) := {r : result ε σ α // r.is_ok}
+
+@[inline] protected def result_ok.mk (a : α) (s : σ) : result_ok ε σ α :=
+⟨result.ok a s, result.is_ok.mk a s⟩
+
+protected def result.to_string [has_to_string ε] [has_to_string α] : result ε σ α → string
+| (result.ok a _)    := "ok: " ++ to_string a
+| (result.error e _) := "error: " ++ to_string e
+
+protected def result.repr [has_repr ε] [has_repr α] : result ε σ α → string
+| (result.error e _) := "(error " ++ repr e ++ ")"
+| (result.ok a _)    := "(ok " ++ repr a ++ ")"
+
+instance [has_to_string ε] [has_to_string α] : has_to_string (result ε σ α) := ⟨result.to_string⟩
+instance [has_repr ε] [has_repr α] : has_repr (result ε σ α) := ⟨result.repr⟩
+
+end estate
+
+def estate (ε σ α : Type u) := estate.result_ok punit σ punit → estate.result ε σ α
+
+namespace estate
+
+variables {ε σ α β : Type u}
+
+@[inline] protected def pure (a : α) : estate ε σ α :=
+λ r, match r with
+     | ⟨result.ok _ s, _⟩    := result.ok a s
+     | ⟨result.error _ _, h⟩ := unreachable_error h
+
+@[inline] protected def put (s : σ) : estate ε σ punit :=
+λ r, match r with
+     | ⟨result.ok _ _, _⟩    := result.ok ⟨⟩ s
+     | ⟨result.error _ _, h⟩ := unreachable_error h
+
+@[inline] protected def get : estate ε σ σ :=
+λ r, match r with
+     | ⟨result.ok _ s, _⟩    := result.ok s s
+     | ⟨result.error _ _, h⟩ := unreachable_error h
+
+@[inline] protected def modify (f : σ → σ) : estate ε σ punit :=
+λ r, match r with
+     | ⟨result.ok _ s, _⟩    := result.ok ⟨⟩ (f s)
+     | ⟨result.error _ _, h⟩ := unreachable_error h
+
+@[inline] protected def throw (e : ε) : estate ε σ α :=
+λ r, match r with
+     | ⟨result.ok _ s, _⟩    := result.error e s
+     | ⟨result.error _ _, h⟩ := unreachable_error h
+
+@[inline] protected def catch (x : estate ε σ α) (handle : ε → estate ε σ α) : estate ε σ α :=
+λ r, match x r with
+     | result.error e s := handle e (result_ok.mk ⟨⟩ s)
+     | ok               := ok
+
+@[inline] protected def orelse (x₁ x₂ : estate ε σ α) : estate ε σ α :=
+λ r, match x₁ r with
+     | result.error _ s := x₂ (result_ok.mk ⟨⟩ s)
+     | ok               := ok
+
+/-- Alternative orelse operator that allows to select which exception should be used.
+    The default is to use the first exception since the standard `orelse` uses the second. -/
+@[inline] protected def orelse' (x₁ x₂ : estate ε σ α) (use_first_ex := tt) : estate ε σ α :=
+λ r, match x₁ r with
+     | result.error e₁ s₁ :=
+       (match x₂ (result_ok.mk ⟨⟩ s₁) with
+        | result.error e₂ s₂ := result.error (if use_first_ex then e₁ else e₂) s₂
+        | ok                 := ok)
+     | ok                 := ok
+
+@[inline] def adapt_except {ε' : Type u} [has_lift_t ε' ε] (f : ε → ε') (x : estate ε σ α) : estate ε' σ α :=
+λ r, match x r with
+     | result.error e s := result.error (f e) s
+     | result.ok a s    := result.ok a s
+
+@[inline] protected def bind (x : estate ε σ α) (f : α → estate ε σ β) : estate ε σ β :=
+λ r, match x r with
+     | result.ok a s    := f a (result_ok.mk ⟨⟩ s)
+     | result.error e s := result.error e s
+
+@[inline] protected def map (f : α → β) (x : estate ε σ α) : estate ε σ β :=
+λ r, match x r with
+     | result.ok a s    := result.ok (f a) s
+     | result.error e s := result.error e s
+
+instance : monad (estate ε σ) :=
+{ bind := @estate.bind _ _, pure := @estate.pure _ _, map := @estate.map _ _ }
+
+instance : has_orelse (estate ε σ) :=
+{ orelse := @estate.orelse _ _ }
+
+instance : monad_state σ (estate ε σ) :=
+{ put := @estate.put _ _, get := @estate.get _ _, modify := @estate.modify _ _ }
+
+instance : monad_except ε (estate ε σ) :=
+{ throw := @estate.throw _ _, catch := @estate.catch _ _}
+
+end estate
diff --git a/src/boot/CMakeLists.txt b/src/boot/CMakeLists.txt
index 31bd7c370f..1bd237f4dc 100644
--- a/src/boot/CMakeLists.txt
+++ b/src/boot/CMakeLists.txt
@@ -1 +1 @@
-add_library (boot OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/default.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monad_fail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/basic.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/to_string.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/function.cpp ./init/io.cpp ./init/lean/compiler/const_folding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/ir.cpp ./init/lean/compiler/util.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/string_literal.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
+add_library (boot OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monad_fail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/basic.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/to_string.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/function.cpp ./init/io.cpp ./init/lean/compiler/const_folding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/ir.cpp ./init/lean/compiler/util.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/string_literal.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
diff --git a/src/boot/init/control/estate.cpp b/src/boot/init/control/estate.cpp
new file mode 100644
index 0000000000..7cf52dba24
--- /dev/null
+++ b/src/boot/init/control/estate.cpp
@@ -0,0 +1,1547 @@
+// Lean compiler output
+// Module: init.control.estate
+// Imports: init.control.state init.control.except
+#include "runtime/object.h"
+#include "runtime/apply.h"
+typedef lean::object obj;    typedef lean::usize  usize;
+typedef lean::uint8  uint8;  typedef lean::uint16 uint16;
+typedef lean::uint32 uint32; typedef lean::uint64 uint64;
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+obj* l_estate_get___rarg(obj*);
+obj* l_estate_result_repr___rarg(obj*, obj*, obj*);
+obj* l_estate_result_repr___main(obj*, obj*, obj*);
+obj* l_estate_throw___boxed(obj*, obj*, obj*);
+obj* l_estate_monad___lambda__3___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_estate_pure(obj*, obj*, obj*);
+obj* l_estate_has__orelse(obj*, obj*);
+obj* l_estate_result_repr___boxed(obj*, obj*, obj*);
+obj* l_estate_monad___closed__1;
+obj* l_estate_monad___boxed(obj*, obj*);
+obj* l_estate_throw(obj*, obj*, obj*);
+obj* l_estate_orelse(obj*, obj*, obj*);
+obj* l_estate_modify___rarg(obj*, obj*);
+obj* l_estate_catch___boxed(obj*, obj*, obj*);
+obj* l_estate_monad___lambda__4___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_estate_put(obj*, obj*);
+obj* l_estate_result__ok_mk___boxed(obj*, obj*, obj*);
+obj* l_estate_orelse_x_27(obj*, obj*, obj*);
+obj* l_estate_monad__except(obj*, obj*);
+obj* l_estate_orelse_x_27___rarg(obj*, obj*, uint8, obj*);
+obj* l_estate_monad__state___boxed(obj*, obj*);
+obj* l_estate_result_to__string___boxed(obj*, obj*, obj*);
+obj* l_estate_put___boxed(obj*, obj*);
+namespace lean {
+obj* string_append(obj*, obj*);
+}
+obj* l_estate_orelse_x_27___rarg___boxed(obj*, obj*, obj*, obj*);
+obj* l_estate_result_to__string___main(obj*, obj*, obj*);
+obj* l_estate_orelse_x_27___boxed(obj*, obj*, obj*);
+obj* l_estate_map___boxed(obj*, obj*, obj*, obj*);
+obj* l_estate_adapt__except___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_estate_result_repr___main___rarg(obj*, obj*, obj*);
+obj* l_estate_result_to__string(obj*, obj*, obj*);
+obj* l_estate_result_to__string___main___rarg___closed__1;
+obj* l_estate_has__to__string___boxed(obj*, obj*, obj*);
+obj* l_estate_monad___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_estate_adapt__except(obj*, obj*, obj*, obj*, obj*);
+obj* l_estate_get___boxed(obj*, obj*);
+obj* l_estate_result_repr(obj*, obj*, obj*);
+obj* l_estate_unreachable__error___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
+obj* l_estate_monad__state(obj*, obj*);
+obj* l_estate_pure___boxed(obj*, obj*, obj*);
+obj* l_estate_catch___rarg(obj*, obj*, obj*);
+obj* l_estate_orelse___rarg(obj*, obj*, obj*);
+extern obj* l_except_to__string___main___rarg___closed__2;
+obj* l_estate_monad___lambda__3(obj*, obj*, obj*, obj*, obj*);
+obj* l_estate_monad(obj*, obj*);
+obj* l_estate_bind___boxed(obj*, obj*, obj*, obj*);
+obj* l_estate_result_to__string___main___rarg(obj*, obj*, obj*);
+obj* l_estate_has__orelse___boxed(obj*, obj*);
+obj* l_estate_monad__except___closed__1;
+obj* l_estate_result__ok_mk___rarg(obj*, obj*);
+obj* l_estate_catch(obj*, obj*, obj*);
+obj* l_estate_has__repr___rarg(obj*, obj*);
+obj* l_estate_monad___lambda__2(obj*, obj*, obj*, obj*, obj*);
+obj* l_estate_put___rarg(obj*, obj*);
+obj* l_estate_has__repr(obj*, obj*, obj*);
+obj* l_estate_modify(obj*, obj*);
+obj* l_estate_has__orelse___closed__1;
+obj* l_estate_adapt__except___rarg(obj*, obj*, obj*);
+obj* l_estate_monad___lambda__4(obj*, obj*, obj*, obj*, obj*);
+obj* l_estate_result_to__string___rarg(obj*, obj*, obj*);
+obj* l_estate_map___rarg(obj*, obj*, obj*);
+obj* l_estate_bind___rarg(obj*, obj*, obj*);
+obj* l_estate_has__repr___boxed(obj*, obj*, obj*);
+obj* l_estate_result_to__string___main___boxed(obj*, obj*, obj*);
+obj* l_estate_pure___rarg(obj*, obj*);
+obj* l_estate_result_to__string___main___rarg___closed__2;
+obj* l_estate_result_repr___main___boxed(obj*, obj*, obj*);
+obj* l_estate_orelse___boxed(obj*, obj*, obj*);
+obj* l_estate_result__ok_mk(obj*, obj*, obj*);
+obj* l_estate_has__to__string(obj*, obj*, obj*);
+obj* l_estate_map(obj*, obj*, obj*, obj*);
+obj* l_estate_get(obj*, obj*);
+obj* l_estate_bind(obj*, obj*, obj*, obj*);
+obj* l_estate_throw___rarg(obj*, obj*);
+obj* l_estate_modify___boxed(obj*, obj*);
+extern obj* l_option_has__repr___rarg___closed__3;
+obj* l_estate_monad__except___boxed(obj*, obj*);
+obj* l_estate_monad___lambda__2___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_estate_has__to__string___rarg(obj*, obj*);
+obj* l_estate_monad___lambda__1(obj*, obj*, obj*, obj*, obj*);
+obj* l_estate_unreachable__error(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
+extern obj* l_except_to__string___main___rarg___closed__1;
+obj* l_estate_monad__state___closed__1;
+obj* l_estate_unreachable__error(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
+_start:
+{
+lean_unreachable();
+}
+}
+obj* l_estate_unreachable__error___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
+_start:
+{
+obj* x_7; 
+x_7 = l_estate_unreachable__error(x_0, x_1, x_2, x_3, x_4, x_5, x_6);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+lean::dec(x_3);
+lean::dec(x_4);
+lean::dec(x_5);
+lean::dec(x_6);
+return x_7;
+}
+}
+obj* l_estate_result__ok_mk___rarg(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_2, 0, x_0);
+lean::cnstr_set(x_2, 1, x_1);
+return x_2;
+}
+}
+obj* l_estate_result__ok_mk(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_result__ok_mk___rarg), 2, 0);
+return x_3;
+}
+}
+obj* l_estate_result__ok_mk___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_result__ok_mk(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* _init_l_estate_result_to__string___main___rarg___closed__1() {
+_start:
+{
+obj* x_0; 
+x_0 = lean::mk_string("ok: ");
+return x_0;
+}
+}
+obj* _init_l_estate_result_to__string___main___rarg___closed__2() {
+_start:
+{
+obj* x_0; 
+x_0 = lean::mk_string("error: ");
+return x_0;
+}
+}
+obj* l_estate_result_to__string___main___rarg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+if (lean::obj_tag(x_2) == 0)
+{
+obj* x_4; obj* x_7; obj* x_8; obj* x_9; 
+lean::dec(x_0);
+x_4 = lean::cnstr_get(x_2, 0);
+lean::inc(x_4);
+lean::dec(x_2);
+x_7 = lean::apply_1(x_1, x_4);
+x_8 = l_estate_result_to__string___main___rarg___closed__1;
+x_9 = lean::string_append(x_8, x_7);
+lean::dec(x_7);
+return x_9;
+}
+else
+{
+obj* x_12; obj* x_15; obj* x_16; obj* x_17; 
+lean::dec(x_1);
+x_12 = lean::cnstr_get(x_2, 0);
+lean::inc(x_12);
+lean::dec(x_2);
+x_15 = lean::apply_1(x_0, x_12);
+x_16 = l_estate_result_to__string___main___rarg___closed__2;
+x_17 = lean::string_append(x_16, x_15);
+lean::dec(x_15);
+return x_17;
+}
+}
+}
+obj* l_estate_result_to__string___main(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_result_to__string___main___rarg), 3, 0);
+return x_3;
+}
+}
+obj* l_estate_result_to__string___main___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_result_to__string___main(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l_estate_result_to__string___rarg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_result_to__string___main___rarg(x_0, x_1, x_2);
+return x_3;
+}
+}
+obj* l_estate_result_to__string(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_result_to__string___rarg), 3, 0);
+return x_3;
+}
+}
+obj* l_estate_result_to__string___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_result_to__string(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l_estate_result_repr___main___rarg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+if (lean::obj_tag(x_2) == 0)
+{
+obj* x_4; obj* x_7; obj* x_8; obj* x_9; obj* x_11; obj* x_12; 
+lean::dec(x_0);
+x_4 = lean::cnstr_get(x_2, 0);
+lean::inc(x_4);
+lean::dec(x_2);
+x_7 = lean::apply_1(x_1, x_4);
+x_8 = l_except_to__string___main___rarg___closed__2;
+x_9 = lean::string_append(x_8, x_7);
+lean::dec(x_7);
+x_11 = l_option_has__repr___rarg___closed__3;
+x_12 = lean::string_append(x_9, x_11);
+return x_12;
+}
+else
+{
+obj* x_14; obj* x_17; obj* x_18; obj* x_19; obj* x_21; obj* x_22; 
+lean::dec(x_1);
+x_14 = lean::cnstr_get(x_2, 0);
+lean::inc(x_14);
+lean::dec(x_2);
+x_17 = lean::apply_1(x_0, x_14);
+x_18 = l_except_to__string___main___rarg___closed__1;
+x_19 = lean::string_append(x_18, x_17);
+lean::dec(x_17);
+x_21 = l_option_has__repr___rarg___closed__3;
+x_22 = lean::string_append(x_19, x_21);
+return x_22;
+}
+}
+}
+obj* l_estate_result_repr___main(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_result_repr___main___rarg), 3, 0);
+return x_3;
+}
+}
+obj* l_estate_result_repr___main___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_result_repr___main(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l_estate_result_repr___rarg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_result_repr___main___rarg(x_0, x_1, x_2);
+return x_3;
+}
+}
+obj* l_estate_result_repr(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_result_repr___rarg), 3, 0);
+return x_3;
+}
+}
+obj* l_estate_result_repr___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_result_repr(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l_estate_has__to__string___rarg(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_result_to__string___rarg), 3, 2);
+lean::closure_set(x_2, 0, x_0);
+lean::closure_set(x_2, 1, x_1);
+return x_2;
+}
+}
+obj* l_estate_has__to__string(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_has__to__string___rarg), 2, 0);
+return x_3;
+}
+}
+obj* l_estate_has__to__string___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_has__to__string(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l_estate_has__repr___rarg(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_result_repr___rarg), 3, 2);
+lean::closure_set(x_2, 0, x_0);
+lean::closure_set(x_2, 1, x_1);
+return x_2;
+}
+}
+obj* l_estate_has__repr(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_has__repr___rarg), 2, 0);
+return x_3;
+}
+}
+obj* l_estate_has__repr___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_has__repr(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l_estate_pure___rarg(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_4; obj* x_5; 
+x_2 = lean::cnstr_get(x_1, 1);
+if (lean::is_exclusive(x_1)) {
+ lean::cnstr_release(x_1, 0);
+ x_4 = x_1;
+} else {
+ lean::inc(x_2);
+ lean::dec(x_1);
+ x_4 = lean::box(0);
+}
+if (lean::is_scalar(x_4)) {
+ x_5 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_5 = x_4;
+}
+lean::cnstr_set(x_5, 0, x_0);
+lean::cnstr_set(x_5, 1, x_2);
+return x_5;
+}
+}
+obj* l_estate_pure(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_pure___rarg), 2, 0);
+return x_3;
+}
+}
+obj* l_estate_pure___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_pure(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l_estate_put___rarg(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; obj* x_4; 
+if (lean::is_exclusive(x_1)) {
+ lean::cnstr_release(x_1, 0);
+ lean::cnstr_release(x_1, 1);
+ x_2 = x_1;
+} else {
+ lean::dec(x_1);
+ x_2 = lean::box(0);
+}
+x_3 = lean::box(0);
+if (lean::is_scalar(x_2)) {
+ x_4 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_4 = x_2;
+}
+lean::cnstr_set(x_4, 0, x_3);
+lean::cnstr_set(x_4, 1, x_0);
+return x_4;
+}
+}
+obj* l_estate_put(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_put___rarg), 2, 0);
+return x_2;
+}
+}
+obj* l_estate_put___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_estate_put(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_estate_get___rarg(obj* x_0) {
+_start:
+{
+obj* x_1; obj* x_3; obj* x_5; 
+x_1 = lean::cnstr_get(x_0, 1);
+if (lean::is_exclusive(x_0)) {
+ lean::cnstr_release(x_0, 0);
+ x_3 = x_0;
+} else {
+ lean::inc(x_1);
+ lean::dec(x_0);
+ x_3 = lean::box(0);
+}
+lean::inc(x_1);
+if (lean::is_scalar(x_3)) {
+ x_5 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_5 = x_3;
+}
+lean::cnstr_set(x_5, 0, x_1);
+lean::cnstr_set(x_5, 1, x_1);
+return x_5;
+}
+}
+obj* l_estate_get(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_get___rarg), 1, 0);
+return x_2;
+}
+}
+obj* l_estate_get___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_estate_get(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_estate_modify___rarg(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_4; obj* x_5; obj* x_6; obj* x_7; 
+x_2 = lean::cnstr_get(x_1, 1);
+if (lean::is_exclusive(x_1)) {
+ lean::cnstr_release(x_1, 0);
+ x_4 = x_1;
+} else {
+ lean::inc(x_2);
+ lean::dec(x_1);
+ x_4 = lean::box(0);
+}
+x_5 = lean::apply_1(x_0, x_2);
+x_6 = lean::box(0);
+if (lean::is_scalar(x_4)) {
+ x_7 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_7 = x_4;
+}
+lean::cnstr_set(x_7, 0, x_6);
+lean::cnstr_set(x_7, 1, x_5);
+return x_7;
+}
+}
+obj* l_estate_modify(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_modify___rarg), 2, 0);
+return x_2;
+}
+}
+obj* l_estate_modify___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_estate_modify(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_estate_throw___rarg(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_4; obj* x_5; 
+x_2 = lean::cnstr_get(x_1, 1);
+if (lean::is_exclusive(x_1)) {
+ lean::cnstr_release(x_1, 0);
+ x_4 = x_1;
+} else {
+ lean::inc(x_2);
+ lean::dec(x_1);
+ x_4 = lean::box(0);
+}
+if (lean::is_scalar(x_4)) {
+ x_5 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_5 = x_4;
+ lean::cnstr_set_tag(x_4, 1);
+}
+lean::cnstr_set(x_5, 0, x_0);
+lean::cnstr_set(x_5, 1, x_2);
+return x_5;
+}
+}
+obj* l_estate_throw(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_throw___rarg), 2, 0);
+return x_3;
+}
+}
+obj* l_estate_throw___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_throw(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l_estate_catch___rarg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::apply_1(x_0, x_2);
+if (lean::obj_tag(x_3) == 0)
+{
+lean::dec(x_1);
+return x_3;
+}
+else
+{
+obj* x_5; obj* x_7; obj* x_9; obj* x_10; obj* x_11; obj* x_12; 
+x_5 = lean::cnstr_get(x_3, 0);
+x_7 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ x_9 = x_3;
+} else {
+ lean::inc(x_5);
+ lean::inc(x_7);
+ lean::dec(x_3);
+ x_9 = lean::box(0);
+}
+x_10 = lean::box(0);
+if (lean::is_scalar(x_9)) {
+ x_11 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_11 = x_9;
+ lean::cnstr_set_tag(x_9, 0);
+}
+lean::cnstr_set(x_11, 0, x_10);
+lean::cnstr_set(x_11, 1, x_7);
+x_12 = lean::apply_2(x_1, x_5, x_11);
+return x_12;
+}
+}
+}
+obj* l_estate_catch(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_catch___rarg), 3, 0);
+return x_3;
+}
+}
+obj* l_estate_catch___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_catch(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l_estate_orelse___rarg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::apply_1(x_0, x_2);
+if (lean::obj_tag(x_3) == 0)
+{
+lean::dec(x_1);
+return x_3;
+}
+else
+{
+obj* x_5; obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
+x_5 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ lean::cnstr_release(x_3, 0);
+ x_7 = x_3;
+} else {
+ lean::inc(x_5);
+ lean::dec(x_3);
+ x_7 = lean::box(0);
+}
+x_8 = lean::box(0);
+if (lean::is_scalar(x_7)) {
+ x_9 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_9 = x_7;
+ lean::cnstr_set_tag(x_7, 0);
+}
+lean::cnstr_set(x_9, 0, x_8);
+lean::cnstr_set(x_9, 1, x_5);
+x_10 = lean::apply_1(x_1, x_9);
+return x_10;
+}
+}
+}
+obj* l_estate_orelse(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_orelse___rarg), 3, 0);
+return x_3;
+}
+}
+obj* l_estate_orelse___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_orelse(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l_estate_orelse_x_27___rarg(obj* x_0, obj* x_1, uint8 x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = lean::apply_1(x_0, x_3);
+if (lean::obj_tag(x_4) == 0)
+{
+lean::dec(x_1);
+return x_4;
+}
+else
+{
+obj* x_6; obj* x_8; obj* x_10; obj* x_11; obj* x_12; obj* x_13; 
+x_6 = lean::cnstr_get(x_4, 0);
+x_8 = lean::cnstr_get(x_4, 1);
+if (lean::is_exclusive(x_4)) {
+ x_10 = x_4;
+} else {
+ lean::inc(x_6);
+ lean::inc(x_8);
+ lean::dec(x_4);
+ x_10 = lean::box(0);
+}
+x_11 = lean::box(0);
+if (lean::is_scalar(x_10)) {
+ x_12 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_12 = x_10;
+ lean::cnstr_set_tag(x_10, 0);
+}
+lean::cnstr_set(x_12, 0, x_11);
+lean::cnstr_set(x_12, 1, x_8);
+x_13 = lean::apply_1(x_1, x_12);
+if (lean::obj_tag(x_13) == 0)
+{
+lean::dec(x_6);
+return x_13;
+}
+else
+{
+if (x_2 == 0)
+{
+obj* x_16; obj* x_18; obj* x_20; obj* x_21; 
+lean::dec(x_6);
+x_16 = lean::cnstr_get(x_13, 0);
+x_18 = lean::cnstr_get(x_13, 1);
+if (lean::is_exclusive(x_13)) {
+ x_20 = x_13;
+} else {
+ lean::inc(x_16);
+ lean::inc(x_18);
+ lean::dec(x_13);
+ x_20 = lean::box(0);
+}
+if (lean::is_scalar(x_20)) {
+ x_21 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_21 = x_20;
+}
+lean::cnstr_set(x_21, 0, x_16);
+lean::cnstr_set(x_21, 1, x_18);
+return x_21;
+}
+else
+{
+obj* x_22; obj* x_24; obj* x_25; 
+x_22 = lean::cnstr_get(x_13, 1);
+if (lean::is_exclusive(x_13)) {
+ lean::cnstr_release(x_13, 0);
+ x_24 = x_13;
+} else {
+ lean::inc(x_22);
+ lean::dec(x_13);
+ x_24 = lean::box(0);
+}
+if (lean::is_scalar(x_24)) {
+ x_25 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_25 = x_24;
+}
+lean::cnstr_set(x_25, 0, x_6);
+lean::cnstr_set(x_25, 1, x_22);
+return x_25;
+}
+}
+}
+}
+}
+obj* l_estate_orelse_x_27(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_orelse_x_27___rarg___boxed), 4, 0);
+return x_3;
+}
+}
+obj* l_estate_orelse_x_27___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+uint8 x_4; obj* x_5; 
+x_4 = lean::unbox(x_2);
+x_5 = l_estate_orelse_x_27___rarg(x_0, x_1, x_4, x_3);
+return x_5;
+}
+}
+obj* l_estate_orelse_x_27___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_estate_orelse_x_27(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l_estate_adapt__except___rarg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::apply_1(x_1, x_2);
+if (lean::obj_tag(x_3) == 0)
+{
+obj* x_5; obj* x_7; obj* x_9; obj* x_10; 
+lean::dec(x_0);
+x_5 = lean::cnstr_get(x_3, 0);
+x_7 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ x_9 = x_3;
+} else {
+ lean::inc(x_5);
+ lean::inc(x_7);
+ lean::dec(x_3);
+ x_9 = lean::box(0);
+}
+if (lean::is_scalar(x_9)) {
+ x_10 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_10 = x_9;
+}
+lean::cnstr_set(x_10, 0, x_5);
+lean::cnstr_set(x_10, 1, x_7);
+return x_10;
+}
+else
+{
+obj* x_11; obj* x_13; obj* x_15; obj* x_16; obj* x_17; 
+x_11 = lean::cnstr_get(x_3, 0);
+x_13 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ x_15 = x_3;
+} else {
+ lean::inc(x_11);
+ lean::inc(x_13);
+ lean::dec(x_3);
+ x_15 = lean::box(0);
+}
+x_16 = lean::apply_1(x_0, x_11);
+if (lean::is_scalar(x_15)) {
+ x_17 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_17 = x_15;
+}
+lean::cnstr_set(x_17, 0, x_16);
+lean::cnstr_set(x_17, 1, x_13);
+return x_17;
+}
+}
+}
+obj* l_estate_adapt__except(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_adapt__except___rarg), 3, 0);
+return x_5;
+}
+}
+obj* l_estate_adapt__except___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = l_estate_adapt__except(x_0, x_1, x_2, x_3, x_4);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+lean::dec(x_3);
+lean::dec(x_4);
+return x_5;
+}
+}
+obj* l_estate_bind___rarg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::apply_1(x_0, x_2);
+if (lean::obj_tag(x_3) == 0)
+{
+obj* x_4; obj* x_6; obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
+x_4 = lean::cnstr_get(x_3, 0);
+x_6 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ x_8 = x_3;
+} else {
+ lean::inc(x_4);
+ lean::inc(x_6);
+ lean::dec(x_3);
+ x_8 = lean::box(0);
+}
+x_9 = lean::box(0);
+if (lean::is_scalar(x_8)) {
+ x_10 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_10 = x_8;
+}
+lean::cnstr_set(x_10, 0, x_9);
+lean::cnstr_set(x_10, 1, x_6);
+x_11 = lean::apply_2(x_1, x_4, x_10);
+return x_11;
+}
+else
+{
+obj* x_13; obj* x_15; obj* x_17; obj* x_18; 
+lean::dec(x_1);
+x_13 = lean::cnstr_get(x_3, 0);
+x_15 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ x_17 = x_3;
+} else {
+ lean::inc(x_13);
+ lean::inc(x_15);
+ lean::dec(x_3);
+ x_17 = lean::box(0);
+}
+if (lean::is_scalar(x_17)) {
+ x_18 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_18 = x_17;
+}
+lean::cnstr_set(x_18, 0, x_13);
+lean::cnstr_set(x_18, 1, x_15);
+return x_18;
+}
+}
+}
+obj* l_estate_bind(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_bind___rarg), 3, 0);
+return x_4;
+}
+}
+obj* l_estate_bind___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_estate_bind(x_0, x_1, x_2, x_3);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+lean::dec(x_3);
+return x_4;
+}
+}
+obj* l_estate_map___rarg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::apply_1(x_1, x_2);
+if (lean::obj_tag(x_3) == 0)
+{
+obj* x_4; obj* x_6; obj* x_8; obj* x_9; obj* x_10; 
+x_4 = lean::cnstr_get(x_3, 0);
+x_6 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ x_8 = x_3;
+} else {
+ lean::inc(x_4);
+ lean::inc(x_6);
+ lean::dec(x_3);
+ x_8 = lean::box(0);
+}
+x_9 = lean::apply_1(x_0, x_4);
+if (lean::is_scalar(x_8)) {
+ x_10 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_10 = x_8;
+}
+lean::cnstr_set(x_10, 0, x_9);
+lean::cnstr_set(x_10, 1, x_6);
+return x_10;
+}
+else
+{
+obj* x_12; obj* x_14; obj* x_16; obj* x_17; 
+lean::dec(x_0);
+x_12 = lean::cnstr_get(x_3, 0);
+x_14 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ x_16 = x_3;
+} else {
+ lean::inc(x_12);
+ lean::inc(x_14);
+ lean::dec(x_3);
+ x_16 = lean::box(0);
+}
+if (lean::is_scalar(x_16)) {
+ x_17 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_17 = x_16;
+}
+lean::cnstr_set(x_17, 0, x_12);
+lean::cnstr_set(x_17, 1, x_14);
+return x_17;
+}
+}
+}
+obj* l_estate_map(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_map___rarg), 3, 0);
+return x_4;
+}
+}
+obj* l_estate_map___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_estate_map(x_0, x_1, x_2, x_3);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+lean::dec(x_3);
+return x_4;
+}
+}
+obj* l_estate_monad___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = lean::apply_1(x_3, x_4);
+if (lean::obj_tag(x_5) == 0)
+{
+obj* x_6; obj* x_8; obj* x_9; 
+x_6 = lean::cnstr_get(x_5, 1);
+if (lean::is_exclusive(x_5)) {
+ lean::cnstr_release(x_5, 0);
+ x_8 = x_5;
+} else {
+ lean::inc(x_6);
+ lean::dec(x_5);
+ x_8 = lean::box(0);
+}
+if (lean::is_scalar(x_8)) {
+ x_9 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_9 = x_8;
+}
+lean::cnstr_set(x_9, 0, x_2);
+lean::cnstr_set(x_9, 1, x_6);
+return x_9;
+}
+else
+{
+obj* x_11; obj* x_13; obj* x_15; obj* x_16; 
+lean::dec(x_2);
+x_11 = lean::cnstr_get(x_5, 0);
+x_13 = lean::cnstr_get(x_5, 1);
+if (lean::is_exclusive(x_5)) {
+ x_15 = x_5;
+} else {
+ lean::inc(x_11);
+ lean::inc(x_13);
+ lean::dec(x_5);
+ x_15 = lean::box(0);
+}
+if (lean::is_scalar(x_15)) {
+ x_16 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_16 = x_15;
+}
+lean::cnstr_set(x_16, 0, x_11);
+lean::cnstr_set(x_16, 1, x_13);
+return x_16;
+}
+}
+}
+obj* l_estate_monad___lambda__2(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = lean::apply_1(x_2, x_4);
+if (lean::obj_tag(x_5) == 0)
+{
+obj* x_6; obj* x_8; obj* x_10; obj* x_11; obj* x_12; obj* x_13; 
+x_6 = lean::cnstr_get(x_5, 0);
+x_8 = lean::cnstr_get(x_5, 1);
+if (lean::is_exclusive(x_5)) {
+ x_10 = x_5;
+} else {
+ lean::inc(x_6);
+ lean::inc(x_8);
+ lean::dec(x_5);
+ x_10 = lean::box(0);
+}
+x_11 = lean::box(0);
+if (lean::is_scalar(x_10)) {
+ x_12 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_12 = x_10;
+}
+lean::cnstr_set(x_12, 0, x_11);
+lean::cnstr_set(x_12, 1, x_8);
+x_13 = lean::apply_1(x_3, x_12);
+if (lean::obj_tag(x_13) == 0)
+{
+obj* x_14; obj* x_16; obj* x_18; obj* x_19; obj* x_20; 
+x_14 = lean::cnstr_get(x_13, 0);
+x_16 = lean::cnstr_get(x_13, 1);
+if (lean::is_exclusive(x_13)) {
+ x_18 = x_13;
+} else {
+ lean::inc(x_14);
+ lean::inc(x_16);
+ lean::dec(x_13);
+ x_18 = lean::box(0);
+}
+x_19 = lean::apply_1(x_6, x_14);
+if (lean::is_scalar(x_18)) {
+ x_20 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_20 = x_18;
+}
+lean::cnstr_set(x_20, 0, x_19);
+lean::cnstr_set(x_20, 1, x_16);
+return x_20;
+}
+else
+{
+obj* x_22; obj* x_24; obj* x_26; obj* x_27; 
+lean::dec(x_6);
+x_22 = lean::cnstr_get(x_13, 0);
+x_24 = lean::cnstr_get(x_13, 1);
+if (lean::is_exclusive(x_13)) {
+ x_26 = x_13;
+} else {
+ lean::inc(x_22);
+ lean::inc(x_24);
+ lean::dec(x_13);
+ x_26 = lean::box(0);
+}
+if (lean::is_scalar(x_26)) {
+ x_27 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_27 = x_26;
+}
+lean::cnstr_set(x_27, 0, x_22);
+lean::cnstr_set(x_27, 1, x_24);
+return x_27;
+}
+}
+else
+{
+obj* x_29; obj* x_31; obj* x_33; obj* x_34; 
+lean::dec(x_3);
+x_29 = lean::cnstr_get(x_5, 0);
+x_31 = lean::cnstr_get(x_5, 1);
+if (lean::is_exclusive(x_5)) {
+ x_33 = x_5;
+} else {
+ lean::inc(x_29);
+ lean::inc(x_31);
+ lean::dec(x_5);
+ x_33 = lean::box(0);
+}
+if (lean::is_scalar(x_33)) {
+ x_34 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_34 = x_33;
+}
+lean::cnstr_set(x_34, 0, x_29);
+lean::cnstr_set(x_34, 1, x_31);
+return x_34;
+}
+}
+}
+obj* l_estate_monad___lambda__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = lean::apply_1(x_2, x_4);
+if (lean::obj_tag(x_5) == 0)
+{
+obj* x_6; obj* x_8; obj* x_10; obj* x_11; obj* x_12; obj* x_13; 
+x_6 = lean::cnstr_get(x_5, 0);
+x_8 = lean::cnstr_get(x_5, 1);
+if (lean::is_exclusive(x_5)) {
+ x_10 = x_5;
+} else {
+ lean::inc(x_6);
+ lean::inc(x_8);
+ lean::dec(x_5);
+ x_10 = lean::box(0);
+}
+x_11 = lean::box(0);
+if (lean::is_scalar(x_10)) {
+ x_12 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_12 = x_10;
+}
+lean::cnstr_set(x_12, 0, x_11);
+lean::cnstr_set(x_12, 1, x_8);
+x_13 = lean::apply_1(x_3, x_12);
+if (lean::obj_tag(x_13) == 0)
+{
+obj* x_14; obj* x_16; obj* x_17; 
+x_14 = lean::cnstr_get(x_13, 1);
+if (lean::is_exclusive(x_13)) {
+ lean::cnstr_release(x_13, 0);
+ x_16 = x_13;
+} else {
+ lean::inc(x_14);
+ lean::dec(x_13);
+ x_16 = lean::box(0);
+}
+if (lean::is_scalar(x_16)) {
+ x_17 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_17 = x_16;
+}
+lean::cnstr_set(x_17, 0, x_6);
+lean::cnstr_set(x_17, 1, x_14);
+return x_17;
+}
+else
+{
+obj* x_19; obj* x_21; obj* x_23; obj* x_24; 
+lean::dec(x_6);
+x_19 = lean::cnstr_get(x_13, 0);
+x_21 = lean::cnstr_get(x_13, 1);
+if (lean::is_exclusive(x_13)) {
+ x_23 = x_13;
+} else {
+ lean::inc(x_19);
+ lean::inc(x_21);
+ lean::dec(x_13);
+ x_23 = lean::box(0);
+}
+if (lean::is_scalar(x_23)) {
+ x_24 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_24 = x_23;
+}
+lean::cnstr_set(x_24, 0, x_19);
+lean::cnstr_set(x_24, 1, x_21);
+return x_24;
+}
+}
+else
+{
+obj* x_26; obj* x_28; obj* x_30; obj* x_31; 
+lean::dec(x_3);
+x_26 = lean::cnstr_get(x_5, 0);
+x_28 = lean::cnstr_get(x_5, 1);
+if (lean::is_exclusive(x_5)) {
+ x_30 = x_5;
+} else {
+ lean::inc(x_26);
+ lean::inc(x_28);
+ lean::dec(x_5);
+ x_30 = lean::box(0);
+}
+if (lean::is_scalar(x_30)) {
+ x_31 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_31 = x_30;
+}
+lean::cnstr_set(x_31, 0, x_26);
+lean::cnstr_set(x_31, 1, x_28);
+return x_31;
+}
+}
+}
+obj* l_estate_monad___lambda__4(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = lean::apply_1(x_2, x_4);
+if (lean::obj_tag(x_5) == 0)
+{
+obj* x_6; obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
+x_6 = lean::cnstr_get(x_5, 1);
+if (lean::is_exclusive(x_5)) {
+ lean::cnstr_release(x_5, 0);
+ x_8 = x_5;
+} else {
+ lean::inc(x_6);
+ lean::dec(x_5);
+ x_8 = lean::box(0);
+}
+x_9 = lean::box(0);
+if (lean::is_scalar(x_8)) {
+ x_10 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_10 = x_8;
+}
+lean::cnstr_set(x_10, 0, x_9);
+lean::cnstr_set(x_10, 1, x_6);
+x_11 = lean::apply_1(x_3, x_10);
+return x_11;
+}
+else
+{
+obj* x_13; obj* x_15; obj* x_17; obj* x_18; 
+lean::dec(x_3);
+x_13 = lean::cnstr_get(x_5, 0);
+x_15 = lean::cnstr_get(x_5, 1);
+if (lean::is_exclusive(x_5)) {
+ x_17 = x_5;
+} else {
+ lean::inc(x_13);
+ lean::inc(x_15);
+ lean::dec(x_5);
+ x_17 = lean::box(0);
+}
+if (lean::is_scalar(x_17)) {
+ x_18 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_18 = x_17;
+}
+lean::cnstr_set(x_18, 0, x_13);
+lean::cnstr_set(x_18, 1, x_15);
+return x_18;
+}
+}
+}
+obj* _init_l_estate_monad___closed__1() {
+_start:
+{
+obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; 
+x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_map___boxed), 4, 2);
+lean::closure_set(x_0, 0, lean::box(0));
+lean::closure_set(x_0, 1, lean::box(0));
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_monad___lambda__1___boxed), 5, 0);
+x_2 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_2, 0, x_0);
+lean::cnstr_set(x_2, 1, x_1);
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_pure___boxed), 3, 2);
+lean::closure_set(x_3, 0, lean::box(0));
+lean::closure_set(x_3, 1, lean::box(0));
+x_4 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_monad___lambda__2___boxed), 5, 0);
+x_5 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_monad___lambda__3___boxed), 5, 0);
+x_6 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_monad___lambda__4___boxed), 5, 0);
+x_7 = lean::alloc_cnstr(0, 5, 0);
+lean::cnstr_set(x_7, 0, x_2);
+lean::cnstr_set(x_7, 1, x_3);
+lean::cnstr_set(x_7, 2, x_4);
+lean::cnstr_set(x_7, 3, x_5);
+lean::cnstr_set(x_7, 4, x_6);
+x_8 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_bind___boxed), 4, 2);
+lean::closure_set(x_8, 0, lean::box(0));
+lean::closure_set(x_8, 1, lean::box(0));
+x_9 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_9, 0, x_7);
+lean::cnstr_set(x_9, 1, x_8);
+return x_9;
+}
+}
+obj* l_estate_monad(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_estate_monad___closed__1;
+return x_2;
+}
+}
+obj* l_estate_monad___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = l_estate_monad___lambda__1(x_0, x_1, x_2, x_3, x_4);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_5;
+}
+}
+obj* l_estate_monad___lambda__2___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = l_estate_monad___lambda__2(x_0, x_1, x_2, x_3, x_4);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_5;
+}
+}
+obj* l_estate_monad___lambda__3___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = l_estate_monad___lambda__3(x_0, x_1, x_2, x_3, x_4);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_5;
+}
+}
+obj* l_estate_monad___lambda__4___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = l_estate_monad___lambda__4(x_0, x_1, x_2, x_3, x_4);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_5;
+}
+}
+obj* l_estate_monad___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_estate_monad(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* _init_l_estate_has__orelse___closed__1() {
+_start:
+{
+obj* x_0; 
+x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_orelse___boxed), 3, 2);
+lean::closure_set(x_0, 0, lean::box(0));
+lean::closure_set(x_0, 1, lean::box(0));
+return x_0;
+}
+}
+obj* l_estate_has__orelse(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_estate_has__orelse___closed__1;
+return x_2;
+}
+}
+obj* l_estate_has__orelse___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_estate_has__orelse(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* _init_l_estate_monad__state___closed__1() {
+_start:
+{
+obj* x_0; obj* x_1; obj* x_2; obj* x_3; 
+x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_get___rarg), 1, 0);
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_put___rarg), 2, 0);
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_modify___rarg), 2, 0);
+x_3 = lean::alloc_cnstr(0, 3, 0);
+lean::cnstr_set(x_3, 0, x_0);
+lean::cnstr_set(x_3, 1, x_1);
+lean::cnstr_set(x_3, 2, x_2);
+return x_3;
+}
+}
+obj* l_estate_monad__state(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_estate_monad__state___closed__1;
+return x_2;
+}
+}
+obj* l_estate_monad__state___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_estate_monad__state(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* _init_l_estate_monad__except___closed__1() {
+_start:
+{
+obj* x_0; obj* x_1; obj* x_2; 
+x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_throw___boxed), 3, 2);
+lean::closure_set(x_0, 0, lean::box(0));
+lean::closure_set(x_0, 1, lean::box(0));
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_estate_catch___boxed), 3, 2);
+lean::closure_set(x_1, 0, lean::box(0));
+lean::closure_set(x_1, 1, lean::box(0));
+x_2 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_2, 0, x_0);
+lean::cnstr_set(x_2, 1, x_1);
+return x_2;
+}
+}
+obj* l_estate_monad__except(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_estate_monad__except___closed__1;
+return x_2;
+}
+}
+obj* l_estate_monad__except___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_estate_monad__except(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+void initialize_init_control_state();
+void initialize_init_control_except();
+static bool _G_initialized = false;
+void initialize_init_control_estate() {
+ if (_G_initialized) return;
+ _G_initialized = true;
+ initialize_init_control_state();
+ initialize_init_control_except();
+ l_estate_result_to__string___main___rarg___closed__1 = _init_l_estate_result_to__string___main___rarg___closed__1();
+lean::mark_persistent(l_estate_result_to__string___main___rarg___closed__1);
+ l_estate_result_to__string___main___rarg___closed__2 = _init_l_estate_result_to__string___main___rarg___closed__2();
+lean::mark_persistent(l_estate_result_to__string___main___rarg___closed__2);
+ l_estate_monad___closed__1 = _init_l_estate_monad___closed__1();
+lean::mark_persistent(l_estate_monad___closed__1);
+ l_estate_has__orelse___closed__1 = _init_l_estate_has__orelse___closed__1();
+lean::mark_persistent(l_estate_has__orelse___closed__1);
+ l_estate_monad__state___closed__1 = _init_l_estate_monad__state___closed__1();
+lean::mark_persistent(l_estate_monad__state___closed__1);
+ l_estate_monad__except___closed__1 = _init_l_estate_monad__except___closed__1();
+lean::mark_persistent(l_estate_monad__except___closed__1);
+}