Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The Reprove top-level command #134

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 17 additions & 4 deletions src/abella.ml
Original file line number Diff line number Diff line change
Expand Up @@ -522,6 +522,9 @@ and proof_processor = {

let current_state = State.rref Process_top

(* Used to process the "Reprove" command; Quit just represents a null command *)
let last_top_command = State.rref (TopCommon Quit)

let print_clauses () =
List.iter print_clause !Prover.clauses

Expand Down Expand Up @@ -659,12 +662,21 @@ and process_proof1 name =

and process_top1 () =
fprintf !out "Abella < %!" ;
let input = Parser.top_command Lexer.token !lexbuf in
let input = ref (Parser.top_command Lexer.token !lexbuf) in
if not !interactive then begin
let pre, post = if !annotate then "<b>", "</b>" else "", "" in
fprintf !out "%s%s.%s\n%!" pre (top_command_to_string input) post
fprintf !out "%s%s.%s\n%!" pre (top_command_to_string !input) post
end ;
begin match input with
begin
if !input == Reprove then
match !last_top_command with
| Theorem(_, _, _) -> input := !last_top_command
| _ -> failwith "Reprove requires the last top-level command to be a theorem declaration"
(* Also keep the last command unchanged to enable multiple reproofs *)
else
last_top_command := !input
end ;
begin match !input with
| Theorem(name, tys, thm) ->
let st = get_bind_state () in
let seq = Prover.copy_sequent () in
Expand Down Expand Up @@ -694,7 +706,7 @@ and process_top1 () =
compile (CTheorem(n, tys, t))
end gen_thms ;
| Define _ ->
compile (Prover.register_definition input)
compile (Prover.register_definition !input)
| TopCommon(Back) ->
if !interactive then State.Undo.back 2
else failwith "Cannot use interactive commands in non-interactive mode"
Expand All @@ -707,6 +719,7 @@ and process_top1 () =
| Import(filename, withs) ->
compile (CImport (filename, withs)) ;
import (normalize_filename filename) withs;
| Reprove -> failwith "Assertion failure: Abella should not encounter the Reprove command here"
| Specification(filename) ->
if !can_read_specification then begin
read_specification (normalize_filename filename) ;
Expand Down
2 changes: 2 additions & 0 deletions src/abella_types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,7 @@ type top_command =
| Theorem of id * string list * umetaterm
| Define of flavor * tyctx * udef_clause list
| Import of string * (string * string) list
| Reprove
| Specification of string
| Query of umetaterm
| Kind of id list * knd
Expand Down Expand Up @@ -264,6 +265,7 @@ let top_command_to_string tc =
(withs |>
List.map (fun (a, b) -> a ^ " := " ^ b) |>
String.concat ", ")
| Reprove -> "Reprove"
| Specification filename ->
sprintf "Specification \"%s\"" filename
| Query q ->
Expand Down
1 change: 1 addition & 0 deletions src/lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
"Kind", KKIND ;
"Query", QUERY ;
"Quit", QUIT ;
"Reprove", REPROVE ;
"Set", SET ;
"Show", SHOW ;
"Specification", SPECIFICATION ;
Expand Down
5 changes: 4 additions & 1 deletion src/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@
%token IND INST APPLY CASE FROM SEARCH TO ON WITH INTROS CUT ASSERT CLAUSEEQ
%token SKIP UNDO ABORT COIND LEFT RIGHT MONOTONE IMPORT BY ASYNC
%token SPLIT SPLITSTAR UNFOLD ALL KEEP CLEAR SPECIFICATION SEMICOLON
%token THEOREM DEFINE PLUS CODEFINE SET ABBREV UNABBREV QUERY SHOW
%token THEOREM DEFINE PLUS CODEFINE SET ABBREV UNABBREV QUERY REPROVE SHOW
%token PERMUTE BACKCHAIN QUIT UNDERSCORE AS SSPLIT RENAME
%token BACK RESET
%token COLON RARROW FORALL NABLA EXISTS WITNESS STAR AT HASH OR AND
Expand Down Expand Up @@ -198,6 +198,7 @@ id:
| QUERY { "Query" }
| QUIT { "Quit" }
| RENAME { "rename" }
| REPROVE { "Reprove" }
| RIGHT { "right" }
| SEARCH { "search" }
| SET { "Set" }
Expand Down Expand Up @@ -731,6 +732,8 @@ pure_top_command:
{ Types.Import($2, []) }
| IMPORT QSTRING WITH import_withs DOT
{ Types.Import($2, $4) }
| REPROVE DOT
{ Types.Reprove }
| SPECIFICATION QSTRING DOT
{ Types.Specification($2) }
| KKIND id_list knd DOT
Expand Down