rookiemango commited on
Commit
a4fcbf1
·
verified ·
1 Parent(s): 7da71c8

Upload folder using huggingface_hub

Browse files
This view is limited to 50 files because it contains too many changes.   See raw diff
Files changed (50) hide show
  1. .gitattributes +10 -0
  2. .lake/build/bin/repl +3 -0
  3. .lake/build/bin/repl.hash +1 -0
  4. .lake/build/bin/repl.trace +1 -0
  5. .lake/build/ir/REPL/Frontend.c +743 -0
  6. .lake/build/ir/REPL/Frontend.c.hash +1 -0
  7. .lake/build/ir/REPL/Frontend.c.o +0 -0
  8. .lake/build/ir/REPL/Frontend.c.o.hash +1 -0
  9. .lake/build/ir/REPL/Frontend.c.o.trace +1 -0
  10. .lake/build/ir/REPL/JSON.c +0 -0
  11. .lake/build/ir/REPL/JSON.c.hash +1 -0
  12. .lake/build/ir/REPL/JSON.c.o +0 -0
  13. .lake/build/ir/REPL/JSON.c.o.hash +1 -0
  14. .lake/build/ir/REPL/JSON.c.o.trace +1 -0
  15. .lake/build/ir/REPL/Lean/ContextInfo.c +85 -0
  16. .lake/build/ir/REPL/Lean/ContextInfo.c.hash +1 -0
  17. .lake/build/ir/REPL/Lean/ContextInfo.c.o +0 -0
  18. .lake/build/ir/REPL/Lean/ContextInfo.c.o.hash +1 -0
  19. .lake/build/ir/REPL/Lean/ContextInfo.c.o.trace +1 -0
  20. .lake/build/ir/REPL/Lean/Environment.c +498 -0
  21. .lake/build/ir/REPL/Lean/Environment.c.hash +1 -0
  22. .lake/build/ir/REPL/Lean/Environment.c.o +0 -0
  23. .lake/build/ir/REPL/Lean/Environment.c.o.hash +1 -0
  24. .lake/build/ir/REPL/Lean/Environment.c.o.trace +1 -0
  25. .lake/build/ir/REPL/Lean/InfoTree.c +0 -0
  26. .lake/build/ir/REPL/Lean/InfoTree.c.hash +1 -0
  27. .lake/build/ir/REPL/Lean/InfoTree.c.o +0 -0
  28. .lake/build/ir/REPL/Lean/InfoTree.c.o.hash +1 -0
  29. .lake/build/ir/REPL/Lean/InfoTree.c.o.trace +1 -0
  30. .lake/build/ir/REPL/Lean/InfoTree/ToJson.c +0 -0
  31. .lake/build/ir/REPL/Lean/InfoTree/ToJson.c.hash +1 -0
  32. .lake/build/ir/REPL/Lean/InfoTree/ToJson.c.o +0 -0
  33. .lake/build/ir/REPL/Lean/InfoTree/ToJson.c.o.hash +1 -0
  34. .lake/build/ir/REPL/Lean/InfoTree/ToJson.c.o.trace +1 -0
  35. .lake/build/ir/REPL/Main.c +0 -0
  36. .lake/build/ir/REPL/Main.c.hash +1 -0
  37. .lake/build/ir/REPL/Main.c.o +0 -0
  38. .lake/build/ir/REPL/Main.c.o.hash +1 -0
  39. .lake/build/ir/REPL/Main.c.o.trace +1 -0
  40. .lake/build/ir/REPL/Snapshots.c +0 -0
  41. .lake/build/ir/REPL/Snapshots.c.hash +1 -0
  42. .lake/build/ir/REPL/Snapshots.c.o +0 -0
  43. .lake/build/ir/REPL/Snapshots.c.o.hash +1 -0
  44. .lake/build/ir/REPL/Snapshots.c.o.trace +1 -0
  45. .lake/build/ir/REPL/Util/Path.c +494 -0
  46. .lake/build/ir/REPL/Util/Path.c.hash +1 -0
  47. .lake/build/ir/REPL/Util/Path.c.o +0 -0
  48. .lake/build/ir/REPL/Util/Path.c.o.hash +1 -0
  49. .lake/build/ir/REPL/Util/Path.c.o.trace +1 -0
  50. .lake/build/ir/REPL/Util/Pickle.c +709 -0
.gitattributes CHANGED
@@ -74,3 +74,13 @@ compile_result/wild_test/lean4_random_15kpass5.jsonl filter=lfs diff=lfs merge=l
74
  data/updated_lean4_kv.json filter=lfs diff=lfs merge=lfs -text
75
  pass_rate_results/compile_result/lean4_basic_test/lean4_random_15kpass5.jsonl filter=lfs diff=lfs merge=lfs -text
76
  pass_rate_results/compile_result/lean4_random_test/lean4_random_15kpass5.jsonl filter=lfs diff=lfs merge=lfs -text
 
 
 
 
 
 
 
 
 
 
 
74
  data/updated_lean4_kv.json filter=lfs diff=lfs merge=lfs -text
75
  pass_rate_results/compile_result/lean4_basic_test/lean4_random_15kpass5.jsonl filter=lfs diff=lfs merge=lfs -text
76
  pass_rate_results/compile_result/lean4_random_test/lean4_random_15kpass5.jsonl filter=lfs diff=lfs merge=lfs -text
