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

644 commits

Author SHA1 Message Date
Daniel Selsam
8b461ccdaa fix(library/init/data/queue): need not be inhabited 2019-10-03 17:23:53 -07:00
Daniel Selsam
a82266c652 feat(library/init/lean/typeclass): #synth with tabled resolution 2019-10-03 17:23:53 -07:00
Leonardo de Moura
938c018e40 feat: helper functions 2019-10-03 16:50:38 -07:00
Leonardo de Moura
ce80a6d749 chore: naming convention 2019-10-03 16:50:30 -07:00
Leonardo de Moura
b316dc24c8 feat: more array goodies and naming convetion 2019-10-03 16:50:23 -07:00
Leonardo de Moura
c056894da3 feat: add Option.get!, Option.getOrElse ==> Option.getD 2019-10-03 16:50:07 -07:00
Leonardo de Moura
338c9359fa feat: add find! to maps 2019-10-03 16:49:57 -07:00
Leonardo de Moura
680ee21161 feat(library/init/lean/compiler/ir): add unreachbranches.lean 
New optimization pass for eliminating unreachable branches that occur
very often when using `ExceptT` and `EState`.

The current commit implements an abstract interpreter for computing
an approximation of the kinds of values returned by a function.
TODO:
- Implement `FnBody.jmp`.
- Implement `interpDecl`
- Remove unreachable branches in `FnBody.case`
 2019-10-02 19:57:43 -07:00
Leonardo de Moura
db75c8e5cf chore(library/init/data/list): renamed basic_aux ==> basicaux 
@kha we are currently avoiding `_` in file names.
I am not super happy with names such as `neverextractattr.lean`.
I am open to a new name convention for .lean files in the stdlib.
 2019-10-02 10:07:26 -07:00
Sebastian Ullrich
cae1009175 fix(library/init/data/list/aux): rename to basic_aux.lean 
`aux` is a reserved filename on Windows

/cc @leodemoura
 2019-10-02 12:30:29 +02:00
Leonardo de Moura
fdab3b90b9 refactor(library/init/data/array): new name convention for Array functions 2019-10-01 16:46:05 -07:00
Leonardo de Moura
411f397654 refactor(library/init/data/list): new name convention for List functions 
cc @dselsam @kha
 2019-10-01 15:15:02 -07:00
Leonardo de Moura
92b39e7161 chore(library/init): add findD variants 
@cc @dselsam
 2019-09-30 17:26:27 -07:00
Leonardo de Moura
18e6a106f4 feat(library/init/lean/smap): implement SMap using PHashMap instead of RBMap 2019-09-20 14:22:03 -07:00
Leonardo de Moura
a4b860b92a fix(runtime): missing Array.data primitive 2019-09-19 10:27:10 -07:00
Leonardo de Moura
a7d616605a fix(runtime/lean): missing primitive 2019-09-19 09:54:03 -07:00
Sebastian Ullrich
f22c17e94b chore(library/init/data/string/basic): remove broken lineColumn obsoleted by FileMap 2019-09-19 18:12:51 +02:00
Sebastian Ullrich
62d1cdcff9 chore(library/init/data/repr): fix String.Iterator.HasRepr 2019-09-19 17:50:24 +02:00
Leonardo de Moura
1d1ad8e2ed chore(library/init): auxiliary combinators 2019-09-17 17:17:46 -07:00
Leonardo de Moura
fdb1bf84b4 refactor(library/init/data/array/basic): cleanup names and types, add monadic versions 2019-09-17 17:17:46 -07:00
Leonardo de Moura
61a3ea61c4 perf(library/init/lean/compiler/ir/boxing): create auxiliary constants for caching the value of boxed/unboxed literals and constants 
For example, in the new test `qsort64.lean`, the new optimization
prevents the repeated execution of `box UInt64.inhabited`.
On my machine
```
./run.sh qsort64.lean 2000000
```
Goes from 1.22s to 0.355s
 2019-09-11 10:37:35 -07:00
