summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml4
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/goal.ml6
-rw-r--r--proofs/goal.mli4
-rw-r--r--proofs/logic.ml8
-rw-r--r--proofs/pfedit.ml14
-rw-r--r--proofs/pfedit.mli22
-rw-r--r--proofs/proof.ml134
-rw-r--r--proofs/proof.mli14
-rw-r--r--proofs/proof_global.ml72
-rw-r--r--proofs/proof_global.mli6
-rw-r--r--proofs/proofview.ml11
-rw-r--r--proofs/proofview.mli5
-rw-r--r--proofs/refiner.ml4
-rw-r--r--proofs/refiner.mli1
-rw-r--r--proofs/tacexpr.ml11
-rw-r--r--proofs/tacmach.ml8
-rw-r--r--proofs/tacmach.mli3
-rw-r--r--proofs/tactic_debug.ml103
-rw-r--r--proofs/tactic_debug.mli7
20 files changed, 229 insertions, 210 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index d06c6f2e..b98101e0 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -500,8 +500,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
let clause = mk_clenv_from_env env sigma n (c,t) in
clenv_constrain_dep_args hyps_only largs clause
| ExplicitBindings lbind ->
- let clause = mk_clenv_from_env env sigma n
- (c,rename_bound_vars_as_displayed [] t)
+ let clause = mk_clenv_from_env env sigma n
+ (c,rename_bound_vars_as_displayed [] [] t)
in clenv_match_args lbind clause
| NoBindings ->
mk_clenv_from_env env sigma n (c,t)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 36268de1..6fa95dc8 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -40,7 +40,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
error "Instantiate called on already-defined evar";
let env = Evd.evar_env evi in
let sigma',typed_c =
- try Pretyping.Default.understand_ltac true sigma env ltac_var
+ try Pretyping.Default.understand_ltac ~resolve_classes:true true sigma env ltac_var
(Pretyping.OfType (Some evi.evar_concl)) rawc
with _ ->
let loc = Glob_term.loc_of_glob_constr rawc in
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 1542267e..eeaba76e 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -163,8 +163,8 @@ module Refinable = struct
(* spiwack: it is not very fine grain since it solves all typeclasses holes,
not only those containing the current goal, or a given term. But it
seems to fit our needs so far. *)
- let resolve_typeclasses ?onlyargs ?split ?(fail=false) () env rdefs _ _ =
- rdefs:=Typeclasses.resolve_typeclasses ?onlyargs ?split ~fail env !rdefs;
+ let resolve_typeclasses ?filter ?split ?(fail=false) () env rdefs _ _ =
+ rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs;
()
@@ -563,7 +563,7 @@ module V82 = struct
let new_sigma = Evd.add Evd.empty evk new_evi in
{ Evd.it = build evk ; sigma = new_sigma }
- (* Used by the typeclasses *)
+ (* Used by the compatibility layer and typeclasses *)
let nf_evar sigma gl =
let evi = content sigma gl in
let evi = Evarutil.nf_evar_info sigma evi in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index e9d23065..50709555 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -72,7 +72,7 @@ module Refinable : sig
(* [with_type c typ] constrains term [c] to have type [typ]. *)
val with_type : Term.constr -> Term.types -> Term.constr sensitive
- val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
+ val resolve_typeclasses : ?filter:(Evd.hole_kind -> bool) -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
(* [constr_of_raw h check_type resolve_classes] is a pretyping function.
@@ -234,7 +234,7 @@ module V82 : sig
(* Used for congruence closure *)
val new_goal_with : Evd.evar_map -> goal -> Environ.named_context_val -> goal Evd.sigma
- (* Used by the typeclasses *)
+ (* Used by the compatibility layer and typeclasses *)
val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
(* Goal represented as a type, doesn't take into account section variables *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a363c6bb..5babd03a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -685,12 +685,8 @@ let prim_refiner r sigma goal =
([gl], sigma)
| Change_evars ->
- (* spiwack: a priori [Change_evars] is now devoid of operational content.
- The new proof engine keeping the evar_map up to date at all time.
- As a compatibility mesure I leave the rule.
- It is possible that my assumption is wrong and some uses of
- [Change_evars] are not subsumed by the new engine. In which
- case something has to be done here. (Feb. 2010) *)
+ (* Normalises evars in goals. Used by instantiate. *)
+ let (goal,sigma) = Goal.V82.nf_evar sigma goal in
([goal],sigma)
(************************************************************************)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 3d507f35..6ac0b553 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -35,8 +35,10 @@ let delete_proof = Proof_global.discard
let delete_current_proof = Proof_global.discard_current
let delete_all_proofs = Proof_global.discard_all
-let undo n =
+let undo n =
let p = Proof_global.give_me_the_proof () in
+ let d = Proof.V82.depth p in
+ if n >= d then raise Proof.EmptyUndoStack;
for i = 1 to n do
Proof.undo p
done
@@ -64,15 +66,7 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook =
Proof_global.start_proof id str goals ?compute_guard hook;
Option.iter Proof_global.run_tactic init_tac
-let restart_proof () =
- let p = Proof_global.give_me_the_proof () in
- try while true do
- Proof.undo p
- done with Proof.EmptyUndoStack -> ()
-
-let resume_last_proof () = Proof_global.resume_last ()
-let resume_proof (_,id) = Proof_global.resume id
-let suspend_proof () = Proof_global.suspend ()
+let restart_proof () = undo_todepth 1
let cook_proof hook =
let prf = Proof_global.give_me_the_proof () in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7297b975..5d45ea7c 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -85,24 +85,6 @@ val start_proof :
val restart_proof : unit -> unit
(** {6 ... } *)
-(** [resume_last_proof ()] focus on the last unfocused proof or fails
- if there is no suspended proofs *)
-
-val resume_last_proof : unit -> unit
-
-(** [resume_proof name] focuses on the proof of name [name] or
- raises [NoSuchProof] if no proof has name [name].
-
- It doesn't [suspend_proof ()] before. *)
-
-val resume_proof : identifier located -> unit
-
-(** [suspend_proof ()] unfocuses the current focused proof or
- failed with [UserError] if no proof is currently focused *)
-
-val suspend_proof : unit -> unit
-
-(** {6 ... } *)
(** [cook_proof opacity] turns the current proof (assumed completed) into
a constant with its name, kind and possible hook (see [start_proof]);
it fails if there is no current proof of if it is not completed;
@@ -143,7 +125,9 @@ val current_proof_statement :
val get_current_proof_name : unit -> identifier
-(** [get_all_proof_names ()] returns the list of all pending proof names *)
+(** [get_all_proof_names ()] returns the list of all pending proof names.
+ The first name is the current proof, the other names may come in
+ any order. *)
val get_all_proof_names : unit -> identifier list
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 72730495..996a895f 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -35,12 +35,12 @@ type _focus_kind = int
type 'a focus_kind = _focus_kind
type focus_info = Obj.t
type unfocusable =
- | Cannot
+ | Cannot of exn
| Loose
| Strict
type _focus_condition =
(_focus_kind -> Proofview.proofview -> unfocusable) *
- (_focus_kind -> focus_info -> focus_info)
+ (_focus_kind -> bool)
type 'a focus_condition = _focus_condition
let next_kind = ref 0
@@ -49,13 +49,8 @@ let new_focus_kind () =
incr next_kind;
r
-(* Auxiliary function to define conditions:
- [check kind1 kind2 inf] returns [inf] if [kind1] and [kind2] match.
- Otherwise it raises [CheckNext] *)
-exception CheckNext
-(* no handler: confined to this module. *)
-let check kind1 kind2 inf =
- if kind1=kind2 then inf else raise CheckNext
+(* Auxiliary function to define conditions. *)
+let check kind1 kind2 = kind1=kind2
(* To be authorized to unfocus one must meet the condition prescribed by
the action which focused.*)
@@ -68,40 +63,55 @@ module Cond = struct
(* first attempt at an algebra of condition *)
(* semantics:
- [Cannot] means that the condition is not met
- - [Strict] that the condition is meant
- - [Loose] that the condition is not quite meant
+ - [Strict] that the condition is met
+ - [Loose] that the condition is not quite met
but authorises to unfocus provided a condition
of a previous focus on the stack is (strictly)
- met.
+ met. [Loose] focuses are those, like bullets,
+ which do not have a closing command and
+ are hence closed by unfocusing actions unrelated
+ to their focus_kind.
*)
- let bool b =
+ let bool e b =
if b then fun _ _ -> Strict
- else fun _ _ -> Cannot
+ else fun _ _ -> Cannot e
let loose c k p = match c k p with
- | Cannot -> Loose
+ | Cannot _ -> Loose
| c -> c
let cloose l c =
if l then loose c
else c
let (&&&) c1 c2 k p=
match c1 k p , c2 k p with
- | Cannot , _
- | _ , Cannot -> Cannot
+ | Cannot e , _
+ | _ , Cannot e -> Cannot e
| Strict, Strict -> Strict
| _ , _ -> Loose
- let kind k0 k p = bool (k0=k) k p
- let pdone k p = bool (Proofview.finished p) k p
+ let kind e k0 k p = bool e (k0=k) k p
+ let pdone e k p = bool e (Proofview.finished p) k p
+end
+
+
+(* Unfocus command.
+ Fails if the proof is not focused. *)
+exception CannotUnfocusThisWay
+let _ = Errors.register_handler begin function
+ | CannotUnfocusThisWay ->
+ Util.error "This proof is focused, but cannot be unfocused this way"
+ | _ -> raise Errors.Unhandled
end
open Cond
-let no_cond ~loose_end k0 =
- cloose loose_end (kind k0)
-let no_cond ?(loose_end=false) k = no_cond ~loose_end k , check k
+let no_cond_gen e ~loose_end k0 =
+ cloose loose_end (kind e k0)
+let no_cond_gen e ?(loose_end=false) k = no_cond_gen e ~loose_end k , check k
+let no_cond ?loose_end = no_cond_gen CannotUnfocusThisWay ?loose_end
(* [done_cond] checks that the unfocusing command uses the right [focus_kind]
and that the focused proofview is complete. *)
-let done_cond ~loose_end k0 =
- (cloose loose_end (kind k0)) &&& pdone
-let done_cond ?(loose_end=false) k = done_cond ~loose_end k , check k
+let done_cond_gen e ~loose_end k0 =
+ (cloose loose_end (kind e k0)) &&& pdone e
+let done_cond_gen e ?(loose_end=false) k = done_cond_gen e ~loose_end k , check k
+let done_cond ?loose_end = done_cond_gen CannotUnfocusThisWay ?loose_end
(* Subpart of the type of proofs. It contains the parts of the proof which
@@ -249,13 +259,13 @@ let save pr =
push_undo (save_state pr) pr
(* This function restores a state, presumably from the top of the undo stack. *)
-let restore_state save pr =
+let restore_state save pr =
match save with
| State save -> pr.state <- save
| Effect undo -> undo ()
(* Interpretes the Undo command. *)
-let undo pr =
+let undo pr =
(* On a single line, since the effects commute *)
restore_state (pop_undo pr) pr
@@ -309,20 +319,11 @@ let focus cond inf i pr =
save pr;
_focus cond (Obj.repr inf) i i pr
-(* Unfocus command.
- Fails if the proof is not focused. *)
-exception CannotUnfocusThisWay
-let _ = Errors.register_handler begin function
- | CannotUnfocusThisWay ->
- Util.error "This proof is focused, but cannot be unfocused this way"
- | _ -> raise Errors.Unhandled
-end
-
let rec unfocus kind pr () =
let starting_point = save_state pr in
let cond = cond_of_focus pr in
match fst cond kind pr.state.proofview with
- | Cannot -> raise CannotUnfocusThisWay
+ | Cannot e -> raise e
| Strict ->
(_unfocus pr;
push_undo starting_point pr)
@@ -336,34 +337,35 @@ let rec unfocus kind pr () =
let unfocus kind pr =
transaction pr (unfocus kind pr)
-
-let get_at_point kind ((_,get),inf,_) = get kind inf
+
exception NoSuchFocus
(* no handler: should not be allowed to reach toplevel. *)
-exception GetDone of Obj.t
-(* no handler: confined to this module. *)
-let get_in_focus_stack kind stack =
- try
- List.iter begin fun pt ->
- try
- raise (GetDone (get_at_point kind pt))
- with CheckNext -> ()
- end stack;
- raise NoSuchFocus
- with GetDone x -> x
+let rec get_in_focus_stack kind stack =
+ match stack with
+ | ((_,check),inf,_)::stack ->
+ if check kind then inf
+ else get_in_focus_stack kind stack
+ | [] -> raise NoSuchFocus
let get_at_focus kind pr =
Obj.magic (get_in_focus_stack kind pr.state.focus_stack)
+let is_last_focus kind pr =
+ let ((_,check),_,_) = List.hd pr.state.focus_stack in
+ check kind
+
let no_focused_goal p =
Proofview.finished p.state.proofview
(*** Proof Creation/Termination ***)
+(* [end_of_stack] is unfocused by return to close every loose focus. *)
let end_of_stack_kind = new_focus_kind ()
-let end_of_stack = done_cond end_of_stack_kind
+let end_of_stack = done_cond_gen FullyUnfocused end_of_stack_kind
+
+let unfocused = is_last_focus end_of_stack_kind
let start goals =
- let pr =
+ let pr =
{ state = { proofview = Proofview.init goals ;
focus_stack = [] ;
intel = Store.empty} ;
@@ -445,14 +447,22 @@ module V82 = struct
let top_evars p =
Proofview.V82.top_evars p.state.proofview
- let instantiate_evar n com pr =
- let starting_point = save_state pr in
- let sp = pr.state.proofview in
- try
- let new_proofview = Proofview.V82.instantiate_evar n com sp in
- pr.state <- { pr.state with proofview = new_proofview };
- push_undo starting_point pr
- with e ->
- restore_state starting_point pr;
- raise e
+ let grab_evars p =
+ if not (is_done p) then
+ raise UnfinishedProof
+ else
+ save p;
+ p.state <- { p.state with proofview = Proofview.V82.grab p.state.proofview }
+
+
+ let instantiate_evar n com pr =
+ let starting_point = save_state pr in
+ let sp = pr.state.proofview in
+ try
+ let new_proofview = Proofview.V82.instantiate_evar n com sp in
+ pr.state <- { pr.state with proofview = new_proofview };
+ push_undo starting_point pr
+ with e ->
+ restore_state starting_point pr;
+ raise e
end
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 12af18f4..715b3341 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -114,12 +114,18 @@ exception CannotUnfocusThisWay
is not met. *)
val unfocus : 'a focus_kind -> proof -> unit
+(* [unfocused p] returns [true] when [p] is fully unfocused. *)
+val unfocused : proof -> bool
+
(* [get_at_focus k] gets the information stored at the closest focus point
of kind [k].
Raises [NoSuchFocus] if there is no focus point of kind [k]. *)
exception NoSuchFocus
val get_at_focus : 'a focus_kind -> proof -> 'a
+(* [is_last_focus k] check if the most recent focus is of kind [k] *)
+val is_last_focus : 'a focus_kind -> proof -> bool
+
(* returns [true] if there is no goal under focus. *)
val no_focused_goal : proof -> bool
@@ -127,8 +133,6 @@ val no_focused_goal : proof -> bool
val get_proof_info : proof -> Store.t
-val set_proof_info : Store.t -> proof -> unit
-
(* Sets the section variables assumed by the proof *)
val set_used_variables : Sign.section_context -> proof -> unit
val get_used_variables : proof -> Sign.section_context option
@@ -151,7 +155,7 @@ val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> unit
a focusing command and a tactic. Transactions are such that if
any of the atomic action fails, the whole transaction fails.
- During a transaction, the undo visible undo stack is constituted only
+ During a transaction, the visible undo stack is constituted only
of the actions performed done during the transaction.
[transaction p f] can be called on an [f] using, itself, [transaction p].*)
@@ -178,6 +182,10 @@ module V82 : sig
(* returns the existential variable used to start the proof *)
val top_evars : proof -> Evd.evar list
+ (* Turns the unresolved evars into goals.
+ Raises [UnfinishedProof] if there are still unsolved goals. *)
+ val grab_evars : proof -> unit
+
(* Implements the Existential command *)
val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit
end
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2745270a..ae0f7d12 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -70,12 +70,10 @@ type proof_info = {
mode : proof_mode
}
-(* Invariant: a proof is at most in one of current_proof and suspended. And the
- domain of proof_info is the union of that of current_proof and suspended.*)
-(* The head of [!current_proof] is the actual current proof, the other ones are to
- be resumed when the current proof is closed, aborted or suspended. *)
+(* Invariant: the domain of proof_info is current_proof.*)
+(* The head of [!current_proof] is the actual current proof, the other ones are
+ to be resumed when the current proof is closed or aborted. *)
let current_proof = ref ([]:nproof list)
-let suspended = ref ([] : nproof list)
let proof_info = ref (Idmap.empty : proof_info Idmap.t)
(* Current proof_mode, for bookkeeping *)
@@ -93,7 +91,7 @@ let update_proof_mode () =
!current_proof_mode.reset ();
current_proof_mode := standard
-(* combinators for the current_proof and suspended lists *)
+(* combinators for the current_proof lists *)
let push a l = l := a::!l;
update_proof_mode ()
@@ -145,8 +143,7 @@ let remove id m =
(*** Proof Global manipulation ***)
let get_all_proof_names () =
- List.map fst !current_proof @
- List.map fst !suspended
+ List.map fst !current_proof
let give_me_the_proof () =
snd (find_top current_proof)
@@ -160,61 +157,40 @@ let get_current_proof_name () =
accessed directly through vernacular commands. Error message should be
pushed to external layers, and so we should be able to have a finer
control on error message on complex actions. *)
-let msg_proofs use_resume =
+let msg_proofs () =
match get_all_proof_names () with
| [] -> (spc () ++ str"(No proof-editing in progress).")
| l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
- (Util.prlist_with_sep Util.pr_spc Nameops.pr_id l) ++
- str"." ++
- (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
- else (mt ()))
- )
-
+ (Util.prlist_with_sep Util.pr_spc Nameops.pr_id l)++ str ".")
let there_is_a_proof () = !current_proof <> []
-let there_are_suspended_proofs () = !suspended <> []
-let there_are_pending_proofs () =
- there_is_a_proof () ||
- there_are_suspended_proofs ()
-let check_no_pending_proof () =
+let there_are_pending_proofs () = there_is_a_proof ()
+let check_no_pending_proof () =
if not (there_are_pending_proofs ()) then
()
else begin
Util.error (Pp.string_of_ppcmds
- (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
+ (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
str"Use \"Abort All\" first or complete proof(s)."))
end
-
-let suspend () =
- rotate_top current_proof suspended
-
-let resume_last () =
- rotate_top suspended current_proof
-
-let resume id =
- rotate_find id suspended current_proof
-
let discard_gen id =
- try
- ignore (extract id current_proof);
- remove id proof_info
- with NoSuchProof -> ignore (extract id suspended)
+ ignore (extract id current_proof);
+ remove id proof_info
let discard (loc,id) =
try
discard_gen id
with NoSuchProof ->
Util.user_err_loc
- (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
+ (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
let discard_current () =
let (id,_) = extract_top current_proof in
remove id proof_info
let discard_all () =
- current_proof := [];
- suspended := [];
+ current_proof := [];
proof_info := Idmap.empty
(* [set_proof_mode] sets the proof mode to be used after it's called. It is
@@ -239,6 +215,11 @@ let set_proof_mode mn =
end pr ;
set_proof_mode m id
+exception AlreadyExists
+let _ = Errors.register_handler begin function
+ | AlreadyExists -> Util.error "Already editing something of that name."
+ | _ -> raise Errors.Unhandled
+end
(* [start_proof s str env t hook tac] starts a proof of name [s] and
conclusion [t]; [hook] is optionally a function to be applied at
proof end (e.g. to declare the built constructions as a coercion
@@ -248,7 +229,11 @@ let set_proof_mode mn =
It raises exception [ProofInProgress] if there is a proof being
currently edited. *)
let start_proof id str goals ?(compute_guard=[]) hook =
- (* arnaud: ajouter une vérification pour la présence de id dans le proof_global *)
+ begin
+ List.iter begin fun (id_ex,_) ->
+ if Names.id_ord id id_ex = 0 then raise AlreadyExists
+ end !current_proof
+ end;
let p = Proof.start goals in
add id { strength=str ;
compute_guard=compute_guard ;
@@ -354,9 +339,14 @@ module Bullet = struct
let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind)
let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind
+ (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command
+ experience will tell if this is the right discipline of if we want to be finer and
+ reset them only for a choice of bullets. *)
let get_bullets pr =
- try Proof.get_at_focus bullet_kind pr
- with Proof.NoSuchFocus -> []
+ if Proof.is_last_focus bullet_kind pr then
+ Proof.get_at_focus bullet_kind pr
+ else
+ []
let has_bullet bul pr =
let rec has_bullet = function
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index ed6a60c7..e266d57c 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -69,12 +69,6 @@ val close_proof : unit ->
exception NoSuchProof
-val suspend : unit -> unit
-val resume_last : unit -> unit
-
-val resume : Names.identifier -> unit
-(** @raise NoSuchProof if it doesn't find one. *)
-
(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
no current proof. *)
val run_tactic : unit Proofview.tactic -> unit
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 0d50d521..4246cc9c 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -475,6 +475,17 @@ module V82 = struct
let has_unresolved_evar pv =
Evd.has_undefined pv.solution
+ (* Main function in the implementation of Grab Existential Variables.*)
+ let grab pv =
+ let goals =
+ List.map begin fun (e,_) ->
+ Goal.build e
+ end (Evd.undefined_list pv.solution)
+ in
+ { pv with comb = goals }
+
+
+
(* Returns the open goals of the proofview together with the evar_map to
interprete them. *)
let goals { comb = comb ; solution = solution } =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 24da9d77..fe24b54b 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -195,6 +195,11 @@ module V82 : sig
val has_unresolved_evar : proofview -> bool
+ (* Main function in the implementation of Grab Existential Variables.
+ Resets the proofview's goals so that it contains all unresolved evars
+ (in chronological order of insertion). *)
+ val grab : proofview -> proofview
+
(* Returns the open goals of the proofview together with the evar_map to
interprete them. *)
val goals : proofview -> Goal.goal list Evd.sigma
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 5cd85547..8901a5a2 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -415,10 +415,6 @@ let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
let pp_info = ref (fun _ _ _ -> assert false)
let set_info_printer f = pp_info := f
-let tclINFO (tac : tactic) gls =
- msgnl (hov 0 (str "Warning: info is currently not working"));
- tac gls
-
(* Check that holes in arguments have been resolved *)
let check_evars env sigma extsigma gl =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 75fd6d3d..9d3d37c2 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -137,7 +137,6 @@ val tclTIMEOUT : int -> tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclNOTSAMEGOAL : tactic -> tactic
-val tclINFO : tactic -> tactic
(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
if it succeeds, applies [tac2] to the resulting subgoals,
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b8279b8f..de2e662f 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -27,6 +27,8 @@ type split_flag = bool (* true = exists false = split *)
type hidden_flag = bool (* true = internal use false = user-level *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
+type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
+
type glob_red_flag =
| FBeta
| FIota
@@ -171,13 +173,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
| TacLApply of 'constr
(* Automation tactics *)
- | TacTrivial of 'constr list * string list option
- | TacAuto of int or_var option * 'constr list * string list option
- | TacAutoTDB of int option
- | TacDestructHyp of (bool * identifier located)
- | TacDestructConcl
- | TacSuperAuto of (int option * reference list * bool * bool)
- | TacDAuto of int or_var option * int option * 'constr list
+ | TacTrivial of debug * 'constr list * string list option
+ | TacAuto of debug * int or_var option * 'constr list * string list option
(* Context management *)
| TacClear of bool * 'id list
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5475daa8..08800902 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -72,14 +72,6 @@ let pf_get_new_ids ids gls =
(fun id acc -> (next_ident_away id (acc@avoid))::acc)
ids []
-let pf_interp_constr gls c =
- let evc = project gls in
- Constrintern.interp_constr evc (pf_env gls) c
-
-let pf_interp_type gls c =
- let evc = project gls in
- Constrintern.interp_type evc (pf_env gls) c
-
let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
let pf_parse_const gls = compose (pf_global gls) id_of_string
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 884a0307..402002de 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -48,9 +48,6 @@ val pf_type_of : goal sigma -> constr -> types
val pf_check_type : goal sigma -> constr -> types -> unit
val pf_hnf_type_of : goal sigma -> constr -> types
-val pf_interp_constr : goal sigma -> Topconstr.constr_expr -> constr
-val pf_interp_type : goal sigma -> Topconstr.constr_expr -> types
-
val pf_get_hyp : goal sigma -> identifier -> named_declaration
val pf_get_hyp_typ : goal sigma -> identifier -> types
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 1c2fb278..b23f361c 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -49,11 +49,12 @@ let db_pr_goal g =
(* Prints the commands *)
let help () =
- msgnl (str "Commands: <Enter>=Continue" ++ fnl() ++
- str " h/?=Help" ++ fnl() ++
- str " r<num>=Run <num> times" ++ fnl() ++
- str " s=Skip" ++ fnl() ++
- str " x=Exit")
+ msgnl (str "Commands: <Enter> = Continue" ++ fnl() ++
+ str " h/? = Help" ++ fnl() ++
+ str " r <num> = Run <num> times" ++ fnl() ++
+ str " r <string> = Run up to next idtac <string>" ++ fnl() ++
+ str " s = Skip" ++ fnl() ++
+ str " x = Exit")
(* Prints the goal and the command to be executed *)
let goal_com g tac =
@@ -62,37 +63,62 @@ let goal_com g tac =
msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ())
end
-(* Gives the number of a run command *)
+let skipped = ref 0
+let skip = ref 0
+let breakpoint = ref None
+
+let rec drop_spaces inst i =
+ if String.length inst > i && inst.[i] = ' ' then drop_spaces inst (i+1)
+ else i
+
+let possibly_unquote s =
+ if String.length s >= 2 & s.[0] = '"' & s.[String.length s - 1] = '"' then
+ String.sub s 1 (String.length s - 2)
+ else
+ s
+
+(* (Re-)initialize debugger *)
+let db_initialize () =
+ skip:=0;skipped:=0;breakpoint:=None
+
+(* Gives the number of steps or next breakpoint of a run command *)
let run_com inst =
if (String.get inst 0)='r' then
- let num = int_of_string (String.sub inst 1 ((String.length inst)-1)) in
- if num>0 then num
- else raise (Invalid_argument "run_com")
+ let i = drop_spaces inst 1 in
+ if String.length inst > i then
+ let s = String.sub inst i (String.length inst - i) in
+ if inst.[0] >= '0' && inst.[0] <= '9' then
+ let num = int_of_string s in
+ if num<0 then raise (Invalid_argument "run_com");
+ skip:=num;skipped:=0
+ else
+ breakpoint:=Some (possibly_unquote s)
+ else
+ raise (Invalid_argument "run_com")
else
raise (Invalid_argument "run_com")
-let allskip = ref 0
-let skip = ref 0
-
(* Prints the run counter *)
let run ini =
if not ini then
+ begin
for i=1 to 2 do
print_char (Char.chr 8);print_char (Char.chr 13)
done;
- msg (str "Executed expressions: " ++ int (!allskip - !skip) ++
- fnl() ++ fnl())
+ msg (str "Executed expressions: " ++ int !skipped ++ fnl() ++ fnl())
+ end;
+ incr skipped
(* Prints the prompt *)
let rec prompt level =
begin
msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
flush stdout;
- let exit () = skip:=0;allskip:=0;raise Sys.Break in
+ let exit () = skip:=0;skipped:=0;raise Sys.Break in
let inst = try read_line () with End_of_file -> exit () in
match inst with
- | "" -> true
- | "s" -> false
+ | "" -> DebugOn (level+1)
+ | "s" -> DebugOff
| "x" -> print_char (Char.chr 8); exit ()
| "h"| "?" ->
begin
@@ -100,32 +126,34 @@ let rec prompt level =
prompt level
end
| _ ->
- (try let ctr=run_com inst in skip:=ctr;allskip:=ctr;run true;true
+ (try run_com inst;run true;DebugOn (level+1)
with Failure _ | Invalid_argument _ -> prompt level)
end
(* Prints the state and waits for an instruction *)
let debug_prompt lev g tac f =
(* What to print and to do next *)
- let continue =
- if !skip = 0 then (goal_com g tac; prompt lev)
- else (decr skip; run false; if !skip=0 then allskip:=0; true) in
+ let newlevel =
+ if !skip = 0 then
+ if !breakpoint = None then (goal_com g tac; prompt lev)
+ else (run false; DebugOn (lev+1))
+ else (decr skip; run false; if !skip=0 then skipped:=0; DebugOn (lev+1)) in
(* What to execute *)
- try f (if continue then DebugOn (lev+1) else DebugOff)
+ try f newlevel
with e ->
- skip:=0; allskip:=0;
+ skip:=0; skipped:=0;
if Logic.catchable_exception e then
ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
raise e
(* Prints a constr *)
let db_constr debug env c =
- if debug <> DebugOff & !skip = 0 then
+ if debug <> DebugOff & !skip = 0 & !breakpoint = None then
msgnl (str "Evaluated term: " ++ print_constr_env env c)
(* Prints the pattern rule *)
let db_pattern_rule debug num r =
- if debug <> DebugOff & !skip = 0 then
+ if debug <> DebugOff & !skip = 0 & !breakpoint = None then
begin
msgnl (str "Pattern rule " ++ int num ++ str ":");
msgnl (str "|" ++ spc () ++ !prmatchrl r)
@@ -138,38 +166,38 @@ let hyp_bound = function
(* Prints a matched hypothesis *)
let db_matched_hyp debug env (id,_,c) ido =
- if debug <> DebugOff & !skip = 0 then
+ if debug <> DebugOff & !skip = 0 & !breakpoint = None then
msgnl (str "Hypothesis " ++
str ((Names.string_of_id id)^(hyp_bound ido)^
" has been matched: ") ++ print_constr_env env c)
(* Prints the matched conclusion *)
let db_matched_concl debug env c =
- if debug <> DebugOff & !skip = 0 then
+ if debug <> DebugOff & !skip = 0 & !breakpoint = None then
msgnl (str "Conclusion has been matched: " ++ print_constr_env env c)
(* Prints a success message when the goal has been matched *)
let db_mc_pattern_success debug =
- if debug <> DebugOff & !skip = 0 then
+ if debug <> DebugOff & !skip = 0 & !breakpoint = None then
msgnl (str "The goal has been successfully matched!" ++ fnl() ++
str "Let us execute the right-hand side part..." ++ fnl())
(* Prints a failure message for an hypothesis pattern *)
let db_hyp_pattern_failure debug env (na,hyp) =
- if debug <> DebugOff & !skip = 0 then
+ if debug <> DebugOff & !skip = 0 & !breakpoint = None then
msgnl (str ("The pattern hypothesis"^(hyp_bound na)^
" cannot match: ") ++
!prmatchpatt env hyp)
(* Prints a matching failure message for a rule *)
let db_matching_failure debug =
- if debug <> DebugOff & !skip = 0 then
+ if debug <> DebugOff & !skip = 0 & !breakpoint = None then
msgnl (str "This rule has failed due to matching errors!" ++ fnl() ++
str "Let us try the next one...")
(* Prints an evaluation failure message for a rule *)
let db_eval_failure debug s =
- if debug <> DebugOff & !skip = 0 then
+ if debug <> DebugOff & !skip = 0 & !breakpoint = None then
let s = str "message \"" ++ s ++ str "\"" in
msgnl
(str "This rule has failed due to \"Fail\" tactic (" ++
@@ -177,9 +205,20 @@ let db_eval_failure debug s =
(* Prints a logic failure message for a rule *)
let db_logic_failure debug err =
- if debug <> DebugOff & !skip = 0 then
+ if debug <> DebugOff & !skip = 0 & !breakpoint = None then
begin
msgnl (!explain_logic_error err);
msgnl (str "This rule has failed due to a logic error!" ++ fnl() ++
str "Let us try the next one...")
end
+
+let is_breakpoint brkname s = match brkname, s with
+ | Some s, MsgString s'::_ -> s = s'
+ | _ -> false
+
+let db_breakpoint debug s =
+ match debug with
+ | DebugOn lev when s <> [] & is_breakpoint !breakpoint s ->
+ breakpoint:=None
+ | _ ->
+ ()
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index d96f4c74..62c2359b 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -34,6 +34,9 @@ type debug_info =
val debug_prompt :
int -> goal sigma -> glob_tactic_expr -> (debug_info -> 'a) -> 'a
+(** Initializes debugger *)
+val db_initialize : unit -> unit
+
(** Prints a constr *)
val db_constr : debug_info -> env -> constr -> unit
@@ -72,3 +75,7 @@ val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
(** Prints a logic failure message for a rule *)
val db_logic_failure : debug_info -> exn -> unit
+
+(** Prints a logic failure message for a rule *)
+val db_breakpoint : debug_info ->
+ identifier Util.located message_token list -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 00:52:16 +0000