1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: decl_interp.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
18
open Pretyping.Default
25
let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args)
27
let intern_justification_items globs =
28
Option.map (List.map (intern_constr globs))
30
let intern_justification_method globs =
31
Option.map (intern_tactic globs)
33
let intern_statement intern_it globs st =
34
{st_label=st.st_label;
35
st_it=intern_it globs st.st_it}
37
let intern_no_bind intern_it globs x =
38
globs,intern_it globs x
40
let intern_constr_or_thesis globs = function
42
| This c -> This (intern_constr globs c)
45
let l1,l2=globs.ltacvars in
46
{globs with ltacvars= (id::l1),(id::l2)}
48
let add_name nam globs=
51
| Name id -> add_var id globs
53
let intern_hyp iconstr globs = function
54
Hvar (loc,(id,topt)) -> add_var id globs,
55
Hvar (loc,(id,Option.map (intern_constr globs) topt))
56
| Hprop st -> add_name st.st_label globs,
57
Hprop (intern_statement iconstr globs st)
59
let intern_hyps iconstr globs hyps =
60
snd (list_fold_map (intern_hyp iconstr) globs hyps)
62
let intern_cut intern_it globs cut=
63
let nglobs,nstat=intern_it globs cut.cut_stat in
65
cut_by=intern_justification_items nglobs cut.cut_by;
66
cut_using=intern_justification_method nglobs cut.cut_using}
68
let intern_casee globs = function
69
Real c -> Real (intern_constr globs c)
70
| Virtual cut -> Virtual
71
(intern_cut (intern_no_bind (intern_statement intern_constr)) globs cut)
73
let intern_hyp_list args globs =
74
let intern_one globs (loc,(id,opttyp)) =
76
(loc,(id,Option.map (intern_constr globs) opttyp)) in
77
list_fold_map intern_one globs args
79
let intern_suffices_clause globs (hyps,c) =
80
let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in
81
nglobs,(nhyps,intern_constr_or_thesis nglobs c)
83
let intern_fundecl args body globs=
84
let nglobs,nargs = intern_hyp_list args globs in
85
nargs,intern_constr nglobs body
87
let rec add_vars_of_simple_pattern globs = function
88
CPatAlias (loc,p,id) ->
89
add_vars_of_simple_pattern (add_var id globs) p
90
(* Stdpp.raise_with_loc loc
91
(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
93
Stdpp.raise_with_loc loc
94
(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
95
| CPatDelimiters (_,_,p) ->
96
add_vars_of_simple_pattern globs p
97
| CPatCstr (_,_,pl) ->
98
List.fold_left add_vars_of_simple_pattern globs pl
99
| CPatNotation(_,_,(pl,pll)) ->
100
List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll))
101
| CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
104
let rec intern_bare_proof_instr globs = function
105
Pthus i -> Pthus (intern_bare_proof_instr globs i)
106
| Pthen i -> Pthen (intern_bare_proof_instr globs i)
107
| Phence i -> Phence (intern_bare_proof_instr globs i)
110
(intern_no_bind (intern_statement intern_constr_or_thesis)) globs c)
112
Psuffices (intern_cut intern_suffices_clause globs c)
115
(intern_no_bind (intern_statement intern_constr)) globs c)
116
| Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps)
117
| Pcase (params,pat,hyps) ->
118
let nglobs,nparams = intern_hyp_list params globs in
119
let nnglobs= add_vars_of_simple_pattern nglobs pat in
120
let nhyps = intern_hyps intern_constr_or_thesis nnglobs hyps in
121
Pcase (nparams,pat,nhyps)
122
| Ptake witl -> Ptake (List.map (intern_constr globs) witl)
123
| Pconsider (c,hyps) -> Pconsider (intern_constr globs c,
124
intern_hyps intern_constr globs hyps)
125
| Pper (et,c) -> Pper (et,intern_casee globs c)
128
| Passume hyps -> Passume (intern_hyps intern_constr globs hyps)
129
| Pgiven hyps -> Pgiven (intern_hyps intern_constr globs hyps)
130
| Plet hyps -> Plet (intern_hyps intern_constr globs hyps)
131
| Pclaim st -> Pclaim (intern_statement intern_constr globs st)
132
| Pfocus st -> Pfocus (intern_statement intern_constr globs st)
133
| Pdefine (id,args,body) ->
134
let nargs,nbody = intern_fundecl args body globs in
135
Pdefine (id,nargs,nbody)
137
Pcast (id,intern_constr globs typ)
139
let rec intern_proof_instr globs instr=
141
instr = intern_bare_proof_instr globs instr.instr}
145
let interp_justification_items sigma env =
146
Option.map (List.map (fun c ->understand sigma env (fst c)))
148
let interp_constr check_sort sigma env c =
150
understand_type sigma env (fst c)
152
understand sigma env (fst c)
154
let special_whd env =
155
let infos=Closure.create_clos_infos Closure.betadeltaiota env in
156
(fun t -> Closure.whd_val infos (Closure.inject t))
158
let _eq = Libnames.constr_of_global (Coqlib.glob_eq)
160
let decompose_eq env id =
161
let typ = Environ.named_type id env in
162
let whd = special_whd env typ in
163
match kind_of_term whd with
165
if eq_constr f _eq && (Array.length args)=3
167
else error "Previous step is not an equality."
168
| _ -> error "Previous step is not an equality."
170
let get_eq_typ info env =
171
let typ = decompose_eq env (get_last env) in
174
let interp_constr_in_type typ sigma env c =
175
understand sigma env (fst c) ~expected_type:typ
177
let interp_statement interp_it sigma env st =
178
{st_label=st.st_label;
179
st_it=interp_it sigma env st.st_it}
181
let interp_constr_or_thesis check_sort sigma env = function
183
| This c -> This (interp_constr check_sort sigma env c)
185
let type_tester_var body typ =
187
RLambda(dummy_loc,Anonymous,Explicit,typ,
188
RSort (dummy_loc,RProp Null)),body)
190
let abstract_one_hyp inject h raw =
192
Hvar (loc,(id,None)) ->
193
RProd (dummy_loc,Name id, Explicit, RHole (loc,Evd.BinderType (Name id)), raw)
194
| Hvar (loc,(id,Some typ)) ->
195
RProd (dummy_loc,Name id, Explicit, fst typ, raw)
197
RProd (dummy_loc,st.st_label, Explicit, inject st.st_it, raw)
199
let rawconstr_of_hyps inject hyps head =
200
List.fold_right (abstract_one_hyp inject) hyps head
202
let raw_prop = RSort (dummy_loc,RProp Null)
204
let rec match_hyps blend names constr = function
205
[] -> [],substl names constr
207
let (name,typ,body)=destProd constr in
208
let st= {st_label=name;st_it=substl names typ} in
211
Anonymous -> mkMeta 0 :: names
212
| Name id -> mkVar id :: names in
213
let qhyp = match hyp with
214
Hprop st' -> Hprop (blend st st')
215
| Hvar _ -> Hvar st in
216
let rhyps,head = match_hyps blend qnames body q in
219
let interp_hyps_gen inject blend sigma env hyps head =
220
let constr=understand sigma env (rawconstr_of_hyps inject hyps head) in
221
match_hyps blend [] constr hyps
223
let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps raw_prop)
225
let dummy_prefix= id_of_string "__"
227
let rec deanonymize ids =
229
PatVar (loc,Anonymous) ->
230
let (found,known) = !ids in
231
let new_id=Nameops.next_ident_away dummy_prefix known in
232
let _= ids:= (loc,new_id) :: found , new_id :: known in
233
PatVar (loc,Name new_id)
234
| PatVar (loc,Name id) as pat ->
235
let (found,known) = !ids in
236
let _= ids:= (loc,id) :: found , known in
238
| PatCstr(loc,cstr,lpat,nam) ->
239
PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam)
243
PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable"
244
| PatVar (loc,Name id) ->
246
| PatCstr(loc,((ind,_) as cstr),lpat,_) ->
247
let mind= fst (Global.lookup_inductive ind) in
248
let rec add_params n q =
250
add_params (pred n) (RHole(dummy_loc,
251
Evd.TomatchTypeParameter(ind,n))::q) in
252
let args = List.map raw_of_pat lpat in
253
raw_app(loc,RRef(dummy_loc,Libnames.ConstructRef cstr),
254
add_params mind.Declarations.mind_nparams args)
256
let prod_one_hyp = function
259
RProd (dummy_loc,Name id, Explicit,
260
RHole (loc,Evd.BinderType (Name id)), raw))
261
| (loc,(id,Some typ)) ->
263
RProd (dummy_loc,Name id, Explicit, fst typ, raw))
265
let prod_one_id (loc,id) raw =
266
RProd (dummy_loc,Name id, Explicit,
267
RHole (loc,Evd.BinderType (Name id)), raw)
269
let let_in_one_alias (id,pat) raw =
270
RLetIn (dummy_loc,Name id, raw_of_pat pat, raw)
272
let rec bind_primary_aliases map pat =
275
| PatCstr(loc,_,lpat,nam) ->
279
| Name id -> (id,pat)::map
281
List.fold_left bind_primary_aliases map1 lpat
283
let bind_secondary_aliases map subst =
284
List.fold_left (fun map (ids,idp) -> (ids,List.assoc idp map)::map) map subst
286
let bind_aliases patvars subst patt =
287
let map = bind_primary_aliases [] patt in
288
let map1 = bind_secondary_aliases map subst in
291
let interp_pattern env pat_expr =
292
let patvars,pats = Constrintern.intern_pattern env pat_expr in
294
[] -> anomaly "empty pattern list"
296
(patvars,bind_aliases patvars subst patt,patt)
297
| _ -> anomaly "undetected disjunctive pattern"
299
let rec match_args dest names constr = function
300
[] -> [],names,substl names constr
302
let (name,typ,body)=dest constr in
303
let st={st_label=name;st_it=substl names typ} in
306
Anonymous -> assert false
307
| Name id -> mkVar id :: names in
308
let args,bnames,body = match_args dest qnames body q in
311
let rec match_aliases names constr = function
312
[] -> [],names,substl names constr
314
let (name,c,typ,body)=destLetIn constr in
315
let st={st_label=name;st_it=(substl names c,substl names typ)} in
318
Anonymous -> assert false
319
| Name id -> mkVar id :: names in
320
let args,bnames,body = match_aliases qnames body q in
323
let detype_ground c = Detyping.detype false [] [] c
325
let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
327
match info.pm_stack with
328
Per(et,pi,_,_)::_ -> et,pi
329
| _ -> error "No proof per cases/induction/inversion in progress." in
330
let mib,oib=Global.lookup_inductive pinfo.per_ind in
331
let num_params = pinfo.per_nparams in
333
let expected = mib.Declarations.mind_nparams - num_params in
334
if List.length params <> expected then
335
errorlabstrm "suppose it is"
336
(str "Wrong number of extra arguments: " ++
337
(if expected = 0 then str "none" else int expected) ++
340
let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in
341
let rparams = List.map detype_ground pinfo.per_params in
345
RVar (loc,id)) params in
347
list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark (Evd.Define false)))
348
oib.Declarations.mind_nrealargs in
349
raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
350
let pat_vars,aliases,patt = interp_pattern env pat in
351
let inject = function
352
Thesis (Plain) -> Rawterm.RSort(dummy_loc,RProp Null)
353
| Thesis (For rec_occ) ->
354
if not (List.mem rec_occ pat_vars) then
355
errorlabstrm "suppose it is"
356
(str "Variable " ++ Nameops.pr_id rec_occ ++
357
str " does not occur in pattern.");
358
Rawterm.RSort(dummy_loc,RProp Null)
360
let term1 = rawconstr_of_hyps inject hyps raw_prop in
362
let rids=ref ([],pat_vars) in
363
let npatt= deanonymize rids patt in
364
List.rev (fst !rids),npatt in
366
RLetIn(dummy_loc,Anonymous,
367
RCast(dummy_loc,raw_of_pat npatt,
368
CastConv (DEFAULTcast,app_ind)),term1) in
369
let term3=List.fold_right let_in_one_alias aliases term2 in
370
let term4=List.fold_right prod_one_id loc_ids term3 in
371
let term5=List.fold_right prod_one_hyp params term4 in
372
let constr = understand sigma env term5 in
373
let tparams,nam4,rest4 = match_args destProd [] constr params in
374
let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in
375
let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in
376
let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in
379
Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label}
380
| This _ -> {st_it = This st.st_it;st_label=st.st_label} in
381
let thyps = fst (match_hyps blend nam2 (Termops.pop rest1) hyps) in
382
tparams,{pat_vars=tpatvars;
383
pat_aliases=taliases;
389
let interp_cut interp_it sigma env cut=
390
let nenv,nstat = interp_it sigma env cut.cut_stat in
393
cut_by=interp_justification_items sigma nenv cut.cut_by}
395
let interp_no_bind interp_it sigma env x =
396
env,interp_it sigma env x
398
let interp_suffices_clause sigma env (hyps,cot)=
399
let (locvars,_) as res =
402
let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in
404
| Thesis Plain as th -> interp_hyps sigma env hyps,th
405
| Thesis (For n) -> error "\"thesis for\" is not applicable here." in
406
let push_one hyp env0 =
408
(Hprop st | Hvar st) ->
409
match st.st_label with
410
Name id -> Environ.push_named (id,None,st.st_it) env0
412
let nenv = List.fold_right push_one locvars env in
415
let interp_casee sigma env = function
416
Real c -> Real (understand sigma env (fst c))
417
| Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut)
419
let abstract_one_arg = function
422
RLambda (dummy_loc,Name id, Explicit,
423
RHole (loc,Evd.BinderType (Name id)), raw))
424
| (loc,(id,Some typ)) ->
426
RLambda (dummy_loc,Name id, Explicit, fst typ, raw))
428
let rawconstr_of_fun args body =
429
List.fold_right abstract_one_arg args (fst body)
431
let interp_fun sigma env args body =
432
let constr=understand sigma env (rawconstr_of_fun args body) in
433
match_args destLambda [] constr args
435
let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = function
436
Pthus i -> Pthus (interp_bare_proof_instr info sigma env i)
437
| Pthen i -> Pthen (interp_bare_proof_instr info sigma env i)
438
| Phence i -> Phence (interp_bare_proof_instr info sigma env i)
439
| Pcut c -> Pcut (interp_cut
440
(interp_no_bind (interp_statement
441
(interp_constr_or_thesis true)))
444
Psuffices (interp_cut interp_suffices_clause sigma env c)
445
| Prew (s,c) -> Prew (s,interp_cut
446
(interp_no_bind (interp_statement
447
(interp_constr_in_type (get_eq_typ info env))))
450
| Psuppose hyps -> Psuppose (interp_hyps sigma env hyps)
451
| Pcase (params,pat,hyps) ->
452
let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in
453
Pcase (tparams,tpat,thyps)
455
Ptake (List.map (fun c -> understand sigma env (fst c)) witl)
456
| Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c,
457
interp_hyps sigma env hyps)
458
| Pper (et,c) -> Pper (et,interp_casee sigma env c)
461
| Passume hyps -> Passume (interp_hyps sigma env hyps)
462
| Pgiven hyps -> Pgiven (interp_hyps sigma env hyps)
463
| Plet hyps -> Plet (interp_hyps sigma env hyps)
464
| Pclaim st -> Pclaim (interp_statement (interp_constr true) sigma env st)
465
| Pfocus st -> Pfocus (interp_statement (interp_constr true) sigma env st)
466
| Pdefine (id,args,body) ->
467
let nargs,_,nbody = interp_fun sigma env args body in
468
Pdefine (id,nargs,nbody)
470
Pcast(id,interp_constr true sigma env typ)
472
let rec interp_proof_instr info sigma env instr=
474
instr = interp_bare_proof_instr info sigma env instr.instr}
added
removed
tactics/decl_interp.ml
