+
+(* term xml printing ********************************************************)
+
+let id frm a =
+ let f s = function
+ | true -> F.fprintf frm " name=%S" s
+ | false -> F.fprintf frm " name=%S" ("^" ^ s)
+ in
+ B.name C.start 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 exp_obj frm = function
+ | _, uri, B.Abst w ->
+ let str = U.string_of_uri uri in
+ F.fprintf frm "<ABST uri=%S/>@,%a" str exp_term w
+ | _, uri, B.Abbr v ->
+ let str = U.string_of_uri uri in
+ F.fprintf frm "<ABBR uri=%S/>@,%a" str exp_term v
+ | _, uri, B.Void ->
+ let str = U.string_of_uri uri in
+ F.fprintf frm "<VOID uri=%S/>" str
+
+let export_obj frm obj =
+ F.fprintf frm "@,@[<v3> %a@]@," exp_obj obj