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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
|
open Closure
open RedFlags
open Declarations
open Entries
open Dyn
open Libobject
open Pattern
open Matching
open Pp
open Rawterm
open Sign
open Tacred
open Util
open Names
open Nameops
open Libnames
open Nametab
open Pfedit
open Proof_type
open Refiner
open Tacmach
open Tactic_debug
open Topconstr
open Term
open Termops
open Tacexpr
open Safe_typing
open Typing
open Hiddentac
open Genarg
open Decl_kinds
open Mod_subst
open Printer
open Inductiveops
open Syntax_def
open Tacinterp
open Vernacexpr
open Notation
module SPretyping = Subtac_pretyping.Pretyping
open Subtac_utils
open Pretyping
(*********************************************************************)
(* Functions to parse and interpret constructions *)
let interp_gen kind isevars env
?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
c =
let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
let c'' = Subtac_interp_fixpoint.rewrite_cases c' in
Evd.evars_of !isevars, SPretyping.pretype_gen isevars env ([],[]) kind c''
let interp_constr isevars env c =
interp_gen (OfType None) isevars env c
let interp_type isevars env ?(impls=([],[])) c =
interp_gen IsType isevars env ~impls c
let interp_casted_constr isevars env ?(impls=([],[])) c typ =
interp_gen (OfType (Some typ)) isevars env ~impls c
let interp_open_constr isevars env c =
SPretyping.pretype_gen isevars env ([], []) (OfType None)
(Constrintern.intern_constr (Evd.evars_of !isevars) env c)
let interp_constr_judgment isevars env c =
let s, j = SPretyping.understand_judgment_tcc (Evd.evars_of !isevars) env
(Constrintern.intern_constr (Evd.evars_of !isevars) env c)
in
Evd.create_evar_defs s, j
(* try to find non recursive definitions *)
let list_chop_hd i l = match list_chop i l with
| (l1,x::l2) -> (l1,x,l2)
| _ -> assert false
let collect_non_rec env =
let rec searchrec lnonrec lnamerec ldefrec larrec nrec =
try
let i =
list_try_find_i
(fun i f ->
if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
then i else failwith "try_find_i")
0 lnamerec
in
let (lf1,f,lf2) = list_chop_hd i lnamerec in
let (ldef1,def,ldef2) = list_chop_hd i ldefrec in
let (lar1,ar,lar2) = list_chop_hd i larrec in
let newlnv =
try
match list_chop i nrec with
| (lnv1,_::lnv2) -> (lnv1@lnv2)
| _ -> [] (* nrec=[] for cofixpoints *)
with Failure "list_chop" -> []
in
searchrec ((f,def,ar)::lnonrec)
(lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
with Failure "try_find_i" ->
(List.rev lnonrec,
(Array.of_list lnamerec, Array.of_list ldefrec,
Array.of_list larrec, Array.of_list nrec))
in
searchrec []
let recursive_message v =
match Array.length v with
| 0 -> error "no recursive definition"
| 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
| _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
spc () ++ str "are recursively defined")
let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
let sigma = Evd.empty
and env0 = Global.env()
and protos = List.map (fun ((f, n, _, _, _),_) -> f,n) lnameargsardef
in
let lnameargsardef =
List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))
lnameargsardef
in
let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef
and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
in
(* Build the recursive context and notations for the recursive types *)
let (rec_sign,rec_impls,arityl) =
List.fold_left
(fun (env,impls,arl) ((recname,_,bl,arityc,_),_) ->
let arityc = Command.generalize_constr_expr arityc bl in
let isevars = ref (Evd.create_evar_defs sigma) in
let isevars, arity = interp_type isevars env0 arityc in
let impl =
if Impargs.is_implicit_args()
then Impargs.compute_implicits env0 arity
else [] in
let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
(Environ.push_named (recname,None,arity) env, impls', (isevars, arity)::arl))
(env0,[],[]) lnameargsardef in
let arityl = List.rev arityl in
let notations =
List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l)
lnameargsardef [] in
let recdef =
(* Declare local notations *)
let fs = States.freeze() in
let def =
try
List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
Metasyntax.add_notation_interpretation df rec_impls c None) notations;
List.map2
(fun ((_,_,bl,_,def),_) (evm, arity) ->
let def = abstract_constr_expr def bl in
interp_casted_constr (ref (Evd.create_evar_defs evm)) rec_sign ~impls:([],rec_impls)
def arity)
lnameargsardef arityl
with e ->
States.unfreeze fs; raise e in
States.unfreeze fs; def
in
let (lnonrec,(namerec,defrec,arrec,nvrec)) =
collect_non_rec env0 lrecnames recdef arityl nv in
let nvrec' = Array.map fst nvrec in(* ignore rec order *)
let declare arrec defrec =
let recvec =
Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
let rec declare i fi =
trace (str "Declaring: " ++ pr_id fi);
let ce =
{ const_entry_body = mkFix ((nvrec',i),recdecls);
const_entry_type = Some arrec.(i);
const_entry_opaque = false;
const_entry_boxed = boxed} in
let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
in (ConstRef kn)
in
(* declare the recursive definitions *)
let lrefrec = Array.mapi declare namerec in
Options.if_verbose ppnl (recursive_message lrefrec);
(* (* The others are declared as normal definitions *)
let var_subst id = (id, Constrintern.global_reference id) in
let _ =
List.fold_left
(fun subst (f,def,t) ->
let ce = { const_entry_body = replace_vars subst def;
const_entry_type = Some t;
const_entry_opaque = false;
const_entry_boxed = boxed } in
let _ =
Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition)
in
warning ((string_of_id f)^" is non-recursively defined");
(var_subst f) :: subst)
(List.map var_subst (Array.to_list namerec))
lnonrec
in*)
List.iter (fun (df,c,scope) ->
Metasyntax.add_notation_interpretation df [] c scope) notations
in
let declare l =
let recvec = Array.of_list l
and arrec = Array.map snd arrec
in declare arrec recvec
in
let recdefs = Array.length defrec in
trace (int recdefs ++ str " recursive definitions");
(* Solve remaining evars *)
let rec solve_evars i acc =
if i < recdefs then
let (evm, def) = defrec.(i) in
if Evd.dom evm = [] then
solve_evars (succ i) (def :: acc)
else
let _,typ = arrec.(i) in
let id = namerec.(i) in
(* Generalize by the recursive prototypes *)
let def =
Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
and typ =
Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in
let tac = Eterm.etermtac (evm, def) in
let _ =
trace (str "Starting proof of a fixpoint def:" ++ spc () ++ my_print_constr env0 def ++
spc () ++ str " with goal: " ++ my_print_constr env0 typ ++
spc () ++ str " with evar map = " ++ Evd.pr_evar_map evm)
in
begin
Command.start_proof (id_of_string (string_of_id id ^ "_evars")) goal_kind typ
(fun _ gr ->
let _ = trace (str "Got a proof of: " ++ pr_global gr) in
let constant = match gr with Libnames.ConstRef c -> c
| _ -> assert(false)
in
try
let def = Environ.constant_value (Global.env ()) constant in
let _ = trace (str "Got constant value") in
let _, c = decompose_lam_n recdefs def in
let _ = trace (str "Fixpoint body is: " ++ spc () ++ my_print_constr (Global.env ()) c) in
solve_evars (succ i) (c :: acc)
with Environ.NotEvaluableConst cer ->
match cer with
Environ.NoBody -> trace (str "Constant has no body")
| Environ.Opaque -> trace (str "Constant is opaque")
);
trace (str "Started proof");
Pfedit.by tac;
trace (str "Applied eterm tac");
end
else declare (List.rev acc)
in solve_evars 0 []
|
