- revision of ground_2 and basic_2

[helm.git] / helm / software / helena / src / complete_rg / crg.ml

diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml
index 0acd43336d090ee42a3c096d300287623036c296..455eb6ed4547b193ca52becf1e6fcd4c0e07554e 100644 (file)
--- a/helm/software/helena/src/complete_rg/crg.ml
+++ b/helm/software/helena/src/complete_rg/crg.ml
@@ -13,14 +13,14 @@
 (* note          : fragment of complete \lambda\delta serving as abstract layer *) 
 
 module C = Cps
+module N = Layer
 module E = Entity
-module N = Level
 
 type uri = E.uri
 type id = E.id
 type attrs = E.node_attrs
 
-type bind = Abst of N.level * term      (* level, type *)
+type bind = Abst of N.layer * term      (* layer, type *)
           | Abbr of term                (* body *)
           | Void                        (* *)
 
@@ -73,7 +73,8 @@ let resolve_lref err f id lenv =
      | EAppl (tl, _, _)  -> aux i tl
      | EBind (tl, a, _)  ->
         let f id0 _ = if id0 = id then f a i else aux (succ i) tl in
-        E.name err f a 
+        let err () = aux (succ i) tl in
+        E.name err f a
      | EProj (tl, _, d)  -> append (aux i) tl d
    in
    aux 0 lenv
@@ -113,3 +114,14 @@ let rec mem err f e b = match e with
    | EAppl (e, _, _) -> mem err f e b
    | EProj (e, _, d) -> 
       let err () = mem err f e b in mem err f d b
+
+let replace f n0 e =
+   let rec aux f = function
+      | ESort                     -> f ESort
+      | EBind (e, a, Abst (n, w)) -> aux (push_bind f a (Abst (n0, w))) e
+      | EBind (e, a, b)           -> aux (push_bind f a b) e
+      | EAppl (e, a, v)           -> aux (push_appl f a v) e
+      | EProj (e, a, d)           -> let f d = aux (push_proj f a d) e in aux f d
+
+   in
+   aux f e