77
+ .lake/build/bin/repl filter=lfs diff=lfs merge=lfs -text
78
+ .lake/build/lib/REPL/JSON.olean filter=lfs diff=lfs merge=lfs -text
79
+ .lake/build/lib/REPL/Main.olean filter=lfs diff=lfs merge=lfs -text
80
+ .lake/packages/proofwidgets/.lake/build/lib/ProofWidgets/Component/InteractiveSvg.olean filter=lfs diff=lfs merge=lfs -text
81
+ .lake/packages/proofwidgets/.lake/build/lib/ProofWidgets/Component/PenroseDiagram.olean filter=lfs diff=lfs merge=lfs -text
82
+ .lake/packages/proofwidgets/.lake/build/lib/ProofWidgets/Component/Recharts.olean filter=lfs diff=lfs merge=lfs -text
83
+ .lake/packages/proofwidgets/.lake/build/lib/ProofWidgets/Data/Html.olean filter=lfs diff=lfs merge=lfs -text
84
+ .lake/packages/proofwidgets/.lake/build/lib/ProofWidgets/Data/Svg.olean filter=lfs diff=lfs merge=lfs -text
85
+ .lake/packages/proofwidgets/.lake/build/lib/ProofWidgets/Demos/Conv.olean filter=lfs diff=lfs merge=lfs -text
86
+ .lake/packages/proofwidgets/.lake/build/lib/ProofWidgets/Demos/RbTree.olean filter=lfs diff=lfs merge=lfs -text
.lake/build/bin/repl ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:f530364a5e1032f46ad6d18f42d85e24f0dec4db59c3a1c874d6bad47de21cf3
3
+ size 79965432
.lake/build/bin/repl.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 55802926989229838
.lake/build/bin/repl.trace ADDED
@@ -0,0 +1 @@
 
 
1
+ 8002134274837948266
.lake/build/ir/REPL/Frontend.c ADDED
@@ -0,0 +1,743 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Lean compiler output
2
+ // Module: REPL.Frontend
3
+ // Imports: Init Lean.Elab.Frontend
4
+ #include <lean/lean.h>
5
+ #if defined(__clang__)
6
+ #pragma clang diagnostic ignored "-Wunused-parameter"
7
+ #pragma clang diagnostic ignored "-Wunused-label"
8
+ #elif defined(__GNUC__) && !defined(__CLANG__)
9
+ #pragma GCC diagnostic ignored "-Wunused-parameter"
10
+ #pragma GCC diagnostic ignored "-Wunused-label"
11
+ #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
12
+ #endif
13
+ #ifdef __cplusplus
14
+ extern "C" {
15
+ #endif
16
+ static lean_object* l_Lean_Elab_IO_processCommandsWithInfoTrees___closed__1;
17
+ lean_object* l_Lean_Elab_Command_mkState(lean_object*, lean_object*, lean_object*);
18
+ lean_object* l_Lean_Elab_processHeader(lean_object*, lean_object*, lean_object*, lean_object*, uint32_t, uint8_t, lean_object*);
19
+ LEAN_EXPORT lean_object* l_Functor_mapRev___at_Lean_Elab_IO_processCommandsWithInfoTrees___spec__1___rarg(lean_object*, lean_object*, lean_object*);
20
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processInput_unsafe__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
21
+ lean_object* l_Lean_PersistentArray_toList___rarg(lean_object*);
22
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processCommandsWithInfoTrees___lambda__1(lean_object*);
23
+ lean_object* l_Lean_initSearchPath(lean_object*, lean_object*, lean_object*);
24
+ lean_object* l_Lean_findSysroot(lean_object*, lean_object*);
25
+ lean_object* lean_enable_initializer_execution(lean_object*);
26
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processInput_unsafe__1___lambda__1(lean_object*, lean_object*, lean_object*);
27
+ static lean_object* l_Lean_Elab_IO_processInput_unsafe__1___closed__2;
28
+ lean_object* l_Lean_Parser_mkInputContext(lean_object*, lean_object*);
29
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processCommandsWithInfoTrees(lean_object*, lean_object*, lean_object*, lean_object*);
30
+ lean_object* l_Lean_Elab_IO_processCommands(lean_object*, lean_object*, lean_object*, lean_object*);
31
+ static lean_object* l_Lean_Elab_IO_processInput_unsafe__1___closed__3;
32
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processCommandsWithInfoTrees___lambda__1___boxed(lean_object*);
33
+ LEAN_EXPORT lean_object* l_Functor_mapRev___at_Lean_Elab_IO_processCommandsWithInfoTrees___spec__1(lean_object*, lean_object*);
34
+ static lean_object* l_Lean_Elab_IO_processInput_unsafe__1___closed__1;
35
+ lean_object* l_Lean_Parser_parseHeader(lean_object*, lean_object*);
36
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processInput(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
37
+ LEAN_EXPORT lean_object* l_Functor_mapRev___at_Lean_Elab_IO_processCommandsWithInfoTrees___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
38
+ _start:
39
+ {
40
+ lean_object* x_4;
41
+ x_4 = lean_apply_1(x_1, x_3);
42
+ if (lean_obj_tag(x_4) == 0)
43
+ {
44
+ uint8_t x_5;
45
+ x_5 = !lean_is_exclusive(x_4);
46
+ if (x_5 == 0)
47
+ {
48
+ lean_object* x_6; lean_object* x_7;
49
+ x_6 = lean_ctor_get(x_4, 0);
50
+ x_7 = lean_apply_1(x_2, x_6);
51
+ lean_ctor_set(x_4, 0, x_7);
52
+ return x_4;
53
+ }
54
+ else
55
+ {
56
+ lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
57
+ x_8 = lean_ctor_get(x_4, 0);
58
+ x_9 = lean_ctor_get(x_4, 1);
59
+ lean_inc(x_9);
60
+ lean_inc(x_8);
61
+ lean_dec(x_4);
62
+ x_10 = lean_apply_1(x_2, x_8);
63
+ x_11 = lean_alloc_ctor(0, 2, 0);
64
+ lean_ctor_set(x_11, 0, x_10);
65
+ lean_ctor_set(x_11, 1, x_9);
66
+ return x_11;
67
+ }
68
+ }
69
+ else
70
+ {
71
+ uint8_t x_12;
72
+ lean_dec(x_2);
73
+ x_12 = !lean_is_exclusive(x_4);
74
+ if (x_12 == 0)
75
+ {
76
+ return x_4;
77
+ }
78
+ else
79
+ {
80
+ lean_object* x_13; lean_object* x_14; lean_object* x_15;
81
+ x_13 = lean_ctor_get(x_4, 0);
82
+ x_14 = lean_ctor_get(x_4, 1);
83
+ lean_inc(x_14);
84
+ lean_inc(x_13);
85
+ lean_dec(x_4);
86
+ x_15 = lean_alloc_ctor(1, 2, 0);
87
+ lean_ctor_set(x_15, 0, x_13);
88
+ lean_ctor_set(x_15, 1, x_14);
89
+ return x_15;
90
+ }
91
+ }
92
+ }
93
+ }
94
+ LEAN_EXPORT lean_object* l_Functor_mapRev___at_Lean_Elab_IO_processCommandsWithInfoTrees___spec__1(lean_object* x_1, lean_object* x_2) {
95
+ _start:
96
+ {
97
+ lean_object* x_3;
98
+ x_3 = lean_alloc_closure((void*)(l_Functor_mapRev___at_Lean_Elab_IO_processCommandsWithInfoTrees___spec__1___rarg), 3, 0);
99
+ return x_3;
100
+ }
101
+ }
102
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processCommandsWithInfoTrees___lambda__1(lean_object* x_1) {
103
+ _start:
104
+ {
105
+ lean_object* x_2;
106
+ x_2 = lean_ctor_get(x_1, 0);
107
+ lean_inc(x_2);
108
+ return x_2;
109
+ }
110
+ }
111
+ static lean_object* _init_l_Lean_Elab_IO_processCommandsWithInfoTrees___closed__1() {
112
+ _start:
113
+ {
114
+ lean_object* x_1;
115
+ x_1 = lean_alloc_closure((void*)(l_Lean_Elab_IO_processCommandsWithInfoTrees___lambda__1___boxed), 1, 0);
116
+ return x_1;
117
+ }
118
+ }
119
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processCommandsWithInfoTrees(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
120
+ _start:
121
+ {
122
+ uint8_t x_5;
123
+ x_5 = !lean_is_exclusive(x_3);
124
+ if (x_5 == 0)
125
+ {
126
+ lean_object* x_6; uint8_t x_7;
127
+ x_6 = lean_ctor_get(x_3, 7);
128
+ x_7 = !lean_is_exclusive(x_6);
129
+ if (x_7 == 0)
130
+ {
131
+ uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
132
+ x_8 = 1;
133
+ lean_ctor_set_uint8(x_6, sizeof(void*)*2, x_8);
134
+ x_9 = lean_alloc_closure((void*)(l_Lean_Elab_IO_processCommands), 4, 3);
135
+ lean_closure_set(x_9, 0, x_1);
136
+ lean_closure_set(x_9, 1, x_2);
137
+ lean_closure_set(x_9, 2, x_3);
138
+ x_10 = l_Lean_Elab_IO_processCommandsWithInfoTrees___closed__1;
139
+ x_11 = l_Functor_mapRev___at_Lean_Elab_IO_processCommandsWithInfoTrees___spec__1___rarg(x_9, x_10, x_4);
140
+ if (lean_obj_tag(x_11) == 0)
141
+ {
142
+ uint8_t x_12;
143
+ x_12 = !lean_is_exclusive(x_11);
144
+ if (x_12 == 0)
145
+ {
146
+ lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
147
+ x_13 = lean_ctor_get(x_11, 0);
148
+ x_14 = lean_ctor_get(x_13, 1);
149
+ lean_inc(x_14);
150
+ x_15 = l_Lean_PersistentArray_toList___rarg(x_14);
151
+ x_16 = lean_ctor_get(x_13, 7);
152
+ lean_inc(x_16);
153
+ x_17 = lean_ctor_get(x_16, 1);
154
+ lean_inc(x_17);
155
+ lean_dec(x_16);
156
+ x_18 = l_Lean_PersistentArray_toList___rarg(x_17);
157
+ x_19 = lean_alloc_ctor(0, 2, 0);
158
+ lean_ctor_set(x_19, 0, x_15);
159
+ lean_ctor_set(x_19, 1, x_18);
160
+ x_20 = lean_alloc_ctor(0, 2, 0);
161
+ lean_ctor_set(x_20, 0, x_13);
162
+ lean_ctor_set(x_20, 1, x_19);
163
+ lean_ctor_set(x_11, 0, x_20);
164
+ return x_11;
165
+ }
166
+ else
167
+ {
168
+ lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
169
+ x_21 = lean_ctor_get(x_11, 0);
170
+ x_22 = lean_ctor_get(x_11, 1);
171
+ lean_inc(x_22);
172
+ lean_inc(x_21);
173
+ lean_dec(x_11);
174
+ x_23 = lean_ctor_get(x_21, 1);
175
+ lean_inc(x_23);
176
+ x_24 = l_Lean_PersistentArray_toList___rarg(x_23);
177
+ x_25 = lean_ctor_get(x_21, 7);
178
+ lean_inc(x_25);
179
+ x_26 = lean_ctor_get(x_25, 1);
180
+ lean_inc(x_26);
181
+ lean_dec(x_25);
182
+ x_27 = l_Lean_PersistentArray_toList___rarg(x_26);
183
+ x_28 = lean_alloc_ctor(0, 2, 0);
184
+ lean_ctor_set(x_28, 0, x_24);
185
+ lean_ctor_set(x_28, 1, x_27);
186
+ x_29 = lean_alloc_ctor(0, 2, 0);
187
+ lean_ctor_set(x_29, 0, x_21);
188
+ lean_ctor_set(x_29, 1, x_28);
189
+ x_30 = lean_alloc_ctor(0, 2, 0);
190
+ lean_ctor_set(x_30, 0, x_29);
191
+ lean_ctor_set(x_30, 1, x_22);
192
+ return x_30;
193
+ }
194
+ }
195
+ else
196
+ {
197
+ uint8_t x_31;
198
+ x_31 = !lean_is_exclusive(x_11);
199
+ if (x_31 == 0)
200
+ {
201
+ return x_11;
202
+ }
203
+ else
204
+ {
205
+ lean_object* x_32; lean_object* x_33; lean_object* x_34;
206
+ x_32 = lean_ctor_get(x_11, 0);
207
+ x_33 = lean_ctor_get(x_11, 1);
208
+ lean_inc(x_33);
209
+ lean_inc(x_32);
210
+ lean_dec(x_11);
211
+ x_34 = lean_alloc_ctor(1, 2, 0);
212
+ lean_ctor_set(x_34, 0, x_32);
213
+ lean_ctor_set(x_34, 1, x_33);
214
+ return x_34;
215
+ }
216
+ }
217
+ }
218
+ else
219
+ {
220
+ lean_object* x_35; lean_object* x_36; uint8_t x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
221
+ x_35 = lean_ctor_get(x_6, 0);
222
+ x_36 = lean_ctor_get(x_6, 1);
223
+ lean_inc(x_36);
224
+ lean_inc(x_35);
225
+ lean_dec(x_6);
226
+ x_37 = 1;
227
+ x_38 = lean_alloc_ctor(0, 2, 1);
228
+ lean_ctor_set(x_38, 0, x_35);
229
+ lean_ctor_set(x_38, 1, x_36);
230
+ lean_ctor_set_uint8(x_38, sizeof(void*)*2, x_37);
231
+ lean_ctor_set(x_3, 7, x_38);
232
+ x_39 = lean_alloc_closure((void*)(l_Lean_Elab_IO_processCommands), 4, 3);
233
+ lean_closure_set(x_39, 0, x_1);
234
+ lean_closure_set(x_39, 1, x_2);
235
+ lean_closure_set(x_39, 2, x_3);
236
+ x_40 = l_Lean_Elab_IO_processCommandsWithInfoTrees___closed__1;
237
+ x_41 = l_Functor_mapRev___at_Lean_Elab_IO_processCommandsWithInfoTrees___spec__1___rarg(x_39, x_40, x_4);
238
+ if (lean_obj_tag(x_41) == 0)
239
+ {
240
+ lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52;
241
+ x_42 = lean_ctor_get(x_41, 0);
242
+ lean_inc(x_42);
243
+ x_43 = lean_ctor_get(x_41, 1);
244
+ lean_inc(x_43);
245
+ if (lean_is_exclusive(x_41)) {
246
+ lean_ctor_release(x_41, 0);
247
+ lean_ctor_release(x_41, 1);
248
+ x_44 = x_41;
249
+ } else {
250
+ lean_dec_ref(x_41);
251
+ x_44 = lean_box(0);
252
+ }
253
+ x_45 = lean_ctor_get(x_42, 1);
254
+ lean_inc(x_45);
255
+ x_46 = l_Lean_PersistentArray_toList___rarg(x_45);
256
+ x_47 = lean_ctor_get(x_42, 7);
257
+ lean_inc(x_47);
258
+ x_48 = lean_ctor_get(x_47, 1);
259
+ lean_inc(x_48);
260
+ lean_dec(x_47);
261
+ x_49 = l_Lean_PersistentArray_toList___rarg(x_48);
262
+ x_50 = lean_alloc_ctor(0, 2, 0);
263
+ lean_ctor_set(x_50, 0, x_46);
264
+ lean_ctor_set(x_50, 1, x_49);
265
+ x_51 = lean_alloc_ctor(0, 2, 0);
266
+ lean_ctor_set(x_51, 0, x_42);
267
+ lean_ctor_set(x_51, 1, x_50);
268
+ if (lean_is_scalar(x_44)) {
269
+ x_52 = lean_alloc_ctor(0, 2, 0);
270
+ } else {
271
+ x_52 = x_44;
272
+ }
273
+ lean_ctor_set(x_52, 0, x_51);
274
+ lean_ctor_set(x_52, 1, x_43);
275
+ return x_52;
276
+ }
277
+ else
278
+ {
279
+ lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56;
280
+ x_53 = lean_ctor_get(x_41, 0);
281
+ lean_inc(x_53);
282
+ x_54 = lean_ctor_get(x_41, 1);
283
+ lean_inc(x_54);
284
+ if (lean_is_exclusive(x_41)) {
285
+ lean_ctor_release(x_41, 0);
286
+ lean_ctor_release(x_41, 1);
287
+ x_55 = x_41;
288
+ } else {
289
+ lean_dec_ref(x_41);
290
+ x_55 = lean_box(0);
291
+ }
292
+ if (lean_is_scalar(x_55)) {
293
+ x_56 = lean_alloc_ctor(1, 2, 0);
294
+ } else {
295
+ x_56 = x_55;
296
+ }
297
+ lean_ctor_set(x_56, 0, x_53);
298
+ lean_ctor_set(x_56, 1, x_54);
299
+ return x_56;
300
+ }
301
+ }
302
+ }
303
+ else
304
+ {
305
+ lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; uint8_t x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74;
306
+ x_57 = lean_ctor_get(x_3, 7);
307
+ x_58 = lean_ctor_get(x_3, 0);
308
+ x_59 = lean_ctor_get(x_3, 1);
309
+ x_60 = lean_ctor_get(x_3, 2);
310
+ x_61 = lean_ctor_get(x_3, 3);
311
+ x_62 = lean_ctor_get(x_3, 4);
312
+ x_63 = lean_ctor_get(x_3, 5);
313
+ x_64 = lean_ctor_get(x_3, 6);
314
+ x_65 = lean_ctor_get(x_3, 8);
315
+ lean_inc(x_65);
316
+ lean_inc(x_57);
317
+ lean_inc(x_64);
318
+ lean_inc(x_63);
319
+ lean_inc(x_62);
320
+ lean_inc(x_61);
321
+ lean_inc(x_60);
322
+ lean_inc(x_59);
323
+ lean_inc(x_58);
324
+ lean_dec(x_3);
325
+ x_66 = lean_ctor_get(x_57, 0);
326
+ lean_inc(x_66);
327
+ x_67 = lean_ctor_get(x_57, 1);
328
+ lean_inc(x_67);
329
+ if (lean_is_exclusive(x_57)) {
330
+ lean_ctor_release(x_57, 0);
331
+ lean_ctor_release(x_57, 1);
332
+ x_68 = x_57;
333
+ } else {
334
+ lean_dec_ref(x_57);
335
+ x_68 = lean_box(0);
336
+ }
337
+ x_69 = 1;
338
+ if (lean_is_scalar(x_68)) {
339
+ x_70 = lean_alloc_ctor(0, 2, 1);
340
+ } else {
341
+ x_70 = x_68;
342
+ }
343
+ lean_ctor_set(x_70, 0, x_66);
344
+ lean_ctor_set(x_70, 1, x_67);
345
+ lean_ctor_set_uint8(x_70, sizeof(void*)*2, x_69);
346
+ x_71 = lean_alloc_ctor(0, 9, 0);
347
+ lean_ctor_set(x_71, 0, x_58);
348
+ lean_ctor_set(x_71, 1, x_59);
349
+ lean_ctor_set(x_71, 2, x_60);
350
+ lean_ctor_set(x_71, 3, x_61);
351
+ lean_ctor_set(x_71, 4, x_62);
352
+ lean_ctor_set(x_71, 5, x_63);
353
+ lean_ctor_set(x_71, 6, x_64);
354
+ lean_ctor_set(x_71, 7, x_70);
355
+ lean_ctor_set(x_71, 8, x_65);
356
+ x_72 = lean_alloc_closure((void*)(l_Lean_Elab_IO_processCommands), 4, 3);
357
+ lean_closure_set(x_72, 0, x_1);
358
+ lean_closure_set(x_72, 1, x_2);
359
+ lean_closure_set(x_72, 2, x_71);
360
+ x_73 = l_Lean_Elab_IO_processCommandsWithInfoTrees___closed__1;
361
+ x_74 = l_Functor_mapRev___at_Lean_Elab_IO_processCommandsWithInfoTrees___spec__1___rarg(x_72, x_73, x_4);
362
+ if (lean_obj_tag(x_74) == 0)
363
+ {
364
+ lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85;
365
+ x_75 = lean_ctor_get(x_74, 0);
366
+ lean_inc(x_75);
367
+ x_76 = lean_ctor_get(x_74, 1);
368
+ lean_inc(x_76);
369
+ if (lean_is_exclusive(x_74)) {
370
+ lean_ctor_release(x_74, 0);
371
+ lean_ctor_release(x_74, 1);
372
+ x_77 = x_74;
373
+ } else {
374
+ lean_dec_ref(x_74);
375
+ x_77 = lean_box(0);
376
+ }
377
+ x_78 = lean_ctor_get(x_75, 1);
378
+ lean_inc(x_78);
379
+ x_79 = l_Lean_PersistentArray_toList___rarg(x_78);
380
+ x_80 = lean_ctor_get(x_75, 7);
381
+ lean_inc(x_80);
382
+ x_81 = lean_ctor_get(x_80, 1);
383
+ lean_inc(x_81);
384
+ lean_dec(x_80);
385
+ x_82 = l_Lean_PersistentArray_toList___rarg(x_81);
386
+ x_83 = lean_alloc_ctor(0, 2, 0);
387
+ lean_ctor_set(x_83, 0, x_79);
388
+ lean_ctor_set(x_83, 1, x_82);
389
+ x_84 = lean_alloc_ctor(0, 2, 0);
390
+ lean_ctor_set(x_84, 0, x_75);
391
+ lean_ctor_set(x_84, 1, x_83);
392
+ if (lean_is_scalar(x_77)) {
393
+ x_85 = lean_alloc_ctor(0, 2, 0);
394
+ } else {
395
+ x_85 = x_77;
396
+ }
397
+ lean_ctor_set(x_85, 0, x_84);
398
+ lean_ctor_set(x_85, 1, x_76);
399
+ return x_85;
400
+ }
401
+ else
402
+ {
403
+ lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89;
404
+ x_86 = lean_ctor_get(x_74, 0);
405
+ lean_inc(x_86);
406
+ x_87 = lean_ctor_get(x_74, 1);
407
+ lean_inc(x_87);
408
+ if (lean_is_exclusive(x_74)) {
409
+ lean_ctor_release(x_74, 0);
410
+ lean_ctor_release(x_74, 1);
411
+ x_88 = x_74;
412
+ } else {
413
+ lean_dec_ref(x_74);
414
+ x_88 = lean_box(0);
415
+ }
416
+ if (lean_is_scalar(x_88)) {
417
+ x_89 = lean_alloc_ctor(1, 2, 0);
418
+ } else {
419
+ x_89 = x_88;
420
+ }
421
+ lean_ctor_set(x_89, 0, x_86);
422
+ lean_ctor_set(x_89, 1, x_87);
423
+ return x_89;
424
+ }
425
+ }
426
+ }
427
+ }
428
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processCommandsWithInfoTrees___lambda__1___boxed(lean_object* x_1) {
429
+ _start:
430
+ {
431
+ lean_object* x_2;
432
+ x_2 = l_Lean_Elab_IO_processCommandsWithInfoTrees___lambda__1(x_1);
433
+ lean_dec(x_1);
434
+ return x_2;
435
+ }
436
+ }
437
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processInput_unsafe__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
438
+ _start:
439
+ {
440
+ lean_object* x_4; lean_object* x_5; lean_object* x_6;
441
+ x_4 = lean_ctor_get(x_2, 0);
442
+ lean_inc(x_4);
443
+ x_5 = lean_ctor_get(x_2, 1);
444
+ lean_inc(x_5);
445
+ lean_dec(x_2);
446
+ x_6 = l_Lean_Elab_IO_processCommandsWithInfoTrees(x_1, x_4, x_5, x_3);
447
+ return x_6;
448
+ }
449
+ }
450
+ static lean_object* _init_l_Lean_Elab_IO_processInput_unsafe__1___closed__1() {
451
+ _start:
452
+ {
453
+ lean_object* x_1;
454
+ x_1 = lean_mk_string_from_bytes("lean", 4);
455
+ return x_1;
456
+ }
457
+ }
458
+ static lean_object* _init_l_Lean_Elab_IO_processInput_unsafe__1___closed__2() {
459
+ _start:
460
+ {
461
+ lean_object* x_1; uint8_t x_2; lean_object* x_3;
462
+ x_1 = lean_unsigned_to_nat(0u);
463
+ x_2 = 0;
464
+ x_3 = lean_alloc_ctor(0, 1, 1);
465
+ lean_ctor_set(x_3, 0, x_1);
466
+ lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
467
+ return x_3;
468
+ }
469
+ }
470
+ static lean_object* _init_l_Lean_Elab_IO_processInput_unsafe__1___closed__3() {
471
+ _start:
472
+ {
473
+ lean_object* x_1;
474
+ x_1 = lean_mk_string_from_bytes("<input>", 7);
475
+ return x_1;
476
+ }
477
+ }
478
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processInput_unsafe__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
479
+ _start:
480
+ {
481
+ lean_object* x_6; lean_object* x_7;
482
+ x_6 = l_Lean_Elab_IO_processInput_unsafe__1___closed__1;
483
+ x_7 = l_Lean_findSysroot(x_6, x_5);
484
+ if (lean_obj_tag(x_7) == 0)
485
+ {
486
+ lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
487
+ x_8 = lean_ctor_get(x_7, 0);
488
+ lean_inc(x_8);
489
+ x_9 = lean_ctor_get(x_7, 1);
490
+ lean_inc(x_9);
491
+ lean_dec(x_7);
492
+ x_10 = lean_box(0);
493
+ x_11 = l_Lean_initSearchPath(x_8, x_10, x_9);
494
+ if (lean_obj_tag(x_11) == 0)
495
+ {
496
+ lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
497
+ x_12 = lean_ctor_get(x_11, 1);
498
+ lean_inc(x_12);
499
+ lean_dec(x_11);
500
+ x_13 = lean_enable_initializer_execution(x_12);
501
+ x_14 = lean_ctor_get(x_13, 1);
502
+ lean_inc(x_14);
503
+ lean_dec(x_13);
504
+ if (lean_obj_tag(x_4) == 0)
505
+ {
506
+ lean_object* x_52;
507
+ x_52 = l_Lean_Elab_IO_processInput_unsafe__1___closed__3;
508
+ x_15 = x_52;
509
+ goto block_51;
510
+ }
511
+ else
512
+ {
513
+ lean_object* x_53;
514
+ x_53 = lean_ctor_get(x_4, 0);
515
+ lean_inc(x_53);
516
+ lean_dec(x_4);
517
+ x_15 = x_53;
518
+ goto block_51;
519
+ }
520
+ block_51:
521
+ {
522
+ lean_object* x_16;
523
+ x_16 = l_Lean_Parser_mkInputContext(x_1, x_15);
524
+ if (lean_obj_tag(x_2) == 0)
525
+ {
526
+ lean_object* x_17;
527
+ lean_inc(x_16);
528
+ x_17 = l_Lean_Parser_parseHeader(x_16, x_14);
529
+ if (lean_obj_tag(x_17) == 0)
530
+ {
531
+ lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint32_t x_24; uint8_t x_25; lean_object* x_26;
532
+ x_18 = lean_ctor_get(x_17, 0);
533
+ lean_inc(x_18);
534
+ x_19 = lean_ctor_get(x_18, 1);
535
+ lean_inc(x_19);
536
+ x_20 = lean_ctor_get(x_17, 1);
537
+ lean_inc(x_20);
538
+ lean_dec(x_17);
539
+ x_21 = lean_ctor_get(x_18, 0);
540
+ lean_inc(x_21);
541
+ lean_dec(x_18);
542
+ x_22 = lean_ctor_get(x_19, 0);
543
+ lean_inc(x_22);
544
+ x_23 = lean_ctor_get(x_19, 1);
545
+ lean_inc(x_23);
546
+ lean_dec(x_19);
547
+ x_24 = 0;
548
+ x_25 = 0;
549
+ lean_inc(x_3);
550
+ x_26 = l_Lean_Elab_processHeader(x_21, x_3, x_23, x_16, x_24, x_25, x_20);
551
+ lean_dec(x_21);
552
+ if (lean_obj_tag(x_26) == 0)
553
+ {
554
+ lean_object* x_27; lean_object* x_28; uint8_t x_29;
555
+ x_27 = lean_ctor_get(x_26, 0);
556
+ lean_inc(x_27);
557
+ x_28 = lean_ctor_get(x_26, 1);
558
+ lean_inc(x_28);
559
+ lean_dec(x_26);
560
+ x_29 = !lean_is_exclusive(x_27);
561
+ if (x_29 == 0)
562
+ {
563
+ lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
564
+ x_30 = lean_ctor_get(x_27, 0);
565
+ x_31 = lean_ctor_get(x_27, 1);
566
+ x_32 = l_Lean_Elab_Command_mkState(x_30, x_31, x_3);
567
+ lean_ctor_set(x_27, 1, x_32);
568
+ lean_ctor_set(x_27, 0, x_22);
569
+ x_33 = l_Lean_Elab_IO_processInput_unsafe__1___lambda__1(x_16, x_27, x_28);
570
+ return x_33;
571
+ }
572
+ else
573
+ {
574
+ lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
575
+ x_34 = lean_ctor_get(x_27, 0);
576
+ x_35 = lean_ctor_get(x_27, 1);
577
+ lean_inc(x_35);
578
+ lean_inc(x_34);
579
+ lean_dec(x_27);
580
+ x_36 = l_Lean_Elab_Command_mkState(x_34, x_35, x_3);
581
+ x_37 = lean_alloc_ctor(0, 2, 0);
582
+ lean_ctor_set(x_37, 0, x_22);
583
+ lean_ctor_set(x_37, 1, x_36);
584
+ x_38 = l_Lean_Elab_IO_processInput_unsafe__1___lambda__1(x_16, x_37, x_28);
585
+ return x_38;
586
+ }
587
+ }
588
+ else
589
+ {
590
+ uint8_t x_39;
591
+ lean_dec(x_22);
592
+ lean_dec(x_16);
593
+ lean_dec(x_3);
594
+ x_39 = !lean_is_exclusive(x_26);
595
+ if (x_39 == 0)
596
+ {
597
+ return x_26;
598
+ }
599
+ else
600
+ {
601
+ lean_object* x_40; lean_object* x_41; lean_object* x_42;
602
+ x_40 = lean_ctor_get(x_26, 0);
603
+ x_41 = lean_ctor_get(x_26, 1);
604
+ lean_inc(x_41);
605
+ lean_inc(x_40);
606
+ lean_dec(x_26);
607
+ x_42 = lean_alloc_ctor(1, 2, 0);
608
+ lean_ctor_set(x_42, 0, x_40);
609
+ lean_ctor_set(x_42, 1, x_41);
610
+ return x_42;
611
+ }
612
+ }
613
+ }
614
+ else
615
+ {
616
+ uint8_t x_43;
617
+ lean_dec(x_16);
618
+ lean_dec(x_3);
619
+ x_43 = !lean_is_exclusive(x_17);
620
+ if (x_43 == 0)
621
+ {
622
+ return x_17;
623
+ }
624
+ else
625
+ {
626
+ lean_object* x_44; lean_object* x_45; lean_object* x_46;
627
+ x_44 = lean_ctor_get(x_17, 0);
628
+ x_45 = lean_ctor_get(x_17, 1);
629
+ lean_inc(x_45);
630
+ lean_inc(x_44);
631
+ lean_dec(x_17);
632
+ x_46 = lean_alloc_ctor(1, 2, 0);
633
+ lean_ctor_set(x_46, 0, x_44);
634
+ lean_ctor_set(x_46, 1, x_45);
635
+ return x_46;
636
+ }
637
+ }
638
+ }
639
+ else
640
+ {
641
+ lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50;
642
+ lean_dec(x_3);
643
+ x_47 = lean_ctor_get(x_2, 0);
644
+ lean_inc(x_47);
645
+ lean_dec(x_2);
646
+ x_48 = l_Lean_Elab_IO_processInput_unsafe__1___closed__2;
647
+ x_49 = lean_alloc_ctor(0, 2, 0);
648
+ lean_ctor_set(x_49, 0, x_48);
649
+ lean_ctor_set(x_49, 1, x_47);
650
+ x_50 = l_Lean_Elab_IO_processInput_unsafe__1___lambda__1(x_16, x_49, x_14);
651
+ return x_50;
652
+ }
653
+ }
654
+ }
655
+ else
656
+ {
657
+ uint8_t x_54;
658
+ lean_dec(x_4);
659
+ lean_dec(x_3);
660
+ lean_dec(x_2);
661
+ lean_dec(x_1);
662
+ x_54 = !lean_is_exclusive(x_11);
663
+ if (x_54 == 0)
664
+ {
665
+ return x_11;
666
+ }
667
+ else
668
+ {
669
+ lean_object* x_55; lean_object* x_56; lean_object* x_57;
670
+ x_55 = lean_ctor_get(x_11, 0);
671
+ x_56 = lean_ctor_get(x_11, 1);
672
+ lean_inc(x_56);
673
+ lean_inc(x_55);
674
+ lean_dec(x_11);
675
+ x_57 = lean_alloc_ctor(1, 2, 0);
676
+ lean_ctor_set(x_57, 0, x_55);
677
+ lean_ctor_set(x_57, 1, x_56);
678
+ return x_57;
679
+ }
680
+ }
681
+ }
682
+ else
683
+ {
684
+ uint8_t x_58;
685
+ lean_dec(x_4);
686
+ lean_dec(x_3);
687
+ lean_dec(x_2);
688
+ lean_dec(x_1);
689
+ x_58 = !lean_is_exclusive(x_7);
690
+ if (x_58 == 0)
691
+ {
692
+ return x_7;
693
+ }
694
+ else
695
+ {
696
+ lean_object* x_59; lean_object* x_60; lean_object* x_61;
697
+ x_59 = lean_ctor_get(x_7, 0);
698
+ x_60 = lean_ctor_get(x_7, 1);
699
+ lean_inc(x_60);
700
+ lean_inc(x_59);
701
+ lean_dec(x_7);
702
+ x_61 = lean_alloc_ctor(1, 2, 0);
703
+ lean_ctor_set(x_61, 0, x_59);
704
+ lean_ctor_set(x_61, 1, x_60);
705
+ return x_61;
706
+ }
707
+ }
708
+ }
709
+ }
710
+ LEAN_EXPORT lean_object* l_Lean_Elab_IO_processInput(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
711
+ _start:
712
+ {
713
+ lean_object* x_6;
714
+ x_6 = l_Lean_Elab_IO_processInput_unsafe__1(x_1, x_2, x_3, x_4, x_5);
715
+ return x_6;
716
+ }
717
+ }
718
+ lean_object* initialize_Init(uint8_t builtin, lean_object*);
719
+ lean_object* initialize_Lean_Elab_Frontend(uint8_t builtin, lean_object*);
720
+ static bool _G_initialized = false;
721
+ LEAN_EXPORT lean_object* initialize_REPL_Frontend(uint8_t builtin, lean_object* w) {
722
+ lean_object * res;
723
+ if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
724
+ _G_initialized = true;
725
+ res = initialize_Init(builtin, lean_io_mk_world());
726
+ if (lean_io_result_is_error(res)) return res;
727
+ lean_dec_ref(res);
728
+ res = initialize_Lean_Elab_Frontend(builtin, lean_io_mk_world());
729
+ if (lean_io_result_is_error(res)) return res;
730
+ lean_dec_ref(res);
731
+ l_Lean_Elab_IO_processCommandsWithInfoTrees___closed__1 = _init_l_Lean_Elab_IO_processCommandsWithInfoTrees___closed__1();
732
+ lean_mark_persistent(l_Lean_Elab_IO_processCommandsWithInfoTrees___closed__1);
733
+ l_Lean_Elab_IO_processInput_unsafe__1___closed__1 = _init_l_Lean_Elab_IO_processInput_unsafe__1___closed__1();
734
+ lean_mark_persistent(l_Lean_Elab_IO_processInput_unsafe__1___closed__1);
735
+ l_Lean_Elab_IO_processInput_unsafe__1___closed__2 = _init_l_Lean_Elab_IO_processInput_unsafe__1___closed__2();
736
+ lean_mark_persistent(l_Lean_Elab_IO_processInput_unsafe__1___closed__2);
737
+ l_Lean_Elab_IO_processInput_unsafe__1___closed__3 = _init_l_Lean_Elab_IO_processInput_unsafe__1___closed__3();
738
+ lean_mark_persistent(l_Lean_Elab_IO_processInput_unsafe__1___closed__3);
739
+ return lean_io_result_mk_ok(lean_box(0));
740
+ }
741
+ #ifdef __cplusplus
742
+ }
743
+ #endif
.lake/build/ir/REPL/Frontend.c.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 139939702429269950
.lake/build/ir/REPL/Frontend.c.o ADDED
Binary file (16 kB). View file
 
