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
|
(* 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,c2) -> T.mkCast (aux c1, 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.in_dom sigma e & Evd.is_defined sigma e ->
aux (Instantiate.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.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
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 sigma = ref 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.Tactic (_,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=Some(PT.Change_evars,[pf])} -> (proof_extractor vl) pf
| {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 = Util.list_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 goal.Evd.evar_hyps) in
let sorted_rels =
Sort.list (fun (n1,_) (n2,_) -> n1 < n2 ) visible_rels in
let context =
List.map
(fun (_,id) -> Sign.lookup_named id goal.Evd.evar_hyps)
sorted_rels
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 sigma',evar =
Evarutil.new_isevar_sign env !sigma goal.Evd.evar_concl evar_instance
in
sigma := sigma' ;
evar
| _ -> Util.anomaly "Bug : a case has been forgotten in proof_extractor"
in
let unsharedconstr =
let evar_nf_constr =
nf_evar !sigma ~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: ") (Refiner.print_proof !sigma [] 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, !sigma, 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)
;;
|
