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

124 commits

Author SHA1 Message Date
Leonardo de Moura
2563d03ae2 feat: add notFollowedBy 2020-08-31 15:37:41 -07:00
Sebastian Ullrich
75b2dc1baf refactor: simplify ppModule using new module parser 2020-08-31 15:44:58 +02:00
Sebastian Ullrich
2418d851fc feat: declarative module parser 
/cc @leodemoura
 2020-08-31 14:45:21 +02:00
Leonardo de Moura
e3f3a1db8f feat: add refine! tactic syntax 2020-08-30 16:00:24 -07:00
Leonardo de Moura
6f0e9452b2 chore: remove begin ... end syntax 
We should use `by { ... }` from now on.

cc @Kha
 2020-08-30 14:15:33 -07:00
Leonardo de Moura
0a0ca9f930 fix: funImplicitBinder 2020-08-30 08:10:58 -07:00
Leonardo de Moura
b4f938d859 chore: namedHole => syntheticHole 2020-08-30 08:04:15 -07:00
Leonardo de Moura
89e0fa1488 chore: allow ?_ 
Note that `?_` is not equivalent to `_`. Both do not have a name, but
`?_` is a synthetic metavariable which **cannot** be assigned by typing
constraints, and `_` is a regular metavariable.
We use `?_` to mark an anonymous hole that must be filled using tactics.

@Kha I will rename `namedHole` to `syntheticHole`
 2020-08-30 07:54:34 -07:00
Leonardo de Moura
825d9643cd feat: allow structure instances as fun binder without () 
The issue is that `{ x := ... }` was being parsed as an implicit
binder, and we were getting an error at `:=`.
 2020-08-30 07:35:41 -07:00
Leonardo de Moura
fc65b76331 feat: lift useful binder term syntax to tactics 2020-08-30 07:15:42 -07:00
Leonardo de Moura
a9e70a4d83 feat: intro similar to fun 2020-08-29 15:15:24 -07:00
Leonardo de Moura
af86cc801d feat: add change tactic parser 2020-08-29 08:10:55 -07:00
Leonardo de Moura
2287c7e7b3 feat: elaborate #print axioms command 2020-08-28 13:08:42 -07:00
Leonardo de Moura
cc1c9f3dfb feat: add #print axioms 2020-08-28 12:26:07 -07:00
Leonardo de Moura
76bda91ff8 feat: add evalMatch for tactics 2020-08-27 18:05:06 -07:00
Leonardo de Moura
d2f9f250db feat: add match tactic parser 2020-08-27 15:57:05 -07:00
Leonardo de Moura
546c108497 chore: revise letrec syntax 2020-08-26 10:50:32 -07:00
Leonardo de Moura
effaf64a07 feat: allow user to specify attributes letrec declarations 2020-08-26 09:57:46 -07:00
Leonardo de Moura
6a83577703 feat: letrec syntax 2020-08-26 09:33:52 -07:00
Leonardo de Moura
5ffbada3df feat: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions 
This is the first set of polymorphic methods. I will add more later,
and keep reducing code duplication.

cc @Kha
 2020-08-22 16:00:43 -07:00
Leonardo de Moura
916b395d1b chore: cleanup 2020-08-21 09:29:09 -07:00
Sebastian Ullrich
e5de32c2dd feat: auto-generate header formatter 2020-08-21 16:43:55 +02:00
Sebastian Ullrich
5f30d62d9b feat: [runParserAttributeHooks] 2020-08-21 16:38:41 +02:00
Sebastian Ullrich
14211cc932 refactor: more core 2020-08-21 15:51:37 +02:00
Leonardo de Moura
c55376a1ba chore: more conventional MonadIO 2020-08-20 11:13:10 -07:00
Sebastian Ullrich
aa452b795d refactor: make formatter precompiled as well 2020-08-20 15:29:33 +02:00
Leonardo de Moura
68a4c145f7 refactor: implement attribute hooks using CoreM 
We were using a mix of `IO` and `Except`
 2020-08-19 14:44:54 -07:00
