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

11961 commits

Author SHA1 Message Date
Leonardo de Moura
2afb60cc07 fix: typo 2019-11-24 06:59:52 -08:00
Leonardo de Moura
8d30b7d3fb doc: document DiscrTree module 2019-11-24 06:51:17 -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
4a6d0a8082 feat: projections of classes should not be reducible 2019-11-23 09:25:49 -08:00
Leonardo de Moura
84d582bf9a feat: add DiscrTree.insert 2019-11-23 09:07:21 -08:00
Leonardo de Moura
c6048f0f94 feat: generalize binInsert 2019-11-23 08:20:20 -08:00
Leonardo de Moura
013bc5b589 feat: add modifyM 2019-11-23 07:37:33 -08:00
Leonardo de Moura
2e610227e4 feat: add Array.binInsert 2019-11-22 18:22:26 -08:00
Leonardo de Moura
69723b48c3 feat: add Array.insertAt 2019-11-22 17:42:27 -08:00
Leonardo de Moura
ea2d971bd3 chore: add isDefEq abbreviation for isExprDefEq 
Most tactic users will never use `isLevelDefEq`.
 2019-11-22 11:54:06 -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
b0ee140670 chore: trace messages 2019-11-22 11:18:48 -08:00
Leonardo de Moura
a9a27c77d8 feat: add helper combinators 2019-11-22 11:09:01 -08:00
Leonardo de Moura
ba7d14ebc2 fix: default path 2019-11-22 07:58:05 -08:00
Leonardo de Moura
b21559b338 chore: move Makefile.in 2019-11-22 07:48:04 -08:00
Leonardo de Moura
c445199747 chore: library/Init ==> src/Init 
cc @Kha @dselsam @cipher1024
 2019-11-22 06:06:05 -08:00
Leonardo de Moura
4adacf1413 chore: src/init ==> src/initialize 2019-11-22 04:59:13 -08:00
Leonardo de Moura
3fb49fa765 chore: remove broken assertion 
@Kha I just commented it since we will soon delete this module.
 2019-11-21 16:15:57 -08:00
Leonardo de Moura
73859521e9 fix: proj print 2019-11-21 16:09:35 -08:00
Sebastian Ullrich
e426e5dd28 chore: add CCACHE option, on by default if available 2019-11-21 13:11:02 -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
86a678f90e chore: move clean-stdlib out of Makefile so that it can be executed even with broken .depend files 
/cc @leodemoura
 2019-11-21 15:46:15 +01:00
Sebastian Ullrich
0571a1c913 chore: use paths instead of indices for stdlib tests 2019-11-20 08:07:28 -08:00
Leonardo de Moura
49f1f0dfe3 chore: apply required change after update-stage0 
cc @Kha
 2019-11-20 08:00:11 -08:00
Sebastian Ullrich
44d5eddf16 chore: remove support for relative imports 2019-11-20 16:39:53 +01:00
Sebastian Ullrich
33ce758126 feat: assume A in --plugin A.so is package name and use it to synthesize initializer symbol name 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
ab42cffad2 refactor: rename all Default.lean files except for Init/Default.lean 2019-11-19 13:52:21 +01:00
Sebastian Ullrich
3980194fbf chore: more assertions and old code 2019-11-19 12:55:02 +01:00
Sebastian Ullrich
11809d23a9 chore: remove outdated assertion 
/cc @leodemoura
 2019-11-19 10:56:35 +01:00
Sebastian Ullrich
c93fb5c4b2 chore: interpreter: rename misleading accessor 2019-11-19 09:36:59 +01:00
Leonardo de Moura
269f20efe8 fix: ensure C++ and Lean use the same hash for Name 2019-11-18 19:54:05 -08:00
Leonardo de Moura
46adfcfdb6 refactor: Name fully implemented in Lean 2019-11-18 19:54:05 -08:00
Leonardo de Moura
cba3dabcec chore: update stage0 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
3ae5c2f2e4 chore: remove old comment 2019-11-15 14:11:50 -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
aea02eb1f8 chore: fix MVar refactoring issues 2019-11-15 10:04:42 -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
eb52fbca10 chore: skip stdlib tests on Windows 2019-11-14 17:00:04 -08:00
Leonardo de Moura
fd66963e85 chore: remove dead code 2019-11-14 15:24:18 -08:00