+ 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 (fi,ti,bi) i ->
+ [< X.xml_nempty "CofixFunction" ["name", fi]
+ [< X.xml_nempty "type" [] [< aux ti >] ;
+ X.xml_nempty "body" [] [< aux bi >]
+ >] ;
+ i
+ >]
+ ) funs [<>]
+ >]
+ in
+ aux
+;;
+
+exception NotImplemented;;
+
+(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
+let print_object curi ~ids_to_inner_sorts =
+ let rec aux =
+ let module C = Cic in
+ let module X = Xml in
+ let module U = UriManager in
+ function
+ C.ACurrentProof (id,n,conjectures,bo,ty) ->
+ X.xml_nempty "CurrentProof" ["name",n ; "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.Anonimous -> ["id",hid])
+ (print_term curi 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.Anonimous -> ["id",hid])
+ (print_term curi ids_to_inner_sorts t)
+ | None -> X.xml_empty "Hidden" ["id",hid]
+ ) ;
+ i
+ >]
+ ) [< >] canonical_context ;
+ X.xml_nempty "Goal" []
+ (print_term curi ids_to_inner_sorts t)
+ >]
+ >])
+ [<>] conjectures ;
+ X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
+ X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >]
+ | C.ADefinition (id,n,bo,ty,C.Actual params) ->
+ let params' =
+ List.fold_right
+ (fun (_,x) i ->
+ List.fold_right
+ (fun x i ->
+ U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
+ ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
+ ) params ""
+ in
+ X.xml_nempty "Definition" ["name",n ; "params",params' ; "id", id]
+ [< X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
+ X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >]
+ | C.ADefinition _ -> assert false
+ | _ -> raise NotImplemented