diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 155 | ||||
| -rw-r--r-- | engine/eConstr.mli | 22 | ||||
| -rw-r--r-- | engine/evarutil.ml | 43 | ||||
| -rw-r--r-- | engine/evarutil.mli | 24 | ||||
| -rw-r--r-- | engine/evd.ml | 167 | ||||
| -rw-r--r-- | engine/evd.mli | 69 | ||||
| -rw-r--r-- | engine/ftactic.ml | 10 | ||||
| -rw-r--r-- | engine/ftactic.mli | 14 | ||||
| -rw-r--r-- | engine/logic_monad.ml | 10 | ||||
| -rw-r--r-- | engine/logic_monad.mli | 10 | ||||
| -rw-r--r-- | engine/namegen.ml | 67 | ||||
| -rw-r--r-- | engine/namegen.mli | 17 | ||||
| -rw-r--r-- | engine/nameops.ml | 10 | ||||
| -rw-r--r-- | engine/nameops.mli | 10 | ||||
| -rw-r--r-- | engine/proofview.ml | 174 | ||||
| -rw-r--r-- | engine/proofview.mli | 82 | ||||
| -rw-r--r-- | engine/proofview_monad.ml | 40 | ||||
| -rw-r--r-- | engine/proofview_monad.mli | 31 | ||||
| -rw-r--r-- | engine/termops.ml | 35 | ||||
| -rw-r--r-- | engine/termops.mli | 19 | ||||
| -rw-r--r-- | engine/uState.ml | 137 | ||||
| -rw-r--r-- | engine/uState.mli | 21 | ||||
| -rw-r--r-- | engine/universes.ml | 263 | ||||
| -rw-r--r-- | engine/universes.mli | 39 | ||||
| -rw-r--r-- | engine/univops.ml | 10 | ||||
| -rw-r--r-- | engine/univops.mli | 10 |
26 files changed, 966 insertions, 523 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 9ac16b5b48..bd47a04f1e 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -546,44 +548,111 @@ let fold sigma f acc c = match kind sigma c with | CoFix (_,(lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl -let compare_gen k eq_inst eq_sort eq_constr c1 c2 = - (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr c1 c2 +let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 = + (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2 let eq_constr sigma c1 c2 = let kind c = kind_upto sigma c in - let rec eq_constr c1 c2 = - compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal eq_constr c1 c2 + let rec eq_constr nargs c1 c2 = + compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal eq_constr nargs c1 c2 in - eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2) + eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2) let eq_constr_nounivs sigma c1 c2 = let kind c = kind_upto sigma c in - let rec eq_constr c1 c2 = - compare_gen kind (fun _ _ _ -> true) (fun _ _ -> true) eq_constr c1 c2 + let rec eq_constr nargs c1 c2 = + compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2 in - eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2) + eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2) let compare_constr sigma cmp c1 c2 = let kind c = kind_upto sigma c in - let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in - compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2) + let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in + compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2) -let test_constr_universes sigma leq m n = +let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = + let open Universes in + if not nargs_ok then enforce_eq_instances_univs false u u' cstrs + else + CArray.fold_left3 + (fun cstrs v u u' -> + let open Univ.Variance in + match v with + | Irrelevant -> Constraints.add (UWeak (u,u')) cstrs + | Covariant -> + let u = Univ.Universe.make u in + let u' = Univ.Universe.make u' in + (match cv_pb with + | Reduction.CONV -> Constraints.add (UEq (u,u')) cstrs + | Reduction.CUMUL -> Constraints.add (ULe (u,u')) cstrs) + | Invariant -> + let u = Univ.Universe.make u in + let u' = Univ.Universe.make u' in + Constraints.add (UEq (u,u')) cstrs) + cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u') + +let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs = + let open Universes in + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); + cstrs + | Declarations.Polymorphic_ind _ -> + enforce_eq_instances_univs false u1 u2 cstrs + | Declarations.Cumulative_ind cumi -> + let num_param_arity = Reduction.inductive_cumulativity_arguments spec in + let variances = Univ.ACumulativityInfo.variance cumi in + compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs + +let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = + let open Universes in + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + cstrs + | Declarations.Polymorphic_ind _ -> + enforce_eq_instances_univs false u1 u2 cstrs + | Declarations.Cumulative_ind cumi -> + let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in + if not (Int.equal num_cnstr_args nargs) + then enforce_eq_instances_univs false u1 u2 cstrs + else + Array.fold_left2 (fun cstrs u1 u2 -> Universes.(Constraints.add (UWeak (u1,u2)) cstrs)) + cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2) + +let eq_universes env sigma cstrs cv_pb ref nargs l l' = + if Univ.Instance.is_empty l then (assert (Univ.Instance.is_empty l'); true) + else + let l = Evd.normalize_universe_instance sigma l + and l' = Evd.normalize_universe_instance sigma l' in + let open Universes in + match ref with + | VarRef _ -> assert false (* variables don't have instances *) + | ConstRef _ -> + cstrs := enforce_eq_instances_univs true l l' !cstrs; true + | IndRef ind -> + let mind = Environ.lookup_mind (fst ind) env in + cstrs := cmp_inductives cv_pb (mind,snd ind) nargs l l' !cstrs; + true + | ConstructRef ((mi,ind),ctor) -> + let mind = Environ.lookup_mind mi env in + cstrs := cmp_constructors (mind,ind,ctor) nargs l l' !cstrs; + true + +let test_constr_universes env sigma leq m n = let open Universes in let kind c = kind_upto sigma c in if m == n then Some Constraints.empty - else + else let cstrs = ref Constraints.empty in - let eq_universes strict l l' = - let l = EInstance.kind sigma (EInstance.make l) in - let l' = EInstance.kind sigma (EInstance.make l') in - cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = + let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in + let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l' + and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in + let eq_sorts s1 s2 = let s1 = ESorts.kind sigma (ESorts.make s1) in let s2 = ESorts.kind sigma (ESorts.make s2) in if Sorts.equal s1 s2 then true else (cstrs := Constraints.add - (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; + (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; true) in let leq_sorts s1 s2 = @@ -592,27 +661,28 @@ let test_constr_universes sigma leq m n = if Sorts.equal s1 s2 then true else (cstrs := Constraints.add - (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; + (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; true) in - let rec eq_constr' m n = compare_gen kind eq_universes eq_sorts eq_constr' m n in + let rec eq_constr' nargs m n = compare_gen kind eq_universes eq_sorts eq_constr' nargs m n in let res = if leq then - let rec compare_leq m n = - Constr.compare_head_gen_leq_with kind kind eq_universes leq_sorts eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - compare_leq m n + let rec compare_leq nargs m n = + Constr.compare_head_gen_leq_with kind kind leq_universes leq_sorts + eq_constr' leq_constr' nargs m n + and leq_constr' nargs m n = m == n || compare_leq nargs m n in + compare_leq 0 m n else - Constr.compare_head_gen_with kind kind eq_universes eq_sorts eq_constr' m n + Constr.compare_head_gen_with kind kind eq_universes eq_sorts eq_constr' 0 m n in if res then Some !cstrs else None -let eq_constr_universes sigma m n = - test_constr_universes sigma false (unsafe_to_constr m) (unsafe_to_constr n) -let leq_constr_universes sigma m n = - test_constr_universes sigma true (unsafe_to_constr m) (unsafe_to_constr n) +let eq_constr_universes env sigma m n = + test_constr_universes env sigma false (unsafe_to_constr m) (unsafe_to_constr n) +let leq_constr_universes env sigma m n = + test_constr_universes env sigma true (unsafe_to_constr m) (unsafe_to_constr n) -let compare_head_gen_proj env sigma equ eqs eqc' m n = +let compare_head_gen_proj env sigma equ eqs eqc' nargs m n = let kind c = kind_upto sigma c in match kind_upto sigma m, kind_upto sigma n with | Proj (p, c), App (f, args) @@ -622,29 +692,28 @@ let compare_head_gen_proj env sigma equ eqs eqc' m n = let pb = Environ.lookup_projection p env in let npars = pb.Declarations.proj_npars in if Array.length args == npars + 1 then - eqc' c args.(npars) + eqc' 0 c args.(npars) else false | _ -> false) - | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' m n + | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n let eq_constr_universes_proj env sigma m n = let open Universes in if m == n then Some Constraints.empty else let cstrs = ref Constraints.empty in - let eq_universes strict l l' = - cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = + let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in + let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else (cstrs := Constraints.add - (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs; + (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs; true) in - let rec eq_constr' m n = - m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n in - let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in + let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None let universes_of_constr env sigma c = diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 6fa338c73d..28c9dd3c21 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CSig @@ -67,7 +69,10 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term val to_constr : Evd.evar_map -> t -> Constr.t -(** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *) +(** Returns the evar-normal form of the argument, and cast it as a theoretically + evar-free term. In practice this function does not check that the result + is actually evar-free, it is currently the duty of the caller to do so. + This might change in the future. *) val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type @@ -193,9 +198,12 @@ val whd_evar : Evd.evar_map -> constr -> constr val eq_constr : Evd.evar_map -> t -> t -> bool val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool -val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option -val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option +val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option +val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option + +(** [eq_constr_universes_proj] can equate projections and their eta-expanded constant form. *) val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option + val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool (** {6 Iterators} *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index f82ffccdc3..9cf81eccea 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -87,15 +89,15 @@ let nf_evars_universes evm = (Evd.universe_subst evm) let nf_evars_and_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in evm, nf_evars_universes evm let e_nf_evars_and_universes evdref = - evdref := Evd.nf_constraints !evdref; + evdref := Evd.minimize_universes !evdref; nf_evars_universes !evdref, Evd.universe_subst !evdref let nf_evar_map_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in let subst = Evd.universe_subst evm in if Univ.LMap.is_empty subst then evm, nf_evar0 evm else @@ -811,6 +813,33 @@ let subterm_source evk (loc,k) = | _ -> evk in (loc,Evar_kinds.SubEvar evk) +(* Add equality constraints for covariant/invariant positions. For + irrelevant positions, unify universes when flexible. *) +let compare_cumulative_instances cv_pb variances u u' sigma = + let open Universes in + let cstrs = Univ.Constraint.empty in + let soft = Constraints.empty in + let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' -> + let open Univ.Variance in + match v with + | Irrelevant -> cstrs, Constraints.add (UWeak (u,u')) soft + | Covariant when cv_pb == Reduction.CUMUL -> + Univ.Constraint.add (u,Univ.Le,u') cstrs, soft + | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft) + (cstrs,soft) variances (Univ.Instance.to_array u) (Univ.Instance.to_array u') + in + match Evd.add_constraints sigma cstrs with + | sigma -> + Inl (Evd.add_universe_constraints sigma soft) + | exception Univ.UniverseInconsistency p -> Inr p + +let compare_constructor_instances evd u u' = + let open Universes in + let soft = + Array.fold_left2 (fun cs u u' -> Constraints.add (UWeak (u,u')) cs) + Constraints.empty (Univ.Instance.to_array u) (Univ.Instance.to_array 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 diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 923bf49a9c..e289ca1692 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -201,6 +203,20 @@ val kind_of_term_upto : evar_map -> Constr.constr -> assumed to be an extention of those in [sigma1]. *) val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool +(** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns + [Inl sigma'] where [sigma'] is [sigma] augmented with universe + constraints such that [u1 cv_pb? u2] according to [variance]. + Additionally flexible universes in irrelevant positions are unified + if possible. Returns [Inr p] when the former is impossible. *) +val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array -> + Univ.Instance.t -> Univ.Instance.t -> evar_map -> + (evar_map, Univ.univ_inconsistency) Util.union + +(** We should only compare constructors at convertible types, so this + is only an opportunity to unify universes. *) +val compare_constructor_instances : evar_map -> + Univ.Instance.t -> Univ.Instance.t -> evar_map + (** {6 Removing hyps in evars'context} raise OccurHypInSimpleClause if the removal breaks dependencies *) diff --git a/engine/evd.ml b/engine/evd.ml index 0e94721589..f6e13e1f43 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -251,21 +253,8 @@ let instantiate_evar_array info c args = | [] -> c | _ -> replace_vars inst c -type evar_universe_context = UState.t - -type 'a in_evar_universe_context = 'a * evar_universe_context -let empty_evar_universe_context = UState.empty -let union_evar_universe_context = UState.union -let evar_universe_context_set = UState.context_set -let evar_universe_context_constraints = UState.constraints -let evar_context_universe_context = UState.context -let evar_universe_context_of = UState.of_context_set -let evar_universe_context_subst = UState.subst -let add_constraints_context = UState.add_constraints -let add_universe_constraints_context = UState.add_universe_constraints -let constrain_variables = UState.constrain_variables -let evar_universe_context_of_binders = UState.of_binders +type 'a in_evar_universe_context = 'a * UState.t (*******************************************************************) (* Metamaps *) @@ -419,13 +408,15 @@ let key id (_, idtoev) = end +type goal_kind = ToShelve | ToGiveUp + type evar_map = { (** Existential variables *) defn_evars : evar_info EvMap.t; undf_evars : evar_info EvMap.t; evar_names : EvNames.t; (** Universes *) - universes : evar_universe_context; + universes : UState.t; (** Conversion problems *) conv_pbs : evar_constraint list; last_mods : Evar.Set.t; @@ -443,6 +434,7 @@ type evar_map = { name) of the evar which will be instantiated with a term containing [e]. *) + future_goals_status : goal_kind EvMap.t; extras : Store.t; } @@ -482,7 +474,8 @@ let remove d e = | Some e' -> if Evar.equal e e' then None else d.principal_future_goal in let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in - { d with undf_evars; defn_evars; principal_future_goal; future_goals } + let future_goals_status = EvMap.remove e d.future_goals_status in + { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status } let find d e = try EvMap.find e d.undf_evars @@ -556,10 +549,10 @@ let existential_type d (n, args) = instantiate_evar_array info info.evar_concl args let add_constraints d c = - { d with universes = add_constraints_context d.universes c } + { d with universes = UState.add_constraints d.universes c } let add_universe_constraints d c = - { d with universes = add_universe_constraints_context d.universes c } + { d with universes = UState.add_universe_constraints d.universes c } (*** /Lifting... ***) @@ -584,7 +577,7 @@ let create_evar_defs sigma = { sigma with let empty = { defn_evars = EvMap.empty; undf_evars = EvMap.empty; - universes = empty_evar_universe_context; + universes = UState.empty; conv_pbs = []; last_mods = Evar.Set.empty; metas = Metamap.empty; @@ -592,6 +585,7 @@ let empty = { evar_names = EvNames.empty; (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; + future_goals_status = EvMap.empty; extras = Store.empty; } @@ -607,14 +601,14 @@ let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d = let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in let universes = if not with_univs then evd.universes - else union_evar_universe_context evd.universes d.universes + else UState.union evd.universes d.universes in { evd with metas = d.metas; last_mods; conv_pbs; universes } let merge_universe_context evd uctx' = - { evd with universes = union_evar_universe_context evd.universes uctx' } + { evd with universes = UState.union evd.universes uctx' } let set_universe_context evd uctx' = { evd with universes = uctx' } @@ -796,16 +790,6 @@ let make_flexible_variable evd ~algebraic u = { evd with universes = UState.make_flexible_variable evd.universes ~algebraic u } -let make_evar_universe_context e l = - let uctx = UState.make (Environ.universes e) in - match l with - | None -> uctx - | Some us -> - List.fold_left - (fun uctx (loc,id) -> - fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx)) - uctx us - (****************************************) (* Operations on constants *) (****************************************) @@ -873,15 +857,10 @@ let set_eq_sort env d s1 s2 = | Some (u1, u2) -> if not (type_in_type env) then add_universe_constraints d - (Universes.Constraints.singleton (u1,Universes.UEq,u2)) + (Universes.Constraints.singleton (Universes.UEq (u1,u2))) else d -let has_lub evd u1 u2 = - if Univ.Universe.equal u1 u2 then evd - else add_universe_constraints evd - (Universes.Constraints.singleton (u1,Universes.ULub,u2)) - let set_eq_level d u1 u2 = add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty) @@ -899,7 +878,7 @@ let set_leq_sort env evd s1 s2 = | None -> evd | Some (u1, u2) -> if not (type_in_type env) then - add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2)) + add_universe_constraints evd (Universes.Constraints.singleton (Universes.ULe (u1,u2))) else evd let check_eq evd s s' = @@ -908,10 +887,6 @@ let check_eq evd s s' = let check_leq evd s s' = UGraph.check_leq (UState.ugraph evd.universes) s s' -let normalize_evar_universe_context_variables = UState.normalize_variables - -let abstract_undefined_variables = UState.abstract_undefined_variables - let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } @@ -920,16 +895,14 @@ let refresh_undefined_universes evd = let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in evd', subst -let normalize_evar_universe_context = UState.normalize - -let nf_univ_variables evd = - let subst, uctx' = normalize_evar_universe_context_variables evd.universes in +let nf_univ_variables evd = + let subst, uctx' = UState.normalize_variables evd.universes in let evd' = {evd with universes = uctx'} in evd', subst -let nf_constraints evd = - let subst, uctx' = normalize_evar_universe_context_variables evd.universes in - let uctx' = normalize_evar_universe_context uctx' in +let minimize_universes evd = + let subst, uctx' = UState.normalize_variables evd.universes in + let uctx' = UState.minimize uctx' in {evd with universes = uctx'} let universe_of_name evd s = UState.universe_of_name evd.universes s @@ -956,25 +929,72 @@ let drop_side_effects evd = let eval_side_effects evd = evd.effects (* Future goals *) -let declare_future_goal evk evd = - { evd with future_goals = evk::evd.future_goals } +let declare_future_goal ?tag evk evd = + { evd with future_goals = evk::evd.future_goals; + future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status } -let declare_principal_goal evk evd = +let declare_principal_goal ?tag evk evd = match evd.principal_future_goal with | None -> { evd with future_goals = evk::evd.future_goals; - principal_future_goal=Some evk; } + principal_future_goal=Some evk; + future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status; + } | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.") +type future_goals = Evar.t list * Evar.t option * goal_kind EvMap.t + let future_goals evd = evd.future_goals let principal_future_goal evd = evd.principal_future_goal -let reset_future_goals evd = - { evd with future_goals = [] ; principal_future_goal=None } +let save_future_goals evd = + (evd.future_goals, evd.principal_future_goal, evd.future_goals_status) -let restore_future_goals evd gls pgl = - { evd with future_goals = gls ; principal_future_goal = pgl } +let reset_future_goals evd = + { evd with future_goals = [] ; principal_future_goal = None; + future_goals_status = EvMap.empty } + +let restore_future_goals evd (gls,pgl,map) = + { evd with future_goals = gls ; principal_future_goal = pgl; + future_goals_status = map } + +let fold_future_goals f sigma (gls,pgl,map) = + List.fold_left f sigma gls + +let map_filter_future_goals f (gls,pgl,map) = + (* Note: map is now a superset of filtered evs, but its size should + not be too big, so that's probably ok not to update it *) + (List.map_filter f gls,Option.bind pgl f,map) + +let filter_future_goals f (gls,pgl,map) = + (List.filter f gls,Option.bind pgl (fun a -> if f a then Some a else None),map) + +let dispatch_future_goals_gen distinguish_shelf (gls,pgl,map) = + let rec aux (comb,shelf,givenup as acc) = function + | [] -> acc + | evk :: gls -> + let acc = + try match EvMap.find evk map with + | ToGiveUp -> (comb,shelf,evk::givenup) + | ToShelve -> + if distinguish_shelf then (comb,evk::shelf,givenup) + else raise Not_found + with Not_found -> (evk::comb,shelf,givenup) in + aux acc gls in + (* Note: this reverses the order of initial list on purpose *) + let (comb,shelf,givenup) = aux ([],[],[]) gls in + (comb,shelf,givenup,pgl) + +let dispatch_future_goals = + dispatch_future_goals_gen true + +let extract_given_up_future_goals goals = + let (comb,_,givenup,_) = dispatch_future_goals_gen false goals in + (comb,givenup) + +let shelve_on_future_goals shelved (gls,pgl,map) = + (shelved @ gls, pgl, List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved map) (**********************************************************) (* Accessing metas *) @@ -991,6 +1011,7 @@ let set_metas evd metas = { effects = evd.effects; evar_names = evd.evar_names; future_goals = evd.future_goals; + future_goals_status = evd.future_goals_status; principal_future_goal = evd.principal_future_goal; extras = evd.extras; } @@ -1074,7 +1095,7 @@ let clear_metas evd = {evd with metas = Metamap.empty} let meta_merge ?(with_univs = true) evd1 evd2 = let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in let universes = - if with_univs then union_evar_universe_context evd2.universes evd1.universes + if with_univs then UState.union evd2.universes evd1.universes else evd2.universes in {evd2 with universes; metas; } @@ -1174,3 +1195,25 @@ module Monad = (* Failure explanation *) type unsolvability_explanation = SeveralInstancesFound of int + +(** Deprecated *) +type evar_universe_context = UState.t +let empty_evar_universe_context = UState.empty +let union_evar_universe_context = UState.union +let evar_universe_context_set = UState.context_set +let evar_universe_context_constraints = UState.constraints +let evar_context_universe_context = UState.context +let evar_universe_context_of = UState.of_context_set +let evar_universe_context_subst = UState.subst +let add_constraints_context = UState.add_constraints +let constrain_variables = UState.constrain_variables +let evar_universe_context_of_binders = UState.of_binders +let make_evar_universe_context e l = + let g = Environ.universes e in + match l with + | None -> UState.make g + | Some l -> UState.make_with_initial_binders g l +let normalize_evar_universe_context_variables = UState.normalize_variables +let abstract_undefined_variables = UState.abstract_undefined_variables +let normalize_evar_universe_context = UState.minimize +let nf_constraints = minimize_universes diff --git a/engine/evd.mli b/engine/evd.mli index b28ce2a62d..911799c447 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -280,11 +282,13 @@ val drop_side_effects : evar_map -> evar_map (** {5 Future goals} *) -val declare_future_goal : Evar.t -> evar_map -> evar_map +type goal_kind = ToShelve | ToGiveUp + +val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map (** Adds an existential variable to the list of future goals. For internal uses only. *) -val declare_principal_goal : Evar.t -> evar_map -> evar_map +val declare_principal_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map (** Adds an existential variable to the list of future goals and make it principal. Only one existential variable can be made principal, an error is raised otherwise. For internal uses only. *) @@ -297,16 +301,41 @@ val principal_future_goal : evar_map -> Evar.t option (** Retrieves the name of the principal existential variable if there is one. Used by the [refine] primitive of the tactic engine. *) +type future_goals + +val save_future_goals : evar_map -> future_goals +(** Retrieves the list of future goals including the principal future + goal. Used by the [refine] primitive of the tactic engine. *) + val reset_future_goals : evar_map -> evar_map (** Clears the list of future goals (as well as the principal future goal). Used by the [refine] primitive of the tactic engine. *) -val restore_future_goals : evar_map -> Evar.t list -> Evar.t option -> evar_map +val restore_future_goals : evar_map -> future_goals -> evar_map (** Sets the future goals (including the principal future goal) to a previous value. Intended to be used after a local list of future goals has been consumed. Used by the [refine] primitive of the tactic engine. *) +val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> future_goals -> evar_map +(** Fold future goals *) + +val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals +(** Applies a function on the future goals *) + +val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals +(** Applies a filter on the future goals *) + +val dispatch_future_goals : future_goals -> Evar.t list * Evar.t list * Evar.t list * Evar.t option +(** Returns the future_goals dispatched into regular, shelved, given_up + goals; last argument is the goal tagged as principal if any *) + +val extract_given_up_future_goals : future_goals -> Evar.t list * Evar.t list +(** An ad hoc variant for Proof.proof; not for general use *) + +val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals +(** Push goals on the shelve of future goals *) + (** {5 Sort variables} Evar maps also keep track of the universe constraints defined at a given @@ -318,8 +347,8 @@ exception UniversesDiffer val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map (** Add the given universe unification constraints to the evar map. - @raises UniversesDiffer in case a first-order unification fails. - @raises UniverseInconsistency + @raise UniversesDiffer in case a first-order unification fails. + @raise UniverseInconsistency . *) (** {5 Extra data} @@ -491,22 +520,31 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * UState.t val evar_universe_context_set : UState.t -> Univ.ContextSet.t +[@@ocaml.deprecated "Alias of UState.context_set"] val evar_universe_context_constraints : UState.t -> Univ.Constraint.t +[@@ocaml.deprecated "Alias of UState.constraints"] val evar_context_universe_context : UState.t -> Univ.UContext.t [@@ocaml.deprecated "alias of UState.context"] val evar_universe_context_of : Univ.ContextSet.t -> UState.t +[@@ocaml.deprecated "Alias of UState.of_context_set"] val empty_evar_universe_context : UState.t +[@@ocaml.deprecated "Alias of UState.empty"] val union_evar_universe_context : UState.t -> UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.union"] val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst +[@@ocaml.deprecated "Alias of UState.subst"] val constrain_variables : Univ.LSet.t -> UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.constrain_variables"] val evar_universe_context_of_binders : Universes.universe_binders -> UState.t +[@@ocaml.deprecated "Alias of UState.of_binders"] -val make_evar_universe_context : env -> (Id.t located) list option -> UState.t +val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t +[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"] val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> Id.t -> Univ.Level.t @@ -514,13 +552,15 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t val universe_binders : evar_map -> Universes.universe_binders val add_constraints_context : UState.t -> Univ.Constraint.t -> UState.t +[@@ocaml.deprecated "Alias of UState.add_constraints"] val normalize_evar_universe_context_variables : UState.t -> Univ.universe_subst in_evar_universe_context +[@@ocaml.deprecated "Alias of UState.normalize_variables"] -val normalize_evar_universe_context : UState.t -> - UState.t +val normalize_evar_universe_context : UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.minimize"] val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t @@ -543,7 +583,6 @@ val normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map val set_eq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map -val has_lub : evar_map -> Univ.Universe.t -> Univ.Universe.t -> evar_map val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map val set_eq_instances : ?flex:bool -> @@ -579,12 +618,16 @@ val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_co val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val abstract_undefined_variables : UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"] val fix_undefined_variables : evar_map -> evar_map val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst +(** Universe minimization *) +val minimize_universes : evar_map -> evar_map val nf_constraints : evar_map -> evar_map +[@@ocaml.deprecated "Alias of Evd.minimize_universes"] val update_sigma_env : evar_map -> env -> evar_map diff --git a/engine/ftactic.ml b/engine/ftactic.ml index 8e4c5f2206..e23a03c0c7 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Proofview.Notations diff --git a/engine/ftactic.mli b/engine/ftactic.mli index c108c0c2ea..6c389b2d67 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module defines potentially focussing tactics. They are used by Ltac to @@ -39,10 +41,10 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic (** {5 Focussing} *) -val nf_enter : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t +val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal. The resulting tactic is focussed. *) -val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t +val enter : (Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal, without evar normalization. The resulting tactic is focussed. *) diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 3674bb9432..4afa817b27 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines the low-level monadic operations used by the diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 50b4abd8bd..545334ce9a 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file implements the low-level monadic operations used by the diff --git a/engine/namegen.ml b/engine/namegen.ml index ff0b5a74e7..d66b77b573 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created from contents that was formerly in termops.ml and @@ -190,9 +192,45 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = (**********************************************************************) (* Fresh names *) +(* Introduce a mode where auto-generated names are mangled + to test dependence of scripts on auto-generated names *) + +let mangle_names = ref false + +let _ = Goptions.( + declare_bool_option + { optdepr = false; + optname = "mangle auto-generated names"; + optkey = ["Mangle";"Names"]; + optread = (fun () -> !mangle_names); + optwrite = (:=) mangle_names; }) + +let mangle_names_prefix = ref (Id.of_string "_0") +let set_prefix x = mangle_names_prefix := forget_subscript x + +let set_mangle_names_mode x = begin + set_prefix x; + mangle_names := true + end + +let _ = Goptions.( + declare_string_option + { optdepr = false; + optname = "mangled names prefix"; + optkey = ["Mangle";"Names";"Prefix"]; + optread = (fun () -> Id.to_string !mangle_names_prefix); + optwrite = begin fun x -> + set_prefix + (try Id.of_string x + with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) + end }) + +let mangle_id id = if !mangle_names then !mangle_names_prefix else id + (* Looks for next "good" name by lifting subscript *) let next_ident_away_from id bad = + let id = mangle_id id in let rec name_rec id = if bad id then name_rec (increment_subscript id) else id in name_rec id @@ -291,6 +329,7 @@ let next_global_ident_away id avoid = looks for same name with lower available subscript *) let next_ident_away id avoid = + let id = mangle_id id in if Id.Set.mem id avoid then next_ident_away_from (restart_subscript id) (fun id -> Id.Set.mem id avoid) else id @@ -421,23 +460,3 @@ let rename_bound_vars_as_displayed sigma avoid env c = | _ -> c in rename avoid env c - -(**********************************************************************) -(* "H"-based naming strategy introduced June 2014 for hypotheses in - Prop produced by case/elim/destruct/induction, in place of the - strategy that was using the first letter of the type, leading to - inelegant "n:~A", "e:t=u", etc. when eliminating sumbool or similar - types *) - -let h_based_elimination_names = ref false - -let use_h_based_elimination_names () = !h_based_elimination_names - -open Goptions - -let _ = declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "use of \"H\"-based proposition names in elimination tactics"; - optkey = ["Standard";"Proposition";"Elimination";"Names"]; - optread = (fun () -> !h_based_elimination_names); - optwrite = (:=) h_based_elimination_names } diff --git a/engine/namegen.mli b/engine/namegen.mli index abeed9f62d..1b70ef68dd 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file features facilities to generate fresh names. *) @@ -114,7 +116,6 @@ val compute_displayed_name_in_gen : (evar_map -> int -> 'a -> bool) -> evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t -(**********************************************************************) -(* Naming strategy for arguments in Prop when eliminating inductive types *) - -val use_h_based_elimination_names : unit -> bool +val set_mangle_names_mode : Id.t -> unit +(** Turn on mangled names mode and with the given prefix. + @raise UserError if the argument is invalid as an identifier. *) diff --git a/engine/nameops.ml b/engine/nameops.ml index 5105d7becc..53969cafa8 100644 --- a/engine/nameops.ml +++ b/engine/nameops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/engine/nameops.mli b/engine/nameops.mli index 0fec8a925d..96842dfb99 100644 --- a/engine/nameops.mli +++ b/engine/nameops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/engine/proofview.ml b/engine/proofview.ml index 47b9b406d8..22271dd02c 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) @@ -33,7 +35,7 @@ type entry = (EConstr.constr * EConstr.types) list (* In this version: returns the list of focused goals together with the [evar_map] context. *) let proofview p = - p.comb , p.solution + List.map drop_state p.comb , p.solution let compact el ({ solution } as pv) = let nf c = Evarutil.nf_evar solution c in @@ -74,7 +76,7 @@ let dependent_init = let (gl, _) = EConstr.destEvar sigma econstr in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let entry = (econstr, typ) :: ret in - entry, { solution = sol; comb = gl :: comb; shelf = [] } + entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] } in fun t -> let entry, v = aux t in @@ -110,7 +112,7 @@ let partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry) (* First component is a reverse list of the goals which come before and second component is the list of the goals which go after (in the expected order). *) -type focus_context = Evar.t list * Evar.t list +type focus_context = goal_with_state list * goal_with_state list (** Returns a stylised view of a focus_context for use by, for @@ -120,11 +122,12 @@ type focus_context = Evar.t list * Evar.t list new nearly identical function everytime. 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 f = f +let focus_context (left,right) = + (List.map drop_state left, List.map drop_state 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 + [(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 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 @@ -149,21 +152,35 @@ let unfocus_sublist (left,right) s = proofview. It returns the focused proofview, and a context for the focus stack. *) let focus i j sp = - let (new_comb, context) = focus_sublist i j sp.comb in - ( { sp with comb = new_comb } , context ) + let (new_comb, (left, right)) = focus_sublist i j sp.comb in + ( { sp with comb = new_comb } , (left, right) ) + +let cleared_alias evd g = + let evk = drop_state g in + let state = get_state g in + Option.map (fun g -> goal_with_state g state) (Evarutil.advance evd evk) (** [undefined defs l] is the list of goals in [l] which are still unsolved (after advancing cleared goals). Note that order matters. *) -let undefined defs l = +let undefined_evars defs l = List.fold_right (fun evk l -> match Evarutil.advance defs evk with | Some evk -> List.add_set Evar.equal evk l | None -> l) l [] +let goal_with_state_equal x y = Evar.equal (drop_state x) (drop_state y) +let undefined defs l = + List.fold_right (fun evk l -> + match cleared_alias defs evk with + | Some evk -> List.add_set goal_with_state_equal evk l + | None -> l) l [] (** Unfocuses a proofview with respect to a context. *) -let unfocus c sp = - { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) } +let unfocus (left, right) sp = + { sp with comb = undefined sp.solution (unfocus_sublist (left, right) sp.comb) } +let with_empty_state = Proofview_monad.with_empty_state +let drop_state = Proofview_monad.drop_state +let goal_with_state = Proofview_monad.goal_with_state (** {6 The tactic monad} *) @@ -406,7 +423,8 @@ let tclFOCUSID id t = try let ev = Evd.evar_key id initial.solution in try - let n = CList.index Evar.equal ev initial.comb in + let comb = CList.map drop_state initial.comb in + let n = CList.index Evar.equal ev comb in (* goal is already under focus *) let (focused,context) = focus n n initial in Pv.set focused >> @@ -415,7 +433,7 @@ let tclFOCUSID id t = return result with Not_found -> (* otherwise, save current focus and work purely on the shelve *) - Comb.set [ev] >> + Comb.set [with_empty_state ev] >> t >>= fun result -> Comb.set initial.comb >> return result @@ -445,7 +463,7 @@ let iter_goal i = Comb.get >>= fun initial -> Proof.List.fold_left begin fun (subgoals as cur) goal -> Solution.get >>= fun step -> - match Evarutil.advance step goal with + match cleared_alias step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -462,7 +480,7 @@ let map_goal i = Comb.get >>= fun initial -> Proof.List.fold_left begin fun (acc, subgoals as cur) goal -> Solution.get >>= fun step -> - match Evarutil.advance step goal with + match cleared_alias step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -488,7 +506,7 @@ let fold_left2_goal i s l = in Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a -> Solution.get >>= fun step -> - match Evarutil.advance step goal with + match cleared_alias step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -532,7 +550,7 @@ let tclDISPATCHGEN0 join tacs = let open Proof in Pv.get >>= function | { comb=[goal] ; solution } -> - begin match Evarutil.advance solution goal with + begin match cleared_alias solution goal with | None -> tclUNIT (join []) | Some _ -> Proof.map (fun res -> join [res]) tac end @@ -554,8 +572,8 @@ let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs (** [extend_to_list startxs rx endxs l] builds a list - [startxs@[rx,...,rx]@endxs] of the same length as [l]. Raises - [SizeMismatch] if [startxs@endxs] is already longer than [l]. *) + [startxs @ [rx,...,rx] @ endxs] of the same length as [l]. Raises + [SizeMismatch] if [startxs @ endxs] is already longer than [l]. *) let extend_to_list startxs rx endxs l = (* spiwack: I use [l] essentially as a natural number *) let rec duplicate acc = function @@ -624,12 +642,12 @@ let shelve = Comb.get >>= fun initial -> Comb.set [] >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> - Shelf.modify (fun gls -> gls @ initial) + Shelf.modify (fun gls -> gls @ CList.map drop_state initial) let shelve_goals l = let open Proof in Comb.get >>= fun initial -> - let comb = CList.filter (fun g -> not (CList.mem g l)) initial in + let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in Comb.set comb >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >> Shelf.modify (fun gls -> gls @ l) @@ -656,9 +674,27 @@ let free_evars sigma l = in List.map map l +let free_evars_with_state sigma l = + let cache = Evarutil.create_undefined_evars_cache () in + let map ev = + (** Computes the set of evars appearing in the hypotheses, the conclusion or + the body of the evar_info [evi]. Note: since we want to use it on goals, + the body is actually supposed to be empty. *) + let ev = drop_state ev in + let evi = Evd.find sigma ev in + let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in + (ev, fevs) + in + List.map map l + + (** [unifiable sigma g l] checks whether [g] appears in another subgoal of [l]. The list [l] may contain [g], but it does not affect the result. *) +let unifiable_delayed_with_state sigma g l = + let g = drop_state g in + unifiable_delayed g l + let unifiable sigma g l = let l = free_evars sigma l in unifiable_delayed g l @@ -668,8 +704,8 @@ let unifiable sigma g l = whose definition other goals of [l] depend, and [n] are the non-unifiable goals. *) let partition_unifiable sigma l = - let fevs = free_evars sigma l in - CList.partition (fun g -> unifiable_delayed g fevs) l + let fevs = free_evars_with_state sigma l in + CList.partition (fun g -> unifiable_delayed_with_state sigma g fevs) l (** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not @@ -680,7 +716,7 @@ let shelve_unifiable = let (u,n) = partition_unifiable initial.solution initial.comb in Comb.set n >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >> - Shelf.modify (fun gls -> gls @ u) + Shelf.modify (fun gls -> gls @ CList.map drop_state u) (** [guard_no_unifiable] returns the list of unifiable goals if some goals are unifiable (see {!shelve_unifiable}) in the current focus. *) @@ -691,13 +727,14 @@ let guard_no_unifiable = match u with | [] -> tclUNIT None | gls -> - let l = CList.map (fun g -> Evd.dependent_evar_ident g initial.solution) gls in + let l = CList.map (fun g -> Evd.dependent_evar_ident (drop_state g) initial.solution) gls in let l = CList.map (fun id -> Names.Name id) l in tclUNIT (Some l) (** [unshelve l p] adds all the goals in [l] at the end of the focused goals of p *) let unshelve l p = + let l = List.map with_empty_state l in (* advance the goals in case of clear *) let l = undefined p.solution l in { p with comb = p.comb@l } @@ -731,12 +768,13 @@ let with_shelf tac = tac >>= fun ans -> Pv.get >>= fun npv -> let { shelf = gls; solution = sigma } = npv in + (* The pending future goals are necessarily coming from V82.tactic *) + (* and thus considered as to shelve, as in Proof.run_tactic *) let gls' = Evd.future_goals sigma in - let fgoals = Evd.future_goals solution in - let pgoal = Evd.principal_future_goal solution in - let sigma = Evd.restore_future_goals sigma fgoals pgoal in + let fgoals = Evd.save_future_goals solution in + let sigma = Evd.restore_future_goals sigma fgoals in (* Ensure we mark and return only unsolved goals *) - let gls' = undefined sigma (CList.rev_append gls' gls) in + let gls' = undefined_evars sigma (CList.rev_append gls' gls) in let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in let npv = { npv with shelf; solution = sigma } in Pv.set npv >> tclUNIT (gls', ans) @@ -818,7 +856,7 @@ let give_up = Comb.set [] >> mark_as_unsafe >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >> - Giveup.put initial + Giveup.put (CList.map drop_state initial) @@ -859,8 +897,8 @@ module Progress = struct (** 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 + let evi1 = Evd.find evars1 (drop_state gl1) in + let evi2 = Evd.find evars2 (drop_state gl2) in eq_evar_info evars1 evars2 evi1 evi2 end @@ -974,6 +1012,15 @@ module Unsafe = struct let tclSETGOALS = Comb.set + let tclGETSHELF = Shelf.get + + let tclSETSHELF = Shelf.set + + let tclPUTSHELF to_shelve = + tclBIND tclGETSHELF (fun shelf -> tclSETSHELF (to_shelve@shelf)) + + let tclPUTGIVENUP = Giveup.put + let tclEVARSADVANCE evd = Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb }) @@ -1023,14 +1070,19 @@ let catchable_exception = function module Goal = struct - type 'a t = { + type t = { env : Environ.env; sigma : Evd.evar_map; concl : EConstr.constr ; + state : StateStore.t; self : Evar.t ; (* for compatibility with old-style definitions *) } - let assume (gl : 'a t) = (gl :> [ `NF ] t) + let assume (gl : t) = (gl : t) + + let print { sigma; self } = { Evd.it = self; sigma } + + let state { state=state } = state let env {env} = env let sigma {sigma} = sigma @@ -1038,16 +1090,19 @@ module Goal = struct let concl {concl} = concl let extra {sigma; self} = goal_extra sigma self - let gmake_with info env sigma goal = + let gmake_with info env sigma goal state = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; sigma = sigma ; concl = EConstr.of_constr (Evd.evar_concl info); + state = state ; self = goal } let nf_gmake env sigma goal = + let state = get_state goal in + let goal = drop_state goal in let info = Evarutil.nf_evar_info sigma (Evd.find sigma goal) in let sigma = Evd.add sigma goal info in - gmake_with info env sigma goal , sigma + gmake_with info env sigma goal state , sigma let nf_enter f = InfoL.tag (Info.Dispatch) begin @@ -1063,15 +1118,17 @@ module Goal = struct end end - let normalize { self } = + let normalize { self; state } = Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> - let (gl,sigma) = nf_gmake env sigma self in + 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 let info = Evd.find sigma goal in - gmake_with info env sigma goal + gmake_with info env sigma goal state let enter f = let f gl = InfoL.tag (Info.DBranch) (f gl) in @@ -1104,7 +1161,7 @@ module Goal = struct Pv.get >>= fun step -> let sigma = step.solution in let map goal = - match Evarutil.advance sigma goal with + match cleared_alias sigma goal with | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> let gl = @@ -1157,25 +1214,29 @@ let tclCHECKINTERRUPT = module V82 = struct type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - let tactic tac = + let tactic ?(nf_evars=true) tac = (* spiwack: we ignore the dependencies between goals here, expectingly preserving the semantics of <= 8.2 tactics *) (* spiwack: convenience notations, waiting for ocaml 3.12 *) let open Proof in Pv.get >>= fun ps -> try - let tac gl evd = + let tac g_w_s evd = + let g, w = drop_state g_w_s, get_state g_w_s in let glsigma = - tac { Evd.it = gl ; sigma = evd; } in + tac { Evd.it = g ; sigma = evd; } in let sigma = glsigma.Evd.sigma in - let g = glsigma.Evd.it in + let g = CList.map (fun g -> goal_with_state g w) glsigma.Evd.it in ( g, sigma ) in (* Old style tactics expect the goals normalized with respect to evars. *) - let (initgoals,initevd) = - Evd.Monad.List.map (fun g s -> goal_nf_evar s g) ps.comb ps.solution + let (initgoals_w_state, initevd) = + Evd.Monad.List.map (fun g_w_s s -> + let g, w = drop_state g_w_s, get_state g_w_s in + let g, s = if nf_evars then goal_nf_evar s g else g, s in + goal_with_state g w, s) ps.comb ps.solution in - let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in + let (goalss,evd) = Evd.Monad.List.map tac initgoals_w_state initevd in let sgs = CList.flatten goalss in let sgs = undefined evd sgs in InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >> @@ -1190,8 +1251,9 @@ module V82 = struct let nf_evar_goals = Pv.modify begin fun ps -> let map g s = goal_nf_evar s g in - let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in - { ps with solution = evd; comb = goals; } + let comb = CList.map drop_state ps.comb in + let (_goals,evd) = Evd.Monad.List.map map comb ps.solution in + { ps with solution = evd; } end let has_unresolved_evar pv = @@ -1201,14 +1263,14 @@ module V82 = struct let grab pv = let undef = Evd.undefined_map pv.solution in let goals = CList.rev_map fst (Evar.Map.bindings undef) in - { pv with comb = goals } + { pv with comb = List.map with_empty_state goals } (* Returns the open goals of the proofview together with the evar_map to interpret them. *) let goals { comb = comb ; solution = solution; } = - { Evd.it = comb ; sigma = solution } + { Evd.it = List.map drop_state comb ; sigma = solution } let top_goals initial { solution=solution; } = let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in @@ -1222,9 +1284,9 @@ module V82 = struct let of_tactic t gls = try - let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in + let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in - { Evd.sigma = final.solution ; it = final.comb } + { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } with Logic_monad.TacticFailure e as src -> let (_, info) = CErrors.push src in iraise (e, info) diff --git a/engine/proofview.mli b/engine/proofview.mli index b02fde3a80..e7be665527 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This files defines the basic mechanism of proofs: the [proofview] @@ -72,7 +74,15 @@ val return : proofview -> Evd.evar_map val partial_proof : entry -> proofview -> constr list val initial_goals : entry -> (constr * types) list +(** goal <-> goal_with_state *) +val with_empty_state : + Proofview_monad.goal -> Proofview_monad.goal_with_state +val drop_state : + Proofview_monad.goal_with_state -> Proofview_monad.goal +val goal_with_state : + Proofview_monad.goal -> Proofview_monad.StateStore.t -> + Proofview_monad.goal_with_state (** {6 Focusing commands} *) @@ -416,14 +426,26 @@ module Unsafe : sig (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved, appending them to the list of focused goals. If a goal is already solved, it is not added. *) - val tclNEWGOALS : Evar.t list -> unit tactic + val tclNEWGOALS : Proofview_monad.goal_with_state list -> unit tactic (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a goal is already solved, it is not set. *) - val tclSETGOALS : Evar.t list -> unit tactic + val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic (** [tclGETGOALS] returns the list of goals under focus. *) - val tclGETGOALS : Evar.t list tactic + val tclGETGOALS : Proofview_monad.goal_with_state list tactic + + (** [tclSETSHELF gls] sets goals [gls] as the current shelf. *) + val tclSETSHELF : Evar.t list -> unit tactic + + (** [tclGETSHELF] returns the list of goals on the shelf. *) + val tclGETSHELF : Evar.t list tactic + + (** [tclPUTSHELF] appends goals to the shelf. *) + val tclPUTSHELF : Evar.t list -> unit tactic + + (** [tclPUTGIVENUP] add an given up goal. *) + val tclPUTGIVENUP : Evar.t list -> unit tactic (** Sets the evar universe context. *) val tclEVARUNIVCONTEXT : UState.t -> unit tactic @@ -461,56 +483,51 @@ end module Goal : sig - (** Type of goals. - - The first parameter type is a phantom argument indicating whether the data - contained in the goal has been normalized w.r.t. the current sigma. If it - is the case, it is flagged [ `NF ]. You may still access the un-normalized - data using {!assume} if you known you do not rely on the assumption of - being normalized, at your own risk. - - *) - type 'a t + (** Type of goals. *) + type t (** Assume that you do not need the goal to be normalized. *) - val assume : 'a t -> [ `NF ] t + val assume : t -> t + [@@ocaml.deprecated "Normalization is enforced by EConstr, [assume] is not needed anymore"] (** Normalises the argument goal. *) - val normalize : 'a t -> [ `NF ] t tactic + val normalize : t -> t tactic (** [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 hypotheses) and the current evar map. *) - val concl : 'a t -> constr - val hyps : 'a t -> named_context - val env : 'a t -> Environ.env - val sigma : 'a t -> Evd.evar_map - val extra : 'a t -> Evd.Store.t + val concl : t -> constr + val hyps : t -> named_context + val env : t -> Environ.env + val sigma : t -> Evd.evar_map + val extra : t -> Evd.Store.t + val state : t -> Proofview_monad.StateStore.t (** [nf_enter t] applies the goal-dependent tactic [t] in each goal independently, in the manner of {!tclINDEPENDENT} except that the current goal is also given as an argument to [t]. The goal is normalised with respect to evars. *) - val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic + val nf_enter : (t -> unit tactic) -> unit tactic (** Like {!nf_enter}, but does not normalize the goal beforehand. *) - val enter : ([ `LZ ] t -> unit tactic) -> unit tactic + val enter : (t -> unit tactic) -> unit tactic (** Like {!enter}, but assumes exactly one goal under focus, raising *) (** a fatal error otherwise. *) - val enter_one : ?__LOC__:string -> ([ `LZ ] t -> 'a tactic) -> 'a tactic + val enter_one : ?__LOC__:string -> (t -> 'a tactic) -> 'a tactic (** Recover the list of current goals under focus, without evar-normalization. FIXME: encapsulate the level in an existential type. *) - val goals : [ `LZ ] t tactic list tactic + val goals : t tactic list tactic (** [unsolved g] is [true] if [g] is still unsolved in the current proof state. *) - val unsolved : 'a t -> bool tactic + val unsolved : t -> bool tactic (** Compatibility: avoid if possible *) - val goal : [ `NF ] t -> Evar.t + val goal : t -> Evar.t + val print : t -> Goal.goal Evd.sigma end @@ -547,7 +564,10 @@ val tclLIFT : 'a NonLogical.t -> 'a tactic (*** Compatibility layer with <= 8.2 tactics ***) module V82 : sig type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - val tactic : tac -> unit tactic + + (* [nf_evars=true] applies the evar (assignment) map to the goals + * (conclusion and context) before calling the tactic *) + val tactic : ?nf_evars:bool -> tac -> unit tactic (* normalises the evars in the goals, and stores the result in solution. *) diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index d0f4712258..52bcabf958 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines the datatypes used as internal states by the @@ -149,13 +151,25 @@ module Info = struct CList.map_append (collapse_tree n) f end +module StateStore = Store.Make(struct end) + +(* let (set_state, get_state) = StateDyn.Easy.make_dyn "goal_state" *) + +type goal = Evar.t +type goal_with_state = Evar.t * StateStore.t + +let drop_state = fst +let get_state = snd +let goal_with_state g s = (g, s) +let with_empty_state g = (g, StateStore.empty) +let map_goal_with_state f (g, s) = (f g, s) (** Type of proof views: current [evar_map] together with the list of focused goals. *) type proofview = { solution : Evd.evar_map; - comb : Evar.t list; - shelf : Evar.t list; + comb : goal_with_state list; + shelf : goal list; } (** {6 Instantiation of the logic monad} *) @@ -169,7 +183,7 @@ module P = struct type e = bool (** Status (safe/unsafe) * shelved goals * given up *) - type w = bool * Evar.t list + type w = bool * goal list let wunit = true , [] let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2 @@ -209,9 +223,9 @@ module Solution : State with type t := Evd.evar_map = struct let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution }) end -module Comb : State with type t = Evar.t list = struct +module Comb : State with type t = goal_with_state list = struct (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list + type t = goal_with_state list let get = Logical.map (fun {comb} -> comb) Pv.get let set c = Pv.modify (fun pv -> { pv with comb = c }) let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb }) @@ -227,17 +241,17 @@ module Status : Writer with type t := bool = struct let put s = Logical.put (s, []) end -module Shelf : State with type t = Evar.t list = struct +module Shelf : State with type t = goal list = struct (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list + type t = goal list let get = Logical.map (fun {shelf} -> shelf) Pv.get let set c = Pv.modify (fun pv -> { pv with shelf = c }) let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf }) end -module Giveup : Writer with type t = Evar.t list = struct +module Giveup : Writer with type t = goal list = struct (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list + type t = goal list let put gs = Logical.put (true, gs) end diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index e7123218b1..9d75242175 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines the datatypes used as internal states by the @@ -67,12 +69,21 @@ module Info : sig end +module StateStore : Store.S +type goal = Evar.t +type goal_with_state +val drop_state : goal_with_state -> goal +val get_state : goal_with_state -> StateStore.t +val goal_with_state : goal -> StateStore.t -> goal_with_state +val with_empty_state : goal -> goal_with_state +val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state + (** Type of proof views: current [evar_map] together with the list of focused goals. *) type proofview = { solution : Evd.evar_map; - comb : Evar.t list; - shelf : Evar.t list; + comb : goal_with_state list; + shelf : goal list; } (** {6 Instantiation of the logic monad} *) @@ -81,7 +92,7 @@ module P : sig type s = proofview * Environ.env (** Status (safe/unsafe) * given up *) - type w = bool * Evar.t list + type w = bool * goal list val wunit : w val wprod : w -> w -> w @@ -118,7 +129,7 @@ module Pv : State with type t := proofview module Solution : State with type t := Evd.evar_map (** Lens to the list of focused goals. *) -module Comb : State with type t = Evar.t list +module Comb : State with type t = goal_with_state list (** Lens to the global environment. *) module Env : State with type t := Environ.env @@ -128,11 +139,11 @@ module Status : Writer with type t := bool (** Lens to the list of goals which have been shelved during the execution of the tactic. *) -module Shelf : State with type t = Evar.t list +module Shelf : State with type t = goal list (** Lens to the list of goals which were given up during the execution of the tactic. *) -module Giveup : Writer with type t = Evar.t list +module Giveup : Writer with type t = goal list (** Lens and utilies pertaining to the info trace *) module InfoL : sig diff --git a/engine/termops.ml b/engine/termops.ml index 40b3d0d8b6..3dfb0c34fd 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -292,16 +294,17 @@ let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_cont let pr_evar_universe_context ctx = let open UState in - let open Evd in let prl = pr_uctx_level ctx in if UState.is_empty ctx then mt () else (str"UNIVERSES:"++brk(0,1)++ - h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++ + h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl()) + h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ + str "WEAK CONSTRAINTS:"++brk(0,1)++ + h 0 (UState.pr_weak prl ctx) ++ fnl ()) let print_env_short env = let print_constr = print_kconstr in @@ -797,9 +800,9 @@ let fold_constr_with_binders sigma g f n acc c = each binder traversal; it is not recursive and the order with which subterms are processed is not specified *) -let iter_constr_with_full_binders g f l c = +let iter_constr_with_full_binders sigma g f l c = let open RelDecl in - match kind c with + match EConstr.kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () | Cast (c,_, t) -> f l c; f l t @@ -913,12 +916,9 @@ let vars_of_global_reference env gr = (* Tests whether [m] is a subterm of [t]: [m] is appropriately lifted through abstractions of [t] *) -let dependent_main noevar univs sigma m t = +let dependent_main noevar sigma m t = let open EConstr in - let eqc x y = - if univs then not (Option.is_empty (eq_constr_universes sigma x y)) - else eq_constr_nounivs sigma x y - in + let eqc x y = eq_constr_nounivs sigma x y in let rec deprec m t = if eqc m t then raise Occur @@ -935,11 +935,8 @@ let dependent_main noevar univs sigma m t = in try deprec m t; false with Occur -> true -let dependent sigma c t = dependent_main false false sigma c t -let dependent_no_evar sigma c t = dependent_main true false sigma c t - -let dependent_univs sigma c t = dependent_main false true sigma c t -let dependent_univs_no_evar sigma c t = dependent_main true true sigma c t +let dependent sigma c t = dependent_main false sigma c t +let dependent_no_evar sigma c t = dependent_main true sigma c t let dependent_in_decl sigma a decl = let open NamedDecl in diff --git a/engine/termops.mli b/engine/termops.mli index a3559a693b..3b0c4bba64 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines various utilities for term manipulation that are not @@ -76,9 +78,10 @@ val fold_constr_with_full_binders : Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -val iter_constr_with_full_binders : - (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> Constr.constr -> unit) -> 'a -> - Constr.constr -> unit +val iter_constr_with_full_binders : Evd.evar_map -> + (rel_declaration -> 'a -> 'a) -> + ('a -> constr -> unit) -> 'a -> + constr -> unit (**********************************************************************) @@ -105,8 +108,6 @@ val free_rels : Evd.evar_map -> constr -> Int.Set.t (** [dependent m t] tests whether [m] is a subterm of [t] *) val dependent : Evd.evar_map -> constr -> constr -> bool val dependent_no_evar : Evd.evar_map -> constr -> constr -> bool -val dependent_univs : Evd.evar_map -> constr -> constr -> bool -val dependent_univs_no_evar : Evd.evar_map -> constr -> constr -> bool val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool val count_occurrences : Evd.evar_map -> constr -> constr -> int val collect_metas : Evd.evar_map -> constr -> int list diff --git a/engine/uState.ml b/engine/uState.ml index 4b650c9c94..6c8dbe3f44 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -18,6 +20,8 @@ type uinfo = { uloc : Loc.t option; } +module UPairSet = Universes.UPairSet + (* 2nd part used to check consistency on the fly. *) type t = { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t; @@ -30,6 +34,7 @@ type t = algebraic universes as they appear in inferred types only. *) uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) + uctx_weak_constraints : UPairSet.t } let empty = @@ -39,7 +44,8 @@ let empty = uctx_univ_variables = Univ.LMap.empty; uctx_univ_algebraic = Univ.LSet.empty; uctx_universes = UGraph.initial_universes; - uctx_initial_universes = UGraph.initial_universes; } + uctx_initial_universes = UGraph.initial_universes; + uctx_weak_constraints = UPairSet.empty; } let make u = { empty with @@ -67,6 +73,7 @@ let union ctx ctx' = let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) (Univ.ContextSet.levels ctx.uctx_local) in let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in + let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in let declarenew g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g in @@ -80,10 +87,11 @@ let union ctx ctx' = Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; uctx_initial_universes = declarenew ctx.uctx_initial_universes; uctx_universes = - if local == ctx.uctx_local then ctx.uctx_universes - else - let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in - UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) } + (if local == ctx.uctx_local then ctx.uctx_universes + else + let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in + UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes)); + uctx_weak_constraints = weak} let context_set ctx = ctx.uctx_local @@ -140,11 +148,21 @@ let instantiate_variable l b v = exception UniversesDiffer +let drop_weak_constraints = ref false + let process_universe_constraints ctx cstrs = let open Univ in + let open Universes in let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in - let normalize = Universes.normalize_universe_opt_subst vars in + let weak = ref ctx.uctx_weak_constraints in + let normalize = normalize_univ_variable_opt_subst vars in + let nf_constraint = function + | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v) + | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v) + | UEq (u, v) -> UEq (subst_univs_universe normalize u, subst_univs_universe normalize v) + | ULe (u, v) -> ULe (subst_univs_universe normalize u, subst_univs_universe normalize v) + in let is_local l = Univ.LMap.mem l !vars in let varinfo x = match Univ.Universe.level x with @@ -183,12 +201,12 @@ let process_universe_constraints ctx cstrs = if UGraph.check_eq univs l r then local else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) in - let unify_universes (l, d, r) local = - let l = normalize l and r = normalize r in - if Univ.Universe.equal l r then local + let unify_universes cst local = + let cst = nf_constraint cst in + if Constraints.is_trivial cst then local else - match d with - | Universes.ULe -> + 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. *) @@ -216,43 +234,47 @@ let process_universe_constraints ctx cstrs = else Univ.enforce_leq l r local end - | Universes.ULub -> - begin match Universe.level l, Universe.level r with - | Some l', Some r' -> - equalize_variables true l l' r r' local - | _, _ -> assert false - end - | Universes.UEq -> equalize_universes l r local + | ULub (l, r) -> + equalize_variables true (Universe.make l) l (Universe.make r) r local + | UWeak (l, r) -> + if not !drop_weak_constraints then weak := UPairSet.add (l,r) !weak; local + | UEq (l, r) -> equalize_universes l r local in let local = - Universes.Constraints.fold unify_universes cstrs Univ.Constraint.empty + Constraints.fold unify_universes cstrs Univ.Constraint.empty in - !vars, local + !vars, !weak, local let add_constraints ctx cstrs = let univs, local = ctx.uctx_local in let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> let l = Univ.Universe.make l and r = Univ.Universe.make r in - let cstr' = - if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r) - else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r) + let cstr' = match d with + | Univ.Lt -> + Universes.ULe (Univ.Universe.super l, r) + | Univ.Le -> Universes.ULe (l, r) + | Univ.Eq -> Universes.UEq (l, r) in Universes.Constraints.add cstr' acc) cstrs Universes.Constraints.empty in - let vars, local' = process_universe_constraints ctx cstrs' in - { ctx with uctx_local = (univs, Univ.Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } + let vars, weak, local' = process_universe_constraints ctx cstrs' in + { ctx with + uctx_local = (univs, Univ.Constraint.union local local'); + uctx_univ_variables = vars; + uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes; + uctx_weak_constraints = weak; } (* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *) (* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *) let add_universe_constraints ctx cstrs = let univs, local = ctx.uctx_local in - let vars, local' = process_universe_constraints ctx cstrs in - { ctx with uctx_local = (univs, Univ.Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } + let vars, weak, local' = process_universe_constraints ctx cstrs in + { ctx with + uctx_local = (univs, Univ.Constraint.union local local'); + uctx_univ_variables = vars; + uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes; + uctx_weak_constraints = weak; } let constrain_variables diff ctx = let univs, local = ctx.uctx_local in @@ -274,7 +296,7 @@ let constrain_variables diff ctx = let reference_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try Libnames.Ident (Loc.tag @@ Option.get (Univ.LMap.find l map_rev).uname) + try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> Universes.reference_of_level l @@ -282,7 +304,7 @@ let pr_uctx_level uctx l = Libnames.pr_reference (reference_of_level uctx l) type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl let error_unbound_universes left uctx = let open Univ in @@ -305,7 +327,7 @@ let universe_context ~names ~extensible uctx = let levels = ContextSet.levels uctx.uctx_local in let newinst, left = List.fold_right - (fun (loc,id) (newinst, acc) -> + (fun { CAst.loc; v = id } (newinst, acc) -> let l = try UNameMap.find id (fst uctx.uctx_names) with Not_found -> assert false @@ -325,7 +347,7 @@ let check_universe_context_set ~names ~extensible uctx = if extensible then () else let open Univ in - let left = List.fold_left (fun left (loc,id) -> + let left = List.fold_left (fun left { CAst.loc; v = id } -> let l = try UNameMap.find id (fst uctx.uctx_names) with Not_found -> assert false @@ -474,6 +496,13 @@ let new_univ_variable ?loc rigid name uctx_initial_universes = initial} in uctx', u +let make_with_initial_binders e us = + let uctx = make e in + List.fold_left + (fun uctx { CAst.loc; v = id } -> + fst (new_univ_variable ?loc univ_rigid (Some id) uctx)) + uctx us + let add_global_univ uctx u = let initial = UGraph.add_universe u true uctx.uctx_initial_universes @@ -554,16 +583,18 @@ let fix_undefined_variables uctx = let refresh_undefined_univ_variables uctx = let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in - let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) + let subst_fn u = Univ.subst_univs_level_level subst u in + let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc) uctx.uctx_univ_algebraic Univ.LSet.empty in let vars = Univ.LMap.fold (fun u v acc -> - Univ.LMap.add (Univ.subst_univs_level_level subst u) + Univ.LMap.add (subst_fn u) (Option.map (Univ.subst_univs_level_universe subst) v) acc) uctx.uctx_univ_variables Univ.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 = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) (Univ.ContextSet.levels ctx') g in let initial = declare uctx.uctx_initial_universes in @@ -573,18 +604,20 @@ 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_initial_universes = initial } in + uctx_initial_universes = initial; + uctx_weak_constraints = weak; } in uctx', subst -let normalize uctx = - let ((vars',algs'), us') = - Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables - uctx.uctx_univ_algebraic +let minimize uctx = + let open Universes in + let ((vars',algs'), us') = + normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables + uctx.uctx_univ_algebraic uctx.uctx_weak_constraints in if Univ.ContextSet.equal us' uctx.uctx_local then uctx else let us', universes = - Universes.refresh_constraints uctx.uctx_initial_universes us' + refresh_constraints uctx.uctx_initial_universes us' in { uctx_names = uctx.uctx_names; uctx_local = us'; @@ -592,7 +625,8 @@ let normalize uctx = uctx_univ_variables = vars'; uctx_univ_algebraic = algs'; uctx_universes = universes; - uctx_initial_universes = uctx.uctx_initial_universes } + uctx_initial_universes = uctx.uctx_initial_universes; + uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) } let universe_of_name uctx s = UNameMap.find s (fst uctx.uctx_names) @@ -604,3 +638,10 @@ let update_sigma_env uctx env = uctx_universes = univs } in merge true univ_rigid eunivs eunivs.uctx_local + +let pr_weak prl {uctx_weak_constraints=weak} = + let open Pp in + prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak) + +(** Deprecated *) +let normalize = minimize diff --git a/engine/uState.mli b/engine/uState.mli index 6657d6047d..48c38fafc8 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines universe unification states which are part of evarmaps. @@ -24,6 +26,8 @@ val empty : t val make : UGraph.t -> t +val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t + val is_empty : t -> bool val union : t -> t -> t @@ -68,6 +72,8 @@ val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes (** {5 Constraints handling} *) +val drop_weak_constraints : bool ref + val add_constraints : t -> Univ.Constraint.t -> t (** @raise UniversesDiffer when universes differ @@ -129,10 +135,13 @@ val fix_undefined_variables : t -> t val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst +(** Universe minimization *) +val minimize : t -> t val normalize : t -> t +[@@ocaml.deprecated "Alias of UState.minimize"] type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl (** [check_univ_decl ctx decl] @@ -157,3 +166,5 @@ val update_sigma_env : t -> Environ.env -> t val pr_uctx_level : t -> Univ.Level.t -> Pp.t val reference_of_level : t -> Univ.Level.t -> Libnames.reference + +val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t diff --git a/engine/universes.ml b/engine/universes.ml index 3a00f0fd1d..e5f9212a71 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Sorts @@ -16,7 +18,10 @@ open Univ open Globnames open Nametab -let reference_of_level l = +module UPairs = OrderedType.UnorderedPair(Univ.Level) +module UPairSet = Set.Make (UPairs) + +let reference_of_level l = CAst.make @@ match Level.name l with | Some (d, n as na) -> let qid = @@ -24,8 +29,8 @@ let reference_of_level l = with Not_found -> let name = Id.of_string_soft (string_of_int n) in Libnames.make_qualid d name - in Libnames.Qualid (Loc.tag @@ qid) - | None -> Libnames.Ident (Loc.tag @@ Id.of_string_soft (Level.to_string l)) + in Libnames.Qualid qid + | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l)) let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l) @@ -92,14 +97,14 @@ let register_universe_binders ref ubinders = if not (Id.Map.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) -type univ_name_list = Name.t Loc.located list +type univ_name_list = Misctypes.lname list let universe_binders_with_opt_names ref levels = function | None -> universe_binders_of_global ref | Some udecl -> if Int.equal(List.length levels) (List.length udecl) then - List.fold_left2 (fun acc (_,na) lvl -> match na with + List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with | Anonymous -> acc | Name na -> Names.Id.Map.add na lvl acc) empty_binders udecl levels @@ -112,53 +117,60 @@ let universe_binders_with_opt_names ref levels = function let set_minimization = ref true let is_set_minimization () = !set_minimization -type universe_constraint_type = ULe | UEq | ULub - -type universe_constraint = Universe.t * universe_constraint_type * Universe.t +type universe_constraint = + | ULe of Universe.t * Universe.t + | UEq of Universe.t * Universe.t + | ULub of Level.t * Level.t + | UWeak of Level.t * Level.t module Constraints = struct module S = Set.Make( struct type t = universe_constraint - let compare_type c c' = - match c, c' with - | ULe, ULe -> 0 - | ULe, _ -> -1 - | _, ULe -> 1 - | UEq, UEq -> 0 - | UEq, _ -> -1 - | ULub, ULub -> 0 - | ULub, _ -> 1 - - let compare (u,c,v) (u',c',v') = - let i = compare_type c c' in - if Int.equal i 0 then - let i' = Universe.compare u u' in - if Int.equal i' 0 then Universe.compare v v' - else - if c != ULe && Universe.compare u v' = 0 && Universe.compare v u' = 0 then 0 - else i' - else i + let compare x y = + match x, y with + | ULe (u, v), ULe (u', v') -> + let i = Universe.compare u u' in + if Int.equal i 0 then Universe.compare v v' + else i + | UEq (u, v), UEq (u', v') -> + let i = Universe.compare u u' in + if Int.equal i 0 then Universe.compare v v' + else if Universe.equal u v' && Universe.equal v u' then 0 + else i + | ULub (u, v), ULub (u', v') | UWeak (u, v), UWeak (u', v') -> + let i = Level.compare u u' in + if Int.equal i 0 then Level.compare v v' + else if Level.equal u v' && Level.equal v u' then 0 + else i + | ULe _, _ -> -1 + | _, ULe _ -> 1 + | UEq _, _ -> -1 + | _, UEq _ -> 1 + | ULub _, _ -> -1 + | _, ULub _ -> 1 end) include S - - let add (l,d,r as cst) s = - if Universe.equal l r then s - else add cst s - let tr_dir = function - | ULe -> Le - | UEq -> Eq - | ULub -> Eq + let is_trivial = function + | ULe (u, v) | UEq (u, v) -> Universe.equal u v + | ULub (u, v) | UWeak (u, v) -> Level.equal u v - let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ " + let add cst s = + if is_trivial cst then s + else add cst s + + let pr_one = function + | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v + | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v + | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v + | UWeak (u, v) -> Level.pr u ++ str " ~ " ++ Level.pr v let pr c = - fold (fun (u1,op,u2) pp_std -> - pp_std ++ Universe.pr u1 ++ str (op_str op) ++ - Universe.pr u2 ++ fnl ()) c (str "") + fold (fun cst pp_std -> + pp_std ++ pr_one cst ++ fnl ()) c (str "") let equal x y = x == y || equal x y @@ -172,13 +184,13 @@ type 'a universe_constrained = 'a * universe_constraints type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints let enforce_eq_instances_univs strict x y c = - let d = if strict then ULub else UEq in + let mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in let ax = Instance.to_array x and ay = Instance.to_array y in if Array.length ax != Array.length ay then CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++ Pp.str " instances of different lengths."); CArray.fold_right2 - (fun x y -> Constraints.add (Universe.make x, d, Universe.make y)) + (fun x y -> Constraints.add (mk x y)) ax ay c let enforce_univ_constraint (u,d,v) = @@ -205,30 +217,65 @@ let subst_univs_constraints subst csts = (fun c cstrs -> subst_univs_constraint subst c cstrs) csts Constraint.empty -let subst_univs_universe_constraint fn (u,d,v) = - let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in +let level_subst_of f = + fun l -> + try let u = f l in + match Universe.level u with + | None -> l + | Some l -> l + with Not_found -> l + +let subst_univs_universe_constraint fn = function + | ULe (u, v) -> + let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in + if Universe.equal u' v' then None + else Some (ULe (u',v')) + | UEq (u, v) -> + let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in if Universe.equal u' v' then None - else Some (u',d,v') + else Some (ULe (u',v')) + | ULub (u, v) -> + let u' = level_subst_of fn u and v' = level_subst_of fn v in + if Level.equal u' v' then None + else Some (ULub (u',v')) + | UWeak (u, v) -> + let u' = level_subst_of fn u and v' = level_subst_of fn v in + if Level.equal u' v' then None + else Some (UWeak (u',v')) let subst_univs_universe_constraints subst csts = Constraints.fold (fun c -> Option.fold_right Constraints.add (subst_univs_universe_constraint subst c)) csts Constraints.empty - -let to_constraints g s = - let tr (x,d,y) acc = - let add l d l' acc = Constraint.add (l,Constraints.tr_dir d,l') acc in - match Universe.level x, d, Universe.level y with - | Some l, (ULe | UEq | ULub), Some l' -> add l d l' acc - | _, ULe, Some l' -> enforce_leq x y acc - | _, ULub, _ -> acc - | _, d, _ -> - let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in - if f g x y then acc else - raise (Invalid_argument - "to_constraints: non-trivial algebraic constraint between universes") - in Constraints.fold tr s Constraint.empty +let to_constraints ~force_weak g s = + let invalid () = + raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes") + in + let tr cst acc = + match cst with + | ULub (l, l') -> Constraint.add (l, Eq, l') acc + | UWeak (l, l') when force_weak -> Constraint.add (l, Eq, l') acc + | UWeak _-> acc + | ULe (l, l') -> + begin match Universe.level l, Universe.level l' with + | Some l, Some l' -> Constraint.add (l, Le, l') acc + | None, Some _ -> enforce_leq l l' acc + | _, None -> + if UGraph.check_leq g l l' + then acc + else invalid () + end + | UEq (l, l') -> + begin match Universe.level l, Universe.level l' with + | Some l, Some l' -> Constraint.add (l, Eq, l') acc + | None, _ | _, None -> + if UGraph.check_eq g l l' + then acc + else invalid () + end + in + Constraints.fold tr s Constraint.empty (** Variant of [eq_constr_univs_infer] taking kind-of-term functions, to expose subterms of [m] and [n], arguments. *) @@ -240,54 +287,21 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = [kind1,kind2], because [kind1] and [kind2] may be different, typically evaluating [m] and [n] in different evar maps. *) let cstrs = ref accu in - let eq_universes strict = UGraph.check_eq_instances univs in + let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + match fold (Constraints.singleton (UEq (u1, u2))) !cstrs with | None -> false | Some accu -> cstrs := accu; true in - let rec eq_constr' m n = - Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' nargs m n in - let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in + let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in if res then Some !cstrs else None -let compare_head_gen_proj env equ eqs eqc' m n = - match kind m, kind n with - | Proj (p, c), App (f, args) - | App (f, args), Proj (p, c) -> - (match kind f with - | Const (p', u) when Constant.equal (Projection.constant p) p' -> - let pb = Environ.lookup_projection p env in - let npars = pb.Declarations.proj_npars in - if Array.length args == npars + 1 then - eqc' c args.(npars) - else false - | _ -> false) - | _ -> Constr.compare_head_gen equ eqs eqc' m n - -let eq_constr_universes_proj env m n = - if m == n then true, Constraints.empty - else - let cstrs = ref Constraints.empty in - let eq_universes strict l l' = - cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - (cstrs := Constraints.add - (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs; - true) - in - let rec eq_constr' m n = - m == n || compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n - in - let res = eq_constr' m n in - res, !cstrs - (* Generator of levels *) type universe_id = DirPath.t * int @@ -543,14 +557,6 @@ let choose_canonical ctx flexible algs s = let canon = LSet.choose algs in canon, (global, rigid, LSet.remove canon flexible) -let level_subst_of f = - fun l -> - try let u = f l in - match Universe.level u with - | None -> l - | Some l -> l - with Not_found -> l - let subst_univs_fn_constr f c = let changed = ref false in let fu = Univ.subst_univs_universe f in @@ -912,7 +918,7 @@ let minimize_univ_variables ctx us algs left right cstrs = else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs) us (ctx, us, algs, lbounds, cstrs) -let normalize_context_set ctx us algs = +let normalize_context_set g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in let uf = UF.create () in (** Keep the Prop/Set <= i constraints separate for minimization *) @@ -932,7 +938,7 @@ let normalize_context_set ctx us algs = else (smallles, Constraint.add cstr noneqs)) csts (Constraint.empty, Constraint.empty) in - let csts = + let csts = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) @@ -970,7 +976,7 @@ let normalize_context_set ctx us algs = let noneqs = Constraint.union noneqs smallles in let partition = UF.partition uf in let flex x = LMap.mem x us in - let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s -> + let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s -> let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in (* Add equalities for globals which can't be merged anymore. *) let cstrs = LSet.fold (fun g cst -> @@ -982,16 +988,41 @@ let normalize_context_set ctx us algs = Constraint.add (canon, Univ.Eq, g) cst) rigid cstrs in - let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in - let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in let canonu = Some (Universe.make canon) in let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in - (LSet.diff ctx flexible, subst, us, cstrs)) - (ctx, LMap.empty, us, Constraint.empty) partition + (LSet.diff ctx flexible, us, cstrs)) + (ctx, us, Constraint.empty) partition in + (* Process weak constraints: when one side is flexible and the 2 + universes are unrelated unify them. *) + let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) -> + let norm = let us = ref us in level_subst_of (normalize_univ_variable_opt_subst us) in + let u = norm u and v = norm v in + let set_to a b = + (LSet.remove a ctx, + LMap.add a (Some (Universe.make b)) us, + UGraph.enforce_constraint (a,Eq,b) g) + in + if UGraph.check_constraint g (u,Le,v) || UGraph.check_constraint g (v,Le,u) + then acc + else + if LMap.mem u us + then set_to u v + else if LMap.mem v us + then set_to v u + else acc) + weak (ctx, us, g) in (* Noneqs is now in canonical form w.r.t. equality constraints, and contains only inequality constraints. *) - let noneqs = subst_univs_level_constraints subst noneqs in + let noneqs = + let us = ref us in + let norm = level_subst_of (normalize_univ_variable_opt_subst us) in + Constraint.fold (fun (u,d,v) noneqs -> + let u = norm u and v = norm v in + if d != Lt && Level.equal u v then noneqs + else Constraint.add (u,d,v) noneqs) + noneqs Constraint.empty + in (* Compute the left and right set of flexible variables, constraints mentionning other variables remain in noneqs. *) let noneqs, ucstrsl, ucstrsr = diff --git a/engine/universes.mli b/engine/universes.mli index cb6e2ba1b6..4823c57463 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -12,6 +14,9 @@ open Constr open Environ open Univ +(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *) +module UPairSet : CSet.S with type elt = (Level.t * Level.t) + val set_minimization : bool ref val is_set_minimization : unit -> bool @@ -35,7 +40,7 @@ val empty_binders : universe_binders val register_universe_binders : Globnames.global_reference -> universe_binders -> unit val universe_binders_of_global : Globnames.global_reference -> universe_binders -type univ_name_list = Name.t Loc.located list +type univ_name_list = Misctypes.lname list (** [universe_binders_with_opt_names ref u l] @@ -67,14 +72,21 @@ val new_sort_in_family : Sorts.family -> Sorts.t When doing conversion of universes, not only do we have =/<= constraints but also Lub constraints which correspond to unification of two levels which might not be necessary if unfolding is performed. + + UWeak constraints come from irrelevant universes in cumulative polymorphism. *) -type universe_constraint_type = ULe | UEq | ULub +type universe_constraint = + | ULe of Universe.t * Universe.t + | UEq of Universe.t * Universe.t + | ULub of Level.t * Level.t + | UWeak of Level.t * Level.t -type universe_constraint = Universe.t * universe_constraint_type * Universe.t module Constraints : sig include Set.S with type elt = universe_constraint + val is_trivial : universe_constraint -> bool + val pr : t -> Pp.t end @@ -90,7 +102,9 @@ val subst_univs_universe_constraints : universe_subst_fn -> val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function -val to_constraints : UGraph.t -> Constraints.t -> Constraint.t +(** With [force_weak] UWeak constraints are turned into equalities, + otherwise they're forgotten. *) +val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of {!eq_constr_univs_infer} taking kind-of-term functions, to expose @@ -100,10 +114,6 @@ val eq_constr_univs_infer_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option -(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe constraints in [c]. *) -val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained - (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) @@ -165,9 +175,10 @@ val make_opt_subst : universe_opt_subst -> universe_subst_fn val subst_opt_univs_constr : universe_opt_subst -> constr -> constr -val normalize_context_set : ContextSet.t -> +val normalize_context_set : UGraph.t -> ContextSet.t -> universe_opt_subst (* The defined and undefined variables *) -> - LSet.t (* univ variables that can be substituted by algebraics *) -> + LSet.t (* univ variables that can be substituted by algebraics *) -> + UPairSet.t (* weak equality constraints *) -> (universe_opt_subst * LSet.t) in_universe_context_set val normalize_univ_variables : universe_opt_subst -> diff --git a/engine/univops.ml b/engine/univops.ml index df25d87252..76dbaa250a 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Univ diff --git a/engine/univops.mli b/engine/univops.mli index 30fcc43681..d1585414c1 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr |