+
+(* term xml printing ********************************************************)
+
+let rec exp_term c frm = function
+ | 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
+ | 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
+ 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
+ | 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
+
+and exp_boxed c frm t =
+ F.fprintf frm "@,@[<v3> %a@]@," (exp_term c) t
+
+and exp_bind c frm = function
+ | B.Abst (a, w) ->
+ F.fprintf frm "<Abst%a>%a</Abst>" X.old_name a (exp_boxed c) w
+ | 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 export_term frm t =
+ F.fprintf frm "%a" (exp_boxed B.empty_lenv) t