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

3509 commits

Author SHA1 Message Date
Leonardo de Moura
7a323a0c7b feat: allow parser! and tparser! to set the parser precedence 2020-06-03 18:11:13 -07:00
Sebastian Ullrich
e6d27c276b feat: #eval: capture stderr 2020-05-26 14:32:42 +02:00
Sebastian Ullrich
b35b973a5d fix: precedence of ! in old frontend 2020-05-26 11:26:57 +02:00
Leonardo de Moura
7c76a19885 chore: fix includes 2020-05-22 14:17:25 -07:00
Leonardo de Moura
c01da783ca fix: { ... : <expected-type> } syntax in the old frontend 2020-05-20 15:49:40 -07:00
Leonardo de Moura
22ae065d16 feat: add { ... : <expected-type> } syntax 
It replaces the `{ <struct-name> . ... }` syntax.
 2020-05-20 15:24:27 -07:00
Leonardo de Moura
3f44e8f3df chore: remove .. src syntax from old frontend 2020-05-20 13:07:21 -07:00
Leonardo de Moura
8bdca35282 chore: use #include <lean/runtime/...> for runtime .h files 2020-05-18 11:30:07 -07:00
Sebastian Ullrich
76a97ea4fc feat: infer module name from cwd instead of LEAN_PATH, also make build system less specific to Init/ 2020-05-14 14:38:52 +02:00
Leonardo de Moura
03403ba3c8 feat: make RelaxedImplicit the default behavior 2020-05-12 15:02:03 -07:00
Leonardo de Moura
e596820f2e chore: remove () modifier 
cc @Kha
 2020-05-12 15:02:02 -07:00
Sebastian Ullrich
ec9f4b579d chore: improve precision of compilation time profiling 2020-04-24 15:11:36 +02:00
Sebastian Ullrich
24f22f7643 chore: log cumulative #eval execution time 2020-04-24 15:11:36 +02:00
Sebastian Ullrich
8f67db0101 refactor: never implicitly ignore monadic results 
Also change `do e; f` to desugar to `e *> f` so that it is affected as well
 2020-04-23 11:09:59 -07:00
Leonardo de Moura
746615d81d chore: remove ⇒ as alternative for => 2020-04-06 13:45:22 -07:00
Sebastian Ullrich
b6fc9428f1 fix: support Windows newlines and '\r' escape 2020-03-27 13:21:21 -07:00
Leonardo de Moura
2efc1855f0 fix: object may be a boxed scalar 
Example: IOError.unexpectedEof
 2020-03-23 12:14:32 -07:00
Sebastian Ullrich
4cff135ec3 feat: #eval: auto-hide () output for m Unit chained instances 2020-03-19 17:18:15 -07:00
Leonardo de Moura
7a82318d37 fix: to_pattern_fn bug 2020-03-17 12:58:08 -07:00
Sebastian Ullrich
e3920552b0 fix: updating binding info of variables 2020-03-11 07:30:58 -07:00
Leonardo de Moura
6873400193 chore: remove silent | matchFailed support 
Before this commit
```lean
pattern <- action
```
was being translated by the old frontend into
```lean
pattern <- action | matchFailed
```
This produced counterintuitive behavior, and performance problems when
tryin to synthesize `MonadFail` instances.
BTW, the new frontend does not implement this feature. I didn't even
remember the old frontend did this.
I will also remove the class `MonadFail` from stdlib.

cc @Kha @dselsam
 2020-02-10 13:15:21 -08:00
Sebastian Ullrich
933ff6dc88 perf: short-circuit all antiquotation parsers 2020-02-06 08:12:08 -08:00
Leonardo de Moura
f0f522a6d6 chore: prepare to rename old coe primitives 2020-01-28 08:18:56 -08:00
Sebastian Ullrich
58313a050a Revert "fix: #eval redirection of stdout" 
This reverts commit 123577126c.
 2020-01-25 16:32:06 +01:00
