Leonardo de Moura
898a08a0c1
chore: avoid Has prefix in type classes
...
closes #203
2020-10-27 18:29:19 -07:00
Leonardo de Moura
97c93ec557
chore: prepare to rename
2020-10-27 18:09:03 -07:00
Leonardo de Moura
ff493751b5
chore: HasFormat ==> ToFormat
2020-10-27 16:19:14 -07:00
Leonardo de Moura
10c32fcf94
chore: HasToString => ToString
2020-10-27 16:11:48 -07:00
Leonardo de Moura
5ea49c92bb
chore: cleanup
2020-10-27 13:26:21 -07:00
Leonardo de Moura
633578cfaf
chore: use StateRefT macro
2020-10-27 13:05:12 -07:00
Leonardo de Moura
c979d81934
refactor: add polymorphic methods for updating/querying reducibility status
2020-10-26 17:07:28 -07:00
Leonardo de Moura
bddc826648
chore: remove unnecessary liftMs
2020-10-26 16:27:45 -07:00
Leonardo de Moura
79609938a8
feat: allow universe constraints to be postponed longer
...
Before this commit, each `isDefEq u v` invocation would fail if there
were pending universe level constraints. This commit, moves the
postponed universe constraints back to the `MetaM` state.
It also adds the combinator
```lean
withoutPostponingUniverseConstraints x
```
which executes `x` and throws an error if there are pending universe
constraints. We use the combinator at `elabApp` and `elabBinders`.
Without this commit, we would fail to elaborate simple terms such as
```lean
Functor.map Prod.fst (x s)
```
because after elaborating `Prod.fst` and trying to ensure its type
match the expected one, we would be stuck at the universe constraint:
```
u =?= max u ?v
```
Another benefit of the new approach is better error messages. Instead
of getting a mysterious type mismatch constraint, we get a list of
universe contraints the system is stuck at.
cc @Kha
2020-10-26 15:50:05 -07:00
Leonardo de Moura
5481999560
chore: cleanup
2020-10-26 14:25:38 -07:00
Leonardo de Moura
91d51d06e0
chore: cleanup
2020-10-26 14:00:13 -07:00
Leonardo de Moura
13c2a8ff51
chore: remove #lang lean4 header
2020-10-25 09:54:07 -07:00
Leonardo de Moura
3f0cc1d2ec
fix: library/constructions primitives crash at kernel_exception
2020-10-24 18:52:01 -07:00
Leonardo de Moura
6ccf086b99
fix: modify mkAppM behavior and fix issue at Structural.lean
...
`Structural.lean` uses `mkAppM` for creating projections `PProd.fst`
and `PProd.snd`. However, given `x : (([Decidable p] → Bool) × Nat`,
the old ``mkApp `PProd.fst #[x]`` returned
```
Prod.fst ([Decidable p] → Bool) Nat x _inst
```
The extra unexpected argument `_inst` broke `Structural.lean`.
In the new implementation, it returns
```
Prod.fst ([Decidable p] → Bool) Nat x
```
which has type `[Decidable p] → Bool`.
2020-10-24 13:25:51 -07:00
Leonardo de Moura
d89f559683
chore: fix definitions
...
See commit before update stage0 for explanation.
2020-10-24 07:27:25 -07:00
Leonardo de Moura
21757b2be9
feat: add helper option for fixing bootstrapping issue at src/Init/Data/Int/Basic
2020-10-23 11:13:04 -07:00
Leonardo de Moura
bebd5075fd
chore: cleanup
2020-10-23 10:00:23 -07:00
Sebastian Ullrich
fc5f93331d
feat: profile new frontend
2020-10-23 18:34:47 +02:00
Leonardo de Moura
bc8b78f481
chore: cleanup
2020-10-22 16:30:06 -07:00
Leonardo de Moura
620647f2f1
refactor: simplify MonadCache and generalize instantiateExprMVars
2020-10-22 16:30:06 -07:00
Leonardo de Moura
a5a153d1fb
refactor: remove foldlFrom from PersistentArray and LocalContext
2020-10-22 16:30:05 -07:00
Leonardo de Moura
43fbfec1fd
chore: avoid Array.iterate and Array.iterateM
2020-10-22 16:30:04 -07:00
Leonardo de Moura
af968c60e6
chore: cleanup
2020-10-22 07:32:23 -07:00
Sebastian Ullrich
4e8f4fcaef
refactor: extract AttributeImplCore, introduce ParametricAttributeImpl
2020-10-22 11:59:55 +02:00
Leonardo de Moura
82ee2e361b
chore: cleanup
2020-10-21 18:43:47 -07:00
Leonardo de Moura
ea829b75c0
chore: remove coercions for old frontend
2020-10-21 17:37:35 -07:00
Leonardo de Moura
299a89e2c0
fix: missing instantiateMVars
2020-10-20 14:43:32 -07:00
Leonardo de Moura
dcd3068b42
chore: improve error messages
2020-10-20 14:22:01 -07:00
Leonardo de Moura
80a0200ab2
chore: move to new frontend
...
@Kha another significant milestone: all files at `src/Lean/Meta` are
being compiled with the new frontend.
2020-10-20 10:59:02 -07:00
Leonardo de Moura
8d8e8f7556
chore: move to new frontend
2020-10-20 09:33:50 -07:00
Leonardo de Moura
ddf4669d5d
chore: move to new frontend
2020-10-20 09:33:50 -07:00
Leonardo de Moura
27205ddff7
chore: move to new frontend
2020-10-20 09:33:50 -07:00
Leonardo de Moura
8dffd752a8
chore: move to new frontend
2020-10-20 09:33:50 -07:00
Leonardo de Moura
1b6d1a83c7
chore: move to new frontend
2020-10-20 09:33:50 -07:00
Leonardo de Moura
69dfb23805
chore: move to new frontend
2020-10-19 15:43:32 -07:00
Leonardo de Moura
86ab4d4029
chore: move to new frontend
2020-10-19 15:38:47 -07:00
Leonardo de Moura
1495f403a1
chore: use builtin_initialize instead of initialize at src/Lean
2020-10-19 15:17:02 -07:00
Leonardo de Moura
ef18b0ab49
chore: use [builtinInit]
2020-10-19 14:58:38 -07:00
Leonardo de Moura
e4b2614f5b
chore: move to new frontend
2020-10-19 13:21:15 -07:00
Leonardo de Moura
d9daa68d54
chore: move to new frontend
2020-10-19 13:14:14 -07:00
Leonardo de Moura
97be6fa3a5
chore: move to new frontend
2020-10-19 12:43:00 -07:00
Leonardo de Moura
9995eb7ece
chore: move to new frontend
2020-10-19 12:22:26 -07:00
Leonardo de Moura
c3897fff31
chore: move to new frontend
2020-10-19 12:15:48 -07:00
Leonardo de Moura
ab047cc4d1
chore: remove unnecessary file
2020-10-19 12:12:03 -07:00
Leonardo de Moura
a13569ab0f
chore: move to new frontend
2020-10-19 12:04:50 -07:00
Leonardo de Moura
9778eca9b2
chore: move to new frontend
2020-10-19 11:50:42 -07:00
Leonardo de Moura
7f5ef0c30b
chore: move to new frontend
2020-10-19 11:38:00 -07:00
Leonardo de Moura
e54a207986
refactor: provide Options to lean_eval_const
...
add `ImportM` monad for `addImportedFn`
cc @Kha
2020-10-19 10:21:38 -07:00
Leonardo de Moura
d3946e49f4
chore: move to new frontend
2020-10-19 06:13:11 -07:00
Leonardo de Moura
9abe45ae4f
chore: move to new frontend
2020-10-19 06:03:09 -07:00
