michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/parser): display failed state in noninteractive mode, stop processing tactic commands when a Lean command is found

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-06 05:13:29 -08:00
parent c841763a05
commit d46cf5fdd5
5 changed files with 107 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/parser.cpp
View file

@ -380,8 +380,7 @@ class parser::imp {
void display_error(tactic_cmd_error const & ex) {
display_error(ex.what(), ex.m_pos.first, ex.m_pos.second);
if (m_interactive)
display_proof_state(ex.m_state);
display_proof_state(ex.m_state);
}
/**
@ -1395,6 +1394,9 @@ class parser::imp {
throw tactic_cmd_error(sstream() << "invalid tactic command '" << id << "'", p, s);
}
break;
case scanner::token::CommandId:
st = status::Abort;
break;
default:
next();
throw tactic_cmd_error("invalid tactic command, identifier expected", p, s);

15
tests/lean/interactive/t10.lean Normal file
View file

@ -0,0 +1,15 @@
(**
simple_tac = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
**)
Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
Discharge (fun H : A /\ B,
let H1 : A := _,
H2 : B := _,
main : B /\ A := _
in main).
apply simple_tac. done.
apply simple2_tac. done.
apply simple_tac. done.
Echo "echo command after failure"

21
tests/lean/interactive/t10.lean.expected.out Normal file
View file

@ -0,0 +1,21 @@
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
# Set: pp::colors
Set: pp::unicode
Proof state:
A : Bool, B : Bool, H : A ∧ B ⊢ A
## Proof state:
no goals
## Proof state:
A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
## Error (line: 15, pos: 3) unknown tactic 'simple2_tac'
Proof state:
A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
## Error (line: 15, pos: 22) invalid 'done' command, proof cannot be produced from this state
Proof state:
A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
## Proof state:
no goals
## Proof state:
A : Bool, B : Bool, H : A ∧ B, H1 : A, H2 : B ⊢ B ∧ A
## Error (line: 18, pos: 0) failed to prove theorem, proof has been aborted
# echo command after failure

30
tests/lean/interactive/t9.lean Normal file
View file

@ -0,0 +1,30 @@
Theorem T1 (A B : Bool) : A /\ B => B /\ A :=
Discharge (fun H : A /\ B,
let main : B /\ A :=
(let H1 : B := _,
H2 : A := _
in _)
in main).
apply conj_hyp_tac.
assumption.
done.
apply conj_hyp_tac.
assumption.
done.
apply Conj.
assumption.
done.
(**
simple_tac = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
**)
Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
Discharge (fun H : A /\ B,
let H1 : A := _,
H2 : B := _,
main : B /\ A := _
in main).
apply simple_tac. done.
apply simple_tac. done.
apply simple_tac. done.

37
tests/lean/interactive/t9.lean.expected.out Normal file
View file

@ -0,0 +1,37 @@
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
# Set: pp::colors
Set: pp::unicode
Proof state:
A : Bool, B : Bool, H : A ∧ B ⊢ B
## Proof state:
A : Bool, B : Bool, H::1 : A, H::2 : B ⊢ B
## Proof state:
no goals
## Proof state:
A : Bool, B : Bool, H : A ∧ B, H1 : B ⊢ A
## Proof state:
A : Bool, B : Bool, H::1 : A, H::2 : B, H1 : B ⊢ A
## Proof state:
no goals
## Proof state:
A : Bool, B : Bool, H : A ∧ B, H1 : B, H2 : A ⊢ B ∧ A
## Proof state:
A : Bool, B : Bool, H : A ∧ B, H1 : B, H2 : A ⊢ B
A : Bool, B : Bool, H : A ∧ B, H1 : B, H2 : A ⊢ A
## Proof state:
no goals
## Proved: T1
# Proof state:
A : Bool, B : Bool, H : A ∧ B ⊢ A
## Proof state:
no goals
## Proof state:
A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
## Proof state:
no goals
## Proof state:
A : Bool, B : Bool, H : A ∧ B, H1 : A, H2 : B ⊢ B ∧ A
## Proof state:
no goals
## Proved: T2
#