.lake/build/ir/REPL/Frontend.c.o.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 1643467189858040856
.lake/build/ir/REPL/Frontend.c.o.trace ADDED
@@ -0,0 +1 @@
 
 
1
+ 5185828946200883428
.lake/build/ir/REPL/JSON.c ADDED
The diff for this file is too large to render. See raw diff
 
.lake/build/ir/REPL/JSON.c.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 15401370983323712534
.lake/build/ir/REPL/JSON.c.o ADDED
Binary file (199 kB). View file
 
.lake/build/ir/REPL/JSON.c.o.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 14128581864194759368
.lake/build/ir/REPL/JSON.c.o.trace ADDED
@@ -0,0 +1 @@
 
 
1
+ 1270579146660084140
.lake/build/ir/REPL/Lean/ContextInfo.c ADDED
@@ -0,0 +1,85 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Lean compiler output
2
+ // Module: REPL.Lean.ContextInfo
3
+ // Imports: Init Lean
4
+ #include <lean/lean.h>
5
+ #if defined(__clang__)
6
+ #pragma clang diagnostic ignored "-Wunused-parameter"
7
+ #pragma clang diagnostic ignored "-Wunused-label"
8
+ #elif defined(__GNUC__) && !defined(__CLANG__)
9
+ #pragma GCC diagnostic ignored "-Wunused-parameter"
10
+ #pragma GCC diagnostic ignored "-Wunused-label"
11
+ #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
12
+ #endif
13
+ #ifdef __cplusplus
14
+ extern "C" {
15
+ #endif
16
+ lean_object* l_Lean_Meta_ppExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
17
+ LEAN_EXPORT lean_object* l_Lean_Elab_ContextInfo_ppExpr___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
18
+ LEAN_EXPORT lean_object* l_Lean_Elab_ContextInfo_ppExpr(lean_object*, lean_object*, lean_object*, lean_object*);
19
+ lean_object* l_Lean_instantiateMVars___at___private_Lean_Meta_Basic_0__Lean_Meta_isClassApp_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
20
+ LEAN_EXPORT lean_object* l_Lean_Elab_ContextInfo_ppExpr___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
21
+ lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
22
+ LEAN_EXPORT lean_object* l_Lean_Elab_ContextInfo_ppExpr___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
23
+ LEAN_EXPORT lean_object* l_Lean_Elab_ContextInfo_ppExpr___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
24
+ _start:
25
+ {
26
+ lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
27
+ x_7 = l_Lean_instantiateMVars___at___private_Lean_Meta_Basic_0__Lean_Meta_isClassApp_x3f___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
28
+ x_8 = lean_ctor_get(x_7, 0);
29
+ lean_inc(x_8);
30
+ x_9 = lean_ctor_get(x_7, 1);
31
+ lean_inc(x_9);
32
+ lean_dec(x_7);
33
+ x_10 = l_Lean_Meta_ppExpr(x_8, x_2, x_3, x_4, x_5, x_9);
34
+ return x_10;
35
+ }
36
+ }
37
+ LEAN_EXPORT lean_object* l_Lean_Elab_ContextInfo_ppExpr(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
38
+ _start:
39
+ {
40
+ lean_object* x_5; lean_object* x_6;
41
+ x_5 = lean_alloc_closure((void*)(l_Lean_Elab_ContextInfo_ppExpr___lambda__1___boxed), 6, 1);
42
+ lean_closure_set(x_5, 0, x_3);
43
+ x_6 = l_Lean_Elab_ContextInfo_runMetaM___rarg(x_1, x_2, x_5, x_4);
44
+ return x_6;
45
+ }
46
+ }
47
+ LEAN_EXPORT lean_object* l_Lean_Elab_ContextInfo_ppExpr___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
48
+ _start:
49
+ {
50
+ lean_object* x_7;
51
+ x_7 = l_Lean_Elab_ContextInfo_ppExpr___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
52
+ lean_dec(x_5);
53
+ lean_dec(x_4);
54
+ lean_dec(x_3);
55
+ lean_dec(x_2);
56
+ return x_7;
57
+ }
58
+ }
59
+ LEAN_EXPORT lean_object* l_Lean_Elab_ContextInfo_ppExpr___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
60
+ _start:
61
+ {
62
+ lean_object* x_5;
63
+ x_5 = l_Lean_Elab_ContextInfo_ppExpr(x_1, x_2, x_3, x_4);
64
+ lean_dec(x_1);
65
+ return x_5;
66
+ }
67
+ }
68
+ lean_object* initialize_Init(uint8_t builtin, lean_object*);
69
+ lean_object* initialize_Lean(uint8_t builtin, lean_object*);
70
+ static bool _G_initialized = false;
71
+ LEAN_EXPORT lean_object* initialize_REPL_Lean_ContextInfo(uint8_t builtin, lean_object* w) {
72
+ lean_object * res;
73
+ if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
74
+ _G_initialized = true;
75
+ res = initialize_Init(builtin, lean_io_mk_world());
76
+ if (lean_io_result_is_error(res)) return res;
77
+ lean_dec_ref(res);
78
+ res = initialize_Lean(builtin, lean_io_mk_world());
79
+ if (lean_io_result_is_error(res)) return res;
80
+ lean_dec_ref(res);
81
+ return lean_io_result_mk_ok(lean_box(0));
82
+ }
83
+ #ifdef __cplusplus
84
+ }
85
+ #endif
.lake/build/ir/REPL/Lean/ContextInfo.c.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 12429617970449745360
.lake/build/ir/REPL/Lean/ContextInfo.c.o ADDED
Binary file (3.66 kB). View file
 
