1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
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)
;;
|
