aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml6
-rw-r--r--pretyping/cbv.ml5
-rw-r--r--pretyping/classops.ml57
-rw-r--r--pretyping/classops.mli18
-rw-r--r--pretyping/coercion.ml7
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/reductionops.ml22
-rw-r--r--pretyping/reductionops.mli4
-rw-r--r--pretyping/tacred.ml6
-rw-r--r--pretyping/vnorm.ml3
10 files changed, 61 insertions, 69 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6a63fb02f8..ad33297f0a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -373,6 +373,11 @@ let ltac_interp_realnames lvar = function
| t, IsInd (ty,ind,realnal) -> t, IsInd (ty,ind,List.map (ltac_interp_name lvar) realnal)
| _ as x -> x
+let is_patvar pat =
+ match DAst.get pat with
+ | PatVar _ -> true
+ | _ -> false
+
let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) =
let loc = loc_of_glob_constr tomatch in
let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
@@ -381,6 +386,7 @@ let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) =
let typ = nf_evar !evdref j.uj_type in
lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar;
let t =
+ if realnames = None && pats <> [] && List.for_all is_patvar pats then NotInd (None,typ) else
try try_find_ind env !evdref typ realnames
with Not_found ->
unify_tomatch_with_patterns evdref env loc typ pats realnames in
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 3758008189..da6e26cc4b 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -280,8 +280,9 @@ let rec norm_head info env t stack =
| Var id -> norm_head_ref 0 info env stack (VarKey id)
| Const sp ->
- Reductionops.reduction_effect_hook (env_of_infos info.infos) info.sigma t (lazy (reify_stack t stack));
- norm_head_ref 0 info env stack (ConstKey sp)
+ Reductionops.reduction_effect_hook (env_of_infos info.infos) info.sigma
+ (fst sp) (lazy (reify_stack t stack));
+ norm_head_ref 0 info env stack (ConstKey sp)
| LetIn (_, b, _, c) ->
(* zeta means letin are contracted; delta without zeta means we *)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 7ac08e755e..542fb5456c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -42,18 +42,15 @@ type coe_typ = GlobRef.t
module CoeTypMap = Refmap_env
type coe_info_typ = {
- coe_value : constr;
- coe_type : types;
+ coe_value : GlobRef.t;
coe_local : bool;
- coe_context : Univ.ContextSet.t;
coe_is_identity : bool;
coe_is_projection : Projection.Repr.t option;
- coe_param : int }
+ coe_param : int;
+}
let coe_info_typ_equal c1 c2 =
- let eq_constr c1 c2 = Termops.eq_constr Evd.empty (EConstr.of_constr c1) (EConstr.of_constr c2) in
- eq_constr c1.coe_value c2.coe_value &&
- eq_constr c1.coe_type c2.coe_type &&
+ GlobRef.equal c1.coe_value c2.coe_value &&
c1.coe_local == c2.coe_local &&
c1.coe_is_identity == c2.coe_is_identity &&
c1.coe_is_projection == c2.coe_is_projection &&
@@ -77,9 +74,7 @@ module IntMap = Map.Make(Int)
let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
-type coe_index = coe_info_typ
-
-type inheritance_path = coe_index list
+type inheritance_path = coe_info_typ list
(* table des classes, des coercions et graphe d'heritage *)
@@ -300,31 +295,25 @@ let lookup_path_to_fun_from env sigma s =
let lookup_path_to_sort_from env sigma s =
apply_on_class_of env sigma s lookup_path_to_sort_from_class
+let mkNamed = function
+ | GlobRef.ConstRef c -> EConstr.mkConst c
+ | VarRef v -> EConstr.mkVar v
+ | ConstructRef c -> EConstr.mkConstruct c
+ | IndRef i -> EConstr.mkInd i
+
let get_coercion_constructor env coe =
- let c, _ =
- Reductionops.whd_all_stack env Evd.empty (EConstr.of_constr coe.coe_value)
- in
- match EConstr.kind Evd.empty (** FIXME *) c with
- | Construct (cstr,u) ->
- (cstr, Inductiveops.constructor_nrealargs cstr -1)
- | _ ->
- raise Not_found
+ let evd = Evd.from_env env in
+ let red x = fst (Reductionops.whd_all_stack env evd x) in
+ match EConstr.kind evd (red (mkNamed coe.coe_value)) with
+ | Constr.Construct (c, _) ->
+ c, Inductiveops.constructor_nrealargs c -1
+ | _ -> raise Not_found
let lookup_pattern_path_between env (s,t) =
let i = inductive_class_of s in
let j = inductive_class_of t in
List.map (get_coercion_constructor env) (ClPairMap.find (i,j) !inheritance_graph)
-(* coercion_value : coe_index -> unsafe_judgment * bool *)
-
-let coercion_value { coe_value = c; coe_type = t; coe_context = ctx;
- coe_is_identity = b; coe_is_projection = b' } =
- let subst, ctx = UnivGen.fresh_universe_context_set_instance ctx in
- let c' = Vars.subst_univs_level_constr subst c
- and t' = Vars.subst_univs_level_constr subst t in
- (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx
-
-(* pretty-print functions are now in Pretty *)
(* rajouter une coercion dans le graphe *)
let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref =
@@ -442,17 +431,13 @@ let cache_coercion env sigma (_, c) =
let () = add_class c.coercion_target in
let is, _ = class_info c.coercion_source in
let it, _ = class_info c.coercion_target in
- let value, ctx = UnivGen.fresh_global_instance env c.coercion_type in
- let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in
- let typ = EConstr.Unsafe.to_constr typ in
let xf =
- { coe_value = value;
- coe_type = typ;
- coe_context = ctx;
+ { coe_value = c.coercion_type;
coe_local = c.coercion_local;
coe_is_identity = c.coercion_is_id;
coe_is_projection = c.coercion_is_proj;
- coe_param = c.coercion_params } in
+ coe_param = c.coercion_params;
+ } in
let () = add_new_coercion c.coercion_type xf in
add_coercion_in_graph env sigma (xf,is,it)
@@ -531,8 +516,6 @@ let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps
Lib.add_anonymous_leaf (inCoercion c)
(* For printing purpose *)
-let get_coercion_value v = v.coe_value
-
let pr_cl_index = Bijint.Index.print
let classes () = Bijint.dom !class_tab
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 8df085e15c..af00c0a8dc 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -39,16 +39,19 @@ type cl_info_typ = {
type coe_typ = GlobRef.t
(** This is the type of infos for declared coercions *)
-type coe_info_typ
+type coe_info_typ = {
+ coe_value : GlobRef.t;
+ coe_local : bool;
+ coe_is_identity : bool;
+ coe_is_projection : Projection.Repr.t option;
+ coe_param : int;
+}
(** [cl_index] is the type of class keys *)
type cl_index
-(** [coe_index] is the type of coercion keys *)
-type coe_index
-
(** This is the type of paths from a class to another *)
-type inheritance_path = coe_index list
+type inheritance_path = coe_info_typ list
(** {6 Access to classes infos } *)
@@ -79,8 +82,6 @@ val declare_coercion :
(** {6 Access to coercions infos } *)
val coercion_exists : coe_typ -> bool
-val coercion_value : coe_index -> (unsafe_judgment * bool * Projection.Repr.t option) Univ.in_universe_context_set
-
(** {6 Lookup functions for coercion paths } *)
(** @raise Not_found in the following functions when no path exists *)
@@ -105,10 +106,9 @@ val install_path_printer :
val string_of_class : cl_typ -> string
val pr_class : cl_typ -> Pp.t
val pr_cl_index : cl_index -> Pp.t
-val get_coercion_value : coe_index -> Constr.t
val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
val classes : unit -> cl_typ list
-val coercions : unit -> coe_index list
+val coercions : unit -> coe_info_typ list
(** [hide_coercion] returns the number of params to skip if the coercion must
be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index c6c2f57dd4..5e3821edf1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -369,8 +369,11 @@ let apply_coercion env sigma p hj typ_cl =
let j,t,evd =
List.fold_left
(fun (ja,typ_cl,sigma) i ->
- let ((fv,isid,isproj),ctx) = coercion_value i in
- let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+ let isid = i.coe_is_identity in
+ let isproj = i.coe_is_projection in
+ let sigma, c = new_global sigma i.coe_value in
+ let typ = Retyping.get_type_of env sigma c in
+ let fv = make_judge c typ in
let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
let sigma, jres =
apply_coercion_args env sigma true isproj argl fv
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b379cdf410..ec0ff73062 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -633,7 +633,7 @@ let is_predicate_explicitly_dep env sigma pred arsign =
dependency status (of course, Anonymous implies non
dependent, but not conversely).
- From Coq > 8.2, using or not the the effective dependency of
+ From Coq > 8.2, using or not the effective dependency of
the predicate is parametrable! *)
begin match na with
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 63c7ab3c69..ba40262815 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -47,29 +47,28 @@ open Libobject
type effect_name = string
(** create a persistent set to store effect functions *)
-module ConstrMap = Map.Make (Constr)
(* Table bindings a constant to an effect *)
-let constant_effect_table = Summary.ref ~name:"reduction-side-effect" ConstrMap.empty
+let constant_effect_table = Summary.ref ~name:"reduction-side-effect" Cmap.empty
(* Table bindings function key to effective functions *)
let effect_table = Summary.ref ~name:"reduction-function-effect" String.Map.empty
(** a test to know whether a constant is actually the effect function *)
-let reduction_effect_hook env sigma termkey c =
+let reduction_effect_hook env sigma con c =
try
- let funkey = ConstrMap.find termkey !constant_effect_table in
+ let funkey = Cmap.find con !constant_effect_table in
let effect = String.Map.find funkey !effect_table in
effect env sigma (Lazy.force c)
with Not_found -> ()
-let cache_reduction_effect (_,(termkey,funkey)) =
- constant_effect_table := ConstrMap.add termkey funkey !constant_effect_table
+let cache_reduction_effect (_,(con,funkey)) =
+ constant_effect_table := Cmap.add con funkey !constant_effect_table
-let subst_reduction_effect (subst,(termkey,funkey)) =
- (subst_mps subst termkey,funkey)
+let subst_reduction_effect (subst,(con,funkey)) =
+ (subst_constant subst con,funkey)
-let inReductionEffect : Constr.constr * string -> obj =
+let inReductionEffect : Constant.t * string -> obj =
declare_object {(default_object "REDUCTION-EFFECT") with
cache_function = cache_reduction_effect;
open_function = (fun i o -> if Int.equal i 1 then cache_reduction_effect o);
@@ -83,8 +82,7 @@ let declare_reduction_effect funkey f =
(** A function to set the value of the print function *)
let set_reduction_effect x funkey =
- let termkey = UnivGen.constr_of_global x in
- Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey))
+ Lib.add_anonymous_leaf (inReductionEffect (x,funkey))
(** Machinery to custom the behavior of the reduction *)
@@ -872,7 +870,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
| Some body -> whrec cst_l (body, stack)
| None -> fold ())
| Const (c,u as const) ->
- reduction_effect_hook env sigma (EConstr.to_constr sigma x)
+ reduction_effect_hook env sigma c
(lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack))));
if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then
let u' = EInstance.kind sigma u in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b44c642d43..07eeec9276 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -41,10 +41,10 @@ val declare_reduction_effect : effect_name ->
(Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit
(* [set_reduction_effect cst name] declares effect [name] to be called when [cst] is found *)
-val set_reduction_effect : GlobRef.t -> effect_name -> unit
+val set_reduction_effect : Constant.t -> effect_name -> unit
(* [effect_hook env sigma key term] apply effect associated to [key] on [term] *)
-val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constr.constr ->
+val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constant.t ->
Constr.constr Lazy.t -> unit
(** {6 Machinery about a stack of unfolded constant }
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 599a0f8162..8911a2f343 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -539,7 +539,7 @@ let reduce_mind_case_use_function func env sigma mia =
let match_eval_ref env sigma constr stack =
match EConstr.kind sigma constr with
| Const (sp, u) ->
- reduction_effect_hook env sigma (EConstr.to_constr sigma constr)
+ reduction_effect_hook env sigma sp
(lazy (EConstr.to_constr sigma (applist (constr,stack))));
if is_evaluable env (EvalConstRef sp) then Some (EvalConst sp, u) else None
| Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, EInstance.empty)
@@ -550,7 +550,7 @@ let match_eval_ref env sigma constr stack =
let match_eval_ref_value env sigma constr stack =
match EConstr.kind sigma constr with
| Const (sp, u) ->
- reduction_effect_hook env sigma (EConstr.to_constr sigma constr)
+ reduction_effect_hook env sigma sp
(lazy (EConstr.to_constr sigma (applist (constr,stack))));
if is_evaluable env (EvalConstRef sp) then
let u = EInstance.kind sigma u in
@@ -558,8 +558,6 @@ let match_eval_ref_value env sigma constr stack =
else
None
| Proj (p, c) when not (Projection.unfolded p) ->
- reduction_effect_hook env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma constr)
- (lazy (EConstr.to_constr sigma (applist (constr,stack))));
if is_evaluable env (EvalConstRef (Projection.constant p)) then
Some (mkProj (Projection.unfold p, c))
else None
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c944080503..255707dc7b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -209,6 +209,9 @@ and nf_evar env sigma evk stk =
| Zapp args :: stk ->
(** We assume that there is no consecutive Zapp nodes in a VM stack. Is that
really an invariant? *)
+ (** Let-bound arguments are present in the evar arguments but not in the
+ type, so we turn the let into a product. *)
+ let hyps = Context.Named.drop_bodies hyps in
let fold accu d = Term.mkNamedProd_or_LetIn d accu in
let t = List.fold_left fold concl hyps in
let t, args = nf_args env sigma args t in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 17:39:21 +0000