.lake/build/ir/REPL/Lean/ContextInfo.c.o.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 4759976862977137146
.lake/build/ir/REPL/Lean/ContextInfo.c.o.trace ADDED
@@ -0,0 +1 @@
 
 
1
+ 6289274348988205506
.lake/build/ir/REPL/Lean/Environment.c ADDED
@@ -0,0 +1,498 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Lean compiler output
2
+ // Module: REPL.Lean.Environment
3
+ // Imports: Init REPL.Util.Pickle Lean.Replay
4
+ #include <lean/lean.h>
5
+ #if defined(__clang__)
6
+ #pragma clang diagnostic ignored "-Wunused-parameter"
7
+ #pragma clang diagnostic ignored "-Wunused-label"
8
+ #elif defined(__GNUC__) && !defined(__CLANG__)
9
+ #pragma GCC diagnostic ignored "-Wunused-parameter"
10
+ #pragma GCC diagnostic ignored "-Wunused-label"
11
+ #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
12
+ #endif
13
+ #ifdef __cplusplus
14
+ extern "C" {
15
+ #endif
16
+ LEAN_EXPORT lean_object* l_Lean_Environment_unpickle_unsafe__1(lean_object*, lean_object*);
17
+ static lean_object* l_Lean_Environment_pickle___closed__1;
18
+ static lean_object* l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1___closed__1;
19
+ lean_object* l_Lean_HashMap_insert___at___private_Lean_Environment_0__Lean_Environment_addAux___spec__6(lean_object*, lean_object*, lean_object*);
20
+ LEAN_EXPORT lean_object* l_Lean_Environment_unpickle_unsafe__1___boxed(lean_object*, lean_object*);
21
+ static lean_object* l_Lean_Environment_pickle___closed__4;
22
+ lean_object* l_Lean_Name_mkStr3(lean_object*, lean_object*, lean_object*);
23
+ lean_object* l_Lean_Environment_replay(lean_object*, lean_object*, lean_object*);
24
+ LEAN_EXPORT lean_object* l_Lean_HashMap_ofList___at_Lean_Environment_unpickle_unsafe__1___spec__3(lean_object*);
25
+ LEAN_EXPORT lean_object* l_Lean_Environment_unpickle(lean_object*, lean_object*);
26
+ static lean_object* l_Lean_Environment_pickle___closed__2;
27
+ lean_object* l_unpickle___rarg(lean_object*, lean_object*);
28
+ lean_object* l_Lean_PersistentHashMap_foldlMAux___at_Lean_MetavarContext_getExprAssignmentDomain___spec__2___rarg(lean_object*, lean_object*, lean_object*);
29
+ static lean_object* l_Lean_HashMap_ofList___at_Lean_Environment_unpickle_unsafe__1___spec__3___closed__1;
30
+ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1(lean_object*);
31
+ LEAN_EXPORT lean_object* l_Lean_Environment_pickle(lean_object*, lean_object*, lean_object*);
32
+ LEAN_EXPORT lean_object* l_Lean_Environment_unpickle___boxed(lean_object*, lean_object*);
33
+ LEAN_EXPORT lean_object* l_List_foldl___at_Lean_Environment_unpickle_unsafe__1___spec__4(lean_object*, lean_object*);
34
+ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1___lambda__1(lean_object*, lean_object*, lean_object*);
35
+ lean_object* l_Lean_mkHashMapImp___rarg(lean_object*);
36
+ static lean_object* l_Lean_Environment_pickle___closed__3;
37
+ LEAN_EXPORT lean_object* l_Lean_Environment_pickle___boxed(lean_object*, lean_object*, lean_object*);
38
+ lean_object* lean_import_modules(lean_object*, lean_object*, uint32_t, uint8_t, lean_object*);
39
+ lean_object* lean_save_module_data(lean_object*, lean_object*, lean_object*, lean_object*);
40
+ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_foldlM___at_Lean_Environment_unpickle_unsafe__1___spec__2(lean_object*, lean_object*, lean_object*);
41
+ static lean_object* _init_l_Lean_Environment_pickle___closed__1() {
42
+ _start:
43
+ {
44
+ lean_object* x_1;
45
+ x_1 = lean_mk_string_from_bytes("Lean", 4);
46
+ return x_1;
47
+ }
48
+ }
49
+ static lean_object* _init_l_Lean_Environment_pickle___closed__2() {
50
+ _start:
51
+ {
52
+ lean_object* x_1;
53
+ x_1 = lean_mk_string_from_bytes("Environment", 11);
54
+ return x_1;
55
+ }
56
+ }
57
+ static lean_object* _init_l_Lean_Environment_pickle___closed__3() {
58
+ _start:
59
+ {
60
+ lean_object* x_1;
61
+ x_1 = lean_mk_string_from_bytes("pickle", 6);
62
+ return x_1;
63
+ }
64
+ }
65
+ static lean_object* _init_l_Lean_Environment_pickle___closed__4() {
66
+ _start:
67
+ {
68
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
69
+ x_1 = l_Lean_Environment_pickle___closed__1;
70
+ x_2 = l_Lean_Environment_pickle___closed__2;
71
+ x_3 = l_Lean_Environment_pickle___closed__3;
72
+ x_4 = l_Lean_Name_mkStr3(x_1, x_2, x_3);
73
+ return x_4;
74
+ }
75
+ }
76
+ LEAN_EXPORT lean_object* l_Lean_Environment_pickle(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
77
+ _start:
78
+ {
79
+ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
80
+ x_4 = lean_ctor_get(x_1, 4);
81
+ x_5 = lean_ctor_get(x_4, 1);
82
+ x_6 = lean_ctor_get(x_1, 1);
83
+ x_7 = lean_ctor_get(x_6, 1);
84
+ lean_inc(x_7);
85
+ lean_inc(x_5);
86
+ x_8 = lean_alloc_ctor(0, 2, 0);
87
+ lean_ctor_set(x_8, 0, x_5);
88
+ lean_ctor_set(x_8, 1, x_7);
89
+ x_9 = l_Lean_Environment_pickle___closed__4;
90
+ x_10 = lean_save_module_data(x_2, x_9, x_8, x_3);
91
+ lean_dec(x_8);
92
+ return x_10;
93
+ }
94
+ }
95
+ LEAN_EXPORT lean_object* l_Lean_Environment_pickle___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
96
+ _start:
97
+ {
98
+ lean_object* x_4;
99
+ x_4 = l_Lean_Environment_pickle(x_1, x_2, x_3);
100
+ lean_dec(x_2);
101
+ lean_dec(x_1);
102
+ return x_4;
103
+ }
104
+ }
105
+ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_foldlM___at_Lean_Environment_unpickle_unsafe__1___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
106
+ _start:
107
+ {
108
+ lean_object* x_4; lean_object* x_5;
109
+ x_4 = lean_ctor_get(x_1, 0);
110
+ lean_inc(x_4);
111
+ lean_dec(x_1);
112
+ x_5 = l_Lean_PersistentHashMap_foldlMAux___at_Lean_MetavarContext_getExprAssignmentDomain___spec__2___rarg(x_2, x_4, x_3);
113
+ return x_5;
114
+ }
115
+ }
116
+ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
117
+ _start:
118
+ {
119
+ lean_object* x_4; lean_object* x_5;
120
+ x_4 = lean_alloc_ctor(0, 2, 0);
121
+ lean_ctor_set(x_4, 0, x_2);
122
+ lean_ctor_set(x_4, 1, x_3);
123
+ x_5 = lean_alloc_ctor(1, 2, 0);
124
+ lean_ctor_set(x_5, 0, x_4);
125
+ lean_ctor_set(x_5, 1, x_1);
126
+ return x_5;
127
+ }
128
+ }
129
+ static lean_object* _init_l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1___closed__1() {
130
+ _start:
131
+ {
132
+ lean_object* x_1;
133
+ x_1 = lean_alloc_closure((void*)(l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1___lambda__1), 3, 0);
134
+ return x_1;
135
+ }
136
+ }
137
+ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1(lean_object* x_1) {
138
+ _start:
139
+ {
140
+ lean_object* x_2; lean_object* x_3; lean_object* x_4;
141
+ x_2 = lean_box(0);
142
+ x_3 = l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1___closed__1;
143
+ x_4 = l_Lean_PersistentHashMap_foldlM___at_Lean_Environment_unpickle_unsafe__1___spec__2(x_1, x_3, x_2);
144
+ return x_4;
145
+ }
146
+ }
147
+ LEAN_EXPORT lean_object* l_List_foldl___at_Lean_Environment_unpickle_unsafe__1___spec__4(lean_object* x_1, lean_object* x_2) {
148
+ _start:
149
+ {
150
+ if (lean_obj_tag(x_2) == 0)
151
+ {
152
+ return x_1;
153
+ }
154
+ else
155
+ {
156
+ lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
157
+ x_3 = lean_ctor_get(x_2, 0);
158
+ lean_inc(x_3);
159
+ x_4 = lean_ctor_get(x_2, 1);
160
+ lean_inc(x_4);
161
+ lean_dec(x_2);
162
+ x_5 = lean_ctor_get(x_3, 0);
163
+ lean_inc(x_5);
164
+ x_6 = lean_ctor_get(x_3, 1);
165
+ lean_inc(x_6);
166
+ lean_dec(x_3);
167
+ x_7 = l_Lean_HashMap_insert___at___private_Lean_Environment_0__Lean_Environment_addAux___spec__6(x_1, x_5, x_6);
168
+ x_1 = x_7;
169
+ x_2 = x_4;
170
+ goto _start;
171
+ }
172
+ }
173
+ }
174
+ static lean_object* _init_l_Lean_HashMap_ofList___at_Lean_Environment_unpickle_unsafe__1___spec__3___closed__1() {
175
+ _start:
176
+ {
177
+ lean_object* x_1; lean_object* x_2;
178
+ x_1 = lean_unsigned_to_nat(8u);
179
+ x_2 = l_Lean_mkHashMapImp___rarg(x_1);
180
+ return x_2;
181
+ }
182
+ }
183
+ LEAN_EXPORT lean_object* l_Lean_HashMap_ofList___at_Lean_Environment_unpickle_unsafe__1___spec__3(lean_object* x_1) {
184
+ _start:
185
+ {
186
+ lean_object* x_2; lean_object* x_3;
187
+ x_2 = l_Lean_HashMap_ofList___at_Lean_Environment_unpickle_unsafe__1___spec__3___closed__1;
188
+ x_3 = l_List_foldl___at_Lean_Environment_unpickle_unsafe__1___spec__4(x_2, x_1);
189
+ return x_3;
190
+ }
191
+ }
192
+ LEAN_EXPORT lean_object* l_Lean_Environment_unpickle_unsafe__1(lean_object* x_1, lean_object* x_2) {
193
+ _start:
194
+ {
195
+ lean_object* x_3;
196
+ x_3 = l_unpickle___rarg(x_1, x_2);
197
+ if (lean_obj_tag(x_3) == 0)
198
+ {
199
+ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8;
200
+ x_4 = lean_ctor_get(x_3, 0);
201
+ lean_inc(x_4);
202
+ x_5 = lean_ctor_get(x_4, 0);
203
+ lean_inc(x_5);
204
+ x_6 = lean_ctor_get(x_3, 1);
205
+ lean_inc(x_6);
206
+ lean_dec(x_3);
207
+ x_7 = lean_ctor_get(x_4, 1);
208
+ lean_inc(x_7);
209
+ lean_dec(x_4);
210
+ x_8 = !lean_is_exclusive(x_5);
211
+ if (x_8 == 0)
212
+ {
213
+ lean_object* x_9; lean_object* x_10; lean_object* x_11; uint32_t x_12; uint8_t x_13; lean_object* x_14;
214
+ x_9 = lean_ctor_get(x_5, 0);
215
+ x_10 = lean_ctor_get(x_5, 1);
216
+ x_11 = lean_box(0);
217
+ x_12 = 0;
218
+ x_13 = 0;
219
+ x_14 = lean_import_modules(x_9, x_11, x_12, x_13, x_6);
220
+ if (lean_obj_tag(x_14) == 0)
221
+ {
222
+ lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
223
+ x_15 = lean_ctor_get(x_14, 0);
224
+ lean_inc(x_15);
225
+ x_16 = lean_ctor_get(x_14, 1);
226
+ lean_inc(x_16);
227
+ lean_dec(x_14);
228
+ x_17 = l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1(x_10);
229
+ x_18 = l_Lean_HashMap_ofList___at_Lean_Environment_unpickle_unsafe__1___spec__3(x_17);
230
+ x_19 = l_Lean_Environment_replay(x_18, x_15, x_16);
231
+ if (lean_obj_tag(x_19) == 0)
232
+ {
233
+ uint8_t x_20;
234
+ x_20 = !lean_is_exclusive(x_19);
235
+ if (x_20 == 0)
236
+ {
237
+ lean_object* x_21;
238
+ x_21 = lean_ctor_get(x_19, 0);
239
+ lean_ctor_set(x_5, 1, x_7);
240
+ lean_ctor_set(x_5, 0, x_21);
241
+ lean_ctor_set(x_19, 0, x_5);
242
+ return x_19;
243
+ }
244
+ else
245
+ {
246
+ lean_object* x_22; lean_object* x_23; lean_object* x_24;
247
+ x_22 = lean_ctor_get(x_19, 0);
248
+ x_23 = lean_ctor_get(x_19, 1);
249
+ lean_inc(x_23);
250
+ lean_inc(x_22);
251
+ lean_dec(x_19);
252
+ lean_ctor_set(x_5, 1, x_7);
253
+ lean_ctor_set(x_5, 0, x_22);
254
+ x_24 = lean_alloc_ctor(0, 2, 0);
255
+ lean_ctor_set(x_24, 0, x_5);
256
+ lean_ctor_set(x_24, 1, x_23);
257
+ return x_24;
258
+ }
259
+ }
260
+ else
261
+ {
262
+ uint8_t x_25;
263
+ lean_free_object(x_5);
264
+ lean_dec(x_7);
265
+ x_25 = !lean_is_exclusive(x_19);
266
+ if (x_25 == 0)
267
+ {
268
+ return x_19;
269
+ }
270
+ else
271
+ {
272
+ lean_object* x_26; lean_object* x_27; lean_object* x_28;
273
+ x_26 = lean_ctor_get(x_19, 0);
274
+ x_27 = lean_ctor_get(x_19, 1);
275
+ lean_inc(x_27);
276
+ lean_inc(x_26);
277
+ lean_dec(x_19);
278
+ x_28 = lean_alloc_ctor(1, 2, 0);
279
+ lean_ctor_set(x_28, 0, x_26);
280
+ lean_ctor_set(x_28, 1, x_27);
281
+ return x_28;
282
+ }
283
+ }
284
+ }
285
+ else
286
+ {
287
+ uint8_t x_29;
288
+ lean_free_object(x_5);
289
+ lean_dec(x_10);
290
+ lean_dec(x_7);
291
+ x_29 = !lean_is_exclusive(x_14);
292
+ if (x_29 == 0)
293
+ {
294
+ return x_14;
295
+ }
296
+ else
297
+ {
298
+ lean_object* x_30; lean_object* x_31; lean_object* x_32;
299
+ x_30 = lean_ctor_get(x_14, 0);
300
+ x_31 = lean_ctor_get(x_14, 1);
301
+ lean_inc(x_31);
302
+ lean_inc(x_30);
303
+ lean_dec(x_14);
304
+ x_32 = lean_alloc_ctor(1, 2, 0);
305
+ lean_ctor_set(x_32, 0, x_30);
306
+ lean_ctor_set(x_32, 1, x_31);
307
+ return x_32;
308
+ }
309
+ }
310
+ }
311
+ else
312
+ {
313
+ lean_object* x_33; lean_object* x_34; lean_object* x_35; uint32_t x_36; uint8_t x_37; lean_object* x_38;
314
+ x_33 = lean_ctor_get(x_5, 0);
315
+ x_34 = lean_ctor_get(x_5, 1);
316
+ lean_inc(x_34);
317
+ lean_inc(x_33);
318
+ lean_dec(x_5);
319
+ x_35 = lean_box(0);
320
+ x_36 = 0;
321
+ x_37 = 0;
322
+ x_38 = lean_import_modules(x_33, x_35, x_36, x_37, x_6);
323
+ if (lean_obj_tag(x_38) == 0)
324
+ {
325
+ lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
326
+ x_39 = lean_ctor_get(x_38, 0);
327
+ lean_inc(x_39);
328
+ x_40 = lean_ctor_get(x_38, 1);
329
+ lean_inc(x_40);
330
+ lean_dec(x_38);
331
+ x_41 = l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1(x_34);
332
+ x_42 = l_Lean_HashMap_ofList___at_Lean_Environment_unpickle_unsafe__1___spec__3(x_41);
333
+ x_43 = l_Lean_Environment_replay(x_42, x_39, x_40);
334
+ if (lean_obj_tag(x_43) == 0)
335
+ {
336
+ lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
337
+ x_44 = lean_ctor_get(x_43, 0);
338
+ lean_inc(x_44);
339
+ x_45 = lean_ctor_get(x_43, 1);
340
+ lean_inc(x_45);
341
+ if (lean_is_exclusive(x_43)) {
342
+ lean_ctor_release(x_43, 0);
343
+ lean_ctor_release(x_43, 1);
344
+ x_46 = x_43;
345
+ } else {
346
+ lean_dec_ref(x_43);
347
+ x_46 = lean_box(0);
348
+ }
349
+ x_47 = lean_alloc_ctor(0, 2, 0);
350
+ lean_ctor_set(x_47, 0, x_44);
351
+ lean_ctor_set(x_47, 1, x_7);
352
+ if (lean_is_scalar(x_46)) {
353
+ x_48 = lean_alloc_ctor(0, 2, 0);
354
+ } else {
355
+ x_48 = x_46;
356
+ }
357
+ lean_ctor_set(x_48, 0, x_47);
358
+ lean_ctor_set(x_48, 1, x_45);
359
+ return x_48;
360
+ }
361
+ else
362
+ {
363
+ lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52;
364
+ lean_dec(x_7);
365
+ x_49 = lean_ctor_get(x_43, 0);
366
+ lean_inc(x_49);
367
+ x_50 = lean_ctor_get(x_43, 1);
368
+ lean_inc(x_50);
369
+ if (lean_is_exclusive(x_43)) {
370
+ lean_ctor_release(x_43, 0);
371
+ lean_ctor_release(x_43, 1);
372
+ x_51 = x_43;
373
+ } else {
374
+ lean_dec_ref(x_43);
375
+ x_51 = lean_box(0);
376
+ }
377
+ if (lean_is_scalar(x_51)) {
378
+ x_52 = lean_alloc_ctor(1, 2, 0);
379
+ } else {
380
+ x_52 = x_51;
381
+ }
382
+ lean_ctor_set(x_52, 0, x_49);
383
+ lean_ctor_set(x_52, 1, x_50);
384
+ return x_52;
385
+ }
386
+ }
387
+ else
388
+ {
389
+ lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56;
390
+ lean_dec(x_34);
391
+ lean_dec(x_7);
392
+ x_53 = lean_ctor_get(x_38, 0);
393
+ lean_inc(x_53);
394
+ x_54 = lean_ctor_get(x_38, 1);
395
+ lean_inc(x_54);
396
+ if (lean_is_exclusive(x_38)) {
397
+ lean_ctor_release(x_38, 0);
398
+ lean_ctor_release(x_38, 1);
399
+ x_55 = x_38;
400
+ } else {
401
+ lean_dec_ref(x_38);
402
+ x_55 = lean_box(0);
403
+ }
404
+ if (lean_is_scalar(x_55)) {
405
+ x_56 = lean_alloc_ctor(1, 2, 0);
406
+ } else {
407
+ x_56 = x_55;
408
+ }
409
+ lean_ctor_set(x_56, 0, x_53);
410
+ lean_ctor_set(x_56, 1, x_54);
411
+ return x_56;
412
+ }
413
+ }
414
+ }
415
+ else
416
+ {
417
+ uint8_t x_57;
418
+ x_57 = !lean_is_exclusive(x_3);
419
+ if (x_57 == 0)
420
+ {
421
+ return x_3;
422
+ }
423
+ else
424
+ {
425
+ lean_object* x_58; lean_object* x_59; lean_object* x_60;
426
+ x_58 = lean_ctor_get(x_3, 0);
427
+ x_59 = lean_ctor_get(x_3, 1);
428
+ lean_inc(x_59);
429
+ lean_inc(x_58);
430
+ lean_dec(x_3);
431
+ x_60 = lean_alloc_ctor(1, 2, 0);
432
+ lean_ctor_set(x_60, 0, x_58);
433
+ lean_ctor_set(x_60, 1, x_59);
434
+ return x_60;
435
+ }
436
+ }
437
+ }
438
+ }
439
+ LEAN_EXPORT lean_object* l_Lean_Environment_unpickle_unsafe__1___boxed(lean_object* x_1, lean_object* x_2) {
440
+ _start:
441
+ {
442
+ lean_object* x_3;
443
+ x_3 = l_Lean_Environment_unpickle_unsafe__1(x_1, x_2);
444
+ lean_dec(x_1);
445
+ return x_3;
446
+ }
447
+ }
448
+ LEAN_EXPORT lean_object* l_Lean_Environment_unpickle(lean_object* x_1, lean_object* x_2) {
449
+ _start:
450
+ {
451
+ lean_object* x_3;
452
+ x_3 = l_Lean_Environment_unpickle_unsafe__1(x_1, x_2);
453
+ return x_3;
454
+ }
455
+ }
456
+ LEAN_EXPORT lean_object* l_Lean_Environment_unpickle___boxed(lean_object* x_1, lean_object* x_2) {
457
+ _start:
458
+ {
459
+ lean_object* x_3;
460
+ x_3 = l_Lean_Environment_unpickle(x_1, x_2);
461
+ lean_dec(x_1);
462
+ return x_3;
463
+ }
464
+ }
465
+ lean_object* initialize_Init(uint8_t builtin, lean_object*);
466
+ lean_object* initialize_REPL_Util_Pickle(uint8_t builtin, lean_object*);
467
+ lean_object* initialize_Lean_Replay(uint8_t builtin, lean_object*);
468
+ static bool _G_initialized = false;
469
+ LEAN_EXPORT lean_object* initialize_REPL_Lean_Environment(uint8_t builtin, lean_object* w) {
470
+ lean_object * res;
471
+ if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
472
+ _G_initialized = true;
473
+ res = initialize_Init(builtin, lean_io_mk_world());
474
+ if (lean_io_result_is_error(res)) return res;
475
+ lean_dec_ref(res);
476
+ res = initialize_REPL_Util_Pickle(builtin, lean_io_mk_world());
477
+ if (lean_io_result_is_error(res)) return res;
478
+ lean_dec_ref(res);
479
+ res = initialize_Lean_Replay(builtin, lean_io_mk_world());
480
+ if (lean_io_result_is_error(res)) return res;
481
+ lean_dec_ref(res);
482
+ l_Lean_Environment_pickle___closed__1 = _init_l_Lean_Environment_pickle___closed__1();
483
+ lean_mark_persistent(l_Lean_Environment_pickle___closed__1);
484
+ l_Lean_Environment_pickle___closed__2 = _init_l_Lean_Environment_pickle___closed__2();
485
+ lean_mark_persistent(l_Lean_Environment_pickle___closed__2);
486
+ l_Lean_Environment_pickle___closed__3 = _init_l_Lean_Environment_pickle___closed__3();
487
+ lean_mark_persistent(l_Lean_Environment_pickle___closed__3);
488
+ l_Lean_Environment_pickle___closed__4 = _init_l_Lean_Environment_pickle___closed__4();
489
+ lean_mark_persistent(l_Lean_Environment_pickle___closed__4);
490
+ l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1___closed__1 = _init_l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1___closed__1();
491
+ lean_mark_persistent(l_Lean_PersistentHashMap_toList___at_Lean_Environment_unpickle_unsafe__1___spec__1___closed__1);
492
+ l_Lean_HashMap_ofList___at_Lean_Environment_unpickle_unsafe__1___spec__3___closed__1 = _init_l_Lean_HashMap_ofList___at_Lean_Environment_unpickle_unsafe__1___spec__3___closed__1();
493
+ lean_mark_persistent(l_Lean_HashMap_ofList___at_Lean_Environment_unpickle_unsafe__1___spec__3___closed__1);
494
+ return lean_io_result_mk_ok(lean_box(0));
495
+ }
496
+ #ifdef __cplusplus
497
+ }
498
+ #endif
.lake/build/ir/REPL/Lean/Environment.c.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 12909436216813462993
.lake/build/ir/REPL/Lean/Environment.c.o ADDED
Binary file (12.1 kB). View file
 
