diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-04 15:26:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-17 11:44:04 +0200 |
| commit | e43710b391c278ac7fcb808ec28d720b4317660c (patch) | |
| tree | 00c9b48f65ed5567e1fcac31a344944d6ea148b9 /pretyping | |
| parent | a4839aa1ff076a8938ca182615a93d6afe748860 (diff) | |
Remove the proj_body field from the kernel.
This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.
Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.
Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 5 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 3 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 8 |
3 files changed, 15 insertions, 1 deletions
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/inductiveops.ml b/pretyping/inductiveops.ml index 4ad32fc66..1a790be64 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -549,6 +549,9 @@ let compute_projections env (kn, _ as ind) = 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 diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 506cdd8c9..aa53f7e67 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -198,6 +198,14 @@ 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 : |