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

99 commits

Author SHA1 Message Date
Sebastian Ullrich
5e334b3e90 chore: postpone TSyntax adoption for some parts 
The namespace `TSyntax.Compat` can be opened for a coercion
`Syntax -> TSyntax k` for any `k`, as otherwise this PR would never be done.
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
6982536108 fix: one more struct instance syntax manipulation 2022-06-16 23:33:57 +02:00
Sebastian Ullrich
ce054fb2e7 fix: introduce semicolonOrLinebreak, replace many(1) with sepBy(1) where appropriate 2022-06-16 23:33:57 +02:00
Leonardo de Moura
041827bed5 chore: unused variables 2022-06-07 17:54:10 -07:00
Sebastian Ullrich
fb2a2b3de2 fix: fixup previous commit 2022-06-07 16:37:45 -07:00
Sebastian Ullrich
ae7b895f7a refactor: unname some unused variables 2022-06-07 16:37:45 -07:00
Leonardo de Moura
66c82dadc9 fix: the default value for structure fields may now depend on the structure parameters 2022-04-21 17:38:19 -07:00
Leonardo de Moura
0bd9de1cb9 perf: add InstantiateLevelCaches for types and values at CoreM 2022-03-15 17:42:38 -07:00
Leonardo de Moura
7850dc023b fix: make sure the structure instance notation does not leak auxiliary type annotations (e.g., autoParam and optParam) 2022-03-10 08:41:00 -08:00
Sebastian Ullrich
2c7d67d498 fix: make info of fields synthesized by structure update synthetic 2022-02-06 08:50:07 -08:00
Leonardo de Moura
12e2a79170 chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
Sebastian Ullrich
4063729b6c doc: document some built-in term notations 2021-11-26 17:13:19 +01:00
Leonardo de Moura
9a152d2051 fix: use withSynthesize at elabStructInstance 
fixes #783
 2021-11-15 16:45:26 -08:00
Gabriel Ebner
bfc74decde feat: add info field to Syntax.node 2021-10-26 20:19:27 +02:00
Leonardo de Moura
2994747ed9 chore: remove workaround 2021-08-13 18:25:32 -07:00
Leonardo de Moura
4b58c4cc02 refactor: instances that "hide" coercions 
Example:
```
instance [CoeHTCT α β] [Add β] : HAdd α β β where
  hAdd a b := Add.add a b
```
 2021-08-13 17:18:55 -07:00
Leonardo de Moura
a6b6d61b39 chore: simplify mkProjStx? 2021-08-12 09:50:43 -07:00
Leonardo de Moura
da03262937 fix: check redundant sources at structure instance notation 2021-08-12 09:16:30 -07:00
Leonardo de Moura
c68882ca67 feat: structure instance notation with multiple sources 
closes #462
closes #463
 2021-08-12 06:18:47 -07:00
Leonardo de Moura
a02a490a10 feat: add mkProjStx? 2021-08-12 05:41:00 -07:00
Leonardo de Moura
accf198a88 feat: add ExplicitSourceInfo 2021-08-12 04:29:19 -07:00
Leonardo de Moura
c591902547 refactor: add structure to Source.explicit 2021-08-12 04:10:47 -07:00
Leonardo de Moura
45e4dc26e1 refactor: simplify Source.explicit 2021-08-12 03:40:30 -07:00
Leonardo de Moura
67103f54a9 chore: add TODOs for multiple sources 2021-08-11 19:28:49 -07:00
Leonardo de Moura
d78101f00d chore: remove mutual recursion workaround 
It was a leftover hack for the old frontend.
 2021-08-11 16:57:53 -07:00
Leonardo de Moura
4abbb3d74c chore: cleanup 2021-08-11 16:05:07 -07:00
Leonardo de Moura
f1738ce2a0 feat: add macro for expanding field abbrev notation 
The new macro allows us to use the field abbrev notation in patterns
too. See new test.
 2021-08-11 16:02:50 -07:00
Leonardo de Moura
09c2b668e6 feat: allow multiple sources in the structure instance parser 
This commit also fixes some macros, and make sure the elaborator still
works, but it does not support multiple sources yet.
 2021-08-11 13:07:56 -07:00
