X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fxml%2FxmlCrg.ml;h=5d112bed2d1dcd7ebc924556711f41db9006a439;hb=4217fb2c3c93019cdf9c22a80ed46d6814f1cb7d;hp=b2029149be5999b0824ba1511e8f77cfbd44a17c;hpb=a0c8e5f59273c09542a1b8184dd1577d8f4240d7;p=helm.git

diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml
index b2029149b..5d112bed2 100644
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -17,83 +17,87 @@ module R  = Alpha
 module XL = XmlLibrary
 module D  = Crg
 
+IFDEF OBJECTS THEN
+
 (* internal functions *******************************************************)
 
 let lenv_iter map_bind map_appl map_proj st e lenv out tab = 
    let rec aux = function
-      | D.ESort           -> e
-      | D.EBind (e, a, b) ->
+      | D.ESort              -> e
+      | D.EBind (e, a, y, b) ->
          let e = aux e in
 (* NOTE: the inner binders are alpha-converted first *)
-         let a = R.alpha D.mem e a in
-         map_bind st e a b out tab; D.EBind (e, a, b)
-      | D.EAppl (e, a, x, v) ->
+         let y = R.alpha D.mem e y in
+         map_bind st e a y b out tab; D.EBind (e, a, y, b)
+      | D.EAppl (e, x, v)    ->
          let e = aux e in
-         map_appl st e a x v out tab; D.EAppl (e, a, x, v)
-      | D.EProj (e, a, d) ->
+         map_appl st e x v out tab; D.EAppl (e, x, v)
+      | D.EProj (e, d)       ->
          let e = aux e in
-         map_proj st e a d out tab; D.EProj (e, a, d)
+         map_proj st e d out tab; D.EProj (e, d)
    in
    ignore (aux lenv)
 
 let rec exp_term st e t out tab = match t with
-   | D.TSort (a, h)       ->
-      let a =
-         let err _ = a in
-         let f s = {a with E.n_name = Some (s, true)} in
-	 H.string_of_sort err f h
+   | D.TSort k         ->
+      let y =
+         let err _ = E.empty_bind in
+         let f s = E.bind_attrs ~name:(s, true) () in
+	 H.string_of_sort err f k
       in
-      let attrs = [XL.position h; XL.name a] in
+      let attrs = [XL.position k; XL.name y] in
       XL.tag XL.sort attrs out tab
-   | D.TLRef (a, i)       ->
-      let a = 
-         let err _ = a in
-	 let f n r = {a with E.n_name = Some (n, r)} in
+   | D.TLRef (_, i)    ->
+      let y = 
+         let err _ = E.empty_bind in
+	 let f s r = E.bind_attrs ~name:(s, r) () in
          D.get_name err f i e
       in
-      let attrs = [XL.depth i; XL.name a] in
+      let attrs = [XL.depth i; XL.name y] in
       XL.tag XL.lref attrs out tab
-   | D.TGRef (a, n)       ->
-      let a = {a with E.n_name = Some (U.name_of_uri n, true)} in
-      let attrs = [XL.uri n; XL.name a] in
+   | D.TGRef (_, n)    ->
+      let y = E.bind_attrs ~name:(U.name_of_uri n, true) () in
+      let attrs = [XL.uri n; XL.name y] in
       XL.tag XL.gref attrs out tab
-   | D.TCast (a, u, t)    ->
+   | D.TCast (u, t)    ->
       let attrs = [] in
       XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab;
       exp_term st e t out tab
-   | D.TAppl (a, x, v, t) ->
+   | D.TAppl (x, v, t) ->
       let attrs = [] in
       XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
       exp_term st e t out tab
-   | D.TProj (a, lenv, t) ->
+   | D.TProj (lenv, t) ->
       let attrs = [] in
       XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab;
-      exp_term st (D.push_proj C.start a lenv e) t out tab
-   | D.TBind (a, b, t) ->
+      exp_term st (D.push_proj C.start lenv e) t out tab
+   | D.TBind (y, b, t) ->
 (* NOTE: the inner binders are alpha-converted first *)
-      let a = R.alpha D.mem e a in
-      exp_bind st e a b out tab; 
-      exp_term st (D.push_bind C.start a b e) t out tab 
+      let y = R.alpha D.mem e y in
+      exp_bind st e E.empty_node y b out tab; 
+      exp_term st (D.push_bind C.start E.empty_node y b e) t out tab 
 
-and exp_appl st e a x v out tab =
+and exp_appl st e x v out tab =
    let attrs = [] in
    XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
 
-and exp_bind st e a b out tab = match b with
+and exp_bind st e a y b out tab = match b with
    | D.Abst (_, n, w) ->
-      let attrs = [XL.layer st n; XL.name a] in
+      let attrs = XL.layer st n :: XL.name y :: XL.side y @ XL.main y in
       XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
    | D.Abbr v         ->
-      let attrs = [XL.name a] in
+      let attrs = [XL.name y] in
       XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
    | D.Void           ->
-      let attrs = [XL.name a] in
+      let attrs = [XL.name y] in
       XL.tag XL.void attrs out tab
 
-and exp_proj st e a lenv out tab =
+and exp_proj st e lenv out tab =
    let attrs = [] in
    XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab
 
 (* interface functions ******************************************************)
 
 let export_term st = exp_term st D.empty_lenv
+
+END