+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ X.xml_nempty "COFIX"
+ ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
+ [< List.fold_right
+ (fun (id,fi,ti,bi) i ->
+ [< X.xml_nempty "CofixFunction" ["id",id ; "name", fi]
+ [< X.xml_nempty "type" [] [< aux ti >] ;
+ X.xml_nempty "body" [] [< aux bi >]
+ >] ;
+ i
+ >]
+ ) funs [<>]
+ >]
+ and aux_subst buri target subst =
+(*CSC: I have now no way to assign an ID to the explicit named substitution *)
+ let id = None in
+ if subst = [] then
+ target
+ else
+ Xml.xml_nempty "instantiate"
+ (match id with None -> [] | Some id -> ["id",id])
+ [< target ;
+ List.fold_left
+ (fun i (uri,arg) ->
+ let relUri =
+ let buri_frags =
+ Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in
+ let uri_frags =
+ Str.split (Str.regexp "/") (UriManager.string_of_uri uri) in
+ let rec find_relUri buri_frags uri_frags =
+ match buri_frags,uri_frags with
+ [_], _ -> String.concat "/" uri_frags
+ | he1::tl1, he2::tl2 ->
+ assert (he1 = he2) ;
+ find_relUri tl1 tl2
+ | _,_ -> assert false (* uri is not relative to buri *)
+ in
+ find_relUri buri_frags uri_frags
+ in
+ [< i ; Xml.xml_nempty "arg" ["relUri", relUri] (aux arg) >]
+ ) [<>] subst
+ >]
+ in
+ aux
+;;
+
+let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
+ let module C = Cic in
+ let module X = Xml in
+ let module U = UriManager in
+ let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
+ match obj with
+ C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
+ let params' = param_attribute_of_params params in
+ let xml_for_current_proof_body =
+(*CSC: Should the CurrentProof also have the list of variables it depends on? *)
+(*CSC: I think so. Not implemented yet. *)
+ X.xml_nempty "CurrentProof"
+ ["of",UriManager.string_of_uri uri ; "id", id]
+ [< List.fold_left
+ (fun i (cid,n,canonical_context,t) ->
+ [< i ;
+ X.xml_nempty "Conjecture"
+ ["id", cid ; "no",(string_of_int n)]
+ [< List.fold_left
+ (fun i (hid,t) ->
+ [< (match t with
+ Some (n,C.ADecl t) ->
+ X.xml_nempty "Decl"
+ (match n with
+ C.Name n' -> ["id",hid;"name",n']
+ | C.Anonymous -> ["id",hid])
+ (print_term ids_to_inner_sorts t)
+ | Some (n,C.ADef t) ->
+ X.xml_nempty "Def"
+ (match n with
+ C.Name n' -> ["id",hid;"name",n']
+ | C.Anonymous -> ["id",hid])
+ (print_term ids_to_inner_sorts t)
+ | None -> X.xml_empty "Hidden" ["id",hid]
+ ) ;
+ i
+ >]
+ ) [< >] canonical_context ;
+ X.xml_nempty "Goal" []
+ (print_term ids_to_inner_sorts t)
+ >]
+ >])
+ [<>] conjectures ;
+ X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
+ in
+ let xml_for_current_proof_type =
+ X.xml_nempty "ConstantType" ["name",n ; "params",params' ; "id", id]
+ (print_term ids_to_inner_sorts ty)
+ in
+ let xmlbo =
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
+ xml_for_current_proof_body
+ >] in
+ let xmlty =
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
+ xml_for_current_proof_type
+ >]
+ in
+ xmlty, Some xmlbo
+ | C.AConstant (id,idbody,n,bo,ty,params) ->
+ let params' = param_attribute_of_params params in
+ let xmlbo =
+ match bo with
+ None -> None
+ | Some bo ->
+ Some
+ [< X.xml_cdata
+ "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata
+ ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
+ X.xml_nempty "ConstantBody"
+ ["for",UriManager.string_of_uri uri ; "params",params' ;
+ "id", id]
+ [< print_term ids_to_inner_sorts bo >]
+ >]
+ in
+ let xmlty =
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
+ X.xml_nempty "ConstantType"
+ ["name",n ; "params",params' ; "id", id]
+ [< print_term ids_to_inner_sorts ty >]
+ >]
+ in
+ xmlty, xmlbo
+ | C.AVariable (id,n,bo,ty,params) ->
+ let params' = param_attribute_of_params params in
+ let xmlbo =
+ match bo with
+ None -> [< >]
+ | Some bo ->
+ X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >]
+ in
+ let aobj =
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
+ X.xml_nempty "Variable"
+ ["name",n ; "params",params' ; "id", id]
+ [< xmlbo ;
+ X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)