Intégration de la branche mowgli

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

1 files changed, 823 insertions, 0 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
new file mode 100644
index 0000000000..151d4582b9
--- /dev/null
+++ b/contrib/xml/xmlcommand.ml
@@ -0,0 +1,823 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*****************************************************************************)
+(*                                                                           *)
+(*                             PROJECT MoWGLI                                *)
+(*                                                                           *)
+(*                    A module to print Coq objects in XML                   *)
+(*                                                                           *)
+(*               Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                22/06/2002                                 *)
+(*                                                                           *)
+(*****************************************************************************)
+
+
+(* CONFIGURATION PARAMETERS *)
+
+(*CSC: was false*)
+let verbose = ref true;; (* always set to true during a "Print XML All" *)
+
+(* UTILITY FUNCTIONS *)
+
+let print_if_verbose s = if !verbose then print_string s;;
+
+(* Next exception is used only inside print_coq_object and tag_of_string_tag *)
+exception Uninteresting;;
+
+(*CSC: CODE USEFUL ONLY FOR THE CODE COMMENTED OUT
+let tag_of_string_tag =
+ function
+    "CONSTANT"
+  | "PARAMETER"       -> Constant
+  | "INDUCTIVE"       -> Inductive
+  | "VARIABLE"        -> Variable
+  | _                 -> raise Uninteresting
+;;
+*)
+
+(* Internally, for Coq V7, params of inductive types are associated     *)
+(* not to the whole block of mutual inductive (as it was in V6) but to  *)
+(* each member of the block; but externally, all params are required    *)
+(* to be the same; the following function checks that the parameters    *)
+(* of each inductive of a same block are all the same, then returns     *)
+(* this number; it fails otherwise                                      *)
+let extract_nparams pack =
+ let module D = Declarations in
+ let module U = Util in
+ let module S = Sign in
+
+  let {D.mind_nparams=nparams0} = pack.(0) in
+  let arity0 = pack.(0).D.mind_user_arity in
+  let params0, _ = S.decompose_prod_n_assum nparams0 arity0 in
+  for i = 1 to Array.length pack - 1 do
+    let {D.mind_nparams=nparamsi} = pack.(i) in
+    let arityi = pack.(i).D.mind_user_arity in
+    let paramsi, _ = S.decompose_prod_n_assum nparamsi arityi in
+    if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block"
+  done;
+  nparams0
+
+(* 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 DK = Decl_kinds in
+ let module D = Declare in
+  let tag = Libobject.object_tag o in
+   print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
+   match tag with
+      "CONSTANT" ->
+        (match D.constant_strength sp with
+          | DK.Local  -> false (* a local definition *)
+          | DK.Global -> true  (* a non-local one    *)
+        )
+    | "PARAMETER"                 (* axioms and                               *)
+    | "INDUCTIVE"       -> true   (* mutual inductive types are never local   *)
+    | "VARIABLE"        -> false  (* variables are local, so no namesakes     *)
+    | _                 -> false  (* uninteresting thing that won't be printed*)
+;;
+
+
+(* A SIMPLE DATA STRUCTURE AND SOME FUNCTIONS TO MANAGE THE CURRENT *)
+(* ENVIRONMENT (= [(name1,l1); ...;(namen,ln)] WHERE li IS THE LIST *)
+(* OF VARIABLES DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT   *)
+(* SECTION, WHOSE PATH IS namei                                     *)
+
+let pvars =
+ ref ([Names.id_of_string "",[]] : (Names.identifier * string list) list);;
+let cumenv = ref Environ.empty_env;;
+
+(* filter_params pvars hyps *)
+(* filters out from pvars (which is a list of lists) all the variables *)
+(* that does not belong to hyps (which is a simple list)               *)
+(* It returns a list of couples relative section path -- list of       *)
+(* variable names.                                                     *)
+let filter_params pvars hyps =
+ let rec aux ids =
+  function
+     [] -> []
+   | (id,he)::tl ->
+      let ids' = id::ids in
+      let ids'' =
+       "cic:/" ^
+        String.concat "/" (List.rev (List.map Names.string_of_id ids')) in
+      let he' =
+       ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in
+      let tl' = aux ids' tl in
+       match he' with
+          _,[] -> tl'
+        | _,_  -> he'::tl'
+ in
+  let cwd = Lib.cwd () in
+  let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
+  let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in
+   aux (Names.repr_dirpath modulepath) (List.rev pvars)
+;;
+
+type variables_type = 
+   Definition of string * Term.constr * Term.types
+ | Assumption of string * Term.constr
+;;
+
+let add_to_pvars x =
+ let module E = Environ in
+  let v =
+   match x with
+      Definition (v, bod, typ) ->
+       cumenv :=
+         E.push_named (Names.id_of_string v, Some bod, typ) !cumenv ;
+       v
+    | Assumption (v, typ) ->
+       cumenv :=
+         E.push_named (Names.id_of_string v, None, typ) !cumenv ;
+       v
+  in
+   match !pvars with
+      []       -> assert false
+    | ((name,l)::tl) -> pvars := (name,v::l)::tl
+;;
+
+(* The computation is very inefficient, but we can't do anything *)
+(* better unless this function is reimplemented in the Declare   *)
+(* module.                                                       *)
+let search_variables () =
+ let module N = Names in
+  let cwd = Lib.cwd () in
+  let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
+  let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in
+   let rec aux =
+    function
+       [] -> []
+     | he::tl as modules ->
+        let one_section_variables =
+         let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in
+          let t = List.map N.string_of_id (Declare.last_section_hyps dirpath) in
+           [he,t]
+        in
+         one_section_variables @ aux tl
+   in
+    aux
+     (Cic2acic.remove_module_dirpath_from_dirpath
+       ~basedir:modulepath cwd)
+;;
+
+(* FUNCTIONS TO PRINT A SINGLE OBJECT OF COQ *)
+
+let body_filename_of_filename =
+ function
+    Some f -> Some (f ^ ".body")
+  | None   -> None
+;;
+
+let types_filename_of_filename =
+ function
+    Some f -> Some (f ^ ".types")
+  | None   -> None
+;;
+
+let prooftree_filename_of_filename =
+ function
+    Some f -> Some (f ^ ".proof_tree")
+  | None   -> None
+;;
+
+let print_object uri obj sigma proof_tree_infos filename =
+ (* function to pretty print and compress an XML file *)
+(*CSC: Unix.system "gzip ..." is an orrible non-portable solution. *)
+ let pp xml filename =
+  Xml.pp xml filename ;
+  match filename with
+     None -> ()
+   | Some fn ->
+      let fn' =
+       let rec escape s n =
+        try
+         let p = String.index_from s n '\'' in
+          String.sub s n (p - n) ^ "\\'" ^ escape s (p+1)
+        with Not_found -> String.sub s n (String.length s - n)
+       in
+        escape fn 0
+      in
+       ignore (Unix.system ("gzip " ^ fn' ^ ".xml"))
+ in
+  let (annobj,_,constr_to_ids,_,ids_to_inner_sorts,ids_to_inner_types,_,_) =
+   Cic2acic.acic_object_of_cic_object !pvars sigma obj in
+  let (xml, xml') = Acic2Xml.print_object uri ids_to_inner_sorts annobj in
+  let xmltypes =
+   Acic2Xml.print_inner_types uri ids_to_inner_sorts ids_to_inner_types in
+  pp xml filename ;
+  begin
+   match xml' with
+      None -> ()
+    | Some xml' -> pp xml' (body_filename_of_filename filename)
+  end ;
+  pp xmltypes (types_filename_of_filename filename) ;
+  match proof_tree_infos with
+     None -> ()
+   | Some (sigma0,proof_tree,proof_tree_to_constr,
+           proof_tree_to_flattened_proof_tree) ->
+      let xmlprooftree =
+       ProofTree2Xml.print_proof_tree
+        uri sigma0 proof_tree proof_tree_to_constr
+        proof_tree_to_flattened_proof_tree constr_to_ids
+      in
+       pp xmlprooftree (prooftree_filename_of_filename filename)
+;;
+
+let string_list_of_named_context_list =
+ List.map
+  (function (n,_,_) -> Names.string_of_id n)
+;;
+
+(* Function to collect the variables that occur in a term. *)
+(* Used only for variables (since for constants and mutual *)
+(* inductive types this information is already available.  *)
+let find_hyps t =
+ let module T = Term in
+  let rec aux l t =
+   match T.kind_of_term t with
+      T.Var id when not (List.mem id l) ->
+       let (_,bo,ty) = Global.lookup_named id in
+        let boids = 
+         match bo with
+            Some bo' -> aux l bo'
+          | None -> l
+        in
+         id::(aux boids ty)
+    | T.Var _
+    | T.Rel _
+    | T.Meta _
+    | T.Evar _
+    | T.Sort _ -> l
+    | T.Cast (te,ty) -> aux (aux l te) ty
+    | T.Prod (_,s,t) -> aux (aux l s) t
+    | T.Lambda (_,s,t) -> aux (aux l s) t
+    | T.LetIn (_,s,_,t) -> aux (aux l s) t
+    | T.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl
+    | T.Const con ->
+       let hyps = (Global.lookup_constant con).Declarations.const_hyps in
+        map_and_filter l hyps @ l
+    | T.Ind ind
+    | T.Construct (ind,_) ->
+       let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in
+        map_and_filter l hyps @ l
+    | T.Case (_,t1,t2,b) ->
+       Array.fold_left (fun i x -> aux i x) (aux (aux l t1) t2) b
+    | T.Fix (_,(_,tys,bodies))
+    | T.CoFix (_,(_,tys,bodies)) ->
+       let r = Array.fold_left (fun i x -> aux i x) l tys in
+        Array.fold_left (fun i x -> aux i x) r bodies
+  and map_and_filter l =
+   function
+      [] -> []
+    | (n,_,_)::tl when not (List.mem n l) -> n::(map_and_filter l tl)
+    | _::tl -> map_and_filter l tl
+  in
+   aux [] t
+;;
+
+(* Functions to construct an object *)
+
+let mk_variable_obj id body typ =
+ let hyps,unsharedbody =
+  match body with
+     None -> [],None
+   | Some bo -> find_hyps bo, Some (Unshare.unshare bo)
+ in
+  let hyps' = find_hyps typ @ hyps in
+  let hyps'' = List.map Names.string_of_id hyps' in
+  let variables = search_variables () in
+  let params = filter_params variables hyps'' in
+   Acic.Variable
+    (Names.string_of_id id, unsharedbody,
+     (Unshare.unshare (Term.body_of_type typ)), params)
+;;
+
+(* Unsharing is not performed on the body, that must be already unshared. *)
+(* The evar map and the type, instead, are unshared by this function.     *)
+let mk_current_proof_obj id bo ty evar_map env =
+ let unshared_ty = Unshare.unshare (Term.body_of_type ty) in
+ let metasenv =
+  List.map
+   (function
+     (n, {Evd.evar_concl = evar_concl ;
+          Evd.evar_hyps = evar_hyps}
+      ) ->
+       (* We map the named context to a rel context and every Var to a Rel *)
+       let final_var_ids,context =
+        let rec aux var_ids =
+         function
+            [] -> var_ids,[]
+          | (n,None,t)::tl ->
+              let final_var_ids,tl' = aux (n::var_ids) tl in
+              let t' = Term.subst_vars var_ids t in
+               final_var_ids,(n, Acic.Decl (Unshare.unshare t'))::tl'
+          | (n,Some b,t)::tl ->
+              let final_var_ids,tl' = aux (n::var_ids) tl in
+              let b' = Term.subst_vars var_ids b in
+               (* t will not be exported to XML. Thus no unsharing performed *)
+               final_var_ids,(n, Acic.Def  (Unshare.unshare b',t))::tl'
+        in
+         aux [] (List.rev evar_hyps)
+       in
+        (* We map the named context to a rel context and every Var to a Rel *)
+        (n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl))
+   ) (Evd.non_instantiated evar_map)
+ in
+  let id' = Names.string_of_id id in
+   if metasenv = [] then
+    let ids =
+     Names.Idset.union
+      (Environ.global_vars_set env bo) (Environ.global_vars_set env ty) in
+    let hyps0 = Environ.keep_hyps env ids in
+    let hyps = string_list_of_named_context_list hyps0 in
+    (* Variables are the identifiers of the variables in scope *)
+    let variables = search_variables () in
+    let params = filter_params variables hyps in
+     Acic.Constant (id',Some bo,unshared_ty,params)
+   else
+    Acic.CurrentProof (id',metasenv,bo,unshared_ty)
+;;
+
+let mk_constant_obj id bo ty variables hyps =
+ let hyps = string_list_of_named_context_list hyps in
+ let ty = Unshare.unshare (Term.body_of_type ty) in
+ let params = filter_params variables hyps in
+  match bo with
+     None ->
+      Acic.Constant (Names.string_of_id id,None,ty,params)
+   | Some c ->
+      Acic.Constant
+       (Names.string_of_id id, Some (Unshare.unshare (Declarations.force c)),
+         ty,params)
+;;
+
+let mk_inductive_obj sp packs variables hyps finite =
+ let module D = Declarations in
+  let hyps = string_list_of_named_context_list hyps in
+  let params = filter_params variables hyps in
+  let nparams = extract_nparams packs in
+   let tys =
+    let tyno = ref (Array.length packs) in
+    Array.fold_right
+     (fun p i ->
+       decr tyno ;
+       let {D.mind_consnames=consnames ;
+            D.mind_typename=typename ;
+            D.mind_nf_arity=arity} = p
+       in
+        let lc = Inductive.arities_of_constructors (Global.env ()) (sp,!tyno) in
+        let cons =
+         (Array.fold_right (fun (name,lc) i -> (name,lc)::i)
+          (Array.mapi
+           (fun j x ->(x,Unshare.unshare (Term.body_of_type lc.(j)))) consnames)
+          []
+         )
+        in
+         (typename,finite,Unshare.unshare arity,cons)::i
+     ) packs []
+   in
+    Acic.InductiveDefinition (tys,params,nparams)
+;;
+
+(* print id dest                                                          *)
+(*  where sp   is the qualified identifier (section path) of a            *)
+(*             definition/theorem, variable or 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 (_,qid as locqid) fn =
+ let module D = Declarations in
+ let module De = Declare in
+ let module G = Global in
+ let module N = Names in
+ let module Nt = Nametab in
+ let module T = Term in
+ let module X = Xml in
+ let module Ln = Libnames in
+  let (_,id) = Libnames.repr_qualid qid in
+  let glob_ref =
+(*CSC: ask Hugo why Nametab.global does not work with variables and *)
+(*CSC: we have to do this hugly try ... with                        *)
+   try
+    Nt.global locqid
+   with
+    _ -> let (_,id) = Ln.repr_qualid qid in Ln.VarRef id
+  in
+  (* Variables are the identifiers of the variables in scope *)
+  let variables = search_variables () in
+  let keep_sections,kn,tag,obj =
+   match glob_ref with
+      Ln.VarRef id ->
+       let sp = Declare.find_section_variable id in
+       (* this kn is fake since it is not provided by Coq *)
+       let kn = 
+        let (mod_path,dir_path) = Lib.current_prefix () in
+        N.make_kn mod_path dir_path (N.label_of_id (Ln.basename sp))
+       in
+       let (_,body,typ) = G.lookup_named id in
+        true,kn,Cic2acic.Variable,mk_variable_obj id body typ
+    | Ln.ConstRef kn ->
+       let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
+        G.lookup_constant kn in
+        false,kn,Cic2acic.Constant,mk_constant_obj id val0 typ variables hyps
+    | Ln.IndRef (kn,_) ->
+       let {D.mind_packets=packs ;
+            D.mind_hyps=hyps;
+            D.mind_finite=finite} = G.lookup_mind kn in
+          false,kn,Cic2acic.Inductive,
+           mk_inductive_obj kn packs variables hyps finite
+    | Ln.ConstructRef _ ->
+       Util.anomaly ("print: this should not happen")
+  in
+   print_object (Cic2acic.uri_of_kernel_name ~keep_sections kn tag) obj
+    Evd.empty None 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_pftreestate fn pftst id =
+ let str = Names.string_of_id id in
+ let pf = Tacmach.proof_of_pftreestate pftst in
+ let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in
+ let val0,evar_map,proof_tree_to_constr,proof_tree_to_flattened_proof_tree,
+     unshared_pf
+ =
+  Proof2aproof.extract_open_pftreestate pftst in
+ let kn = Lib.make_kn id in
+ let env = Global.env () in
+ let obj = mk_current_proof_obj id val0 typ evar_map env in
+  print_object (Cic2acic.uri_of_kernel_name kn Cic2acic.Constant) obj evar_map
+   (Some (Tacmach.evc_of_pftreestate pftst,unshared_pf,proof_tree_to_constr,
+    proof_tree_to_flattened_proof_tree)) fn 
+;;
+
+let show fn =
+ let pftst = Pfedit.get_pftreestate () in
+ let id = Pfedit.get_current_proof_name () in
+  show_pftreestate fn pftst id
+;;
+
+(*
+(* 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 printed = ref [];;
+
+(* makes a filename from a directory name, a section path and an extension *)
+let mkfilename dn sp ext =
+(*CSC:
+ let dir_list_of_dirpath s =
+  let rec aux n =
+   try
+    let pos = String.index_from s n '/' in
+    let head = String.sub s n (pos - n) in
+     head::(aux (pos + 1))
+   with
+    Not_found -> [String.sub s n (String.length s - n)]
+  in
+   aux 0
+ in
+ let rec join_dirs cwd =
+   function
+      []  -> assert false
+    | [he] -> "/" ^ he
+    | 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 L = Library in
+  let module S = System in
+  let module N = Names in
+  let module No = Nameops in
+   match dn with
+      None         -> None
+    | Some basedir ->
+	let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in
+	let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in
+       Some (basedir ^ join_dirs basedir dir ^ "." ^ ext)
+*) match dn with None -> None | Some _ -> Some "/tmp/nonloso"
+;;
+
+(* print_coq_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_coq_object lobj id sp dn fv env =
+ let module D = Declarations in
+ let module E = Environ in
+ let module G = Global in
+ let module N = Names in
+ let module T = Term in
+ let module X = Xml in
+(*CSC: GROSSO BUG: env e' l'environment cumulativo in cui aggiungiamo passo passo tutte le variabili. Qui, invece, non lo stiamo piu' usando per nulla. Quindi la prima variabile che incontreremo non verra' trovata ;-(((( Direi che l'environment vada passato fino alla print_object che a sua volta lo passera' a chi di dovere (ovvero sia a Cic2Acic che a DoubleTypeInference *)
+  let strtag = Libobject.object_tag lobj in
+   try
+    let tag = tag_of_string_tag strtag in
+    let obj =
+     match strtag with
+        "CONSTANT"  (* = Definition, Theorem *)
+      | "PARAMETER" (* = Axiom *) ->
+          let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
+           G.lookup_constant sp
+          in
+           mk_constant_obj id val0 typ fv hyps
+      | "INDUCTIVE" ->
+           let
+            {D.mind_packets=packs ;
+             D.mind_hyps = hyps;
+             D.mind_finite = finite
+            } = G.lookup_mind sp
+           in
+            mk_inductive_obj sp packs fv hyps finite
+      | "VARIABLE" ->
+          let (_,(_,varentry,_)) = Declare.out_variable lobj in
+           begin
+            match varentry with
+               Declare.SectionLocalDef (body,optt,opaq) ->
+                 let typ = match optt with
+		   | None -> Retyping.get_type_of env Evd.empty body 
+		   | Some t -> t in
+                 add_to_pvars (Definition (N.string_of_id id, body, typ)) ;
+                 mk_variable_obj id (Some body) typ
+             | Declare.SectionLocalAssum typ ->
+                add_to_pvars (Assumption (N.string_of_id id, typ)) ;
+                mk_variable_obj id None (T.body_of_type typ)
+           end
+      | "CLASS"
+      | "COERCION"
+      | _ -> raise Uninteresting
+    in
+     let fileext () = ext_of_tag tag in
+     let fn = mkfilename dn sp (fileext ()) in
+      print_object (uri_of_path sp tag) obj Evd.empty None fn
+   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 ("Print_library_segment: " ^ Names.string_of_path sp ^ "\n") ;
+     print_node node (Nameops.basename sp) sp bprintleaf dn ;
+     print_if_verbose "\n"
+   ) (List.rev 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
+         if not (List.mem id !printed) then
+          (* this is an uncooked term or a local (with no namesakes) term *)
+          begin
+(*CSC: pezza quando i .vo sono magri
+try
+*)
+           if could_have_namesakes o sp then
+            begin
+             (* this is an uncooked term *)
+             print_if_verbose ("OK, stampo solo questa volta " ^ Names.string_of_id id ^ "\n") ;
+             print_coq_object o id sp dn !pvars !cumenv ;
+             printed := id::!printed
+            end
+           else
+            begin
+             (* this is a local term *)
+             print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n") ;
+             print_coq_object o id sp dn !pvars !cumenv
+            end
+(*CSC: pezza quando i .vo sono magri
+with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n");
+*)
+          end
+         else
+          begin
+           (* update the least cooked sp *)
+           print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n")
+          end
+       end
+   | L.OpenedSection (dir,_) ->
+       let id = snd (Nameops.split_dirpath dir) in
+       print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n")
+   | L.ClosedSection (_,dir,state) ->
+      let id = snd (Nameops.split_dirpath dir) in
+      print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ;
+      if bprintleaf then
+       begin
+        (* open a new scope *)
+        let (_,section_name) = Nameops.split_dirpath dir in
+         pvars := (section_name,[])::!pvars ;
+         print_library_segment state bprintleaf dn ;
+         (* close the scope *)
+         match !pvars with
+            [] -> assert false
+          | he::tl -> pvars := tl
+       end ;
+      print_if_verbose "/ClosedDir\n"
+   | L.Module s ->
+      print_if_verbose ("Module " ^ (Names.string_of_dirpath 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
+  printed := [] ;
+  pvars := [Names.id_of_string "",[]] ;
+  cumenv := Safe_typing.env_of_safe_env (Global.safe_env ()) ;
+  print_if_verbose ("Module " ^ s ^ ":\n") ;
+  print_library_segment ls true dn ;
+  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 (loc,qid) dn =
+ let module L = Library in
+ let module N = Nametab in
+ let module X = Xml in
+
+  let (_,dir_path,_) = L.locate_qualified_library qid in
+
+  let str = N.string_of_qualid qid in 
+  let ls = L.module_segment (Some dir_path) in
+   print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^
+    (L.module_full_filename dir_path) ^ "\n") ;
+   print_closed_section str (List.rev ls) dn ;
+   print_if_verbose ("MODULE_END " ^ str ^ " " ^
+    (L.module_full_filename dir_path) ^ "\n")
+;;
+
+(* printSection identifier directory_name                                    *)
+(*  where identifier     is the name of a closed 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 closed section d                                         *)
+(* Note: the terms are printed in their uncooked form plus the informations  *)
+(* on the parameters of their most cooked form                               *)
+let printSection id dn =
+ let module L = Library in
+ let module N = Names in
+ let module No = Nameops in
+ let module X = Xml in
+  let sp = Lib.make_path id in
+  let ls =
+   let rec find_closed_section =
+    function
+       [] -> raise Not_found
+     | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (No.split_dirpath dir) = id
+	 -> ls
+     | _::t -> find_closed_section t
+   in
+    print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ;
+    find_closed_section (Lib.contents_after None)
+  in
+  let str = N.string_of_id id in 
+   print_if_verbose ("SECTION_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ "\n");
+   print_closed_section str ls dn ;
+   print_if_verbose ("SECTION_END " ^ str ^ " " ^ N.string_of_path sp ^ "\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
+;;
+*)
+
+
+let rec join_dirs cwd =
+ function
+    []  -> assert false
+  | [he] -> cwd ^ "/" ^ he
+  | he::tail ->
+     let newcwd = cwd ^ "/" ^ he in
+      (try
+        Unix.mkdir newcwd 0o775
+       with _ -> () (* Let's ignore the errors on mkdir *)
+      ) ;
+      join_dirs newcwd tail
+;;
+
+let filename_of_path ?(keep_sections=false) xml_library_root kn tag =
+ let module N = Names in
+  match xml_library_root with
+     None -> None  (* stdout *)
+   | Some xml_library_root' ->
+      let tokens = Cic2acic.token_list_of_kernel_name ~keep_sections kn tag in
+       Some (join_dirs xml_library_root' tokens)
+;;
+
+(*CSC: Ask Hugo for a better solution *)
+let qualid_of_kernel_name kn =
+ let module N = Names in
+  let (modpath,_,label) = N.repr_kn kn in
+   match modpath with
+      N.MPself _ -> Libnames.make_qualid (Lib.cwd ()) (N.id_of_label label)
+    | _ ->
+      Util.anomaly ("qualid_of_kernel_name: the module path is not MPself")
+;;
+
+(* Let's register the callbacks *)
+let xml_library_root =
+  try
+   Some (Sys.getenv "COQ_XML_LIBRARY_ROOT")
+  with Not_found -> None
+;;
+
+let proof_to_export = ref None (* holds the proof-tree to export *)
+;;
+
+let _ =
+  Pfedit.set_xml_cook_proof
+   (function pftreestate -> proof_to_export := Some pftreestate)
+;;
+
+let _ =
+  Declare.set_xml_declare_variable
+   (function kn ->
+     let filename =
+      filename_of_path ~keep_sections:true xml_library_root kn
+       Cic2acic.Variable in
+     let qualid = qualid_of_kernel_name kn in
+     let dummy_location = -1,-1 in
+      print (dummy_location,qualid) filename)
+;;
+
+let _ =
+  Declare.set_xml_declare_constant
+   (function kn ->
+     let filename = filename_of_path xml_library_root kn Cic2acic.Constant in
+     let qualid = qualid_of_kernel_name kn in
+     match !proof_to_export with
+        None ->
+         let dummy_location = -1,-1 in
+          print (dummy_location,qualid) filename
+      | Some pftreestate ->
+         (* It is a proof. Let's export it starting from the proof-tree *)
+         (* I saved in the Pfedit.set_xml_cook_proof callback.          *)
+         show_pftreestate filename pftreestate
+          (Names.id_of_label (Names.label kn)) ;
+         proof_to_export := None)
+;;
+
+let _ =
+  Declare.set_xml_declare_inductive
+   (function kn ->
+     let filename = filename_of_path xml_library_root kn Cic2acic.Inductive in
+     let qualid = qualid_of_kernel_name kn in
+     let dummy_location = -1,-1 in
+      print (dummy_location,qualid) filename)
+;;