- the disambiguation of unified binders continues

[helm.git] / helm / software / helena / src / xml / xmlCrg.ml

diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml
index ce14855e0abd4b21bd68ea20116d255a545f6e9f..ec103f7ec93a7961a5d281bbc35e9c50625b6e52 100644 (file)
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -12,33 +12,35 @@
 module U  = NUri
 module C  = Cps
 module H  = Hierarchy
-module Y  = Entity
+module E  = Entity
 module R  = Alpha
 module XL = XmlLibrary
 module D  = Crg
 
 (* internal functions *******************************************************)
 
-let lenv_iter map_bind map_appl map_proj e lenv out tab = 
+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) -> 
          let e = aux e in
-         map_bind e a b out tab; D.EBind (e, a, b)
+(* 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, v) ->
          let e = aux e in
-         map_appl e a v out tab; D.EAppl (e, a, v)
+         map_appl st e a v out tab; D.EAppl (e, a, v)
       | D.EProj (e, a, d) ->
          let e = aux e in
-         map_proj e a d out tab; D.EProj (e, a, d)
+         map_proj st e a d out tab; D.EProj (e, a, d)
    in
    ignore (aux lenv)
 
-let rec exp_term e t out tab = match t with
+let rec exp_term st e t out tab = match t with
    | D.TSort (a, l)       ->
       let a =
          let err _ = a in
-         let f s = Y.Name (s, true) :: a in
+         let f s = {a with E.n_name = Some (s, true)} in
         H.string_of_sort err f l
       in
       let attrs = [XL.position l; XL.name a] in
@@ -46,52 +48,52 @@ let rec exp_term e t out tab = match t with
    | D.TLRef (a, i)       ->
       let a = 
          let err _ = a in
-        let f n r = Y.Name (n, r) :: a in
+        let f n r = {a with E.n_name = Some (n, r)} in
          D.get_name err f i e
       in
       let attrs = [XL.position i; 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 a = {a with E.n_name = Some (U.name_of_uri n, true)} in
       let attrs = [XL.uri n; XL.name a; XL.apix a] in
       XL.tag XL.gref attrs out tab
    | D.TCast (a, u, t)    ->
       let attrs = [] in
-      XL.tag XL.cast attrs ~contents:(exp_term e u) out tab;
-      exp_term e t out tab
+      XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab;
+      exp_term st e t out tab
    | D.TAppl (a, v, t)    ->
       let attrs = [] in
-      XL.tag XL.appl attrs ~contents:(exp_term e v) out tab;
-      exp_term e t out tab
+      XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
+      exp_term st e t out tab
    | D.TProj (a, lenv, t) ->
       let attrs = [] in
-      XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj e lenv) out tab;
-      exp_term (D.push_proj C.start a lenv e) t out tab
+      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) ->
 (* NOTE: the inner binders are alpha-converted first *)
-      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 a b e) t out tab 
+      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 
 
-and exp_appl e a v out tab =
+and exp_appl st e a v out tab =
    let attrs = [] in
-   XL.tag XL.appl attrs ~contents:(exp_term e v) out tab;
+   XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
 
-and exp_bind e a b out tab = match b with
+and exp_bind st e a b out tab = match b with
    | D.Abst (n, w) ->
-      let attrs = [XL.level n; XL.name a; XL.mark a] in
-      XL.tag XL.abst attrs ~contents:(exp_term e w) out tab
+      let attrs = [XL.level st n; XL.name a] in
+      XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
    | D.Abbr v      ->
       let attrs = [XL.name a] in
-      XL.tag XL.abbr attrs ~contents:(exp_term e v) out tab
+      XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
    | D.Void        ->
       let attrs = [XL.name a] in
       XL.tag XL.void attrs out tab
 
-and exp_proj e a lenv out tab =
+and exp_proj st e a lenv out tab =
    let attrs = [] in
-   XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj e lenv) out tab
+   XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab
 
 (* interface functions ******************************************************)
 
-let export_term = exp_term D.empty_lenv
+let export_term st = exp_term st D.empty_lenv