From 723f4434d7c715630533031f1bb1522d5d933ce5 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 4 Jan 2019 16:16:11 +0100 Subject: Remove Printing Primitive Projection Compatibility The code to generate the legacy bodies is moved to its only user in extraction. It almost seems like we could remove it (ie no special extraction code for primitive projection constants) but then we run into issues with automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets extracted to `type foo = nat` and (if we remove the special code) `let a = a`. --- pretyping/detyping.ml | 42 ++++++------------------------------------ pretyping/inductiveops.ml | 29 +---------------------------- pretyping/inductiveops.mli | 8 -------- 3 files changed, 7 insertions(+), 72 deletions(-) (limited to 'pretyping') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 517834f014..92a30dd508 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module CVars = Vars - open Pp open CErrors open Util @@ -175,16 +173,6 @@ let () = declare_bool_option optread = print_primproj_params; optwrite = (:=) print_primproj_params_value } -let print_primproj_compatibility_value = ref false -let print_primproj_compatibility () = !print_primproj_compatibility_value - -let () = declare_bool_option - { optdepr = false; - optname = "backwards-compatible printing of primitive projections"; - optkey = ["Printing";"Primitive";"Projection";"Compatibility"]; - optread = print_primproj_compatibility; - optwrite = (:=) print_primproj_compatibility_value } - (* Auxiliary function for MutCase printing *) (* [computable] tries to tell if the predicate typing the result is inferable*) @@ -702,30 +690,12 @@ and detype_r d flags avoid env sigma t = GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), [detype d flags avoid env sigma c]) else - if print_primproj_compatibility () && Projection.unfolded p then - (* Print the compatibility match version *) - let c' = - try - let ind = Projection.inductive p in - let bodies = Inductiveops.legacy_match_projection (snd env) ind in - let body = bodies.(Projection.arg p) 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 - let u = EInstance.kind sigma u in - let body' = CVars.subst_instance_constr u body' in - let body' = EConstr.of_constr body' in - substl (c :: List.rev args) body' - with Retyping.RetypeError _ | Not_found -> - anomaly (str"Cannot detype an unfolded primitive projection.") - in DAst.get (detype d flags avoid env sigma c') - else - if print_primproj_params () then - try - let c = Retyping.expand_projection (snd env) sigma p c [] in - DAst.get (detype d flags avoid env sigma c) - with Retyping.RetypeError _ -> noparams () - else noparams () + if print_primproj_params () then + try + let c = Retyping.expand_projection (snd env) sigma p c [] in + DAst.get (detype d flags avoid env sigma c) + with Retyping.RetypeError _ -> noparams () + else noparams () | Evar (evk,cl) -> let bound_to_itself_or_letin decl c = diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ff552c7caf..290bb60ba4 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -480,25 +480,6 @@ let compute_projections env (kn, i as ind) = (* [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 = pkt.mind_consnrealdecls; - ci_cstr_nargs = pkt.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 (proj_arg, j, pbs, subst) = match decl with | LocalDef (na,c,t) -> @@ -528,10 +509,9 @@ let compute_projections env (kn, i as ind) = 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 + let body = (etab, etat) in (proj_arg + 1, j + 1, body :: pbs, fterm :: subst) | Anonymous -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") @@ -541,13 +521,6 @@ let compute_projections env (kn, i 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 - (**************************************************) let extract_mrectype sigma t = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index b2e205115f..5a4257e175 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -194,14 +194,6 @@ 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 : -- cgit v1.2.3