Skip to content

Commit 62ea34f

Browse files
RemyDegenneRemyDegenne
committed
junk values; characterization graph
1 parent cbf9563 commit 62ea34f

262 files changed

Lines changed: 46271 additions & 160 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎JunkValues/.lake/build/ir/JunkValues.c‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
// Lean compiler output
2+
// Module: JunkValues
3+
// Imports: public import Init public meta import Init public import JunkValues.Rule public import JunkValues.Registry public import JunkValues.RuleSet public import JunkValues.Report public import JunkValues.Guard public import JunkValues.Scan public import JunkValues.Frontend public import JunkValues.Elab
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* runtime_initialize_Init(uint8_t builtin);
17+
lean_object* runtime_initialize_JunkValues_JunkValues_Rule(uint8_t builtin);
18+
lean_object* runtime_initialize_JunkValues_JunkValues_Registry(uint8_t builtin);
19+
lean_object* runtime_initialize_JunkValues_JunkValues_RuleSet(uint8_t builtin);
20+
lean_object* runtime_initialize_JunkValues_JunkValues_Report(uint8_t builtin);
21+
lean_object* runtime_initialize_JunkValues_JunkValues_Guard(uint8_t builtin);
22+
lean_object* runtime_initialize_JunkValues_JunkValues_Scan(uint8_t builtin);
23+
lean_object* runtime_initialize_JunkValues_JunkValues_Frontend(uint8_t builtin);
24+
lean_object* runtime_initialize_JunkValues_JunkValues_Elab(uint8_t builtin);
25+
static bool _G_runtime_initialized = false;
26+
LEAN_EXPORT lean_object* runtime_initialize_JunkValues_JunkValues(uint8_t builtin) {
27+
lean_object * res;
28+
if (_G_runtime_initialized) return lean_io_result_mk_ok(lean_box(0));
29+
_G_runtime_initialized = true;
30+
res = runtime_initialize_Init(builtin);
31+
if (lean_io_result_is_error(res)) return res;
32+
lean_dec_ref(res);
33+
res = runtime_initialize_JunkValues_JunkValues_Rule(builtin);
34+
if (lean_io_result_is_error(res)) return res;
35+
lean_dec_ref(res);
36+
res = runtime_initialize_JunkValues_JunkValues_Registry(builtin);
37+
if (lean_io_result_is_error(res)) return res;
38+
lean_dec_ref(res);
39+
res = runtime_initialize_JunkValues_JunkValues_RuleSet(builtin);
40+
if (lean_io_result_is_error(res)) return res;
41+
lean_dec_ref(res);
42+
res = runtime_initialize_JunkValues_JunkValues_Report(builtin);
43+
if (lean_io_result_is_error(res)) return res;
44+
lean_dec_ref(res);
45+
res = runtime_initialize_JunkValues_JunkValues_Guard(builtin);
46+
if (lean_io_result_is_error(res)) return res;
47+
lean_dec_ref(res);
48+
res = runtime_initialize_JunkValues_JunkValues_Scan(builtin);
49+
if (lean_io_result_is_error(res)) return res;
50+
lean_dec_ref(res);
51+
res = runtime_initialize_JunkValues_JunkValues_Frontend(builtin);
52+
if (lean_io_result_is_error(res)) return res;
53+
lean_dec_ref(res);
54+
res = runtime_initialize_JunkValues_JunkValues_Elab(builtin);
55+
if (lean_io_result_is_error(res)) return res;
56+
lean_dec_ref(res);
57+
return lean_io_result_mk_ok(lean_box(0));
58+
}
59+
lean_object* runtime_initialize_Init(uint8_t builtin);
60+
static bool _G_meta_initialized = false;
61+
LEAN_EXPORT lean_object* meta_initialize_JunkValues_JunkValues(uint8_t builtin) {
62+
lean_object * res;
63+
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
64+
_G_meta_initialized = true;
65+
res = runtime_initialize_Init(builtin);
66+
if (lean_io_result_is_error(res)) return res;
67+
lean_dec_ref(res);
68+
return lean_io_result_mk_ok(lean_box(0));
69+
}
70+
lean_object* initialize_Init(uint8_t builtin);
71+
lean_object* initialize_Init(uint8_t builtin);
72+
lean_object* initialize_JunkValues_JunkValues_Rule(uint8_t builtin);
73+
lean_object* initialize_JunkValues_JunkValues_Registry(uint8_t builtin);
74+
lean_object* initialize_JunkValues_JunkValues_RuleSet(uint8_t builtin);
75+
lean_object* initialize_JunkValues_JunkValues_Report(uint8_t builtin);
76+
lean_object* initialize_JunkValues_JunkValues_Guard(uint8_t builtin);
77+
lean_object* initialize_JunkValues_JunkValues_Scan(uint8_t builtin);
78+
lean_object* initialize_JunkValues_JunkValues_Frontend(uint8_t builtin);
79+
lean_object* initialize_JunkValues_JunkValues_Elab(uint8_t builtin);
80+
static bool _G_initialized = false;
81+
LEAN_EXPORT lean_object* initialize_JunkValues_JunkValues(uint8_t builtin) {
82+
lean_object * res;
83+
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
84+
_G_initialized = true;
85+
res = initialize_Init(builtin);
86+
if (lean_io_result_is_error(res)) return res;
87+
lean_dec_ref(res);
88+
res = initialize_Init(builtin);
89+
if (lean_io_result_is_error(res)) return res;
90+
lean_dec_ref(res);
91+
res = initialize_JunkValues_JunkValues_Rule(builtin);
92+
if (lean_io_result_is_error(res)) return res;
93+
lean_dec_ref(res);
94+
res = initialize_JunkValues_JunkValues_Registry(builtin);
95+
if (lean_io_result_is_error(res)) return res;
96+
lean_dec_ref(res);
97+
res = initialize_JunkValues_JunkValues_RuleSet(builtin);
98+
if (lean_io_result_is_error(res)) return res;
99+
lean_dec_ref(res);
100+
res = initialize_JunkValues_JunkValues_Report(builtin);
101+
if (lean_io_result_is_error(res)) return res;
102+
lean_dec_ref(res);
103+
res = initialize_JunkValues_JunkValues_Guard(builtin);
104+
if (lean_io_result_is_error(res)) return res;
105+
lean_dec_ref(res);
106+
res = initialize_JunkValues_JunkValues_Scan(builtin);
107+
if (lean_io_result_is_error(res)) return res;
108+
lean_dec_ref(res);
109+
res = initialize_JunkValues_JunkValues_Frontend(builtin);
110+
if (lean_io_result_is_error(res)) return res;
111+
lean_dec_ref(res);
112+
res = initialize_JunkValues_JunkValues_Elab(builtin);
113+
if (lean_io_result_is_error(res)) return res;
114+
lean_dec_ref(res);
115+
res = runtime_initialize_JunkValues_JunkValues(builtin);
116+
if (lean_io_result_is_error(res)) return res;
117+
lean_dec_ref(res);
118+
res = meta_initialize_JunkValues_JunkValues(builtin);
119+
if (lean_io_result_is_error(res)) return res;
120+
lean_dec_ref(res);
121+
return initialize_JunkValues_JunkValues(builtin);
122+
}
123+
#ifdef __cplusplus
124+
}
125+
#endif

