From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- plugins/xml/acic.ml | 2 +- plugins/xml/acic2Xml.ml4 | 2 +- plugins/xml/cic2acic.ml | 2 +- plugins/xml/doubleTypeInference.ml | 4 +- plugins/xml/doubleTypeInference.mli | 2 +- plugins/xml/dumptree.ml4 | 32 +++-------- plugins/xml/proof2aproof.ml | 108 ++---------------------------------- plugins/xml/proofTree2Xml.ml4 | 21 +++---- plugins/xml/unshare.ml | 2 +- plugins/xml/unshare.mli | 2 +- plugins/xml/xml.ml4 | 2 +- plugins/xml/xml.mli | 4 +- plugins/xml/xmlcommand.ml | 46 +++------------ plugins/xml/xmlcommand.mli | 4 +- plugins/xml/xmlentries.ml4 | 4 +- 15 files changed, 42 insertions(+), 195 deletions(-) (limited to 'plugins/xml') diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml index 97287d18..653c2b7b 100644 --- a/plugins/xml/acic.ml +++ b/plugins/xml/acic.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* str "" + | TacArg (_,Tacexp t) -> str "" | t -> str "" ;; @@ -56,13 +56,11 @@ let pr_rule_xml pr = function hov 2 (str "" ++ fnl () ++ begin match cmpd with Tactic (texp, _) -> pr_tactic_xml texp - | Proof_instr (_,instr) -> pr_proof_instr_xml instr end ++ fnl () ++ pr subtree ) ++ fnl () ++ str "" | Daimon -> str "" | Decl_proof _ -> str "" -(* | Change_evars -> str ""*) ;; let pr_var_decl_xml env (id,c,typ) = @@ -115,11 +113,11 @@ let pr_subgoal_metas_xml metas env= List.fold_left (++) (mt ()) (List.map pr_one metas) ;; -let pr_goal_xml g = - let env = try evar_unfiltered_env g with _ -> empty_env in - if g.evar_extra = None then +let pr_goal_xml sigma g = + let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in + if Decl_mode.try_get_info sigma g = None then (hov 2 (str "" ++ fnl () ++ str "" ++ (pr_context_xml env)) ++ fnl () ++ str "") @@ -129,23 +127,9 @@ let pr_goal_xml g = fnl () ++ str "") ;; -let rec print_proof_xml sigma osign pf = - let hyps = Environ.named_context_of_val pf.goal.evar_hyps in - let hyps' = thin_sign osign hyps in - match pf.ref with - | None -> hov 2 (str "" ++ fnl () ++ (pr_goal_xml {pf.goal with evar_hyps=hyps'})) ++ fnl () ++ str "" - | Some(r,spfl) -> - hov 2 (str "" ++ fnl () ++ - (pr_goal_xml {pf.goal with evar_hyps=hyps'}) ++ fnl () ++ (pr_rule_xml (print_proof_xml sigma osign) r) ++ - (List.fold_left (fun x y -> x ++ fnl () ++ y) (mt ()) (List.map (print_proof_xml sigma hyps) spfl))) ++ fnl () ++ str "" -;; - let print_proof_xml () = - let pp = print_proof_xml Evd.empty Sign.empty_named_context - (Tacmach.proof_of_pftreestate (Refiner.top_of_tree (Pfedit.get_pftreestate ()))) - in - msgnl pp -;; + Util.anomaly "Dump Tree command not supported in this version." + VERNAC COMMAND EXTEND DumpTree [ "Dump" "Tree" ] -> [ print_proof_xml () ] diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml index d871935b..2d16190b 100644 --- a/plugins/xml/proof2aproof.ml +++ b/plugins/xml/proof2aproof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let unshared_ref = - match ref with - None -> None - | Some (rule,pfs) -> - let unshared_rule = - match rule with - PT.Nested (cmpd, pf) -> - PT.Nested (cmpd, unshare_proof_tree pf) - | other -> other - in - Some (unshared_rule, List.map unshare_proof_tree pfs) - in - {PT.open_subgoals = status ; - PT.goal = goal ; - PT.ref = unshared_ref} -;; - module ProofTreeHash = Hashtbl.Make (struct @@ -94,83 +70,9 @@ module ProofTreeHash = let extract_open_proof sigma pf = - let module PT = Proof_type in - let module L = Logic in - let evd = ref (Evd.create_evar_defs sigma) in - let proof_tree_to_constr = ProofTreeHash.create 503 in - let proof_tree_to_flattened_proof_tree = ProofTreeHash.create 503 in - let unshared_constrs = ref S.empty in - let rec proof_extractor vl node = - let constr = - match node with - {PT.ref=Some(PT.Prim _,_)} as pf -> - L.prim_extractor proof_extractor vl pf - - | {PT.ref=Some(PT.Nested (_,hidden_proof),spfl)} -> - let sgl,v = Refiner.frontier hidden_proof in - let flat_proof = v spfl in - ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ; - proof_extractor vl flat_proof - - | {PT.ref=None;PT.goal=goal} -> - let visible_rels = - Util.map_succeed - (fun id -> - (* Section variables are in the [id] list but are not *) - (* lambda abstracted in the term [vl] *) - try let n = Logic.proof_variable_index id vl in (n,id) - with Not_found -> failwith "caught") -(*CSC: the above function must be modified such that when it is found *) -(*CSC: it becomes a Rel; otherwise a Var. Then it can be already used *) -(*CSC: as the evar_instance. Ordering the instance becomes useless (it *) -(*CSC: will already be ordered. *) - (Termops.ids_of_named_context - (Environ.named_context_of_val goal.Evd.evar_hyps)) in - let sorted_rels = - Sort.list (fun (n1,_) (n2,_) -> n1 < n2 ) visible_rels in - let context = - let l = - List.map - (fun (_,id) -> Sign.lookup_named id - (Environ.named_context_of_val goal.Evd.evar_hyps)) - sorted_rels in - Environ.val_of_named_context l - in -(*CSC: the section variables in the right order must be added too *) - let evar_instance = List.map (fun (n,_) -> Term.mkRel n) sorted_rels in - (* let env = Global.env_of_context context in *) - let evd',evar = - Evarutil.new_evar_instance context !evd goal.Evd.evar_concl - evar_instance in - evd := evd' ; - evar - - | _ -> Util.anomaly "Bug : a case has been forgotten in proof_extractor" - in - let unsharedconstr = - let evar_nf_constr = - nf_evar ( !evd) - ~preserve:(function e -> S.mem e !unshared_constrs) constr - in - Unshare.unshare - ~already_unshared:(function e -> S.mem e !unshared_constrs) - evar_nf_constr - in -(*CSC: debugging stuff to be removed *) -if ProofTreeHash.mem proof_tree_to_constr node then - Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") - (Tactic_printer.print_proof ( !evd) [] node)) ; - ProofTreeHash.add proof_tree_to_constr node unsharedconstr ; - unshared_constrs := S.add unsharedconstr !unshared_constrs ; - unsharedconstr - in - let unshared_pf = unshare_proof_tree pf in - let pfterm = proof_extractor [] unshared_pf in - (pfterm, !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree, - unshared_pf) -;; + (* Deactivated and candidate for removal. (Apr. 2010) *) + () let extract_open_pftreestate pts = - extract_open_proof (Refiner.evc_of_pftreestate pts) - (Tacmach.proof_of_pftreestate pts) -;; + (* Deactivated and candidate for removal. (Apr. 2010) *) + () diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 index 21c86c79..2f5eb6ac 100644 --- a/plugins/xml/proofTree2Xml.ml4 +++ b/plugins/xml/proofTree2Xml.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + | 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 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 {Evd.evar_concl=concl; - Evd.evar_hyps=hyps}=goal in + + 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 @@ -188,14 +185,12 @@ Pp.ppnl (Pp.(++) (Pp.str [<(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 + | {PT.ref=Some(PT.Decl_proof _, _)} -> failwith "TODO: xml and decl_proof" in [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n"); diff --git a/plugins/xml/unshare.ml b/plugins/xml/unshare.ml index 344a1581..c854427d 100644 --- a/plugins/xml/unshare.ml +++ b/plugins/xml/unshare.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* let id = N.id_of_label (N.con_label kn) in - let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = - G.lookup_constant kn in + let cb = G.lookup_constant kn in + let val0 = D.body_of_constant cb in + let typ = cb.D.const_type in + let hyps = cb.D.const_hyps in let typ = Typeops.type_of_constant_type (Global.env()) typ in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Ln.IndRef (kn,_) -> @@ -557,43 +559,13 @@ let print_ref qid fn = (* where dest is either None (for stdout) or (Some filename) *) (* pretty prints via Xml.pp the proof in progress on dest *) let show_pftreestate internal fn (kind,pftst) id = - let pf = Tacmach.proof_of_pftreestate pftst in - let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in - let val0,evar_map,proof_tree_to_constr,proof_tree_to_flattened_proof_tree, - unshared_pf - = - Proof2aproof.extract_open_pftreestate pftst in - let env = Global.env () in - let obj = - mk_current_proof_obj (fst kind = Decl_kinds.Local) id val0 typ evar_map env in - let uri = - match kind with - Decl_kinds.Local, _ -> - let uri = - "cic:/" ^ String.concat "/" - (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.TVariable) - in - let kind_of_var = "VARIABLE","LocalFact" in - (match internal with - | Declare.KernelSilent -> () - | _ -> print_object_kind uri kind_of_var - ); uri - | Decl_kinds.Global, _ -> - let uri = Cic2acic.uri_of_declaration id Cic2acic.TConstant in - (match internal with - | Declare.KernelSilent -> () - | _ -> print_object_kind uri (kind_of_global_goal kind) - ); uri - in - print_object uri obj evar_map - (Some (Tacmach.evc_of_pftreestate pftst,unshared_pf,proof_tree_to_constr, - proof_tree_to_flattened_proof_tree)) fn -;; + if true then + Util.anomaly "Xmlcommand.show_pftreestate is not supported in this version." let show fn = let pftst = Pfedit.get_pftreestate () in let (id,kind,_,_) = Pfedit.current_proof_statement () in - show_pftreestate Declare.KernelVerbose fn (kind,pftst) id + show_pftreestate false fn (kind,pftst) id ;; @@ -680,7 +652,7 @@ let _ = end ; Option.iter (fun fn -> - let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in + let coqdoc = Filename.concat Envars.coqbin ("coqdoc" ^ Coq_config.exec_extension) in let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let command cmd = if Sys.command cmd <> 0 then diff --git a/plugins/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli index eadf3cfd..ec50d623 100644 --- a/plugins/xml/xmlcommand.mli +++ b/plugins/xml/xmlcommand.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*