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
let equal_option = Option.equal
module Reified_goal = struct
type 'a hyp =
{ names : String.t List.t
; def : 'a option
; ty : 'a
}
[@@deriving equal]
let map_hyp ~f { names; def; ty } =
let def = Option.map f def in
let ty = f ty in
{ names; def; ty }
type info =
{ evar : Evar.t
; name : Names.Id.t option
}
[@@deriving equal]
type 'a t =
{ info : info
; hyps : 'a hyp List.t
; ty : 'a
}
[@@deriving equal]
let map ~f { info; ty; hyps } =
let ty = f ty in
let hyps = List.map (map_hyp ~f) hyps in
{ info; ty; hyps }
end
type ('a, 'pp) t =
{ goals : 'a List.t
; stack : ('a List.t * 'a List.t) List.t
; bullet : 'pp option
; shelf : 'a List.t
; given_up : 'a List.t
}
[@@deriving equal]
let map ~f ~g { goals; stack; bullet; shelf; given_up } =
let goals = List.map f goals in
let stack = List.map (fun (s, r) -> (List.map f s, List.map f r)) stack in
let bullet = Option.map g bullet in
let shelf = List.map f shelf in
let given_up = List.map f given_up in
{ goals; stack; bullet; shelf; given_up }
type ('goals, 'pp) reified = ('goals Reified_goal.t, 'pp) t
(** XXX: Do we need to perform evar normalization? *)
module CDC = Context.Compacted.Declaration
type cdcl = EConstr.compacted_declaration
let binder_name n = Context.binder_name n |> Names.Id.to_string
let to_tuple ppx : cdcl -> 'pc Reified_goal.hyp =
let open CDC in
function
| LocalAssum (idl, tm) ->
let names = List.map binder_name idl in
{ Reified_goal.names; def = None; ty = ppx tm }
| LocalDef (idl, tdef, tm) ->
let names = List.map binder_name idl in
{ names; def = Some (ppx tdef); ty = ppx tm }
(** gets a hypothesis *)
let get_hyp (ppx : EConstr.t -> 'pc) (_sigma : Evd.evar_map) (hdecl : cdcl) :
'pc Reified_goal.hyp =
to_tuple ppx hdecl
(** gets the constr associated to the type of the current goal *)
let get_goal_type (ppx : EConstr.t -> 'pc) (env : Environ.env)
(sigma : Evd.evar_map) (g : Evar.t) : _ =
let (EvarInfo evi) = Evd.find sigma g in
let concl =
match Evd.evar_body evi with
| Evd.Evar_empty -> Evd.evar_concl evi
| Evd.Evar_defined body -> Retyping.get_type_of env sigma body
in
ppx concl
let build_info sigma g =
{ Reified_goal.evar = g; name = Evd.evar_ident g sigma }
(** Generic processor *)
let process_goal_gen ~ppx ~compact sigma g : 'a Reified_goal.t =
let env = Global.env () in
let (EvarInfo evi) = Evd.find sigma g in
let env = Evd.evar_filtered_env env evi in
let ctx =
if compact then
Termops.compact_named_context sigma (EConstr.named_context env)
else List.map CDC.of_named_decl (EConstr.named_context env)
in
let ppx = ppx env sigma in
let hyps = List.map (get_hyp ppx sigma) ctx |> List.rev in
let info = build_info sigma g in
{ info; ty = get_goal_type ppx env sigma g; hyps }
let if_not_empty (pp : Pp.t) =
if Pp.(repr pp = Ppcmd_empty) then None else Some pp
let reify ~ppx ~compact lemmas =
let lemmas = State.Proof.to_coq lemmas in
let proof =
Vernacstate.LemmaStack.with_top lemmas ~f:(fun pstate ->
Declare.Proof.get pstate)
in
let { Proof.goals; stack; sigma; _ } = Proof.data proof in
let ppx = List.map (process_goal_gen ~ppx ~compact sigma) in
{ goals = ppx goals
; stack = List.map (fun (g1, g2) -> (ppx g1, ppx g2)) stack
; bullet = if_not_empty @@ Proof_bullet.suggest proof
; shelf = Evd.shelf sigma |> ppx
; given_up = Evd.given_up sigma |> Evar.Set.elements |> ppx
}
module Equality = struct
let eq_constr (_env1, evd1, c1) (_env2, evd2, c2) =
let c1 = EConstr.to_constr evd1 c1 in
let c2 = EConstr.to_constr evd2 c2 in
Constr.equal c1 c2
let eq_pp pp1 pp2 = pp1 = pp2
let eq_rgoal = Reified_goal.equal eq_constr
let equal_goals st1 st2 =
let ppx env evd c = (env, evd, c) in
let compact = false in
let g1 = reify ~ppx ~compact st1 in
let g2 = reify ~ppx ~compact st2 in
equal eq_rgoal eq_pp g1 g2
end