Leonardo de Moura
a55841aa68
chore: simplify synthInstance cache
...
Make sure it handle the common cases efficiently.
2019-12-01 18:32:48 -08:00
Leonardo de Moura
99840f6212
chore: move abbreviation
2019-12-01 18:32:48 -08:00
Leonardo de Moura
2867cd627b
feat: add tryOpt
2019-12-01 18:32:48 -08:00
Leonardo de Moura
00b991baf6
feat: add openAbstractMVarsResult
2019-12-01 18:32:48 -08:00
Leonardo de Moura
7dafba2c6c
feat: add instantiateLevelParamsArray
2019-12-01 18:32:48 -08:00
Leonardo de Moura
427df087e8
feat: instantiateLevelParams in Lean
2019-12-01 18:32:48 -08:00
Leonardo de Moura
9ec9091f93
refactor: Level.instantiate ==> Level.instantiateParams
2019-12-01 18:32:48 -08:00
Leonardo de Moura
24a31ab50e
feat: improve Level.instantiate
2019-12-01 18:32:48 -08:00
Leonardo de Moura
27bf6c8229
chore: refine synthInstance cache
2019-12-01 18:32:48 -08:00
Leonardo de Moura
11d829eccd
feat: add lambdaMetaTelescope
...
We need it because `abstractMVars` use lambdas
2019-12-01 18:32:48 -08:00
Leonardo de Moura
e73b5e3c88
chore: SynthInstanceAnswer ==> SynthInstance.Answer
2019-12-01 18:32:48 -08:00
Leonardo de Moura
ef43a08b91
feat: add checkOutParam validation
...
It implements the approach we have discussed at
`src/library/type_context.cpp`.
2019-12-01 18:32:48 -08:00
Leonardo de Moura
ad02d21852
feat: add hasAnyFVar
2019-12-01 18:32:48 -08:00
Leonardo de Moura
3bc5e144a2
feat: add synthInstance cache
2019-12-01 18:32:48 -08:00
Leonardo de Moura
e82ca1456e
chore: user lambda instead of forall to store result
...
Reason: ensure the resulting expression is type correct.
2019-12-01 18:32:48 -08:00
Sebastian Ullrich
21ac37378e
doc: update build docs
2019-11-29 11:23:42 +01:00
Sebastian Ullrich
27aa0938c8
chore: update .gitignores
2019-11-29 11:18:26 +01:00
Leonardo de Moura
f701683388
chore: add abbreviations MVarId and FVarId
2019-11-28 08:18:06 -08:00
Leonardo de Moura
f8fb195719
feat: cache local instances at metavariable declarations
2019-11-28 05:57:46 -08:00
Leonardo de Moura
2733a5bebd
chore: remove unnecessary method
2019-11-28 05:40:03 -08:00
Leonardo de Moura
deacb03802
feat: add isReadOnlyExprMVar
2019-11-28 05:34:12 -08:00
Leonardo de Moura
be9dab41ad
fix: abstractMVars
2019-11-27 10:53:25 -08:00
Leonardo de Moura
b1f9b7cd4d
feat: add AbstractMVars
2019-11-27 09:45:40 -08:00
Leonardo de Moura
005d03fc3d
feat: remove ignoreImplict workaround
2019-11-27 06:54:55 -08:00
Leonardo de Moura
32c066946b
chore: udpate stage0
2019-11-27 05:54:40 -08:00
Sebastian Ullrich
d5f30ddb83
fix: update-stage0
2019-11-27 05:53:22 -08:00
Sebastian Ullrich
98b83e96cb
chore: do not build bin_lean_stage2 by default
2019-11-27 05:53:22 -08:00
Sebastian Ullrich
682ad9f605
feat: stage 2 and 3 builds
...
While stage 1 is still the main build and the source of `bin/lean`, we now have optional targets
* lean_stage2, lean_stage3: build respective executable in `<build>/shell` from previous stage, compiling the stdlib
from scratch
* bin_lean_stage2: copy `lean_stage2` to `bin/` (stage 3 should always be identical to stage 2)
2019-11-27 05:53:22 -08:00
Sebastian Ullrich
2ad21d0f4c
feat: have --make take an optional .olean filename argument
...
Not documented since it is mostly useful for internal builds of further bootstrap stages
2019-11-27 05:53:22 -08:00
Leonardo de Moura
e99f8a9d22
chore: naming convention
...
suffix `?` should only be used for functions/methods returning `Bool`.
2019-11-27 05:50:31 -08:00
Leonardo de Moura
dfbc9cb8b5
chore: update stage0
2019-11-27 05:45:35 -08:00
Leonardo de Moura
e8bd90a753
fix: performance issue introduced by 2809cea147
2019-11-27 05:43:28 -08:00
Leonardo de Moura
a5cf1ac5ae
chore: fix tests
2019-11-26 18:07:13 -08:00
Leonardo de Moura
e45211f31c
test: display discrimination tree containing type class instances
2019-11-26 18:00:31 -08:00
Leonardo de Moura
e08c6def07
chore: update stage0
2019-11-26 17:57:21 -08:00
Leonardo de Moura
42fcf6e6e8
feat: add parameter ignoreImplicit
2019-11-26 17:56:07 -08:00
Leonardo de Moura
734a3001da
chore: update stage0
2019-11-26 17:32:05 -08:00
Leonardo de Moura
2809cea147
chore: remove DecidableEq workaround
...
We have better indexing now.
2019-11-26 17:30:18 -08:00
Leonardo de Moura
9a160a197a
fix: addGlobalInstance
2019-11-26 17:19:03 -08:00
Leonardo de Moura
6abf0ddf1a
chore: update stage0
2019-11-26 17:02:51 -08:00
Leonardo de Moura
81278c1509
feat: add instanceExtension
...
Use discrimination trees indexing type class instances.
2019-11-26 17:01:36 -08:00
Leonardo de Moura
55ab0f29e9
feat: break insert into two steps
...
Only the first step `Expr -> Array Key` requires the `MetaM` monad.
Motivation: we can save `(Array Key, Expr)` into .olean files, and
import modules without using `MetaM`.
2019-11-26 17:01:36 -08:00
Leonardo de Moura
f9376fe04b
feat: add withNewMCtxDepth
2019-11-26 17:01:36 -08:00
Leonardo de Moura
04417fafe8
chore: add missing instance
2019-11-26 17:01:36 -08:00
Leonardo de Moura
1f815ac521
feat: add forallMetaTelescope
2019-11-26 17:01:36 -08:00
Leonardo de Moura
4162eb1e08
fix: typo
2019-11-25 15:53:08 -08:00
Leonardo de Moura
856fb0c000
feat: use isProofQuick to implement isDefEqProofIrrel
2019-11-25 08:42:23 -08:00
Leonardo de Moura
292603f8bb
chore: remove ParamInfo.proof field
...
It is an approximation because of dependent types.
Moreover, the new `isProofQuick` should make `isProof` much cheaper.
2019-11-25 08:42:23 -08:00
Leonardo de Moura
ec0eed582e
chore: use isProof
2019-11-25 08:42:23 -08:00
Leonardo de Moura
120778585d
feat: add isProofQuick
2019-11-25 08:42:23 -08:00
