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

5887 commits

Author SHA1 Message Date
Leonardo de Moura
148c0324c4 fix: do not extract closed terms from join point applications 2020-02-15 15:43:24 -08:00
Leonardo de Moura
0cf226220c fix: remove incorrect assertion 
Note that `get_cases_on_minors_range` is now parametric on `m_before_erasure`:
`get_cases_on_minors_range(env(), const_name(fn), m_before_erasure)`
 2020-02-13 18:26:12 -08:00
Leonardo de Moura
6873400193 chore: remove silent | matchFailed support 
Before this commit
```lean
pattern <- action
```
was being translated by the old frontend into
```lean
pattern <- action | matchFailed
```
This produced counterintuitive behavior, and performance problems when
tryin to synthesize `MonadFail` instances.
BTW, the new frontend does not implement this feature. I didn't even
remember the old frontend did this.
I will also remove the class `MonadFail` from stdlib.

cc @Kha @dselsam
 2020-02-10 13:15:21 -08:00
Sebastian Ullrich
47f3d54acb fix: interpreter: do not consume values in explicit unbox instructions 2020-02-06 09:36:19 -08:00
Leonardo de Moura
38e6961003 feat: MutQuot by implementedBy 2020-02-04 16:51:08 -08:00
Leonardo de Moura
850b1c90a0 feat: mark as irrelevant functions that return types 2020-02-04 15:55:21 -08:00
Leonardo de Moura
bcfaeaceab feat: change ite and dite argument order 
Motivation: make sure `propagateExpectedType` heuristic is applied in
the new frontend when processing them.
 2020-02-03 14:11:29 -08:00
Leonardo de Moura
f0f522a6d6 chore: prepare to rename old coe primitives 2020-01-28 08:18:56 -08:00
Leonardo de Moura
c7d96a6522 fix: theorem values are tasks 2020-01-16 17:20:36 -08:00
Leonardo de Moura
654b464747 chore: improve old pretty printer on numeric literals 2020-01-09 13:48:15 -08:00
Leonardo de Moura
bccaaa7af0 fix: bug at lit_type binding 
cc @kha
 2020-01-06 15:44:38 -08:00
Leonardo de Moura
8628b52b21 feat: missing support for Empty.rec 2020-01-03 18:23:52 -08:00
Sebastian Ullrich
2791cdf326 fix: interpreter::call_boxed: support under-application 
/cc @leodemoura
 2020-01-01 21:15:05 +01:00
Leonardo de Moura
73e114c6a2 chore: remove unnecessary argument 2020-01-01 09:19:00 -08:00
Sebastian Ullrich
b439de68a5 feat: support nested interpreter executions and make sure closures are run in compatible environments 
/cc @leodemoura
 2019-12-31 00:07:45 +01:00
Leonardo de Moura
28a4859832 feat: expose evalConst 
@Kha Could you please check `lean_eval_const`?
 2019-12-30 11:41:36 -08:00
Sebastian Ullrich
a2d668ec99 fix: leaks 2019-12-22 17:24:57 -08:00
Sebastian Ullrich
3b37737c8a fix: leaks 2019-12-22 15:09:19 -08:00
Leonardo de Moura
4eb6f67e7a chore: style 2019-12-16 10:48:54 -08:00
Leonardo de Moura
7d736e63b1 fix: print for string literal 2019-12-16 10:28:28 -08:00
Leonardo de Moura
8feb40e9f7 fix: add new approximation flag 
During TC, we don't want it. It allows us to find "solutions" that
trigger nontermination.
 2019-12-13 18:15:47 -08:00
Leonardo de Moura
15c8b14aad fix: is_def_eq approximation 2019-12-13 10:29:30 -08:00
Leonardo de Moura
a124461dca chore: rename projection function major field to self 
This is useful for projection function for classes + named arguments.
 2019-12-12 08:55:55 -08:00
Leonardo de Moura
b773bb9ceb fix: make sure instances created by class command are stored in the new DiscrTree 2019-12-11 17:16:12 -08:00
Sebastian Ullrich
948b0bf1f1 fix: interpreter::call_boxed: support over-application 
MetaHasEval instances were not fully eta-expanded
 2019-12-05 13:21:08 +01:00
