aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.ml2
-rw-r--r--pretyping/detyping.ml1
-rw-r--r--pretyping/detyping.mli4
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/glob_ops.ml6
-rw-r--r--pretyping/glob_ops.mli3
-rw-r--r--pretyping/glob_term.ml3
-rw-r--r--pretyping/keys.ml162
-rw-r--r--pretyping/keys.mli23
-rw-r--r--pretyping/patternops.ml1
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/unification.ml32
-rw-r--r--pretyping/unification.mli6
15 files changed, 228 insertions, 26 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 534c0ca20b..a86d237164 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -47,7 +47,7 @@ let discharge_rename_args = function
| _, (ReqGlobal (c, names), _ as req) when not (isVarRef c && Lib.is_in_section c) ->
(try
let vars = Lib.variable_section_segment_of_reference c in
- let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
+ let var_names = List.map (NamedDecl.get_id %> Name.mk_name) vars in
let names' = var_names @ names in
Some (ReqGlobal (c, names), (c, names'))
with Not_found -> Some req)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 2061b41292..e8c83c7de9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -25,7 +25,6 @@ open Namegen
open Libnames
open Globnames
open Mod_subst
-open Decl_kinds
open Context.Named.Declaration
open Ltac_pretype
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index cc9f520583..9eb014aa62 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -57,10 +57,10 @@ val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (
val share_pattern_names :
(Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int ->
- (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list ->
+ (Name.t * binding_kind * 'b option * 'a) list ->
Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern ->
Pattern.constr_pattern ->
- (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list * 'a * 'a
+ (Name.t * binding_kind * 'b option * 'a) list * 'a * 'a
val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index be21a3a60d..288a349b8b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -773,7 +773,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
(* Evar must be undefined since we have flushed evars *)
let () = if !debug_unification then
let open Pp in
- Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
+ Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
match (flex_kind_of_term flags env evd term1 sk1,
flex_kind_of_term flags env evd term2 sk2) with
| Flexible (sp1,al1), Flexible (sp2,al2) ->
@@ -1569,7 +1569,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
let () = if !debug_unification then
let open Pp in
- Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++
+ Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++
Termops.Internal.print_constr_env env evd t1 ++ cut () ++
Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
let app_empty = Array.is_empty l1 && Array.is_empty l2 in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6bde3dfd81..93f5923474 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -67,9 +67,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with
| (UNamed _ | UAnonymous _), _ -> false
let binding_kind_eq bk1 bk2 = match bk1, bk2 with
- | Decl_kinds.Explicit, Decl_kinds.Explicit -> true
- | Decl_kinds.Implicit, Decl_kinds.Implicit -> true
- | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false
+ | Explicit, Explicit -> true
+ | Implicit, Implicit -> true
+ | (Explicit | Implicit), _ -> false
let case_style_eq s1 s2 = let open Constr in match s1, s2 with
| LetStyle, LetStyle -> true
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 467b72e520..37aa31d094 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -48,6 +48,9 @@ val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g -> 'a glob_const
val map_glob_constr :
(glob_constr -> glob_constr) -> glob_constr -> glob_constr
+(** Equality on [binding_kind] *)
+val binding_kind_eq : binding_kind -> binding_kind -> bool
+
(** Ensure traversal from left to right *)
val map_glob_constr_left_to_right :
(glob_constr -> glob_constr) -> glob_constr -> glob_constr
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 7c859a5332..10e9d60fd5 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -17,7 +17,6 @@
arguments and pattern-matching compilation are not. *)
open Names
-open Decl_kinds
type existential_name = Id.t
@@ -66,6 +65,8 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t
type cases_pattern = [ `any ] cases_pattern_g
+type binding_kind = Explicit | Implicit
+
(** Representation of an internalized (or in other words globalized) term. *)
type 'a glob_constr_r =
| GRef of GlobRef.t * glob_level list option
diff --git a/pretyping/keys.ml b/pretyping/keys.ml
new file mode 100644
index 0000000000..f8eecd80d4
--- /dev/null
+++ b/pretyping/keys.ml
@@ -0,0 +1,162 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** Keys for unification and indexing *)
+
+open Names
+open Constr
+open Libobject
+open Globnames
+
+type key =
+ | KGlob of GlobRef.t
+ | KLam
+ | KLet
+ | KProd
+ | KSort
+ | KCase
+ | KFix
+ | KCoFix
+ | KRel
+ | KInt
+
+module KeyOrdered = struct
+ type t = key
+
+ let hash gr =
+ match gr with
+ | KGlob gr -> 9 + GlobRef.Ordered.hash gr
+ | KLam -> 0
+ | KLet -> 1
+ | KProd -> 2
+ | KSort -> 3
+ | KCase -> 4
+ | KFix -> 5
+ | KCoFix -> 6
+ | KRel -> 7
+ | KInt -> 8
+
+ let compare gr1 gr2 =
+ match gr1, gr2 with
+ | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2
+ | _, KGlob _ -> -1
+ | KGlob _, _ -> 1
+ | k, k' -> Int.compare (hash k) (hash k')
+
+ let equal k1 k2 =
+ match k1, k2 with
+ | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2
+ | _, KGlob _ -> false
+ | KGlob _, _ -> false
+ | k, k' -> k == k'
+end
+
+module Keymap = HMap.Make(KeyOrdered)
+module Keyset = Keymap.Set
+
+(* Mapping structure for references to be considered equivalent *)
+
+let keys = Summary.ref Keymap.empty ~name:"Keys_decl"
+
+let add_kv k v m =
+ try Keymap.modify k (fun k' vs -> Keyset.add v vs) m
+ with Not_found -> Keymap.add k (Keyset.singleton v) m
+
+let add_keys k v =
+ keys := add_kv k v (add_kv v k !keys)
+
+let equiv_keys k k' =
+ k == k' || KeyOrdered.equal k k' ||
+ try Keyset.mem k' (Keymap.find k !keys)
+ with Not_found -> false
+
+(** Registration of keys as an object *)
+
+let load_keys _ (_,(ref,ref')) =
+ add_keys ref ref'
+
+let cache_keys o =
+ load_keys 1 o
+
+let subst_key subst k =
+ match k with
+ | KGlob gr -> KGlob (subst_global_reference subst gr)
+ | _ -> k
+
+let subst_keys (subst,(k,k')) =
+ (subst_key subst k, subst_key subst k')
+
+let discharge_key = function
+ | KGlob (GlobRef.VarRef _ as g) when Lib.is_in_section g -> None
+ | x -> Some x
+
+let discharge_keys (_,(k,k')) =
+ match discharge_key k, discharge_key k' with
+ | Some x, Some y -> Some (x, y)
+ | _ -> None
+
+type key_obj = key * key
+
+let inKeys : key_obj -> obj =
+ declare_object @@ superglobal_object "KEYS"
+ ~cache:cache_keys
+ ~subst:(Some subst_keys)
+ ~discharge:discharge_keys
+
+let declare_equiv_keys ref ref' =
+ Lib.add_anonymous_leaf (inKeys (ref,ref'))
+
+let constr_key kind c =
+ try
+ let rec aux k =
+ match kind k with
+ | Const (c, _) -> KGlob (GlobRef.ConstRef c)
+ | Ind (i, u) -> KGlob (GlobRef.IndRef i)
+ | Construct (c,u) -> KGlob (GlobRef.ConstructRef c)
+ | Var id -> KGlob (GlobRef.VarRef id)
+ | App (f, _) -> aux f
+ | Proj (p, _) -> KGlob (GlobRef.ConstRef (Projection.constant p))
+ | Cast (p, _, _) -> aux p
+ | Lambda _ -> KLam
+ | Prod _ -> KProd
+ | Case _ -> KCase
+ | Fix _ -> KFix
+ | CoFix _ -> KCoFix
+ | Rel _ -> KRel
+ | Meta _ -> raise Not_found
+ | Evar _ -> raise Not_found
+ | Sort _ -> KSort
+ | LetIn _ -> KLet
+ | Int _ -> KInt
+ in Some (aux c)
+ with Not_found -> None
+
+open Pp
+
+let pr_key pr_global = function
+ | KGlob gr -> pr_global gr
+ | KLam -> str"Lambda"
+ | KLet -> str"Let"
+ | KProd -> str"Product"
+ | KSort -> str"Sort"
+ | KCase -> str"Case"
+ | KFix -> str"Fix"
+ | KCoFix -> str"CoFix"
+ | KRel -> str"Rel"
+ | KInt -> str"Int"
+
+let pr_keyset pr_global v =
+ prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)
+
+let pr_mapping pr_global k v =
+ pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v
+
+let pr_keys pr_global =
+ Keymap.fold (fun k v acc -> pr_mapping pr_global k v ++ fnl () ++ acc) !keys (mt())
diff --git a/pretyping/keys.mli b/pretyping/keys.mli
new file mode 100644
index 0000000000..a7adf7791b
--- /dev/null
+++ b/pretyping/keys.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+type key
+
+val declare_equiv_keys : key -> key -> unit
+(** Declare two keys as being equivalent. *)
+
+val equiv_keys : key -> key -> bool
+(** Check equivalence of keys. *)
+
+val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
+(** Compute the head key of a term. *)
+
+val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t
+(** Pretty-print the mapping *)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 99e3c5025e..ccc3b6e83c 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -18,7 +18,6 @@ open Context
open Glob_term
open Pp
open Mod_subst
-open Decl_kinds
open Pattern
open Environ
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c28c3ab730..4fed526cfc 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1193,7 +1193,7 @@ let path_convertible env sigma p q =
let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in
let mkGVar id = DAst.make @@ Glob_term.GVar(id) in
let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in
- let mkGLambda(n,t,b) = DAst.make @@ Glob_term.GLambda(n,Decl_kinds.Explicit,t,b) in
+ let mkGLambda(n,t,b) = DAst.make @@ Glob_term.GLambda(n,Explicit,t,b) in
let mkGHole () = DAst.make @@ Glob_term.GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) in
let path_to_gterm p =
match p with
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 34a6cecc95..0ca39f0404 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -35,4 +35,5 @@ Indrec
GlobEnv
Cases
Pretyping
+Keys
Unification
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7362955eb7..df161b747a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -918,7 +918,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
let () = if !debug_RAKAM then
let open Pp in
let pr c = Termops.Internal.print_constr_env env sigma c in
- Feedback.msg_notice
+ Feedback.msg_debug
(h 0 (str "<<" ++ pr x ++
str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++
str "|" ++ cut () ++ Stack.pr pr stack ++
@@ -927,7 +927,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
let c0 = EConstr.kind sigma x in
let fold () =
let () = if !debug_RAKAM then
- let open Pp in Feedback.msg_notice (str "<><><><><>") in
+ let open Pp in Feedback.msg_debug (str "<><><><><>") in
((EConstr.of_kind c0, stack),cst_l)
in
match c0 with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a9eb43e573..4d34139ec0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -254,6 +254,10 @@ let unify_r2l x = x
let sort_eqns = unify_r2l
*)
+type allowed_evars =
+| AllowAll
+| AllowFun of (Evar.t -> bool)
+
type core_unify_flags = {
modulo_conv_on_closed_terms : TransparentState.t option;
(* What this flag controls was activated with all constants transparent, *)
@@ -287,8 +291,8 @@ type core_unify_flags = {
(* This allowed for instance to unify "forall x:?A, ?B x" with "A' -> B'" *)
(* when ?B is a Meta. *)
- frozen_evars : Evar.Set.t;
- (* Evars of this set are considered axioms and never instantiated *)
+ allowed_evars : allowed_evars;
+ (* Evars that are allowed to be instantiated *)
(* Useful e.g. for autorewrite *)
restrict_conv_on_strict_subterms : bool;
@@ -339,7 +343,7 @@ let default_core_unify_flags () =
check_applied_meta_types = true;
use_pattern_unification = true;
use_meta_bound_pattern_unification = true;
- frozen_evars = Evar.Set.empty;
+ allowed_evars = AllowAll;
restrict_conv_on_strict_subterms = false;
modulo_betaiota = true;
modulo_eta = true;
@@ -417,6 +421,10 @@ let default_no_delta_unify_flags ts =
resolve_evars = false
}
+let allow_new_evars sigma =
+ let undefined = Evd.undefined_map sigma in
+ AllowFun (fun evk -> not (Evar.Map.mem evk undefined))
+
(* Default flags for looking for subterms in elimination tactics *)
(* Not used in practice at the current date, to the exception of *)
(* allow_K) because only closed terms are involved in *)
@@ -424,9 +432,7 @@ let default_no_delta_unify_flags ts =
(* call w_unify for induction/destruct/case/elim (13/6/2011) *)
let elim_core_flags sigma = { (default_core_unify_flags ()) with
modulo_betaiota = false;
- frozen_evars =
- fold_undefined (fun evk _ evars -> Evar.Set.add evk evars)
- sigma Evar.Set.empty;
+ allowed_evars = allow_new_evars sigma;
}
let elim_flags_evars sigma =
@@ -600,8 +606,12 @@ let do_reduce ts (env, nb) sigma c =
Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state
ts env sigma (c, Stack.empty))
+let is_evar_allowed flags evk = match flags.allowed_evars with
+| AllowAll -> true
+| AllowFun f -> f evk
+
let isAllowedEvar sigma flags c = match EConstr.kind sigma c with
- | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars)
+ | Evar (evk,_) -> is_evar_allowed flags evk
| _ -> false
@@ -749,7 +759,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cM)
| Evar (evk,_ as ev), Evar (evk',_)
- when not (Evar.Set.mem evk flags.frozen_evars)
+ when is_evar_allowed flags evk
&& Evar.equal evk evk' ->
begin match constr_cmp cv_pb env sigma flags cM cN with
| Some sigma ->
@@ -758,14 +768,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
sigma,metasubst,((curenv,ev,cN)::evarsubst)
end
| Evar (evk,_ as ev), _
- when not (Evar.Set.mem evk flags.frozen_evars)
+ when is_evar_allowed flags evk
&& not (occur_evar sigma evk cN) ->
let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in
if Int.Set.subset cnvars cmvars then
sigma,metasubst,((curenv,ev,cN)::evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cN)
| _, Evar (evk,_ as ev)
- when not (Evar.Set.mem evk flags.frozen_evars)
+ when is_evar_allowed flags evk
&& not (occur_evar sigma evk cM) ->
let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in
if Int.Set.subset cmvars cnvars then
@@ -1554,7 +1564,7 @@ let default_matching_core_flags sigma =
check_applied_meta_types = true;
use_pattern_unification = false;
use_meta_bound_pattern_unification = false;
- frozen_evars = Evar.Map.domain (Evd.undefined_map sigma);
+ allowed_evars = allow_new_evars sigma;
restrict_conv_on_strict_subterms = false;
modulo_betaiota = false;
modulo_eta = false;
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 0ee71246d8..d7ddbcb721 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -13,6 +13,10 @@ open EConstr
open Environ
open Evd
+type allowed_evars =
+| AllowAll
+| AllowFun of (Evar.t -> bool)
+
type core_unify_flags = {
modulo_conv_on_closed_terms : TransparentState.t option;
use_metas_eagerly_in_conv_on_closed_terms : bool;
@@ -22,7 +26,7 @@ type core_unify_flags = {
check_applied_meta_types : bool;
use_pattern_unification : bool;
use_meta_bound_pattern_unification : bool;
- frozen_evars : Evar.Set.t;
+ allowed_evars : allowed_evars;
restrict_conv_on_strict_subterms : bool;
modulo_betaiota : bool;
modulo_eta : bool;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 16:01:09 +0000