new xml exportation procedure for basic_rg (10 times faster than previous). the stati...

[helm.git] / helm / software / lambda-delta / basic_rg / brgOutput.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml
index 7dfb2b9371d223058a5f4700eb6e55a0b4e9f152..58a407f04867041f157da26ab633b2966127c483 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml
@@ -222,44 +222,50 @@ let specs = {
 
 (* term xml printing ********************************************************)
 
-let rec exp_term c frm = function
+let rec exp_term e t out tab = match t with
    | B.Sort (a, l)    ->
       let a =
          let err _ = a in
          let f s = Y.Name (s, true) :: a in
         H.get_sort err f l
       in
-      F.fprintf frm "<Sort position=%S%a/>" (string_of_int l) X.old_name a
+      let attrs = [X.position l; X.name a] in
+      X.tag X.sort attrs out tab
    | B.LRef (a, i)    ->
       let a = 
          let err _ = a in
         let f n r = Y.Name (n, r) :: a in
         let f _ b = attrs_of_binder (Y.name err f) b in
-         B.get err f c i
+         B.get err f e i
       in
-      F.fprintf frm "<LRef position=%S%a/>" (string_of_int i) X.old_name a
-   | B.GRef (a, u)    ->
-      let a = Y.Name (U.name_of_uri u, true) :: a in
-      F.fprintf frm "<GRef uri=%S%a/>" (U.string_of_uri u) X.old_name a
-   | B.Cast (a, w, t) ->
-      F.fprintf frm "<Cast%a>%a</Cast>@,%a" X.old_name a (exp_boxed c) w (exp_term c) t 
+      let attrs = [X.position i; X.name a] in
+      X.tag X.lref attrs out tab
+   | B.GRef (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
+   | B.Cast (a, u, t) ->
+      let attrs = [] in
+      X.tag X.cast attrs ~contents:(exp_term e u) out tab;
+      exp_term e t out tab
    | B.Appl (a, v, t) ->
-      F.fprintf frm "<Appl%a>%a</Appl>@,%a" X.old_name a (exp_boxed c) v (exp_term c) t 
-   | B.Bind (b, t) ->
-      let f b cc = F.fprintf frm "%a@,%a" (exp_bind c) b (exp_term cc) t in 
-      let f b = B.push (f b) c b in
-      rename_bind f c b
+      let attrs = [] in
+      X.tag X.appl attrs ~contents:(exp_term e v) out tab;
+      exp_term e t out tab
+   | B.Bind (b, t)    ->
+      let b = rename_bind C.start e b in
+      exp_bind e b out tab; 
+      exp_term (B.push C.start e b) t out tab 
 
-and exp_boxed c frm t =
-   F.fprintf frm "@,@[<v3>   %a@]@," (exp_term c) t
-
-and exp_bind c frm = function
+and exp_bind e b out tab = match b with
    | B.Abst (a, w) ->
-      F.fprintf frm "<Abst%a>%a</Abst>" X.old_name a (exp_boxed c) w
+      let attrs = [X.name a; X.mark a] in
+      X.tag X.abst attrs ~contents:(exp_term e w) out tab
    | B.Abbr (a, v) ->
-      F.fprintf frm "<Abbr%a/>%a</Abbr>" X.old_name a (exp_boxed c) v
-   | B.Void a      ->
-      F.fprintf frm "<Void%a/>" X.old_name a
+      let attrs = [X.name a; X.mark a] in
+      X.tag X.abbr attrs ~contents:(exp_term e v) out tab
+   | B.Void a ->
+      let attrs = [X.name a; X.mark a] in
+      X.tag X.void attrs out tab
 
-let export_term frm t =
-   F.fprintf frm "%a" (exp_boxed B.empty_lenv) t
+let export_term = exp_term B.empty_lenv