new kernel basic_ag (with absolute local references)

[helm.git] / helm / software / lambda-delta / basic_ag / bagSubstitution.ml

diff --git a/helm/software/lambda-delta/basic_ag/bagSubstitution.ml b/helm/software/lambda-delta/basic_ag/bagSubstitution.ml
new file mode 100644 (file)
index 0000000..2572552
--- /dev/null
+++ b/helm/software/lambda-delta/basic_ag/bagSubstitution.ml
@@ -0,0 +1,48 @@
+(*
+    ||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
+   lref_map f map t