aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml1
-rw-r--r--pretyping/detyping.ml5
-rw-r--r--pretyping/evarsolve.ml2
-rw-r--r--pretyping/glob_ops.ml14
-rw-r--r--pretyping/inductiveops.ml104
-rw-r--r--pretyping/inductiveops.mli12
-rw-r--r--pretyping/typing.ml7
7 files changed, 135 insertions, 10 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index aa1c23f52..0dd3c5944 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1427,6 +1427,7 @@ and match_current pb (initial,tomatch) =
let case =
make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
in
+ let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in
Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
{ uj_val = applist (case, inst);
uj_type = prod_applist !(pb.evdref) typ inst }
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index df89d9eac..5a54c6f05 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -690,7 +690,10 @@ and detype_r d flags avoid env sigma t =
let c' =
try
let pb = Environ.lookup_projection p (snd env) in
- let body = pb.Declarations.proj_body in
+ (** FIXME: handle mutual records *)
+ let ind = (pb.Declarations.proj_ind, 0) in
+ let bodies = Inductiveops.legacy_match_projection (snd env) ind in
+ let body = bodies.(pb.Declarations.proj_arg) in
let ty = Retyping.get_type_of (snd env) sigma c in
let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
let body' = strip_lam_assum body in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index aefae1ecc..8afb9b942 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -929,7 +929,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
with Not_found ->
match expand_alias_once evd aliases t with
| None -> raise Not_found
- | Some c -> aux k c in
+ | Some c -> aux k (lift k c) in
try
let c = aux 0 c_in_env_extended_with_k_binders in
Invertible (UniqueProjection (c,!effects))
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 71a457280..11cfd2040 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -269,8 +269,9 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
| GCases (_,rtntypopt,tml,pl) ->
let fold_pattern acc {v=(idl,p,c)} = f (List.fold_right g idl v) acc c in
let fold_tomatch (v',acc) (tm,(na,onal)) =
- (Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'')
- (Name.fold_right g na v') onal,
+ ((if rtntypopt = None then v' else
+ Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'')
+ (Name.fold_right g na v') onal),
f v acc tm) in
let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in
let acc = Option.fold_left (f v') acc rtntypopt in
@@ -281,6 +282,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
| GIf (c,rtntyp,b1,b2) ->
f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2
| GRec (_,idl,bll,tyl,bv) ->
+ let v' = Array.fold_right g idl v in
let f' i acc fid =
let v,acc =
List.fold_left
@@ -288,7 +290,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
(Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty))
(v,acc)
bll.(i) in
- f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in
+ f v' (f v acc tyl.(i)) (bv.(i)) in
Array.fold_left_i f' acc idl
| GCast (c,k) ->
let acc = match k with
@@ -412,8 +414,10 @@ let loc_of_glob_constr c = c.CAst.loc
(**********************************************************************)
(* Alpha-renaming *)
+exception UnsoundRenaming
+
let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l
-let test_id l id = if collide_id l id then raise Not_found
+let test_id l id = if collide_id l id then raise UnsoundRenaming
let test_na l na = Name.iter (test_id l) na
let update_subst na l =
@@ -427,8 +431,6 @@ let update_subst na l =
else na,l)
na (na,l)
-exception UnsoundRenaming
-
let rename_var l id =
try
let id' = Id.List.assoc id l in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b1ab2d2b7..1a790be64 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -454,6 +454,110 @@ let build_branch_type env sigma dep p cs =
(**************************************************)
+(** From a rel context describing the constructor arguments,
+ build an expansion function.
+ The term built is expecting to be substituted first by
+ a substitution of the form [params, x : ind params] *)
+let compute_projections env (kn, _ as ind) =
+ let open Term in
+ let mib = Environ.lookup_mind kn env in
+ let indu = match mib.mind_universes with
+ | Monomorphic_ind _ -> mkInd ind
+ | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx)
+ | Cumulative_ind ctx ->
+ mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx))
+ in
+ let x = match mib.mind_record with
+ | None | Some None ->
+ anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+ | Some (Some (id, _, _)) -> Name id
+ in
+ (** FIXME: handle mutual records *)
+ let pkt = mib.mind_packets.(0) in
+ let { mind_consnrealargs; mind_consnrealdecls } = pkt in
+ let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
+ let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in
+ let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
+ let mp, dp, l = MutInd.repr3 kn in
+ (** We build a substitution smashing the lets in the record parameters so
+ that typechecking projections requires just a substitution and not
+ matching with a parameter context. *)
+ let indty =
+ (* [ty] = [Ind inst] is typed in context [params] *)
+ let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
+ let ty = mkApp (indu, inst) in
+ (* [Ind inst] is typed in context [params-wo-let] *)
+ ty
+ in
+ let ci =
+ let print_info =
+ { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+ { ci_ind = ind;
+ ci_npar = nparamargs;
+ ci_cstr_ndecls = mind_consnrealdecls;
+ ci_cstr_nargs = mind_consnrealargs;
+ ci_pp_info = print_info }
+ in
+ let len = List.length ctx in
+ let compat_body ccl i =
+ (* [ccl] is defined in context [params;x:indty] *)
+ (* [ccl'] is defined in context [params;x:indty;x:indty] *)
+ let ccl' = liftn 1 2 ccl in
+ let p = mkLambda (x, lift 1 indty, ccl') in
+ let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
+ let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
+ it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
+ in
+ let projections decl (j, pbs, subst) =
+ match decl with
+ | LocalDef (na,c,t) ->
+ (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
+ to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
+ let c = liftn 1 j c in
+ (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
+ to [params, x:I |- c(params,proj1 x,..,projj x)] *)
+ let c1 = substl subst c in
+ (* From [params, x:I |- subst:field1,..,fieldj]
+ to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
+ is represented with instance of field1 last *)
+ let subst = c1 :: subst in
+ (j+1, pbs, subst)
+ | LocalAssum (na,t) ->
+ match na with
+ | Name id ->
+ let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+ (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)]
+ to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *)
+ let t = liftn 1 j t in
+ (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)]
+ to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *)
+ (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
+ to [params, x:I |- t(proj1 x,..,projj x)] *)
+ let ty = substl subst t in
+ let term = mkProj (Projection.make kn true, mkRel 1) in
+ let fterm = mkProj (Projection.make kn false, mkRel 1) in
+ let compat = compat_body ty (j - 1) in
+ let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
+ let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
+ let body = (etab, etat, compat) in
+ (j + 1, body :: pbs, fterm :: subst)
+ | Anonymous ->
+ anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+ in
+ let (_, pbs, subst) =
+ List.fold_right projections ctx (1, [], [])
+ in
+ Array.rev_of_list pbs
+
+let legacy_match_projection env ind =
+ Array.map pi3 (compute_projections env ind)
+
+let compute_projections ind mib =
+ let ans = compute_projections ind mib in
+ Array.map (fun (prj, ty, _) -> (prj, ty)) ans
+
+(**************************************************)
+
let extract_mrectype sigma t =
let open EConstr in
let (t, l) = decompose_app sigma t in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index b0d714b03..aa53f7e67 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -194,6 +194,18 @@ val make_case_or_project :
val make_default_case_info : env -> case_style -> inductive -> case_info
i*)
+val compute_projections : Environ.env -> inductive -> (constr * types) array
+(** Given a primitive record type, for every field computes the eta-expanded
+ projection and its type. *)
+
+val legacy_match_projection : Environ.env -> inductive -> constr array
+(** Given a record type, computes the legacy match-based projection of the
+ projections.
+
+ BEWARE: such terms are ill-typed, and should thus only be used in upper
+ layers. The kernel will probably badly fail if presented with one of
+ those. *)
+
(********************)
val type_of_inductive_knowing_conclusion :
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index bffe36eea..cf34ac016 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -197,10 +197,13 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj =
(* FIXME: might depend on the level of actual parameters!*)
let check_allowed_sort env sigma ind c p =
- let pj = Retyping.get_judgment_of env sigma p in
- let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in
let specif = Global.lookup_inductive (fst ind) in
let sorts = elim_sorts specif in
+ let pj = Retyping.get_judgment_of env sigma p in
+ let _, s = splay_prod env sigma pj.uj_type in
+ let ksort = match EConstr.kind sigma s with
+ | Sort s -> Sorts.family (ESorts.kind sigma s)
+ | _ -> error_elim_arity env sigma ind sorts c pj None in
if not (List.exists ((==) ksort) sorts) then
let s = inductive_sort_family (snd specif) in
error_elim_arity env sigma ind sorts c pj
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-25 21:27:49 +0000