X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgOutput.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgOutput.ml;h=1aa3f9db7d4ecc0ddda91c04138d7bb9db7c140c;hb=5780dca4cfcee57e680213186cf3eaae402b6c88;hp=aaa559be687f46f0d89a8a1b3de72a00269a8731;hpb=3532e6714b7d0ee10b692e41c356866cfab5c646;p=helm.git

diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml
index aaa559be6..1aa3f9db7 100644
--- a/helm/software/lambda-delta/basic_rg/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml
@@ -15,6 +15,7 @@ module U = NUri
 module L = Log
 module H = Hierarchy
 module O = Output
+module CL = CommonLibrary
 module B = Brg
 
 (* nodes count **************************************************************)
@@ -185,3 +186,52 @@ let pp_context frm c =
 let specs = {
    L.pp_term = pp_term; L.pp_context = pp_context
 }
+
+(* term xml printing ********************************************************)
+
+let id frm a =
+   let f = function
+      | None            -> ()
+      | Some (true, s)  -> F.fprintf frm " name=%S" s
+      | Some (false, n) -> F.fprintf frm " name=%S" ("^" ^ n)
+   in      
+   B.name f a
+
+let rec exp_term frm = function
+   | B.Sort (a, l)    ->
+      F.fprintf frm "<Sort position=%S%a/>" (string_of_int l) id a
+   | B.LRef (a, i)    ->
+      F.fprintf frm "<LRef position=%S%a/>" (string_of_int i) id a
+   | B.GRef (a, u)    ->
+      F.fprintf frm "<GRef uri=%S%a/>" (U.string_of_uri u) id a
+   | B.Cast (a, w, t) ->
+      F.fprintf frm "<Cast%a/>%a%a" id a exp_boxed w exp_term t 
+   | B.Appl (a, v, t) ->
+      F.fprintf frm "<Appl%a/>%a%a" id a exp_boxed v exp_term t 
+   | B.Bind (a, b, t) ->
+      F.fprintf frm "%a%a" (exp_bind a) b exp_term t
+
+and exp_boxed frm t =
+   F.fprintf frm "@,@[<v3>   %a@]@," exp_term t
+
+and exp_bind a frm = function
+   | B.Abst w ->
+      F.fprintf frm "<Abst%a/>%a" id a exp_boxed w
+   | B.Abbr v ->
+      F.fprintf frm "<Abbr%a/>%a" id a exp_boxed v
+   | B.Void   ->
+      F.fprintf frm "<Void%a/>" id a
+
+let export_obj frm = function
+   | _, uri, B.Abst w -> 
+      let str = U.string_of_uri uri in
+      F.fprintf frm "%s@,@,<ABST uri=%S>%a</ABST>" 
+         (CL.doctype "ABST") str exp_boxed w
+   | _, uri, B.Abbr v -> 
+      let str = U.string_of_uri uri in
+      F.fprintf frm "%s@,@,<ABBR uri=%S>%a</ABBR>"
+         (CL.doctype "ABBR") str exp_boxed v
+   | _, uri, B.Void   -> 
+      let str = U.string_of_uri uri in
+      F.fprintf frm "%s@,@,<VOID uri=%S/>" 
+         (CL.doctype "VOID") str