- common/entity: new format for kernel entities

[helm.git] / helm / software / lambda-delta / dual_rg / drg.ml

diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml
index e598a59867d40eb0adf175bfe9c35f324b2a4e74..a300820465e7cc83de4d974009de453eca364135 100644 (file)
--- a/helm/software/lambda-delta/dual_rg/drg.ml
+++ b/helm/software/lambda-delta/dual_rg/drg.ml
@@ -14,28 +14,24 @@
 
 type uri = Entity.uri
 type id = Entity.id
+type attrs = Entity.attrs
 
-type attr = Name of id * bool  (* name, real? *)
-         | Priv               (* private global definition *)
-
-type attrs = attr list (* attributes *)
-
-type bind = Abst of attrs * term (* attrs, domain *)
-          | Abbr of attrs * term (* attrs, body   *)
-          | Void of attrs        (* attrs         *)
+type bind = Abst of term list (* domains *)
+          | Abbr of term list (* bodies  *)
+          | Void of int       (* number of exclusions *)
 
 and term = Sort of attrs * int              (* attrs, hierarchy index *)
-         | LRef of attrs * int              (* attrs, position index *)
+         | LRef of attrs * int * int        (* attrs, position indexes *)
          | GRef of attrs * uri              (* attrs, reference *)
          | Cast of attrs * term * term      (* attrs, domain, element *)
          | Appl of attrs * term list * term (* attrs, arguments, function *)
-        | Bind of lenv * term              (* closure, scope *)
-
-and lenv = bind list (* local environment *)
+        | Proj of attrs * lenv * term      (* attrs, closure, member *)
+        | Bind of attrs * bind * term      (* attrs, binder, scope *)
 
-type entry = bind Entity.entry (* age, uri, binder *)
+and lenv = Null
+         | Cons of lenv * attrs * bind (* closure, attrs, binder *)
 
-type entity = bind Entity.entity
+type entity = term Entity.entity
 
 (* helpers ******************************************************************)
 
@@ -43,22 +39,16 @@ let mk_uri root f s =
    let str = String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] in
    f str
 
-let rec name_of err f = function
-   | Name (n, r) :: _ -> f n r
-   | _ :: tl          -> name_of err f tl
-   | []               -> err ()
+let empty_lenv = Null
 
-let name_of_binder err f = function
-   | Abst (a, _) -> name_of err f a
-   | Abbr (a, _) -> name_of err f a
-   | Void a      -> name_of err f a
+let push f lenv a b = f (Cons (lenv, a, b))
 
 let resolve_lref err f id lenv =
-   let rec aux f i = function
-     | []      -> err ()
-     | b :: tl ->
-        let err () = aux f (succ i) tl in
-       let f name _ = if name = id then f i else err () in
-       name_of_binder err f b
+   let rec aux f i k = function
+     | Null            -> err ()
+     | Cons (tl, a, _) ->
+        let err kk = aux f (succ i) (k + kk) tl in
+       let f j = f i j k in
+       Entity.resolve err f id a
    in
-   aux f 0 lenv
+   aux f 0 0 lenv