Mario Carneiro
|
37252e5fa7
|
chore: remove Bootstrap package
|
2022-09-02 16:39:03 -07:00 |
|
Mario Carneiro
|
158e182b8b
|
chore: move Bootstrap.Dynamic -> Init.Dynamic
|
2022-09-02 04:36:54 -07:00 |
|
Leonardo de Moura
|
d96bf8a633
|
chore: restore accidentally deleted test
25447af13c
|
2022-09-01 06:06:03 -07:00 |
|
Leonardo de Moura
|
d00627364c
|
feat: add simp compiler pass
|
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 |
|
Mario Carneiro
|
ebb5b97d73
|
chore: move Bootstrap.Data -> Lean.Data
|
2022-08-31 11:48:57 -07:00 |
|
Leonardo de Moura
|
a0b47195ba
|
fix: fixes #1547
|
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 |
|
Mario Carneiro
|
6a7ccb5797
|
refactor: generalize ShareCommon to a typeclass (#1537)
|
2022-08-29 09:34:38 -07:00 |
|
Mario Carneiro
|
850ee17346
|
chore: move Bootstrap.System.Uri to Init
|
2022-08-29 08:06:30 -07:00 |
|
Mario Carneiro
|
0efbc0bc03
|
chore: remove BinomialHeap, DList, Stack, Queue
These are moving to std4.
|
2022-08-29 07:07:53 -07:00 |
|
Mario Carneiro
|
bf89c5a0f5
|
chore: move Std -> Bootstrap
|
2022-08-29 01:26:12 -07:00 |
|
Mario Carneiro
|
31784c9a24
|
doc: documentation for Init.Core
|
2022-08-29 00:41:24 -07:00 |
|
Leonardo de Moura
|
ee8e771445
|
fix: dotted name bug
|
2022-08-27 10:41:55 -07: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 |
|
Mario Carneiro
|
ee22e637cd
|
fix: use withContext at ac_rfl
|
2022-08-26 15:23:24 -07:00 |
|
Sebastian Ullrich
|
e81ba951c6
|
fix: Core.transform API and uses
|
2022-08-25 19:07:42 -07:00 |
|
Fynn Schmitt-Ulms
|
064ab16791
|
feat: Float.abs function (#1514)
|
2022-08-25 18:45:46 -07:00 |
|
Gabriel Ebner
|
8fc3bae47c
|
chore: remove unexpanded coercion support from pp.analyze
|
2022-08-24 21:58:13 -07:00 |
|
Leonardo de Moura
|
85866fc238
|
chore: fix and disable some LCNF tests
We still need to port code to the new architecture
|
2022-08-24 14:12:27 -07:00 |
|
Leonardo de Moura
|
eaa384bd81
|
perf: remove unnecessary calls to ensureUniqueLetVarNames
`instantiateRevInternalize` is already ensuring we have unique names.
|
2022-08-21 14:15:42 -07:00 |
|
Leonardo de Moura
|
84204432db
|
chore: fix test output
|
2022-08-21 14:01:18 -07:00 |
|
Leonardo de Moura
|
776a9b0dcb
|
feat: don't eagerly simplify local functions that will be inlined
|
2022-08-20 20:03:05 -07:00 |
|
Leonardo de Moura
|
d2d0a745d5
|
feat: use eta-reduction when reducing projection instances
|
2022-08-20 20:03:05 -07:00 |
|
Sebastian Ullrich
|
5ce5576b5d
|
fix: hygienic resolution of namespaces
|
2022-08-20 22:29:46 +02:00 |
|
Leonardo de Moura
|
879a466875
|
perf: improve isTypeFormerType
|
2022-08-19 18:23:28 -07:00 |
|
Leonardo de Moura
|
8aa9d2cdbf
|
feat: add "cases on cases" simplification
|
2022-08-19 17:39:10 -07:00 |
|
Leonardo de Moura
|
49823c28c4
|
fix: inlining heuristic
|
2022-08-19 16:23:37 -07:00 |
|
Leonardo de Moura
|
a29a61b728
|
chore: remove dead code
|
2022-08-19 11:56:22 -07:00 |
|
Leonardo de Moura
|
9ae2b83ac0
|
feat: add Compiler.Decl.pullInstances
|
2022-08-18 15:09:22 -07:00 |
|
Leonardo de Moura
|
18c95e8322
|
fix: bug at toLCNF cache
|
2022-08-17 17:16:13 -07:00 |
|
Leonardo de Moura
|
f0791559b8
|
chore: fix test
Ensure `targetUri`s in the test output do not contain full paths on my machine.
|
2022-08-17 15:24:00 -07:00 |
|
Mario Carneiro
|
8182f83929
|
doc: documentation for Init.Tactics
|
2022-08-17 14:44:40 -07:00 |
|
Leonardo de Moura
|
0d52a3f92b
|
fix: add attachJp
Auxiliary function for attaching jump to a join point to an existing
let-code block.
|
2022-08-17 07:32:11 -07:00 |
|
Leonardo de Moura
|
763cf31c3b
|
test: go to definition
|
2022-08-17 06:05:00 -07:00 |
|
E.W.Ayers
|
81ad807bb3
|
test: more unit tests
Some taken from https://stackoverflow.com/questions/37172819/test-if-c98-string-is-a-number-in-scientific-notation
|
2022-08-17 05:57:22 -07:00 |
|
E.W.Ayers
|
4e7c1e1ec8
|
fix: missing digits in scientific literal should be an error
|
2022-08-17 05:57:22 -07:00 |
|
Mario Carneiro
|
37a12b635b
|
feat: add declId hover for syntax/notation/mixfix
|
2022-08-17 05:55:06 -07:00 |
|
Mario Carneiro
|
e0221db2e2
|
feat: add @[inheritDoc] attribute
|
2022-08-16 18:31:55 -07:00 |
|
Leonardo de Moura
|
0e3e1353e2
|
feat: new Compiler trace classes
|
2022-08-16 18:23:49 -07:00 |
|
E.W.Ayers
|
2e99e8c22d
|
feat: Float ↔ Json
|
2022-08-16 08:01:23 -07:00 |
|
E.W.Ayers
|
9e194e3c3d
|
fix: add + parser to decimalNumberFn
|
2022-08-16 07:29:39 -07:00 |
|
E.W.Ayers
|
a763d9d81e
|
fix: decodeScientificLitVal? parses 1.0e+1 correctly
fixes #1484
|
2022-08-16 07:29:39 -07:00 |
|
Leonardo de Moura
|
37ba0df584
|
feat: do not generate code for matcher auxiliary declarations
We are macro inlining them.
|
2022-08-15 20:10:33 -07:00 |
|
Leonardo de Moura
|
e931c6b5b5
|
fix: bug at toLCNF
|
2022-08-15 12:59:36 -07:00 |
|
Leonardo de Moura
|
4f79d2caa0
|
feat: improve toLCNF
Preserve type formers only if they are application arguments
|
2022-08-15 09:53:48 -07:00 |
|