aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/glob_ops.ml16
-rw-r--r--pretyping/glob_term.ml19
-rw-r--r--pretyping/inferCumulativity.ml93
-rw-r--r--pretyping/nativenorm.ml38
-rw-r--r--pretyping/patternops.ml24
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/vnorm.ml2
9 files changed, 99 insertions, 101 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index eaa5736336..062e3ca8b2 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -653,7 +653,7 @@ let detype_fix detype flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
let v = Array.map3
(fun c t i -> share_names detype flags (i+1) [] def_avoid def_env sigma c (lift n t))
bodies tys vn in
- GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+ GRec(GFix (Array.map (fun i -> Some i) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
Array.map (fun (bl,_,_) -> bl) v,
Array.map (fun (_,_,ty) -> ty) v,
Array.map (fun (_,bd,_) -> bd) v)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6da168711c..85b9faac77 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -106,19 +106,9 @@ let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) =
Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
Option.equal f c1 c2 && f t1 t2
-let fix_recursion_order_eq f o1 o2 = match o1, o2 with
- | GStructRec, GStructRec -> true
- | GWfRec c1, GWfRec c2 -> f c1 c2
- | GMeasureRec (c1, o1), GMeasureRec (c2, o2) ->
- f c1 c2 && Option.equal f o1 o2
- | (GStructRec | GWfRec _ | GMeasureRec _), _ -> false
-
-let fix_kind_eq f k1 k2 = match k1, k2 with
+let fix_kind_eq k1 k2 = match k1, k2 with
| GFix (a1, i1), GFix (a2, i2) ->
- let eq (i1, o1) (i2, o2) =
- Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2
- in
- Int.equal i1 i2 && Array.equal eq a1 a2
+ Int.equal i1 i2 && Array.equal (Option.equal Int.equal) a1 a2
| GCoFix i1, GCoFix i2 -> Int.equal i1 i2
| (GFix _ | GCoFix _), _ -> false
@@ -150,7 +140,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
f m1 m2 && Name.equal pat1 pat2 &&
Option.equal f p1 p2 && f c1 c2 && f t1 t2
| GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) ->
- fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 &&
+ fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 &&
Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 &&
Array.equal f c1 c2 && Array.equal f t1 t2
| GSort s1, GSort s2 -> glob_sort_eq s1 s2
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index c57cf88cc6..02cb294f6d 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -41,6 +41,12 @@ type glob_constraint = glob_level * Univ.constraint_type * glob_level
type sort_info = (Libnames.qualid * int) option list
type glob_sort = sort_info glob_sort_gen
+type glob_recarg = int option
+
+and glob_fix_kind =
+ | GFix of (glob_recarg array * int)
+ | GCoFix of int
+
(** Casts *)
type 'a cast_type =
@@ -78,7 +84,7 @@ type 'a glob_constr_r =
(** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *)
| GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
| GIf of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
- | GRec of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array *
+ | GRec of glob_fix_kind * Id.t array * 'a glob_decl_g list array *
'a glob_constr_g array * 'a glob_constr_g array
| GSort of glob_sort
| GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
@@ -88,15 +94,6 @@ and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
-and 'a fix_recursion_order_g =
- | GStructRec
- | GWfRec of 'a glob_constr_g
- | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option
-
-and 'a fix_kind_g =
- | GFix of ((int option * 'a fix_recursion_order_g) array * int)
- | GCoFix of int
-
and 'a predicate_pattern_g =
Name.t * (inductive * Name.t list) CAst.t option
(** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
@@ -117,9 +114,7 @@ type tomatch_tuples = [ `any ] tomatch_tuples_g
type cases_clause = [ `any ] cases_clause_g
type cases_clauses = [ `any ] cases_clauses_g
type glob_decl = [ `any ] glob_decl_g
-type fix_kind = [ `any ] fix_kind_g
type predicate_pattern = [ `any ] predicate_pattern_g
-type fix_recursion_order = [ `any ] fix_recursion_order_g
type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index fefc15dfb2..9f2397ec38 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -12,41 +12,44 @@ 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 [Variance.t]. It starts as a trivial mapping to
- [Irrelevant] and every time we encounter a local universe we
- restrict it accordingly. *)
+ 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 =
- if LMap.mem u variances
- then LMap.set u Variance.Invariant variances
- else variances
+ maybe_trivial (LMap.remove u variances)
let infer_level_leq u variances =
- match LMap.find u variances with
- | exception Not_found -> variances
- | varu -> LMap.set u (Variance.sup varu Variance.Covariant) 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 variance_pb cv_pb var =
- let open Variance in
- match cv_pb, var with
- | _, Irrelevant -> Irrelevant
- | _, Invariant -> Invariant
- | CONV, Covariant -> Invariant
- | CUMUL, Covariant -> Covariant
-
let infer_cumulative_ind_instance cv_pb mind_variance variances u =
Array.fold_left2 (fun variances varu u ->
- match LMap.find u variances with
- | exception Not_found -> variances
- | varu' ->
- LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances)
+ 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 =
@@ -182,6 +185,32 @@ let infer_arity_constructor is_arity env variances arcn =
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;
@@ -195,27 +224,11 @@ let infer_inductive env mie =
| Monomorphic_entry _ -> assert false
| Polymorphic_entry (_,uctx) -> uctx
in
- let uarray = Instance.to_array @@ UContext.instance uctx in
- let env = Environ.push_context uctx env in
- let variances =
- Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant 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
- let variances = Array.map (fun u -> LMap.find u variances) uarray in
- Some variances
+ 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) Variance.Irrelevant
+ | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 0003fc7280..0fcd6a9e9d 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -415,7 +415,7 @@ and nf_predicate env sigma ind mip params v pT =
and nf_evar env sigma evk args =
let evi = try Evd.find sigma evk with Not_found -> assert false in
let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
- let ty = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in
+ let ty = EConstr.to_constr ~abort_on_undefined_evars:false sigma @@ Evd.evar_concl evi in
if List.is_empty hyps then begin
assert (Int.equal (Array.length args) 0);
mkEvar (evk, [||]), ty
@@ -492,25 +492,23 @@ let native_norm env sigma c ty =
Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
*)
- let ml_filename, prefix = Nativelib.get_ml_filename () in
- let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in
- let profile = get_profiling_enabled () in
- match Nativelib.compile ml_filename code ~profile:profile with
- | true, fn ->
- if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ...");
- let profiler_pid = if profile then start_profiler () else None in
- let t0 = Sys.time () in
- Nativelib.call_linker ~fatal:true prefix fn (Some upd);
- let t1 = Sys.time () in
- if profile then stop_profiler profiler_pid;
- let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
- if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
- let res = nf_val env sigma !Nativelib.rt1 ty in
- let t2 = Sys.time () in
- let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in
- if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
- EConstr.of_constr res
- | _ -> anomaly (Pp.str "Compilation failure.")
+ let ml_filename, prefix = Nativelib.get_ml_filename () in
+ let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in
+ let profile = get_profiling_enabled () in
+ let fn = Nativelib.compile ml_filename code ~profile:profile in
+ if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ...");
+ let profiler_pid = if profile then start_profiler () else None in
+ let t0 = Sys.time () in
+ Nativelib.call_linker ~fatal:true prefix fn (Some upd);
+ let t1 = Sys.time () in
+ if profile then stop_profiler profiler_pid;
+ let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
+ if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+ let res = nf_val env sigma !Nativelib.rt1 ty in
+ let t2 = Sys.time () in
+ let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in
+ if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+ EConstr.of_constr res
let native_conv_generic pb sigma t =
Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b29afd1fd2..c788efda48 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -470,17 +470,19 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
PCase (info, pred, pat_of_raw metas vars c, brs)
| GRec (GFix (ln,n), ids, decls, tl, cl) ->
- if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then
- err ?loc (Pp.str "\"struct\" annotation is expected.")
- else
- let ln = Array.map (fst %> Option.get) ln in
- let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
- let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
- let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
- let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
- let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
- let names = Array.map (fun id -> Name id) ids in
- PFix ((ln,n), (names, tl, cl))
+ let get_struct_arg = function
+ | Some n -> n
+ | None -> err ?loc (Pp.str "\"struct\" annotation is expected.")
+ (* TODO why can't the annotation be omitted? *)
+ in
+ let ln = Array.map get_struct_arg ln in
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
+ let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
+ let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
+ let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
+ let names = Array.map (fun id -> Name id) ids in
+ PFix ((ln,n), (names, tl, cl))
| GRec (GCoFix n, ids, decls, tl, cl) ->
let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0f7676cd19..48d981082c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -607,10 +607,10 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env
fixpoints ?) *)
let possible_indexes =
Array.to_list (Array.mapi
- (fun i (n,_) -> match n with
+ (fun i annot -> match annot with
| Some n -> [n]
| None -> List.map_i (fun i _ -> i) 0 ctxtv.(i))
- vn)
+ vn)
in
let fixdecls = (names,ftys,fdefs) in
let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 71fbfe8716..1871609e18 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -53,7 +53,7 @@ type effect_name = string
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
+let effect_table = ref String.Map.empty
(** a test to know whether a constant is actually the effect function *)
let reduction_effect_hook env sigma con c =
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 62e9e477f7..1fe6545ce4 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -202,7 +202,7 @@ and nf_univ_args ~nb_univs mk env sigma stk =
and nf_evar env sigma evk stk =
let evi = try Evd.find sigma evk with Not_found -> assert false in
let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
- let concl = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in
+ let concl = EConstr.to_constr ~abort_on_undefined_evars:false sigma @@ Evd.evar_concl evi in
if List.is_empty hyps then
nf_stk env sigma (mkEvar (evk, [||])) concl stk
else match stk with
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 16:37:57 +0000