diff options
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 | ||||
| -rw-r--r-- | plugins/xml/dumptree.ml4 | 3 | ||||
| -rw-r--r-- | plugins/xml/proof2aproof.ml | 78 | ||||
| -rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 133 | ||||
| -rw-r--r-- | plugins/xml/xml_plugin.mllib | 2 | ||||
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 34 | ||||
| -rw-r--r-- | plugins/xml/xmlcommand.mli | 11 | ||||
| -rw-r--r-- | printing/printing.mllib | 1 | ||||
| -rw-r--r-- | printing/tactic_printer.ml | 152 | ||||
| -rw-r--r-- | printing/tactic_printer.mli | 21 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 9 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 16 | ||||
| -rw-r--r-- | proofs/refiner.ml | 10 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 |
16 files changed, 5 insertions, 471 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index f06530442..8e7258062 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -144,7 +144,6 @@ Pcoq Printer Pptactic Ppdecl_proof -Tactic_printer Egramml Egramcoq Himsg diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e65e41847..8e7a92a8f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -20,7 +20,6 @@ open Sign open Univ open Environ open Printer -open Tactic_printer open Term open Termops open Cerrors 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 diff --git a/printing/printing.mllib b/printing/printing.mllib index 6d6e1bba6..f5840bc3e 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -2,6 +2,5 @@ Pputils Ppconstr Printer Pptactic -Tactic_printer Printmod Prettyp diff --git a/printing/tactic_printer.ml b/printing/tactic_printer.ml deleted file mode 100644 index 49d7c21f6..000000000 --- a/printing/tactic_printer.ml +++ /dev/null @@ -1,152 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open Errors -open Util -open Evd -open Tacexpr -open Proof_type -open Printer - -let pr_tactic = function - | TacArg (_,Tacexp t) -> - (*top tactic from tacinterp*) - Pptactic.pr_glob_tactic (Global.env()) t - | t -> - Pptactic.pr_tactic (Global.env()) t - -let pr_rule = function - | Prim r -> hov 0 (pr_prim_rule r) - | Daimon -> str "<Daimon>" - | Decl_proof _ -> str "proof" - -(* Does not print change of evars *) -let pr_rule_dot = function - | Prim Change_evars ->str "PC: ch_evars" ++ mt () - (* PC: this might be redundant *) - | r -> pr_rule r ++ str"." - -let pr_rule_dot_fnl = function - | Prim Change_evars -> mt () - | r -> pr_rule_dot r ++ fnl () - -let rec print_proof sigma osign pf = - (* spiwack: [osign] is currently ignored, not sure if this function is even used. *) - let hyps = Environ.named_context_of_val (Goal.V82.hyps sigma pf.goal) in - match pf.ref with - | None -> - hov 0 (pr_goal {sigma = sigma; it=pf.goal }) - | Some(r,spfl) -> - hov 0 - (hov 0 (pr_goal {sigma = sigma; it=pf.goal }) ++ - spc () ++ str" BY " ++ - hov 0 (pr_rule r) ++ fnl () ++ - str" " ++ - hov 0 (prlist_with_sep fnl (print_proof sigma hyps) spfl)) - -let pr_change sigma gl = - str"change " ++ - pr_lconstr_env (Goal.V82.env sigma gl) (Goal.V82.concl sigma gl) ++ str"." - -let print_decl_script tac_printer ?(nochange=true) sigma pf = - let rec print_prf pf = - match pf.ref with - | None -> - (if nochange then - (str"<Your Proof Text here>") - else - pr_change sigma pf.goal) - ++ fnl () - | Some (Daimon,[]) -> str "(* Some proof has been skipped here *)" - | Some (Prim Change_evars,[subpf]) -> print_prf subpf - | _ -> anomaly "Not Applicable" in - print_prf pf - -let print_script ?(nochange=true) sigma pf = - let rec print_prf pf = - match pf.ref with - | None -> - (if nochange then - (str"<Your Tactic Text here>") - else - pr_change sigma pf.goal) - ++ fnl () - | Some(Decl_proof opened,script) -> - assert (List.length script = 1); - begin - if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ()) - end ++ - begin - hov 0 (str "proof." ++ fnl () ++ - print_decl_script print_prf - ~nochange sigma (List.hd script)) - end ++ fnl () ++ - begin - if opened then mt () else (str "end proof." ++ fnl ()) - end - | Some(Daimon,spfl) -> - ((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++ - prlist_with_sep fnl print_prf spfl ) - | Some(rule,spfl) -> - ((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++ - pr_rule_dot_fnl rule ++ - prlist_with_sep fnl print_prf spfl ) in - print_prf pf - -(* printed by Show Script command *) - -let print_treescript ?(nochange=true) sigma pf = - let rec print_prf pf = - match pf.ref with - | None -> - if nochange then - str"<Your Proof Text here>" - else pr_change sigma pf.goal - | Some(Decl_proof opened,script) -> - assert (List.length script = 1); - begin - if nochange then mt () else pr_change sigma pf.goal ++ fnl () - end ++ - hov 0 - begin str "proof." ++ fnl () ++ - print_decl_script print_prf ~nochange sigma (List.hd script) - end ++ fnl () ++ - begin - if opened then mt () else (str "end proof." ++ fnl ()) - end - | Some(Daimon,spfl) -> - (if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++ - prlist_with_sep fnl (print_script ~nochange sigma) spfl - | Some(r,spfl) -> - let indent = if List.length spfl >= 2 then 1 else 0 in - (if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++ - hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl print_prf spfl) - in hov 0 (print_prf pf) - -let rec print_info_script sigma osign pf = - let sign = Goal.V82.hyps sigma pf.goal in - match pf.ref with - | None -> (mt ()) - | Some(r,spfl) -> - (pr_rule r ++ - match spfl with - | [pf1] -> - if pf1.ref = None then - (str "." ++ fnl ()) - else - (str";" ++ brk(1,3) ++ - print_info_script sigma - (Environ.named_context_of_val sign) pf1) - | _ -> (str"." ++ fnl () ++ - prlist_with_sep fnl - (print_info_script sigma - (Environ.named_context_of_val sign)) spfl)) - -let format_print_info_script sigma osign pf = - hov 0 (print_info_script sigma osign pf) diff --git a/printing/tactic_printer.mli b/printing/tactic_printer.mli deleted file mode 100644 index e94a2a771..000000000 --- a/printing/tactic_printer.mli +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Sign -open Evd -open Proof_type - -(** These are the entry points for tactics, proof trees, ... *) - -val print_proof : evar_map -> named_context -> proof_tree -> Pp.std_ppcmds -val pr_rule : rule -> Pp.std_ppcmds -val pr_tactic : tactic_expr -> Pp.std_ppcmds -val print_script : - ?nochange:bool -> evar_map -> proof_tree -> Pp.std_ppcmds -val print_treescript : - ?nochange:bool -> evar_map -> proof_tree -> Pp.std_ppcmds diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 4652bac2e..d806d80b8 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -40,14 +40,7 @@ type prim_rule = | Rename of identifier * identifier | Change_evars -type proof_tree = { - goal : goal; - ref : (rule * proof_tree list) option } - -and rule = - | Prim of prim_rule - | Decl_proof of bool - | Daimon +type rule = Prim of prim_rule type compound_rule= | Tactic of tactic_expr * bool diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index d6081e56c..832377e31 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -66,21 +66,7 @@ type prim_rule = in the type of evar] \} \} \} v} *) -(** {6 ... } *) -(** Proof trees. - [ref] = [None] if the goal has still to be proved, - and [Some (r,l)] if the rule [r] was applied to the goal - and gave [l] as subproofs to be completed. - if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof - that the goal can be proven if the goals in [l] are solved. *) -type proof_tree = { - goal : goal; - ref : (rule * proof_tree list) option } - -and rule = - | Prim of prim_rule - | Decl_proof of bool - | Daimon +type rule = Prim of prim_rule type compound_rule= (** the boolean of Tactic tells if the default tactic is used *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 87ba77dc5..9b9b91337 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -35,16 +35,6 @@ let refiner = function {it=sgl; sigma = sigma'}) - | Decl_proof _ -> - failwith "Refiner: should not occur" - - (* Daimon is a canonical unfinished proof *) - - | Daimon -> - fun gls -> - {it=[];sigma=gls.sigma} - - let norm_evar_tac gl = refiner (Prim Change_evars) gl (*********************) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 4524fe6a1..80a450bcd 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -109,8 +109,6 @@ let pf_matches = pf_apply Matching.matches_conv (* Tactics handling a list of goals *) (************************************) -type validation_list = proof_tree list -> proof_tree list - type tactic_list = Refiner.tactic_list let first_goal = first_goal diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index e7ad5d000..da9aecde9 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -118,8 +118,6 @@ val rename_hyp : (identifier*identifier) list -> tactic (** {6 Tactics handling a list of goals. } *) -type validation_list = proof_tree list -> proof_tree list - type tactic_list = Refiner.tactic_list val first_goal : 'a list sigma -> 'a sigma |