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

696 commits

Author SHA1 Message Date
Leonardo de Moura
993ae96fb7 chore: elaborate let_core 2020-01-25 15:21:47 -08:00
Leonardo de Moura
5796eba368 chore: add elabLetDeclAux 2020-01-25 15:14:28 -08:00
Leonardo de Moura
58833e6f79 chore: add let_core 
We want to change the representation of `let` terms.
`let_core` is a temporary syntax for helping us with the translation.
 2020-01-25 15:08:36 -08:00
Leonardo de Moura
bdb9f4c86e feat: allow raw identifiers to be used where terms are expected 
@Kha this commit fix another example of weird error message I have
experienced in the last few days.

The macro
```lean
syntax "case!" ident ":" term "with" term "," term : term
macro_rules
| `(case! $h : $cond with $t, $e) =>
  `((fun $h => cond $h $t $e) $cond)
```
is accepted, but as in `fun` binders, we get a weird error when
trying to elaborate an instance of the macro.
Example:
```lean
check case! h : 0 == 0 with h, not h
```
 2020-01-25 14:55:32 -08:00
Leonardo de Moura
7b6caba457 feat: add `ident as a valid elaboration kind 2020-01-25 14:55:32 -08:00
Leonardo de Moura
6d5de9f965 feat: handle raw identifiers as binders in fun 
@Kha I am adding this kind of feature to improve the user experience.
For example, the macro
```
syntax "[" ident "↦" term "]" : term
macro_rules
| `([$x ↦ $v]) => `(fun $x => $v)
```
is accepted and looks perfectly reasonable.
However, before this commit, we would get a nasty error when
elaborating
```lean
check [x ↦ x + 1]
```
 2020-01-25 14:55:21 -08:00
Sebastian Ullrich
2509b3913a Revert "feat: add std streams" 
This reverts commit 7575a32035.
 2020-01-25 16:32:06 +01:00
Sebastian Ullrich
0be2424910 Revert "feat: override standard streams" 
This reverts commit bd87ea5d5e.
 2020-01-25 16:32:06 +01:00
Sebastian Ullrich
b760692a26 Revert "fix: thread local storage of std streams" 
This reverts commit 961861ceab.
 2020-01-25 16:32:06 +01:00
Sebastian Ullrich
a4858bf9f9 Revert "feat: MonadIO now extends MonadExcept IO.Error" 
This reverts commit c0a7495495.
 2020-01-25 16:32:06 +01:00
Sebastian Ullrich
88fe0de284 fix: default LEAN_PATH for installed Lean 2020-01-25 15:58:06 +01:00
Sebastian Ullrich
5c0fa84af5 feat: barely implement do elaboration 2020-01-25 15:57:41 +01:00
Sebastian Ullrich
02c773bc70 refactor: further Quotation cleanup 2020-01-25 13:47:27 +01:00
Sebastian Ullrich
093518725c refactor: minor cleanups for standalone expander 2020-01-25 11:58:29 +01:00
Leonardo de Moura
aa045f3b07 feat: safer mkCIdentFrom 
cc @Kha
 2020-01-24 17:23:21 -08:00
Leonardo de Moura
364bb7bdf7 fix: proper Name literals 
cc @kha
 2020-01-24 12:38:15 -08:00
Leonardo de Moura
35179809a2 feat: hide macro scopes encoding when displaying errors 2020-01-23 15:33:02 -08:00
Leonardo de Moura
060a68d73f feat: remove addMacroScope approximation 2020-01-23 14:59:31 -08:00
Leonardo de Moura
ed6cb007d0 refactor: ExtractMacroScopesResult => MacroScopesView, add MacroScopesView.review 2020-01-23 14:11:32 -08:00
Leonardo de Moura
c309f1dccd chore: remove unnecessary field 2020-01-23 13:05:27 -08:00
Leonardo de Moura
b47caaa0a5 refactor: notation and macro commands are now just macros 2020-01-23 13:04:21 -08:00
Leonardo de Moura
9359a6569a feat: add [builtinMacro] 2020-01-23 12:54:04 -08:00
Leonardo de Moura
954c69de35 feat: use macroscopes for creating fresh kinds 2020-01-23 12:38:31 -08:00
Leonardo de Moura
d99ef11447 fix: nested addMacroScope 2020-01-23 12:36:37 -08:00
Leonardo de Moura
e681bd71d9 feat: simplify MacroM 2020-01-23 12:22:33 -08:00
Leonardo de Moura
0228f9c9b7 chore: remove addMacroScopeExt 2020-01-23 12:08:20 -08:00
Leonardo de Moura
6fdcb1c192 chore: prepare to remove addMacroScopeExt 2020-01-23 12:02:45 -08:00
Leonardo de Moura
4ef8aa347a feat: missing case 2020-01-23 11:46:29 -08:00
Leonardo de Moura
fab256d4cc feat: improve macroscope encoding 2020-01-23 11:33:35 -08:00
Leonardo de Moura
87d002bb43 feat: extend MacroM 
It now has access to `mainModule` and a name generator.
 2020-01-23 09:48:37 -08:00
Leonardo de Moura
98ee6e9734 refactor: move NameGenerator to LeanInit 2020-01-23 08:49:58 -08:00
Leonardo de Moura
67535441ad fix: macroTail issue 
cc @Kha
 2020-01-22 20:14:09 -08:00
Leonardo de Moura
764b854742 fix: bug at longestMatchStep 
@Kha I found the bug by accident when I was playing with the
bigop.lean
 2020-01-22 17:31:54 -08:00
Leonardo de Moura
3f24b31286 chore: remove leftover 2020-01-22 16:50:05 -08:00
Leonardo de Moura
1ff7950a77 feat: use truncateTrailing at error messages 2020-01-22 16:19:07 -08:00
Leonardo de Moura
ae84270226 feat: include result of sequence of macro expansions 
@Kha I added this feature to help debugging macros.
I was using `set_option trace.Elab true` as a workaround, but it is
too verbose.
For example, in the following buggy code

```
new_frontend