.lake/build/ir/REPL/Lean/Environment.c.o.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 10948395708289941493
.lake/build/ir/REPL/Lean/Environment.c.o.trace ADDED
@@ -0,0 +1 @@
 
 
1
+ 5577881518732137303
.lake/build/ir/REPL/Lean/InfoTree.c ADDED
The diff for this file is too large to render. See raw diff
 
.lake/build/ir/REPL/Lean/InfoTree.c.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 176342699958617316
.lake/build/ir/REPL/Lean/InfoTree.c.o ADDED
Binary file (94.5 kB). View file
 
.lake/build/ir/REPL/Lean/InfoTree.c.o.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 15115882140174476820
.lake/build/ir/REPL/Lean/InfoTree.c.o.trace ADDED
@@ -0,0 +1 @@
 
 
1
+ 8688494094792636710
.lake/build/ir/REPL/Lean/InfoTree/ToJson.c ADDED
The diff for this file is too large to render. See raw diff
 
.lake/build/ir/REPL/Lean/InfoTree/ToJson.c.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 1347255799403920269
.lake/build/ir/REPL/Lean/InfoTree/ToJson.c.o ADDED
Binary file (60.1 kB). View file
 
.lake/build/ir/REPL/Lean/InfoTree/ToJson.c.o.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 14447304762711021773
.lake/build/ir/REPL/Lean/InfoTree/ToJson.c.o.trace ADDED
@@ -0,0 +1 @@
 
 
1
+ 5405264490761089779
.lake/build/ir/REPL/Main.c ADDED
The diff for this file is too large to render. See raw diff
 
.lake/build/ir/REPL/Main.c.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 2447817378394231335
.lake/build/ir/REPL/Main.c.o ADDED
Binary file (217 kB). View file
 
.lake/build/ir/REPL/Main.c.o.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 16621928521591753648
.lake/build/ir/REPL/Main.c.o.trace ADDED
@@ -0,0 +1 @@
 
 
1
+ 17552246326444282193
.lake/build/ir/REPL/Snapshots.c ADDED
The diff for this file is too large to render. See raw diff
 
.lake/build/ir/REPL/Snapshots.c.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 30813973382806577
.lake/build/ir/REPL/Snapshots.c.o ADDED
Binary file (140 kB). View file
 
