max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/frontends/lean
History
Leonardo de Moura 7cdf917c97 fix: compiler do a; b as a >>= fun _ => b 
Consider the following example
```lean
def div!: Nat → Nat → Nat
| x, 0 => panic! "division by zero"
| x, y => x/y

def weird (x : Nat) : MetaM Nat :=
unless (x > 0) (throwOther "x == 0") *>
let y := div! 10 x;
pure y
```
If we execute `weird 0`, it produces a "division by zero" panic
message.
This is a simple version of a much bigger function in the new
frontend.
This is not due to a bug in the compiler.
It produces the panic message because of the `do`-encoding
refactoring. Recall that, a few months ago,
we started to compile `do a; b` as `a *> b` (i.e., `seqRight a b`).
Thus, the example above is
`seqRight action1 (let y := div! 10 x; pure y)`
where `action1` is the `unless ...`.
In A-normal form, this is equivalent to

```lean
let y:= div! 10 x;
let action2 := pure y;
seqRight action1 action2
```
Thus, we execute `div! 10 x` before we even execute the `seqRight`.
This is counterintuitive and demonstrates once again how impure
features such as `panic!` are dangerous.

This commit reverts the `do`-encoding refactoring, and encodes
`do a; b` as `a >>= fun _ b` as we did in Lean3.

cc @Kha
2020-08-15 15:51:00 -07:00
..
brackets.cpp fix: { ... : <expected-type> } syntax in the old frontend 2020-05-20 15:49:40 -07:00
brackets.h
builtin_cmds.cpp feat: allow #eval to update Environment 2020-07-30 16:48:31 -07:00
builtin_cmds.h
builtin_exprs.cpp fix: compiler do a; b as a >>= fun _ => b 2020-08-15 15:51:00 -07:00
builtin_exprs.h chore(frontends/lean): remove tactic notation 2018-08-23 13:44:52 -07:00
choice.cpp chore(frontends/lean/choice): cleanup 2018-06-18 15:29:21 -07:00
choice.h refactor(frontends/lean/choice): use mdata to implement choice 2018-06-18 14:21:11 -07:00
CMakeLists.txt chore: remove dead code 2019-11-14 15:24:18 -08:00
cmd_table.h chore(frontends/lean): fix clang++ warnings at C++ 2019-01-30 15:19:34 -08:00
decl_attributes.cpp chore: disable attribute features that are not currently being used 2020-01-08 15:49:55 -08:00
decl_attributes.h feat: allow attributes to be applied before elaboration 2019-11-13 15:40:19 -08:00
decl_cmds.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
decl_cmds.h feat(frontends/lean, library/init/lean): opaque constants 2019-03-15 17:41:44 -07:00
decl_util.cpp refactor: remove Expr.FVar hack 2019-11-15 14:04:26 -08:00
decl_util.h feat(frontends/lean): add simple parser! macro 2019-06-24 15:48:11 -07:00
definition_cmds.cpp chore: remove comment from Linter 2020-06-17 21:28:03 -07:00
definition_cmds.h feat(library/init/lean/elaborator,frontends/lean/vm_elaborator): implement def/theorem/abbreviation 2019-01-12 15:10:00 +01:00
elaborator.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
elaborator.h chore: remove silent | matchFailed support 2020-02-10 13:15:21 -08:00
inductive_cmds.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
inductive_cmds.h fix(frontends/lean/inductive_cmds): set m_explicit_levels, and call collect_implicit_locals only after that 2019-01-15 16:47:28 +01:00
init_module.cpp chore(frontends/lean): delete lean_environment 2019-05-13 13:05:04 -07:00
init_module.h
json.cpp refactor(library/messages): make an object_ref 2018-09-11 13:55:25 -07:00
json.h refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
local_context_adapter.cpp refactor: remove Expr.FVar hack 2019-11-15 14:04:26 -08:00
local_context_adapter.h
local_decls.h chore: fix C++ warnings 2020-08-14 14:42:44 +02:00
local_level_decls.h chore: fix C++ warnings 2020-08-14 14:42:44 +02:00
match_expr.cpp feat(library/init): use new "empty match" syntax 2019-07-15 16:25:14 -07:00
match_expr.h feat(frontends/lean): add new "empty/no match" syntax to old parser 2019-07-15 16:18:44 -07:00
notation_cmd.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
notation_cmd.h chore(frontends/lean): fix clang++ warnings at C++ 2019-01-30 15:19:34 -08:00
parse_table.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
parse_table.h chore(frontends/lean): fix clang++ warnings at C++ 2019-01-30 15:19:34 -08:00
parser.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
parser.h chore: fix includes 2020-05-22 14:17:25 -07:00
parser_config.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
parser_config.h chore: fix includes 2020-05-22 14:17:25 -07:00
parser_pos_provider.h refactor(kernel): remove tag from kernel expressions 2018-06-08 10:29:22 -07:00
parser_state.h chore(frontends/lean): remove break_at_pos support 2018-09-07 08:34:19 -07:00
pp.cpp chore: hack metavariable case 2020-08-04 16:42:48 -07:00
pp.h chore: fix includes 2020-05-22 14:17:25 -07:00
prenum.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
prenum.h chore: fix includes 2020-05-22 14:17:25 -07:00
print_cmd.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
print_cmd.h chore(frontends/lean): fix clang++ warnings at C++ 2019-01-30 15:19:34 -08:00
scanner.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
scanner.h chore: fix includes 2020-05-22 14:17:25 -07:00
simple_pos_info_provider.h feat(frontends/lean/vm_elaborator): recover from unknown identifiers 2019-02-07 14:16:28 +01:00
structure_cmd.cpp chore: remove dead code 2020-07-24 09:52:35 -07:00
structure_cmd.h feat(frontends/lean/structure_cmd): implement structure 2019-01-15 15:01:52 +01:00
structure_instance.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
structure_instance.h feat(frontends/lean/{parser,elaborator}): structure instance patterns 2017-11-22 12:16:28 -08:00
token_table.cpp feat: adjust fun/do precedence in old frontend 2020-06-16 10:41:42 -07:00
token_table.h
tokens.cpp chore(frontends/lean): fun x, e ==> fun x => e 2019-07-02 13:22:11 -07:00
tokens.h chore(frontends/lean): fun x, e ==> fun x => e 2019-07-02 13:22:11 -07:00
tokens.txt chore(frontends/lean): fun x, e ==> fun x => e 2019-07-02 13:22:11 -07:00
type_util.cpp feat: make RelaxedImplicit the default behavior 2020-05-12 15:02:03 -07:00
type_util.h chore(frontends/lean): fix clang++ warnings at C++ 2019-01-30 15:19:34 -08:00
typed_expr.cpp refactor(library/typed_expr): move typed_expr to frontends/lean 2018-04-09 15:25:40 -07:00
typed_expr.h refactor(library/typed_expr): move typed_expr to frontends/lean 2018-04-09 15:25:40 -07:00
util.cpp chore: fix includes 2020-05-22 14:17:25 -07:00
util.h refactor(util/sexpr/options): options as a Lean object 2019-05-16 14:27:44 -07:00