From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- proofs/clenv.ml | 6 ++--- proofs/clenv.mli | 4 +-- proofs/clenvtac.ml | 2 +- proofs/clenvtac.mli | 2 +- proofs/evar_refiner.ml | 2 +- proofs/evar_refiner.mli | 2 +- proofs/goal.ml | 2 +- proofs/goal.mli | 2 +- proofs/logic.ml | 2 +- proofs/logic.mli | 2 +- proofs/logic_monad.ml | 2 +- proofs/logic_monad.mli | 2 +- proofs/pfedit.ml | 12 ++++++--- proofs/pfedit.mli | 9 +++++-- proofs/proof.ml | 2 +- proofs/proof.mli | 2 +- proofs/proof_global.ml | 40 ++++++++++++++++++--------- proofs/proof_global.mli | 19 +++++++------ proofs/proof_type.ml | 2 +- proofs/proof_type.mli | 2 +- proofs/proof_using.ml | 2 +- proofs/proof_using.mli | 2 +- proofs/proofview.ml | 67 +++++++++++++++++++++++++++++++++++++--------- proofs/proofview.mli | 6 ++++- proofs/proofview_monad.ml | 25 ++++++++++------- proofs/proofview_monad.mli | 14 ++++++---- proofs/redexpr.ml | 2 +- proofs/redexpr.mli | 2 +- proofs/refiner.ml | 2 +- proofs/refiner.mli | 2 +- proofs/tacmach.ml | 2 +- proofs/tacmach.mli | 2 +- proofs/tactic_debug.ml | 2 +- proofs/tactic_debug.mli | 2 +- 34 files changed, 165 insertions(+), 85 deletions(-) (limited to 'proofs') 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* 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"")) >> - 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(*