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

47 commits

Author SHA1 Message Date
Kim Morrison
5b1c6b558a
feat: align take/drop/extract across List/Array/Vector (#6860) 
This PR makes `take`/`drop`/`extract` available for each of
`List`/`Array`/`Vector`. The simp normal forms differ, however: in
`List`, we simplify `extract` to `take+drop`, while in `Array` and
`Vector` we simplify `take` and `drop` to `extract`. We also provide
`Array/Vector.shrink`, which simplifies to `take`, but is implemented by
repeatedly popping. Verification lemmas for `Array/Vector.extract` to
follow in a subsequent PR.
 2025-01-30 01:24:25 +00:00
Kim Morrison
71122696a1
feat: rename Array.shrink to take, and relate to List.take (#5796) 2024-10-21 23:35:32 +00:00
Joachim Breitner
b2d668c340
perf: Use flat ByteArrays in Trie (#2529) 2023-09-20 13:22:37 +02:00
Sebastian Ullrich
8a02dfec4f feat: subsume variables under variable 
/cc @leodemoura
 2021-01-22 14:36:05 +01:00
Leonardo de Moura
898a08a0c1 chore: avoid Has prefix in type classes 
closes #203
 2020-10-27 18:29:19 -07:00
Leonardo de Moura
10c32fcf94 chore: HasToString => ToString 2020-10-27 16:11:48 -07:00
Sebastian Ullrich
aef4a7159b chore(*): remove obsolete leanpkg.path files 2019-07-25 17:46:53 -07:00
Leonardo de Moura
e90a79f996 chore(tests/playground/parser/syntax): fix test 2019-06-05 14:19:24 -07:00
Leonardo de Moura
6da0fc7207 chore(tests/playground/parser/syntax): fix test 2019-05-18 11:39:44 -07:00
Leonardo de Moura
45d09d3044 fix(library/compiler/ir): bug at LLNF -> IR 2019-05-01 17:38:44 -07:00
Leonardo de Moura
ed5e461130 feat(library/init/lean/compiler/ir): add maxVar 2019-05-01 17:38:44 -07:00
Leonardo de Moura
fa0b4bff40 chore(tests/playground/parser/syntax): fix experiment 2019-04-30 18:06:03 -07:00
Leonardo de Moura
e1a84d2f2c fix(library/compiler/struct_cases_on): performance problem exposed by badupdate1.lean 2019-04-26 16:30:19 -07:00
Leonardo de Moura
c8a045d69f test(tests/playground/parser/parser): add HasAndthen and HasOrelse instances 2019-04-24 14:05:45 -07:00
Leonardo de Moura
014c7e3374 test(tests/playground/parser/parser): "liftable" longestMatch 
For lists of size 0, 1 and 2, it avoids the overhead of creating
temporary lists of closures. I measure the overhead with `test1.lean`
and there is no overhead in this case.
`test1.lean` has a test for length = 4, and the overhead is 7%.
We only use longestMatch to implement the Pratt Parser.
The lists should be small. So, the overhead is acceptable.
If it is not. We can add back the `longestMatch` specific for `TermParser`.

cc @kha
 2019-04-24 11:23:06 -07:00
Leonardo de Moura
5991337279 test(tests/playground/parser/test1): add test and timeit 2019-04-24 11:20:44 -07:00
Leonardo de Moura
5188adc685 test(tests/playground/parser): add longestMatch and other helper functions 2019-04-23 17:29:38 -07:00
Leonardo de Moura
3d8c3d5789 test(tests/playground/parser/parser): add unicodeSymbol parser 2019-04-23 09:34:41 -07:00
Leonardo de Moura
e844afb64a test(tests/playground/parser/syntax): propagate lazy macro scopes 2019-04-19 14:52:52 -07:00
Leonardo de Moura
2eed00039a chore(tests/playground/parser/parser): remove Thunk hack 
The artificial `Thunk` was being used just to make sure a `Parser`
object was small enough to be inlined. We don't need this hack anymore.
Commit 0ea944a adds a new transformation that makes sure the size of
field `info` does not impact the decision on whether field `fn` will be
inlined or not.
 2019-04-18 13:18:31 -07:00
Leonardo de Moura
0ea944ad9f feat(library/compiler/csimp): add transformation to complement eager lambda lifting 2019-04-18 13:12:11 -07:00
Leonardo de Moura
6b53700d60 test(tests/playground/parser/test1): improve 2019-04-13 08:15:56 -07:00
Leonardo de Moura
a716528067 fix(tests/playground/parser/parser): reset position 2019-04-13 08:07:29 -07:00
Leonardo de Moura
68e8faeef1 test(tests/playground/parser/parser): add sepBy and sepBy1 2019-04-13 07:56:35 -07:00
Leonardo de Moura
52fa06ad38 fix(tests/playground/parser/parser): fix tryFn 2019-04-13 07:36:48 -07:00
Leonardo de Moura
2377b10c2c test(tests/playground/parser): minor 2019-04-12 09:05:22 -07:00
Leonardo de Moura
d7de85e1e7 fix(tests/playground/parser/parser): small bugs 2019-04-12 08:58:02 -07:00
Leonardo de Moura
48ba69775a fix(tests/playground/parser/syntax): initialization 2019-04-12 08:25:47 -07:00
Leonardo de Moura
e53cb81255 test(tests/playground/parser): replace parser.lean with parser2.lean 2019-04-12 07:50:50 -07:00
Leonardo de Moura
87690217c6 test(tests/playground/parser/parser2): add missing definitions 2019-04-12 07:30:43 -07:00
Leonardo de Moura
376830bd0d chore(tests/playground/parser): missing files and small issues 2019-04-12 07:29:46 -07:00
Leonardo de Moura
be328bd8e9 test(tests/playground/parser/parser2): add symbol BasicParser 2019-04-10 08:58:41 -07:00
Leonardo de Moura
1c73a4d089 test(tests/playground/parser): add identFn 2019-04-09 09:16:12 -07:00
Leonardo de Moura
67ba4d25b1 test(tests/playground/parser/parser2): add number parser 2019-04-09 07:20:35 -07:00
Leonardo de Moura
ab5519c7fe test(tests/playground/parser/parser2): add recurse 2019-04-08 07:57:45 -07:00
Leonardo de Moura
b633b32f2c test(tests/playground/parser/parser2): add whitespace and strLit 2019-04-08 07:39:55 -07:00
Leonardo de Moura
363f4449e4 test(tests/playground/parser/parser2): add optional combinator 2019-04-08 06:37:41 -07:00
Leonardo de Moura
deba610203 test(tests/playground/parser/parser2): add many and many1 combinators 2019-04-07 13:41:22 -07:00
Leonardo de Moura
16f9d1a5b6 test(tests/playground/parser/parser2): add node combinator 2019-04-07 13:26:25 -07:00
Leonardo de Moura
d7035497f3 test(tests/playground/parser): continue experiment 2019-04-07 12:45:11 -07:00
Leonardo de Moura
97ebe4603b test(tests/playground/parser): add syntax.lean with flat nodes and arrays 2019-04-06 19:36:04 -07:00
Leonardo de Moura
0c9fe3c7d4 feat(library/compiler): add [inline2] attribute, and stage2 inlining 
This feature is useful since it allows us to perform inlining
after lambda lifting has been performed.
 2019-04-06 08:00:58 -07:00
Leonardo de Moura
23febc9977 test(tests/playground/parser/parser2): more experiments 2019-04-05 18:09:13 -07:00
Leonardo de Moura
69fb157ff7 chore(tests/playground/parser/parser2): update TODO list 2019-04-05 17:25:36 -07:00
Leonardo de Moura
c44f79f981 test(tests/playground/parser/parser2): yet another parsing combinators experiment 2019-04-05 08:18:28 -07:00
Leonardo de Moura
f25554baa7 test(tests/playground/parser): multiple targets 2019-04-04 10:50:34 -07:00
Leonardo de Moura
dd72df26bd test(tests/playground/parser): create directory and Makefile for experiment 2019-04-04 10:36:17 -07:00