From d6f1694326bec39c1fe41f38c7c9bd37c1a8c27b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 25 Nov 2019 15:26:20 +0100
Subject: Cleanup substitution API.

---
 kernel/esubst.ml  | 33 ---------------------------------
 kernel/esubst.mli | 10 +---------
 2 files changed, 1 insertion(+), 42 deletions(-)

(limited to 'kernel')

diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 3e8502b988..558ff96486 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -93,11 +93,6 @@ let subs_shft = function
   | (n, s)            -> SHIFT (n,s)
 let subs_shft s = if Int.equal (fst s) 0 then snd s else subs_shft s
 
-let subs_shift_cons = function
-  (0, s, t)           -> CONS(t,s)
-| (k, SHIFT(n,s1), t) -> CONS(t,SHIFT(k+n, s1))
-| (k, s, t)           -> CONS(t,SHIFT(k, s));;
-
 (* Tests whether a substitution is equal to the identity *)
 let rec is_subs_id = function
     ESID _     -> true
@@ -156,31 +151,3 @@ let rec lift_subst mk_cl s1 s2 = match s1 with
       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
-    | ESID _, _ -> s2
-    | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2)
-    | _, CONS(x,s') ->
-        CONS(Array.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
-    | CONS(x,s), SHIFT(k,s') ->
-        let lg = Array.length x in
-        if k == lg then comp mk_cl s s'
-        else if k > lg then comp mk_cl s (SHIFT(k-lg, s'))
-        else comp mk_cl (CONS(Array.sub x 0 (lg-k), s)) s'
-    | CONS(x,s), LIFT(k,s') ->
-        let lg = Array.length x in
-        if k == lg then CONS(x, comp mk_cl s s')
-        else if k > lg then CONS(x, comp mk_cl s (LIFT(k-lg, s')))
-        else
-          CONS(Array.sub x (lg-k) k,
-               comp mk_cl (CONS(Array.sub x 0 (lg-k),s)) s')
-    | LIFT(k,s), SHIFT(k',s') ->
-        if k<k'
-        then subs_shft(k, comp mk_cl s (subs_shft(k'-k, s')))
-        else subs_shft(k', comp mk_cl (subs_liftn (k-k') s) s')
-    | LIFT(k,s), LIFT(k',s') ->
-        if k<k'
-        then subs_liftn k (comp mk_cl s (subs_liftn (k'-k) s'))
-        else subs_liftn k' (comp mk_cl (subs_liftn (k-k') s) s')
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index 4239e42adc..551c6f1732 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -18,11 +18,7 @@
     - SHIFT(n,S)          = (^n o S) terms in S are relocated with n vars
     - LIFT(n,S)           = (%n S) stands for ((^n o S).n...1)
          (corresponds to S crossing n binders) *)
-type 'a subs = private
-  | ESID of int
-  | CONS of 'a array * 'a subs
-  | SHIFT of int * 'a subs
-  | LIFT of int * 'a subs
+type 'a subs
 
 (** Derived constructors granting basic invariants *)
 val subs_id : int -> 'a subs
@@ -31,9 +27,6 @@ val subs_shft: int * 'a subs -> 'a subs
 val subs_lift: 'a subs -> 'a subs
 val subs_liftn: int -> 'a subs -> 'a subs
 
-(** [subs_shift_cons(k,s,[|t1..tn|])] builds (^k s).t1..tn *)
-val subs_shift_cons: int * 'a subs * 'a array -> 'a subs
-
 (** [expand_rel k subs] expands de Bruijn [k] in the explicit substitution
     [subs]. The result is either (Inl(lams,v)) when the variable is
     substituted by value [v] under lams binders (i.e. v *has* to be
@@ -51,7 +44,6 @@ val is_subs_id: 'a subs -> bool
     mk_clos is used when a closure has to be created, i.e. when
     s1 is applied on an element of s2.
 *)
-val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
 
 (** {6 Compact representation } *)
 (** Compact representation of explicit relocations
-- 
cgit v1.2.3