diff options
Diffstat (limited to 'proofs')
34 files changed, 165 insertions, 85 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index a2cccc0e..88e1bce9 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -379,12 +379,12 @@ let fchain_flags () = { (default_unify_flags ()) with allow_K_in_toplevel_higher_order_unification = true } -let clenv_fchain ?(flags=fchain_flags ()) mv clenv nextclenv = +let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv = (* Add the metavars of [nextclenv] to [clenv], with their name-environment *) let clenv' = { templval = clenv.templval; templtyp = clenv.templtyp; - evd = meta_merge nextclenv.evd clenv.evd; + evd = meta_merge ?with_univs nextclenv.evd clenv.evd; env = nextclenv.env } in (* unify the type of the template of [nextclenv] with the type of [mv] *) let clenv'' = diff --git a/proofs/clenv.mli b/proofs/clenv.mli index eb108170..7ecc26ec 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -51,7 +51,7 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst val connect_clenv : Goal.goal sigma -> clausenv -> clausenv val clenv_fchain : - ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv + ?with_univs:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv (** {6 Unification with clenvs } *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index aaa49f11..8e922599 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index ea204361..00e74a24 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 9b358210..059ae54c 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 673dad55..35a3e5d8 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/goal.ml b/proofs/goal.ml index 107ce7f8..1dd5be0e 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/goal.mli b/proofs/goal.mli index a00a95a2..6152826c 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/logic.ml b/proofs/logic.ml index 3273c957..ed3a1df1 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/logic.mli b/proofs/logic.mli index d034b73c..ed99d3a3 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml index e3caa886..68efa71e 100644 --- a/proofs/logic_monad.ml +++ b/proofs/logic_monad.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli index 84ffda75..96655d53 100644 --- a/proofs/logic_monad.mli +++ b/proofs/logic_monad.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 02dbd1fd..b635cc96 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -20,14 +20,15 @@ let get_current_proof_name = Proof_global.get_current_proof_name let get_all_proof_names = Proof_global.get_all_proof_names type lemma_possible_guards = Proof_global.lemma_possible_guards +type universe_binders = Proof_global.universe_binders let delete_proof = Proof_global.discard let delete_current_proof = Proof_global.discard_current let delete_all_proofs = Proof_global.discard_all -let start_proof (id : Id.t) str sigma hyps c ?init_tac terminator = +let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator = let goals = [ (Global.env_of_context hyps , c) ] in - Proof_global.start_proof sigma id str goals terminator; + Proof_global.start_proof sigma id ?pl str goals terminator; let env = Global.env () in ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with @@ -54,6 +55,9 @@ let set_used_variables l = let get_used_variables () = Proof_global.get_used_variables () +let get_universe_binders () = + Proof_global.get_universe_binders () + exception NoSuchGoal let _ = Errors.register_handler begin function | NoSuchGoal -> Errors.error "No such goal." @@ -139,7 +143,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let status = by tac in let _,(const,univs,_) = cook_proof () in delete_current_proof (); - const, status, univs + const, status, fst univs with reraise -> let reraise = Errors.push reraise in delete_current_proof (); diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index fc521ea4..cd899201 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -55,8 +55,10 @@ val delete_all_proofs : unit -> unit type lemma_possible_guards = Proof_global.lemma_possible_guards +type universe_binders = Id.t Loc.located list + val start_proof : - Id.t -> goal_kind -> Evd.evar_map -> named_context_val -> constr -> + Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr -> ?init_tac:unit Proofview.tactic -> Proof_global.proof_terminator -> unit @@ -121,6 +123,9 @@ val set_used_variables : Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list val get_used_variables : unit -> Context.section_context option +(** {6 Universe binders } *) +val get_universe_binders : unit -> universe_binders option + (** {6 ... } *) (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th subgoal of the current focused proof or raises a [UserError] if no diff --git a/proofs/proof.ml b/proofs/proof.ml index c7aa5bad..0489305a 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/proof.mli b/proofs/proof.mli index a0ed0654..5053fc7f 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index c303f486..f22cdbcc 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -63,14 +63,14 @@ let _ = (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_universes = Evd.evar_universe_context +type proof_universes = Evd.evar_universe_context * Universes.universe_binders option +type universe_binders = Id.t Loc.located list type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: proof_universes; - (* constraints : Univ.constraints; *) } type proof_ending = @@ -89,6 +89,7 @@ type pstate = { proof : Proof.proof; strength : Decl_kinds.goal_kind; mode : proof_mode Ephemeron.key; + universe_binders: universe_binders option; } (* The head of [!pstates] is the actual current proof, the other ones are @@ -226,7 +227,7 @@ let disactivate_proof_mode mode = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints). *) -let start_proof sigma id str goals terminator = +let start_proof sigma id ?pl str goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; @@ -234,10 +235,11 @@ let start_proof sigma id str goals terminator = endline_tactic = None; section_vars = None; strength = str; - mode = find_proof_mode "No" } in + mode = find_proof_mode "No"; + universe_binders = pl } in push initial_state pstates -let start_dependent_proof id str goals terminator = +let start_dependent_proof id ?pl str goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; @@ -245,12 +247,14 @@ let start_dependent_proof id str goals terminator = endline_tactic = None; section_vars = None; strength = str; - mode = find_proof_mode "No" } in + mode = find_proof_mode "No"; + universe_binders = pl } in push initial_state pstates let get_used_variables () = (cur_pstate ()).section_vars +let get_universe_binders () = (cur_pstate ()).universe_binders -let proof_using_auto_clear = ref true +let proof_using_auto_clear = ref false let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optdepr = false; @@ -296,7 +300,8 @@ let get_open_goals () = List.length shelf let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = - let { pid; section_vars; strength; proof; terminator } = cur_pstate () in + let { pid; section_vars; strength; proof; terminator; universe_binders } = + cur_pstate () in let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in @@ -328,7 +333,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = (* For vi2vo compilation proofs are computed now but we need to * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) - let ctx_body = restrict_universe_context ctx used_univs_body in + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let ctx_body = restrict_universe_context ctx used_univs in (initunivs, typ), ((body, ctx_body), eff) else let initunivs = Univ.UContext.empty in @@ -362,8 +368,13 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = const_entry_opaque = true; const_entry_universes = univs; const_entry_polymorphic = poly}) - fpl initial_goals in - { id = pid; entries = entries; persistence = strength; universes = universes }, + fpl initial_goals in + let binders = + Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes))) + universe_binders + in + { id = pid; entries = entries; persistence = strength; + universes = (universes, binders) }, fun pr_ending -> Ephemeron.get terminator pr_ending type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context @@ -612,7 +623,10 @@ module Bullet = struct (!current_behavior).name end; optwrite = begin fun n -> - current_behavior := Hashtbl.find behaviors n + current_behavior := + try Hashtbl.find behaviors n + with Not_found -> + Errors.error ("Unknown bullet behavior: \"" ^ n ^ "\".") end } diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index a2254508..7fbd183e 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -55,18 +55,18 @@ val compact_the_proof : unit -> unit (i.e. an proof ending command) and registers the appropriate values. *) type lemma_possible_guards = int list list -type proof_universes = Evd.evar_universe_context +type proof_universes = Evd.evar_universe_context * Universes.universe_binders option +type universe_binders = Names.Id.t Loc.located list type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: proof_universes; - (* constraints : Univ.constraints; *) - (** guards : lemma_possible_guards; *) } type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * + proof_universes | Proved of Vernacexpr.opacity_flag * (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * proof_object @@ -80,14 +80,15 @@ type closed_proof = proof_object * proof_terminator closing commands and the xml plugin); [terminator] is used at the end of the proof to close the proof. *) val start_proof : - Evd.evar_map -> Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list -> + Evd.evar_map -> Names.Id.t -> ?pl:universe_binders -> + Decl_kinds.goal_kind -> (Environ.env * Term.types) list -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between initial goals. *) val start_dependent_proof : - Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope -> - proof_terminator -> unit + Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind -> + Proofview.telescope -> proof_terminator -> unit (** Update the proofs global environment after a side-effecting command (e.g. a sublemma definition) has been run inside it. Assumes @@ -140,6 +141,8 @@ val set_used_variables : Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list val get_used_variables : unit -> Context.section_context option +val get_universe_binders : unit -> universe_binders option + (**********************************************************) (* *) (* Proof modes *) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 47b2b255..dd2c7b25 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index f5e2bad2..aa05f58a 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index 7eed1cb3..a69645b1 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli index dcf8a0fc..1bf38b69 100644 --- a/proofs/proof_using.mli +++ b/proofs/proof_using.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 4fc0c164..a6d9735f 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,7 +32,7 @@ type entry = (Term.constr * Term.types) list let proofview p = p.comb , p.solution -let compact el { comb; solution } = +let compact el ({ solution } as pv) = let nf = Evarutil.nf_evar solution in let size = Evd.fold (fun _ _ i -> i+1) solution 0 in let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in @@ -45,7 +45,7 @@ let compact el { comb; solution } = let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); - new_el, { comb; solution = new_solution } + new_el, { pv with solution = new_solution; } (** {6 Starting and querying a proof view} *) @@ -62,13 +62,13 @@ let dependent_init = let src = (Loc.ghost,Evar_kinds.GoalEvar) in (* Main routine *) let rec aux = function - | TNil sigma -> [], { solution = sigma; comb = []; } + | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let (gl, _) = Term.destEvar econstr in let entry = (econstr, typ) :: ret in - entry, { solution = sol; comb = gl :: comb; } + entry, { solution = sol; comb = gl :: comb; shelf = [] } in fun t -> let entry, v = aux t in @@ -232,6 +232,9 @@ let apply env t sp = match ans with | Nil (e, info) -> iraise (TacticFailure e, info) | Cons ((r, (state, _), status, info), _) -> + let (status, gaveup) = status in + let status = (status, state.shelf, gaveup) in + let state = { state with shelf = [] } in r, state, status, Trace.to_tree info @@ -578,7 +581,7 @@ let shelve = Comb.get >>= fun initial -> Comb.set [] >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> - Shelf.put initial + Shelf.modify (fun gls -> gls @ initial) (** [contained_in_info e evi] checks whether the evar [e] appears in @@ -617,7 +620,7 @@ let shelve_unifiable = let (u,n) = partition_unifiable initial.solution initial.comb in Comb.set n >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >> - Shelf.put u + Shelf.modify (fun gls -> gls @ u) (** [guard_no_unifiable] fails with error [UnresolvedBindings] if some goals are unifiable (see {!shelve_unifiable}) in the current focus. *) @@ -639,6 +642,20 @@ let unshelve l p = let l = undefined p.solution l in { p with comb = p.comb@l } +let with_shelf tac = + let open Proof in + Pv.get >>= fun pv -> + let { shelf; solution } = pv in + Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >> + tac >>= fun ans -> + Pv.get >>= fun npv -> + let { shelf = gls; solution = sigma } = npv in + let gls' = Evd.future_goals sigma in + let fgoals = Evd.future_goals solution in + let pgoal = Evd.principal_future_goal solution in + let sigma = Evd.restore_future_goals sigma fgoals pgoal in + Pv.set { npv with shelf; solution = sigma } >> + tclUNIT (CList.rev_append gls' gls, ans) (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) @@ -867,7 +884,7 @@ module Unsafe = struct let tclSETGOALS = Comb.set let tclEVARSADVANCE evd = - Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb }) + Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb }) let tclEVARUNIVCONTEXT ctx = Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) @@ -1010,10 +1027,34 @@ end module Refine = struct + let extract_prefix env info = + let ctx1 = List.rev (Environ.named_context env) in + let ctx2 = List.rev (Evd.evar_context info) in + let rec share l1 l2 accu = match l1, l2 with + | d1 :: l1, d2 :: l2 -> + if d1 == d2 then share l1 l2 (d1 :: accu) + else (accu, d2 :: l2) + | _ -> (accu, l2) + in + share ctx1 ctx2 [] + let typecheck_evar ev env sigma = let info = Evd.find sigma ev in + (** Typecheck the hypotheses. *) + let type_hyp (sigma, env) (na, body, t as decl) = + let evdref = ref sigma in + let _ = Typing.sort_of env evdref t in + let () = match body with + | None -> () + | Some body -> Typing.check env evdref body t + in + (!evdref, Environ.push_named decl env) + in + let (common, changed) = extract_prefix env info in + let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in + let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in + (** Typecheck the conclusion *) let evdref = ref sigma in - let env = Environ.reset_with_named_context (Evd.evar_hyps info) env in let _ = Typing.sort_of env evdref (Evd.evar_concl info) in !evdref @@ -1061,7 +1102,7 @@ struct let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in let open Proof in InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> - Pv.set { solution = sigma; comb; } + Pv.modify (fun ps -> { ps with solution = sigma; comb; }) end (** Useful definitions *) @@ -1140,7 +1181,7 @@ module V82 = struct let sgs = CList.flatten goalss in let sgs = undefined evd sgs in InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >> - Pv.set { solution = evd; comb = sgs; } + Pv.set { ps with solution = evd; comb = sgs; } with e when catchable_exception e -> let (e, info) = Errors.push e in tclZERO ~info e @@ -1152,7 +1193,7 @@ module V82 = struct Pv.modify begin fun ps -> let map g s = GoalV82.nf_evar s g in let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in - { solution = evd; comb = goals; } + { ps with solution = evd; comb = goals; } end let has_unresolved_evar pv = @@ -1197,7 +1238,7 @@ module V82 = struct let of_tactic t gls = try - let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in + let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in let (_,final,_,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = final.comb } with Logic_monad.TacticFailure e as src -> diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 927df33a..2157459f 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -303,6 +303,10 @@ val guard_no_unifiable : unit tactic goals of p *) val unshelve : Goal.goal list -> proofview -> proofview +(** [with_shelf tac] executes [tac] and returns its result together with the set + of goals shelved by [tac]. The current shelf is unchanged. *) +val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic + (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] is negative, then it puts the [n] last goals first.*) val cycle : int -> unit tactic diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml index 6e68cd2e..e9bc7761 100644 --- a/proofs/proofview_monad.ml +++ b/proofs/proofview_monad.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -157,8 +157,11 @@ end (** Type of proof views: current [evar_map] together with the list of focused goals. *) -type proofview = { solution : Evd.evar_map; comb : Goal.goal list } - +type proofview = { + solution : Evd.evar_map; + comb : Goal.goal list; + shelf : Goal.goal list; +} (** {6 Instantiation of the logic monad} *) @@ -171,10 +174,10 @@ module P = struct type e = bool (** Status (safe/unsafe) * shelved goals * given up *) - type w = bool * Evar.t list * Evar.t list + type w = bool * Evar.t list - let wunit = true , [] , [] - let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2 + let wunit = true , [] + let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2 type u = Info.state @@ -226,19 +229,21 @@ module Env : State with type t := Environ.env = struct end module Status : Writer with type t := bool = struct - let put s = Logical.put (s,[],[]) + let put s = Logical.put (s, []) end -module Shelf : Writer with type t = Evar.t list = struct +module Shelf : State with type t = Evar.t list = struct (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) type t = Evar.t list - let put sh = Logical.put (true,sh,[]) + let get = Logical.map (fun {shelf} -> shelf) Pv.get + let set c = Pv.modify (fun pv -> { pv with shelf = c }) + let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf }) end module Giveup : Writer with type t = Evar.t list = struct (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) type t = Evar.t list - let put gs = Logical.put (true,[],gs) + let put gs = Logical.put (true, gs) end (** Lens and utilies pertaining to the info trace *) diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index d2a2e55f..7a6ea10f 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -68,15 +68,19 @@ end (** Type of proof views: current [evar_map] together with the list of focused goals. *) -type proofview = { solution : Evd.evar_map; comb : Goal.goal list } +type proofview = { + solution : Evd.evar_map; + comb : Goal.goal list; + shelf : Goal.goal list; +} (** {6 Instantiation of the logic monad} *) module P : sig type s = proofview * Environ.env - (** Status (safe/unsafe) * shelved goals * given up *) - type w = bool * Evar.t list * Evar.t list + (** Status (safe/unsafe) * given up *) + type w = bool * Evar.t list val wunit : w val wprod : w -> w -> w @@ -123,7 +127,7 @@ module Status : Writer with type t := bool (** Lens to the list of goals which have been shelved during the execution of the tactic. *) -module Shelf : Writer with type t = Evar.t list +module Shelf : State with type t = Evar.t list (** Lens to the list of goals which were given up during the execution of the tactic. *) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index be92f2b0..ea21917a 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index b32cedf8..b9191108 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ba62b2cb..14493458 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index a81555ff..13a9be59 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 4238d1e3..a75b6fa0 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index a0e1a015..7e943cb1 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 6d6215c5..a4a447e8 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index e4c0a23e..215c5b29 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |