- new attributes system

[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..0acd43336d090ee42a3c096d300287623036c296 100644 (file)
--- a/helm/software/helena/src/complete_rg/crg.ml
+++ b/helm/software/helena/src/complete_rg/crg.ml
@@ -18,7 +18,7 @@ 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 *)
           | Abbr of term                (* body *)
@@ -72,7 +72,7 @@ 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
+        let f id0 _ = if id0 = id then f a i else aux (succ i) tl in
         E.name err f a 
      | EProj (tl, _, d)  -> append (aux i) tl d
    in
@@ -89,44 +89,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 +101,15 @@ 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