‎JunkValues/.lake/build/ir/JunkValues.c.hash‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
695983013032fa9b

‎JunkValues/.lake/build/ir/JunkValues.setup.json‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
{"plugins": [],
2+
"package": "JunkValues",
3+
"options": {},
4+
"name": "JunkValues",
5+
"isModule": true,
6+
"importArts":
7+
{"JunkValues.Scan":
8+
[["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Scan.olean",
9+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Scan.olean.server"],
10+
["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Scan.ir.sig",
11+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Scan.ir"]],
12+
"JunkValues.RuleSet":
13+
[["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/RuleSet.olean",
14+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/RuleSet.olean.server"],
15+
["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/RuleSet.ir.sig",
16+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/RuleSet.ir"]],
17+
"JunkValues.Rule":
18+
[["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Rule.olean",
19+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Rule.olean.server"],
20+
["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Rule.ir.sig",
21+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Rule.ir"]],
22+
"JunkValues.Report":
23+
[["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Report.olean",
24+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Report.olean.server"],
25+
["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Report.ir.sig",
26+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Report.ir"]],
27+
"JunkValues.Registry":
28+
[["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Registry.olean",
29+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Registry.olean.server"],
30+
["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Registry.ir.sig",
31+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Registry.ir"]],
32+
"JunkValues.Guard":
33+
[["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Guard.olean",
34+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Guard.olean.server"],
35+
["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Guard.ir.sig",
36+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Guard.ir"]],
37+
"JunkValues.Frontend":
38+
[["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Frontend.olean",
39+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Frontend.olean.server"],
40+
["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Frontend.ir.sig",
41+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Frontend.ir"]],
42+
"JunkValues.Elab":
43+
[["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Elab.olean",
44+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Elab.olean.server"],
45+
["/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Elab.ir.sig",
46+
"/home/rdegenne/Documents/Lean/exposition/JunkValues/.lake/build/lib/lean/JunkValues/Elab.ir"]]},
47+
"dynlibs": []}

0 commit comments

Comments
 (0)