Sebastian Ullrich
ad29568051 Revert "fix: redirect" 
This reverts commit addbb8dd67.
 2020-01-25 16:32:06 +01:00
Leonardo de Moura
addbb8dd67 fix: redirect 
@cipher1024 I modified your fix. It would produce memory leaks if the
code executed by #eval modifies the stdout.
Here is the problem.
- Your replaces the handler with some new handler `H` and stores the
  old handler `O` in a `flet`.
- Code is executed and replaces the stdout handler with `H'`. The `H`s RC is
  decremented and `H'`s RC is incremeneted. So far, so good.
- Now, the destructor of your `flet` is executed, and it replaces `H'`
  with `O`, but `H'` RC is not decremented.
 2020-01-23 15:58:34 -08:00
Simon Hudon
123577126c fix: #eval redirection of stdout 2020-01-23 15:44:49 -08:00
Leonardo de Moura
42642a2890 fix: new_frontend command issue 2020-01-15 20:53:23 -08:00
Simon Hudon
92c8773137 feat: file IO using handles 2020-01-12 08:02:48 -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
fe09e99fef chore: disable attribute features that are not currently being used 2020-01-08 15:49:55 -08:00
Leonardo de Moura
8e7c719ee8 chore: Pi => forall 2020-01-07 11:15:40 -08:00
Leonardo de Moura
091cc48901 feat: expose old pretty printer in Lean 2020-01-07 10:29:10 -08:00
Leonardo de Moura
477d53f2dd fix: position information 2020-01-06 21:07:41 -08:00
Leonardo de Moura
e0ae6068d4 chore: set end_pos 2020-01-06 21:00:52 -08:00
Leonardo de Moura
139d6c64e6 feat: add new_frontend command 
cc @kha
 2020-01-06 20:44:53 -08:00
Leonardo de Moura
c650e11d6b fix: missing isUnsafe fieldat OpaqueVal 2019-12-30 11:53:08 -08:00
Sebastian Ullrich
1f2040727c feat: autogenerate antiquotations in parser! 2019-12-30 08:24:29 -08:00
Sebastian Ullrich
88a924b728 feat: support (almost) proper name resolution in quotations in the old frontend 2019-12-18 20:11:45 -08:00
Sebastian Ullrich
6a2dbad53f feat: match_syntax support in the old parser 2019-12-17 12:16:34 -08:00
Sebastian Ullrich
2310ec2413 chore: separate C++ calls for parsing & expansion 2019-12-17 12:16:34 -08:00
Leonardo de Moura
8feb40e9f7 fix: add new approximation flag 
During TC, we don't want it. It allows us to find "solutions" that
trigger nontermination.
 2019-12-13 18:15:47 -08:00
Leonardo de Moura
820016e09a chore: remove dead code 2019-12-12 07:58:55 -08:00
Leonardo de Moura
820f57880f chore: compilation warning 2019-12-11 09:53:28 -08:00
Sebastian Ullrich
52c97e7bee feat: integrate quotation terms into old parser 2019-12-10 22:45:35 +01:00
Sebastian Ullrich
948b0bf1f1 fix: interpreter::call_boxed: support over-application 
MetaHasEval instances were not fully eta-expanded
 2019-12-05 13:21:08 +01:00
Sebastian Ullrich
fde58d8fe4 feat: add Lean.MetaHasEval, rename HasEval to Lean.HasEval 2019-12-05 13:20:24 +01:00
Leonardo de Moura
b6dde16be5 chore: remove #synth debugging command 2019-12-03 14:51:54 -08:00
Leonardo de Moura
3fb49fa765 chore: remove broken assertion 
@Kha I just commented it since we will soon delete this module.
 2019-11-21 16:15:57 -08:00
Sebastian Ullrich
f6973be5e3 refactor: replace C++ import parser with Lean one 
imports are now completely opaque to C++
 2019-11-21 15:52:01 +01:00