module L = Log
module H = Hierarchy
module O = Output
+module CL = CommonLibrary
module B = Brg
(* nodes count **************************************************************)
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