Leonardo de Moura
63ad42ba47 refactor: move and generalize reduceProj? 2021-08-10 20:21:04 -07:00
Leonardo de Moura
3f3e5d9dcb fix: private field + default value bug 2021-08-09 19:01:08 -07:00
Leonardo de Moura
0869bbe558 fix: missig registerMVarErrorImplicitArgInfo for postponed instance mvars 2021-08-04 16:58:00 -07:00
Leonardo de Moura
cfb7e27b87 fix: isStructure vs isStructureLike 2021-08-02 18:54:19 -07:00
Wojciech Nawrocki
f51b80060d feat: generic tagged Format 2021-08-01 09:58:44 +02:00
Leonardo de Moura
3f22d5f624 feat: take auto params into account in the structure instance notation 
closes #461
 2021-07-27 15:49:23 -07:00
Leonardo de Moura
714cadfb31 fix: bug at structure instance notation 
It was exposed by the second example at #461.
 2021-07-27 11:56:33 -07:00
Wojciech Nawrocki
dfcdc57302 feat: go-to for structure fields 2021-07-05 19:42:01 +02:00
Leonardo de Moura
953dd85c06 chore: avoid inline 2021-06-28 10:17:01 -07:00
Leonardo de Moura
ae6a28af52 chore: remove unnecessary specialize 2021-06-28 10:11:23 -07:00
Leonardo de Moura
e8aa02cd51 feat: closes #415 2021-05-03 18:04:01 -07:00
Leonardo de Moura
1e41e2eb4a chore: use double backticks 2021-05-03 14:26:27 -07:00
Leonardo de Moura
292bab5a11 fix: loop due to error recovery 2021-04-13 08:12:39 -07:00
Leonardo de Moura
7de9cfeac8 chore: fix StructInst and add mkGroupNode 2021-04-07 22:46:07 -07:00
Leonardo de Moura
578b3b822f fix: do not use nullKind for group combinator 
We use `nullKind` for the `group` parser combinator.
When pattern matching `nullKind` nodes, we check their arities.
So, error recovery often fails for parsers that use the `group`
combinator.
For example, we have the parser
```
def whereDecls := leading_parser "where " >> many1Indent (group (letRecDecl >> optional ";"))
```
If there is syntax error at `letRecDecl`, the node corresponding to
```
group (letRecDecl >> optional ";")
```
will contain only one child, and the pattern matching at
```
def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
  match whereDecls with
  | `(whereDecls|where $[$decls:letRecDecl $[;]?]*) => `(let rec $decls:letRecDecl,*; $body)
  | _ => Macro.throwUnsupported
```
fails, and we can't elaborate the partial syntax tree for
`letRecDecl`, and auto-completion will not work there.

We address this issue by using a new kind for the `group` combinator.
The idea is to pattern match `group` as we pattern match `node`s with
proper syntax node kinds. This change is consistent with the way we
use `group` where it mainly a convenience for saving us the trouble of
defining a new parser definition that is used only once.
 2021-04-07 22:30:51 -07:00
Leonardo de Moura
566fad77d4 chore: helper methods 2021-03-27 18:48:03 -07:00
Leonardo de Moura
dc87bef04c fix: error message 
This is a fix for bug reported by @JasonGross at Zulip
 2021-03-11 12:16:15 -08:00
Leonardo de Moura
be841a7cad chore: throwError! => throwError, throwErrorAt! => throwErrorAt 
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
 2021-03-11 11:59:45 -08:00
Leonardo de Moura
164577d94e chore: remove parser! and tparser! 
The new macros are called "leading_parser` and `trailing_parser`.

cc @Kha
 2021-03-11 09:36:58 -08:00
Leonardo de Moura
68143ca8ba chore: trace[...]! ==> trace[...] 
@Kha I think this one is a good change, there is no real reason for
using the `!` suffix here.
 2021-03-10 18:44:43 -08:00
Leonardo de Moura
5e0b6a404f chore: naming convention 2021-02-11 15:05:26 -08:00
Leonardo de Moura
ea0fda39bc chore: Declaration.lean naming convention 
`Declaration.lean` was one of the first Lean 4 files, and was still
using an old naming convention.

cc @Kha
 2021-01-20 17:07:02 -08:00