From 9953fc3c125d0bdd39e3bd5801040f406f2e708f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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.ml | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'kernel/esubst.ml')

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
-- 
cgit v1.2.3