From 2f1ee61f9700e3d73e637a82f9089807efab186a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Jul 2017 14:28:04 +0200 Subject: Allocation-friendly detyping of term arrays. This is important for externalization big terms. We were indeed allocating twice as much as needed lists for the application node case, as the Array.map_to_list function is exactly List.map o Array.to_list. We could probably tweak this function instead, at the expense that order of evaluation is not guaranteed. I'm not willing to do that though. --- pretyping/detyping.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'pretyping/detyping.ml') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index f830d4be3..98f6c24aa 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -475,8 +475,8 @@ let rec detype flags avoid env sigma t = CAst.make @@ GApp (f',args''@args') | _ -> GApp (f',args') in - mkapp (detype flags avoid env sigma f) - (Array.map_to_list (detype flags avoid env sigma) args) + mkapp (detype flags avoid env sigma f) + (detype_array flags avoid env sigma args) | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = @@ -694,6 +694,13 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in GLetIn (na', c, t, r) +and detype_array flags avoid env sigma args = + let ans = ref [] in + for i = Array.length args - 1 downto 0 do + ans := detype flags avoid env sigma args.(i) :: !ans; + done; + !ans + let detype_rel_context ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in let rec aux avoid env = function -- cgit v1.2.3 From d5ee6e2d24d0f9b42499b507fe9d03555c9ddf45 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 26 Jul 2017 15:29:16 +0200 Subject: Add a comment regarding the specialization of the combinator in Detyping. --- pretyping/detyping.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'pretyping/detyping.ml') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 98f6c24aa..ebd270e9f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -694,6 +694,8 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in GLetIn (na', c, t, r) +(** We use a dedicated function here to prevent overallocation from + Array.map_to_list. *) and detype_array flags avoid env sigma args = let ans = ref [] in for i = Array.length args - 1 downto 0 do -- cgit v1.2.3