macro "foo" x:term : term => `(x + 1)
macro "bla" x:term : term => `(foo $x)
```

We get the error message
```
<input>:6:11: error: unknown identifier 'x.15'
with resulting expansion
   x  +  1
while expanding
   foo 1
while expanding
  bla 1
```

Perhaps we should preserve the macroscopes at "with resulting
expansion". Anyway, I think it is better than the previous error.

```
<input>:6:11: error: unknown identifier 'x.15'
while expanding
   foo 1
while expanding
  bla 1
```
 2020-01-22 16:08:07 -08:00
Leonardo de Moura
37e83651f0 fix: postpone synthesizeUsingDefault 2020-01-22 14:09:05 -08:00
Leonardo de Moura
e57289f98e feat: handle new HasOfNat.ofNat at evalNat 2020-01-22 13:55:13 -08:00
Leonardo de Moura
a7a36f80bb feat: add termIdToAntiquot 2020-01-22 13:18:09 -08:00
Leonardo de Moura
5193ce45e4 refactor: move Syntax helper functions to LeanInit 2020-01-22 12:58:06 -08:00
Leonardo de Moura
a5bcebb07f feat: add antiquotation support for strLit, numLit and charLit 2020-01-22 12:57:28 -08:00
Leonardo de Moura
0be31c14ec fix: workaround for term parser antiquotation issue 
@Kha this is a temporary workaround. We should discuss how to cleanup
in the next Dev meeting.
 2020-01-22 12:05:12 -08:00
Leonardo de Moura
642850efb2 fix: antiquotation for all categories 2020-01-22 11:52:08 -08:00
Leonardo de Moura
e8c54ad1bf fix: use nonReservedSymbol when defining tactic new syntax 2020-01-21 14:37:29 -08:00
Leonardo de Moura
a83487ca5f chore: simplify toParserDescr 2020-01-21 14:00:29 -08:00
Leonardo de Moura
14347456d7 feat: extensible tactics 2020-01-21 13:25:45 -08:00
Leonardo de Moura
6f9f581566 feat: add Syntax.identToAtom 2020-01-21 13:25:20 -08:00
Leonardo de Moura
8fb710c31e chore: remove simple parser kind 
Now, the previous commit makes sure pratt's parsers subsume simple parsers
 2020-01-21 09:16:38 -08:00
Leonardo de Moura
f3c1928d2d feat: improve prattParser tables 
We can delete the simple category after this change

cc @Kha
 2020-01-21 09:16:38 -08:00
Leonardo de Moura
67fb63c9fd feat: use mpz_pow_ui to implement Nat.pow 2020-01-21 09:16:38 -08:00