diff options
Diffstat (limited to 'engine')
36 files changed, 328 insertions, 447 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 96beb72a56..c946125d3f 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 *) @@ -26,24 +26,7 @@ let safe_evar_value sigma ev = try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None -(** Combinators *) - -let evd_comb0 f evdref = - let (evd',x) = f !evdref in - evdref := evd'; - x - -let evd_comb1 f evdref x = - let (evd',y) = f !evdref x in - evdref := evd'; - y - -let evd_comb2 f evdref x y = - let (evd',z) = f !evdref x y in - evdref := evd'; - z - -let new_global evd x = +let new_global evd x = let (evd, c) = Evd.fresh_global (Global.env()) evd x in (evd, c) @@ -348,11 +331,16 @@ let push_rel_decl_to_named_context let map_decl f d = NamedDecl.map_constr f d in - let replace_var_named_declaration id0 id decl = - let id' = NamedDecl.get_id decl in - let id' = if Id.equal id0 id' then id else id' in - let vsubst = [id0 , mkVar id] in - decl |> NamedDecl.set_id id' |> map_decl (replace_vars vsubst) + let rec replace_var_named_declaration id0 id = function + | [] -> [] + | decl :: nc -> + if Id.equal id0 (NamedDecl.get_id decl) then + (* Stop here, the variable cannot occur before its definition *) + (NamedDecl.set_id id decl) :: nc + else + let nc = replace_var_named_declaration id0 id nc in + let vsubst = [id0 , mkVar id] in + map_decl (fun c -> replace_vars vsubst c) decl :: nc in let extract_if_neq id = function | Anonymous -> None @@ -383,7 +371,7 @@ let push_rel_decl_to_named_context context. Unless [id] is a section variable. *) let subst = update_var id0 id subst in let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in - let nc = List.map (replace_var_named_declaration id0 id) nc in + let nc = replace_var_named_declaration id0 id nc in (push_var id0 subst, Id.Set.add id avoid, d :: nc) | Some id0 when hypnaming = FailIfConflict -> user_err Pp.(Id.print id0 ++ str " is already used.") @@ -673,26 +661,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 @@ -812,7 +800,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 @@ -873,12 +861,12 @@ let compare_constructor_instances evd u u' = in Evd.add_universe_constraints evd soft -(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and - [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]. *) -let eq_constr_univs_test sigma1 sigma2 t u = +(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of + [t] and [u] up to existential variable instantiation and + equalisable universes. The term [t] is interpreted in [evd] while + [u] is interpreted in [extended_evd]. The universe constraints in + [extended_evd] are assumed to be an extension of those in [evd]. *) +let eq_constr_univs_test ~evd ~extended_evd t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in let t = EConstr.Unsafe.to_constr t @@ -889,8 +877,8 @@ let eq_constr_univs_test sigma1 sigma2 t u = in let ans = UnivProblem.eq_constr_univs_infer_with - (fun t -> kind_of_term_upto sigma1 t) - (fun u -> kind_of_term_upto sigma2 u) - (universes sigma2) fold t u sigma2 + (fun t -> kind_of_term_upto evd t) + (fun u -> kind_of_term_upto extended_evd u) + (universes extended_evd) fold t u extended_evd in match ans with None -> false | Some _ -> true diff --git a/engine/evarutil.mli b/engine/evarutil.mli index bb0da44103..7877b94582 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 *) @@ -204,12 +204,17 @@ val finalize : ?abort_on_undefined_evars:bool -> evar_map -> val kind_of_term_upto : evar_map -> Constr.constr -> (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term -(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and - [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]. *) -val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool +(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of + [t] and [u] up to existential variable instantiation and + equalisable universes. The term [t] is interpreted in [evd] while + [u] is interpreted in [extended_evd]. The universe constraints in + [extended_evd] are assumed to be an extension of those in [evd]. *) +val eq_constr_univs_test : + evd:Evd.evar_map -> + extended_evd:Evd.evar_map -> + constr -> + constr -> + bool (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns [Inl sigma'] where [sigma'] is [sigma] augmented with universe @@ -274,15 +279,6 @@ val push_rel_context_to_named_context : ?hypnaming:naming_mode -> val generalize_evar_over_rels : evar_map -> existential -> types * constr list -(** Evar combinators *) - -val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a -[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"] -val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a -[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"] -val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a -[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"] - val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located diff --git a/engine/evd.ml b/engine/evd.ml index b89222cf8e..6a721a1a8a 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; @@ -689,7 +702,7 @@ let empty = { } let from_env e = - { empty with universes = UState.make (Environ.universes e) } + { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) } let from_ctx ctx = { empty with universes = ctx } @@ -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 *) @@ -869,8 +855,6 @@ let to_universe_context evd = UState.context evd.universes let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes -let const_univ_entry = univ_entry - let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl let restrict_universe_context evd vars = @@ -1040,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 @@ -1406,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 b0fcddb068..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 @@ -615,9 +626,6 @@ val to_universe_context : evar_map -> Univ.UContext.t val univ_entry : poly:bool -> evar_map -> Entries.universes_entry -val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry -[@@ocaml.deprecated "Use [univ_entry]."] - val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry val merge_universe_context : evar_map -> UState.t -> evar_map diff --git a/engine/ftactic.ml b/engine/ftactic.ml index ac0344148a..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) @@ -56,13 +56,6 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l) -let nf_enter f = - bind goals - (fun gl -> - gl >>= fun gl -> - Proofview.Goal.normalize gl >>= fun nfgl -> - Proofview.V82.wrap_exceptions (fun () -> f nfgl)) [@warning "-3"] - let enter f = bind goals (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) diff --git a/engine/ftactic.mli b/engine/ftactic.mli index 3c4fa6f4e8..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,23 +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} *) -val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t -[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"] - -(** 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..3c383b2e00 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 *) @@ -30,7 +30,7 @@ exception Exception of exn (** This exception is used to signal abortion in [timeout] functions. *) -exception Timeout +exception Tac_Timeout (** This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system @@ -38,10 +38,9 @@ exception Timeout exception TacticFailure of exn let _ = CErrors.register_handler begin function - | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!") | Exception e -> CErrors.print e | TacticFailure e -> CErrors.print e - | _ -> Pervasives.raise CErrors.Unhandled + | _ -> raise CErrors.Unhandled end (** {6 Non-logical layer} *) @@ -70,11 +69,11 @@ struct let map f a = (); fun () -> f (a ()) end) - type 'a ref = 'a Pervasives.ref + type 'a ref = 'a Util.pervasives_ref let ignore a = (); fun () -> ignore (a ()) - let ref a = (); fun () -> Pervasives.ref a + let ref a = (); fun () -> ref a (** [Pervasives.(:=)] *) let (:=) r a = (); fun () -> r := a @@ -93,13 +92,13 @@ struct let (src, info) = CErrors.push src in h (e, info) () - let read_line = fun () -> try Pervasives.read_line () with e -> + let read_line = fun () -> try read_line () with e -> let (e, info) = CErrors.push e in raise ~info e () let print_char = fun c -> (); fun () -> print_char c let timeout = fun n t -> (); fun () -> - Control.timeout n t () (Exception Timeout) + Control.timeout n t () (Exception Tac_Timeout) let make f = (); fun () -> try f () @@ -108,7 +107,7 @@ struct Util.iraise (Exception e, info) (** Use the current logger. The buffer is also flushed. *) - let print_debug s = make (fun _ -> Feedback.msg_info s) + let print_debug s = make (fun _ -> Feedback.msg_debug s) let print_info s = make (fun _ -> Feedback.msg_info s) let print_warning s = make (fun _ -> Feedback.msg_warning s) let print_notice s = make (fun _ -> Feedback.msg_notice s) @@ -151,7 +150,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..75920455ce 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 *) @@ -30,7 +30,7 @@ exception Exception of exn (** This exception is used to signal abortion in [timeout] functions. *) -exception Timeout +exception Tac_Timeout (** This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system diff --git a/engine/namegen.ml b/engine/namegen.ml index 10ece55a63..89c2fade62 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 *) @@ -24,7 +24,6 @@ open EConstr open Vars open Nameops open Libnames -open Globnames open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -72,7 +71,7 @@ let is_imported_modpath = function in find_prefix (Lib.current_mp ()) | _ -> false -let is_imported_ref = function +let is_imported_ref = let open GlobRef in function | VarRef _ -> false | IndRef (kn,_) | ConstructRef ((kn,_),_) -> @@ -90,7 +89,7 @@ let is_global id = let is_constructor id = try match Nametab.locate (qualid_of_ident id) with - | ConstructRef _ -> true + | GlobRef.ConstructRef _ -> true | _ -> false with Not_found -> false @@ -102,7 +101,7 @@ let is_section_variable id = (**********************************************************************) (* Generating "intuitive" names from its type *) -let global_of_constr = function +let global_of_constr = let open GlobRef in function | Const (c, _) -> ConstRef c | Ind (i, _) -> IndRef i | Construct (c, _) -> ConstructRef c @@ -149,8 +148,8 @@ let hdchar env sigma c = | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn))) | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn)) - | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") - | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.IndRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") | Var id -> lowercase_first_char id | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> 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 316f02bc37..1f076470c1 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.(>>) @@ -345,29 +345,19 @@ let tclBREAK = Proof.break exception NoSuchGoals of int -(* This hook returns a string to be appended to the usual message. - Primarily used to add a suggestion about the right bullet to use to - focus the next goal, if applicable. *) -let nosuchgoals_hook:(int -> Pp.t) ref = ref (fun n -> mt ()) -let set_nosuchgoals_hook f = nosuchgoals_hook := f - - - -(* This uses the hook above *) let _ = CErrors.register_handler begin function | NoSuchGoals n -> - let suffix = !nosuchgoals_hook n in - CErrors.user_err - (str "No such " ++ str (String.plural n "goal") ++ str "." ++ - pr_non_empty_arg (fun x -> x) suffix) - | _ -> raise CErrors.Unhandled + CErrors.user_err + (str "No such " ++ str (String.plural n "goal") ++ str ".") + | _ -> raise CErrors.Unhandled end -(** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where +(** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where only the goals numbered [i] to [j] are focused (the rest of the goals is restored at the end of the tactic). If the range [i]-[j] is not valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *) -let tclFOCUS_gen nosuchgoal i j t = +let tclFOCUS ?nosuchgoal i j t = + let nosuchgoal = Option.default (tclZERO (NoSuchGoals (j+1-i))) nosuchgoal in let open Proof in Pv.get >>= fun initial -> try @@ -378,41 +368,32 @@ let tclFOCUS_gen nosuchgoal i j t = return result with CList.IndexOutOfRange -> nosuchgoal -let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t -let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t +let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t -let tclFOCUSLIST l 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 - | [] -> tclZERO (NoSuchGoals 0) - | (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 id t = +let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t = let open Proof in Pv.get >>= fun initial -> try @@ -432,7 +413,7 @@ let tclFOCUSID id t = t >>= fun result -> Comb.set initial.comb >> return result - with Not_found -> tclZERO (NoSuchGoals 1) + with Not_found -> nosuchgoal (** {7 Dispatching on goals} *) @@ -561,7 +542,7 @@ let tclDISPATCHGEN join tacs = let tacs = CList.map branch tacs in InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs) -let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs +let tclDISPATCH tacs = tclDISPATCHGEN ignore tacs let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs @@ -652,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 @@ -868,7 +849,8 @@ let give_up = module Progress = struct - let eq_constr = Evarutil.eq_constr_univs_test + let eq_constr evd extended_evd = + Evarutil.eq_constr_univs_test ~evd ~extended_evd (** equality function on hypothesis contexts *) let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = @@ -898,10 +880,10 @@ module Progress = struct eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body (** Equality function on goals *) - let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in - eq_evar_info evars1 evars2 evi1 evi2 + let goal_equal ~evd ~extended_evd evar extended_evar = + let evi = Evd.find evd evar in + let extended_evi = Evd.find extended_evd extended_evar in + eq_evar_info evd extended_evd evi extended_evi end @@ -918,18 +900,18 @@ let tclPROGRESS t = let test = quick_test || Util.List.for_all2eq begin fun i f -> - Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f) + Progress.goal_equal ~evd:initial.solution + ~extended_evd:final.solution (drop_state i) (drop_state f) end initial.comb final.comb in if not test then tclUNIT res else - tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) + tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress.")) -exception Timeout let _ = CErrors.register_handler begin function - | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") - | _ -> Pervasives.raise CErrors.Unhandled + | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | _ -> raise CErrors.Unhandled end let tclTIMEOUT n t = @@ -953,7 +935,8 @@ let tclTIMEOUT n t = end begin let open Logic_monad.NonLogical in function (e, info) -> match e with - | Logic_monad.Timeout -> return (Util.Inr (Timeout, info)) + | Logic_monad.Tac_Timeout -> + return (Util.Inr (Logic_monad.Tac_Timeout, info)) | Logic_monad.TacticFailure e -> return (Util.Inr (e, info)) | e -> Logic_monad.NonLogical.raise ~info e @@ -1115,13 +1098,6 @@ module Goal = struct tclZERO ~info e end end - - let normalize { self; state } = - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in - tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl) - let gmake env sigma goal = let state = get_state goal in let goal = drop_state goal in @@ -1269,9 +1245,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 c772525c86..764a4a0058 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 @@ -244,15 +244,12 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic (** [tclFOCUS i j t] applies [t] after focusing on the goals number [i] to [j] (see {!focus}). The rest of the goals is restored after the tactic action. If the specified range doesn't correspond to - existing goals, fails with [NoSuchGoals] (a user error). this - exception is caught at toplevel with a default message + a hook - message that can be customized by [set_nosuchgoals_hook] below. - This hook is used to add a suggestion about bullets when - applicable. *) + existing goals, fails with the [nosuchgoal] argument, by default + raising [NoSuchGoals] (a user error). This exception is caught at + toplevel with a default message. *) exception NoSuchGoals of int -val set_nosuchgoals_hook: (int -> Pp.t) -> unit -val tclFOCUS : int -> int -> 'a tactic -> 'a tactic +val tclFOCUS : ?nosuchgoal:'a tactic -> int -> int -> 'a tactic -> 'a tactic (** [tclFOCUSLIST li t] applies [t] on the list of focused goals described by [li]. Each element of [li] is a pair [(i, j)] denoting @@ -261,13 +258,14 @@ val tclFOCUS : int -> int -> 'a tactic -> 'a tactic intervals. If the set of such goals is not a single range, then it will move goals such that it is a single range. (So, for instance, [[1, 3-5]; idtac.] is not the identity.) - If the set of such goals is empty, it will fail. *) -val tclFOCUSLIST : (int * int) list -> 'a tactic -> 'a tactic + If the set of such goals is empty, it will fail with [nosuchgoal], + by default raising [NoSuchGoals 0]. *) +val tclFOCUSLIST : ?nosuchgoal:'a tactic -> (int * int) list -> 'a tactic -> 'a tactic (** [tclFOCUSID x t] applies [t] on a (single) focused goal like {!tclFOCUS}. The goal is found by its name rather than its - number.*) -val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic + number. Fails with [nosuchgoal], by default raising [NoSuchGoals 1]. *) +val tclFOCUSID : ?nosuchgoal:'a tactic -> Names.Id.t -> 'a tactic -> 'a tactic (** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the specified range doesn't correspond to existing goals, behaves like @@ -383,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 @@ -400,14 +398,23 @@ val give_up : unit tactic val tclPROGRESS : 'a tactic -> 'a tactic module Progress : sig - val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool +(** [goal_equal ~evd ~extended_evd evar extended_evar] tests whether + the [evar_info] from [evd] corresponding to [evar] is equal to that + from [extended_evd] corresponding to [extended_evar], up to + existential variable instantiation and equalisable universes. The + universe constraints in [extended_evd] are assumed to be an + extension of the universe constraints in [evd]. *) + val goal_equal : + evd:Evd.evar_map -> + extended_evd:Evd.evar_map -> + Evar.t -> + Evar.t -> + bool end (** Checks for interrupts *) val tclCHECKINTERRUPT : unit tactic -exception Timeout - (** [tclTIMEOUT n t] can have only one success. In case of timeout if fails with [tclZERO Timeout]. *) val tclTIMEOUT : int -> 'a tactic -> 'a tactic @@ -507,10 +514,6 @@ module Goal : sig (** Type of goals. *) type t - (** Normalises the argument goal. *) - val normalize : t -> t tactic - [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"] - (** [concl], [hyps], [env] and [sigma] given a goal [gl] return respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the @@ -601,7 +604,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 8e12c9be88..2ab2f60421 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 *) @@ -25,11 +25,6 @@ module CompactedDecl = Context.Compacted.Declaration module Internal = struct -let pr_sort_family = Sorts.pr_sort_family -[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"] -let pr_fix = Constr.debug_print_fix -[@@ocaml.deprecated "Use [Constr.debug_print_fix]"] - let debug_print_constr c = Constr.debug_print EConstr.Unsafe.(to_constr c) let debug_print_constr_env env sigma c = Constr.debug_print EConstr.(to_constr sigma c) let term_printer = ref debug_print_constr_env @@ -192,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 @@ -311,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 ())) @@ -761,13 +762,6 @@ let fold_constr_with_binders sigma g f n acc c = let c = Unsafe.to_constr (whd_evar sigma c) in Constr.fold_constr_with_binders g f n acc c -(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate - subterms of [c]; it carries an extra data [acc] which is processed by [g] at - each binder traversal; it is not recursive and the order with which - subterms are processed is not specified *) - -let iter_constr_with_full_binders = EConstr.iter_with_full_binders - (***************************) (* occurs check functions *) (***************************) @@ -862,8 +856,6 @@ let collect_vars sigma c = | _ -> EConstr.fold sigma aux vars c in aux Id.Set.empty c -let vars_of_global_reference = vars_of_global - (* Tests whether [m] is a subterm of [t]: [m] is appropriately lifted through abstractions of [t] *) @@ -1066,7 +1058,7 @@ let is_section_variable id = with Not_found -> false let global_of_constr sigma c = - let open Globnames in + let open GlobRef in match EConstr.kind sigma c with | Const (c, u) -> ConstRef c, u | Ind (i, u) -> IndRef i, u @@ -1075,7 +1067,7 @@ let global_of_constr sigma c = | _ -> raise Not_found let is_global sigma c t = - let open Globnames in + let open GlobRef in match c, EConstr.kind sigma t with | ConstRef c, Const (c', _) -> Constant.equal c c' | IndRef i, Ind (i', _) -> eq_ind i i' @@ -1387,7 +1379,7 @@ let dependency_closure env sigma sign hyps = List.rev lh let global_app_of_constr sigma c = - let open Globnames in + let open GlobRef in match EConstr.kind sigma c with | Const (c, u) -> (ConstRef c, u), None | Ind (i, u) -> (IndRef i, u), None @@ -1417,10 +1409,6 @@ let prod_applist_assum sigma n c l = | _ -> anomaly (Pp.str "Not enough prod/let's.") in app n [] c l -let on_judgment = Environ.on_judgment -let on_judgment_value = Environ.on_judgment_value -let on_judgment_type = Environ.on_judgment_type - (* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in variables skips let-in's; let-in's in the middle are put in ctx2 *) let context_chop k ctx = diff --git a/engine/termops.mli b/engine/termops.mli index 1dd9941c5e..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 *) @@ -16,12 +16,6 @@ open Constr open Environ open EConstr -(** printers *) -val pr_sort_family : Sorts.family -> Pp.t -[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"] -val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t -[@@ocaml.deprecated "Use [Constr.debug_print_fix]"] - (** about contexts *) val push_rel_assum : Name.t Context.binder_annot * types -> env -> env val push_rels_assum : (Name.t Context.binder_annot * Constr.types) list -> env -> env @@ -84,12 +78,6 @@ val fold_constr_with_full_binders : Evd.evar_map -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -val iter_constr_with_full_binders : Evd.evar_map -> - (rel_declaration -> 'a -> 'a) -> - ('a -> constr -> unit) -> 'a -> - constr -> unit -[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."] - (**********************************************************************) val strip_head_cast : Evd.evar_map -> constr -> constr @@ -121,9 +109,6 @@ val count_occurrences : Evd.evar_map -> constr -> constr -> int val collect_metas : Evd.evar_map -> constr -> int list val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *) -val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t -[@@ocaml.deprecated "Use [Environ.vars_of_global]"] - (* Substitution of metavariables *) type meta_value_map = (metavariable * Constr.constr) list val subst_meta : meta_value_map -> Constr.constr -> Constr.constr @@ -292,15 +277,6 @@ val is_Type : Evd.evar_map -> constr -> bool val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option -(** Combinators on judgments *) - -val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment -[@@ocaml.deprecated "Use [Environ.on_judgment]."] -val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment -[@@ocaml.deprecated "Use [Environ.on_judgment_value]."] -val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment -[@@ocaml.deprecated "Use [Environ.on_judgment_type]."] - (** {5 Debug pretty-printers} *) open Evd diff --git a/engine/uState.ml b/engine/uState.ml index 6f4f40e2c5..d93ccafcf0 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 *) @@ -34,6 +34,7 @@ type t = (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) + uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *) uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) uctx_weak_constraints : UPairSet.t } @@ -47,6 +48,7 @@ let empty = uctx_univ_variables = LMap.empty; uctx_univ_algebraic = LSet.empty; uctx_universes = initial_sprop_cumulative; + uctx_universes_lbound = Univ.Level.set; uctx_initial_universes = initial_sprop_cumulative; uctx_weak_constraints = UPairSet.empty; } @@ -54,10 +56,12 @@ let elaboration_sprop_cumul = Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration" ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true -let make u = +let make ~lbound u = let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in - { empty with - uctx_universes = u; uctx_initial_universes = u} + { empty with + uctx_universes = u; + uctx_universes_lbound = lbound; + uctx_initial_universes = u} let is_empty ctx = ContextSet.is_empty ctx.uctx_local && @@ -83,9 +87,9 @@ let union ctx ctx' = let newus = LSet.diff newus (LMap.domain ctx.uctx_univ_variables) in let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in let declarenew g = - LSet.fold (fun u g -> UGraph.add_universe u false g) newus g + LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.uctx_universes_lbound ~strict:false g) newus g in - let names_rev = LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in + let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); uctx_local = local; uctx_seff_univs = seff; @@ -99,6 +103,7 @@ let union ctx ctx' = else let cstrsr = ContextSet.constraints ctx'.uctx_local in UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes)); + uctx_universes_lbound = ctx.uctx_universes_lbound; uctx_weak_constraints = weak} let context_set ctx = ctx.uctx_local @@ -116,8 +121,6 @@ let univ_entry ~poly uctx = Polymorphic_entry (nas, uctx) else Monomorphic_entry (context_set uctx) -let const_univ_entry = univ_entry - let of_context_set ctx = { empty with uctx_local = ctx } let subst ctx = ctx.uctx_univ_variables @@ -175,6 +178,7 @@ exception UniversesDiffer let drop_weak_constraints = ref false + let process_universe_constraints ctx cstrs = let open UnivSubst in let open UnivProblem in @@ -216,7 +220,8 @@ let process_universe_constraints ctx cstrs = | Inr l, Inl r | Inl r, Inr l -> let alg = LSet.mem l ctx.uctx_univ_algebraic in let inst = univ_level_rem l r r in - if alg then (instantiate_variable l inst vars; local) + if alg && not (LSet.mem l (Universe.levels inst)) then + (instantiate_variable l inst vars; local) else let lu = Universe.make l in if univ_level_mem l r then @@ -232,22 +237,21 @@ let process_universe_constraints ctx cstrs = else match cst with | ULe (l, r) -> - if UGraph.check_leq univs l r then - (* Keep Prop/Set <= var around if var might be instantiated by prop or set - later. *) - match Universe.level l, Universe.level r with - | Some l, Some r -> - Constraint.add (l, Le, r) local - | _ -> local - else - begin match Universe.level r with - | None -> user_err Pp.(str "Algebraic universe on the right") - | Some r' -> - if Level.is_small r' then + begin match Univ.Universe.level r with + | None -> + if UGraph.check_leq univs l r then local + else user_err Pp.(str "Algebraic universe on the right") + | Some r' -> + if Level.is_small r' then if not (Universe.is_levels l) - then + then (* l contains a +1 and r=r' small so l <= r impossible *) raise (UniverseInconsistency (Le, l, r, None)) else + if UGraph.check_leq univs l r then match Univ.Universe.level l with + | Some l -> + Univ.Constraint.add (l, Le, r') local + | None -> local + else let levels = Universe.levels l in let fold l' local = let l = Universe.make l' in @@ -256,8 +260,12 @@ let process_universe_constraints ctx cstrs = else raise (UniverseInconsistency (Le, l, r, None)) in LSet.fold fold levels local - else - enforce_leq l r local + else + match Univ.Universe.level l with + | Some l -> + Univ.Constraint.add (l, Le, r') local + | None -> + if UGraph.check_leq univs l r then local else enforce_leq l r local end | ULub (l, r) -> equalize_variables true (Universe.make l) l (Universe.make r) r local @@ -432,18 +440,19 @@ let check_univ_decl ~poly uctx decl = (ContextSet.constraints uctx.uctx_local); ctx -let restrict_universe_context (univs, csts) keep = +let restrict_universe_context ~lbound (univs, csts) keep = let removed = LSet.diff univs keep in if LSet.is_empty removed then univs, csts else let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in let g = UGraph.initial_universes in - let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in + let g = LSet.fold (fun v g -> if Level.is_small v then g else + UGraph.add_universe v ~lbound ~strict:false g) allunivs g in let g = UGraph.merge_constraints csts g in let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in let csts = UGraph.constraints_for ~kept:allkept g in let csts = Constraint.filter (fun (l,d,r) -> - not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in + not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in (LSet.inter univs keep, csts) let restrict ctx vars = @@ -451,12 +460,12 @@ let restrict ctx vars = let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars) (fst ctx.uctx_names) vars in - let uctx' = restrict_universe_context ctx.uctx_local vars in + let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound 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 @@ -498,7 +507,7 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' = else ContextSet.append ctx' uctx.uctx_local in let declare g = LSet.fold (fun u g -> - try UGraph.add_universe u false g + try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g with UGraph.AlreadyDeclared when sideff -> g) levels g in @@ -545,16 +554,17 @@ let new_univ_variable ?loc rigid name | None -> add_uctx_loc u loc uctx.uctx_names in let initial = - UGraph.add_universe u false uctx.uctx_initial_universes + UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u uctx.uctx_initial_universes in let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = UGraph.add_universe u false uctx.uctx_universes; + uctx_universes = UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false + u uctx.uctx_universes; uctx_initial_universes = initial} in uctx', u -let make_with_initial_binders e us = - let uctx = make e in +let make_with_initial_binders ~lbound e us = + let uctx = make ~lbound e in List.fold_left (fun uctx { CAst.loc; v = id } -> fst (new_univ_variable ?loc univ_rigid (Some id) uctx)) @@ -562,10 +572,10 @@ let make_with_initial_binders e us = let add_global_univ uctx u = let initial = - UGraph.add_universe u true uctx.uctx_initial_universes + UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes in let univs = - UGraph.add_universe u true uctx.uctx_universes + UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes in { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local; uctx_initial_universes = initial; @@ -680,8 +690,9 @@ let refresh_undefined_univ_variables uctx = uctx.uctx_univ_variables LMap.empty in let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in - let declare g = LSet.fold (fun u g -> UGraph.add_universe u false g) - (ContextSet.levels ctx') g in + let lbound = uctx.uctx_universes_lbound in + let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g) + (ContextSet.levels ctx') g in let initial = declare uctx.uctx_initial_universes in let univs = declare UGraph.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; @@ -689,14 +700,16 @@ let refresh_undefined_univ_variables uctx = uctx_seff_univs = uctx.uctx_seff_univs; uctx_univ_variables = vars; uctx_univ_algebraic = alg; uctx_universes = univs; + uctx_universes_lbound = lbound; uctx_initial_universes = initial; uctx_weak_constraints = weak; } in uctx', subst let minimize uctx = let open UnivMinim in + let lbound = uctx.uctx_universes_lbound in let ((vars',algs'), us') = - normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables + normalize_context_set ~lbound uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic uctx.uctx_weak_constraints in if ContextSet.equal us' uctx.uctx_local then uctx @@ -710,6 +723,7 @@ let minimize uctx = uctx_univ_variables = vars'; uctx_univ_algebraic = algs'; uctx_universes = universes; + uctx_universes_lbound = lbound; uctx_initial_universes = uctx.uctx_initial_universes; uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) } diff --git a/engine/uState.mli b/engine/uState.mli index a358813825..52e48c4eeb 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 *) @@ -25,9 +25,9 @@ type t val empty : t -val make : UGraph.t -> t +val make : lbound:Univ.Level.t -> UGraph.t -> t -val make_with_initial_binders : UGraph.t -> lident list -> t +val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t val is_empty : t -> bool @@ -67,9 +67,6 @@ val context : t -> Univ.UContext.t val univ_entry : poly:bool -> t -> Entries.universes_entry (** Pick from {!context} or {!context_set} based on [poly]. *) -val const_univ_entry : poly:bool -> t -> Entries.universes_entry -[@@ocaml.deprecated "Use [univ_entry]."] - (** {5 Constraints handling} *) val drop_weak_constraints : bool ref @@ -91,11 +88,11 @@ val universe_of_name : t -> Id.t -> Univ.Level.t (** {5 Unification} *) -(** [restrict_universe_context (univs,csts) keep] restricts [univs] to +(** [restrict_universe_context lbound (univs,csts) keep] restricts [univs] to the universes in [keep]. The constraints [csts] are adjusted so that transitive constraints between remaining universes (those in [keep] and those not in [univs]) are preserved. *) -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t (** [restrict uctx ctx] restricts the local universes of [uctx] to [ctx] extended by local named universes and side effect universes @@ -103,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 c310331b15..b1ed3b2694 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 *) @@ -25,11 +25,6 @@ let new_univ_global () = let fresh_level () = Univ.Level.make (new_univ_global ()) -(* TODO: remove *) -let new_univ () = Univ.Universe.make (fresh_level ()) -let new_Type () = mkType (new_univ ()) -let new_Type_sort () = sort_of_univ (new_univ ()) - let fresh_instance auctx = let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in let ctx = Array.fold_right LSet.add inst LSet.empty in @@ -61,15 +56,15 @@ let fresh_global_instance ?loc ?names env gr = u, ctx let fresh_constant_instance env c = - let u, ctx = fresh_global_instance env (ConstRef c) in + let u, ctx = fresh_global_instance env (GlobRef.ConstRef c) in (c, u), ctx let fresh_inductive_instance env ind = - let u, ctx = fresh_global_instance env (IndRef ind) in + let u, ctx = fresh_global_instance env (GlobRef.IndRef ind) in (ind, u), ctx let fresh_constructor_instance env c = - let u, ctx = fresh_global_instance env (ConstructRef c) in + let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in (c, u), ctx let fresh_global_instance ?loc ?names env gr = @@ -83,50 +78,18 @@ let constr_of_monomorphic_global gr = Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ str " would forget universes.") -let constr_of_global gr = constr_of_monomorphic_global gr - -let constr_of_global_univ = mkRef - let fresh_global_or_constr_instance env = function | IsConstr c -> c, ContextSet.empty | IsGlobal gr -> fresh_global_instance env gr let global_of_constr c = match kind c with - | Const (c, u) -> ConstRef c, u - | Ind (i, u) -> IndRef i, u - | Construct (c, u) -> ConstructRef c, u - | Var id -> VarRef id, Instance.empty + | Const (c, u) -> GlobRef.ConstRef c, u + | Ind (i, u) -> GlobRef.IndRef i, u + | Construct (c, u) -> GlobRef.ConstructRef c, u + | Var id -> GlobRef.VarRef id, Instance.empty | _ -> raise Not_found -open Declarations - -let type_of_reference env r = - match r with - | VarRef id -> Environ.named_type id env, ContextSet.empty - - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let ty = cb.const_type in - let auctx = Declareops.constant_polymorphic_context cb in - let inst, ctx = fresh_instance auctx in - Vars.subst_instance_constr inst ty, ctx - - | IndRef ind -> - let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in - let auctx = Declareops.inductive_polymorphic_context mib in - let inst, ctx = fresh_instance auctx in - let ty = Inductive.type_of_inductive env (specif, inst) in - ty, ctx - - | ConstructRef (ind,_ as cstr) -> - let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let auctx = Declareops.inductive_polymorphic_context mib in - let inst, ctx = fresh_instance auctx in - Inductive.type_of_constructor (cstr,inst) specif, ctx - -let type_of_global t = type_of_reference (Global.env ()) t - let fresh_sort_in_family = function | InSProp -> Sorts.sprop, ContextSet.empty | InProp -> Sorts.prop, ContextSet.empty @@ -135,11 +98,6 @@ let fresh_sort_in_family = function let u = fresh_level () in sort_of_univ (Univ.Universe.make u), ContextSet.singleton u -let new_sort_in_family sf = - fst (fresh_sort_in_family sf) - -let extend_context = Univ.extend_in_context_set - let new_global_univ () = let u = fresh_level () in (Univ.Universe.make u, ContextSet.singleton u) diff --git a/engine/univGen.mli b/engine/univGen.mli index b4598e10d0..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 *) @@ -24,16 +24,7 @@ val new_univ_id : unit -> univ_unique_id (** for the stm *) val new_univ_global : unit -> Level.UGlobal.t val fresh_level : unit -> Level.t -val new_univ : unit -> Universe.t -[@@ocaml.deprecated "Use [new_univ_level]"] -val new_Type : unit -> types -[@@ocaml.deprecated "Use [new_univ_level]"] -val new_Type_sort : unit -> Sorts.t -[@@ocaml.deprecated "Use [new_univ_level]"] - val new_global_univ : unit -> Universe.t in_universe_context_set -val new_sort_in_family : Sorts.family -> Sorts.t -[@@ocaml.deprecated "Use [fresh_sort_in_family]"] (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) @@ -66,27 +57,9 @@ val fresh_universe_context_set_instance : ContextSet.t -> (** Raises [Not_found] if not a global reference. *) val global_of_constr : constr -> GlobRef.t puniverses -val constr_of_global_univ : GlobRef.t puniverses -> constr -[@@ocaml.deprecated "Use [Constr.mkRef]"] - -val extend_context : 'a in_universe_context_set -> ContextSet.t -> - 'a in_universe_context_set -[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"] - (** Create a fresh global in the global environment, without side effects. BEWARE: this raises an error on polymorphic constants/inductives: the constraints should be properly added to an evd. See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for the proper way to get a fresh copy of a polymorphic global reference. *) val constr_of_monomorphic_global : GlobRef.t -> constr - -val constr_of_global : GlobRef.t -> constr -[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\ - use [constr_of_monomorphic_global] if the reference is guaranteed to\ - be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"] - -(** Returns the type of the global reference, by creating a fresh instance of polymorphic - references and computing their instantiated universe context. (side-effect on the - universe counter, use with care). *) -val type_of_global : GlobRef.t -> types in_universe_context_set -[@@ocaml.deprecated "use [Typeops.type_of_global]"] diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 46ff6340b4..30fdd28997 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 *) @@ -203,7 +203,7 @@ let minimize_univ_variables ctx us algs left right cstrs = (acc, [], LMap.empty, LMap.empty) l in let left = CList.uniquize (List.filter (not_lower lower) left) in - (acc, left, LMap.union newlow lower) + (acc, left, LMap.lunion newlow lower) in let instantiate_lbound lbound = let alg = LSet.mem u algs in @@ -269,11 +269,11 @@ module UPairs = OrderedType.UnorderedPair(Univ.Level) module UPairSet = Set.Make (UPairs) (* TODO check is_small/sprop *) -let normalize_context_set g ctx us algs weak = +let normalize_context_set ~lbound g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in (* Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = - Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts + Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts in let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles @@ -282,12 +282,12 @@ let normalize_context_set g ctx us algs weak = let csts, partition = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = LSet.fold (fun v g -> UGraph.add_universe v false g) + let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) ctx UGraph.initial_universes in let add_soft u g = if not (Level.is_small u || LSet.mem u ctx) - then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g + then try UGraph.add_universe ~lbound ~strict:false u g with UGraph.AlreadyDeclared -> g else g in let g = Constraint.fold @@ -300,7 +300,7 @@ let normalize_context_set g ctx us algs weak = (* We ignore the trivial Prop/Set <= i constraints. *) let noneqs = Constraint.filter - (fun (l,d,r) -> not ((d == Le && Level.is_small l) || + (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in @@ -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..72b432e62f 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 *) @@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t) (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -val normalize_context_set : UGraph.t -> ContextSet.t -> +val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t -> universe_opt_subst (* The defined and undefined variables *) -> LSet.t (* univ variables that can be substituted by algebraics *) -> UPairSet.t (* weak equality constraints *) -> 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..1f1edbed16 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 *) @@ -15,5 +15,5 @@ open Univ val universes_of_constr : constr -> LSet.t [@@ocaml.deprecated "Use [Vars.universes_of_constr]"] -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t [@@ocaml.deprecated "Use [UState.restrict_universe_context]"] |