summaryrefslogtreecommitdiff
path: root/plugins/xml/proofTree2Xml.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/xml/proofTree2Xml.ml4')
-rw-r--r--plugins/xml/proofTree2Xml.ml4205
1 files changed, 0 insertions, 205 deletions
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 *)
-(* <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 ->
- 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 "<?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;;
-*)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 16:15:57 +0000