1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * The HELM Project / The EU MoWGLI Project *)
6
(* * University of Bologna *)
7
(************************************************************************)
8
(* This file is distributed under the terms of the *)
9
(* GNU Lesser General Public License Version 2.1 *)
11
(* Copyright (C) 2000-2004, HELM Team. *)
12
(* http://helm.cs.unibo.it *)
13
(************************************************************************)
15
(* Note: we can not use the Set module here because we _need_ physical *)
16
(* equality and there exists no comparison function compatible with *)
17
(* physical equality. *)
27
(* evar reduction that preserves some terms *)
28
let nf_evar sigma ~preserve =
29
let module T = Term in
31
if preserve t then t else
32
match T.kind_of_term t with
33
| T.Rel _ | T.Meta _ | T.Var _ | T.Sort _ | T.Const _ | T.Ind _
35
| T.Cast (c1,k,c2) -> T.mkCast (aux c1, k, aux c2)
36
| T.Prod (na,c1,c2) -> T.mkProd (na, aux c1, aux c2)
37
| T.Lambda (na,t,c) -> T.mkLambda (na, aux t, aux c)
38
| T.LetIn (na,b,t,c) -> T.mkLetIn (na, aux b, aux t, aux c)
41
let l' = Array.map aux l in
42
(match T.kind_of_term c' with
43
T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l')
45
(match T.kind_of_term he with
46
T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l')
47
| _ -> T.mkApp (c', l')
49
| _ -> T.mkApp (c', l'))
50
| T.Evar (e,l) when Evd.mem sigma e & Evd.is_defined sigma e ->
51
aux (Evd.existential_value sigma (e,l))
52
| T.Evar (e,l) -> T.mkEvar (e, Array.map aux l)
53
| T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl)
54
| T.Fix (ln,(lna,tl,bl)) ->
55
T.mkFix (ln,(lna,Array.map aux tl,Array.map aux bl))
56
| T.CoFix(ln,(lna,tl,bl)) ->
57
T.mkCoFix (ln,(lna,Array.map aux tl,Array.map aux bl))
62
(* Unshares a proof-tree. *)
63
(* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *)
64
let rec unshare_proof_tree =
65
let module PT = Proof_type in
66
function {PT.open_subgoals = status ;
75
PT.Nested (cmpd, pf) ->
76
PT.Nested (cmpd, unshare_proof_tree pf)
79
Some (unshared_rule, List.map unshare_proof_tree pfs)
81
{PT.open_subgoals = status ;
83
PT.ref = unshared_ref}
86
module ProofTreeHash =
89
type t = Proof_type.proof_tree
91
let hash = Hashtbl.hash
96
let extract_open_proof sigma pf =
97
let module PT = Proof_type in
98
let module L = Logic in
99
let evd = ref (Evd.create_evar_defs sigma) in
100
let proof_tree_to_constr = ProofTreeHash.create 503 in
101
let proof_tree_to_flattened_proof_tree = ProofTreeHash.create 503 in
102
let unshared_constrs = ref S.empty in
103
let rec proof_extractor vl node =
106
{PT.ref=Some(PT.Prim _,_)} as pf ->
107
L.prim_extractor proof_extractor vl pf
109
| {PT.ref=Some(PT.Nested (_,hidden_proof),spfl)} ->
110
let sgl,v = Refiner.frontier hidden_proof in
111
let flat_proof = v spfl in
112
ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ;
113
proof_extractor vl flat_proof
115
| {PT.ref=None;PT.goal=goal} ->
119
(* Section variables are in the [id] list but are not *)
120
(* lambda abstracted in the term [vl] *)
121
try let n = Logic.proof_variable_index id vl in (n,id)
122
with Not_found -> failwith "caught")
123
(*CSC: the above function must be modified such that when it is found *)
124
(*CSC: it becomes a Rel; otherwise a Var. Then it can be already used *)
125
(*CSC: as the evar_instance. Ordering the instance becomes useless (it *)
126
(*CSC: will already be ordered. *)
127
(Termops.ids_of_named_context
128
(Environ.named_context_of_val goal.Evd.evar_hyps)) in
130
Sort.list (fun (n1,_) (n2,_) -> n1 < n2 ) visible_rels in
134
(fun (_,id) -> Sign.lookup_named id
135
(Environ.named_context_of_val goal.Evd.evar_hyps))
137
Environ.val_of_named_context l
139
(*CSC: the section variables in the right order must be added too *)
140
let evar_instance = List.map (fun (n,_) -> Term.mkRel n) sorted_rels in
141
(* let env = Global.env_of_context context in *)
143
Evarutil.new_evar_instance context !evd goal.Evd.evar_concl
148
| _ -> Util.anomaly "Bug : a case has been forgotten in proof_extractor"
152
nf_evar (Evd.evars_of !evd)
153
~preserve:(function e -> S.mem e !unshared_constrs) constr
156
~already_unshared:(function e -> S.mem e !unshared_constrs)
159
(*CSC: debugging stuff to be removed *)
160
if ProofTreeHash.mem proof_tree_to_constr node then
161
Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ")
162
(Tactic_printer.print_proof (Evd.evars_of !evd) [] node)) ;
163
ProofTreeHash.add proof_tree_to_constr node unsharedconstr ;
164
unshared_constrs := S.add unsharedconstr !unshared_constrs ;
167
let unshared_pf = unshare_proof_tree pf in
168
let pfterm = proof_extractor [] unshared_pf in
169
(pfterm, Evd.evars_of !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree,
173
let extract_open_pftreestate pts =
174
extract_open_proof (Refiner.evc_of_pftreestate pts)
175
(Tacmach.proof_of_pftreestate pts)