Sebastian Ullrich
1840b4b1ff fix: pretty printer with new syntax 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
6cbfe2359b chore: remove old syntax 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
3091bd71e7 feat: unwrap basic token parsers 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
d4952dc40b feat: use insideQuot parsers 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
ed7edf5661 feat: add checkInsideQuot/checkOutsideQuot/toggleInsideQuot parsers 
One use case is to obtain fine-grained control over at what stage changed syntax is activated
 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
eeaf20080c refactor: register parenthesizer compiler as hook 
/cc @leodemoura
 2020-08-18 16:02:33 +02:00
Sebastian Ullrich
58e7af0d7f chore: simplify parser attribute hook registration 
It is unlikely to be needed outside the stdlib
 2020-08-18 15:52:23 +02:00
Sebastian Ullrich
dab53c4986 feat: add [parserAttributeHook] attribute 2020-08-18 14:41:36 +02:00
Leonardo de Moura
1ba3925740 feat: new let-expression syntax 
see 0064f7d2b9
 2020-08-17 07:51:08 -07:00
Sebastian Ullrich
92162ffb7f feat: check parenthesizer attribute arguments 2020-08-14 19:05:02 +02:00
Sebastian Ullrich
72310a4aee fix: parenthesizer: ParserDescr.parsers should not be assumed to be a registered parser, or even one with a kind 2020-08-14 19:05:02 +02:00
Sebastian Ullrich
129b60022d refactor: use distinct syntax kinds for quotations 2020-08-14 17:18:09 +02:00
Sebastian Ullrich
46f5670ba3 chore: Lean.Parser.Parser ~> Lean.Parser.Basic 2020-08-13 18:44:13 +02:00
Sebastian Ullrich
a0f825f67f refactor: move Lean.PrettyPrinter.Parenthesizer in between Lean.Parser.Parser and Lean.Parser.Extension 2020-08-13 18:44:13 +02:00
Sebastian Ullrich
f7e004b44a refactor: split Lean.Parser.Parser 2020-08-13 18:44:13 +02:00
Leonardo de Moura
0e0754346b chore: fix method name 2020-08-12 10:43:26 -07:00
Leonardo de Moura
31bbc6ee6d feat: add primitive for registering syntax node kinds that are not associated with any parser 
@Kha I added this feature to implement match expressions. The idea is
to be able to create a temporary `Syntax` node using an internal kind that has
no parser associated with it. That is, users cannot create them.
However, we can still associate an elaboration function to this kind.
Without this feature, I would have to create some "arbitrary parser"
for representing this temporary `Syntax` node.
 2020-08-12 10:21:37 -07:00
Sebastian Ullrich
f4e59070c4 feat: support interpreting parenthesizers from ParserDescr 2020-08-12 09:15:59 -07:00
Sebastian Ullrich
1f4cc130b7 feat: precompile parenthesizers instead of interpreting them 2020-08-12 09:15:59 -07:00
Sebastian Ullrich
05cb45ca9c refactor: simplify mkCategoryAntiquotParser 2020-08-12 09:15:59 -07:00
Leonardo de Moura
25fd5d0a9a fix: ambiguity at match 
```lean
match x : t with
| ...
```

Two possible intepretations for `x : t`:

1- The discriminant `t` where `x` is the name for the equality proofs `t = ...` in each alternative.

2- The discriminant `x` with a expected type `t` (aka motive) for the match.

This commit resolves the ambiguity by forcing no space before `:` in
the first interpretation.

cc @Kha
 2020-08-10 13:47:09 -07:00
Leonardo de Moura
f974521783 fix: missing node 2020-08-10 11:15:44 -07:00
Leonardo de Moura
3ce794c58a feat: allow h : annotation on match discriminants 2020-08-10 10:12:24 -07:00