Source file expand.ml

open UtilsLib
open Lambda

module Log = Xlog.Make (struct
  let name = "Expand"
end)

(** The {!Address} module implements addresses as used in Makoto's
    paper *)
module Address =
  struct
    type elt = Zero | One
        
    let make_add =
      List.map
        (function 
         | 0 -> Zero
         | 1 -> One
         | i -> raise (Invalid_argument (Printf.sprintf "%d is not part of a valid binary tree domain." i )))

    let elt_cmp e1 e2 =
      match e1, e2 with
      | Zero, Zero -> 0
      | Zero, One -> -1
      | One, Zero -> 1
      | One, One -> 0

    (** [elt_pp fmt elt] prettyp prints the element [elt] on the
        formatter [fmt] *)
    let elt_pp fmt = function
      | Zero -> Format.pp_print_int fmt 0
      | One -> Format.pp_print_int fmt 1

    (** [t] is the type of addresses *)
    type t = elt list

    (** This exception is used on some operation involving an address
        [a] and some address [u] where it is assumed that [u] is a
        prefix of [a]. *)
    exception Not_prefix

    (** [compare] is a lexical order on addresses *)
    let compare = List.compare elt_cmp

    (** [is_prefix ~strict u v] returns [true] if {ul

    {- [u] is a prefix of [v]}

    {- and [u≠v] if [strict] is set to [true]}, and [false]
    otherwise.*)
    let rec is_prefix ~strict a1 a2 =
      match a1, a2 with
      | [], [] when strict -> false
      | [], [] -> true
      | [], _::_ -> true
      | _::_, [] -> false
      | a::tl1, b::tl2 when a=b -> is_prefix ~strict tl1 tl2
      | _ -> false

    (** [extend add elt] extends the address [add] with the symbol
        [elt] added at the end.*)
    let rec extend l i =
      match l with
      | [] -> [i]
      | a :: tl -> a :: (extend tl i)

    let concat a1 a2 = a1 @ a2

    (** [remove ~prefix w] returns [v] if [w=prefix v] and raises {!
        Not_prefix} otherwise. *)
    let rec remove ~prefix l =
      match prefix, l with
      | [], _ -> l
      | a :: prefix', b :: tl when a = b -> remove ~prefix:prefix' tl
      | _, _ -> raise Not_prefix

    (** [pp fnt add] pretty prints the address [add] on the formatter
        [fmt] *)
    let pp = PPUtils.pp_list ~sep:"" elt_pp

  end

(** The {!AddMap} module implements a trie data structure to represent
    maps from {!Address.t} addresses to values of type ['a]*)
module AddMap =
  struct
    (** ['a t] is the type of sets of addresses *)
    type 'a t = M of ('a option * 'a t option * 'a t option)

    (** [empty] is the empty set of addresses *)
    let empty = M (None, None, None)

    (** [mem add m] returns [true] if [add] binds a value map [m] and
        [false] otherwise. *)
    let rec mem add m =
      match add, m with
      | [], M (None, _, _ ) -> false
      | [], M (Some _, _, _ ) -> true
      | Address.Zero::_, M (_, None, _) -> false
      | Address.Zero::tl, M (_, Some left, _) -> mem tl left
      | Address.One::_, M (_, _, None) -> false
      | Address.One::tl, M (_, _, Some right) -> mem tl right

    (** [mem add m] returns [true] if [add] binds a value map [m] and
        [false] otherwise. *)
    let rec find (add:Address.t) (m:'a t) : 'a =
      match add, m with
      | [], M (None, _, _ ) -> raise Not_found
      | [], M (Some v, _, _ ) -> v
      | Address.Zero::_, M (_, None, _) -> raise Not_found
      | Address.Zero::tl, M (_, Some left, _) -> find tl left
      | Address.One::_, M (_, _, None) -> raise Not_found
      | Address.One::tl, M (_, _, Some right) -> find tl right


  (** [add a v m] adds at the address [a] the value [v] into the map
      [m], possibly changing the binding if [a] was already binding a
      value in [m].*)
    let rec add a v m =
      match a, m with
        | [], M (_, l, r) -> M (Some v, l, r)
        | Address.Zero::tl, M (b, None, r) -> M (b, Some (add tl v empty), r)
        | Address.Zero::tl, M (b, Some l, r) -> M (b, Some (add tl v l), r)
        | Address.One::tl, M (b, l, None) -> M (b, l, Some (add tl v empty))
        | Address.One::tl, M (b, l, Some r) -> M (b, l, Some (add tl v r))

    let rec iter_aux f acc (M (b, _, _) as s) =
      let () = 
        match b with 
        | None -> ()
        | Some v -> f acc v in
      match s with
      | M (_, None, None) -> ()
      | M (_, Some l, None) -> 
         iter_aux f (Address.extend acc Address.Zero) l
      | M (_, None, Some r) -> 
         iter_aux f (Address.extend acc Address.One) r
      | M (_, Some l, Some r) -> 
         let () = iter_aux f (Address.extend acc Address.Zero) l in
         iter_aux f (Address.extend acc Address.One) r

    (** [iter f m] iterates the function [f] on every [(k, v)] binding of
        [m].*)
    let iter f s = iter_aux f [] s


    let to_lst m = 
      let rec to_lst_aux acc add (M (b, _, _) as s) =
        let acc' = 
          match b with
          | None -> acc
          | Some v -> (add, v) :: acc in
        match s with
        | M (_, None, None) -> acc'
        | M (_, Some l, None) -> 
           to_lst_aux acc' (Address.extend add Address.Zero) l
        | M (_, None, Some r) -> 
           to_lst_aux acc' (Address.extend add Address.One) r
        | M (_, Some l, Some r) -> 
           let acc'' = to_lst_aux acc' (Address.extend add Address.Zero) l in
           to_lst_aux acc'' (Address.extend add Address.One) r in
      to_lst_aux [] [] m
end

module AddSet = 
  struct
    type t = unit AddMap.t

    let empty = AddMap.empty

    let mem = AddMap.mem

    let add elt s = AddMap.add elt () s

    let iter f s = AddMap.iter (fun a () -> f a) s
end

(** [min ~cmp lst] returns [elt,lst'] where [elt] is the minimal
    element of [lst] according to the comparison function [cmp] (even
    if it occurs several times), and [lst'] is [lst] with this
    occurrence of [elt] removed .*)
let min ~cmp l = 
  let rec min_aux min acc l = 
    match min, l with
    | _, [] -> min, acc
    | None, a::tl -> min_aux (Some a) acc tl
    | Some v, a::tl when (cmp a v) < 0 -> min_aux (Some a) (v::acc) tl
    | _, a::tl -> min_aux min (a::acc) tl in
  min_aux None [] l

let extend_map_to_lst = Utils.IntMap.add_to_list

(*module Domain = Map.Make (Address)*)
module Domain = AddMap

(** This type records for linear and non linear variables at address
    [a] the address of the binder that binds this variable. Therefore,
    [Address.is_prefix ~strict:true k v] should always return true
    whenever [k] maps to [v] in [nl_binders] or in [l_binders]. *)
type binders = { nl_binders : Address.t Domain.t;
                 l_binders : Address.t Domain.t; }

(** This module implements a map from the de Bruijn indices of a
    variable the address of its binder (recorded when the
    corresponding binder was crossed).*)
module BAdd = Lambda.MakeVarEnv (struct type info = Address.t let pp = Address.pp end)

(** A record type to keep track of maps from de Bruijn indices of
    variables to addresses of their binders *)
type addresses = { nl_add : BAdd.t;
                   l_add : BAdd.t; }

(** When representing lambda-terms as trees with 0-ary (variables or
    constants), 1-ary (abstraction), or 2-ary nodes, it's possible to
    have a dedicated zipper type. The node information is basically
    empty, and what is relevant is the local context, i.e., what is
    right above a term (if it's the child of an abstraction), what is
    on its right (if it's the functor of an application, [u] in [Rapp
    u] being its argument), what is on its left (if it's the argument
    of an application, [u] in [Lapp u] being the functor). *)
type term_local_context =
  | LAbs of string
  | Abs of string
  | LApp of Lambda.term
  | RApp of Lambda.term
type term_zipper =
  | ZTop
  | TZip of (term_zipper * term_local_context)

(** [zip_up (z, u)] returns the term [t] such that [u] is its subterm
    in context [z]. *)
let rec zip_up (z, t) =
  match z with
  | ZTop -> t
  | TZip (z', LAbs x) -> zip_up (z', Lambda.LAbs (x, t))
  | TZip (z', Abs x) -> zip_up (z', Lambda.Abs (x, t))
  | TZip (z', LApp u) -> zip_up (z', Lambda.App (u, t))
  | TZip (z', RApp u) -> zip_up (z', Lambda.App (t, u))

type term_sig = 
  { add:Address.t;
    l_env:Lambda.env;
    nl_env: Lambda.env;
    duplicable: bool;
    ctx:term_zipper;
    term: Lambda.term;
  }

(** [subterms_aux (levels, addresses, subtrees, binders) (t, add)]
    returns a tuple [(height, consts), (subtrees', binders')] where
    [height] is the height of the term [t], [consts] is the
    lefto-to-right sequence of (indices of) constants it is made of,
    [subtrees'] is [subtrees], a map from (the opposite of) their
    heighth to terms (in order to fold over this map starting with the
    highest subtrees), augmented with the subterms of [t], whose
    address is [add], and [binders'] is the previous binders map (for
    the term [t] is a subterm of) together with the binder map defined
    by [t]. And [addresses] is a map from the level at which a binder
    is introduced to its address with the tree. *)

(* We assume that [t] is in eta-long form *)

let rec subterms_aux
          (addresses, (l_nvenv, nvenv), (subtrees: (term_sig list) Utils.IntMap.t), binders)
          (t, add, context) = 
  match t, context with
  | Lambda.Var i, _ -> 0,
                       (extend_map_to_lst
                          0
                          {add;
                           l_env=l_nvenv;
                           nl_env=nvenv;
                           duplicable=false;  (* variables can't be dupicated pivot *)
                           ctx=context;
                           term=t;}
                          subtrees,
                        {binders with
                          nl_binders =
                            Domain.add
                              add
                              (BAdd.get i addresses.nl_add)
                              binders.nl_binders})
  | Lambda.LVar i, _ -> 0,
                        (extend_map_to_lst
                           0
                           {add;
                            l_env=l_nvenv;
                            nl_env=nvenv;
                            duplicable=false;  (* variables can't be dupicated pivot *)
                            ctx=context;
                            term=t;}
                          subtrees,
                         {binders with
                           l_binders =
                             Domain.add
                               add
                               (BAdd.get i addresses.l_add)
                               binders.l_binders})
  | Lambda.Const _, ZTop -> 0,
                            (extend_map_to_lst
                               0
                               {add;
                                l_env=l_nvenv;
                                nl_env=nvenv;
                                duplicable=true;
                                ctx=ZTop;
                                term=t;}
                               subtrees,
                             binders)
  | Lambda.Const _, TZip (_, LApp _)  ->
     (* the constant is the right child of an applicitation,
        therefore, it has an atomic type (otherwise there would be a
        lambda since the tern is in eta-long form *)
     0,
     (extend_map_to_lst
         0
         {add;
           l_env=l_nvenv;
           nl_env=nvenv;
           duplicable=true;
           ctx=context;
           term=t;}
         subtrees,
      binders)
  | Lambda.Const _, TZip (_, RApp _)  ->
     (* the constant is the left child of an applicitation, therefore, it has not an atomic type *)
     0,
     (extend_map_to_lst
        0
        {add;
         l_env=l_nvenv;
         nl_env=nvenv;
         duplicable=false;
         ctx=context;
         term=t;}
        subtrees,
      binders)
  | Lambda.DConst _, _ -> failwith "Bug: should not occur. It is expected \
                                    constant definition expansion has \
                                    already been performed at this stage"
  | Lambda.Abs (x, u), _ ->
     let h, (n_subtrees, n_binders) =
       subterms_aux
         ({addresses with nl_add = BAdd.add add addresses.nl_add},
          (l_nvenv, Lambda.VNEnv.add x nvenv),
          subtrees,
          binders)
         (u, Address.(extend add Zero), TZip(context, Abs x)) in
     h+1,
     (n_subtrees, n_binders)
  | Lambda.LAbs (x, u), _ ->
     let h, (n_subtrees, n_binders) =
       subterms_aux
         ({addresses with l_add = BAdd.add add addresses.l_add},
          (Lambda.VNEnv.add x l_nvenv, nvenv),
          subtrees,
          binders)
         (u, Address.(extend add Zero), TZip(context, LAbs x)) in
     h+1,
     (n_subtrees, n_binders)
  | Lambda.App (u, v), _ ->
     let h_u, (n_subt, n_bs) = subterms_aux (addresses, (l_nvenv, nvenv), subtrees, binders) (u, Address.(extend add Zero), TZip(context, RApp v)) in
     let h_v, (n_subtrees, n_binders) = subterms_aux (addresses, (l_nvenv, nvenv), n_subt, n_bs) (v, Address.(extend add One), TZip(context, LApp u)) in
     let n_h = max h_u h_v in
     let nn_subtrees =
       match context with
       | ZTop
         | TZip (_, (LApp _ | Abs _ | LAbs _)) ->
          extend_map_to_lst
            (-(n_h+1))
            {add;
             l_env=l_nvenv;
             nl_env=nvenv;
             duplicable=true;
             ctx=context;
             term=t}
            n_subtrees
       | TZip (_, RApp _) -> 
          extend_map_to_lst
            (-(n_h+1))
            {add;
             l_env=l_nvenv;
             nl_env=nvenv;
             duplicable=false;
             ctx=context;
             term=t}
            n_subtrees in
     n_h + 1,
     (nn_subtrees, n_binders)
  | _, _ -> failwith "Not implemented"


let subterms t =
  let _, (subt, binders) = 
    subterms_aux
      ({nl_add = BAdd.empty;
        l_add = BAdd.empty;},
       Lambda.VNEnv.(empty, empty),
       Utils.IntMap.empty,
       {l_binders = Domain.empty;
        nl_binders = Domain.empty;})
      (t, [], ZTop) in
   subt, binders


(** [congruent_aux ((w, w') binders add t1 t2] returns
    [true] if the two terms [t1] (at address [w add]) and [t2] (at
    address [w' add] are congruent *)
let rec congruent_aux (w, w') binders add t1 t2 =
  match t1, t2, binders.l_binders, binders.nl_binders with
  | Lambda.Const i, Lambda.Const j, _, _ -> i = j
  | Lambda.Var _, Lambda.Var _, _, b_addresses 
  | Lambda.LVar _, Lambda.LVar _, b_addresses, _ ->
     let full_add1 = Address.concat w add in
     let full_add2 = Address.concat w' add in
     let binder1 = Domain.find full_add1 b_addresses in
     let binder2 = Domain.find full_add2 b_addresses in
     if binder1 = binder2 then
       true
     else
       begin
         (* if the address of the two binders are different,
            [b(t1)=wu], [b(t2)=w'u], each binders should have the same
            address below [w] and [w'], resp., i.e., [b(t2)=w'u'] and
            [u=u']. *)
         (* First check that both binder addresses are below [w] and
            [w'], resp., i.e., [w] and [w'] are prefixes of [binder1]
            and [binder2], resp. *)
         try
           let u = Address.remove ~prefix:w binder1 in
           let u' = Address.remove ~prefix:w' binder2 in
           (* We first check that [u] is a prefix of [add], i.e., that
              [t1] is indeed in the scope of the binder that binds
              it *)
           match Address.remove ~prefix:u add with
           | [] -> false
           | _ -> u = u'
           | exception Address.Not_prefix -> false
         with
         | Address.Not_prefix -> 
            false
              (* either [w] is not prefix of [binder1] or [w'] is not
                 prefix of [binder2] *)
       end
  | Lambda.Abs (_, t1'), Lambda.Abs (_, t2'), _, _
  | Lambda.LAbs (_, t1'), Lambda.LAbs (_, t2'), _, _ ->
     congruent_aux (w, w') binders Address.(extend add Zero) t1' t2'
  | Lambda.App (u1, v1), Lambda.App (u2, v2), _, _ ->
     let res = congruent_aux (w, w') binders Address.(extend add Zero) u1 u2 in
     if res then
       congruent_aux (w, w') binders Address.(extend add One) v1 v2
     else
       false
  | _ -> false


let congruent
      ~consts
      binders
      sg
      sg' =
  if (not sg.duplicable) || (not sg'.duplicable) then
    false
  else
    let () =
      Log.debug
        (fun m ->
          m
            "Checking congruency of:@[<v>@,@[%a@]@,and@,@[%a@]@]"
         (Lambda.pp_term ~env:(sg.l_env,sg.nl_env) consts)
         sg.term
         (Lambda.pp_term ~env:(sg'.l_env,sg'.nl_env) consts)
         sg'.term) in
    congruent_aux (sg.add, sg'.add) binders [] sg.term sg'.term


(** [partition ~skip ~pred l] returns [l_partition]
    such that:

    {ul 

    {- [l_partition] is a list [[l1; l2; .. ; ln]] of list of
    elements such that for any [e1∈li] and [e2∈lj], [pred e1 e2] is
    true if and only if [i=j]}

    {- all elements of [l] {e but the ones for which [skip] returns
    true} are in an element of [l_partition]} } } *)
let partition ~skip  ~pred l =
  let rec partition_aux ~skip ~pred l_partition l =
    (* [partition_aux ~skip ~pred l_partition l] returns [l_partition']
       such that:

       {ul

       {- [l_partition'] is a list [[l1; l2; .. ; ln]] of list of
       elements such that for any [e1∈li] and [e2∈lj], [pred e1 e2] is
       true if and only if [i=j]}

       {- all elements of [l] {e but the ones for which [skip] returns
       true} are in an element of [l_partition']}

       {- [l_partition'] extends [l_partition = [l1 ; .. ; lk]] (which is
       assumed to be a correct partition as well), i.e., for every
       [1≤i≤k], there exists [1≤j≤k] such that [li⊂ lj].

       } }
     *)

    match l with
    | [] -> l_partition
    | a :: tl when skip a -> partition_aux ~skip ~pred l_partition tl
    | a :: tl ->
       (* We need to check if [a] could got into an existing subset of
          [l_partition] or if we need to create a new party for it *)
       let partition', found =
         List.fold_left
           (fun (c_partition, found) part ->
             if found then
               (* we already found the part in [l_partition] [a]
                  belongs to. Hence we just add the current part to
                  partion *)
               part :: c_partition, found
             else
               match part with
               | [] -> c_partition, found (* Such a case should not really
                                             occur, but it's safe anyway *)
               | b :: _ when pred a b -> (a :: part) :: c_partition, true
               (* [a] is in the [pred] relation with [b], it therefore
                  belongs to the current part to which it is added, and the
                  whole part is added to [c_partition]. *)
               | _ -> part :: c_partition, found)
           (* otherwise we just keep the part [part] unchanged and add
              it to [c_partition]. *)
           ([], false)
           l_partition in
       let partition'' = if found then partition' else [a]::partition' in
       (partition_aux ~skip ~pred partition'' tl) in

  (* we only keep parts of the partition that have at least 2
     elements *)
  List.filter 
    (fun elt ->
      match elt with
      | _::_::_ -> true
      | _ -> false)
    (partition_aux ~skip ~pred [] l)

(** This exception is raised when a solution is found while scanning a
    map, in order to avoid scanning all the map *)
exception Stop of (int * (term_sig * (term_sig list)))

let subterms_pp consts fmt subterms =
  let dup_pp fmt b =
    if b then
      Tags.red_pp fmt "(duplicable)"
    else
      Tags.blue_pp fmt "(not duplicable)" in
  List.iter (fun {l_env;nl_env;duplicable; add;term=t;_} -> Format.fprintf fmt "@[%a@ %a@] at address: %a@," (Lambda.pp_term ~env:(l_env, nl_env) consts) t dup_pp duplicable Address.pp add) subterms
    [@@alert "-deprecated"]
    [@@warning "-unused-value-declaration"]


(** [is_common_prefix ~strict a lst] returns [true] if [a] is a prefix
    (resp. strict prefix) of all the address fields of the elements of
    [lst]. *)
let is_common_prefix ~strict ad lst = 
  let rec is_common_prefix_aux acc ad = function
    | [] -> acc
    | a::tl when Address.is_prefix ~strict ad a.add -> 
       is_common_prefix_aux(true && acc) ad tl
    | _ -> false in
  is_common_prefix_aux true ad lst

(** [expand subterms level addresses (add, t)] compute the expanded
    subterm of [t] at address [add] and current non-linear abstraction
    level [level] as if a new [Abs] binder has been added at the [0]
    level that would bien all variables whose addresses are in
    [addresses]. Only (non-linear) variables are affected:

    {ul

    {- if [i < level], then [i] is unchanged}

    {- if [i ≥ level], then [i] is replaced by [i + 1]}

    {- if the current address [add] is in [addresses], then a new
    variable indexed by [level] is introduced.}

}

 *)
let expand_subterm addresses (add, t) =
  let rec expand_subterm_aux level (add, t) =
    if AddSet.mem add addresses then
      Lambda.Var level
    else
      match t with
      | Lambda.LVar _ -> t
      | Lambda.Const _ -> t
      | Lambda.DConst _ -> failwith "Bug: the term should be fully expanded"
      | Lambda.LAbs (x, u) -> Lambda.LAbs (x, expand_subterm_aux level (Address.(extend add Zero),u))
      | Lambda.Abs (x, u) -> Lambda.Abs (x, expand_subterm_aux (level + 1) (Address.(extend add Zero),u))
      | Lambda.App (u, v) -> Lambda.App (expand_subterm_aux level (Address.(extend add Zero),u),
                                         expand_subterm_aux level (Address.(extend add One),v))
      | Lambda.Var i when i < level -> Lambda.Var i
      | Lambda.Var i -> Lambda.Var (i + 1)
      | _ -> failwith "Not implemented"
  in expand_subterm_aux 0 (add, t)

(** [collapse ~consts t] returns [None] if [t] is unchanged through
    the collapse algorithm (i.e., no subterm of atomic type occurs at
    least twice in [t]), and [Some u] where [u] is the results of the
    (recursive) collapse algorithm.

    {b It is expected that [t] does not contain unexpanded defined
    constants.}

    If [consts] is provided, the mapping from constant ids to strings
    (in some signature) is used to pretty prints terms if {!Log} log
    level is set to some adequate level. Otherwise, each constant is
    printed as [Const[i]].
    
 *)
let collapse
      ?(consts=fun i -> Abstract_syntax.Abstract_syntax.Default,Printf.sprintf "Const(%d)" i)
      t = 
  let rec collapse_aux ~res t =
    let () = Log.debug (fun m -> m "Starting collapse of @[%a@]" (Lambda.pp_term consts) t) in
    (* We first get all the subterms and all the maps from variable
       addresses to the address of their binders.

       The subterms are in a map from (the opposite of) the height to
       the list of subterms of that height (so that when scanning, it
       starts from highest subterms unti one is found *)
    let heigth_to_subterms, binders = subterms t in
        let () =
          Log.debug
          (fun m -> 
          let pp_map fmt map =
          Utils.IntMap.iter
          (fun k lst ->
          Format.fprintf
          fmt
          "Listing the subterms of height %d@[<v2>@,%a@]@,"
          (-k)
          (subterms_pp consts)
          lst)
          map in
          m "The subterms are:@ @[<v2> @[<v>%a@]@]" pp_map heigth_to_subterms) in
        let () =
          Log.debug
            (fun m ->
              m
                "@[<v>@[Linear bindings:@[<v>@,@[<v>%a@]@,@]@,@]@[Non-linear bindings:@[<v>@,@[<v>%a@]@]@]@]"
             (PPUtils.pp_list ~sep:"@," ~terminal:"@," (fun fmt (add1, add2) -> Format.fprintf fmt "%a ----> %a" Address.pp add1 Address.pp add2))
             (AddMap.to_lst binders.l_binders)
             (PPUtils.pp_list ~sep:"@," ~terminal:"@," (fun fmt (add1, add2) -> Format.fprintf fmt "%a ----> %a" Address.pp add1 Address.pp add2))
             (AddMap.to_lst binders.nl_binders)) in
    try
      begin
        let part =
          (* We go through all set of subterms of a given height,
             starting from the greatest one *)
          Utils.IntMap.fold
            (fun h subts intermed_res ->
              (* for a given set of subterms of height h, we  find the
                 parition according to the [congruent binders]
                 predicate. We [skip] the elements that are marked as
                 non-duplicable. *)
              let l_partitions =
                partition
                  ~skip:(fun {duplicable;_} -> not duplicable)
                  ~pred:(fun a b  -> congruent ~consts binders a b)
                  subts in
              match l_partitions with
              | [] -> 
                 (* No part with more than 2 duplicables elements were
                    found, we just look for a solution at the nect
                    height *)
                 intermed_res
              | _ ->
                 (* There is a part with two elements *)
                 let () = 
                   Log.debug
                     (fun m ->
                       List.iter
                         (fun part ->
                           m
                             "I found the following duplicated pivots of height %d: @[<v2>@,%a@]"
                             (-h)
                             (subterms_pp consts)
                             part)
                         (List.sort (fun l1 l2 -> List.compare_lengths l2 l1) l_partitions)) in 
                 (* We need to find, for each part in the partition,
                    its leftmost element, i.e., the one with the
                    smallest (in lexicographic order) address *)
                 let cmp {add=a1;_} {add=a2;_} = Address.compare a1 a2 in
                 let l_partitions' =
                   List.map
                     (fun part ->
                       (* for a given partition, first find the
                          leftmost element *)
                       match min ~cmp part with
                       | None, _ -> failwith "Bug: should not occurr, \
                                              partitions should not be \
                                              empty"
                       | Some v, p -> v, p )
                     l_partitions in
                 (* then find the part with leftmost element, based on
                    the leftmost element of each part of the
                    partition *)
                 match min ~cmp:(fun (m1,_) (m2,_) -> cmp m1 m2) l_partitions' with
                 | None, _ -> failwith "Bug: Should not occurr"
                 | Some res, _ -> raise (Stop (h, res)))
            heigth_to_subterms
            None in
        match part, res with
        | None, None -> None (* No duplicated pivot, no intermediary result *)
        | None, Some _ -> res (* No duplicated pivot, some
                                          intermediary result. Returns
                                          the latter, there is no need
                                          to continue *)
        | Some _, _ -> failwith "Bug: should not happen"
      end
    with
      (* An exception was raised, i.e., some part with at least two duplicated pivots was found. *)
    | Stop (p_h, (({add;l_env;nl_env;term=leftmost_pivot;_} as dup_p), partition)) ->
       let () = Log.debug
                  (fun m ->
                    m
                      "Found@ leftmost@ duplicated@ pivot@ at@ address: @[%a@]: %a"
                      Address.pp
                      add
                      (Lambda.pp_term ~env:(l_env, nl_env) consts)
                      leftmost_pivot) in     
       let () = Log.debug
                  (fun m -> 
                    m
                      "Other congruent terms are at addresses:@[<v>@,%a@]"
                      (PPUtils.pp_list ~sep:"@," (fun fmt {add;_} -> Address.pp fmt add))
                      partition
                  ) in
       (* Collects all the addresses of the duplicated pivots,
          including the leftmost one *)
       let dup_pivot_addresses = 
         List.fold_left
           (fun acc {add=l_add;_} -> AddSet.add l_add acc)
           (AddSet.empty |> AddSet.add add)
           partition in
       (* Find the pivot (not necessarily duplicated) of minimal
          height that is above all the slected duplicated pivots,
          i.e., whose address is a prefix of all the addresses of the
          duplicated pivots *)
       let min_pivot = 
         Utils.IntMap.fold
           (fun h term_list acc ->
             if h >= p_h then
               (* [-h ≤ -p_h] i.e., we are currently going through
                  subterms that have a heigth less than the one of the
                  duplicated pivot, so we can just skip them *)
               acc
             else
               (* We check if we can find a pivot whose address is a
                  prefix of the addresses of all the duplicated
                  pivots. Finding one is enough.*)
               match
                 List.fold_left
                   (fun l_intermed_res t_sig ->
                     match l_intermed_res with
                     | None ->
                        if is_common_prefix ~strict:true t_sig.add (dup_p::partition) then
                          Some t_sig
                        else
                          l_intermed_res
                     | Some _ -> l_intermed_res)
                   None
                   term_list with
               | None -> acc
               | Some res -> Some (h, res))
           heigth_to_subterms
           None in
       match min_pivot with
       | None ->
          (* If we reach this part, there are duplicated pivots, hence
             there should be a pivot of minimal height ancestor of all
             of them, so this case should not happen. *)
          failwith "Bug: I didn't find a minimal height pivot from which to expand"
       | Some (h,t_sig) ->
          let () = Log.debug (fun m -> m "I found a minimal height pivot of height %d at address: %a" (-h) Address.pp t_sig.add) in
          let () = Log.debug (fun m -> m "The minimal height pivot is: @[%a@]" (Lambda.pp_term ~env:(t_sig.l_env, t_sig.nl_env) consts) t_sig.term) in
          let expanded_subt = expand_subterm dup_pivot_addresses (t_sig.add,t_sig.term) in
          let () = Log.debug (fun m -> m "Raw minimal height pivot: %s" (Lambda.raw_to_string t_sig.term)) in
          let () = Log.debug (fun m -> m "Expanded minimal height pivot: %s"  (Lambda.raw_to_string expanded_subt)) in
          let expanded_t = Lambda.(App(Abs("Z",expanded_subt),leftmost_pivot)) in
          let result = zip_up (t_sig.ctx,expanded_t) in
          let () = Log.debug (fun m ->
                       let l_ref = Lambda.VNEnv.current_level t_sig.nl_env in
                       let nl_env = Lambda.VNEnv.shift ~info:"Z" ~level:(l_ref -1) t_sig.nl_env in
                       m
                         "Its expanded version is: @[%a@]"
                         (Lambda.pp_term ~env:(t_sig.l_env, nl_env) consts)
                         expanded_t) in
          let () = Log.debug (fun m -> m "The whole term is: @[%a@]" (Lambda.pp_term consts) result) in
          collapse_aux ~res:(Some result) (result) in


  let res = collapse_aux ~res:None t in
  match res with
  | None -> let () = Log.debug (fun m -> m "I didn't find a collapsed term" ) in res
  | Some t -> let () = Log.debug (fun m -> m "I found the collapsed term @[%a@]" (Lambda.pp_term consts) t) in res