.lake/build/ir/REPL/Snapshots.c.o.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 7465317517317733738
.lake/build/ir/REPL/Snapshots.c.o.trace ADDED
@@ -0,0 +1 @@
 
 
1
+ 17627810084019723639
.lake/build/ir/REPL/Util/Path.c ADDED
@@ -0,0 +1,494 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Lean compiler output
2
+ // Module: REPL.Util.Path
3
+ // Imports: Init Lean
4
+ #include <lean/lean.h>
5
+ #if defined(__clang__)
6
+ #pragma clang diagnostic ignored "-Wunused-parameter"
7
+ #pragma clang diagnostic ignored "-Wunused-label"
8
+ #elif defined(__GNUC__) && !defined(__CLANG__)
9
+ #pragma GCC diagnostic ignored "-Wunused-parameter"
10
+ #pragma GCC diagnostic ignored "-Wunused-label"
11
+ #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
12
+ #endif
13
+ #ifdef __cplusplus
14
+ extern "C" {
15
+ #endif
16
+ lean_object* l_Lean_Expr_const___override(lean_object*, lean_object*);
17
+ static lean_object* l_termCompile__time__search__path_x25___closed__1;
18
+ static lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__8;
19
+ LEAN_EXPORT lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
20
+ static lean_object* l_termCompile__time__search__path_x25___closed__3;
21
+ lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
22
+ static lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__5;
23
+ static lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__10;
24
+ static lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__9;
25
+ static lean_object* l_instToExprFilePath___closed__2;
26
+ uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
27
+ static lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__1;
28
+ lean_object* l_Lean_Name_mkStr3(lean_object*, lean_object*, lean_object*);
29
+ lean_object* l_Lean_mkStrLit(lean_object*);
30
+ LEAN_EXPORT lean_object* l_instToExprFilePath;
31
+ static lean_object* l_termCompile__time__search__path_x25___closed__4;
32
+ static lean_object* l_instToExprFilePath___closed__3;
33
+ static lean_object* l_instToExprFilePath___lambda__1___closed__4;
34
+ LEAN_EXPORT lean_object* l___private_Lean_ToExpr_0__Lean_List_toExprAux___at___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___spec__1(lean_object*, lean_object*, lean_object*);
35
+ lean_object* lean_st_ref_get(lean_object*, lean_object*);
36
+ LEAN_EXPORT lean_object* l___private_Lean_ToExpr_0__Lean_List_toExprAux___at___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___spec__1___boxed(lean_object*, lean_object*, lean_object*);
37
+ extern lean_object* l_Lean_levelZero;
38
+ lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
39
+ static lean_object* l_instToExprFilePath___lambda__1___closed__3;
40
+ static lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__4;
41
+ static lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__3;
42
+ static lean_object* l_instToExprFilePath___closed__4;
43
+ static lean_object* l_instToExprFilePath___lambda__1___closed__2;
44
+ lean_object* l_Lean_Expr_app___override(lean_object*, lean_object*);
45
+ static lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__11;
46
+ extern lean_object* l_Lean_searchPathRef;
47
+ lean_object* l_Lean_Name_mkStr2(lean_object*, lean_object*);
48
+ LEAN_EXPORT lean_object* l_instToExprFilePath___lambda__1(lean_object*);
49
+ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabLetMVar___spec__1___rarg(lean_object*);
50
+ LEAN_EXPORT lean_object* l_termCompile__time__search__path_x25;
51
+ static lean_object* l_instToExprFilePath___lambda__1___closed__5;
52
+ static lean_object* l_termCompile__time__search__path_x25___closed__2;
53
+ LEAN_EXPORT lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
54
+ static lean_object* l_instToExprFilePath___closed__1;
55
+ static lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__6;
56
+ static lean_object* l_instToExprFilePath___lambda__1___closed__1;
57
+ static lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__7;
58
+ static lean_object* l_termCompile__time__search__path_x25___closed__5;
59
+ static lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__2;
60
+ static lean_object* _init_l_instToExprFilePath___lambda__1___closed__1() {
61
+ _start:
62
+ {
63
+ lean_object* x_1;
64
+ x_1 = lean_mk_string_from_bytes("System", 6);
65
+ return x_1;
66
+ }
67
+ }
68
+ static lean_object* _init_l_instToExprFilePath___lambda__1___closed__2() {
69
+ _start:
70
+ {
71
+ lean_object* x_1;
72
+ x_1 = lean_mk_string_from_bytes("FilePath", 8);
73
+ return x_1;
74
+ }
75
+ }
76
+ static lean_object* _init_l_instToExprFilePath___lambda__1___closed__3() {
77
+ _start:
78
+ {
79
+ lean_object* x_1;
80
+ x_1 = lean_mk_string_from_bytes("mk", 2);
81
+ return x_1;
82
+ }
83
+ }
84
+ static lean_object* _init_l_instToExprFilePath___lambda__1___closed__4() {
85
+ _start:
86
+ {
87
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
88
+ x_1 = l_instToExprFilePath___lambda__1___closed__1;
89
+ x_2 = l_instToExprFilePath___lambda__1___closed__2;
90
+ x_3 = l_instToExprFilePath___lambda__1___closed__3;
91
+ x_4 = l_Lean_Name_mkStr3(x_1, x_2, x_3);
92
+ return x_4;
93
+ }
94
+ }
95
+ static lean_object* _init_l_instToExprFilePath___lambda__1___closed__5() {
96
+ _start:
97
+ {
98
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
99
+ x_1 = lean_box(0);
100
+ x_2 = l_instToExprFilePath___lambda__1___closed__4;
101
+ x_3 = l_Lean_Expr_const___override(x_2, x_1);
102
+ return x_3;
103
+ }
104
+ }
105
+ LEAN_EXPORT lean_object* l_instToExprFilePath___lambda__1(lean_object* x_1) {
106
+ _start:
107
+ {
108
+ lean_object* x_2; lean_object* x_3; lean_object* x_4;
109
+ x_2 = l_Lean_mkStrLit(x_1);
110
+ x_3 = l_instToExprFilePath___lambda__1___closed__5;
111
+ x_4 = l_Lean_Expr_app___override(x_3, x_2);
112
+ return x_4;
113
+ }
114
+ }
115
+ static lean_object* _init_l_instToExprFilePath___closed__1() {
116
+ _start:
117
+ {
118
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
119
+ x_1 = l_instToExprFilePath___lambda__1___closed__1;
120
+ x_2 = l_instToExprFilePath___lambda__1___closed__2;
121
+ x_3 = l_Lean_Name_mkStr2(x_1, x_2);
122
+ return x_3;
123
+ }
124
+ }
125
+ static lean_object* _init_l_instToExprFilePath___closed__2() {
126
+ _start:
127
+ {
128
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
129
+ x_1 = lean_box(0);
130
+ x_2 = l_instToExprFilePath___closed__1;
131
+ x_3 = l_Lean_Expr_const___override(x_2, x_1);
132
+ return x_3;
133
+ }
134
+ }
135
+ static lean_object* _init_l_instToExprFilePath___closed__3() {
136
+ _start:
137
+ {
138
+ lean_object* x_1;
139
+ x_1 = lean_alloc_closure((void*)(l_instToExprFilePath___lambda__1), 1, 0);
140
+ return x_1;
141
+ }
142
+ }
143
+ static lean_object* _init_l_instToExprFilePath___closed__4() {
144
+ _start:
145
+ {
146
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
147
+ x_1 = l_instToExprFilePath___closed__3;
148
+ x_2 = l_instToExprFilePath___closed__2;
149
+ x_3 = lean_alloc_ctor(0, 2, 0);
150
+ lean_ctor_set(x_3, 0, x_1);
151
+ lean_ctor_set(x_3, 1, x_2);
152
+ return x_3;
153
+ }
154
+ }
155
+ static lean_object* _init_l_instToExprFilePath() {
156
+ _start:
157
+ {
158
+ lean_object* x_1;
159
+ x_1 = l_instToExprFilePath___closed__4;
160
+ return x_1;
161
+ }
162
+ }
163
+ static lean_object* _init_l_termCompile__time__search__path_x25___closed__1() {
164
+ _start:
165
+ {
166
+ lean_object* x_1;
167
+ x_1 = lean_mk_string_from_bytes("termCompile_time_search_path%", 29);
168
+ return x_1;
169
+ }
170
+ }
171
+ static lean_object* _init_l_termCompile__time__search__path_x25___closed__2() {
172
+ _start:
173
+ {
174
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
175
+ x_1 = lean_box(0);
176
+ x_2 = l_termCompile__time__search__path_x25___closed__1;
177
+ x_3 = l_Lean_Name_str___override(x_1, x_2);
178
+ return x_3;
179
+ }
180
+ }
181
+ static lean_object* _init_l_termCompile__time__search__path_x25___closed__3() {
182
+ _start:
183
+ {
184
+ lean_object* x_1;
185
+ x_1 = lean_mk_string_from_bytes("compile_time_search_path%", 25);
186
+ return x_1;
187
+ }
188
+ }
189
+ static lean_object* _init_l_termCompile__time__search__path_x25___closed__4() {
190
+ _start:
191
+ {
192
+ lean_object* x_1; lean_object* x_2;
193
+ x_1 = l_termCompile__time__search__path_x25___closed__3;
194
+ x_2 = lean_alloc_ctor(5, 1, 0);
195
+ lean_ctor_set(x_2, 0, x_1);
196
+ return x_2;
197
+ }
198
+ }
199
+ static lean_object* _init_l_termCompile__time__search__path_x25___closed__5() {
200
+ _start:
201
+ {
202
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
203
+ x_1 = l_termCompile__time__search__path_x25___closed__2;
204
+ x_2 = lean_unsigned_to_nat(1024u);
205
+ x_3 = l_termCompile__time__search__path_x25___closed__4;
206
+ x_4 = lean_alloc_ctor(3, 3, 0);
207
+ lean_ctor_set(x_4, 0, x_1);
208
+ lean_ctor_set(x_4, 1, x_2);
209
+ lean_ctor_set(x_4, 2, x_3);
210
+ return x_4;
211
+ }
212
+ }
213
+ static lean_object* _init_l_termCompile__time__search__path_x25() {
214
+ _start:
215
+ {
216
+ lean_object* x_1;
217
+ x_1 = l_termCompile__time__search__path_x25___closed__5;
218
+ return x_1;
219
+ }
220
+ }
221
+ LEAN_EXPORT lean_object* l___private_Lean_ToExpr_0__Lean_List_toExprAux___at___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
222
+ _start:
223
+ {
224
+ if (lean_obj_tag(x_3) == 0)
225
+ {
226
+ lean_dec(x_2);
227
+ lean_inc(x_1);
228
+ return x_1;
229
+ }
230
+ else
231
+ {
232
+ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
233
+ x_4 = lean_ctor_get(x_3, 0);
234
+ lean_inc(x_4);
235
+ x_5 = lean_ctor_get(x_3, 1);
236
+ lean_inc(x_5);
237
+ lean_dec(x_3);
238
+ x_6 = l_Lean_mkStrLit(x_4);
239
+ x_7 = l_instToExprFilePath___lambda__1___closed__5;
240
+ x_8 = l_Lean_Expr_app___override(x_7, x_6);
241
+ lean_inc(x_2);
242
+ x_9 = l___private_Lean_ToExpr_0__Lean_List_toExprAux___at___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___spec__1(x_1, x_2, x_5);
243
+ x_10 = l_Lean_mkAppB(x_2, x_8, x_9);
244
+ return x_10;
245
+ }
246
+ }
247
+ }
248
+ static lean_object* _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__1() {
249
+ _start:
250
+ {
251
+ lean_object* x_1;
252
+ x_1 = l_Lean_searchPathRef;
253
+ return x_1;
254
+ }
255
+ }
256
+ static lean_object* _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__2() {
257
+ _start:
258
+ {
259
+ lean_object* x_1;
260
+ x_1 = lean_mk_string_from_bytes("List", 4);
261
+ return x_1;
262
+ }
263
+ }
264
+ static lean_object* _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__3() {
265
+ _start:
266
+ {
267
+ lean_object* x_1;
268
+ x_1 = lean_mk_string_from_bytes("nil", 3);
269
+ return x_1;
270
+ }
271
+ }
272
+ static lean_object* _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__4() {
273
+ _start:
274
+ {
275
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
276
+ x_1 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__2;
277
+ x_2 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__3;
278
+ x_3 = l_Lean_Name_mkStr2(x_1, x_2);
279
+ return x_3;
280
+ }
281
+ }
282
+ static lean_object* _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__5() {
283
+ _start:
284
+ {
285
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
286
+ x_1 = lean_box(0);
287
+ x_2 = l_Lean_levelZero;
288
+ x_3 = lean_alloc_ctor(1, 2, 0);
289
+ lean_ctor_set(x_3, 0, x_2);
290
+ lean_ctor_set(x_3, 1, x_1);
291
+ return x_3;
292
+ }
293
+ }
294
+ static lean_object* _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__6() {
295
+ _start:
296
+ {
297
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
298
+ x_1 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__4;
299
+ x_2 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__5;
300
+ x_3 = l_Lean_Expr_const___override(x_1, x_2);
301
+ return x_3;
302
+ }
303
+ }
304
+ static lean_object* _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__7() {
305
+ _start:
306
+ {
307
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
308
+ x_1 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__6;
309
+ x_2 = l_instToExprFilePath___closed__2;
310
+ x_3 = l_Lean_Expr_app___override(x_1, x_2);
311
+ return x_3;
312
+ }
313
+ }
314
+ static lean_object* _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__8() {
315
+ _start:
316
+ {
317
+ lean_object* x_1;
318
+ x_1 = lean_mk_string_from_bytes("cons", 4);
319
+ return x_1;
320
+ }
321
+ }
322
+ static lean_object* _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__9() {
323
+ _start:
324
+ {
325
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
326
+ x_1 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__2;
327
+ x_2 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__8;
328
+ x_3 = l_Lean_Name_mkStr2(x_1, x_2);
329
+ return x_3;
330
+ }
331
+ }
332
+ static lean_object* _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__10() {
333
+ _start:
334
+ {
335
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
336
+ x_1 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__9;
337
+ x_2 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__5;
338
+ x_3 = l_Lean_Expr_const___override(x_1, x_2);
339
+ return x_3;
340
+ }
341
+ }
342
+ static lean_object* _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__11() {
343
+ _start:
344
+ {
345
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
346
+ x_1 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__10;
347
+ x_2 = l_instToExprFilePath___closed__2;
348
+ x_3 = l_Lean_Expr_app___override(x_1, x_2);
349
+ return x_3;
350
+ }
351
+ }
352
+ LEAN_EXPORT lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
353
+ _start:
354
+ {
355
+ lean_object* x_10; uint8_t x_11;
356
+ x_10 = l_termCompile__time__search__path_x25___closed__2;
357
+ x_11 = l_Lean_Syntax_isOfKind(x_1, x_10);
358
+ if (x_11 == 0)
359
+ {
360
+ lean_object* x_12;
361
+ x_12 = l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabLetMVar___spec__1___rarg(x_9);
362
+ return x_12;
363
+ }
364
+ else
365
+ {
366
+ lean_object* x_13; lean_object* x_14; uint8_t x_15;
367
+ x_13 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__1;
368
+ x_14 = lean_st_ref_get(x_13, x_9);
369
+ x_15 = !lean_is_exclusive(x_14);
370
+ if (x_15 == 0)
371
+ {
372
+ lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
373
+ x_16 = lean_ctor_get(x_14, 0);
374
+ x_17 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__7;
375
+ x_18 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__11;
376
+ x_19 = l___private_Lean_ToExpr_0__Lean_List_toExprAux___at___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___spec__1(x_17, x_18, x_16);
377
+ lean_ctor_set(x_14, 0, x_19);
378
+ return x_14;
379
+ }
380
+ else
381
+ {
382
+ lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
383
+ x_20 = lean_ctor_get(x_14, 0);
384
+ x_21 = lean_ctor_get(x_14, 1);
385
+ lean_inc(x_21);
386
+ lean_inc(x_20);
387
+ lean_dec(x_14);
388
+ x_22 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__7;
389
+ x_23 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__11;
390
+ x_24 = l___private_Lean_ToExpr_0__Lean_List_toExprAux___at___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___spec__1(x_22, x_23, x_20);
391
+ x_25 = lean_alloc_ctor(0, 2, 0);
392
+ lean_ctor_set(x_25, 0, x_24);
393
+ lean_ctor_set(x_25, 1, x_21);
394
+ return x_25;
395
+ }
396
+ }
397
+ }
398
+ }
399
+ LEAN_EXPORT lean_object* l___private_Lean_ToExpr_0__Lean_List_toExprAux___at___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
400
+ _start:
401
+ {
402
+ lean_object* x_4;
403
+ x_4 = l___private_Lean_ToExpr_0__Lean_List_toExprAux___at___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___spec__1(x_1, x_2, x_3);
404
+ lean_dec(x_1);
405
+ return x_4;
406
+ }
407
+ }
408
+ LEAN_EXPORT lean_object* l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
409
+ _start:
410
+ {
411
+ lean_object* x_10;
412
+ x_10 = l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
413
+ lean_dec(x_8);
414
+ lean_dec(x_7);
415
+ lean_dec(x_6);
416
+ lean_dec(x_5);
417
+ lean_dec(x_4);
418
+ lean_dec(x_3);
419
+ lean_dec(x_2);
420
+ return x_10;
421
+ }
422
+ }
423
+ lean_object* initialize_Init(uint8_t builtin, lean_object*);
424
+ lean_object* initialize_Lean(uint8_t builtin, lean_object*);
425
+ static bool _G_initialized = false;
426
+ LEAN_EXPORT lean_object* initialize_REPL_Util_Path(uint8_t builtin, lean_object* w) {
427
+ lean_object * res;
428
+ if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
429
+ _G_initialized = true;
430
+ res = initialize_Init(builtin, lean_io_mk_world());
431
+ if (lean_io_result_is_error(res)) return res;
432
+ lean_dec_ref(res);
433
+ res = initialize_Lean(builtin, lean_io_mk_world());
434
+ if (lean_io_result_is_error(res)) return res;
435
+ lean_dec_ref(res);
436
+ l_instToExprFilePath___lambda__1___closed__1 = _init_l_instToExprFilePath___lambda__1___closed__1();
437
+ lean_mark_persistent(l_instToExprFilePath___lambda__1___closed__1);
438
+ l_instToExprFilePath___lambda__1___closed__2 = _init_l_instToExprFilePath___lambda__1___closed__2();
439
+ lean_mark_persistent(l_instToExprFilePath___lambda__1___closed__2);
440
+ l_instToExprFilePath___lambda__1___closed__3 = _init_l_instToExprFilePath___lambda__1___closed__3();
441
+ lean_mark_persistent(l_instToExprFilePath___lambda__1___closed__3);
442
+ l_instToExprFilePath___lambda__1___closed__4 = _init_l_instToExprFilePath___lambda__1___closed__4();
443
+ lean_mark_persistent(l_instToExprFilePath___lambda__1___closed__4);
444
+ l_instToExprFilePath___lambda__1___closed__5 = _init_l_instToExprFilePath___lambda__1___closed__5();
445
+ lean_mark_persistent(l_instToExprFilePath___lambda__1___closed__5);
446
+ l_instToExprFilePath___closed__1 = _init_l_instToExprFilePath___closed__1();
447
+ lean_mark_persistent(l_instToExprFilePath___closed__1);
448
+ l_instToExprFilePath___closed__2 = _init_l_instToExprFilePath___closed__2();
449
+ lean_mark_persistent(l_instToExprFilePath___closed__2);
450
+ l_instToExprFilePath___closed__3 = _init_l_instToExprFilePath___closed__3();
451
+ lean_mark_persistent(l_instToExprFilePath___closed__3);
452
+ l_instToExprFilePath___closed__4 = _init_l_instToExprFilePath___closed__4();
453
+ lean_mark_persistent(l_instToExprFilePath___closed__4);
454
+ l_instToExprFilePath = _init_l_instToExprFilePath();
455
+ lean_mark_persistent(l_instToExprFilePath);
456
+ l_termCompile__time__search__path_x25___closed__1 = _init_l_termCompile__time__search__path_x25___closed__1();
457
+ lean_mark_persistent(l_termCompile__time__search__path_x25___closed__1);
458
+ l_termCompile__time__search__path_x25___closed__2 = _init_l_termCompile__time__search__path_x25___closed__2();
459
+ lean_mark_persistent(l_termCompile__time__search__path_x25___closed__2);
460
+ l_termCompile__time__search__path_x25___closed__3 = _init_l_termCompile__time__search__path_x25___closed__3();
461
+ lean_mark_persistent(l_termCompile__time__search__path_x25___closed__3);
462
+ l_termCompile__time__search__path_x25___closed__4 = _init_l_termCompile__time__search__path_x25___closed__4();
463
+ lean_mark_persistent(l_termCompile__time__search__path_x25___closed__4);
464
+ l_termCompile__time__search__path_x25___closed__5 = _init_l_termCompile__time__search__path_x25___closed__5();
465
+ lean_mark_persistent(l_termCompile__time__search__path_x25___closed__5);
466
+ l_termCompile__time__search__path_x25 = _init_l_termCompile__time__search__path_x25();
467
+ lean_mark_persistent(l_termCompile__time__search__path_x25);
468
+ l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__1 = _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__1();
469
+ lean_mark_persistent(l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__1);
470
+ l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__2 = _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__2();
471
+ lean_mark_persistent(l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__2);
472
+ l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__3 = _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__3();
473
+ lean_mark_persistent(l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__3);
474
+ l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__4 = _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__4();
475
+ lean_mark_persistent(l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__4);
476
+ l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__5 = _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__5();
477
+ lean_mark_persistent(l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__5);
478
+ l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__6 = _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__6();
479
+ lean_mark_persistent(l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__6);
480
+ l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__7 = _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__7();
481
+ lean_mark_persistent(l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__7);
482
+ l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__8 = _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__8();
483
+ lean_mark_persistent(l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__8);
484
+ l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__9 = _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__9();
485
+ lean_mark_persistent(l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__9);
486
+ l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__10 = _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__10();
487
+ lean_mark_persistent(l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__10);
488
+ l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__11 = _init_l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__11();
489
+ lean_mark_persistent(l___aux__REPL__Util__Path______elabRules__termCompile__time__search__path_x25__1___closed__11);
490
+ return lean_io_result_mk_ok(lean_box(0));
491
+ }
492
+ #ifdef __cplusplus
493
+ }
494
+ #endif
.lake/build/ir/REPL/Util/Path.c.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 10432507961615664798
.lake/build/ir/REPL/Util/Path.c.o ADDED
Binary file (12.2 kB). View file
 
