Skip to content

Commit

Permalink
add pstate to tactic_error to fix issue 1144
Browse files Browse the repository at this point in the history
  • Loading branch information
Alidra committed Oct 22, 2024
1 parent d27c7d7 commit 11d6b5c
Showing 4 changed files with 28 additions and 14 deletions.
15 changes: 10 additions & 5 deletions src/handle/tactic.ml
Original file line number Diff line number Diff line change
@@ -391,6 +391,11 @@ let rec handle :
(** Representation of a tactic output. *)
type tac_output = proof_state * Query.result

exception Tactic_error of tac_output * Pos.popt option * string
let tactic_error : tac_output -> Pos.popt -> ('a,'b) Lplib.Base.koutfmt -> 'a = fun a pos fmt ->
let cont _ = raise (Tactic_error(a, Some(pos), Format.flush_str_formatter ())) in
Format.kfprintf cont Format.str_formatter fmt

(** [handle ss sym_pos prv ps tac] applies tactic [tac] in the proof state
[ps] and returns the new proof state. *)
let handle :
@@ -421,20 +426,20 @@ let handle :
let nb_newgoals = nb_goals_after - nb_goals_before in
if nb_newgoals <= 0 then
if nb_subproofs = 0 then a
else fatal t.pos "A subproof is given but there is no subgoal."
else tactic_error a t.pos "A subproof is given but there is no subgoal."
else if is_destructive t then
match nb_newgoals + 1 - nb_subproofs with
| 0 -> a
| n when n > 0 ->
fatal t.pos "Missing subproofs (%d subproofs for %d subgoals):@.%a"
tactic_error a t.pos "Missing subproofs (%d subproofs for %d subgoals):@.%a"
nb_subproofs (nb_newgoals + 1) goals ps'
| _ ->
fatal t.pos "Too many subproofs (%d subproofs for %d subgoals):@.%a"
tactic_error a t.pos "Too many subproofs (%d subproofs for %d subgoals):@.%a"
nb_subproofs (nb_newgoals + 1) goals ps'
else match nb_newgoals - nb_subproofs with
| 0 -> a
| n when n > 0 ->
fatal t.pos "Missing subproofs (%d subproofs for %d subgoals):@.%a"
tactic_error a t.pos "Missing subproofs (%d subproofs for %d subgoals):@.%a"
nb_subproofs nb_newgoals goals ps'
| _ -> fatal t.pos "Too many subproofs (%d subproofs for %d subgoals)."
| _ -> tactic_error a t.pos "Too many subproofs (%d subproofs for %d subgoals)."
nb_subproofs nb_newgoals
14 changes: 9 additions & 5 deletions src/lsp/lp_doc.ml
Original file line number Diff line number Diff line change
@@ -63,11 +63,15 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs =
let goals = Some (current_goals pstate) in
let qres = match qres with None -> "OK" | Some x -> x in
pstate, (tac_loc, 4, qres, goals) :: diags, logs
| Tac_Error(loc,msg) ->
let loc = option_default loc tac_loc in
pstate, (loc, 1, msg, None) :: diags, ((1, msg), loc) :: logs

let process_proof pstate tacs logs =
| Tac_Error(a, loc,msg) ->
match a with
| None -> let loc = option_default loc tac_loc in
pstate, (loc, 1, msg, None) :: diags, ((1, msg), loc) :: logs
| Some pstate ->
let goals = Some (current_goals pstate) in
pstate, (tac_loc, 4, "qres", goals) :: diags, logs

let process_proof pstate tacs logs =
Pure.ProofTree.fold process_pstep (pstate,[],logs) tacs

let get_goals dg_proof =
11 changes: 8 additions & 3 deletions src/pure/pure.ml
Original file line number Diff line number Diff line change
@@ -125,7 +125,7 @@ type command_result =

type tactic_result =
| Tac_OK of proof_state * string option
| Tac_Error of Pos.popt option * string
| Tac_Error of proof_state option * Pos.popt option * string

let t0 : Time.t Stdlib.ref = Stdlib.ref (Time.save ())

@@ -166,8 +166,13 @@ let handle_tactic : proof_state -> Tactic.t -> int -> tactic_result =
let ps, qres = Handle.Tactic.handle ss sym_pos prv (ps, None) tac n in
let qres = Option.map (fun f -> f ()) qres in
Tac_OK((Time.save (), ss, ps, finalize, prv, sym_pos), qres)
with Fatal(Some p,m) ->
Tac_Error(Some p, Pos.popt_to_string p ^ m)
with
| Fatal(Some p,m) ->
Tac_Error(None , Some p, Pos.popt_to_string p ^ m)
| Handle.Tactic.Tactic_error(a, Some p,m) ->
let ps, qres = a in
let _qres = Option.map (fun f -> f ()) qres in
Tac_Error(Some (Time.save (), ss, ps, finalize, prv, sym_pos), Some p, Pos.popt_to_string p ^ m)

let end_proof : proof_state -> command_result =
fun (_, ss, ps, finalize, _, _) ->
2 changes: 1 addition & 1 deletion src/pure/pure.mli
Original file line number Diff line number Diff line change
@@ -64,7 +64,7 @@ type command_result =
(** Result type of the [handle_tactic] function. *)
type tactic_result =
| Tac_OK of proof_state * string option
| Tac_Error of Pos.popt option * string
| Tac_Error of proof_state option * Pos.popt option * string

(** [initial_state fname] gives an initial state for working with the (source)
file [fname]. The resulting state can be used by [handle_command]. *)

0 comments on commit 11d6b5c

Please sign in to comment.