From 4a8188a2b460ab014379c508abac933690b48555 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 6 Oct 2012 10:08:27 +0000 Subject: 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 --- plugins/xml/dumptree.ml4 | 3 - plugins/xml/proof2aproof.ml | 78 ------------------------- plugins/xml/proofTree2Xml.ml4 | 133 ------------------------------------------ plugins/xml/xml_plugin.mllib | 2 - plugins/xml/xmlcommand.ml | 34 +---------- plugins/xml/xmlcommand.mli | 11 ---- 6 files changed, 3 insertions(+), 258 deletions(-) delete mode 100644 plugins/xml/proof2aproof.ml delete mode 100644 plugins/xml/proofTree2Xml.ml4 (limited to 'plugins') 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 "" - | Daimon -> str "" - | Decl_proof _ -> str "" -;; 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 *) -(* 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 *) -(* 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 "\n" ; - X.xml_cdata ("\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 -- cgit v1.2.3