X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_ag%2Fbag.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_ag%2Fbag.ml;h=fc0f72f9ab6e0df795a63cf13da12c05c6092a20;hb=a5709dff43233c041f77a4ee4b7f2df1a3c51ab6;hp=d6432863db8831e43e4b22548209cc2054af8cb6;hpb=f3f6b451707a3feb8245717e3fa7ca25df0ce8ef;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_ag/bag.ml b/helm/software/lambda-delta/src/basic_ag/bag.ml
index d6432863d..fc0f72f9a 100644
--- a/helm/software/lambda-delta/src/basic_ag/bag.ml
+++ b/helm/software/lambda-delta/src/basic_ag/bag.ml
@@ -15,22 +15,22 @@
 module E = Entity
 
 type uri = E.uri
-type id = E.id
+type attrs = E.attrs
 
 type bind = Void         (* exclusion *)
           | Abst of term (* abstraction *)
           | Abbr of term (* abbreviation *)
 
-and term = Sort of int                    (* hierarchy index *)
-         | LRef of int                    (* location *)
-         | GRef of uri                    (* reference *)
-         | Cast of term * term            (* domain, element *)
-         | Appl of term * term            (* argument, function *)
-         | Bind of int * id * bind * term (* location, name, binder, scope *)
+and term = Sort of int                       (* hierarchy index *)
+         | LRef of int                       (* location *)
+         | GRef of uri                       (* reference *)
+         | Cast of term * term               (* domain, element *)
+         | Appl of term * term               (* argument, function *)
+         | Bind of attrs * int * bind * term (* name, location, binder, scope *)
 
 type entity = term E.entity (* attrs, uri, binder *)
 
-type lenv = (int * id * bind) list (* location, name, binder *) 
+type lenv = (attrs * int * bind) list (* location, name, binder *) 
 
 type message = (lenv, term) Log.item list
 
@@ -46,32 +46,24 @@ let cast u t = Cast (u, t)
 
 let appl u t = Appl (u, t)
 
-let bind l id b t = Bind (l, id, b, t)
+let bind a l b t = Bind (a, l, b, t)
 
-let bind_abst l id u t = Bind (l, id, Abst u, t)
+let bind_abst a l u t = Bind (a, l, Abst u, t)
 
-let bind_abbr l id v t = Bind (l, id, Abbr v, t)
-
-(* location handling functions **********************************************)
-
-let location = ref 0
-
-let new_location () = let loc = !location in incr location; loc
-
-let locations () = !location
+let bind_abbr a l v t = Bind (a, l, Abbr v, t)
 
 (* local environment handling functions *************************************)
 
 let empty_lenv = []
 
-let push msg f es l id b =
+let push msg f es a l b =
    let rec does_not_occur loc = function
       | []                          -> true
-      | (l, _, _) :: _ when l = loc -> false
+      | (_, l, _) :: _ when l = loc -> false
       | _ :: es                     -> does_not_occur l es
    in
    if not (does_not_occur l es) then failwith msg else
-   let c = (l, id, b) :: es in f c
+   let c = (a, l, b) :: es in f c
 
 let append f es1 es2 = 
    f (List.append es2 es1)
@@ -81,9 +73,17 @@ let map f map es =
 
 let contents f es = f es
 
-let get f es i =
+let get err f es i =
    let rec aux = function
-      | []               -> f None
-      | (l, id, b) :: tl -> if l = i then f (Some (id, b)) else aux tl
+      | []              -> err ()
+      | (a, l, b) :: tl -> if l = i then f a b else aux tl
    in
    aux es
+
+let nth err f loc e =
+   let rec aux n = function
+      | []                          -> err loc
+      | (_, l, _) :: _ when l = loc -> f n
+      | _ :: e                      -> aux (succ n) e
+   in
+   aux 0 e