summaryrefslogtreecommitdiff
path: root/contrib/xml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml')
-rw-r--r--contrib/xml/cic2acic.ml28
-rw-r--r--contrib/xml/doubleTypeInference.ml2
-rw-r--r--contrib/xml/dumptree.ml4152
-rw-r--r--contrib/xml/xmlcommand.ml41
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 ^ "\"")
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 07:13:16 +0000