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

12473 commits

Author SHA1 Message Date
Sebastian Ullrich
2e5f62d44f test: parser/macro macros 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
586f515470 fix: global name resolution of macro-introduced idents 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
3f63635388 refactor: use adaptExpander in Elab.Quotation 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
05d216beb0 feat: command elaboration step trace 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
8d021e0cec fix: fresh macro scope per command 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
82078fba84 chore: make Syntax.reprint output without source info more readable 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
c08fcdb662 chore: ad-hoc match_syntax support in the new frontend 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
db2218cbfd feat: support antiquotation splices mixed with other items (quotation terms only) 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
753ecab6c1 feat: support macro-generated parser! 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
c6100ed25f feat: antiquoting rawIdent 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
912011f12f fix: variable patterns in match_syntax 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
437e1b7245 fix: elaboration of macro-generated defs 2020-01-12 10:32:27 -08:00
Sebastian Ullrich
b18e0a3373 feat: support expanding into multiple commands 2020-01-12 10:32:27 -08:00
Leonardo de Moura
64ef03d736 chore: lowercase error messages 
@cipher1024 We use lowercase error messages in Lean. I know other
systems capitalize, but we need consistency.
 2020-01-12 08:21:26 -08:00
Simon Hudon
6d8927da10 fix: little details 2020-01-12 08:02:48 -08:00
Simon Hudon
92c8773137 feat: file IO using handles 2020-01-12 08:02:48 -08:00
Leonardo de Moura
bfe8c6d060 feat: prevent adversarial users from using hugeFuel in actual code 2020-01-11 15:34:39 -08:00
Leonardo de Moura
6d77aa20aa feat: catch deep recursion at MetaM, TermElabM and CommandElabM 
cc @Kha
 2020-01-11 15:03:58 -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
246e0a5532 fix: propagate type before synthesizeSyntheticMVars 2020-01-11 12:01:12 -08:00
Leonardo de Moura
c729973742 fix: restore state when catching postpone 
Reason: avoid error messages to be generated multiple times; avoid
internal postponed mvars to leak; etc
 2020-01-11 11:57:39 -08:00
Leonardo de Moura
82a36fbfe2 feat: declare_syntax_cat without importing Init.Lean 
cc @Kha
 2020-01-11 09:02:50 -08:00
Leonardo de Moura
e817257922 feat: elaborate declare_syntax_cat 
TODO: `registerParserCategory` uses `registerAttribute` which relies
on the environment having a declaration of type `AttributeImpl`.
This is bad since forces users to import `Init.Lean`.

@Kha The key problem is that we cannot serialize `AttributeImpl`.
I will try to address this issue tomorrow. I am considering different
workarounds.
 2020-01-10 21:10:02 -08:00
Leonardo de Moura
80e00a87c6 feat: add declare_syntax_cat command parser 2020-01-10 20:38:08 -08:00
Leonardo de Moura
799914daf2 feat: registerParserCategory 2020-01-10 20:32:16 -08:00
Leonardo de Moura
3c8d8c7434 feat: add attributeExtension 2020-01-10 19:51:53 -08:00
Leonardo de Moura
48600dbbfc refactor: registerAttribute ==> registerBuiltinAttribute 2020-01-10 17:08:12 -08:00
Leonardo de Moura
f783115d21 refactor: SyntaxNode => Syntax at TermElab and CommandElab 
@Kha It is too annoying to write `.val` all over the place. Moreover,
we now have `match_syntax`.
 2020-01-10 15:17:58 -08:00
Leonardo de Moura
f73ff914eb feat: extensible elaboration functions 
@kha `termParserAttr.lean` has a small example
 2020-01-10 15:05:14 -08:00
Leonardo de Moura
63cd3a8c41 fix: nontermination at isDefEqOffset 2020-01-10 13:25:20 -08:00
Leonardo de Moura
06b6beb9f7 feat: add kabstract 2020-01-10 13:10:03 -08:00
Leonardo de Moura
3077d13b56 feat: add HeadIndex 2020-01-10 11:58:22 -08:00
Leonardo de Moura
947438afbe feat: add Occurrences 2020-01-10 11:06:36 -08:00
Leonardo de Moura
a76b104f61 chore: move Message to Lean 2020-01-10 10:58:50 -08:00
Leonardo de Moura
f8c7d6ca6b feat: elaborate optParam 2020-01-10 09:32:01 -08:00
Leonardo de Moura
d7b23cf297 fix: typo 2020-01-10 08:36:48 -08:00
Daniel Selsam
27158eb3e2 fix: DiscrTree typos 2020-01-10 08:07:41 -08:00
Leonardo de Moura
c5111de0f0 feat: add option set_option synthInstance.maxSteps <num> 
cc @dselsam @kha
 2020-01-10 08:04:25 -08:00
Leonardo de Moura
733ea89000 feat: improve application type mismatch error message 2020-01-09 16:41:27 -08:00
Leonardo de Moura
e2ad834a2c fix: weird bug that only occurs in debug mode 2020-01-09 16:11:33 -08:00
Leonardo de Moura
56d6961529 fix: old constant names 2020-01-09 15:40:55 -08:00
Leonardo de Moura
bba9cdd8ff feat: improve support for nat literals 2020-01-09 15:36:46 -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
3d1ee3f408 fix: add isNewAnswer predicate 
reactivate `typeclass_coerce.lean` test
 2020-01-09 13:37:21 -08:00
Leonardo de Moura
125faad936 fix: missing do 
This is nasty. The following
```
if entry.answers.contains answer then pure () -- if answer was already found, then do nothing
else
  let newEntry := { answers := entry.answers.push answer, .. entry };
  modify $ fun s => { tableEntries := s.tableEntries.insert key newEntry, .. s };
  entry.waiters.forM (wakeUp answer)
```
was being parsed as
```
if entry.answers.contains answer then pure () -- if answer was already found, then do nothing
else
  (let newEntry := { answers := entry.answers.push answer, .. entry };
   modify $ fun s => { tableEntries := s.tableEntries.insert key newEntry, .. s });
entry.waiters.forM (wakeUp answer)
```
 2020-01-09 12:44:41 -08:00
Leonardo de Moura
f3d4005fc6 fix: outParam support 2020-01-09 11:39:12 -08:00
Leonardo de Moura
78c50125dd fix: bug preprocessArgs 2020-01-09 11:13:25 -08:00
Leonardo de Moura
ebd20432b6 fix: isDefEqOffset 2020-01-09 10:47:02 -08:00
Leonardo de Moura
11d15575f7 feat: ignore Nat.succ, Nat.zero Nat.add and HasAdd.add at `DiscrTree 
@dselsam We need this feature to be able to retrieve instances of the
form `Top (Nat.succ ?m)` given `Top 1` where `1` is the literal `1`
 2020-01-09 10:28:09 -08:00
Leonardo de Moura
f49e1cd0fb fix: isDefEqOffset 2020-01-09 10:10:32 -08:00