Clean-up : no more Proof_type.proof_tree

 Btw, remove unused code in the xml plugin and in Tactic_printer

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

6 files changed, 3 insertions, 258 deletions

diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index c29e4a3b3..b8a8c5137 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -47,9 +47,6 @@ let pr_proof_instr_xml instr =
 
 let pr_rule_xml pr = function
   | Prim r -> str "<rule text=\"" ++ xmlstream (pr_prim_rule r) ++ str "\"/>"
-  | Daimon -> str "<daimon/>"
-  | Decl_proof _ -> str "<proof/>"
-;;
 
 let pr_var_decl_xml env (id,c,typ) =
   let ptyp = print_constr_env env typ in
diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml
deleted file mode 100644
index 2d16190bc..000000000
--- a/plugins/xml/proof2aproof.ml
+++ /dev/null
@@ -1,78 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
-(*         *   University of Bologna                                    *)
-(************************************************************************)
-(*          This file is distributed under the terms of the             *)
-(*           GNU Lesser General Public License Version 2.1              *)
-(*                                                                      *)
-(*                 Copyright (C) 2000-2004, HELM Team.                  *)
-(*                       http://helm.cs.unibo.it                        *)
-(************************************************************************)
-
-(* Note: we can not use the Set module here because we _need_ physical *)
-(* equality and there exists no comparison function compatible with    *)
-(* physical equality.                                                  *)
-
-module S =
- struct
-  let empty = []
-  let mem = List.memq
-  let add x l = x::l
- end
-;;
-
-(* evar reduction that preserves some terms *)
-let nf_evar sigma ~preserve =
- let module T = Term in
-  let rec aux t =
-   if preserve t then t else
-    match T.kind_of_term t with
-     | T.Rel _ | T.Meta _ | T.Var _ | T.Sort _ | T.Const _ | T.Ind _
-     | T.Construct _ -> t
-     | T.Cast (c1,k,c2) -> T.mkCast (aux c1, k, aux c2)
-     | T.Prod (na,c1,c2) -> T.mkProd (na, aux c1, aux c2)
-     | T.Lambda (na,t,c) -> T.mkLambda (na, aux t, aux c)
-     | T.LetIn (na,b,t,c) -> T.mkLetIn (na, aux b, aux t, aux c)
-     | T.App (c,l) ->
-        let c' = aux c in
-        let l' = Array.map aux l in
-         (match T.kind_of_term c' with
-             T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l')
-           | T.Cast (he,_,_) ->
-              (match T.kind_of_term he with
-                  T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l')
-                | _ -> T.mkApp (c', l')
-              )
-           | _ -> T.mkApp (c', l'))
-     | T.Evar (e,l) when Evd.mem sigma e & Evd.is_defined sigma e ->
-	aux (Evd.existential_value sigma (e,l))
-     | T.Evar (e,l) -> T.mkEvar (e, Array.map aux l)
-     | T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl)
-     | T.Fix (ln,(lna,tl,bl)) ->
-         T.mkFix (ln,(lna,Array.map aux tl,Array.map aux bl))
-     | T.CoFix(ln,(lna,tl,bl)) ->
-         T.mkCoFix (ln,(lna,Array.map aux tl,Array.map aux bl))
-   in
-    aux
-;;
-
-module ProofTreeHash =
- Hashtbl.Make
-  (struct
-    type t = Proof_type.proof_tree
-    let equal = (==)
-    let hash = Hashtbl.hash
-   end)
-;;
-
-
-let extract_open_proof sigma pf =
-  (* Deactivated and candidate for removal. (Apr. 2010) *)
-   ()
-
-let extract_open_pftreestate pts =
-  (* Deactivated and candidate for removal. (Apr. 2010) *)
-   ()
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
deleted file mode 100644
index 3831ee9fa..000000000
--- a/plugins/xml/proofTree2Xml.ml4
+++ /dev/null
@@ -1,133 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
-(*         *   University of Bologna                                    *)
-(************************************************************************)
-(*          This file is distributed under the terms of the             *)
-(*           GNU Lesser General Public License Version 2.1              *)
-(*                                                                      *)
-(*                 Copyright (C) 2000-2004, HELM Team.                  *)
-(*                       http://helm.cs.unibo.it                        *)
-(************************************************************************)
-
-let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";;
-
-let idref_of_id id = "v" ^ id;;
-
-(* Transform a constr to an Xml.token Stream.t *)
-(* env is a named context                      *)
-(*CSC: in verita' dovrei "separare" le variabili vere e lasciarle come Var! *)
-let constr_to_xml obj sigma env =
-  let ids_to_terms = Hashtbl.create 503 in
-  let constr_to_ids = Acic.CicHash.create 503 in
-  let ids_to_father_ids = Hashtbl.create 503 in
-  let ids_to_inner_sorts = Hashtbl.create 503 in
-  let ids_to_inner_types = Hashtbl.create 503 in
-
-  (* named_context holds section variables and local variables *)
-  let named_context = Environ.named_context env  in
-  (* real_named_context holds only the section variables *)
-  let real_named_context = Environ.named_context (Global.env ()) in
-  (* named_context' holds only the local variables *)
-  let named_context' =
-   List.filter (function n -> not (List.mem n real_named_context)) named_context
-  in
-  let idrefs =
-   List.map
-    (function x,_,_ -> idref_of_id (Names.string_of_id x)) named_context' in
-  let rel_context = Sign.push_named_to_rel_context named_context' [] in
-  let rel_env =
-   Environ.push_rel_context rel_context
-    (Environ.reset_with_named_context
-	(Environ.val_of_named_context real_named_context) env) in
-  let obj' =
-   Term.subst_vars (List.map (function (i,_,_) -> i) named_context') obj in
-  let seed = ref 0 in
-   try
-    let annobj =
-     Cic2acic.acic_of_cic_context' false seed ids_to_terms constr_to_ids
-      ids_to_father_ids ids_to_inner_sorts ids_to_inner_types rel_env
-      idrefs sigma (Unshare.unshare obj') None
-    in
-     Acic2Xml.print_term ids_to_inner_sorts annobj
-   with e ->
-    Errors.anomaly
-     ("Problem during the conversion of constr into XML: " ^
-      Printexc.to_string e)
-;;
-
-let first_word s =
-   try let i = String.index s ' ' in
-       String.sub s 0 i
-   with _ -> s
-;;
-
-let string_of_prim_rule x = match x with
-  | Proof_type.Intro _-> "Intro"
-  | Proof_type.Cut _ -> "Cut"
-  | Proof_type.FixRule _ -> "FixRule"
-  | Proof_type.Cofix _ -> "Cofix"
-  | Proof_type.Refine _ -> "Refine"
-  | Proof_type.Convert_concl _ -> "Convert_concl"
-  | Proof_type.Convert_hyp _->"Convert_hyp"
-  | Proof_type.Thin _ -> "Thin"
-  | Proof_type.ThinBody _-> "ThinBody"
-  | Proof_type.Move (_,_,_) -> "Move"
-  | Proof_type.Order _ -> "Order"
-  | Proof_type.Rename (_,_) -> "Rename"
-  | Proof_type.Change_evars -> "Change_evars"
-
-let
- print_proof_tree curi sigma pf proof_tree_to_constr
-  proof_tree_to_flattened_proof_tree constr_to_ids
-=
- let module PT = Proof_type in
- let module L = Logic in
- let module X = Xml in
-  let ids_of_node node =
-   let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in
-   try
-    Some (Acic.CicHash.find constr_to_ids constr)
-   with _ ->
-Pp.msg_warning (Pp.(++) (Pp.str
-"The_generated_term_is_not_a_subterm_of_the_final_lambda_term")
-(Printer.pr_lconstr constr)) ;
-    None
-  in
-  let rec aux node old_hyps =
-   let of_attribute =
-    match ids_of_node node with
-       None -> []
-     | Some id -> ["of",id]
-   in
-    match node with
-       {PT.ref=Some(PT.Prim tactic_expr,nodes)} ->
-         let tac = string_of_prim_rule tactic_expr in
-         let of_attribute = ("name",tac)::of_attribute in
-          if nodes = [] then
-           X.xml_empty "Prim" of_attribute
-          else
-           X.xml_nempty "Prim" of_attribute
-            (List.fold_left
-              (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
-
-     | {PT.ref=Some(PT.Daimon,_)} ->
-         X.xml_empty "Hidden_open_goal" of_attribute
-
-     | {PT.ref=None;PT.goal=goal} ->
-         X.xml_empty "Open_goal" of_attribute
-     | {PT.ref=Some(PT.Decl_proof _, _)} -> failwith "TODO: xml and decl_proof"
-  in
-   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
-      X.xml_cdata ("<!DOCTYPE ProofTree SYSTEM \""^prooftreedtdname ^"\">\n\n");
-      X.xml_nempty "ProofTree" ["of",curi] (aux pf [])
-   >]
-;;
-
-
-(* Hook registration *)
-(* CSC: debranched since it is bugged
-Xmlcommand.set_print_proof_tree print_proof_tree;;
-*)
diff --git a/plugins/xml/xml_plugin.mllib b/plugins/xml/xml_plugin.mllib
index 90797e8dd..655ea957e 100644
--- a/plugins/xml/xml_plugin.mllib
+++ b/plugins/xml/xml_plugin.mllib
@@ -4,9 +4,7 @@ Acic
 DoubleTypeInference
 Cic2acic
 Acic2Xml
-Proof2aproof
 Xmlcommand
-ProofTree2Xml
 Xmlentries
 Cic2Xml
 Dumptree
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 2550e248a..0673e79fb 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -16,21 +16,6 @@
 
 let verbose = ref false;;
 
-(* HOOKS *)
-let print_proof_tree, set_print_proof_tree =
- let print_proof_tree = ref (fun _ _ _ _ _ _ -> None) in
-  (fun () -> !print_proof_tree),
-   (fun f ->
-     print_proof_tree :=
-     fun
-      curi sigma0 pf proof_tree_to_constr proof_tree_to_flattened_proof_tree
-      constr_to_ids
-     ->
-      Some
-       (f curi sigma0 pf proof_tree_to_constr
-        proof_tree_to_flattened_proof_tree constr_to_ids))
-;;
-
 (* UTILITY FUNCTIONS *)
 
 let print_if_verbose s = if !verbose then print_string s;;
@@ -139,7 +124,7 @@ let theory_filename xml_library_root =
      let alltoks = List.rev toks in
        Some (join_dirs xml_library_root' alltoks ^ ".theory")
 
-let print_object uri obj sigma proof_tree_infos filename =
+let print_object uri obj sigma filename =
  (* function to pretty print and compress an XML file *)
 (*CSC: Unix.system "gzip ..." is an horrible non-portable solution. *)
  let pp xml filename =
@@ -169,20 +154,7 @@ let print_object uri obj sigma proof_tree_infos filename =
       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 =
-       print_proof_tree ()
-        uri sigma0 proof_tree proof_tree_to_constr
-        proof_tree_to_flattened_proof_tree constr_to_ids
-      in
-       match xmlprooftree with
-          None -> ()
-        | Some xmlprooftree ->
-           pp xmlprooftree (prooftree_filename_of_filename filename)
+  pp xmltypes (types_filename_of_filename filename)
 ;;
 
 let string_list_of_named_context_list =
@@ -445,7 +417,7 @@ let print internal glob_ref kind xml_library_root =
   (match internal with
     | Declare.KernelSilent -> ()
     | _ -> print_object_kind uri kind);
-   print_object uri obj Evd.empty None fn
+   print_object uri obj Evd.empty fn
 ;;
 
 let print_ref qid fn =
diff --git a/plugins/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli
index ec50d6234..8e6254efc 100644
--- a/plugins/xml/xmlcommand.mli
+++ b/plugins/xml/xmlcommand.mli
@@ -26,14 +26,3 @@ val print_ref : Libnames.reference -> string option -> unit
 (*  where dest is either None (for stdout) or (Some filename) *)
 (* pretty prints via Xml.pp the proof in progress on dest     *)
 val show : string option -> unit
-
-(* set_print_proof_tree f                                      *)
-(*  sets a callback function f to export the proof_tree to XML *)
-val set_print_proof_tree :
-    (string ->
-     Evd.evar_map ->
-     Proof_type.proof_tree ->
-     Term.constr Proof2aproof.ProofTreeHash.t ->
-     Proof_type.proof_tree Proof2aproof.ProofTreeHash.t ->
-     string Acic.CicHash.t -> Xml.token Stream.t) ->
-    unit