- common/entity: new format for kernel entities

[helm.git] / helm / software / lambda-delta / basic_rg / brg.ml

diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml
index e3c5866818c2d8e1a8db71a42d3d100ecd84d057..373f5342feb091dd68032a03e3dcf7d36a6cf60e 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brg.ml
+++ b/helm/software/lambda-delta/basic_rg/brg.ml
@@ -14,11 +14,7 @@
 
 type uri = Entity.uri
 type id = Entity.id
-
-type attr = Name of bool * id  (* real?, name *)
-          | Apix of int        (* additional position index *)
-
-type attrs = attr list
+type attrs = Entity.attrs
 
 type bind = Void of attrs        (* attrs       *)
           | Abst of attrs * term (* attrs, type *)
@@ -31,9 +27,7 @@ and term = Sort of attrs * int         (* attrs, hierarchy index *)
          | Appl of attrs * term * term (* attrs, argument, function *)
          | Bind of bind * term         (* binder, scope *)
 
-type entry = bind Entity.entry (* age, uri, binder *)
-
-type entity = bind Entity.entity
+type entity = term Entity.entity (* attrs, uri, binder *)
 
 type lenv = Null
 (* Cons: tail, relative local environment, binder *) 
@@ -85,13 +79,3 @@ let rec fold_left f map x = function
    | Cons (tl, _, b) ->
       let f x = fold_left f map x tl in
       map f x b
-
-let rec name err f = function
-   | []               -> err ()
-   | Name (r, n) :: _ -> f n r
-   | _ :: tl          -> name err f tl
-
-let rec apix err f = function
-   | []          -> err ()
-   | Apix i :: _ -> f i
-   | _ :: tl     -> apix err f tl