diff options
Diffstat (limited to 'contrib/xml')
-rw-r--r-- | contrib/xml/cic2acic.ml | 28 | ||||
-rw-r--r-- | contrib/xml/doubleTypeInference.ml | 2 | ||||
-rw-r--r-- | contrib/xml/dumptree.ml4 | 152 | ||||
-rw-r--r-- | contrib/xml/xmlcommand.ml | 41 |
4 files changed, 181 insertions, 42 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 8a5967a2..1a6cb9c8 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -55,18 +55,8 @@ let remove_module_dirpath_from_dirpath ~basedir dir = let get_uri_of_var v pvars = - let module D = Declare in + let module D = Decls in let module N = Names in - let rec search_in_pvars names = - function - [] -> None - | ((name,l)::tl) -> - let names' = name::names in - if List.mem v l then - Some names' - else - search_in_pvars names' tl - in let rec search_in_open_sections = function [] -> Util.error ("Variable "^v^" not found") @@ -78,9 +68,10 @@ let get_uri_of_var v pvars = search_in_open_sections tl in let path = - match search_in_pvars [] pvars with - None -> search_in_open_sections (N.repr_dirpath (Lib.cwd ())) - | Some path -> path + if List.mem v pvars then + [] + else + search_in_open_sections (N.repr_dirpath (Lib.cwd ())) in "cic:" ^ List.fold_left @@ -241,16 +232,15 @@ let typeur sigma metamap = | T.Var id -> (try let (_,_,ty) = Environ.lookup_named id env in - T.body_of_type ty + ty with Not_found -> Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound")) | T.Const c -> let cb = Environ.lookup_constant c env in Typeops.type_of_constant_type env (cb.Declarations.const_type) | T.Evar ev -> Evd.existential_type sigma ev - | T.Ind ind -> T.body_of_type (Inductiveops.type_of_inductive env ind) - | T.Construct cstr -> - T.body_of_type (Inductiveops.type_of_constructor env cstr) + | T.Ind ind -> Inductiveops.type_of_inductive env ind + | T.Construct cstr -> Inductiveops.type_of_constructor env cstr | T.Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) @@ -273,7 +263,7 @@ let typeur sigma metamap = match sort_of env cstr with Coq_sort T.InProp -> T.mkProp | Coq_sort T.InSet -> T.mkSet - | Coq_sort T.InType -> T.mkType Univ.prop_univ (* ERROR HERE *) + | Coq_sort T.InType -> T.mkType Univ.type1_univ (* ERROR HERE *) | CProp -> T.mkConst DoubleTypeInference.cprop and sort_of env t = diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index cce78891..de8c540c 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -51,7 +51,7 @@ let type_judgment env sigma j = ;; let type_judgment_cprop env sigma j = - match Term.kind_of_term(whd_betadeltaiotacprop env sigma (Term.body_of_type j.Environ.uj_type)) with + match Term.kind_of_term(whd_betadeltaiotacprop env sigma j.Environ.uj_type) with | Term.Sort s -> Some {Environ.utj_val = j.Environ.uj_val; Environ.utj_type = s } | _ -> None (* None means the CProp constant *) ;; diff --git a/contrib/xml/dumptree.ml4 b/contrib/xml/dumptree.ml4 new file mode 100644 index 00000000..407f86b3 --- /dev/null +++ b/contrib/xml/dumptree.ml4 @@ -0,0 +1,152 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module provides the "Dump Tree" command that allows dumping the + current state of the proof stree in XML format *) + +(** Contributed by Cezary Kaliszyk, Radboud University Nijmegen *) + +(*i camlp4deps: "parsing/grammar.cma" i*) +open Tacexpr;; +open Decl_mode;; +open Printer;; +open Pp;; +open Environ;; +open Format;; +open Proof_type;; +open Evd;; +open Termops;; +open Ppconstr;; +open Names;; + +exception Different + +let xmlstream s = + (* In XML we want to print the whole stream so we can force the evaluation *) + Stream.of_list (List.map xmlescape (Stream.npeek max_int s)) +;; + +let thin_sign osign sign = + Sign.fold_named_context + (fun (id,c,ty as d) sign -> + try + if Sign.lookup_named id osign = (id,c,ty) then sign + else raise Different + with Not_found | Different -> Environ.push_named_context_val d sign) + sign ~init:Environ.empty_named_context_val +;; + +let pr_tactic_xml = function + | TacArg (Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>" + | t -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_tactic (Global.env()) t) ++ str "\"/>" +;; + +let pr_proof_instr_xml instr = + Ppdecl_proof.pr_proof_instr (Global.env()) instr +;; + +let pr_rule_xml pr = function + | Prim r -> str "<rule text=\"" ++ xmlstream (pr_prim_rule r) ++ str "\"/>" + | Nested(cmpd, subtree) -> + hov 2 (str "<cmpdrule>" ++ 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 "</cmpdrule>" + | Daimon -> str "<daimon/>" + | Decl_proof _ -> str "<proof/>" +(* | Change_evars -> str "<chgevars/>"*) +;; + +let pr_var_decl_xml env (id,c,typ) = + let ptyp = print_constr_env env typ in + match c with + | None -> + (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\"/>") + | Some c -> + (* Force evaluation *) + let pb = print_constr_env env c in + (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\" body=\"" ++ + xmlstream pb ++ str "\"/>") +;; + +let pr_rel_decl_xml env (na,c,typ) = + let pbody = match c with + | None -> mt () + | Some c -> + (* Force evaluation *) + let pb = print_constr_env env c in + (str" body=\"" ++ xmlstream pb ++ str "\"") in + let ptyp = print_constr_env env typ in + let pid = + match na with + | Anonymous -> mt () + | Name id -> str " id=\"" ++ pr_id id ++ str "\"" + in + (str "<hyp" ++ pid ++ str " type=\"" ++ xmlstream ptyp ++ str "\"" ++ pbody ++ str "/>") +;; + +let pr_context_xml env = + let sign_env = + fold_named_context + (fun env d pp -> pp ++ pr_var_decl_xml env d) + env ~init:(mt ()) + in + let db_env = + fold_rel_context + (fun env d pp -> pp ++ pr_rel_decl_xml env d) + env ~init:(mt ()) + in + (sign_env ++ db_env) +;; + +let pr_subgoal_metas_xml metas env= + let pr_one (meta, typ) = + fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_ltype_env_at_top env typ) ++ + str "\"/>" + in + List.fold_left (++) (mt ()) (List.map pr_one metas) +;; + +let pr_goal_xml g = + let env = try evar_env g with _ -> empty_env in + if g.evar_extra = None then + (hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++ + xmlstream (pr_ltype_env_at_top env g.evar_concl) ++ + str "\"/>" ++ + (pr_context_xml env)) ++ + fnl () ++ str "</goal>") + else + (hov 2 (str "<goal type=\"declarative\">" ++ + (pr_context_xml env)) ++ + fnl () ++ str "</goal>") +;; + +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 "<tree>" ++ fnl () ++ (pr_goal_xml {pf.goal with evar_hyps=hyps'})) ++ fnl () ++ str "</tree>" + | Some(r,spfl) -> + hov 2 (str "<tree>" ++ 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 "</tree>" +;; + +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 +;; + +VERNAC COMMAND EXTEND DumpTree + [ "Dump" "Tree" ] -> [ print_proof_xml () ] +END diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 01271323..3c4b01f5 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -73,11 +73,7 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *) let tag = Libobject.object_tag o in print_if_verbose ("Object tag: " ^ tag ^ "\n") ; match tag with - "CONSTANT" -> - (match D.constant_strength sp with - | DK.Local -> false (* a local definition *) - | DK.Global -> true (* a non-local one *) - ) + "CONSTANT" -> true (* constants/parameters are non global *) | "INDUCTIVE" -> true (* mutual inductive types are never local *) | "VARIABLE" -> false (* variables are local, so no namesakes *) | _ -> false (* uninteresting thing that won't be printed*) @@ -89,8 +85,7 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *) (* OF VARIABLES DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT *) (* SECTION, WHOSE PATH IS namei *) -let pvars = - ref ([Names.id_of_string "",[]] : (Names.identifier * string list) list);; +let pvars = ref ([] : string list);; let cumenv = ref Environ.empty_env;; (* filter_params pvars hyps *) @@ -138,9 +133,7 @@ let add_to_pvars x = E.push_named (Names.id_of_string v, None, typ) !cumenv ; v in - match !pvars with - [] -> assert false - | ((name,l)::tl) -> pvars := (name,v::l)::tl + pvars := v::!pvars ;; (* The computation is very inefficient, but we can't do anything *) @@ -157,7 +150,7 @@ let search_variables () = | he::tl as modules -> let one_section_variables = let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in - let t = List.map N.string_of_id (Declare.last_section_hyps dirpath) in + let t = List.map N.string_of_id (Decls.last_section_hyps dirpath) in [he,t] in one_section_variables @ aux tl @@ -329,14 +322,13 @@ let mk_variable_obj id body typ = let variables = search_variables () in let params = filter_params variables hyps'' in Acic.Variable - (Names.string_of_id id, unsharedbody, - (Unshare.unshare (Term.body_of_type typ)), params) + (Names.string_of_id id, unsharedbody, Unshare.unshare typ, params) ;; (* Unsharing is not performed on the body, that must be already unshared. *) (* The evar map and the type, instead, are unshared by this function. *) let mk_current_proof_obj is_a_variable id bo ty evar_map env = - let unshared_ty = Unshare.unshare (Term.body_of_type ty) in + let unshared_ty = Unshare.unshare ty in let metasenv = List.map (function @@ -384,7 +376,7 @@ let mk_current_proof_obj is_a_variable id bo ty evar_map env = let mk_constant_obj id bo ty variables hyps = let hyps = string_list_of_named_context_list hyps in - let ty = Unshare.unshare (Term.body_of_type ty) in + let ty = Unshare.unshare ty in let params = filter_params variables hyps in match bo with None -> @@ -413,7 +405,7 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite = let cons = (Array.fold_right (fun (name,lc) i -> (name,lc)::i) (Array.mapi - (fun j x ->(x,Unshare.unshare (Term.body_of_type lc.(j)))) consnames) + (fun j x ->(x,Unshare.unshare lc.(j))) consnames) [] ) in @@ -447,7 +439,7 @@ let kind_of_inductive isrecord kn = let kind_of_variable id = let module DK = Decl_kinds in - match Declare.variable_kind id with + match Decls.variable_kind id with | DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption" | DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis" | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture" @@ -458,7 +450,7 @@ let kind_of_variable id = let kind_of_constant kn = let module DK = Decl_kinds in - match Declare.constant_kind (Nametab.sp_of_global(Libnames.ConstRef kn)) with + match Decls.constant_kind kn with | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration" | DK.IsAssumption DK.Logical -> "AXIOM","Axiom" | DK.IsAssumption DK.Conjectural -> @@ -492,6 +484,12 @@ let kind_of_constant kn = | DK.IsDefinition DK.IdentityCoercion -> Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" + | DK.IsDefinition DK.Instance -> + Pp.warning "Instance not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Method -> + Pp.warning "Method not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> "THEOREM",DK.string_of_theorem_kind thm | DK.IsProof _ -> @@ -541,11 +539,10 @@ let print internal glob_ref kind xml_library_root = let tag,obj = match glob_ref with Ln.VarRef id -> - let sp = Declare.find_section_variable id in (* this kn is fake since it is not provided by Coq *) let kn = let (mod_path,dir_path) = Lib.current_prefix () in - N.make_kn mod_path dir_path (N.label_of_id (Ln.basename sp)) + N.make_kn mod_path dir_path (N.label_of_id id) in let (_,body,typ) = G.lookup_named id in Cic2acic.Variable kn,mk_variable_obj id body typ @@ -692,11 +689,11 @@ let _ = Buffer.output_buffer ch theory_buffer ; close_out ch end ; - Util.option_iter + Option.iter (fun fn -> let coqdoc = Coq_config.bindir^"/coqdoc" in let options = " --html -s --body-only --no-index --latin1 --raw-comments" in - let dir = Util.out_some xml_library_root in + let dir = Option.get xml_library_root in let command cmd = if Sys.command cmd <> 0 then Util.anomaly ("Error executing \"" ^ cmd ^ "\"") |