Leonardo de Moura
d00627364c
feat: add simp compiler pass
2022-08-31 18:10:32 -07:00
Leonardo de Moura
ba0835e387
feat: refresh binder names during internalization
2022-08-31 18:10:32 -07:00
Leonardo de Moura
25447af13c
feat: new code inliner
2022-08-31 18:10:32 -07:00
Sebastian Ullrich
2e98726973
fix: levelMVarToParam must update levelNames
2022-08-31 17:57:07 -07:00
Sebastian Ullrich
e075b54f22
fix: collision between implicit and auto-bound level names
2022-08-31 17:57:07 -07:00
Sebastian Ullrich
a657a638f0
feat: sub-info tree level hover
2022-08-31 17:49:43 -07:00
Sebastian Ullrich
4050227e5d
chore: revert marking internal notes as parser/elab docstrings
2022-08-31 17:49:43 -07:00
Sebastian Ullrich
b9152a5296
refactor: move, generalize findSyntaxStack?
2022-08-31 17:49:43 -07:00
Henrik Böving
c1949e05e0
feat: migrate to new pass manager
2022-08-31 16:28:07 -07:00
Henrik Böving
fe63bd2e8e
feat: basic pass manager
2022-08-31 16:28:07 -07:00
Sebastian Ullrich
98145ad8ba
chore: not a docstring
2022-08-31 22:19:27 +02:00
Mario Carneiro
ebb5b97d73
chore: move Bootstrap.Data -> Lean.Data
2022-08-31 11:48:57 -07:00
Leonardo de Moura
2fc38fb118
feat: instantiateTypeLevelParams and instantiateValueLevelParams for LCNF.Decl
2022-08-30 20:20:39 -07:00
Leonardo de Moura
a0b47195ba
fix: fixes #1547
2022-08-30 11:45:05 -07:00
Leonardo de Moura
c451bf0c91
feat: add simpFunDecl
2022-08-30 11:45:05 -07:00
Mario Carneiro
b2b02295b0
chore: move ShareCommon to Init / Lean
2022-08-30 07:51:43 -07:00
Leonardo de Moura
ca80bc52dc
feat: LCNF.simp .let case
2022-08-29 09:52:16 -07:00
Leonardo de Moura
7b161d33d1
refactor: add MonadFVarSubst class
2022-08-29 09:52:16 -07:00
Mario Carneiro
850ee17346
chore: move Bootstrap.System.Uri to Init
2022-08-29 08:06:30 -07:00
Siddharth Bhat
a7b128fee1
doc: explanations for LCNF.
2022-08-29 07:17:25 -07:00
Mario Carneiro
bf89c5a0f5
chore: move Std -> Bootstrap
2022-08-29 01:26:12 -07:00
Leonardo de Moura
062d4728a1
feat: more LCNF update functions
...
and bug fixes at CSE
2022-08-28 19:00:49 -07:00
Leonardo de Moura
5552d610e8
chore: missing updateCases!
2022-08-28 16:30:54 -07:00
Leonardo de Moura
e80028b7d1
feat: add pure field to LetDecl, add helper functions for updating LCNF code
...
The update functions try to minimize the amount of memory allocation
2022-08-28 08:55:35 -07:00
Leonardo de Moura
d5fa178fc3
feat: modify FVarSubst used in the new code generator
2022-08-28 08:55:35 -07:00
Leonardo de Moura
6a9f8ad919
fix: Compiler/LCNF/ElimDead.lean
2022-08-28 08:55:35 -07:00
Leonardo de Moura
cd0dd4cc2f
feat: start simp for new LCNF format
2022-08-27 19:59:31 -07:00
Leonardo de Moura
9446ae3056
feat: add cleanup function for CompilerM
2022-08-27 18:35:30 -07:00
Leonardo de Moura
30d8ae70f7
chore: remove workarounds
2022-08-27 10:56:15 -07:00
Leonardo de Moura
ee8e771445
fix: dotted name bug
2022-08-27 10:41:55 -07:00
Leonardo de Moura
0f40dfc063
feat: add FunDecl.etaExpand
2022-08-27 10:41:54 -07:00
Leonardo de Moura
11c8253f6c
feat: more update functions for LCNF
2022-08-27 10:41:54 -07:00
Leonardo de Moura
bdf89b4d85
chore: add {crossEmoji} at failure
2022-08-27 10:41:54 -07:00
Sebastian Ullrich
fb408c024b
fix: deleting built-in docstrings
2022-08-27 17:19:25 +02:00
Mario Carneiro
9bd886f37d
fix: @[inheritDoc] on notation
2022-08-27 07:11:39 -07:00
Sebastian Ullrich
a69d7fb018
fix: remove broken Handle.isEof
2022-08-26 20:55:09 -07:00
E.W.Ayers
f52a1bd37c
doc: JSON-RPC
2022-08-26 20:49:57 -07:00
Leonardo de Moura
969dce70db
perf: improve FVarSubst apply functions in the new compiler stack
2022-08-26 20:10:36 -07:00
Mario Carneiro
ee22e637cd
fix: use withContext at ac_rfl
2022-08-26 15:23:24 -07:00
E.W.Ayers
ff792c3a3a
feat: abstract visitLet, visitLambda, visitForall
2022-08-25 19:09:16 -07:00
E.W.Ayers
d18667c484
feat: generalise forEachExpr
...
Lean.Meta.forEachExpr should be general over monads rather than restricted to the MetaM monad.
This is similar to the generalisation of Lean.Meta.transform
2022-08-25 19:09:16 -07:00
Sebastian Ullrich
e81ba951c6
fix: Core.transform API and uses
2022-08-25 19:07:42 -07:00
Leonardo de Moura
65f9344f01
feat: check whether join points are fully applied at Check.lean
2022-08-25 18:17:54 -07:00
Leonardo de Moura
14944aeb3c
chore: print decl size at trace message
2022-08-25 18:11:49 -07:00
Leonardo de Moura
4c9c2d2bf7
feat: new CSE.lean
2022-08-25 18:08:22 -07:00
Leonardo de Moura
98575b4250
feat: new PullLetDecls.lean
2022-08-25 13:39:15 -07:00
Gabriel Ebner
90f92c3a9e
fix: use delabAppExplicit for tooltips
2022-08-25 18:38:21 +02:00
Gabriel Ebner
a6a913495d
feat: make (_ : a = b) hoverable in infoview
2022-08-25 18:38:21 +02:00
Gabriel Ebner
82e9f09bca
fix: remove incorrect syntax coercion
2022-08-25 17:54:26 +02:00
Gabriel Ebner
8fc3bae47c
chore: remove unexpanded coercion support from pp.analyze
2022-08-24 21:58:13 -07:00
