From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- plugins/xml/proofTree2Xml.ml4 | 205 ------------------------------------------ 1 file changed, 205 deletions(-) delete mode 100644 plugins/xml/proofTree2Xml.ml4 (limited to 'plugins/xml/proofTree2Xml.ml4') diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 deleted file mode 100644 index 2f5eb6ac..00000000 --- a/plugins/xml/proofTree2Xml.ml4 +++ /dev/null @@ -1,205 +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 -> - Util.anomaly - ("Problem during the conversion of constr into XML: " ^ - Printexc.to_string e) -(* CSC: debugging stuff -Pp.ppnl (Pp.str "Problem during the conversion of constr into XML") ; -Pp.ppnl (Pp.str "ENVIRONMENT:") ; -Pp.ppnl (Printer.pr_context_of rel_env) ; -Pp.ppnl (Pp.str "TERM:") ; -Pp.ppnl (Printer.pr_lconstr_env rel_env obj') ; -Pp.ppnl (Pp.str "RAW-TERM:") ; -Pp.ppnl (Printer.pr_lconstr obj') ; -Xml.xml_empty "MISSING TERM" [] (*; raise 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 module T = Tacexpr in - let ids_of_node node = - let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in -(* -let constr = - try - Proof2aproof.ProofTreeHash.find proof_tree_to_constr node - with _ -> Pp.ppnl (Pp.(++) (Pp.str "Node of the proof-tree that generated -no lambda-term: ") (Refiner.print_script true (Evd.empty) -(Global.named_context ()) node)) ; assert false (* Closed bug, should not -happen any more *) -in -*) - try - Some (Acic.CicHash.find constr_to_ids constr) - with _ -> -Pp.ppnl (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.goal=goal; - PT.ref=Some(PT.Nested (PT.Tactic(tactic_expr,_),hidden_proof),nodes)} -> - (* [hidden_proof] is the proof of the tactic; *) - (* [nodes] are the proof of the subgoals generated by the tactic; *) - (* [flat_proof] if the proof-tree obtained substituting [nodes] *) - (* for the holes in [hidden_proof] *) - let flat_proof = - Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node - in begin - match tactic_expr with - | T.TacArg (_,T.Tacexp _) -> - (* We don't need to keep the level of abstraction introduced at *) - (* user-level invocation of tactic... (see Tacinterp.hide_interp)*) - aux flat_proof old_hyps - | _ -> - (****** la tactique employee *) - let prtac = Pptactic.pr_tactic (Global.env()) in - let tac = Pp.string_of_ppcmds (prtac tactic_expr) in - let tacname= first_word tac in - let of_attribute = ("name",tacname)::("script",tac)::of_attribute in - - (****** le but *) - - let concl = Goal.V82.concl sigma goal in - let hyps = Goal.V82.hyps sigma goal in - - let env = Global.env_of_context hyps in - - - let xgoal = - X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in - - let rec build_hyps = - function - | [] -> xgoal - | (id,c,tid)::hyps1 -> - let id' = Names.string_of_id id in - [< build_hyps hyps1; - (X.xml_nempty "Hypothesis" - ["id",idref_of_id id' ; "name",id'] - (constr_to_xml tid sigma env)) - >] in - let old_names = List.map (fun (id,c,tid)->id) old_hyps in - let nhyps = Environ.named_context_of_val hyps in - let new_hyps = - List.filter (fun (id,c,tid)-> not (List.mem id old_names)) nhyps in - - X.xml_nempty "Tactic" of_attribute - [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>] - end - - | {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;; -*) -- cgit v1.2.3