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

1204 commits

Author SHA1 Message Date
Daniel Selsam
e071501342 chore(lean/typeclass): 'synth_command' -> 'synthCommand' 2019-10-03 17:23:53 -07:00
Daniel Selsam
710b115885 chore(library/init): macro version of panic 2019-10-03 17:23:53 -07:00
Daniel Selsam
1d0e0378c0 chore(library/init/lean): Mvar -> MVar 2019-10-03 17:23:53 -07:00
Daniel Selsam
9c4f33593b chore(typeclass): use Option.toBool 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
b4a002f0f2 feat: abstract interpreter entry point, and missing stuff 
TODO: widening to ensure termination
 2019-10-03 16:50:47 -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
45d664ff25 fix(library/init/lean/compiler/ir/livevars): bug at updateLiveVars 2019-10-02 16:50:37 -07:00
Leonardo de Moura
874dd1d55c chore(library/init/lean/compiler/ir/basic): remove unnecessary function 2019-10-02 16:50:37 -07:00
Leonardo de Moura
e9bcbd5b0d fix(library/init/lean/compiler/ir/unboxresult): reject recursive types 2019-10-02 16:50:37 -07:00
Leonardo de Moura
4a219b6bd2 feat(library/init/lean/compiler/ir): add [unbox] attribute 2019-10-02 16:50:37 -07:00
Leonardo de Moura
cc18c0ef91 feat(library/init/lean/expr): add Expr.hasFVar and Expr.hasMVar 
cc @dselsam
 2019-10-02 10:07:26 -07: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
6ad9d58b0f fix(library/init/lean/compiler/neverextractattr): auxiliary declarations should inherit @[neverExtract] attribute 2019-10-01 14:57:16 -07:00
Leonardo de Moura
70a90ca73e feat(library/init/lean/parser/identifier): allow ! and ? in the identifiers 2019-10-01 14:45:07 -07:00
Leonardo de Moura
9d2eadc754 chore(library/init/lean/compiler): delete @[effectful] 2019-10-01 14:08:31 -07:00
Leonardo de Moura
80d3ca9d77 feat(library/init/lean/compiler): add @[neverExtract] attribute 
It will replace `@[effectful]`

cc @kha
 2019-10-01 14:00:02 -07:00
Leonardo de Moura
a507145eb1 feat(library/init/lean/level): add instance : HasBeq Level 2019-10-01 09:47:44 -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
e451c4dc78 feat(library/init/lean/compiler): add @[effectful] 
This attribute is used for low-level primitives like unsafeIO
 2019-09-30 16:12:41 -07:00
Leonardo de Moura
2b252a441e feat(library/init/lean/declaration): add ConstantInfo.instantiateTypeUnivParams and ConstantInfo.instantiateValueUnivParams 
cc @dselsam

See new test for an example.
 2019-09-30 15:46:19 -07:00
Leonardo de Moura
864b9c730c feat(library/init/lean/expr): helper functions 
cc @dselsam

Notes:
- x.isAppOrConst => x.isApp || x.isConst
- x.isPi => x.isForall
 2019-09-30 15:16:40 -07:00
Leonardo de Moura
faebe15a7f feat(library/init/lean/expr): add efficient instantiate1 
cc: @dselsam
 2019-09-30 14:33:32 -07:00
Leonardo de Moura
d6ea1d1a3f feat(frontends/lean/builtin_cmds): add #synth command 2019-09-24 11:32:43 +08:00
Leonardo de Moura
28c905f684 chore(library/init/lean): add typeclass skelethon 2019-09-24 11:19:02 +08: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
02e4abb24a feat(library/init/lean/elaborator): convertForall skeleton 2019-09-17 17:17:46 -07:00
Leonardo de Moura
06bb3a82d3 feat(library/init/lean/localcontext): add LocalContext.mkLambda and LocalContext.mkForall 2019-09-17 17:17:46 -07:00
Leonardo de Moura
eebc722f57 feat(library/init/lean/expr): add abstractRange 2019-09-17 17:17:46 -07:00
Leonardo de Moura
75e5f5bfd8 feat(library/init/lean/expr): expose abstract 2019-09-16 18:34:45 -07:00
Leonardo de Moura
704f90d728 feat(library/init/lean/expr): expose instantiate and instantiateRev 2019-09-16 18:29:43 -07:00
Leonardo de Moura
2996d306c9 feat(library/init): add more general modify: modifyGet 
This commit also adds a few helper elaboration functions.
 2019-09-16 15:14:02 -07:00
Leonardo de Moura
bd7ee8b01b feat(library/init/lean/elaborator/term): add elabList, and fix elabTermAux 2019-09-14 08:41:49 -07:00
Sebastian Ullrich
560e7af128 fix(library/init/lean/compiler/ir/compilerm): borrow annotations on extern decls do not do anything right now 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
9015fc1e34 chore(library/compiler/ir_interpreter): add step-level trace 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
1a99fc5c5d feat(init/lean/compiler): export some internals 2019-09-12 18:22:02 +02:00
Leonardo de Moura
8e47b6396f chore(library/init/lean/compiler/ir): simplify mkCase, the xType field is set by explicitBoxing 2019-09-12 08:55:09 -07:00
Leonardo de Moura
ca54240843 fix(library/init/lean/compiler/ir): the xType field at FnBody.case must be set by explicitBoxing 2019-09-12 08:47:58 -07:00
Leonardo de Moura
0284d4a7a2 chore(library/compiler/ir): use new mkCase 2019-09-12 08:23:29 -07:00
Leonardo de Moura
a16d3f09cf feat(library/init/lean/compiler/ir): store scrutinee type at FnBody.case 2019-09-12 08:07:47 -07:00
Leonardo de Moura
56e0c0efae chore(library/init/lean/compiler/ir/boxing): apply elimDead 2019-09-11 11:55:38 -07:00
Leonardo de Moura
3aeeadd255 chore(library/init/lean/compiler/ir/boxing): cleanup 2019-09-11 11:11:33 -07:00
Leonardo de Moura
f39220ac01 feat(library/init/lean/compiler/ir/boxing): ignore "cheap" cases when caching boxing operations 2019-09-11 10:56:37 -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
e8cdd2b29f fix(library/init/lean/compiler/ir/default): missing explicitRC 2019-09-09 10:53:34 -07:00