diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /contrib/xml | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'contrib/xml')
-rw-r--r-- | contrib/xml/cic2acic.ml | 2 | ||||
-rw-r--r-- | contrib/xml/doubleTypeInference.ml | 2 | ||||
-rw-r--r-- | contrib/xml/proof2aproof.ml | 19 | ||||
-rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 8 | ||||
-rw-r--r-- | contrib/xml/xmlcommand.ml | 7 |
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 |