aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-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/inferCumulativity.ml234
-rw-r--r--pretyping/inferCumulativity.mli14
-rw-r--r--pretyping/patternops.ml1
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--pretyping/reductionops.ml4
12 files changed, 15 insertions, 262 deletions
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/inferCumulativity.ml b/pretyping/inferCumulativity.ml
deleted file mode 100644
index ed069eace0..0000000000
--- a/pretyping/inferCumulativity.ml
+++ /dev/null
@@ -1,234 +0,0 @@
-(************************************************************************)
-(* * 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) *)
-(************************************************************************)
-
-open Reduction
-open Declarations
-open Constr
-open Univ
-open Variance
-open Util
-
-type inferred = IrrelevantI | CovariantI
-
-(** Throughout this module we modify a map [variances] from local
- universes to [inferred]. It starts as a trivial mapping to
- [Irrelevant] and every time we encounter a local universe we
- restrict it accordingly.
- [Invariant] universes are removed from the map.
-*)
-exception TrivialVariance
-
-let maybe_trivial variances =
- if LMap.is_empty variances then raise TrivialVariance
- else variances
-
-let infer_level_eq u variances =
- maybe_trivial (LMap.remove u variances)
-
-let infer_level_leq u variances =
- (* can only set Irrelevant -> Covariant so nontrivial *)
- LMap.update u (function
- | None -> None
- | Some CovariantI as x -> x
- | Some IrrelevantI -> Some CovariantI)
- variances
-
-let infer_generic_instance_eq variances u =
- Array.fold_left (fun variances u -> infer_level_eq u variances)
- variances (Instance.to_array u)
-
-let infer_cumulative_ind_instance cv_pb mind_variance variances u =
- Array.fold_left2 (fun variances varu u ->
- match cv_pb, varu with
- | _, Irrelevant -> variances
- | _, Invariant | CONV, Covariant -> infer_level_eq u variances
- | CUMUL, Covariant -> infer_level_leq u variances)
- variances mind_variance (Instance.to_array u)
-
-let infer_inductive_instance cv_pb env variances ind nargs u =
- let mind = Environ.lookup_mind (fst ind) env in
- match mind.mind_variance with
- | None -> infer_generic_instance_eq variances u
- | Some mind_variance ->
- if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs)
- then infer_generic_instance_eq variances u
- else infer_cumulative_ind_instance cv_pb mind_variance variances u
-
-let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u =
- let mind = Environ.lookup_mind mi env in
- match mind.mind_variance with
- | None -> infer_generic_instance_eq variances u
- | Some _ ->
- if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs)
- then infer_generic_instance_eq variances u
- else variances (* constructors are convertible at common supertype *)
-
-let infer_sort cv_pb variances s =
- match cv_pb with
- | CONV ->
- LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances
- | CUMUL ->
- LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances
-
-let infer_table_key infos variances c =
- let open Names in
- match c with
- | ConstKey (_, u) ->
- infer_generic_instance_eq variances u
- | VarKey _ | RelKey _ -> variances
-
-let whd_stack (infos, tab) hd stk = CClosure.whd_stack infos tab hd stk
-
-let rec infer_fterm cv_pb infos variances hd stk =
- Control.check_for_interrupt ();
- let hd,stk = whd_stack infos hd stk in
- let open CClosure in
- match fterm_of hd with
- | FAtom a ->
- begin match kind a with
- | Sort s -> infer_sort cv_pb variances s
- | Meta _ -> infer_stack infos variances stk
- | _ -> assert false
- end
- | FEvar ((_,args),e) ->
- let variances = infer_stack infos variances stk in
- infer_vect infos variances (Array.map (mk_clos e) args)
- | FRel _ -> infer_stack infos variances stk
- | FInt _ -> infer_stack infos variances stk
- | FFlex fl ->
- let variances = infer_table_key infos variances fl in
- infer_stack infos variances stk
- | FProj (_,c) ->
- let variances = infer_fterm CONV infos variances c [] in
- infer_stack infos variances stk
- | FLambda _ ->
- let (_,ty,bd) = destFLambda mk_clos hd in
- let variances = infer_fterm CONV infos variances ty [] in
- infer_fterm CONV infos variances bd []
- | FProd (_,dom,codom,e) ->
- let variances = infer_fterm CONV infos variances dom [] in
- infer_fterm cv_pb infos variances (mk_clos (Esubst.subs_lift e) codom) []
- | FInd (ind, u) ->
- let variances =
- if Instance.is_empty u then variances
- else
- let nargs = stack_args_size stk in
- infer_inductive_instance cv_pb (info_env (fst infos)) variances ind nargs u
- in
- infer_stack infos variances stk
- | FConstruct (ctor,u) ->
- let variances =
- if Instance.is_empty u then variances
- else
- let nargs = stack_args_size stk in
- infer_constructor_instance_eq (info_env (fst infos)) variances ctor nargs u
- in
- infer_stack infos variances stk
- | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) ->
- let n = Array.length cl in
- let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in
- let le = Esubst.subs_liftn n e in
- let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in
- infer_stack infos variances stk
-
- (* Removed by whnf *)
- | FLOCKED | FCaseT _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false
-
-and infer_stack infos variances (stk:CClosure.stack) =
- match stk with
- | [] -> variances
- | z :: stk ->
- let open CClosure in
- let variances = match z with
- | Zapp v -> infer_vect infos variances v
- | Zproj _ -> variances
- | Zfix (fx,a) ->
- let variances = infer_fterm CONV infos variances fx [] in
- infer_stack infos variances a
- | ZcaseT (ci,p,br,e) ->
- let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
- infer_vect infos variances (Array.map (mk_clos e) br)
- | Zshift _ -> variances
- | Zupdate _ -> variances
- | Zprimitive (_,_,rargs,kargs) ->
- let variances = List.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances rargs in
- let variances = List.fold_left (fun variances (_,c) -> infer_fterm CONV infos variances c []) variances kargs in
- variances
- in
- infer_stack infos variances stk
-
-and infer_vect infos variances v =
- Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
-
-let infer_term cv_pb env variances c =
- let open CClosure in
- let infos = (create_clos_infos all env, create_tab ()) in
- infer_fterm cv_pb infos variances (CClosure.inject c) []
-
-let infer_arity_constructor is_arity env variances arcn =
- let infer_typ typ (env,variances) =
- match typ with
- | Context.Rel.Declaration.LocalAssum (_, typ') ->
- (Environ.push_rel typ env, infer_term CUMUL env variances typ')
- | Context.Rel.Declaration.LocalDef _ -> assert false
- in
- let typs, codom = Reduction.dest_prod env arcn in
- let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in
- (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j}
- i is irrelevant, j is invariant. *)
- if not is_arity then infer_term CUMUL env variances codom else variances
-
-open Entries
-
-let infer_inductive_core env params entries uctx =
- let uarray = Instance.to_array @@ UContext.instance uctx in
- if Array.is_empty uarray then raise TrivialVariance;
- let env = Environ.push_context uctx env in
- let variances =
- Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances)
- LMap.empty uarray
- in
- let env, params = Typeops.check_context env params in
- let variances = List.fold_left (fun variances entry ->
- let variances = infer_arity_constructor true
- env variances entry.mind_entry_arity
- in
- List.fold_left (infer_arity_constructor false env)
- variances entry.mind_entry_lc)
- variances
- entries
- in
- Array.map (fun u -> match LMap.find u variances with
- | exception Not_found -> Invariant
- | IrrelevantI -> Irrelevant
- | CovariantI -> Covariant)
- uarray
-
-let infer_inductive env mie =
- let open Entries in
- let { mind_entry_params = params;
- mind_entry_inds = entries; } = mie
- in
- let variances =
- match mie.mind_entry_variance with
- | None -> None
- | Some _ ->
- let uctx = match mie.mind_entry_universes with
- | Monomorphic_entry _ -> assert false
- | Polymorphic_entry (_,uctx) -> uctx
- in
- try Some (infer_inductive_core env params entries uctx)
- with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant)
- in
- { mie with mind_entry_variance = variances }
-
-let dummy_variance = let open Entries in function
- | Monomorphic_entry _ -> assert false
- | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant
diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli
deleted file mode 100644
index a234e334d1..0000000000
--- a/pretyping/inferCumulativity.mli
+++ /dev/null
@@ -1,14 +0,0 @@
-(************************************************************************)
-(* * 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) *)
-(************************************************************************)
-
-val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
- Entries.mutual_inductive_entry
-
-val dummy_variance : Entries.universes_entry -> Univ.Variance.t array
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 0ca39f0404..7e140f4399 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -4,7 +4,6 @@ Locusops
Pretype_errors
Reductionops
Inductiveops
-InferCumulativity
Arguments_renaming
Retyping
Vnorm
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 11:24:51 +0000