From 9953fc3c125d0bdd39e3bd5801040f406f2e708f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 22 May 2018 08:58:53 +0200 Subject: Faster and cleaner fconstr-to-constr conversion function. We untangle the implementation in several ways. - No higher-order self argument function as there is only one caller. - Compute composition of lifts + substitution on terms using a dedicated function instead of mk_clos followed by to_constr. - Take more advantage of identity substitutions. --- kernel/esubst.mli | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'kernel/esubst.mli') diff --git a/kernel/esubst.mli b/kernel/esubst.mli index a674c425a..475b64f47 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -72,3 +72,10 @@ val el_liftn : int -> lift -> lift val el_lift : lift -> lift val reloc_rel : int -> lift -> int val is_lift_id : lift -> bool + +(** Lift applied to substitution: [lift_subst mk_clos el s] computes a + substitution equivalent to applying el then s. Argument + mk_clos is used when a closure has to be created, i.e. when + el is applied on an element of s. +*) +val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs -- cgit v1.2.3