new intermediate language complete_rg,

[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 c11614af56c4268ad7c4bdf93df7f5a44b0ab27d..ce14855e0abd4b21bd68ea20116d255a545f6e9f 100644 (file)
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -19,33 +19,20 @@ module D  = Crg
 
 (* internal functions *******************************************************)
 
-let rec list_iter map l out tab = match l with
-   | []       -> ()
-   | hd :: tl -> map hd out tab; list_iter map tl out tab
-
-let list_rev_iter map e ns l out tab =
-   let rec aux err f e = function
-      | [], []            -> f e
-      | n :: ns, hd :: tl -> 
-        let f e =
-(*     
-           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 ~attr:n ~t:hd ())
-       in
-       aux err f e (ns, tl) 
-      | _                 -> err ()
+let lenv_iter map_bind map_appl map_proj 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)
+      | D.EAppl (e, a, v) ->
+         let e = aux e in
+         map_appl 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)
    in
-   ignore (aux C.err C.start e (ns, l))
-
-let lenv_iter map1 map2 l out tab = 
-   let rec aux f = function
-      | D.ESort              -> f ()
-      | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
-      | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
-   in 
-   aux C.start l
+   ignore (aux lenv)
 
 let rec exp_term e t out tab = match t with
    | D.TSort (a, l)       ->
@@ -56,13 +43,13 @@ let rec exp_term e t out tab = match t with
       in
       let attrs = [XL.position l; XL.name a] in
       XL.tag XL.sort attrs out tab
-   | D.TLRef (a, i, j)    ->
+   | D.TLRef (a, i)       ->
       let a = 
          let err _ = a in
         let f n r = Y.Name (n, r) :: a in
-         D.get_name err f i j e
+         D.get_name err f i e
       in
-      let attrs = [XL.position i; XL.offset j; XL.name a] 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
@@ -72,39 +59,38 @@ let rec exp_term e t out tab = match t with
       let attrs = [] in
       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 = [XL.arity vs] in
-      XL.tag XL.appl attrs ~contents:(list_iter (exp_term e) vs) 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
    | D.TProj (a, lenv, t) ->
       let attrs = [] in
-      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
+      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
    | 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 e a b) t out tab 
+      exp_term (D.push_bind C.start a b e) t out tab 
+
+and exp_appl e a v out tab =
+   let attrs = [] in
+   XL.tag XL.appl attrs ~contents:(exp_term e v) out tab;
 
-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 (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 = [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_bind 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
+   | D.Abbr v      ->
+      let attrs = [XL.name a] in
+      XL.tag XL.abbr attrs ~contents:(exp_term e v) out tab
+   | D.Void        ->
+      let attrs = [XL.name a] in
+      XL.tag XL.void attrs out tab
 
-and exp_eproj e a lenv out tab =
+and exp_proj e a lenv out tab =
    let attrs = [] in
-   XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+   XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj e lenv) out tab
 
 (* interface functions ******************************************************)