diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/xml/proof2aproof.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/xml/proof2aproof.ml')
-rw-r--r-- | plugins/xml/proof2aproof.ml | 176 |
1 files changed, 176 insertions, 0 deletions
diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml new file mode 100644 index 00000000..1beabf26 --- /dev/null +++ b/plugins/xml/proof2aproof.ml @@ -0,0 +1,176 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +(* Note: we can not use the Set module here because we _need_ physical *) +(* equality and there exists no comparison function compatible with *) +(* physical equality. *) + +module S = + struct + let empty = [] + let mem = List.memq + let add x l = x::l + end +;; + +(* evar reduction that preserves some terms *) +let nf_evar sigma ~preserve = + let module T = Term in + let rec aux t = + if preserve t then t else + match T.kind_of_term t with + | T.Rel _ | T.Meta _ | T.Var _ | T.Sort _ | T.Const _ | T.Ind _ + | T.Construct _ -> t + | T.Cast (c1,k,c2) -> T.mkCast (aux c1, k, aux c2) + | T.Prod (na,c1,c2) -> T.mkProd (na, aux c1, aux c2) + | T.Lambda (na,t,c) -> T.mkLambda (na, aux t, aux c) + | T.LetIn (na,b,t,c) -> T.mkLetIn (na, aux b, aux t, aux c) + | T.App (c,l) -> + let c' = aux c in + let l' = Array.map aux l in + (match T.kind_of_term c' with + T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l') + | T.Cast (he,_,_) -> + (match T.kind_of_term he with + T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l') + | _ -> T.mkApp (c', l') + ) + | _ -> T.mkApp (c', l')) + | T.Evar (e,l) when Evd.mem sigma e & Evd.is_defined sigma e -> + aux (Evd.existential_value sigma (e,l)) + | T.Evar (e,l) -> T.mkEvar (e, Array.map aux l) + | T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl) + | T.Fix (ln,(lna,tl,bl)) -> + T.mkFix (ln,(lna,Array.map aux tl,Array.map aux bl)) + | T.CoFix(ln,(lna,tl,bl)) -> + T.mkCoFix (ln,(lna,Array.map aux tl,Array.map aux bl)) + in + aux +;; + +(* Unshares a proof-tree. *) +(* 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} -> + let unshared_ref = + match ref with + None -> None + | Some (rule,pfs) -> + let unshared_rule = + match rule with + 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} +;; + +module ProofTreeHash = + Hashtbl.Make + (struct + type t = Proof_type.proof_tree + let equal = (==) + let hash = Hashtbl.hash + end) +;; + + +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) +;; + +let extract_open_pftreestate pts = + extract_open_proof (Refiner.evc_of_pftreestate pts) + (Tacmach.proof_of_pftreestate pts) +;; |