45
module SPretyping = Subtac_pretyping.Pretyping
48
open Subtac_obligations
50
(*********************************************************************)
51
(* Functions to parse and interpret constructions *)
53
let evar_nf isevars c =
54
isevars := Evarutil.nf_evar_defs !isevars;
55
Evarutil.nf_isevar !isevars c
57
let interp_gen kind isevars env
58
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
60
let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in
61
let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
64
let interp_constr isevars env c =
65
interp_gen (OfType None) isevars env c
67
let interp_type_evars isevars env ?(impls=([],[])) c =
68
interp_gen IsType isevars env ~impls c
70
let interp_casted_constr isevars env ?(impls=([],[])) c typ =
71
interp_gen (OfType (Some typ)) isevars env ~impls c
73
let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
74
interp_gen (OfType (Some typ)) isevars env ~impls c
76
let interp_open_constr isevars env c =
77
msgnl (str "Pretyping " ++ my_print_constr_expr c);
78
let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in
79
let c' = SPretyping.pretype_gen isevars env ([], []) (OfType None) c in
82
let interp_constr_judgment isevars env c =
84
SPretyping.understand_judgment_tcc isevars env
85
(Constrintern.intern_constr (Evd.evars_of !isevars) env c)
87
{ uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
89
let locate_if_isevar loc na = function
92
| Name id -> Reserve.find_reserved_type id
93
| Anonymous -> raise Not_found
94
with Not_found -> RHole (loc, Evd.BinderType na))
97
let interp_binder sigma env na t =
98
let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in
99
SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
101
let interp_context_evars evdref env params =
102
let bl = Constrintern.intern_context false (Evd.evars_of !evdref) env params in
103
let (env, par, _, impls) =
105
(fun (env,params,n,impls) (na, k, b, t) ->
108
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
109
let t = SPretyping.understand_tcc_evars evdref env IsType t' in
110
let d = (na,None,t) in
113
let na = match na with Name n -> Some n | Anonymous -> None in
114
(ExplByPos (n, na), (true, true)) :: impls
117
(push_rel d env, d::params, succ n, impls)
119
let c = SPretyping.understand_judgment_tcc evdref env b in
120
let d = (na, Some c.uj_val, c.uj_type) in
121
(push_rel d env,d::params, succ n, impls))
122
(env,[],1,[]) (List.rev bl)
125
(* try to find non recursive definitions *)
127
let list_chop_hd i l = match list_chop i l with
128
| (l1,x::l2) -> (l1,x,l2)
129
| (x :: [], l2) -> ([], x, [])
132
let collect_non_rec env =
133
let rec searchrec lnonrec lnamerec ldefrec larrec nrec =
138
if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
139
then i else failwith "try_find_i")
142
let (lf1,f,lf2) = list_chop_hd i lnamerec in
143
let (ldef1,def,ldef2) = list_chop_hd i ldefrec in
144
let (lar1,ar,lar2) = list_chop_hd i larrec in
147
match list_chop i nrec with
148
| (lnv1,_::lnv2) -> (lnv1@lnv2)
149
| _ -> [] (* nrec=[] for cofixpoints *)
150
with Failure "list_chop" -> []
152
searchrec ((f,def,ar)::lnonrec)
153
(lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
154
with Failure "try_find_i" ->
156
(Array.of_list lnamerec, Array.of_list ldefrec,
157
Array.of_list larrec, Array.of_list nrec))
161
let list_of_local_binders l =
162
let rec aux acc = function
163
Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
164
| Topconstr.LocalRawAssum (nl, k, c) :: tl ->
165
aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
169
let lift_binders k n l =
170
let rec aux n = function
171
| (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl
175
let rec gen_rels = function
177
| n -> mkRel n :: gen_rels (pred n)
179
let split_args n rel = match list_chop ((List.length rel) - n) rel with
180
(l1, x :: l2) -> l1, x, l2
183
let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
184
Coqlib.check_required_library ["Coq";"Program";"Wf"];
185
let sigma = Evd.empty in
186
let isevars = ref (Evd.create_evar_defs sigma) in
187
let env = Global.env() in
188
let pr c = my_print_constr env c in
189
let prr = Printer.pr_rel_context env in
190
let _prn = Printer.pr_named_context env in
191
let _pr_rel env = Printer.pr_rel_context env in
193
(* try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ *)
194
(* Ppconstr.pr_binders bl ++ str " : " ++ *)
195
(* Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ *)
196
(* Ppconstr.pr_constr_expr body) *)
199
let (env', binders_rel), impls = interp_context_evars isevars env bl in
200
let after, ((argname, _, argtyp) as arg), before =
201
let idx = list_index (Name (snd n)) (List.rev_map (fun (na, _, _) -> na) binders_rel) in
202
split_args idx binders_rel in
203
let before_length, after_length = List.length before, List.length after in
204
let argid = match argname with Name n -> n | _ -> assert(false) in
205
let liftafter = lift_binders 1 after_length after in
206
let envwf = push_rel_context before env in
207
let wf_rel, wf_rel_fun, measure_fn =
208
let rconstr_body, rconstr =
209
let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in
210
let env = push_rel_context [arg] envwf in
211
let capp = interp_constr isevars env app in
212
capp, mkLambda (argname, argtyp, capp)
214
trace (str"rconstr_body: " ++ pr rconstr_body);
216
let lt_rel = constr_of_global (Lazy.force lt_ref) in
217
let name s = Name (id_of_string s) in
218
let wf_rel_fun lift x y = (* lift to before_env *)
219
trace (str"lifter rconstr_body:" ++ pr (liftn lift 2 rconstr_body));
220
mkApp (lt_rel, [| subst1 x (liftn lift 2 rconstr_body);
221
subst1 y (liftn lift 2 rconstr_body) |])
224
mkLambda (name "x", argtyp,
225
mkLambda (name "y", lift 1 argtyp,
226
wf_rel_fun 0 (mkRel 2) (mkRel 1)))
228
wf_rel, wf_rel_fun , Some rconstr
229
else rconstr, (fun lift x y -> mkApp (rconstr, [|x; y|])), None
231
let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
233
let argid' = id_of_string (string_of_id argid ^ "'") in
234
let wfarg len = (Name argid', None,
235
mkSubset (Name argid') (lift len argtyp)
236
(wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1))))
238
let top_bl = after @ (arg :: before) in
239
let top_env = push_rel_context top_bl env in
240
let top_arity = interp_type_evars isevars top_env arityc in
241
let intern_bl = wfarg 1 :: arg :: before in
242
let _intern_env = push_rel_context intern_bl env in
243
let proj = (Lazy.force sig_).Coqlib.proj1 in
245
mkApp (proj, [| argtyp ;
246
(mkLambda (Name argid', argtyp,
247
(wf_rel_fun 1 (mkRel 1) (mkRel 3)))) ;
251
let intern_arity = it_mkProd_or_LetIn top_arity after in
252
(* Intern arity is in top_env = arg :: before *)
253
let intern_arity = liftn 2 2 intern_arity in
254
(* trace (str "After lifting arity: " ++ *)
255
(* my_print_constr (push_rel (Name argid', None, lift 2 argtyp) intern_env) *)
257
(* arity is now in something :: wfarg :: arg :: before
258
where what refered to arg now refers to something *)
259
let intern_arity = substl [projection] intern_arity in
260
(* substitute the projection of wfarg for something *)
261
let intern_before_env = push_rel_context before env in
262
let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
263
let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
264
let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in
265
let fun_env = push_rel_context fun_bl intern_before_env in
266
let fun_arity = interp_type_evars isevars fun_env arityc in
267
let intern_body = interp_casted_constr isevars fun_env body fun_arity in
268
let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
270
try trace ((* str "Fun bl: " ++ prr fun_bl ++ spc () ++ *)
271
str "Intern bl" ++ prr intern_bl ++ spc ())
272
(* str "Top bl" ++ prr top_bl ++ spc () ++ *)
273
(* str "Intern arity: " ++ pr intern_arity ++ *)
274
(* str "Top arity: " ++ pr top_arity ++ spc () ++ *)
275
(* str "Intern body " ++ pr intern_body_lam) *)
278
let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
279
(* Lift to get to constant arguments *)
280
let lift_cst = List.length after + 1 in
282
match measure_fn with
284
mkApp (constr_of_global (Lazy.force fix_sub_ref),
287
make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
289
lift lift_cst intern_body_lam |])
291
mkApp (constr_of_global (Lazy.force fix_measure_sub_ref),
292
[| lift lift_cst argtyp ;
295
lift lift_cst intern_body_lam |])
297
let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
298
let def = it_mkLambda_or_LetIn def_appl binders_rel in
299
let typ = it_mkProd_or_LetIn top_arity binders_rel in
300
let fullcoqc = Evarutil.nf_isevar !isevars def in
301
let fullctyp = Evarutil.nf_isevar !isevars typ in
302
let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in
303
let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in
304
let evm = non_instanciated_map env isevars evm in
305
let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
306
Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars
308
let nf_evar_context isevars ctx =
309
List.map (fun (n, b, t) ->
310
(n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
312
let interp_fix_context evdref env fix =
313
interp_context_evars evdref env fix.Command.fix_binders
315
let interp_fix_ccl evdref (env,_) fix =
316
interp_type_evars evdref env fix.Command.fix_type
318
let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
319
let env = push_rel_context ctx env_rec in
320
let body = interp_casted_constr_evars evdref env ~impls fix.Command.fix_body ccl in
321
it_mkLambda_or_LetIn body ctx
323
let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
325
let prepare_recursive_declaration fixnames fixtypes fixdefs =
326
let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
327
let names = List.map (fun id -> Name id) fixnames in
328
(Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
330
let rel_index n ctx =
331
list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx))
335
| Some (x, b') -> x :: unfold f b'
338
let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
340
| Some (loc, n) -> [rel_index n fixctx]
342
(* If recursive argument was not given by user, we try all args.
343
An earlier approach was to look only for inductive arguments,
344
but doing it properly involves delta-reduction, and it finally
345
doesn't seem to worth the effort (except for huge mutual
347
let len = List.length fixctx in
348
unfold (function x when x = len -> None
349
| n -> Some (n, succ n)) 0
351
let push_named_context = List.fold_right push_named
353
let check_evars env initial_sigma evd c =
354
let sigma = evars_of evd in
355
let c = nf_evar sigma c in
357
match kind_of_term c with
359
assert (Evd.mem sigma evk);
360
if not (Evd.mem initial_sigma evk) then
361
let (loc,k) = evar_source evk evd in
363
| QuestionMark _ -> ()
365
let evi = nf_evar_info sigma (Evd.find sigma evk) in
366
Pretype_errors.error_unsolvable_implicit loc env sigma evi k None)
367
| _ -> iter_constr proc_rec c
370
let interp_recursive fixkind l boxed =
371
let env = Global.env() in
372
let fixl, ntnl = List.split l in
373
let kind = if fixkind <> Command.IsCoFixpoint then Fixpoint else CoFixpoint in
374
let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
376
(* Interp arities allowing for unresolved types *)
377
let evdref = ref (Evd.create_evar_defs Evd.empty) in
378
let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in
379
let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
380
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
382
List.fold_left2 (fun env id t -> (id,None,t) :: env)
385
let env_rec = push_named_context rec_sign env in
387
(* Get interpretation metadatas *)
388
let impls = Command.compute_interning_datas env Constrintern.Recursive [] fixnames fixtypes fiximps in
389
let notations = List.fold_right Option.List.cons ntnl [] in
391
(* Interp bodies with rollback because temp use of notations/implicit *)
393
States.with_state_protection (fun () ->
394
List.iter (Command.declare_interning_data impls) notations;
395
list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
398
(* Instantiate evars and check all are resolved *)
399
let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in
400
let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in
401
let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in
402
let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in
404
let recdefs = List.length rec_sign in
405
List.iter (check_evars env_rec Evd.empty evd) fixdefs;
406
List.iter (check_evars env Evd.empty evd) fixtypes;
407
Command.check_mutuality env kind (List.combine fixnames fixdefs);
409
(* Russell-specific code *)
411
(* Get the interesting evars, those that were not instanciated *)
412
let isevars = Evd.undefined_evars evd in
413
let evm = Evd.evars_of isevars in
414
(* Solve remaining evars *)
415
let rec collect_evars id def typ imps =
416
(* Generalize by the recursive prototypes *)
418
Termops.it_mkNamedLambda_or_LetIn def rec_sign
420
Termops.it_mkNamedProd_or_LetIn typ rec_sign
422
let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
423
let evm' = Subtac_utils.evars_of_term evm evm' typ in
424
let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
425
(id, def, typ, imps, evars)
427
let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
429
| Command.IsFixpoint wfl ->
430
let possible_indexes =
431
list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
432
let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
433
Array.of_list fixtypes,
434
Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
436
let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
437
list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l
438
| Command.IsCoFixpoint -> ());
439
Subtac_obligations.add_mutual_definitions defs notations fixkind
443
| None -> raise Not_found
445
let build_recursive l b =
446
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
448
[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
449
ignore(build_wellfounded (id, out_n n, bl, typ, def) r false ntn false)
451
| [(n, CMeasureRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
452
ignore(build_wellfounded (id, out_n n, bl, typ, def) r true ntn false)
454
| _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
455
let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) ->
456
({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l
457
in interp_recursive (Command.IsFixpoint g) fixl b
459
errorlabstrm "Subtac_command.build_recursive"
460
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
462
let build_corecursive l b =
463
let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
464
({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn))
466
interp_recursive Command.IsCoFixpoint fixl b
added
removed
contrib/subtac/subtac_command.ml
