lean4-htt/src/Lean/Compiler/LCNF
2022-10-07 16:07:17 -07:00
..
Simp feat: automatic extension names 2022-10-06 17:19:30 -07:00
AlphaEqv.lean feat: alpha equivalence for LCNF code 2022-09-05 08:06:05 -07:00
BaseTypes.lean feat: detect trivial structures and add extension for storing mono phase types 2022-10-05 08:55:44 -07:00
Basic.lean feat: extend join point context pass 2022-10-03 17:03:22 -07:00
Bind.lean feat: detect trivial structures and add extension for storing mono phase types 2022-10-05 08:55:44 -07:00
Check.lean fix: constructor parameter validation for mono phase 2022-10-06 06:57:06 -07:00
Closure.lean refactor: add Closure.lean 2022-10-07 15:56:10 -07:00
CompilerM.lean refactor: add LCNF/Internalize.lean 2022-10-03 09:18:11 -07:00
ConfigOptions.lean feat: configuration options for the code generator 2022-09-27 16:26:49 -07:00
CSE.lean chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
DependsOn.lean feat: add CodeDecl.dependsOn 2022-10-03 19:36:26 -07:00
ElimDead.lean refactor: LCNF local context 2022-09-14 19:25:16 -07:00
FixedArgs.lean feat: treat erased arguments as fixed arguments 2022-09-11 20:19:44 -07:00
ForEachExpr.lean feat: LCNF Code.forEachExpr and Decl.forEachExpr 2022-09-29 15:50:49 -07:00
InferType.lean feat: detect trivial structures and add extension for storing mono phase types 2022-10-05 08:55:44 -07:00
Internalize.lean refactor: merge lcAny and lcErased 2022-10-05 04:46:52 -07:00
JoinPoints.lean feat: extend join point context pass 2022-10-03 17:03:22 -07:00
LCtx.lean chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
Level.lean chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
Main.lean feat: display mono phase code 2022-10-06 07:48:59 -07:00
MonadScope.lean refactor: add MonadScope class 2022-10-07 14:59:59 -07:00
MonoTypes.lean fix: bug at toMonoType 2022-10-06 07:41:36 -07:00
OtherDecl.lean feat: detect trivial structures and add extension for storing mono phase types 2022-10-05 08:55:44 -07:00
Passes.lean feat: automatic extension names 2022-10-06 17:19:30 -07:00
PassManager.lean feat: add phaseOut field to Pass 2022-10-06 03:29:21 -07:00
PhaseExt.lean feat: automatic extension names 2022-10-06 17:19:30 -07:00
PrettyPrinter.lean refactor: add LCNF/Internalize.lean 2022-10-03 09:18:11 -07:00
PullFunDecls.lean feat: add occurences and phases to PassManager 2022-09-10 14:58:49 -07:00
PullLetDecls.lean feat: add occurences and phases to PassManager 2022-09-10 14:58:49 -07:00
ReduceJpArity.lean refactor: LCNF local context 2022-09-14 19:25:16 -07:00
Renaming.lean feat: preserve user provided names at LCNF Simp 2022-09-26 21:04:13 -07:00
Simp.lean refactor: add DiscrM.lean 2022-10-03 19:00:30 -07:00
Specialize.lean feat: reuse specialized functions between different compilation units 2022-10-07 16:07:17 -07:00
SpecInfo.lean feat: automatic extension names 2022-10-06 17:19:30 -07:00
Testing.lean chore: typo 2022-09-17 09:55:46 -07:00
ToDecl.lean feat: add flag at LCNF Decl indicating whether the original Lean declaration was declared using partial or unsafe 2022-09-30 19:28:05 -07:00
ToExpr.lean feat: dependency collector for the code specializer 2022-09-15 19:55:37 -07:00
ToLCNF.lean refactor: merge lcAny and lcErased 2022-10-05 04:46:52 -07:00
ToMono.lean fix: erase type (and type former) parameters occurrences at toMono 2022-10-06 06:23:08 -07:00
Types.lean feat: detect trivial structures and add extension for storing mono phase types 2022-10-05 08:55:44 -07:00
Util.lean fix: shouldGenerateCode fix for axiom 2022-09-23 14:25:48 -07:00