(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.              
     \ /   This software is distributed as is, NO WARRANTY.              
      V_______________________________________________________________ *)

module S = Share
module B = Bag

(* Internal functions *******************************************************)

let rec lref_map_bind f map b = match b with
   | B.Abbr v ->
      let f v' = f (S.sh1 v v' b B.abbr) in
      lref_map f map v      
   | B.Abst w ->
      let f w' = f (S.sh1 w w' b B.abst) in
      lref_map f map w
   | B.Void   -> f b

and lref_map f map t = match t with
   | B.LRef i            -> 
      let ii = map i in f (S.sh1 i ii t B.lref)
   | B.GRef _            -> f t
   | B.Sort _            -> f t
   | B.Cast (w, u)       ->
      let f w' u' = f (S.sh2 w w' u u' t B.cast) in
      let f w' = lref_map (f w') map u in 
      lref_map f map w
   | B.Appl (w, u)       ->
      let f w' u' = f (S.sh2 w w' u u' t B.appl) in
      let f w' = lref_map (f w') map u in 
      lref_map f map w
   | B.Bind (l, id, b, u) ->
      let f b' u' = f (S.sh2 b b' u u' t (B.bind l id)) in
      let f b' = lref_map (f b') map u in 
      lref_map_bind f map b

(* Interface functions ******************************************************)

let subst f new_l old_l t =
   let map i = if i = old_l then new_l else i in
   if new_l = old_l then f t else lref_map f map t