xml contribution created.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@756 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 766 insertions, 0 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
new file mode 100644
index 000000000..4440c5063
--- /dev/null
+++ b/contrib/xml/xmlcommand.ml
@@ -0,0 +1,766 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A tactic to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 02/12/1999                                 *)
+(*                                                                            *)
+(* This module defines the functions that implements the new commands         *)
+(*                                                                            *)
+(******************************************************************************)
+
+
+(* CONFIGURATION PARAMETERS *)
+
+let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
+let verbose = ref false;; (* always set to true during a "Print XML All" *)
+
+
+
+exception ImpossiblePossible;;
+type formal_parameters =
+   Actual of string
+ | Possible of string
+;;
+
+
+(* LOCAL MODULES *)
+
+(* Next local module because I can't use the standard module Str in a tactic, *)
+(* so I reimplement the part of it I need                                     *)
+module Str =
+ struct
+  exception WrongTermSuffix of string;;
+
+  (* substitute character c1 with c2 in string str *)
+  let rec substitute str c1 c2 =
+   try
+    let pos = String.index str c1 in
+     str.[pos] <- c2 ;
+     substitute str c1 c2
+   with
+    Not_found -> str ;;
+
+  (* change the suffix suf1 with suf2 in the string str *)
+  let change_suffix str suf1 suf2 =
+   let module S = String in
+    let len  = S.length str
+    and lens = S.length suf1 in
+     if S.sub str (len - lens) lens = suf1 then
+      (S.sub str 0 (len - lens)) ^ suf2
+     else
+      raise (WrongTermSuffix str) ;;
+ end
+;;
+
+(* UTILITY FUNCTIONS *)
+
+let print_if_verbose s = if !verbose then print_string s;;
+
+let ext_of_tag =
+ function
+    "CONSTANT"        -> "con"
+  | "MUTUALINDUCTIVE" -> "ind"
+  | "VARIABLE"        -> "var"
+  | _                 -> "err" (* uninteresting thing that won't be printed *)
+;;
+
+(* could_have_namesakes sp = true iff o is an object that could be cooked and *)
+(* than that could exists in cooked form with the same name in a super        *)
+(* section of the actual section                                              *)
+let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
+ let module D = Declare in
+  let tag = Libobject.object_tag o in
+   match tag with
+      "CONSTANT" ->
+        (match D.constant_strength sp with
+            D.DischargeAt _  -> false (* a local definition *)
+          | D.NeverDischarge -> true  (* a non-local one    *)
+        )
+    | "VARIABLE"        -> false  (* variables are local, so no namesakes     *)
+    | "MUTUALINDUCTIVE" -> true   (* mutual inductive types are never local   *)
+    | _                 -> false  (* uninteresting thing that won't be printed*)
+;;
+
+(* uri_of_path sp is a broken (wrong) uri pointing to the object whose        *)
+(* section path is sp                                                         *)
+let uri_of_path sp =
+(*CSCV7
+ let ext_of_sp sp =
+  let module N = Names in
+   try
+    let lobj = Lib.map_leaf (N.objsp_of sp) in
+    let tag = Libobject.object_tag lobj in
+     ext_of_tag tag
+   with _ -> Util.anomaly ("wrong search of term " ^ N.string_of_path sp)
+*) let ext_of_sp sp = "v7"
+ in
+  let module S = String in
+   let str = Names.string_of_path sp in
+    let uri = Str.substitute str '#' '/' in
+     let uri' = "cic:" ^ uri in
+      let uri'' = Str.change_suffix uri' ".cci" ("." ^ ext_of_sp sp) in
+       uri''
+;;
+
+let string_of_sort =
+ let module T = Term in
+  function
+     T.Prop(T.Pos)  -> "Set"
+   | T.Prop(T.Null) -> "Prop"
+   | T.Type(_)      -> "Type"
+;;
+
+let string_of_name =
+ let module N = Names in
+  function
+     N.Name id -> N.string_of_id id
+   | _         -> Util.anomaly "this should not happen"
+;;
+
+(* A SIMPLE DATA STRUCTURE AND SOME FUNCTIONS TO MANAGE THE CURRENT *)
+(* ENVIRONMENT (= [l1, ..., ln] WHERE li IS THE LIST OF VARIABLES   *)
+(* DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT SECTION        *)
+
+(*CSC: commento sbagliato ed obsoleto *)
+(* list of variables availables in the actual section *)
+let pvars = ref [];;
+
+let pvars_to_string pvars =
+ let rec aux =
+  function
+     [] -> (0, "")
+   | he::tl -> 
+      let (n,s) = aux tl in
+       (n + 1,
+        string_of_int n ^ ": " ^ (String.concat " ") (List.rev he) ^
+         match s with "" -> "" | _ -> " " ^ s 
+       )
+ in
+  snd (aux (List.rev pvars))
+;;
+
+exception XmlCommandInternalError;;
+
+let add_to_pvars v =
+ match !pvars with
+    []       -> raise XmlCommandInternalError
+  | (he::tl) -> pvars := (v::he)::tl
+;;
+
+let get_depth_of_var v =
+ let rec aux n =
+  function
+     [] -> None
+   | (he::tl) -> if List.mem v he then Some n else aux (n + 1) tl
+ in
+  aux 0 !pvars
+;;
+
+(* FUNCTIONS TO CREATE IDENTIFIERS *)
+
+(* seed to create the next identifier *)
+let next_id = ref 0;;
+
+(* reset_id () reset the identifier seed to 0 *)
+let reset_id () =
+ next_id := 0
+;;
+
+(* get_next_id () returns fresh identifier *)
+let get_next_id () =
+ let res = 
+  "i" ^ string_of_int !next_id
+ in
+  incr next_id ;
+  res
+;;
+
+(* FUNCTION TO PRINT A SINGLE TERM OF CIC *)
+
+(* print_term t l where t is a term of Cic returns a stream of XML tokens *)
+(* suitable to be printed via the pretty printer Xml.pp. l is the list of *)
+(* bound names                                                            *)
+let print_term l csr =
+ let module N = Names in
+ let module T = Term in
+ let module X = Xml in
+  let rec names_to_ids =
+   function
+      [] -> []
+    | (N.Name id)::l -> id::(names_to_ids l)
+    | _ -> names_to_ids l
+  in
+  let rec term_display l cstr =
+   (* kind_of_term helps doing pattern matching hiding the lower level of *)
+   (* coq coding of terms (the one of the logical framework)              *)
+   match T.kind_of_term cstr with
+     T.IsRel n  ->
+      (match List.nth l (n - 1) with
+          N.Name id ->
+            X.xml_empty "REL"
+             ["value",(string_of_int n) ;
+              "binder",(N.string_of_id id) ;
+              "id", get_next_id ()]
+        | N.Anonymous -> raise XmlCommandInternalError
+     )
+   | T.IsVar id ->
+      let depth =
+       match get_depth_of_var (N.string_of_id id) with
+          None -> "?" (* when printing via Show XML Proof or Print XML id *)
+                      (* no infos about variables uri are known           *)
+        | Some n -> string_of_int n
+      in
+       X.xml_empty "VAR"
+        ["relUri",depth ^ "," ^ (N.string_of_id id) ;
+         "id", get_next_id ()]
+   | T.IsMeta n ->
+      X.xml_empty "META" ["no",(string_of_int n) ; "id", get_next_id ()]
+   | T.IsSort s ->
+      X.xml_empty "SORT" ["value",(string_of_sort s) ; "id", get_next_id ()]
+   | T.IsCast (t1,t2) ->
+      X.xml_nempty "CAST" ["id", get_next_id ()]
+       [< X.xml_nempty "term" [] (term_display l t1) ;
+          X.xml_nempty "type" [] (term_display l t2)
+       >]
+   | T.IsLetIn (nid,s,_,d)->
+      let nid' = N.next_name_away nid (names_to_ids l) in
+       X.xml_nempty "LETIN" ["id", get_next_id ()]
+        [< X.xml_nempty "term" [] (term_display l s) ;
+           X.xml_nempty "target" ["binder",(N.string_of_id nid')]
+            (term_display ((N.Name nid')::l) d)
+        >]
+   | T.IsProd (N.Name _ as nid, t1, t2) ->
+      let nid' = N.next_name_away nid (names_to_ids l) in
+       X.xml_nempty "PROD" ["id", get_next_id ()]
+        [< X.xml_nempty "source" [] (term_display l t1) ;
+           X.xml_nempty "target" ["binder",(N.string_of_id nid')]
+            (term_display ((N.Name nid')::l) t2)
+        >]
+   | T.IsProd (N.Anonymous as nid, t1, t2) ->
+      X.xml_nempty "PROD" ["id", get_next_id ()]
+       [< X.xml_nempty "source" [] (term_display l t1) ;
+          X.xml_nempty "target" [] (term_display (nid::l) t2)
+       >]
+   | T.IsLambda (N.Name _ as nid, t1, t2) ->
+      let nid' = N.next_name_away nid (names_to_ids l) in
+       X.xml_nempty "LAMBDA" ["id", get_next_id ()]
+        [< X.xml_nempty "source" [] (term_display l t1) ;
+           X.xml_nempty "target" ["binder",(N.string_of_id nid')]
+            (term_display ((N.Name nid')::l) t2)
+        >]
+   | T.IsLambda (N.Anonymous as nid, t1, t2) ->
+      X.xml_nempty "LAMBDA" ["id", get_next_id ()]
+       [< X.xml_nempty "source" [] (term_display l t1) ;
+          X.xml_nempty "target" [] (term_display (nid::l) t2) >]
+   | T.IsApp (h,t) ->
+      X.xml_nempty "APPLY" ["id", get_next_id ()]
+       [< (term_display l h) ;
+          (Array.fold_right (fun x i -> [< (term_display l x) ; i >]) t [<>])
+       >]
+   | T.IsConst (sp,_) ->
+      X.xml_empty "CONST" ["uri",(uri_of_path sp) ; "id", get_next_id ()]
+   | T.IsMutInd ((sp,i),_) ->
+      X.xml_empty "MUTIND"
+       ["uri",(uri_of_path sp) ;
+        "noType",(string_of_int i) ;
+        "id", get_next_id ()]
+   | T.IsMutConstruct (((sp,i),j),_) ->
+      X.xml_empty "MUTCONSTRUCT"
+       ["uri",(uri_of_path sp) ;
+        "noType",(string_of_int i) ;
+        "noConstr",(string_of_int j) ;
+        "id", get_next_id ()]
+   | T.IsMutCase ((_,((sp,i),_,_,_,_)),ty,term,a) ->
+      let (uri, typeno) = (uri_of_path sp),i in
+       X.xml_nempty "MUTCASE"
+        ["uriType",uri ; "noType",(string_of_int typeno) ; "id",get_next_id ()]
+        [< X.xml_nempty "patternsType" [] [< (term_display l ty) >] ;
+	   X.xml_nempty "inductiveTerm" [] [< (term_display l term) >] ;
+	   Array.fold_right
+            (fun x i ->
+              [< X.xml_nempty "pattern" [] [< term_display l x >] ; i>]
+            ) a [<>]
+        >]
+   | T.IsFix ((ai,i),(t,f,b)) ->
+      X.xml_nempty "FIX" ["noFun", (string_of_int i) ; "id",get_next_id ()]
+       [< Array.fold_right
+           (fun (fi,ti,bi,ai) i ->
+             [< X.xml_nempty "FixFunction"
+                 ["name", (string_of_name fi); "recIndex", (string_of_int ai)]
+	         [< X.xml_nempty "type" [] [< term_display l ti >] ;
+	            X.xml_nempty "body" [] [< term_display ((List.rev f)@l) bi >]
+	         >] ;
+                i
+             >]
+           )
+	   (Array.mapi (fun j x -> (x,t.(j),b.(j),ai.(j)) ) (Array.of_list f) )
+           [<>]
+       >]
+   | T.IsCoFix (i,(t,f,b)) ->
+      X.xml_nempty "COFIX" ["noFun", (string_of_int i) ; "id",get_next_id ()]
+       [< Array.fold_right
+           (fun (fi,ti,bi) i ->
+            [< X.xml_nempty "CofixFunction" ["name", (string_of_name fi)]
+	        [< X.xml_nempty "type" [] [< term_display l ti >] ;
+	           X.xml_nempty "body" [] [< term_display ((List.rev f)@l) bi >]
+	        >] ;
+               i
+            >]
+	   )
+	   (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) (Array.of_list f) ) [<>]
+       >]
+   | T.IsXtra _ ->
+      Util.anomaly "Xtra node in a term!!!"
+   | T.IsEvar _ ->
+      Util.anomaly "Evar node in a term!!!"
+  in
+    (*CSC: ad l vanno andrebbero aggiunti i nomi da non *)
+    (*CSC: mascherare (costanti? variabili?)            *)
+    term_display l csr
+;;
+
+(* FUNCTIONS TO PRINT A SINGLE OBJECT OF COQ *)
+
+(* print_current_proof term type id conjectures                            *)
+(*  where term        is the term of the proof in progress p               *)
+(*  and   type        is the type of p                                     *)
+(*  and   id          is the identifier (name) of p                        *)
+(*  and   conjectures is the list of conjectures (cic terms)               *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_current_proof c typ id mv =
+ let module X = Xml in
+  reset_id () ;
+  [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+     X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+     X.xml_nempty "CurrentProof" ["name",id ; "id", get_next_id ()]
+       [< List.fold_right
+           (fun (j,t) i ->
+             [< X.xml_nempty "Conjecture" ["no",(string_of_int j)]
+                 [< print_term [] t >] ; i >])
+           mv [<>] ;
+          X.xml_nempty "body" [] [< print_term [] c >] ;
+          X.xml_nempty "type"  [] [< print_term [] typ >]
+       >]
+  >]
+;;
+
+(* print_axiom id type params                                              *)
+(*  where type        is the type of an axiom a                            *)
+(*  and   id          is the identifier (name) of a                        *)
+(*  and   params      is the list of formal params for a                   *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_axiom id typ fv =
+ let module X = Xml in
+ let module N = Names in
+  reset_id () ;
+  [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+     X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+     X.xml_nempty "Axiom"
+      (["name",(N.string_of_id id) ; "id", get_next_id ()] @
+       match fv with
+          Possible _ -> raise ImpossiblePossible
+        | Actual fv' -> ["params",fv']
+      ) [< X.xml_nempty "type" [] (print_term [] typ) >]
+  >]
+;;
+
+(* print_definition id term type params                                    *)
+(*  where id          is the identifier (name) of a definition d           *)
+(*  and   term        is the term (body) of d                              *)
+(*  and   type        is the type of d                                     *)
+(*  and   params      is the list of formal params for d                   *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_definition id c typ fv =
+ let module X = Xml in
+ let module N = Names in
+  reset_id () ;
+  [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+     X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+     X.xml_nempty "Definition"
+      (["name",(N.string_of_id id) ; "id", get_next_id ()] @
+       match fv with
+          Possible fv' -> ["params",fv' ; "paramMode","POSSIBLE"]
+        | Actual fv' -> ["params",fv'])
+      [< X.xml_nempty "body" [] (print_term [] c) ;
+         X.xml_nempty "type"  [] (print_term [] typ) >]
+  >]
+;;
+
+(* print_variable id type                                                  *)
+(*  where id          is the identifier (name) of a variable v             *)
+(*  and   type        is the type of v                                     *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_variable id typ =
+ let module X = Xml in
+ let module N = Names in
+  reset_id () ;
+  [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+     X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+     X.xml_nempty "Variable" ["name",(N.string_of_id id) ; "id", get_next_id ()]
+      (X.xml_nempty "type" [] (print_term [] typ))
+  >]
+;;
+
+(* print_mutual_inductive_packet p                                           *)
+(*  where p is a mutual inductive packet (an inductive definition in a block *)
+(*          of mutual inductive definitions)                                 *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp   *)
+(* Used only by print_mutual_inductive                                       *)
+let print_mutual_inductive_packet names p =
+ let module D = Declarations in
+ let module N = Names in
+ let module T = Term in
+ let module X = Xml in
+  let {D.mind_consnames=consnames ;
+       D.mind_typename=typename ;
+       D.mind_nf_lc=lc ;
+       D.mind_nf_arity=arity ;
+       D.mind_finite=finite} = p
+  in
+   [< X.xml_nempty "InductiveType"
+       ["name",(N.string_of_id typename) ;
+        "inductive",(string_of_bool finite)
+       ]
+       [<
+          X.xml_nempty "arity" [] (print_term [] (T.body_of_type arity)) ;
+          (Array.fold_right
+           (fun (name,lc) i ->
+             [< X.xml_nempty "Constructor" ["name",(N.string_of_id name)]
+                 (print_term names lc) ;
+                i
+             >])
+	   (Array.mapi (fun j x -> (x,T.body_of_type lc.(j)) ) consnames )
+           [<>]
+          )
+       >]
+   >]
+;;
+
+(* print_mutual_inductive packs params nparams                             *)
+(*  where packs       is the list of inductive definitions in the block of *)
+(*                    mutual inductive definitions b                       *)
+(*  and   params      is the list of formal params for b                   *)
+(*  and   nparams     is the number of "parameters" in the arity of the    *)
+(*                    mutual inductive types                               *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_mutual_inductive packs fv nparams =
+ let module D = Declarations in
+ let module X = Xml in
+ let module N = Names in
+  let names =
+   List.map
+    (fun p -> let {D.mind_typename=typename} = p in N.Name(typename))
+    (Array.to_list packs)
+  in
+   reset_id () ;
+   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+      X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
+       dtdname ^ "\">\n\n") ;
+      X.xml_nempty "InductiveDefinition"
+       (["noParams",string_of_int nparams ; "id",get_next_id ()] @
+        (match fv with
+            Possible fv' -> ["params",fv' ; "paramMode","POSSIBLE"]
+          | Actual fv' -> ["params",fv']))
+       [< (Array.fold_right
+            (fun x i -> [< print_mutual_inductive_packet names x ; i >])
+            packs
+            [< >]
+          )
+       >]
+   >]
+;;
+
+(* print id dest                                                          *)
+(*  where id   is the identifier (name) of a definition/theorem or of an  *)
+(*             inductive definition                                       *)
+(*  and   dest is either None (for stdout) or (Some filename)             *)
+(* pretty prints via Xml.pp the object whose identifier is id on dest     *)
+(* Note: it is printed only (and directly) the most cooked available      *)
+(*       form of the definition (all the parameters are                   *)
+(*       lambda-abstracted, but the object can still refer to variables)  *)
+let print id fn =
+ let module D = Declarations in
+ let module G = Global in
+ let module N = Names in
+ let module T = Term in
+ let module X = Xml in
+  let str = N.string_of_id id in
+  let sp = Nametab.sp_of_id N.CCI id in
+  let pp_cmds =
+   begin
+    try
+     let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
+     let typ = T.body_of_type typ in
+      begin
+       match val0 with
+          None -> print_axiom id typ (Actual "")
+        | Some lcvr ->
+           match !lcvr with
+              D.Cooked c -> print_definition id c typ (Actual "")
+            | D.Recipe _ ->
+               print_string " COOKING THE RECIPE\n" ;
+               ignore (D.cook_constant lcvr) ;
+               let {D.const_body=val0 ; D.const_type = typ} =
+                G.lookup_constant sp in
+               let typ = T.body_of_type typ in
+                begin
+                 match val0 with
+                   Some {contents= D.Cooked c} ->
+                    print_definition id c typ (Actual "")
+                 | _ -> Util.error "COOKING FAILED"
+                end
+          end
+    with
+     Not_found ->
+      try
+       let {D.mind_packets=packs ; D.mind_nparams=nparams} =
+        G.lookup_mind sp
+       in
+        print_mutual_inductive packs (Actual "") nparams
+      with
+       Not_found ->
+        Util.anomaly ("print: this should not happen")
+   end
+  in
+   Xml.pp pp_cmds fn
+;;
+ 
+(* show dest                                                  *)
+(*  where dest is either None (for stdout) or (Some filename) *)
+(* pretty prints via Xml.pp the proof in progress on dest     *)
+let show fn =
+(*
+ let pftst = Pfedit.get_pftreestate () in
+ let id = Pfedit.get_proof () in
+ let pf = Tacmach.proof_of_pftreestate pftst in
+ let typ = (Proof_trees.goal_of_proof pf).Evd.concl in
+ (*CSC: ntrefiner copied verbatim from natural, used, but _not_ understood *)
+ let val0, mv = Ntrefiner.nt_extract_open_proof (Vartab.initial_sign ()) pf in
+ let mv_t = List.map (function i, (t, _) -> i,t) mv in
+  Xml.pp (print_current_proof val0 typ id mv_t) fn
+*) ()
+;;
+
+(* FUNCTIONS TO PRINT AN ENTIRE SECTION OF COQ *)
+
+(* list of (name, uncooked sp, most cooked sp, uncooked leaf object,  *)
+(*          list of possible variables, directory name)               *)
+(* used to collect informations on the uncooked and most cooked forms *)
+(* of objects that could be cooked (have namesakes)                   *)
+let toprint = ref [];;
+
+(* makes a filename from a directory name, a section path and an extension *)
+let mkfilename dn sp ext =
+ let rec join_dirs cwd =
+   function
+      [] -> ""
+    | he::tail ->
+       let newcwd = cwd ^ "/" ^ he in
+        (try
+          Unix.mkdir newcwd 0o775
+         with _ -> () (* Let's ignore the errors on mkdir *)
+        ) ;
+        he ^ "/" ^ join_dirs newcwd tail
+ in
+  let module N = Names in
+   match dn with
+      None         -> None
+    | Some basedir ->
+       let (dirs, filename, _) = N.repr_path sp in
+        let dirs = List.rev dirs in (* misteries of Coq *)
+         Some (basedir ^ "/" ^ join_dirs basedir dirs ^
+               N.string_of_id filename ^ "." ^ ext ^ ".xml")
+;;
+
+(* Next exception is used only inside print_object *)
+exception Uninteresting;;
+
+(* print_object leaf_object id section_path directory_name formal_vars      *)
+(*  where leaf_object    is a leaf object                                   *)
+(*  and   id             is the identifier (name) of the definition/theorem *)
+(*                       or of the inductive definition o                   *)
+(*  and   section_path   is the section path of o                           *)
+(*  and   directory_name is the base directory in which putting the print   *)
+(*  and   formal_vars    is the list of parameters (variables) of o         *)
+(* pretty prints via Xml.pp the object o in the right directory deduced     *)
+(* from directory_name and section_path                                     *)
+(* Note: it is printed only the uncooked available form of the object plus  *)
+(*       the list of parameters of the object deduced from it's most cooked *)
+(*       form                                                               *)
+let print_object o id sp dn fv =
+ let module D = Declarations in
+ let module G = Global in
+ let module N = Names in
+ let module T = Term in
+ let module X = Xml in
+  let lobj = o in
+  let tag = Libobject.object_tag lobj in
+  let pp_cmds () =
+   match tag with
+      "CONSTANT" ->
+         (*CSC: QUI CI SONO ANCHE LE VARIABILI, CREDO, CHIAMATE const_hyps *)
+         let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
+         let typ = T.body_of_type typ in
+          begin
+           match val0 with
+              None -> print_axiom id typ fv
+            | Some lcvr ->
+               match !lcvr with
+                  D.Cooked c -> print_definition id c typ fv
+                | D.Recipe _ -> Util.anomaly "trying to print a recipe"
+          end
+    | "MUTUALINDUCTIVE" ->
+         (*CSC: QUI CI SONO ANCHE LE VARIABILI, CREDO, CHIAMATE mind_hyps *)
+         let {D.mind_packets=packs ; D.mind_nparams=nparams} =
+          G.lookup_mind sp
+         in
+           print_mutual_inductive packs fv nparams
+    | "VARIABLE" ->
+        (*CHE COSA E' IL PRIMO ARGOMENTO?*)
+        let (_,typ) = G.lookup_named id in
+         add_to_pvars (N.string_of_id id) ;
+         print_variable id (T.body_of_type typ)
+    | "CLASS"
+    | "COERCION"
+    | _ -> raise Uninteresting
+  and fileext = ext_of_tag tag
+  in
+   try
+    Xml.pp (pp_cmds ()) (mkfilename dn sp fileext)
+   with
+    Uninteresting -> ()
+;;
+
+(* print_library_segment state bprintleaf directory_name                      *)
+(*  where state          is a list of (section-path, node)                    *)
+(*  and   bprintleaf     is true iff the leaf objects should be printed       *)
+(*  and   directory_name is the name of the base directory in which to print  *)
+(*                       the files                                            *)
+(* print via print_node all the nodes (leafs excluded if bprintleaf is false) *)(* in state                                                                   *)
+let rec print_library_segment state bprintleaf dn =
+  List.iter
+   (function (sp, node) ->
+     print_if_verbose (Names.string_of_path sp ^ "\n") ;
+     print_node node (Names.basename sp) sp bprintleaf dn ;
+     print_if_verbose "\n"
+   ) state
+(* print_node node id section_path bprintleaf directory_name             *)
+(* prints a single node (and all it's subnodes via print_library_segment *)
+and print_node n id sp bprintleaf dn =
+ let module L = Lib in
+  match n with
+     L.Leaf o ->
+      print_if_verbose "LEAF\n" ;
+      if bprintleaf then
+       begin
+        let to_print =
+         try
+          let _ =
+           List.find (function (x,_,_,_,_,_) -> x=id) !toprint
+          in
+           false
+         with Not_found -> true
+        in
+         if to_print then
+          (* this is an uncooked term or a local (with no namesakes) term *)
+          begin
+           if could_have_namesakes o sp then
+            (* this is an uncooked term *)
+            toprint := (id,sp,sp,o,!pvars,dn)::!toprint
+           else
+            (* this is a local term *)
+            print_object o id sp dn (Possible (pvars_to_string !pvars)) ;
+            print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n")
+          end
+         else
+          (* update the least cooked sp *)
+          toprint :=
+           List.map
+            (function
+               (id',usp,_,uo,pv,dn) when id' = id -> (id,usp,sp,uo,pv,dn)
+             | t -> t
+            ) !toprint
+       end
+   | L.OpenedSection s -> print_if_verbose ("OpenDir " ^ s ^ "\n")
+   | L.ClosedSection (s,state) ->
+      print_if_verbose("ClosedDir " ^ s ^ "\n") ;
+      if bprintleaf then
+       begin
+        (* open a new scope *)
+        pvars := []::!pvars ;
+        print_library_segment state bprintleaf dn ;
+        (* close the scope *)
+        match !pvars with
+           [] -> raise XmlCommandInternalError
+         | he::tl -> pvars := tl
+       end ;
+      print_if_verbose "/ClosedDir\n"
+   | L.Module s ->
+      print_if_verbose ("Module " ^ s ^ "\n")
+   | L.FrozenState _ ->
+      print_if_verbose ("FrozenState\n")
+;;
+
+(* print_closed_section module_name node directory_name                      *)
+(*  where module_name is the name of a module                                *)
+(*  and   node is the library segment of the module                          *)
+(*  and   directory_name is the base directory in which to put the xml files *)
+(* prints all the leaf objects of the tree rooted in node using              *)
+(* print_library_segment on all its sons                                     *)
+let print_closed_section s ls dn =
+ let module L = Lib in
+ let module C = Cooking in
+  toprint := [] ;
+  (*CSC: this should always be empty yet! But just to be sure... :-) *)
+  pvars := [] ;
+  print_if_verbose ("Module " ^ s ^ ":\n") ;
+  print_library_segment ls true dn ;
+  print_if_verbose "\nNow saving cooking information: " ;
+  List.iter
+   (function
+      (id,usp,csp,uo,pv,dn) ->
+       print_if_verbose ("\nCooked=" ^ (Names.string_of_path csp) ^
+        "\tUncooked=" ^ (Names.string_of_path usp)) ;
+       let formal_vars = C.add_cooking_information csp pv in
+        pvars := pv ;
+        (*CSC Actual was Some *)
+        print_object uo id usp dn (Actual formal_vars)
+   ) !toprint ;
+  print_if_verbose "\n/Module\n" ;
+;;
+
+(* printModule identifier directory_name                                     *)
+(*  where identifier     is the name of a module (section) d                 *)
+(*  and   directory_name is the directory in which to root all the xml files *)
+(* prints all the xml files and directories corresponding to the subsections *)
+(* and terms of the module d                                                 *)
+(* Note: the terms are printed in their uncooked form plus the informations  *)
+(* on the parameters of their most cooked form                               *)
+let printModule id dn =
+ let module L = Library in
+ let module N = Names in
+ let module X = Xml in
+  let str = N.string_of_id id in 
+  let sp = Lib.make_path id N.OBJ in
+  let ls = L.module_segment (Some str) in
+   print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
+    L.module_filename str ^ "\n") ;
+   print_closed_section str ls dn ;
+   print_if_verbose ("MODULE_END " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
+    L.module_filename str ^ "\n")
+;;
+
+(* print All () prints what is the structure of the current environment of *)
+(* Coq. No terms are printed. Useful only for debugging                    *)
+let printAll () =
+ let state = Library.module_segment None in
+  let oldverbose = !verbose in
+   verbose := true ;
+   print_library_segment state false None ;
+   let ml = Library.loaded_modules () in
+    List.iter (function i -> printModule (Names.id_of_string i) None) ml ;
+    verbose := oldverbose
+;;