max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Compiler/LCNF
History
Henrik Böving 85ce814689
fix: constant folding for UIntX (#10495) 
This PR fixes constant folding for UIntX in the code generator. This
optimization was previously simply dead code due to the way that uint
literals are encoded.
2025-09-22 10:06:24 +00:00
..
Simp fix: constant folding for UIntX (#10495) 2025-09-22 10:06:24 +00:00
AlphaEqv.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
AuxDeclCache.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
BaseTypes.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Basic.lean fix: do not allow access to private primitives in public scope (#9890) 2025-08-14 15:34:54 +00:00
Bind.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Check.lean chore: use ofConstName in error messages (#10121) 2025-08-25 23:20:36 +00:00
Closure.lean perf: during specialization, don't abstract all local fun decls under binders (#9596) 2025-07-28 17:36:43 +00:00
CompatibleTypes.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
CompilerM.lean fix: erase dependencies on let-bound fvars in internalizeCode (#9922) 2025-08-15 01:52:47 +00:00
ConfigOptions.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
CSE.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
DeclHash.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
DependsOn.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ElimDead.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ElimDeadBranches.lean fix: correctly handle non-Nat literal types in LCNF elimDeadBranches (#9703) 2025-08-05 02:14:07 +00:00
ExtractClosed.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
FixedParams.lean chore: don't check type of erased arguments in FixedParams analysis (#9602) 2025-08-05 02:41:36 +00:00
FloatLetIn.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
FVarUtil.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
InferType.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Internalize.lean fix: erase dependencies on let-bound fvars in internalizeCode (#9922) 2025-08-15 01:52:47 +00:00
JoinPoints.lean chore: make Compiler.findJoinPoints trace messages more useful (#9668) 2025-08-01 17:42:32 +00:00
LambdaLifting.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
LCtx.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Level.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Main.lean feat: overhaul meta system (#10362) 2025-09-17 21:04:29 +00:00
MonadScope.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
MonoTypes.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
OtherDecl.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Passes.lean feat: overhaul meta system (#10362) 2025-09-17 21:04:29 +00:00
PassManager.lean refactor: split the LCNF pass list into separate base/mono lists (#9816) 2025-08-10 04:23:19 +00:00
PhaseExt.lean chore: remove support for unused arity specification in ExternAttrData (#9552) 2025-07-25 21:23:56 +00:00
PrettyPrinter.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Probing.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
PullFunDecls.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
PullLetDecls.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ReduceArity.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ReduceJpArity.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Renaming.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ScopeM.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Simp.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Specialize.lean perf: inline dependent instances into specialized decls (#10080) 2025-08-24 00:12:27 +00:00
SpecInfo.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
StructProjCases.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Testing.lean refactor: split the LCNF pass list into separate base/mono lists (#9816) 2025-08-10 04:23:19 +00:00
ToDecl.lean chore: use ofConstName in error messages (#10121) 2025-08-25 23:20:36 +00:00
ToExpr.lean fix: overeager specialisation reuse in codegen (#10429) 2025-09-17 17:35:40 +00:00
ToLCNF.lean chore: kernel changes ahead of String redefinition (#10330) 2025-09-17 09:12:07 +00:00
ToMono.lean fix: incorporate info from _redArg decls for noncomputable check (#10040) 2025-08-22 01:02:40 +00:00
Types.lean fix: check that compiler does not infer inconsistent types between modules (#10418) 2025-09-19 12:36:47 +00:00
Util.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Visibility.lean feat: overhaul meta system (#10362) 2025-09-17 21:04:29 +00:00