max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
29793 commits 1 branch 0 tags 5.3 GiB
Commit graph

20450 commits

Author SHA1 Message Date
Leonardo de Moura
5c925f9345 feat: add functions to create small arrays and use them in the constant folder 
It reduces the code generated for functions using a bunch
of quotations. For example, the size of
`Lean.Elab.Term.Do.ToTerm.matchNestedTermResult` went from 2348 to 1507
 2022-09-28 22:00:50 -07:00
Leonardo de Moura
6bc6522d86 feat: constructor => discriminant optimization 2022-09-28 21:14:19 -07:00
Leonardo de Moura
73ebaf8499 feat: improve visitLambda at toLCNF 2022-09-28 19:17:28 -07:00
Sebastian Ullrich
71e647049f refactor: lexOrd should not be an instance 2022-09-28 15:57:01 -07:00
Sebastian Ullrich
d0a002ffff fix: prefer longer parse even if unsuccessful 2022-09-28 15:57:01 -07:00
Leonardo de Moura
94c2ec38d5 feat: implement cast TODO 
fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/301269857
 2022-09-28 15:40:53 -07:00
Leonardo de Moura
970331de05 chore: avoid a.getAppFn.isAnyType idiom 2022-09-28 15:34:09 -07:00
Mario Carneiro
db110f5dfe fix: preserve tags in simp conv 2022-09-28 14:24:44 -07:00
Mario Carneiro
2a748d3035 fix: conv case => should close the goal conv-style 2022-09-28 14:24:44 -07:00
Mario Carneiro
6f8e861158 fix: case names in congr conv 2022-09-28 14:24:44 -07:00
Mario Carneiro
b6a58d13e1 fix: LHS goals should be pre-whnf'd 2022-09-28 14:24:44 -07:00
Mario Carneiro
b8ed329a5d feat: add dsimp conv <- mathlib4 
Co-authored-by: Moritz Doll <doll@uni-bremen.de>
 2022-09-28 14:24:44 -07:00
Mario Carneiro
a09934c693 feat: more conv goal structuring tactics 2022-09-28 14:24:44 -07:00
Ed Ayers
10971a413a
feat: fromJson? derivations now say where a parsing error occurred (#1656) 2022-09-28 09:15:26 +00:00
Ed Ayers
22bb798995
feat: datatypes for LSP code actions (#1654) 2022-09-28 09:07:39 +00:00
Leonardo de Moura
fd5f3a5bad feat: track recursively inlining 
closes #1657
see #1646

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/inline.20codegen.20crash/near/301099703
 2022-09-27 16:26:49 -07:00
Leonardo de Moura
002c7d2f22 feat: configuration options for the code generator 2022-09-27 16:26:49 -07:00
Leonardo de Moura
135790f41a fix: missing eraseCode at inlineProjInst? 
Fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/LCNF.20local.20context.20contains.20unused.20local.20variable.20declaratio/near/301102923
 2022-09-27 16:26:49 -07:00
Leonardo de Moura
65c307a7b7 feat: add environment extension for constant folder 
TODO: add command/attribute for conveniently installing folders
 2022-09-27 16:26:49 -07:00
Sebastian Ullrich
a03749cbe4 fix: findReferences should find only original syntax 2022-09-27 22:09:54 +02:00
Mario Carneiro
d843e2a418 chore: add docs and test 2022-09-27 22:09:54 +02:00
Mario Carneiro
2270e8cd53 fix: ignore unused anonymous have variables 2022-09-27 22:09:54 +02:00
Mario Carneiro
6bf01ebd30 feat: use have token span for implicit this 2022-09-27 22:09:54 +02:00
Mario Carneiro
969eefe79b fix: let _ := should not introduce a variable called "_" 2022-09-27 22:09:54 +02:00
Mario Carneiro
280d8c9c9b feat: add (canonical := true) option in Syntax 2022-09-27 22:09:54 +02:00
Ed Ayers
64e7f25ffe doc: apply suggestions from code review 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2022-09-27 11:37:49 -07:00
E.W.Ayers
8e085fb637 doc: some documentation for Message.lean 2022-09-27 11:37:49 -07:00
Patrick Massot
f0c8e6fa2d doc: add docstrings in PersistentExtension 
Add docstring to functions with non-obvious persistence properties. See the discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/HashMap.20extension/near/300784691
 2022-09-27 10:34:09 -07:00
Leonardo de Moura
f067382f52 chore: remove old exports 2022-09-27 07:44:38 -07:00
Leonardo de Moura
8596e4af88 fix: mark code as simplified 2022-09-26 21:27:45 -07:00
Leonardo de Moura
193e3fd184 feat: add basic String folding 2022-09-26 21:23:08 -07:00
Leonardo de Moura
e6f5b3758c feat: precompute folders 2022-09-26 21:10:38 -07:00
Leonardo de Moura
1e75001405 feat: preserve user provided names at LCNF Simp 
It helps preserving let-declaration names in pure code, but it is not
very useful for monadic let-decls (e.g., `let x <- act`). The binder
names are often lost we eliminating the abstraction layers.
 2022-09-26 21:04:13 -07:00
Leonardo de Moura
24e584cf00 feat: add Renaming.lean 2022-09-26 21:04:13 -07:00
Henrik Böving
2958b8a7f5 feat: basic constant folder 
supports:
- arithmetic operations:
  - folding full constants
  - folding neutral elements
  - folding annihilators
- List.toArray
 2022-09-26 21:03:47 -07:00
Leonardo de Moura
73d5e12ac5 fix: baseExt must not use SimplePersistentEnvExtension 
We invoke `Decl.saveBase` more than once when we update a declaration.
 2022-09-26 08:15:47 -07:00
Leonardo de Moura
ba619be393 fix: apply macroInline again after inlineMatchers 2022-09-26 07:31:27 -07:00
Leonardo de Moura
837ce4374c feat: use reduceJpArity after successful simpJpCases? 2022-09-26 07:25:29 -07:00
Leonardo de Moura
35ca2b203c refactor: split Simp.lean 2022-09-26 07:04:20 -07:00
Mario Carneiro
85119ba9d1 chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
Leonardo de Moura
fd1ae3118c feat: replace isCasesOnCases? with simpJpCases? 
It addresses the code explosion issue with the old optimization.
For example, the resulting size for `Lean.Json.Parser.escapedChar`
went from 31593 to 361.
 2022-09-25 20:57:24 -07:00
Leonardo de Moura
bbac49e925 feat: add collectJpCasesInfo 
Collect statistics for implementing new optimization that will replace `isCasesOnCases?`
 2022-09-25 20:57:24 -07:00
Mario Carneiro
9b9998f5c8 feat: pattern (occs := ...) conv 2022-09-25 19:52:56 -07:00
Leonardo de Moura
dadfe84c15 doc: update const2ModIdx docstring 2022-09-25 14:06:07 -07:00
Leonardo de Moura
236885e72e chore: remove Stage1 2022-09-25 13:17:50 -07:00
Mario Carneiro
5644bd7a3f feat: show decl module in hover 2022-09-25 06:43:48 -07:00
Mario Carneiro
fa13d7321f feat: generalize e = x at h 2022-09-25 06:42:20 -07:00
Mario Carneiro
84497c1d09 feat: sort simp lemmas by application order 2022-09-25 06:40:56 -07:00
Mario Carneiro
afca560bda chore: revert builtin flag on Origin 2022-09-25 06:40:56 -07:00
Mario Carneiro
b739186e98 feat: use a structured type for simp theorem Origin 2022-09-25 06:40:56 -07:00