.lake/build/ir/REPL/Util/Path.c.o.hash ADDED
@@ -0,0 +1 @@
 
 
1
+ 10141218349971261900
.lake/build/ir/REPL/Util/Path.c.o.trace ADDED
@@ -0,0 +1 @@
 
 
1
+ 11998194603327660164
.lake/build/ir/REPL/Util/Pickle.c ADDED
@@ -0,0 +1,709 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Lean compiler output
2
+ // Module: REPL.Util.Pickle
3
+ // Imports: Init Lean.Environment
4
+ #include <lean/lean.h>
5
+ #if defined(__clang__)
6
+ #pragma clang diagnostic ignored "-Wunused-parameter"
7
+ #pragma clang diagnostic ignored "-Wunused-label"
8
+ #elif defined(__GNUC__) && !defined(__CLANG__)
9
+ #pragma GCC diagnostic ignored "-Wunused-parameter"
10
+ #pragma GCC diagnostic ignored "-Wunused-label"
11
+ #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
12
+ #endif
13
+ #ifdef __cplusplus
14
+ extern "C" {
15
+ #endif
16
+ LEAN_EXPORT lean_object* l_pickle___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
17
+ LEAN_EXPORT lean_object* l_pickle_unsafe__1___rarg(lean_object*);
18
+ lean_object* lean_read_module_data(lean_object*, lean_object*);
19
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__20;
20
+ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
21
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__21;
22
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
23
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__6;
24
+ LEAN_EXPORT lean_object* l_withUnpickle(lean_object*);
25
+ LEAN_EXPORT lean_object* l_unpickle(lean_object*);
26
+ LEAN_EXPORT lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8_;
27
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__13;
28
+ lean_object* lean_array_push(lean_object*, lean_object*);
29
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__18;
30
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__19;
31
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__3;
32
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__12;
33
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__1;
34
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__14;
35
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__15;
36
+ LEAN_EXPORT lean_object* l_pickle___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
37
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__27;
38
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
39
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__17;
40
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__16;
41
+ LEAN_EXPORT lean_object* l_pickle(lean_object*);
42
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__22;
43
+ LEAN_EXPORT lean_object* l_unpickle___rarg(lean_object*, lean_object*);
44
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__29;
45
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg___lambda__2(size_t, lean_object*, lean_object*, lean_object*, lean_object*);
46
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
47
+ lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
48
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__4;
49
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
50
+ LEAN_EXPORT lean_object* l_pickle_unsafe__1___rarg___boxed(lean_object*);
51
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__5;
52
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__11;
53
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__25;
54
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__9;
55
+ LEAN_EXPORT lean_object* l_unpickle___rarg___boxed(lean_object*, lean_object*);
56
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__24;
57
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__10;
58
+ lean_object* l_Lean_CompactedRegion_free___boxed(lean_object*, lean_object*);
59
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__26;
60
+ lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*);
61
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__7;
62
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__23;
63
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__2;
64
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__8;
65
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
66
+ LEAN_EXPORT lean_object* l_pickle_unsafe__1(lean_object*);
67
+ static lean_object* l___auto____x40_REPL_Util_Pickle___hyg_8____closed__28;
68
+ lean_object* lean_save_module_data(lean_object*, lean_object*, lean_object*, lean_object*);
69
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__1() {
70
+ _start:
71
+ {
72
+ lean_object* x_1;
73
+ x_1 = lean_mk_string_from_bytes("Lean", 4);
74
+ return x_1;
75
+ }
76
+ }
77
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__2() {
78
+ _start:
79
+ {
80
+ lean_object* x_1;
81
+ x_1 = lean_mk_string_from_bytes("Parser", 6);
82
+ return x_1;
83
+ }
84
+ }
85
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__3() {
86
+ _start:
87
+ {
88
+ lean_object* x_1;
89
+ x_1 = lean_mk_string_from_bytes("Tactic", 6);
90
+ return x_1;
91
+ }
92
+ }
93
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__4() {
94
+ _start:
95
+ {
96
+ lean_object* x_1;
97
+ x_1 = lean_mk_string_from_bytes("tacticSeq", 9);
98
+ return x_1;
99
+ }
100
+ }
101
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__5() {
102
+ _start:
103
+ {
104
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
105
+ x_1 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__1;
106
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__2;
107
+ x_3 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__3;
108
+ x_4 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__4;
109
+ x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
110
+ return x_5;
111
+ }
112
+ }
113
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__6() {
114
+ _start:
115
+ {
116
+ lean_object* x_1; lean_object* x_2;
117
+ x_1 = lean_unsigned_to_nat(0u);
118
+ x_2 = lean_mk_empty_array_with_capacity(x_1);
119
+ return x_2;
120
+ }
121
+ }
122
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__7() {
123
+ _start:
124
+ {
125
+ lean_object* x_1;
126
+ x_1 = lean_mk_string_from_bytes("tacticSeq1Indented", 18);
127
+ return x_1;
128
+ }
129
+ }
130
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__8() {
131
+ _start:
132
+ {
133
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
134
+ x_1 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__1;
135
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__2;
136
+ x_3 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__3;
137
+ x_4 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__7;
138
+ x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
139
+ return x_5;
140
+ }
141
+ }
142
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__9() {
143
+ _start:
144
+ {
145
+ lean_object* x_1;
146
+ x_1 = lean_mk_string_from_bytes("null", 4);
147
+ return x_1;
148
+ }
149
+ }
150
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__10() {
151
+ _start:
152
+ {
153
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
154
+ x_1 = lean_box(0);
155
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__9;
156
+ x_3 = l_Lean_Name_str___override(x_1, x_2);
157
+ return x_3;
158
+ }
159
+ }
160
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__11() {
161
+ _start:
162
+ {
163
+ lean_object* x_1;
164
+ x_1 = lean_mk_string_from_bytes("exact", 5);
165
+ return x_1;
166
+ }
167
+ }
168
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__12() {
169
+ _start:
170
+ {
171
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
172
+ x_1 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__1;
173
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__2;
174
+ x_3 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__3;
175
+ x_4 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__11;
176
+ x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
177
+ return x_5;
178
+ }
179
+ }
180
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__13() {
181
+ _start:
182
+ {
183
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
184
+ x_1 = lean_box(2);
185
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__11;
186
+ x_3 = lean_alloc_ctor(2, 2, 0);
187
+ lean_ctor_set(x_3, 0, x_1);
188
+ lean_ctor_set(x_3, 1, x_2);
189
+ return x_3;
190
+ }
191
+ }
192
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__14() {
193
+ _start:
194
+ {
195
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
196
+ x_1 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__6;
197
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__13;
198
+ x_3 = lean_array_push(x_1, x_2);
199
+ return x_3;
200
+ }
201
+ }
202
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__15() {
203
+ _start:
204
+ {
205
+ lean_object* x_1;
206
+ x_1 = lean_mk_string_from_bytes("Term", 4);
207
+ return x_1;
208
+ }
209
+ }
210
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__16() {
211
+ _start:
212
+ {
213
+ lean_object* x_1;
214
+ x_1 = lean_mk_string_from_bytes("declName", 8);
215
+ return x_1;
216
+ }
217
+ }
218
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__17() {
219
+ _start:
220
+ {
221
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
222
+ x_1 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__1;
223
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__2;
224
+ x_3 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__15;
225
+ x_4 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__16;
226
+ x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
227
+ return x_5;
228
+ }
229
+ }
230
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__18() {
231
+ _start:
232
+ {
233
+ lean_object* x_1;
234
+ x_1 = lean_mk_string_from_bytes("decl_name%", 10);
235
+ return x_1;
236
+ }
237
+ }
238
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__19() {
239
+ _start:
240
+ {
241
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
242
+ x_1 = lean_box(2);
243
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__18;
244
+ x_3 = lean_alloc_ctor(2, 2, 0);
245
+ lean_ctor_set(x_3, 0, x_1);
246
+ lean_ctor_set(x_3, 1, x_2);
247
+ return x_3;
248
+ }
249
+ }
250
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__20() {
251
+ _start:
252
+ {
253
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
254
+ x_1 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__6;
255
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__19;
256
+ x_3 = lean_array_push(x_1, x_2);
257
+ return x_3;
258
+ }
259
+ }
260
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__21() {
261
+ _start:
262
+ {
263
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
264
+ x_1 = lean_box(2);
265
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__17;
266
+ x_3 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__20;
267
+ x_4 = lean_alloc_ctor(1, 3, 0);
268
+ lean_ctor_set(x_4, 0, x_1);
269
+ lean_ctor_set(x_4, 1, x_2);
270
+ lean_ctor_set(x_4, 2, x_3);
271
+ return x_4;
272
+ }
273
+ }
274
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__22() {
275
+ _start:
276
+ {
277
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
278
+ x_1 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__14;
279
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__21;
280
+ x_3 = lean_array_push(x_1, x_2);
281
+ return x_3;
282
+ }
283
+ }
284
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__23() {
285
+ _start:
286
+ {
287
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
288
+ x_1 = lean_box(2);
289
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__12;
290
+ x_3 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__22;
291
+ x_4 = lean_alloc_ctor(1, 3, 0);
292
+ lean_ctor_set(x_4, 0, x_1);
293
+ lean_ctor_set(x_4, 1, x_2);
294
+ lean_ctor_set(x_4, 2, x_3);
295
+ return x_4;
296
+ }
297
+ }
298
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__24() {
299
+ _start:
300
+ {
301
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
302
+ x_1 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__6;
303
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__23;
304
+ x_3 = lean_array_push(x_1, x_2);
305
+ return x_3;
306
+ }
307
+ }
308
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__25() {
309
+ _start:
310
+ {
311
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
312
+ x_1 = lean_box(2);
313
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__10;
314
+ x_3 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__24;
315
+ x_4 = lean_alloc_ctor(1, 3, 0);
316
+ lean_ctor_set(x_4, 0, x_1);
317
+ lean_ctor_set(x_4, 1, x_2);
318
+ lean_ctor_set(x_4, 2, x_3);
319
+ return x_4;
320
+ }
321
+ }
322
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__26() {
323
+ _start:
324
+ {
325
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
326
+ x_1 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__6;
327
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__25;
328
+ x_3 = lean_array_push(x_1, x_2);
329
+ return x_3;
330
+ }
331
+ }
332
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__27() {
333
+ _start:
334
+ {
335
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
336
+ x_1 = lean_box(2);
337
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__8;
338
+ x_3 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__26;
339
+ x_4 = lean_alloc_ctor(1, 3, 0);
340
+ lean_ctor_set(x_4, 0, x_1);
341
+ lean_ctor_set(x_4, 1, x_2);
342
+ lean_ctor_set(x_4, 2, x_3);
343
+ return x_4;
344
+ }
345
+ }
346
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__28() {
347
+ _start:
348
+ {
349
+ lean_object* x_1; lean_object* x_2; lean_object* x_3;
350
+ x_1 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__6;
351
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__27;
352
+ x_3 = lean_array_push(x_1, x_2);
353
+ return x_3;
354
+ }
355
+ }
356
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__29() {
357
+ _start:
358
+ {
359
+ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
360
+ x_1 = lean_box(2);
361
+ x_2 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__5;
362
+ x_3 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__28;
363
+ x_4 = lean_alloc_ctor(1, 3, 0);
364
+ lean_ctor_set(x_4, 0, x_1);
365
+ lean_ctor_set(x_4, 1, x_2);
366
+ lean_ctor_set(x_4, 2, x_3);
367
+ return x_4;
368
+ }
369
+ }
370
+ static lean_object* _init_l___auto____x40_REPL_Util_Pickle___hyg_8_() {
371
+ _start:
372
+ {
373
+ lean_object* x_1;
374
+ x_1 = l___auto____x40_REPL_Util_Pickle___hyg_8____closed__29;
375
+ return x_1;
376
+ }
377
+ }
378
+ LEAN_EXPORT lean_object* l_pickle_unsafe__1___rarg(lean_object* x_1) {
379
+ _start:
380
+ {
381
+ lean_inc(x_1);
382
+ return x_1;
383
+ }
384
+ }
385
+ LEAN_EXPORT lean_object* l_pickle_unsafe__1(lean_object* x_1) {
386
+ _start:
387
+ {
388
+ lean_object* x_2;
389
+ x_2 = lean_alloc_closure((void*)(l_pickle_unsafe__1___rarg___boxed), 1, 0);
390
+ return x_2;
391
+ }
392
+ }
393
+ LEAN_EXPORT lean_object* l_pickle_unsafe__1___rarg___boxed(lean_object* x_1) {
394
+ _start:
395
+ {
396
+ lean_object* x_2;
397
+ x_2 = l_pickle_unsafe__1___rarg(x_1);
398
+ lean_dec(x_1);
399
+ return x_2;
400
+ }
401
+ }
402
+ LEAN_EXPORT lean_object* l_pickle___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
403
+ _start:
404
+ {
405
+ lean_object* x_5;
406
+ x_5 = lean_save_module_data(x_1, x_3, x_2, x_4);
407
+ return x_5;
408
+ }
409
+ }
410
+ LEAN_EXPORT lean_object* l_pickle(lean_object* x_1) {
411
+ _start:
412
+ {
413
+ lean_object* x_2;
414
+ x_2 = lean_alloc_closure((void*)(l_pickle___rarg___boxed), 4, 0);
415
+ return x_2;
416
+ }
417
+ }
418
+ LEAN_EXPORT lean_object* l_pickle___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
419
+ _start:
420
+ {
421
+ lean_object* x_5;
422
+ x_5 = l_pickle___rarg(x_1, x_2, x_3, x_4);
423
+ lean_dec(x_3);
424
+ lean_dec(x_2);
425
+ lean_dec(x_1);
426
+ return x_5;
427
+ }
428
+ }
429
+ LEAN_EXPORT lean_object* l_unpickle___rarg(lean_object* x_1, lean_object* x_2) {
430
+ _start:
431
+ {
432
+ lean_object* x_3;
433
+ x_3 = lean_read_module_data(x_1, x_2);
434
+ if (lean_obj_tag(x_3) == 0)
435
+ {
436
+ uint8_t x_4;
437
+ x_4 = !lean_is_exclusive(x_3);
438
+ if (x_4 == 0)
439
+ {
440
+ lean_object* x_5; uint8_t x_6;
441
+ x_5 = lean_ctor_get(x_3, 0);
442
+ x_6 = !lean_is_exclusive(x_5);
443
+ if (x_6 == 0)
444
+ {
445
+ return x_3;
446
+ }
447
+ else
448
+ {
449
+ lean_object* x_7; lean_object* x_8; lean_object* x_9;
450
+ x_7 = lean_ctor_get(x_5, 0);
451
+ x_8 = lean_ctor_get(x_5, 1);
452
+ lean_inc(x_8);
453
+ lean_inc(x_7);
454
+ lean_dec(x_5);
455
+ x_9 = lean_alloc_ctor(0, 2, 0);
456
+ lean_ctor_set(x_9, 0, x_7);
457
+ lean_ctor_set(x_9, 1, x_8);
458
+ lean_ctor_set(x_3, 0, x_9);
459
+ return x_3;
460
+ }
461
+ }
462
+ else
463
+ {
464
+ lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
465
+ x_10 = lean_ctor_get(x_3, 0);
466
+ x_11 = lean_ctor_get(x_3, 1);
467
+ lean_inc(x_11);
468
+ lean_inc(x_10);
469
+ lean_dec(x_3);
470
+ x_12 = lean_ctor_get(x_10, 0);
471
+ lean_inc(x_12);
472
+ x_13 = lean_ctor_get(x_10, 1);
473
+ lean_inc(x_13);
474
+ if (lean_is_exclusive(x_10)) {
475
+ lean_ctor_release(x_10, 0);
476
+ lean_ctor_release(x_10, 1);
477
+ x_14 = x_10;
478
+ } else {
479
+ lean_dec_ref(x_10);
480
+ x_14 = lean_box(0);
481
+ }
482
+ if (lean_is_scalar(x_14)) {
483
+ x_15 = lean_alloc_ctor(0, 2, 0);
484
+ } else {
485
+ x_15 = x_14;
486
+ }
487
+ lean_ctor_set(x_15, 0, x_12);
488
+ lean_ctor_set(x_15, 1, x_13);
489
+ x_16 = lean_alloc_ctor(0, 2, 0);
490
+ lean_ctor_set(x_16, 0, x_15);
491
+ lean_ctor_set(x_16, 1, x_11);
492
+ return x_16;
493
+ }
494
+ }
495
+ else
496
+ {
497
+ uint8_t x_17;
498
+ x_17 = !lean_is_exclusive(x_3);
499
+ if (x_17 == 0)
500
+ {
501
+ return x_3;
502
+ }
503
+ else
504
+ {
505
+ lean_object* x_18; lean_object* x_19; lean_object* x_20;
506
+ x_18 = lean_ctor_get(x_3, 0);
507
+ x_19 = lean_ctor_get(x_3, 1);
508
+ lean_inc(x_19);
509
+ lean_inc(x_18);
510
+ lean_dec(x_3);
511
+ x_20 = lean_alloc_ctor(1, 2, 0);
512
+ lean_ctor_set(x_20, 0, x_18);
513
+ lean_ctor_set(x_20, 1, x_19);
514
+ return x_20;
515
+ }
516
+ }
517
+ }
518
+ }
519
+ LEAN_EXPORT lean_object* l_unpickle(lean_object* x_1) {
520
+ _start:
521
+ {
522
+ lean_object* x_2;
523
+ x_2 = lean_alloc_closure((void*)(l_unpickle___rarg___boxed), 2, 0);
524
+ return x_2;
525
+ }
526
+ }
527
+ LEAN_EXPORT lean_object* l_unpickle___rarg___boxed(lean_object* x_1, lean_object* x_2) {
528
+ _start:
529
+ {
530
+ lean_object* x_3;
531
+ x_3 = l_unpickle___rarg(x_1, x_2);
532
+ lean_dec(x_1);
533
+ return x_3;
534
+ }
535
+ }
536
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
537
+ _start:
538
+ {
539
+ lean_object* x_4; lean_object* x_5; lean_object* x_6;
540
+ x_4 = lean_ctor_get(x_1, 0);
541
+ lean_inc(x_4);
542
+ lean_dec(x_1);
543
+ x_5 = lean_ctor_get(x_4, 1);
544
+ lean_inc(x_5);
545
+ lean_dec(x_4);
546
+ x_6 = lean_apply_2(x_5, lean_box(0), x_2);
547
+ return x_6;
548
+ }
549
+ }
550
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg___lambda__2(size_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
551
+ _start:
552
+ {
553
+ lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
554
+ x_6 = lean_box_usize(x_1);
555
+ x_7 = lean_alloc_closure((void*)(l_Lean_CompactedRegion_free___boxed), 2, 1);
556
+ lean_closure_set(x_7, 0, x_6);
557
+ x_8 = lean_apply_2(x_2, lean_box(0), x_7);
558
+ x_9 = lean_alloc_closure((void*)(l_withUnpickle___rarg___lambda__1___boxed), 3, 2);
559
+ lean_closure_set(x_9, 0, x_3);
560
+ lean_closure_set(x_9, 1, x_5);
561
+ x_10 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_8, x_9);
562
+ return x_10;
563
+ }
564
+ }
565
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
566
+ _start:
567
+ {
568
+ lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
569
+ x_6 = lean_ctor_get(x_5, 0);
570
+ lean_inc(x_6);
571
+ x_7 = lean_ctor_get(x_5, 1);
572
+ lean_inc(x_7);
573
+ lean_dec(x_5);
574
+ x_8 = lean_apply_1(x_1, x_6);
575
+ lean_inc(x_4);
576
+ x_9 = lean_alloc_closure((void*)(l_withUnpickle___rarg___lambda__2___boxed), 5, 4);
577
+ lean_closure_set(x_9, 0, x_7);
578
+ lean_closure_set(x_9, 1, x_2);
579
+ lean_closure_set(x_9, 2, x_3);
580
+ lean_closure_set(x_9, 3, x_4);
581
+ x_10 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_8, x_9);
582
+ return x_10;
583
+ }
584
+ }
585
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
586
+ _start:
587
+ {
588
+ lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
589
+ x_7 = lean_ctor_get(x_1, 1);
590
+ lean_inc(x_7);
591
+ x_8 = lean_alloc_closure((void*)(l_unpickle___rarg___boxed), 2, 1);
592
+ lean_closure_set(x_8, 0, x_5);
593
+ lean_inc(x_2);
594
+ x_9 = lean_apply_2(x_2, lean_box(0), x_8);
595
+ lean_inc(x_7);
596
+ x_10 = lean_alloc_closure((void*)(l_withUnpickle___rarg___lambda__3), 5, 4);
597
+ lean_closure_set(x_10, 0, x_6);
598
+ lean_closure_set(x_10, 1, x_2);
599
+ lean_closure_set(x_10, 2, x_1);
600
+ lean_closure_set(x_10, 3, x_7);
601
+ x_11 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_9, x_10);
602
+ return x_11;
603
+ }
604
+ }
605
+ LEAN_EXPORT lean_object* l_withUnpickle(lean_object* x_1) {
606
+ _start:
607
+ {
608
+ lean_object* x_2;
609
+ x_2 = lean_alloc_closure((void*)(l_withUnpickle___rarg), 6, 0);
610
+ return x_2;
611
+ }
612
+ }
613
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
614
+ _start:
615
+ {
616
+ lean_object* x_4;
617
+ x_4 = l_withUnpickle___rarg___lambda__1(x_1, x_2, x_3);
618
+ lean_dec(x_3);
619
+ return x_4;
620
+ }
621
+ }
622
+ LEAN_EXPORT lean_object* l_withUnpickle___rarg___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
623
+ _start:
624
+ {
625
+ size_t x_6; lean_object* x_7;
626
+ x_6 = lean_unbox_usize(x_1);
627
+ lean_dec(x_1);
628
+ x_7 = l_withUnpickle___rarg___lambda__2(x_6, x_2, x_3, x_4, x_5);
629
+ return x_7;
630
+ }
631
+ }
632
+ lean_object* initialize_Init(uint8_t builtin, lean_object*);
633
+ lean_object* initialize_Lean_Environment(uint8_t builtin, lean_object*);
634
+ static bool _G_initialized = false;
635
+ LEAN_EXPORT lean_object* initialize_REPL_Util_Pickle(uint8_t builtin, lean_object* w) {
636
+ lean_object * res;
637
+ if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
638
+ _G_initialized = true;
639
+ res = initialize_Init(builtin, lean_io_mk_world());
640
+ if (lean_io_result_is_error(res)) return res;
641
+ lean_dec_ref(res);
642
+ res = initialize_Lean_Environment(builtin, lean_io_mk_world());
643
+ if (lean_io_result_is_error(res)) return res;
644
+ lean_dec_ref(res);
645
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__1 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__1();
646
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__1);
647
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__2 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__2();
648
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__2);
649
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__3 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__3();
650
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__3);
651
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__4 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__4();
652
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__4);
653
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__5 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__5();
654
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__5);
655
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__6 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__6();
656
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__6);
657
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__7 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__7();
658
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__7);
659
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__8 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__8();
660
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__8);
661
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__9 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__9();
662
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__9);
663
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__10 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__10();
664
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__10);
665
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__11 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__11();
666
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__11);
667
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__12 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__12();
668
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__12);
669
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__13 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__13();
670
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__13);
671
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__14 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__14();
672
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__14);
673
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__15 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__15();
674
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__15);
675
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__16 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__16();
676
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__16);
677
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__17 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__17();
678
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__17);
679
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__18 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__18();
680
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__18);
681
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__19 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__19();
682
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__19);
683
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__20 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__20();
684
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__20);
685
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__21 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__21();
686
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__21);
687
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__22 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__22();
688
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__22);
689
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__23 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__23();
690
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__23);
691
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__24 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__24();
692
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__24);
693
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__25 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__25();
694
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__25);
695
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__26 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__26();
696
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__26);
697
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__27 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__27();
698
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__27);
699
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__28 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__28();
700
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__28);
701
+ l___auto____x40_REPL_Util_Pickle___hyg_8____closed__29 = _init_l___auto____x40_REPL_Util_Pickle___hyg_8____closed__29();
702
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8____closed__29);
703
+ l___auto____x40_REPL_Util_Pickle___hyg_8_ = _init_l___auto____x40_REPL_Util_Pickle___hyg_8_();
704
+ lean_mark_persistent(l___auto____x40_REPL_Util_Pickle___hyg_8_);
705
+ return lean_io_result_mk_ok(lean_box(0));
706
+ }
707
+ #ifdef __cplusplus
708
+ }
709
+ #endif