Sebastian Ullrich
1afd3b9d01 refactor: interpreter::run_main: use call_boxed 2019-12-05 13:21:08 +01:00
Sebastian Ullrich
44ce73ced9 refactor: call generated boxed wrapper instead of reinventing it in the interpreter 2019-12-05 13:21:08 +01:00
Sebastian Ullrich
e3e50b7940 chore: rename confusing interpreter function 2019-12-05 13:21:08 +01:00
Leonardo de Moura
1784b0ee67 chore: Heq ==> HEq 2019-12-04 11:20:38 -08:00
Leonardo de Moura
f8fb195719 feat: cache local instances at metavariable declarations 2019-11-28 05:57:46 -08:00
Leonardo de Moura
4a6d0a8082 feat: projections of classes should not be reducible 2019-11-23 09:25:49 -08:00
Leonardo de Moura
73859521e9 fix: proj print 2019-11-21 16:09:35 -08:00
Leonardo de Moura
21f37e7f6a fix: fvar vs local issue 2019-11-21 10:47:44 -08:00
Sebastian Ullrich
f6973be5e3 refactor: replace C++ import parser with Lean one 
imports are now completely opaque to C++
 2019-11-21 15:52:01 +01:00
Sebastian Ullrich
44d5eddf16 chore: remove support for relative imports 2019-11-20 16:39:53 +01:00
Sebastian Ullrich
3dcd4febd9 feat: make LEAN_PATH a mapping from package names to root dirs, remove C++ impl 2019-11-20 16:39:53 +01:00
Sebastian Ullrich
c93fb5c4b2 chore: interpreter: rename misleading accessor 2019-11-19 09:36:59 +01:00
Leonardo de Moura
46adfcfdb6 refactor: Name fully implemented in Lean 2019-11-18 19:54:05 -08:00
Leonardo de Moura
b09fb4348d chore: rename Name constructors 2019-11-18 19:54:05 -08:00
Leonardo de Moura
043e011b72 fix: bug at USet 
@Kha: I found the bug. The issue was at `USet`. The argument is a
usize scalar. So, we should use `var` instead of `eval_arg`.
 2019-11-18 19:51:53 -08:00
Leonardo de Moura
3bc61e7ee9 chore: remove special support for Name in the equation compiler 2019-11-18 12:45:53 -08:00
Leonardo de Moura
85a1994bbb chore: use mkNameStr and mkNameNum for building quoted names 2019-11-18 12:45:53 -08:00
Leonardo de Moura
5e42b1df09 chore: remove dead constants 2019-11-17 09:46:56 -08:00
Leonardo de Moura
b78ac59523 refactor: Level fully implemented in Lean 2019-11-17 08:24:09 -08:00
Leonardo de Moura
a3ccbe66cf refactor: Expr fully implemented in Lean 
No hidden fields.
 2019-11-16 12:10:49 -08:00
Leonardo de Moura
85092412c7 refactor: remove Expr.FVar hack 
@Kha @dselsam:
This hack was preventing us from making `Expr` a "real" Lean type.
This was bad for a few reasons:
- It was hard to extend/modify `Expr` in Lean since we would also have
to modify the C++ code that creates the `Expr` objects with the hidden
fields.
- `Expr.lam` and `Expr.forallE` were not following the Lean layout
standard where we sort fields by size. @Kha: recall we used that to
avoid a UB. The issue with `Expr.lam` and `Expr.forallE` is that they
have a "visible" field (`BinderInfo`), which is smaller than
hidden fields such as hash code.
- `Expr.fvar` had only one field at `Expr.lean,` but four behind the
scenes.

I added a new constructor `Local` that is only accessible from C++.
It is only used in legacy code we inherited from Lean2.
We will eventually delete it.

This refactoring was quite painful since many parts of the codebase
were mixing the new `Expr.fvar` with the old `Expr.local`.
I doubt I would be able to do it without the new staging framework
@Kha built.

BTW, some of the patches are horrible. I didn't care much since we
are going to deleted the super ugly files. That being said,
you should expect new weird bevaior due to `Expr.fvar` vs `Expr.local`.

Next step: use the new `ExprCachedData` to make all `Expr` hidden visibles
accessible from Lean.

checkpoint
 2019-11-15 14:04:26 -08:00
Leonardo de Moura
0926dee83b chore: remove dead code 2019-11-15 11:53:09 -08:00
Leonardo de Moura
d9f3b4bf63 refactor: remove Expr.mvar hidden field 2019-11-15 10:04:42 -08:00
Leonardo de Moura
beac2a1af5 fix: treat panic as unreachable at ll_infer_type_fn 
Motivation: ensure the correct type `IRType` is inferred for definitions
such as
```
def f (n : UInt32) : UInt32 :=
if n == 0 then panic! "foo"
else n+1
```
 2019-11-14 21:56:09 -08:00
Leonardo de Moura
f31fcbba24 chore: remove unnecessary approximation that just complicates the code 2019-11-14 10:57:34 -08:00