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

475 commits

Author SHA1 Message Date
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
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
Leonardo de Moura
2a8e179a64 feat: add #synth command to new frontend 2020-01-09 09:54:45 -08:00
Leonardo de Moura
923bd321ef chore: remove unnecessary commands 2020-01-09 09:45:07 -08:00
Leonardo de Moura
5888a790d1 feat: add #synth command to new frontend 2020-01-09 09:42:22 -08:00
Leonardo de Moura
c06d515027 fix: typo 2020-01-08 21:22:46 -08:00
Leonardo de Moura
48578c9743 chore: remove hacks 2020-01-08 21:09:17 -08:00
Leonardo de Moura
b2fa433368 chore: add more info to error messages 2020-01-08 21:09:17 -08:00
Leonardo de Moura
d92e59a6fb chore: add temporary staging workaround 2020-01-08 21:09:17 -08:00
Leonardo de Moura
01c5b0710c feat: pointer equality for IO.ref 2020-01-08 21:09:17 -08:00
Leonardo de Moura
c98e3290e4 refactor: parser attributes 2020-01-08 21:09:11 -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
e056908933 fix: getDeclNamesForCodeGen 2020-01-08 15:11:49 -08:00
Leonardo de Moura
9ebf21f2d5 fix: elabConstant 2020-01-08 15:06:18 -08:00
Leonardo de Moura
c4ad3a2390 refactor: ParserContextCore and ParserContext 2020-01-08 14:20:53 -08:00