diff options
Diffstat (limited to 'engine')
36 files changed, 166 insertions, 139 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 981f9454e4..23d066df58 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 25ceffbd04..2afce38db7 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml index ea1e572548..bfe0aa3544 100644 --- a/engine/evar_kinds.ml +++ b/engine/evar_kinds.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/evar_kinds.mli b/engine/evar_kinds.mli index 4facdb2005..008633d754 100644 --- a/engine/evar_kinds.mli +++ b/engine/evar_kinds.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index be0318fbde..911b189deb 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -656,26 +656,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids = (* spiwack: a few functions to gather evars on which goals depend. *) let queue_set q is_dependent set = Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set -let queue_term q is_dependent c = - queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c)) +let queue_term evm q is_dependent c = + queue_set q is_dependent (evars_of_term evm c) let process_dependent_evar q acc evm is_dependent e = let evi = Evd.find evm e in (* Queues evars appearing in the types of the goal (conclusion, then hypotheses), they are all dependent. *) - queue_term q true evi.evar_concl; + queue_term evm q true evi.evar_concl; List.iter begin fun decl -> let open NamedDecl in - queue_term q true (NamedDecl.get_type decl); + queue_term evm q true (NamedDecl.get_type decl); match decl with | LocalAssum _ -> () - | LocalDef (_,b,_) -> queue_term q true b + | LocalDef (_,b,_) -> queue_term evm q true b end (EConstr.named_context_of_val evi.evar_hyps); match evi.evar_body with | Evar_empty -> if is_dependent then Evar.Map.add e None acc else acc | Evar_defined b -> - let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in + let subevars = evars_of_term evm b in (* evars appearing in the definition of an evar [e] are marked as dependent when [e] is dependent itself: if [e] is a non-dependent goal, then, unless they are reach from another @@ -795,7 +795,7 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi = in let accu = match evi.evar_body with | Evar_empty -> Evar.Set.empty - | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b) + | Evar_defined b -> evars_of_term sigma b in let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in @@ -860,7 +860,7 @@ let compare_constructor_instances evd u u' = [u] up to existential variable instantiation and equalisable universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extention of those in [sigma1]. *) + assumed to be an extension of those in [sigma1]. *) let eq_constr_univs_test sigma1 sigma2 t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 8eaff8bd13..e9d579af32 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -208,7 +208,7 @@ val kind_of_term_upto : evar_map -> Constr.constr -> [u] up to existential variable instantiation and equalisable universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extention of those in [sigma1]. *) + assumed to be an extension of those in [sigma1]. *) val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns diff --git a/engine/evd.ml b/engine/evd.ml index d37b49e2dc..b621a3fe2f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -222,7 +222,7 @@ let map_evar_body f = function let map_evar_info f evi = {evi with evar_body = map_evar_body f evi.evar_body; - evar_hyps = map_named_val f evi.evar_hyps; + evar_hyps = map_named_val (fun d -> NamedDecl.map_constr f d) evi.evar_hyps; evar_concl = f evi.evar_concl; evar_candidates = Option.map (List.map f) evi.evar_candidates } @@ -430,6 +430,14 @@ type evar_flags = restricted_evars : Evar.t Evar.Map.t; typeclass_evars : Evar.Set.t } +type side_effect_role = +| Schema of inductive * string + +type side_effects = { + seff_private : Safe_typing.private_constants; + seff_roles : side_effect_role Cmap.t; +} + type evar_map = { (* Existential variables *) defn_evars : evar_info EvMap.t; @@ -444,7 +452,7 @@ type evar_map = { metas : clbinding Metamap.t; evar_flags : evar_flags; (** Interactive proofs *) - effects : Safe_typing.private_constants; + effects : side_effects; future_goals : Evar.t list; (** list of newly created evars, to be eventually turned into goals if not solved.*) principal_future_goal : Evar.t option; (** if [Some e], [e] must be @@ -672,6 +680,11 @@ let empty_evar_flags = restricted_evars = Evar.Map.empty; typeclass_evars = Evar.Set.empty } +let empty_side_effects = { + seff_private = Safe_typing.empty_private_constants; + seff_roles = Cmap.empty; +} + let empty = { defn_evars = EvMap.empty; undf_evars = EvMap.empty; @@ -680,7 +693,7 @@ let empty = { last_mods = Evar.Set.empty; evar_flags = empty_evar_flags; metas = Metamap.empty; - effects = Safe_typing.empty_private_constants; + effects = empty_side_effects; evar_names = EvNames.empty; (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; @@ -823,33 +836,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) = | Evar (evk2,_) -> fst (evar_source evk2 evd) | _ -> None -(** The following functions return the set of evars immediately - contained in the object *) - -(* excluding defined evars *) - -let evars_of_term c = - let rec evrec acc c = - match kind c with - | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) - | _ -> Constr.fold evrec acc c - in - evrec Evar.Set.empty c - -let evars_of_named_context nc = - Context.Named.fold_outside - (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr))) - nc - ~init:Evar.Set.empty - -let evars_of_filtered_evar_info evi = - Evar.Set.union (evars_of_term evi.evar_concl) - (Evar.Set.union - (match evi.evar_body with - | Evar_empty -> Evar.Set.empty - | Evar_defined b -> evars_of_term b) - (evars_of_named_context (evar_filtered_context evi))) - (**********************************************************) (* Sort variables *) @@ -1038,12 +1024,17 @@ exception UniversesDiffer = UState.UniversesDiffer (**********************************************************) (* Side effects *) +let concat_side_effects eff eff' = { + seff_private = Safe_typing.concat_private eff.seff_private eff'.seff_private; + seff_roles = Cmap.fold Cmap.add eff.seff_roles eff'.seff_roles; +} + let emit_side_effects eff evd = - { evd with effects = Safe_typing.concat_private eff evd.effects; - universes = UState.emit_side_effects eff evd.universes } + let effects = concat_side_effects eff evd.effects in + { evd with effects; universes = UState.emit_side_effects eff.seff_private evd.universes } let drop_side_effects evd = - { evd with effects = Safe_typing.empty_private_constants; } + { evd with effects = empty_side_effects; } let eval_side_effects evd = evd.effects @@ -1404,3 +1395,30 @@ module MiniEConstr = struct let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d end + +(** The following functions return the set of evars immediately + contained in the object *) + +(* excluding defined evars *) + +let evars_of_term evd c = + let rec evrec acc c = + match MiniEConstr.kind evd c with + | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) + | _ -> Constr.fold evrec acc c + in + evrec Evar.Set.empty c + +let evars_of_named_context evd nc = + Context.Named.fold_outside + (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term evd constr))) + nc + ~init:Evar.Set.empty + +let evars_of_filtered_evar_info evd evi = + Evar.Set.union (evars_of_term evd evi.evar_concl) + (Evar.Set.union + (match evi.evar_body with + | Evar_empty -> Evar.Set.empty + | Evar_defined b -> evars_of_term evd b) + (evars_of_named_context evd (evar_filtered_context evi))) diff --git a/engine/evd.mli b/engine/evd.mli index 29235050b0..132f7bc745 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -307,10 +307,22 @@ val dependent_evar_ident : Evar.t -> evar_map -> Id.t (** {5 Side-effects} *) -val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map +type side_effect_role = +| Schema of inductive * string + +type side_effects = { + seff_private : Safe_typing.private_constants; + seff_roles : side_effect_role Cmap.t; +} + +val empty_side_effects : side_effects + +val concat_side_effects : side_effects -> side_effects -> side_effects + +val emit_side_effects : side_effects -> evar_map -> evar_map (** Push a side-effect into the evar map. *) -val eval_side_effects : evar_map -> Safe_typing.private_constants +val eval_side_effects : evar_map -> side_effects (** Return the effects contained in the evar map. *) val drop_side_effects : evar_map -> evar_map @@ -491,16 +503,15 @@ val extract_changed_conv_pbs : evar_map -> val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option -(** The following functions return the set of evars immediately - contained in the object; need the term to be evar-normal otherwise - defined evars are returned too. *) +(** The following functions return the set of undefined evars + contained in the object. *) -val evars_of_term : constr -> Evar.Set.t +val evars_of_term : evar_map -> econstr -> Evar.Set.t (** including evars in instances of evars *) -val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t +val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t -val evars_of_filtered_evar_info : evar_info -> Evar.Set.t +val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t (** Metas *) val meta_list : evar_map -> (metavariable * clbinding) list diff --git a/engine/ftactic.ml b/engine/ftactic.ml index dab2e7d5ef..a727375c8d 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -18,8 +18,8 @@ type 'a focus = (** Type of tactics potentially goal-dependent. If it contains a [Depends], then the length of the inner list is guaranteed to be the number of - currently focussed goals. Otherwise it means the tactic does not depend - on the current set of focussed goals. *) + currently focused goals. Otherwise it means the tactic does not depend + on the current set of focused goals. *) type 'a t = 'a focus Proofview.tactic let return (x : 'a) : 'a t = Proofview.tclUNIT (Uniform x) diff --git a/engine/ftactic.mli b/engine/ftactic.mli index ed95d62bc6..666a74d283 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -18,7 +18,7 @@ type +'a t = 'a focus Proofview.tactic (** The type of focussing tactics. A focussing tactic is like a normal tactic, except that it is able to remember it have entered a goal. Whenever this is the case, each subsequent effect of the tactic is dispatched on the - focussed goals. This is a monad. *) + focused goals. This is a monad. *) (** {5 Monadic interface} *) @@ -32,20 +32,20 @@ val bind : 'a t -> ('a -> 'b t) -> 'b t val lift : 'a Proofview.tactic -> 'a t (** Transform a tactic into a focussing tactic. The resulting tactic is not - focussed. *) + focused. *) val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic (** Given a continuation producing a tactic, evaluates the focussing tactic. If - the tactic has not focussed, then the continuation is evaluated once. - Otherwise it is called in each of the currently focussed goals. *) + the tactic has not focused, then the continuation is evaluated once. + Otherwise it is called in each of the currently focused goals. *) (** {5 Focussing} *) -(** Enter a goal. The resulting tactic is focussed. *) +(** Enter a goal. The resulting tactic is focused. *) val enter : (Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal, without evar normalization. The resulting tactic is - focussed. *) + focused. *) val with_env : 'a t -> (Environ.env*'a) t (** [with_env t] returns, in addition to the return type of [t], an diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index e0c24f049f..2354d2c5e8 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -151,7 +151,7 @@ struct (** Double-continuation backtracking monads are reasonable folklore for "search" implementations (including the Tac interactive prover's tactics). Yet it's quite hard to wrap your head around - these. I recommand reading a few times the "Backtracking, + these. I recommend reading a few times the "Backtracking, Interleaving, and Terminating Monad Transformers" paper by O. Kiselyov, C. Shan, D. Friedman, and A. Sabry. The peculiar shape of the monadic type is reminiscent of that of the diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 3e57baab26..90c920439a 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/namegen.ml b/engine/namegen.ml index 10ece55a63..77d45ce1e4 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/namegen.mli b/engine/namegen.mli index 240fd8fa81..7a8544f2d6 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/nameops.ml b/engine/nameops.ml index 31914f9cfa..baa19050d7 100644 --- a/engine/nameops.ml +++ b/engine/nameops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/nameops.mli b/engine/nameops.mli index 222573450b..a0f3a72233 100644 --- a/engine/nameops.mli +++ b/engine/nameops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/proofview.ml b/engine/proofview.ml index ecea637947..c4a624e462 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -31,7 +31,7 @@ type entry = (EConstr.constr * EConstr.types) list ide-s. *) (* spiwack: the type of [proofview] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: returns the list of focused goals together with the [evar_map] context. *) let proofview p = @@ -46,7 +46,7 @@ let compact el ({ solution } as pv) = let apply_subst_einfo _ ei = Evd.({ ei with evar_concl = nf ei.evar_concl; - evar_hyps = Environ.map_named_val nf0 ei.evar_hyps; + evar_hyps = Environ.map_named_val (fun d -> map_constr nf0 d) ei.evar_hyps; evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in 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 @@ -114,7 +114,7 @@ type focus_context = goal_with_state list * goal_with_state list instance, ide-s. *) (* spiwack: the type of [focus_context] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) let focus_context (left,right) = @@ -123,7 +123,7 @@ let focus_context (left,right) = (** This (internal) function extracts a sublist between two indices, and returns this sublist together with its context: if it returns [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the - original list. The focused list has lenght [j-i-1] and contains + original list. The focused list has length [j-i-1] and contains the goals from number [i] to number [j] (both included) the first goal of the list being numbered [1]. [focus_sublist i j l] raises [IndexOutOfRange] if [i > length l], or [j > length l] or [j < @@ -245,7 +245,7 @@ let tclUNIT = Proof.return (** Bind operation of the tactic monad. *) let tclBIND = Proof.(>>=) -(** Interpretes the ";" (semicolon) of Ltac. As a monadic operation, +(** Interprets the ";" (semicolon) of Ltac. As a monadic operation, it's a specialized "bind". *) let tclTHEN = Proof.(>>) @@ -373,32 +373,24 @@ let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t = let open Proof in Comb.get >>= fun comb -> - let n = CList.length comb in - (* First, remove empty intervals, and bound the intervals to the number - of goals. *) - let sanitize (i, j) = - if i > j then None - else if i > n then None - else if j < 1 then None - else Some ((max i 1), (min j n)) - in - let l = CList.map_filter sanitize l in + let n = CList.length comb in + let ok (i, j) = 1 <= i && i <= j && j <= n in + if not (CList.for_all ok l) then nosuchgoal + else match l with - | [] -> nosuchgoal - | (mi, _) :: _ -> - (* Get the left-most goal to focus. This goal won't move, and we - will then place all the other goals to focus to the right. *) - let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in - (* [CList.goto] returns a zipper, so that - [(rev left) @ sub_right = comb]. *) - let left, sub_right = CList.goto (mi-1) comb in - let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in - let sub, right = CList.partitioni p sub_right in - let mj = mi - 1 + CList.length sub in - Comb.set (CList.rev_append left (sub @ right)) >> - tclFOCUS mi mj t - - + | [] -> nosuchgoal + | (mi, _) :: _ -> + (* Get the left-most goal to focus. This goal won't move, and we + will then place all the other goals to focus to the right. *) + let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in + (* [CList.goto] returns a zipper, so that + [(rev left) @ sub_right = comb]. *) + let left, sub_right = CList.goto (mi-1) comb in + let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in + let sub, right = CList.partitioni p sub_right in + let mj = mi - 1 + CList.length sub in + Comb.set (CList.rev_append left (sub @ right)) >> + tclFOCUS mi mj t (** Like {!tclFOCUS} but selects a single goal by name. *) let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t = @@ -641,7 +633,7 @@ let shelve_goals l = [sigma]. *) let depends_on sigma src tgt = let evi = Evd.find sigma tgt in - Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) + Evar.Set.mem src (Evd.evars_of_filtered_evar_info sigma (Evarutil.nf_evar_info sigma evi)) let unifiable_delayed g l = CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l @@ -1251,9 +1243,9 @@ module V82 = struct let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in { Evd.it = goals ; sigma=solution; } - let top_evars initial = + let top_evars initial { solution=sigma; } = let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c)) + Evar.Set.elements (Evd.evars_of_term sigma c) in CList.flatten (CList.map evars_of_initial initial) diff --git a/engine/proofview.mli b/engine/proofview.mli index 92f8b86df5..f90f02f3e1 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -24,7 +24,7 @@ type proofview ide-s. *) (* spiwack: the type of [proofview] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: returns the list of focused goals together with the [evar_map] context. *) val proofview : proofview -> Evar.t list * Evd.evar_map @@ -95,7 +95,7 @@ type focus_context instance, ide-s. *) (* spiwack: the type of [focus_context] will change as we push more refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) + new nearly identical function every time. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) val focus_context : focus_context -> Evar.t list * Evar.t list @@ -381,7 +381,7 @@ val tclENV : Environ.env tactic (** {7 Put-like primitives} *) (** [tclEFFECTS eff] add the effects [eff] to the current state. *) -val tclEFFECTS : Safe_typing.private_constants -> unit tactic +val tclEFFECTS : Evd.side_effects -> unit tactic (** [mark_as_unsafe] declares the current tactic is unsafe. *) val mark_as_unsafe : unit tactic @@ -595,7 +595,7 @@ module V82 : sig val top_goals : entry -> proofview -> Evar.t list Evd.sigma (* returns the existential variable used to start the proof *) - val top_evars : entry -> Evar.t list + val top_evars : entry -> proofview -> Evar.t list (* Caution: this function loses quite a bit of information. It should be avoided as much as possible. It should work as diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index 80eb9d0124..37f6b5e352 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -252,7 +252,7 @@ module Giveup : Writer with type t = goal list = struct let put gs = Logical.put (true, gs) end -(** Lens and utilies pertaining to the info trace *) +(** Lens and utilities pertaining to the info trace *) module InfoL = struct let recording = Logical.(map (fun {P.trace} -> trace) current) let if_recording t = diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index 3437b6ce77..342bfa2806 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -145,7 +145,7 @@ module Shelf : State with type t = goal list of the tactic. *) module Giveup : Writer with type t = goal list -(** Lens and utilies pertaining to the info trace *) +(** Lens and utilities pertaining to the info trace *) module InfoL : sig (** [record_trace t] behaves like [t] and compute its [info] trace. *) val record_trace : 'a Logical.t -> 'a Logical.t diff --git a/engine/termops.ml b/engine/termops.ml index 8a6bd17948..1ed2d93b3c 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -187,7 +187,7 @@ let compute_evar_dependency_graph sigma = in match evar_body evi with | Evar_empty -> acc - | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc + | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term sigma c) acc in Evd.fold fold sigma EvMap.empty @@ -306,9 +306,15 @@ let pr_evar_map_gen with_univs pr_evars env sigma = let pr_evar_list env sigma l = let open Evd in + let pr_restrict ev = + match is_restricted_evar sigma ev with + | None -> mt () + | Some ev' -> str " (restricted to " ++ Evar.print ev' ++ str ")" + in let pr (ev, evi) = h 0 (Evar.print ev ++ str "==" ++ pr_evar_info env sigma evi ++ + pr_restrict ev ++ (if evi.evar_body == Evar_empty then str " {" ++ pr_existential_key sigma ev ++ str "}" else mt ())) diff --git a/engine/termops.mli b/engine/termops.mli index a9217b3586..f970b9ece0 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/uState.ml b/engine/uState.ml index 9b27ff7916..5ed016e0d0 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -453,9 +453,9 @@ let restrict ctx vars = let uctx' = restrict_universe_context ctx.uctx_local vars in { ctx with uctx_local = uctx' } -let demote_seff_univs entry uctx = +let demote_seff_univs universes uctx = let open Entries in - match entry.const_entry_universes with + match universes with | Polymorphic_entry _ -> uctx | Monomorphic_entry (univs, _) -> let seff = LSet.union uctx.uctx_seff_univs univs in diff --git a/engine/uState.mli b/engine/uState.mli index 3df7f9e8e9..9689f2e961 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -100,7 +100,7 @@ val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t universes are preserved. *) val restrict : t -> Univ.LSet.t -> t -val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t +val demote_seff_univs : Entries.universes_entry -> t -> t type rigid = | UnivRigid diff --git a/engine/univGen.ml b/engine/univGen.ml index f1deb1bfaf..a347bba188 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/univGen.mli b/engine/univGen.mli index 34920e5620..1c8735bfa8 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/univMinim.ml b/engine/univMinim.ml index fcbf305f9d..1b7c33b9c1 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -353,7 +353,7 @@ let normalize_context_set g ctx us algs weak = noneqs Constraint.empty in (* Compute the left and right set of flexible variables, constraints - mentionning other variables remain in noneqs. *) + mentioning other variables remain in noneqs. *) let noneqs, ucstrsl, ucstrsr = Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> let lus = LMap.mem l us and rus = LMap.mem r us in diff --git a/engine/univMinim.mli b/engine/univMinim.mli index 9f80b7acbc..21f6efe86a 100644 --- a/engine/univMinim.mli +++ b/engine/univMinim.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/univNames.ml b/engine/univNames.ml index 7e6ed5e4c0..887191f9b7 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/univNames.mli b/engine/univNames.mli index e9c517babf..ebb665c4fd 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/univProblem.ml b/engine/univProblem.ml index bc2edc13de..07cde25564 100644 --- a/engine/univProblem.ml +++ b/engine/univProblem.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/univProblem.mli b/engine/univProblem.mli index ffaebe15ab..68c5d4cd5e 100644 --- a/engine/univProblem.mli +++ b/engine/univProblem.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/univSubst.ml b/engine/univSubst.ml index 2f59a3fa85..737eb83a3d 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/univSubst.mli b/engine/univSubst.mli index e76d253336..fc10a694e9 100644 --- a/engine/univSubst.mli +++ b/engine/univSubst.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/univops.ml b/engine/univops.ml index 53c42023ad..92f69317fd 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/engine/univops.mli b/engine/univops.mli index 597d2d6785..6cc7868a38 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) |