]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_ag/bag.ml
- simpler attribute system
[helm.git] / helm / software / helena / src / basic_ag / bag.ml
index c0e540963e45e26d2b8056da38863b34277f292b..51c644148a55a5a4671da2e6a5b85e4f67efb16e 100644 (file)
@@ -16,22 +16,22 @@ module P = Marks
 module E = Entity
 
 type uri = E.uri
-type attrs = E.node_attrs
+type b_attrs = E.bind_attrs
 
 type bind = Void         (* exclusion *)
           | Abst of term (* abstraction *)
           | Abbr of term (* abbreviation *)
 
-and term = Sort of int                          (* hierarchy index *)
-         | LRef of P.mark                       (* location *)
-         | GRef of uri                          (* reference *)
-         | Cast of term * term                  (* domain, element *)
-         | Appl of term * term                  (* argument, function *)
-         | Bind of attrs * P.mark * bind * term (* name, location, binder, scope *)
+and term = Sort of int                            (* hierarchy index *)
+         | LRef of P.mark                         (* location *)
+         | GRef of uri                            (* reference *)
+         | Cast of term * term                    (* domain, element *)
+         | Appl of term * term                    (* argument, function *)
+         | Bind of b_attrs * P.mark * bind * term (* name, location, binder, scope *)
 
 type entity = term E.entity (* attrs, uri, binder *)
 
-type lenv = (attrs * P.mark * bind) list (* name, location, binder *) 
+type lenv = (b_attrs * P.mark * bind) list (* name, location, binder *) 
 
 type message = (lenv, term) Log.item list
 
@@ -47,24 +47,24 @@ let cast u t = Cast (u, t)
 
 let appl u t = Appl (u, t)
 
-let bind a l b t = Bind (a, l, b, t)
+let bind y l b t = Bind (y, l, b, t)
 
-let bind_abst a l u t = Bind (a, l, Abst u, t)
+let bind_abst y l u t = Bind (y, l, Abst u, t)
 
-let bind_abbr a l v t = Bind (a, l, Abbr v, t)
+let bind_abbr y l v t = Bind (y, l, Abbr v, t)
 
 (* local environment handling functions *************************************)
 
 let empty_lenv = []
 
-let push msg f es a l b =
+let push msg f es y l b =
    let rec does_not_occur loc = function
       | []                          -> true
       | (_, 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 = (a, l, b) :: es in f c
+   let c = (y, l, b) :: es in f c
 
 let append f es1 es2 = 
    f (List.append es2 es1)
@@ -77,7 +77,7 @@ let contents f es = f es
 let get err f es i =
    let rec aux = function
       | []              -> err ()
-      | (a, l, b) :: tl -> if l = i then f a b else aux tl
+      | (y, l, b) :: tl -> if l = i then f y b else aux tl
    in
    aux es