- 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 7ba80ddfb39a7c01156f656b75fc41f7b37c31c0..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.attrs
+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                        (* *)
 
@@ -72,8 +72,9 @@ let resolve_lref err f id lenv =
      | ESort             -> err ()
      | EAppl (tl, _, _)  -> aux i tl
      | EBind (tl, a, _)  ->
-        let f id0 _ = if id0 = id then f i else aux (succ i) tl in
-        E.name err f a 
+        let f id0 _ = if id0 = id then f a i else aux (succ i) tl in
+        let err () = aux (succ i) tl in
+        E.name err f a
      | EProj (tl, _, d)  -> append (aux i) tl d
    in
    aux 0 lenv
@@ -89,44 +90,8 @@ let rec get_name err f i = function
       let err i = get_name err f i tl in 
       get_name err f i e
 
-(*
-let push2 err f lenv ?attr ?t () = match lenv, attr, t with
-   | EBind (e, a, Abst (n, ws)), Some attr, Some t -> 
-      f (EBind (e, (attr :: a), Abst (n, t :: ws)))
-   | EBind (e, a, Abst (n, ws)), None, Some t      -> 
-      f (EBind (e, a, Abst (n, t :: ws)))
-   | EBind (e, a, Abbr vs), Some attr, Some t      ->
-      f (EBind (e, (attr :: a), Abbr (t :: vs)))
-   | EBind (e, a, Abbr vs), None, Some t           ->
-      f (EBind (e, a, Abbr (t :: vs)))
-   | EBind (e, a, Void n), Some attr, None         ->
-      f (EBind (e, (attr :: a), Void (succ n)))
-   | EBind (e, a, Void n), None, None              ->
-      f (EBind (e, a, Void (succ n)))
-   | _                                             -> err ()
-
-let get_index err f i j lenv =
-   let rec aux f i k = function
-      | ESort                      -> err i
-      | EBind (tl, _, Abst (_, []))
-      | EBind (tl, _, Abbr [])
-      | EBind (tl, _, Void 0)      -> aux f i k tl
-      | EBind (_, a, _) when i = 0 ->
-        if E.count_names a > j then f (k + j) else err i
-      | EBind (tl, a, _)           -> 
-         aux f (pred i) (k + E.count_names a) tl
-      | EProj (tl, _, d)           -> aux f i k (eshift C.start tl d)
-   in
-   aux f i 0 lenv
-*)
-let rec names_of_lenv ns = function
-   | ESort            -> ns
-   | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl
-   | EAppl (tl, _, _) -> names_of_lenv ns tl
-   | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl
-
 let rec get e i = match e with 
-   | ESort                      -> ESort, [], Void
+   | ESort                      -> ESort, E.empty_node, Void
    | EBind (e, a, b) when i = 0 -> e, a, b
    | EBind (e, _, _)            -> get e (pred i)
    | EAppl (e, _, _)            -> get e i
@@ -137,7 +102,26 @@ let rec sub_list_strict f e l = match e, l with
    | EBind (e, _, Abst _), _ :: tl -> sub_list_strict f e tl
    | _                             -> assert false
 
-let rec fold_attrs f map a0 = function
-   | ESort                -> f a0
-   | EBind (e, a, Abst _) -> fold_attrs f map (map a0 a) e
-   | _                    -> assert false
+let rec fold_names f map x = function
+   | ESort                                  -> f x
+   | EBind (e, {E.n_name = Some n}, Abst _) -> fold_names f map (map x n) e
+   | _                                      -> assert false
+
+let rec mem err f e b = match e with
+   | ESort           -> err ()
+   | EBind (e, a, _) ->
+      if a.E.n_name = b.E.n_name then f () else mem err f e b
+   | 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