Leonardo de Moura
42642a2890
fix: new_frontend command issue
2020-01-15 20:53:23 -08:00
Simon Hudon
92c8773137
feat: file IO using handles
2020-01-12 08:02:48 -08:00
Leonardo de Moura
5eebda7e34
chore: add workaround for allowing new frontend to see old frontend exports
2020-01-11 13:44:22 -08:00
Leonardo de Moura
fe09e99fef
chore: disable attribute features that are not currently being used
2020-01-08 15:49:55 -08:00
Leonardo de Moura
8e7c719ee8
chore: Pi => forall
2020-01-07 11:15:40 -08:00
Leonardo de Moura
091cc48901
feat: expose old pretty printer in Lean
2020-01-07 10:29:10 -08:00
Leonardo de Moura
477d53f2dd
fix: position information
2020-01-06 21:07:41 -08:00
Leonardo de Moura
e0ae6068d4
chore: set end_pos
2020-01-06 21:00:52 -08:00
Leonardo de Moura
139d6c64e6
feat: add new_frontend command
...
cc @kha
2020-01-06 20:44:53 -08:00
Leonardo de Moura
c650e11d6b
fix: missing isUnsafe fieldat OpaqueVal
2019-12-30 11:53:08 -08:00
Sebastian Ullrich
1f2040727c
feat: autogenerate antiquotations in parser!
2019-12-30 08:24:29 -08:00
Sebastian Ullrich
88a924b728
feat: support (almost) proper name resolution in quotations in the old frontend
2019-12-18 20:11:45 -08:00
Sebastian Ullrich
6a2dbad53f
feat: match_syntax support in the old parser
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
2310ec2413
chore: separate C++ calls for parsing & expansion
2019-12-17 12:16:34 -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
820016e09a
chore: remove dead code
2019-12-12 07:58:55 -08:00
Leonardo de Moura
820f57880f
chore: compilation warning
2019-12-11 09:53:28 -08:00
Sebastian Ullrich
52c97e7bee
feat: integrate quotation terms into old parser
2019-12-10 22:45:35 +01: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
fde58d8fe4
feat: add Lean.MetaHasEval, rename HasEval to Lean.HasEval
2019-12-05 13:20:24 +01:00
Leonardo de Moura
b6dde16be5
chore: remove #synth debugging command
2019-12-03 14:51:54 -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
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
3980194fbf
chore: more assertions and old code
2019-11-19 12:55:02 +01: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
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
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
d9f3b4bf63
refactor: remove Expr.mvar hidden field
2019-11-15 10:04:42 -08:00
Leonardo de Moura
fd66963e85
chore: remove dead code
2019-11-14 15:24:18 -08:00
Leonardo de Moura
c4d974eb89
feat: allow attributes to be applied before elaboration
...
This is useful when the attribute may influence the elaboration of the declaration.
2019-11-13 15:40:19 -08:00
Leonardo de Moura
7dbb927144
chore: temporary hack
...
cc @kha
2019-11-11 11:30:22 -08:00
Sebastian Ullrich
17b8ac894a
fix: parser error recovery should be silent and be able to skip more than one token
2019-11-10 09:01:43 -08:00
Sebastian Ullrich
1442c1b377
feat: call linters on non-mutual definitions
2019-11-09 15:43:37 -08:00
Leonardo de Moura
dce1de3905
chore: remove transparency_mode::None
2019-11-08 10:04:06 -08:00
Leonardo de Moura
f88561ae68
feat: add trace! macro
2019-10-22 16:08:37 -07:00
Sebastian Ullrich
9b55687597
fix: show #eval errors
2019-10-18 13:10:13 +02:00
Sebastian Ullrich
7c56754495
feat: profile #synth calls
2019-10-18 11:27:55 +02:00
Sebastian Ullrich
ef6853979f
fix: syntax for universe parameters in axiom
2019-10-08 18:11:37 +02:00
Leonardo de Moura
4793cbfa9a
feat: add #[elem1, elem2, ..] notation for creating arrays
...
@kha @dselsam: I added this notation because I am tired of writing
`[elem1, elem2, ...].toArray`. BTW, the new notation is based on the
one available in SML.
2019-10-07 15:36:44 -07:00
Leonardo de Moura
5801e0e65a
fix: print module name instead of file name
2019-10-04 20:02:43 -07:00
Leonardo de Moura
0714716477
fix: file and import names, tests and stage0
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2019-10-04 17:04:02 -07:00
Leonardo de Moura
e596089a2d
chore: one module per import command
2019-10-04 12:27:47 -07:00
Daniel Selsam
a82266c652
feat(library/init/lean/typeclass): #synth with tabled resolution
2019-10-03 17:23:53 -07:00
Leonardo de Moura
261c0b9c24
feat(frontends/lean): add panic! macro
...
cc @dselsam
2019-09-30 17:16:19 -07:00
Leonardo de Moura
d6ea1d1a3f
feat(frontends/lean/builtin_cmds): add #synth command
2019-09-24 11:32:43 +08:00
Leonardo de Moura
345cc22f79
feat(frontends/lean/elaborator): do not create checkpoint at let x := v;
2019-09-21 10:27:30 -07:00
