diff options
Diffstat (limited to 'plugins/xml/proof2aproof.ml')
-rw-r--r-- | plugins/xml/proof2aproof.ml | 82 |
1 files changed, 4 insertions, 78 deletions
diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml index 1beabf26c..c7b8b556e 100644 --- a/plugins/xml/proof2aproof.ml +++ b/plugins/xml/proof2aproof.ml @@ -94,83 +94,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) *) + () |