X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fxml%2FxmlCrg.ml;h=45e33178a4ffacc651b4f1eb897e80e6326d36b1;hb=e7f64fe2cc67f3514131c8831f87311ff600d005;hp=62f0654bd9ee593bb8c1cf73394a60a06fa09039;hpb=bb2a0b22a2c38b59ca664b550f34e5e40e6f04c7;p=helm.git

diff --git a/helm/software/lambda-delta/src/xml/xmlCrg.ml b/helm/software/lambda-delta/src/xml/xmlCrg.ml
index 62f0654bd..45e33178a 100644
--- a/helm/software/lambda-delta/src/xml/xmlCrg.ml
+++ b/helm/software/lambda-delta/src/xml/xmlCrg.ml
@@ -9,13 +9,13 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module U = NUri
-module C = Cps
-module H = Hierarchy
-module Y = Entity
-module A = Alpha
-module X = XmlLibrary
-module D = Crg
+module U  = NUri
+module C  = Cps
+module H  = Hierarchy
+module Y  = Entity
+module R  = Alpha
+module XL = XmlLibrary
+module D  = Crg
 
 (* internal functions *******************************************************)
 
@@ -32,7 +32,7 @@ let list_rev_iter map e ns l out tab =
            pp_lenv print_string e; print_string " |- "; 
 	   pp_term print_string hd; print_newline ();
 *)
-	   map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
+	   map e hd out tab; f (D.push2 C.err C.start e ~attr:n ~t:hd ())
 	in
 	aux err f e (ns, tl) 
       | _                 -> err ()
@@ -54,38 +54,35 @@ let rec exp_term e t out tab = match t with
          let f s = Y.Name (s, true) :: a in
 	 H.string_of_sort err f l
       in
-      let attrs = [X.position l; X.name a] in
-      X.tag X.sort attrs out tab
+      let attrs = [XL.position l; XL.name a] in
+      XL.tag XL.sort attrs out tab
    | D.TLRef (a, i, j)    ->
       let a = 
          let err _ = a in
 	 let f n r = Y.Name (n, r) :: a in
          D.get_name err f i j e
       in
-      let attrs = [X.position i; X.offset j; X.name a] in
-      X.tag X.lref attrs out tab
+      let attrs = [XL.position i; XL.offset j; XL.name a] in
+      XL.tag XL.lref attrs out tab
    | D.TGRef (a, n)       ->
       let a = Y.Name (U.name_of_uri n, true) :: a in
-      let attrs = [X.uri n; X.name a] in
-      X.tag X.gref attrs out tab
+      let attrs = [XL.uri n; XL.name a] in
+      XL.tag XL.gref attrs out tab
    | D.TCast (a, u, t)    ->
       let attrs = [] in
-      X.tag X.cast attrs ~contents:(exp_term e u) out tab;
+      XL.tag XL.cast attrs ~contents:(exp_term e u) out tab;
       exp_term e t out tab
    | D.TAppl (a, vs, t)   ->
-      let attrs = [X.arity (List.length vs)] in
-      X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
+      let attrs = [XL.arity vs] in
+      XL.tag XL.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
       exp_term e t out tab
    | D.TProj (a, lenv, t) ->
       let attrs = [] in
-      X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
+      XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
       exp_term (D.push_proj C.start e a lenv) t out tab
    | D.TBind (a, b, t) ->
 (* NOTE: the inner binders are alpha-converted first *)
-(*       so undesirable renamings might occur        *)
-(* EX:   we rename [x][x]x to [x][x_]x_              *)
-(*       whereas [x_][x]x would be more desirable    *)
-      let a = A.alpha (D.names_of_lenv [] e) a in
+      let a = R.alpha (D.names_of_lenv [] e) a in
       exp_bind e a b out tab; 
       exp_term (D.push_bind C.start e a b) t out tab 
 
@@ -93,21 +90,21 @@ and exp_bind e a b out tab =
    let f a ns = a, ns in
    let a, ns = Y.get_names f a in 
    match b with
-      | D.Abst ws ->
-	 let e = D.push_bind C.start e a (D.Abst []) in
-	 let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
-         X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
-      | D.Abbr vs ->
+      | D.Abst (n, ws) ->
+	 let e = D.push_bind C.start e a (D.Abst (n, [])) in
+	 let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity ws] in
+         XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
+      | D.Abbr vs      ->
          let e = D.push_bind C.start e a (D.Abbr []) in
-         let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
-         X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
-      | D.Void n ->
-         let attrs = [X.name a; X.mark a; X.arity n] in
-         X.tag X.void attrs out tab
+         let attrs = [XL.name ns; XL.mark a; XL.arity vs] in
+         XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
+      | D.Void n       ->
+         let attrs = [XL.name a; XL.mark a; XL.arity ~n []] in
+         XL.tag XL.void attrs out tab
 
 and exp_eproj e a lenv out tab =
    let attrs = [] in
-   X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+   XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
 
 (* interface functions ******************************************************)