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.

1 files changed, 23 insertions, 0 deletions

diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 4b8edf63f..9fc3b11d7 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -134,6 +134,29 @@ let rec exp_rel lams k subs =
 
 let expand_rel k subs = exp_rel 0 k subs
 
+let rec subs_map f = function
+| ESID _ as s -> s
+| CONS (x, s) -> CONS (Array.map f x, subs_map f s)
+| SHIFT (n, s) -> SHIFT (n, subs_map f s)
+| LIFT (n, s) -> LIFT (n, subs_map f s)
+
+let rec lift_subst mk_cl s1 s2 = match s1 with
+| ELID -> subs_map (fun c -> mk_cl ELID c) s2
+| ELSHFT(s, k) -> subs_shft(k, lift_subst mk_cl s s2)
+| ELLFT (k, s) ->
+  match s2 with
+  | CONS(x,s') ->
+      CONS(CArray.Fun1.map mk_cl s1 x, lift_subst mk_cl s1 s')
+  | ESID n -> lift_subst mk_cl s (ESID (n + k))
+  | SHIFT(k',s') ->
+      if k<k'
+      then subs_shft(k, lift_subst mk_cl s (subs_shft(k'-k, s')))
+      else subs_shft(k', lift_subst mk_cl (el_liftn (k-k') s) s')
+  | LIFT(k',s') ->
+      if k<k'
+      then subs_liftn k (lift_subst mk_cl s (subs_liftn (k'-k) s'))
+      else subs_liftn k' (lift_subst mk_cl (el_liftn (k-k') s) s')
+
 let rec comp mk_cl s1 s2 =
   match (s1, s2) with
     | _, ESID _ -> s1