summaryrefslogtreecommitdiff
path: root/contrib/xml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml')
-rw-r--r--contrib/xml/cic2acic.ml2
-rw-r--r--contrib/xml/doubleTypeInference.ml2
-rw-r--r--contrib/xml/proof2aproof.ml19
-rw-r--r--contrib/xml/proofTree2Xml.ml48
-rw-r--r--contrib/xml/xmlcommand.ml7
5 files changed, 23 insertions, 15 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index f217b037..ff07c3c4 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -241,7 +241,7 @@ let typeur sigma metamap =
Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
| T.Const c ->
let cb = Environ.lookup_constant c env in
- T.body_of_type cb.Declarations.const_type
+ 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 ->
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index a3336817..c7d3b4ff 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -122,7 +122,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
Typeops.judge_of_variable env id
| T.Const c ->
- E.make_judge cstr (E.constant_type env c)
+ E.make_judge cstr (Typeops.type_of_constant env c)
| T.Ind ind ->
E.make_judge cstr (Inductiveops.type_of_inductive env ind)
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index 678b650c..92cbf6df 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -63,21 +63,24 @@ let nf_evar sigma ~preserve =
(* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *)
let rec unshare_proof_tree =
let module PT = Proof_type in
- function {PT.open_subgoals = status ; PT.goal = goal ; PT.ref = ref} ->
+ function {PT.open_subgoals = status ;
+ PT.goal = goal ;
+ PT.ref = ref} ->
let unshared_ref =
match ref with
None -> None
| Some (rule,pfs) ->
let unshared_rule =
match rule with
- PT.Prim prim -> PT.Prim prim
- | PT.Change_evars -> PT.Change_evars
- | PT.Tactic (tactic_expr, pf) ->
- PT.Tactic (tactic_expr, unshare_proof_tree pf)
- in
+ 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}
+ {PT.open_subgoals = status ;
+ PT.goal = goal ;
+ PT.ref = unshared_ref}
;;
module ProofTreeHash =
@@ -103,7 +106,7 @@ let extract_open_proof sigma pf =
{PT.ref=Some(PT.Prim _,_)} as pf ->
L.prim_extractor proof_extractor vl pf
- | {PT.ref=Some(PT.Tactic (_,hidden_proof),spfl)} ->
+ | {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 ;
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 578c1ed2..dbdc79a8 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -141,7 +141,7 @@ Pp.ppnl (Pp.(++) (Pp.str
(fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
| {PT.goal=goal;
- PT.ref=Some(PT.Tactic (tactic_expr,hidden_proof),nodes)} ->
+ 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] *)
@@ -194,6 +194,12 @@ Pp.ppnl (Pp.(++) (Pp.str
(List.fold_left
(fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
+ | {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
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index b6b1c7b6..f286d2c8 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -408,7 +408,7 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite =
let {D.mind_consnames=consnames ;
D.mind_typename=typename } = p
in
- let arity = Inductive.type_of_inductive (mib,p) in
+ let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in
let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in
let cons =
(Array.fold_right (fun (name,lc) i -> (name,lc)::i)
@@ -522,6 +522,7 @@ let print internal glob_ref kind xml_library_root =
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 typ = Typeops.type_of_constant_type (Global.env()) typ in
Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
| Ln.IndRef (kn,_) ->
let mib = G.lookup_mind kn in
@@ -531,7 +532,7 @@ let print internal glob_ref kind xml_library_root =
D.mind_finite=finite} = mib in
Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite
| Ln.ConstructRef _ ->
- Util.anomaly ("print: this should not happen")
+ Util.error ("a single constructor cannot be printed in XML")
in
let fn = filename_of_path xml_library_root tag in
let uri = Cic2acic.uri_of_kernel_name tag in
@@ -547,14 +548,12 @@ 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 str = Names.string_of_id id in
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 kn = Lib.make_kn id in
let env = Global.env () in
let obj =
mk_current_proof_obj (fst kind = Decl_kinds.Local) id val0 typ evar_map env in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 05:55:14 +0000