Leonardo de Moura
067dca5a65
chore: naming convention
2019-12-15 18:28:00 -08:00
Leonardo de Moura
248cc2ec3a
chore: naming convention
2019-12-15 07:48:42 -08:00
Leonardo de Moura
ac86983128
chore: naming convention
2019-12-15 07:40:32 -08:00
Leonardo de Moura
4184165573
feat: enable foApprox and ctxApprox during type class instance synthesis
2019-12-13 19:24:00 -08:00
Leonardo de Moura
93d987461a
chore: naming convention
2019-12-13 19:17:45 -08:00
Leonardo de Moura
119742e463
feat: make sure MetaM also implements new unifier approximation
2019-12-13 19:12:53 -08:00
Leonardo de Moura
34332ecaa9
fix: forallBoundedTelescope
2019-12-11 18:08:41 -08:00
Leonardo de Moura
4b285a48dc
fix: forallMetaTelescopeReducing
2019-12-11 18:03:11 -08:00
Leonardo de Moura
77bf2a60e1
fix: lambdaMetaTelescope
2019-12-11 17:50:34 -08:00
Leonardo de Moura
e13a10fbf2
feat: elaborate explicit and implicit arguments
2019-12-11 09:04:26 -08:00
Leonardo de Moura
c3005671f5
chore: avoid ^do ...
2019-12-11 06:19:12 -08:00
Leonardo de Moura
1352619ee4
refactor: MonadTracer and helper functions
...
This commit adds
- `addContext : MessageData -> m MessageData` method. We need it to
make sure we wrap the message with the current context. Before this
commit I had to redefine `trace` for `MetaM`, `SynthM`, and
`TermElabM`.
- polymorphic `traceM` method.
2019-12-08 09:05:15 -08:00
Leonardo de Moura
dd0b71938d
feat: register Meta tracing options
2019-12-05 06:38:28 -08:00
Sebastian Ullrich
92380ec5bd
feat: implement MetaHasEval for MetaM
2019-12-05 13:20:24 +01:00
Leonardo de Moura
cc5a3cca29
chore: move helper modules to src/Init/Lean/Util
2019-12-04 17:17:34 -08:00
Leonardo de Moura
f15af1df0a
chore: move Lean auxiliary datatypes to src/Init/Lean/Data
2019-12-04 17:00:13 -08:00
Leonardo de Moura
e3b8013c4e
feat: add mkAppM
...
This is the generic application builder.
2019-12-04 16:12:24 -08:00
Leonardo de Moura
ad54d8e024
feat: add helper functions
2019-12-04 12:43:24 -08:00
Leonardo de Moura
43fc18eb41
fix: incorrect local context being used to create new metavariables
2019-12-03 13:31:24 -08:00
Leonardo de Moura
98f9ec8b07
refactor: avoid code explosion generated by telescope functions
2019-12-03 12:28:54 -08:00
Leonardo de Moura
3eabda1c4d
feat: add withMCtx
2019-12-02 12:48:34 -08:00
Leonardo de Moura
798001af75
refactor: do not save/restore cache at withNewMCtxDepth
2019-12-02 11:17:20 -08:00
Leonardo de Moura
770649ce1d
refactor: do not save/restore cache at "telescope" methods
...
@kha @dselsam FYI
The original motivation for saving/restoring the cache was not
correctness, but cache size management. When we go inside a binder
using the telescope methods, we extend the local context with new fresh
free variables, execute the action `k` using the new extended local
context, and then restore it. Any cached result containing these
fresh variables is dead after executing `k`. So, `savingCache` here
could be viewed as a "checkpoint". However, it also removes any
cached entry that does not contain the new fresh variables.
I found this inconvenient in practice, and it is the wrong choice
in a few cases. Example: we have a `forall` expr (aka arrow), and use a
telescope to go inside, and then invoke TC. If the telescope uses
`savingCache`, we lose the cached TC instance witness. This is
wasteful since the witness often doesn't even depend on the new fresh
free variables created by the telescope.
Thus, this commit removes the `savingCache` occurrences from
the "telescope" methods. Users may still manually use it if
they think it is appropriate. That is, they can write
```lean
savingCache $ forallTelescope e $ fun xs body => <code>
```
if they really want to discard any new cache entry created while
executing `<code>`.
2019-12-02 11:11:49 -08:00
Leonardo de Moura
00a5860ce6
feat: add withMVarContext
...
cc @dselsam @kha
2019-12-02 10:50:00 -08:00
Leonardo de Moura
5682c6e33b
feat: add hasAssignableMVar
2019-12-01 18:32:48 -08:00
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
00b991baf6
feat: add openAbstractMVarsResult
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
3bc5e144a2
feat: add synthInstance cache
2019-12-01 18:32:48 -08: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
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
81278c1509
feat: add instanceExtension
...
Use discrimination trees indexing type class instances.
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
1f815ac521
feat: add forallMetaTelescope
2019-11-26 17:01:36 -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
0592dae46f
chore: rename confusing field name ParamInfo.prop ==> ParamInfo.proof
...
The type of the parameter is a proposition, but the parameter itself
is a proof.
2019-11-25 08:42:23 -08:00
Leonardo de Moura
63d3429246
fix: reducibility setting should not hide non-definitions (constructors, inductive types, etc)
2019-11-23 09:36:22 -08:00
Leonardo de Moura
ad3f5b2490
feat: ensure trace messages at MetaM save Environment, MetavarContext, and LocalContext
2019-11-22 11:50:19 -08:00
Leonardo de Moura
a9a27c77d8
feat: add helper combinators
2019-11-22 11:09:01 -08:00
Leonardo de Moura
c445199747
chore: library/Init ==> src/Init
...
cc @Kha @dselsam @cipher1024
2019-11-22 06:06:05 -08:00