Leonardo de Moura
128acd3b47 chore(library/init): remove @[extern cpp ...] 2019-08-24 07:40:38 -07:00
Leonardo de Moura
98e6e0c09a feat(library/init): add "extern c" attributes 2019-08-20 11:53:46 -07:00
Leonardo de Moura
52b86c3b4b chore(library/init/data/persistentarray/basic): missing "reset" 2019-08-14 16:22:35 -07:00
Leonardo de Moura
8e37fc512b fix(library/init/data/persistentarray/basic): bug at pop 
fixes #28
 2019-08-14 16:14:20 -07:00
Leonardo de Moura
7195244b04 feat(library/init/data/array/qsort): ensure qsort terminates even for bad lt relations 2019-08-10 22:10:14 -07:00
Leonardo de Moura
92da659ec7 feat(library/init/data/persistenthashmap/basic): add PersistentHashMap.contains 2019-08-09 11:25:01 -07:00
Leonardo de Moura
b8cd88a827 chore(library/init): delete dead files 2019-08-09 10:35:38 -07:00
Leonardo de Moura
d00019f57e chore(library/init): fix whitspaces before => 2019-08-09 09:13:49 -07:00
Leonardo de Moura
4d913370a7 chore(library/init): eliminate whitespaces using another patch script 2019-08-09 09:01:39 -07:00
Sebastian Ullrich
3ed67138d5 chore(*): update equation syntax in files and old parser 
for f in ../../**/*.lean; do echo $f; ./patch.lean.out $f > tmp && cat tmp > $f; done
 2019-08-09 11:11:34 +02:00
Leonardo de Moura
d5707bb256 fear(library/init/data/persistentarray/basic): add PersistentArray.mfor 2019-08-07 11:33:44 -07:00
Leonardo de Moura
1b5fc0e2c1 fix(library/init/data/array/basic): incorrect universe level 2019-08-07 11:33:23 -07:00
Leonardo de Moura
3ecf8ac8ec feat(library/init/data/persistentarray/basic): add mfoldlFrom and foldlFrom 2019-08-05 07:41:41 -07:00
Leonardo de Moura
af46e36266 fix(library/init/data/persistentarray/basic): universes 2019-08-04 13:00:32 -07:00
Leonardo de Moura
2a58e58480 feat(library/init/data/persistentarray/basic): add mfind and mfindRev 2019-08-04 12:30:12 -07:00
Leonardo de Moura
4bd347de3a feat(library/init/data/persistentarray/basic): PersistentArray.pop 2019-08-04 11:50:05 -07:00
Leonardo de Moura
f55a00a022 feat(library/init/lean): add LocalContext 2019-08-04 09:29:05 -07:00
Leonardo de Moura
84c4637722 fix(library/init/data/array/basic): fix and rename eraseIdxSz ==> eraseIdx' 2019-08-02 14:06:35 -07:00
Leonardo de Moura
0a86911bd0 fix(library/init/data/persistenthashmap/basic): isUnaryNode 2019-08-02 13:59:31 -07:00
Leonardo de Moura
3c5a30649d feat(library/init/data/persistenthashmap/basic): add PersistentHashMap.erase 2019-08-02 13:31:29 -07:00
Leonardo de Moura
69bca3ad42 feat(library/init/data/array/basic): add version of Array.indexOf with property about resulting size 2019-08-02 13:31:29 -07:00
Leonardo de Moura
19e341cfcc feat(library/init/data/array/basic): add Array.indexOf and Array.eraseIdx 2019-08-02 13:31:29 -07:00
Leonardo de Moura
c371b43970 feat(library/init/data): add PersistentHashMap 2019-08-02 13:31:29 -07:00
Leonardo de Moura
8a4bc188c2 feat(library/init/data): add BinomialHeap 2019-07-31 15:13:00 -07:00
Leonardo de Moura
906272d7e9 feat(library/init/data/list/basic): add eraseIdx 2019-07-31 15:04:43 -07:00
Leonardo de Moura
2ddc797f65 feat(library/init/system/filepath): add dirName 2019-07-26 14:53:54 -07:00
Leonardo de Moura
ff88c35fc1 refactor(library/init): move io and platform to system subdir 2019-07-25 17:29:33 -07:00
Leonardo de Moura
f6d3fc881d feat(library/init): add platform.cpp 2019-07-25 17:19:50 -07:00
Leonardo de Moura
8b0730ef7d feat(library/init/data/list/basic): eraseDups 2019-07-22 18:12:03 -07:00