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
(* $Id: reductionops.ml 11897 2009-02-09 19:28:02Z barras $ *)
27
(**********************************************************************)
28
(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
30
type 'a stack_member =
32
| Zcase of case_info * 'a * 'a array
33
| Zfix of 'a * 'a stack
37
and 'a stack = 'a stack_member list
40
let append_stack_list l s =
43
| (l1, Zapp l :: s) -> Zapp (l1@l) :: s
44
| (l1, s) -> Zapp l1 :: s
45
let append_stack v s = append_stack_list (Array.to_list v) s
47
(* Collapse the shifts in the stack *)
51
| (_,Zshift(k)::s) -> Zshift(n+k)::s
54
let rec stack_args_size = function
55
| Zapp l::s -> List.length l + stack_args_size s
56
| Zshift(_)::s -> stack_args_size s
57
| Zupdate(_)::s -> stack_args_size s
60
(* When used as an argument stack (only Zapp can appear) *)
61
let rec decomp_stack = function
62
| Zapp[v]::s -> Some (v, s)
63
| Zapp(v::l)::s -> Some (v, (Zapp l :: s))
64
| Zapp [] :: s -> decomp_stack s
66
let rec decomp_stackn = function
67
| Zapp [] :: s -> decomp_stackn s
68
| Zapp l :: s -> (Array.of_list l, s)
70
let array_of_stack s =
71
let rec stackrec = function
73
| Zapp args :: s -> args :: (stackrec s)
75
in Array.of_list (List.concat (stackrec s))
76
let rec list_of_stack = function
78
| Zapp args :: s -> args @ (list_of_stack s)
80
let rec app_stack = function
82
| f, (Zapp [] :: s) -> app_stack (f, s)
83
| f, (Zapp args :: s) ->
84
app_stack (applist (f, args), s)
86
let rec stack_assign s p c = match s with
88
let q = List.length args in
90
Zapp args :: stack_assign s (p-q) c
92
(match list_chop p args with
93
(bef, _::aft) -> Zapp (bef@c::aft) :: s
96
let rec stack_tail p s =
100
let q = List.length args in
101
if p >= q then stack_tail (p-q) s
102
else Zapp (list_skipn p args) :: s
103
| _ -> failwith "stack_tail"
104
let rec stack_nth s p = match s with
106
let q = List.length args in
107
if p >= q then stack_nth s (p-q)
109
| _ -> raise Not_found
111
(**************************************************************)
112
(* The type of (machine) states (= lambda-bar-calculus' cuts) *)
113
type state = constr * constr stack
115
type contextual_reduction_function = env -> evar_map -> constr -> constr
116
type reduction_function = contextual_reduction_function
117
type local_reduction_function = evar_map -> constr -> constr
119
type contextual_stack_reduction_function =
120
env -> evar_map -> constr -> constr * constr list
121
type stack_reduction_function = contextual_stack_reduction_function
122
type local_stack_reduction_function =
123
evar_map -> constr -> constr * constr list
125
type contextual_state_reduction_function =
126
env -> evar_map -> state -> state
127
type state_reduction_function = contextual_state_reduction_function
128
type local_state_reduction_function = evar_map -> state -> state
130
(*************************************)
131
(*** Reduction Functions Operators ***)
132
(*************************************)
134
let safe_evar_value sigma ev =
135
try Some (Evd.existential_value sigma ev)
136
with NotInstantiatedEvar | Not_found -> None
138
let rec whd_state sigma (x, stack as s) =
139
match kind_of_term x with
140
| App (f,cl) -> whd_state sigma (f, append_stack cl stack)
141
| Cast (c,_,_) -> whd_state sigma (c, stack)
143
(match safe_evar_value sigma ev with
144
Some c -> whd_state sigma (c,stack)
148
let appterm_of_stack (f,s) = (f,list_of_stack s)
150
let whd_stack sigma x =
151
appterm_of_stack (whd_state sigma (x, empty_stack))
152
let whd_castapp_stack = whd_stack
154
let stack_reduction_of_reduction red_fun env sigma s =
155
let t = red_fun env sigma (app_stack s) in
158
let strong whdfun env sigma t =
159
let rec strongrec env t =
160
map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
163
let local_strong whdfun sigma =
164
let rec strongrec t = map_constr strongrec (whdfun sigma t) in
167
let rec strong_prodspine redfun sigma c =
168
let x = redfun sigma c in
169
match kind_of_term x with
170
| Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
173
(*************************************)
174
(*** Reduction using bindingss ***)
175
(*************************************)
177
(* This signature is very similar to Closure.RedFlagsSig except there
178
is eta but no per-constant unfolding *)
180
module type RedFlagsSig = sig
188
val mkflags : flag list -> flags
189
val red_beta : flags -> bool
190
val red_delta : flags -> bool
191
val red_eta : flags -> bool
192
val red_iota : flags -> bool
193
val red_zeta : flags -> bool
196
(* Naive Implementation
197
module RedFlags = (struct
198
type flag = BETA | DELTA | EVAR | IOTA | ZETA | ETA
199
type flags = flag list
207
let red_beta = List.mem BETA
208
let red_delta = List.mem DELTA
209
let red_evar = List.mem EVAR
210
let red_eta = List.mem ETA
211
let red_iota = List.mem IOTA
212
let red_zeta = List.mem ZETA
216
(* Compact Implementation *)
217
module RedFlags = (struct
225
let mkflags = List.fold_left (lor) 0
226
let red_beta f = f land fbeta <> 0
227
let red_delta f = f land fdelta <> 0
228
let red_eta f = f land feta <> 0
229
let red_iota f = f land fiota <> 0
230
let red_zeta f = f land fzeta <> 0
236
let beta = mkflags [fbeta]
237
let eta = mkflags [feta]
238
let betaiota = mkflags [fiota; fbeta]
239
let betaiotazeta = mkflags [fiota; fbeta;fzeta]
242
let delta = mkflags [fdelta]
243
let betadelta = mkflags [fbeta;fdelta;fzeta]
244
let betadeltaeta = mkflags [fbeta;fdelta;fzeta;feta]
245
let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fiota]
246
let betadeltaiota_nolet = mkflags [fbeta;fdelta;fiota]
247
let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fiota;feta]
248
let betaetalet = mkflags [fbeta;feta;fzeta]
249
let betalet = mkflags [fbeta;fzeta]
251
(* Beta Reduction tools *)
253
let rec stacklam recfun env t stack =
254
match (decomp_stack stack,kind_of_term t) with
255
| Some (h,stacktl), Lambda (_,_,c) -> stacklam recfun (h::env) c stacktl
256
| _ -> recfun (substl env t, stack)
258
let beta_applist (c,l) =
259
stacklam app_stack [] c (append_stack_list l empty_stack)
261
(* Iota reduction tools *)
263
type 'a miota_args = {
264
mP : constr; (* the result type *)
265
mconstr : constr; (* the constructor *)
266
mci : case_info; (* special info to re-build pattern *)
267
mcargs : 'a list; (* the constructor's arguments *)
268
mlf : 'a array } (* the branch code vector *)
270
let reducible_mind_case c = match kind_of_term c with
271
| Construct _ | CoFix _ -> true
274
let contract_cofix (bodynum,(types,names,bodies as typedbodies)) =
275
let nbodies = Array.length bodies in
276
let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in
277
substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
279
let reduce_mind_case mia =
280
match kind_of_term mia.mconstr with
281
| Construct (ind_sp,i) ->
282
(* let ncargs = (fst mia.mci).(i-1) in*)
283
let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
284
applist (mia.mlf.(i-1),real_cargs)
286
let cofix_def = contract_cofix cofix in
287
mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
290
(* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
291
Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
293
let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
294
let nbodies = Array.length recindices in
295
let make_Fi j = mkFix ((recindices,nbodies-j-1),typedbodies) in
296
substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
298
let fix_recarg ((recindices,bodynum),_) stack =
299
assert (0 <= bodynum & bodynum < Array.length recindices);
300
let recargnum = Array.get recindices bodynum in
302
Some (recargnum, stack_nth stack recargnum)
306
type fix_reduction_result = NotReducible | Reduced of state
308
let reduce_fix whdfun sigma fix stack =
309
match fix_recarg fix stack with
310
| None -> NotReducible
311
| Some (recargnum,recarg) ->
312
let (recarg'hd,_ as recarg') = whdfun sigma (recarg, empty_stack) in
313
let stack' = stack_assign stack recargnum (app_stack recarg') in
314
(match kind_of_term recarg'hd with
315
| Construct _ -> Reduced (contract_fix fix, stack')
318
(* Generic reduction function *)
320
(* Y avait un commentaire pour whd_betadeltaiota :
322
NB : Cette fonction alloue peu c'est l'appel
323
``let (c,cargs) = whfun (recarg, empty_stack)''
327
let rec whd_state_gen flags env sigma =
328
let rec whrec (x, stack as s) =
329
match kind_of_term x with
330
| Rel n when red_delta flags ->
331
(match lookup_rel n env with
332
| (_,Some body,_) -> whrec (lift n body, stack)
334
| Var id when red_delta flags ->
335
(match lookup_named id env with
336
| (_,Some body,_) -> whrec (body, stack)
339
(match safe_evar_value sigma ev with
340
| Some body -> whrec (body, stack)
342
| Const const when red_delta flags ->
343
(match constant_opt_value env const with
344
| Some body -> whrec (body, stack)
346
| LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
347
| Cast (c,_,_) -> whrec (c, stack)
348
| App (f,cl) -> whrec (f, append_stack cl stack)
350
(match decomp_stack stack with
351
| Some (a,m) when red_beta flags -> stacklam whrec [a] c m
352
| None when red_eta flags ->
353
let env' = push_rel (na,None,t) env in
354
let whrec' = whd_state_gen flags env' sigma in
355
(match kind_of_term (app_stack (whrec' (c, empty_stack))) with
357
let napp = Array.length cl in
359
let x', l' = whrec' (array_last cl, empty_stack) in
360
match kind_of_term x', decomp_stack l' with
362
let lc = Array.sub cl 0 (napp-1) in
363
let u = if napp=1 then f else appvect (f,lc) in
364
if noccurn 1 u then (pop u,empty_stack) else s
370
| Case (ci,p,d,lf) when red_iota flags ->
371
let (c,cargs) = whrec (d, empty_stack) in
372
if reducible_mind_case c then
373
whrec (reduce_mind_case
374
{mP=p; mconstr=c; mcargs=list_of_stack cargs;
375
mci=ci; mlf=lf}, stack)
377
(mkCase (ci, p, app_stack (c,cargs), lf), stack)
379
| Fix fix when red_iota flags ->
380
(match reduce_fix (fun _ -> whrec) sigma fix stack with
381
| Reduced s' -> whrec s'
388
let local_whd_state_gen flags sigma =
389
let rec whrec (x, stack as s) =
390
match kind_of_term x with
391
| LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
392
| Cast (c,_,_) -> whrec (c, stack)
393
| App (f,cl) -> whrec (f, append_stack cl stack)
395
(match decomp_stack stack with
396
| Some (a,m) when red_beta flags -> stacklam whrec [a] c m
397
| None when red_eta flags ->
398
(match kind_of_term (app_stack (whrec (c, empty_stack))) with
400
let napp = Array.length cl in
402
let x', l' = whrec (array_last cl, empty_stack) in
403
match kind_of_term x', decomp_stack l' with
405
let lc = Array.sub cl 0 (napp-1) in
406
let u = if napp=1 then f else appvect (f,lc) in
407
if noccurn 1 u then (pop u,empty_stack) else s
413
| Case (ci,p,d,lf) when red_iota flags ->
414
let (c,cargs) = whrec (d, empty_stack) in
415
if reducible_mind_case c then
416
whrec (reduce_mind_case
417
{mP=p; mconstr=c; mcargs=list_of_stack cargs;
418
mci=ci; mlf=lf}, stack)
420
(mkCase (ci, p, app_stack (c,cargs), lf), stack)
422
| Fix fix when red_iota flags ->
423
(match reduce_fix (fun _ ->whrec) sigma fix stack with
424
| Reduced s' -> whrec s'
428
(match safe_evar_value sigma ev with
429
Some c -> whrec (c,stack)
437
let stack_red_of_state_red f sigma x =
438
appterm_of_stack (f sigma (x, empty_stack))
440
let red_of_state_red f sigma x =
441
app_stack (f sigma (x,empty_stack))
443
(* 1. Beta Reduction Functions *)
445
let whd_beta_state = local_whd_state_gen beta
446
let whd_beta_stack = stack_red_of_state_red whd_beta_state
447
let whd_beta = red_of_state_red whd_beta_state
450
let whd_betaetalet_state = local_whd_state_gen betaetalet
451
let whd_betaetalet_stack = stack_red_of_state_red whd_betaetalet_state
452
let whd_betaetalet = red_of_state_red whd_betaetalet_state
454
let whd_betalet_state = local_whd_state_gen betalet
455
let whd_betalet_stack = stack_red_of_state_red whd_betalet_state
456
let whd_betalet = red_of_state_red whd_betalet_state
458
(* 2. Delta Reduction Functions *)
460
let whd_delta_state e = whd_state_gen delta e
461
let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env)
462
let whd_delta env = red_of_state_red (whd_delta_state env)
464
let whd_betadelta_state e = whd_state_gen betadelta e
465
let whd_betadelta_stack env =
466
stack_red_of_state_red (whd_betadelta_state env)
467
let whd_betadelta env =
468
red_of_state_red (whd_betadelta_state env)
471
let whd_betadeltaeta_state e = whd_state_gen betadeltaeta e
472
let whd_betadeltaeta_stack env =
473
stack_red_of_state_red (whd_betadeltaeta_state env)
474
let whd_betadeltaeta env =
475
red_of_state_red (whd_betadeltaeta_state env)
477
(* 3. Iota reduction Functions *)
479
let whd_betaiota_state = local_whd_state_gen betaiota
480
let whd_betaiota_stack = stack_red_of_state_red whd_betaiota_state
481
let whd_betaiota = red_of_state_red whd_betaiota_state
483
let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta
484
let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state
485
let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state
487
let whd_betadeltaiota_state e = whd_state_gen betadeltaiota e
488
let whd_betadeltaiota_stack env =
489
stack_red_of_state_red (whd_betadeltaiota_state env)
490
let whd_betadeltaiota env =
491
red_of_state_red (whd_betadeltaiota_state env)
493
let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e
494
let whd_betadeltaiotaeta_stack env =
495
stack_red_of_state_red (whd_betadeltaiotaeta_state env)
496
let whd_betadeltaiotaeta env =
497
red_of_state_red (whd_betadeltaiotaeta_state env)
499
let whd_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e
500
let whd_betadeltaiota_nolet_stack env =
501
stack_red_of_state_red (whd_betadeltaiota_nolet_state env)
502
let whd_betadeltaiota_nolet env =
503
red_of_state_red (whd_betadeltaiota_nolet_state env)
505
(* 3. Eta reduction Functions *)
507
let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack))
509
(****************************************************************************)
510
(* Reduction Functions *)
511
(****************************************************************************)
513
(* Replacing defined evars for error messages *)
514
let rec whd_evar sigma c =
515
match kind_of_term c with
517
(match safe_evar_value sigma ev with
518
Some c -> whd_evar sigma c
520
| Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
521
| _ -> collapse_appl c
524
local_strong whd_evar
526
(* lazy reduction functions. The infos must be created for each term *)
527
(* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add
529
let clos_norm_flags flgs env sigma t =
531
(create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
534
let nf_beta = clos_norm_flags Closure.beta empty_env
535
let nf_betaiota = clos_norm_flags Closure.betaiota empty_env
536
let nf_betadeltaiota env sigma =
537
clos_norm_flags Closure.betadeltaiota env sigma
540
(* Attention reduire un beta-redexe avec un argument qui n'est pas
541
une variable, peut changer enormement le temps de conversion lors
545
let rec whd_betaiota_preserving_vm_cast env sigma t =
546
let rec stacklam_var subst t stack =
547
match (decomp_stack stack,kind_of_term t) with
548
| Some (h,stacktl), Lambda (_,_,c) ->
549
begin match kind_of_term h with
550
| Rel i when not (evaluable_rel i env) ->
551
stacklam_var (h::subst) c stacktl
552
| Var id when not (evaluable_named id env)->
553
stacklam_var (h::subst) c stacktl
554
| _ -> whrec (substl subst t, stack)
556
| _ -> whrec (substl subst t, stack)
557
and whrec (x, stack as s) =
558
match kind_of_term x with
560
(match safe_evar_value sigma ev with
561
| Some body -> whrec (body, stack)
563
| Cast (c,VMcast,t) ->
564
let c = app_stack (whrec (c,empty_stack)) in
565
let t = app_stack (whrec (t,empty_stack)) in
566
(mkCast(c,VMcast,t),stack)
567
| Cast (c,DEFAULTcast,_) ->
569
| App (f,cl) -> whrec (f, append_stack cl stack)
571
(match decomp_stack stack with
572
| Some (a,m) -> stacklam_var [a] c m
574
| Case (ci,p,d,lf) ->
575
let (c,cargs) = whrec (d, empty_stack) in
576
if reducible_mind_case c then
577
whrec (reduce_mind_case
578
{mP=p; mconstr=c; mcargs=list_of_stack cargs;
579
mci=ci; mlf=lf}, stack)
581
(mkCase (ci, p, app_stack (c,cargs), lf), stack)
584
app_stack (whrec (t,empty_stack))
586
let nf_betaiota_preserving_vm_cast =
587
strong whd_betaiota_preserving_vm_cast
589
(* lazy weak head reduction functions *)
590
let whd_flags flgs env sigma t =
592
(create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
595
(********************************************************************)
597
(********************************************************************)
599
let fkey = Profile.declare_profile "fhnf";;
600
let fhnf info v = Profile.profile2 fkey fhnf info v;;
602
let fakey = Profile.declare_profile "fhnf_apply";;
603
let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;;
606
let is_transparent k =
607
Conv_oracle.get_strategy k <> Conv_oracle.Opaque
609
(* Conversion utility functions *)
611
type conversion_test = constraints -> constraints
613
let pb_is_equal pb = pb = CONV
615
let pb_equal = function
619
let sort_cmp = sort_cmp
621
let test_conversion (f:?evars:'a->'b) env sigma x y =
623
f ~evars:(safe_evar_value sigma) env x y in true
624
with NotConvertible -> false
626
let is_conv env sigma = test_conversion Reduction.conv env sigma
627
let is_conv_leq env sigma = test_conversion Reduction.conv_leq env sigma
628
let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq
630
let test_trans_conversion f reds env sigma x y =
631
try let _ = f reds env (nf_evar sigma x) (nf_evar sigma y) in true
632
with NotConvertible -> false
634
let is_trans_conv env sigma = test_trans_conversion Reduction.trans_conv env sigma
635
let is_trans_conv_leq env sigma = test_trans_conversion Reduction.trans_conv_leq env sigma
636
let is_trans_fconv = function | CONV -> is_trans_conv | CUMUL -> is_trans_conv_leq
638
(********************************************************************)
639
(* Special-Purpose Reduction *)
640
(********************************************************************)
642
let whd_meta metamap c = match kind_of_term c with
643
| Meta p -> (try List.assoc p metamap with Not_found -> c)
646
(* Try to replace all metas. Does not replace metas in the metas' values
647
* Differs from (strong whd_meta). *)
648
let plain_instance s c =
649
let rec irec n u = match kind_of_term u with
650
| Meta p -> (try lift n (List.assoc p s) with Not_found -> u)
651
| App (f,l) when isCast f ->
652
let (f,_,t) = destCast f in
653
let l' = Array.map (irec n) l in
654
(match kind_of_term f with
656
(* Don't flatten application nodes: this is used to extract a
657
proof-term from a proof-tree and we want to keep the structure
659
(try let g = List.assoc p s in
660
match kind_of_term g with
662
let h = id_of_string "H" in
663
mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
665
with Not_found -> mkApp (f,l'))
666
| _ -> mkApp (irec n f,l'))
667
| Cast (m,_,_) when isMeta m ->
668
(try lift n (List.assoc (destMeta m) s) with Not_found -> u)
670
map_constr_with_binders succ irec n u
672
if s = [] then c else irec 0 c
674
(* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota]
675
has (unfortunately) different subtle side effects:
677
- ** Order of subgoals **
678
If the lemma is a case analysis with parameters, it will move the
679
parameters as first subgoals (e.g. "case H" applied on
680
"H:D->A/\B|-C" will present the subgoal |-D first while w/o
681
betaiota the subgoal |-D would have come last).
683
- ** Betaiota-contraction in statement **
684
If the lemma has a parameter which is a function and this
685
function is applied in the lemma, then the _strong_ betaiota will
686
contract the application of the function to its argument (e.g.
687
"apply (H (fun x => x))" in "H:forall f, f 0 = 0 |- 0=0" will
688
result in applying the lemma 0=0 in which "(fun x => x) 0" has
689
been contracted). A goal to rewrite may then fail or succeed
692
- ** Naming of hypotheses **
693
If a lemma is a function of the form "fun H:(forall a:A, P a)
694
=> .. F H .." where the expected type of H is "forall b:A, P b",
695
then, without reduction, the application of the lemma will
696
generate a subgoal "forall a:A, P a" (and intro will use name
697
"a"), while with reduction, it will generate a subgoal "forall
698
b:A, P b" (and intro will use name "b").
700
- ** First-order pattern-matching **
701
If a lemma has the type "(fun x => p) t" then rewriting t may fail
702
if the type of the lemma is first beta-reduced (this typically happens
703
when rewriting a single variable and the type of the lemma is obtained
704
by meta_instance (with empty map) which itself calls instance with this
709
(* if s = [] then c else *)
710
local_strong whd_betaiota Evd.empty (plain_instance s c)
712
(* pseudo-reduction rule:
713
* [hnf_prod_app env s (Prod(_,B)) N --> B[N]
714
* with an HNF on the first argument to produce a product.
715
* if this does not work, then we use the string S as part of our
718
let hnf_prod_app env sigma t n =
719
match kind_of_term (whd_betadeltaiota env sigma t) with
720
| Prod (_,_,b) -> subst1 n b
721
| _ -> anomaly "hnf_prod_app: Need a product"
723
let hnf_prod_appvect env sigma t nl =
724
Array.fold_left (hnf_prod_app env sigma) t nl
726
let hnf_prod_applist env sigma t nl =
727
List.fold_left (hnf_prod_app env sigma) t nl
729
let hnf_lam_app env sigma t n =
730
match kind_of_term (whd_betadeltaiota env sigma t) with
731
| Lambda (_,_,b) -> subst1 n b
732
| _ -> anomaly "hnf_lam_app: Need an abstraction"
734
let hnf_lam_appvect env sigma t nl =
735
Array.fold_left (hnf_lam_app env sigma) t nl
737
let hnf_lam_applist env sigma t nl =
738
List.fold_left (hnf_lam_app env sigma) t nl
740
let splay_prod env sigma =
741
let rec decrec env m c =
742
let t = whd_betadeltaiota env sigma c in
743
match kind_of_term t with
745
decrec (push_rel (n,None,a) env)
751
let splay_lambda env sigma =
752
let rec decrec env m c =
753
let t = whd_betadeltaiota env sigma c in
754
match kind_of_term t with
756
decrec (push_rel (n,None,a) env)
762
let splay_prod_assum env sigma =
763
let rec prodec_rec env l c =
764
let t = whd_betadeltaiota_nolet env sigma c in
765
match kind_of_term t with
767
prodec_rec (push_rel (x,None,t) env)
768
(Sign.add_rel_decl (x, None, t) l) c
770
prodec_rec (push_rel (x, Some b, t) env)
771
(Sign.add_rel_decl (x, Some b, t) l) c
772
| Cast (c,_,_) -> prodec_rec env l c
775
prodec_rec env Sign.empty_rel_context
777
let splay_arity env sigma c =
778
let l, c = splay_prod env sigma c in
779
match kind_of_term c with
781
| _ -> invalid_arg "splay_arity"
783
let sort_of_arity env c = snd (splay_arity env Evd.empty c)
785
let decomp_n_prod env sigma n =
786
let rec decrec env m ln c = if m = 0 then (ln,c) else
787
match kind_of_term (whd_betadeltaiota env sigma c) with
789
decrec (push_rel (n,None,a) env)
790
(m-1) (Sign.add_rel_decl (n,None,a) ln) c0
791
| _ -> invalid_arg "decomp_n_prod"
793
decrec env n Sign.empty_rel_context
797
let decomp_sort env sigma t =
798
match kind_of_term (whd_betadeltaiota env sigma t) with
800
| _ -> raise NotASort
802
let is_sort env sigma arity =
803
try let _ = decomp_sort env sigma arity in true
804
with NotASort -> false
806
(* reduction to head-normal-form allowing delta/zeta only in argument
807
of case/fix (heuristic used by evar_conv) *)
809
let whd_betaiota_deltazeta_for_iota_state env sigma s =
811
let (t, stack as s) = whd_betaiota_state sigma s in
812
match kind_of_term t with
813
| Case (ci,p,d,lf) ->
814
let (cr,crargs) = whd_betadeltaiota_stack env sigma d in
815
let rslt = mkCase (ci, p, applist (cr,crargs), lf) in
816
if reducible_mind_case cr then
821
(match reduce_fix (whd_betadeltaiota_state env) sigma fix stack with
822
| Reduced s -> whrec s
827
(* A reduction function like whd_betaiota but which keeps casts
828
* and does not reduce redexes containing existential variables.
829
* Used in Correctness.
830
* Added by JCF, 29/1/98. *)
832
let whd_programs_stack env sigma =
833
let rec whrec (x, stack as s) =
834
match kind_of_term x with
836
let n = Array.length cl - 1 in
838
if occur_existential c then
841
whrec (mkApp (f, Array.sub cl 0 n), append_stack [|c|] stack)
843
if occur_existential b then
846
stacklam whrec [b] c stack
848
(match decomp_stack stack with
850
| Some (a,m) -> stacklam whrec [a] c m)
851
| Case (ci,p,d,lf) ->
852
if occur_existential d then
855
let (c,cargs) = whrec (d, empty_stack) in
856
if reducible_mind_case c then
857
whrec (reduce_mind_case
858
{mP=p; mconstr=c; mcargs=list_of_stack cargs;
859
mci=ci; mlf=lf}, stack)
861
(mkCase (ci, p, app_stack(c,cargs), lf), stack)
863
(match reduce_fix (fun _ ->whrec) sigma fix stack with
864
| Reduced s' -> whrec s'
870
let whd_programs env sigma x =
871
app_stack (whd_programs_stack env sigma (x, empty_stack))
875
let find_conclusion env sigma =
876
let rec decrec env c =
877
let t = whd_betadeltaiota env sigma c in
878
match kind_of_term t with
879
| Prod (x,t,c0) -> decrec (push_rel (x,None,t) env) c0
880
| Lambda (x,t,c0) -> decrec (push_rel (x,None,t) env) c0
885
let is_arity env sigma c =
886
match find_conclusion env sigma c with
890
(*************************************)
893
let meta_value evd mv =
895
match meta_opt_fvalue evd mv with
898
(List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
904
let meta_instance env b =
907
(fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
909
if c_sigma = [] then b.rebus else instance c_sigma b.rebus
911
let nf_meta env c = meta_instance env (mk_freelisted c)
913
(* Instantiate metas that create beta/iota redexes *)
915
let meta_value evd mv =
917
match meta_opt_fvalue evd mv with
920
(List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
926
let meta_reducible_instance evd b =
927
let fm = Metaset.elements b.freemetas in
928
let metas = List.fold_left (fun l mv ->
929
match (try meta_opt_fvalue evd mv with Not_found -> None) with
930
| Some (g,(_,s)) -> (mv,(g.rebus,s))::l
931
| None -> l) [] fm in
933
let u = whd_betaiota Evd.empty u in
934
match kind_of_term u with
935
| Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
936
let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
939
let g,s = List.assoc m metas in
940
if isConstruct g or s <> CoerceToType then Some g else None
941
with Not_found -> None
943
| Some g -> irec (mkCase (ci,p,g,bl))
944
| None -> mkCase (ci,irec p,c,Array.map irec bl))
945
| App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) ->
946
let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in
949
let g,s = List.assoc m metas in
950
if isLambda g or s <> CoerceToType then Some g else None
951
with Not_found -> None
953
| Some g -> irec (mkApp (g,l))
954
| None -> mkApp (f,Array.map irec l))
956
(try let g,s = List.assoc m metas in if s<>CoerceToType then irec g else u
958
| _ -> map_constr irec u
960
if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus
added
removed
pretyping/reductionops.ml
