From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- plugins/xml/proofTree2Xml.ml4 | 210 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 210 insertions(+) create mode 100644 plugins/xml/proofTree2Xml.ml4 (limited to 'plugins/xml/proofTree2Xml.ml4') diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 new file mode 100644 index 00000000..3f1e0a63 --- /dev/null +++ b/plugins/xml/proofTree2Xml.ml4 @@ -0,0 +1,210 @@ +(************************************************************************) +(* 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 = std_ppcmds_to_string (prtac tactic_expr) in + let tacname= first_word tac in + let of_attribute = ("name",tacname)::("script",tac)::of_attribute in + + (****** le but *) + let {Evd.evar_concl=concl; + Evd.evar_hyps=hyps}=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.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} -> + Util.anomaly "Not Implemented" + + | {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 + 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