summaryrefslogtreecommitdiff
path: root/pretyping/reductionops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/reductionops.ml')
-rw-r--r--pretyping/reductionops.ml332
1 files changed, 179 insertions, 153 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 33928f67..1a69b633 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: reductionops.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id$ *)
open Pp
open Util
@@ -25,7 +25,7 @@ exception Elimconst
(**********************************************************************)
-(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
+(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
type 'a stack_member =
| Zapp of 'a list
@@ -80,12 +80,12 @@ let rec list_of_stack = function
let rec app_stack = function
| f, [] -> f
| f, (Zapp [] :: s) -> app_stack (f, s)
- | f, (Zapp args :: s) ->
+ | f, (Zapp args :: s) ->
app_stack (applist (f, args), s)
| _ -> assert false
let rec stack_assign s p c = match s with
| Zapp args :: s ->
- let q = List.length args in
+ let q = List.length args in
if p >= q then
Zapp args :: stack_assign s (p-q) c
else
@@ -109,20 +109,20 @@ let rec stack_nth s p = match s with
| _ -> raise Not_found
(**************************************************************)
-(* The type of (machine) states (= lambda-bar-calculus' cuts) *)
+(* The type of (machine) states (= lambda-bar-calculus' cuts) *)
type state = constr * constr stack
type contextual_reduction_function = env -> evar_map -> constr -> constr
type reduction_function = contextual_reduction_function
type local_reduction_function = evar_map -> constr -> constr
-type contextual_stack_reduction_function =
+type contextual_stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
type stack_reduction_function = contextual_stack_reduction_function
type local_stack_reduction_function =
evar_map -> constr -> constr * constr list
-type contextual_state_reduction_function =
+type contextual_state_reduction_function =
env -> evar_map -> state -> state
type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
@@ -135,36 +135,40 @@ let safe_evar_value sigma ev =
try Some (Evd.existential_value sigma ev)
with NotInstantiatedEvar | Not_found -> None
-let rec whd_state sigma (x, stack as s) =
+let rec whd_app_state sigma (x, stack as s) =
match kind_of_term x with
- | App (f,cl) -> whd_state sigma (f, append_stack cl stack)
- | Cast (c,_,_) -> whd_state sigma (c, stack)
+ | App (f,cl) -> whd_app_state sigma (f, append_stack cl stack)
+ | Cast (c,_,_) -> whd_app_state sigma (c, stack)
| Evar ev ->
(match safe_evar_value sigma ev with
- Some c -> whd_state sigma (c,stack)
+ Some c -> whd_app_state sigma (c,stack)
| _ -> s)
| _ -> s
+let safe_meta_value sigma ev =
+ try Some (Evd.meta_value sigma ev)
+ with Not_found -> None
+
let appterm_of_stack (f,s) = (f,list_of_stack s)
let whd_stack sigma x =
- appterm_of_stack (whd_state sigma (x, empty_stack))
+ appterm_of_stack (whd_app_state sigma (x, empty_stack))
let whd_castapp_stack = whd_stack
let stack_reduction_of_reduction red_fun env sigma s =
let t = red_fun env sigma (app_stack s) in
whd_stack t
-let strong whdfun env sigma t =
+let strong whdfun env sigma t =
let rec strongrec env t =
map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
strongrec env t
-let local_strong whdfun sigma =
+let local_strong whdfun sigma =
let rec strongrec t = map_constr strongrec (whdfun sigma t) in
strongrec
-let rec strong_prodspine redfun sigma c =
+let rec strong_prodspine redfun sigma c =
let x = redfun sigma c in
match kind_of_term x with
| Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
@@ -193,33 +197,13 @@ module type RedFlagsSig = sig
val red_zeta : flags -> bool
end
-(* Naive Implementation
-module RedFlags = (struct
- type flag = BETA | DELTA | EVAR | IOTA | ZETA | ETA
- type flags = flag list
- let fbeta = BETA
- let fdelta = DELTA
- let fevar = EVAR
- let fiota = IOTA
- let fzeta = ZETA
- let feta = ETA
- let mkflags l = l
- let red_beta = List.mem BETA
- let red_delta = List.mem DELTA
- let red_evar = List.mem EVAR
- let red_eta = List.mem ETA
- let red_iota = List.mem IOTA
- let red_zeta = List.mem ZETA
-end : RedFlagsSig)
-*)
-
(* Compact Implementation *)
module RedFlags = (struct
type flag = int
type flags = int
let fbeta = 1
let fdelta = 2
- let feta = 8
+ let feta = 8
let fiota = 16
let fzeta = 32
let mkflags = List.fold_left (lor) 0
@@ -235,6 +219,7 @@ open RedFlags
(* Local *)
let beta = mkflags [fbeta]
let eta = mkflags [feta]
+let zeta = mkflags [fzeta]
let betaiota = mkflags [fiota; fbeta]
let betaiotazeta = mkflags [fiota; fbeta;fzeta]
@@ -298,7 +283,7 @@ let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
let fix_recarg ((recindices,bodynum),_) stack =
assert (0 <= bodynum & bodynum < Array.length recindices);
let recargnum = Array.get recindices bodynum in
- try
+ try
Some (recargnum, stack_nth stack recargnum)
with Not_found ->
None
@@ -319,12 +304,12 @@ let reduce_fix whdfun sigma fix stack =
(* Y avait un commentaire pour whd_betadeltaiota :
- NB : Cette fonction alloue peu c'est l'appel
+ NB : Cette fonction alloue peu c'est l'appel
``let (c,cargs) = whfun (recarg, empty_stack)''
-------------------
qui coute cher *)
-let rec whd_state_gen flags env sigma =
+let rec whd_state_gen flags env sigma =
let rec whrec (x, stack as s) =
match kind_of_term x with
| Rel n when red_delta flags ->
@@ -339,6 +324,10 @@ let rec whd_state_gen flags env sigma =
(match safe_evar_value sigma ev with
| Some body -> whrec (body, stack)
| None -> s)
+ | Meta ev ->
+ (match safe_meta_value sigma ev with
+ | Some body -> whrec (body, stack)
+ | None -> s)
| Const const when red_delta flags ->
(match constant_opt_value env const with
| Some body -> whrec (body, stack)
@@ -373,19 +362,19 @@ let rec whd_state_gen flags env sigma =
whrec (reduce_mind_case
{mP=p; mconstr=c; mcargs=list_of_stack cargs;
mci=ci; mlf=lf}, stack)
- else
+ else
(mkCase (ci, p, app_stack (c,cargs), lf), stack)
-
+
| Fix fix when red_iota flags ->
(match reduce_fix (fun _ -> whrec) sigma fix stack with
| Reduced s' -> whrec s'
| NotReducible -> s)
| x -> s
- in
+ in
whrec
-let local_whd_state_gen flags sigma =
+let local_whd_state_gen flags sigma =
let rec whrec (x, stack as s) =
match kind_of_term x with
| LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
@@ -395,7 +384,7 @@ let local_whd_state_gen flags sigma =
(match decomp_stack stack with
| Some (a,m) when red_beta flags -> stacklam whrec [a] c m
| None when red_eta flags ->
- (match kind_of_term (app_stack (whrec (c, empty_stack))) with
+ (match kind_of_term (app_stack (whrec (c, empty_stack))) with
| App (f,cl) ->
let napp = Array.length cl in
if napp > 0 then
@@ -416,9 +405,9 @@ let local_whd_state_gen flags sigma =
whrec (reduce_mind_case
{mP=p; mconstr=c; mcargs=list_of_stack cargs;
mci=ci; mlf=lf}, stack)
- else
+ else
(mkCase (ci, p, app_stack (c,cargs), lf), stack)
-
+
| Fix fix when red_iota flags ->
(match reduce_fix (fun _ ->whrec) sigma fix stack with
| Reduced s' -> whrec s'
@@ -429,8 +418,13 @@ let local_whd_state_gen flags sigma =
Some c -> whrec (c,stack)
| None -> s)
+ | Meta ev ->
+ (match safe_meta_value sigma ev with
+ Some c -> whrec (c,stack)
+ | None -> s)
+
| x -> s
- in
+ in
whrec
@@ -471,7 +465,7 @@ let whd_betadelta env =
let whd_betadeltaeta_state e = whd_state_gen betadeltaeta e
let whd_betadeltaeta_stack env =
stack_red_of_state_red (whd_betadeltaeta_state env)
-let whd_betadeltaeta env =
+let whd_betadeltaeta env =
red_of_state_red (whd_betadeltaeta_state env)
(* 3. Iota reduction Functions *)
@@ -487,25 +481,29 @@ let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state
let whd_betadeltaiota_state e = whd_state_gen betadeltaiota e
let whd_betadeltaiota_stack env =
stack_red_of_state_red (whd_betadeltaiota_state env)
-let whd_betadeltaiota env =
+let whd_betadeltaiota env =
red_of_state_red (whd_betadeltaiota_state env)
let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e
let whd_betadeltaiotaeta_stack env =
stack_red_of_state_red (whd_betadeltaiotaeta_state env)
-let whd_betadeltaiotaeta env =
+let whd_betadeltaiotaeta env =
red_of_state_red (whd_betadeltaiotaeta_state env)
let whd_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e
let whd_betadeltaiota_nolet_stack env =
stack_red_of_state_red (whd_betadeltaiota_nolet_state env)
-let whd_betadeltaiota_nolet env =
+let whd_betadeltaiota_nolet env =
red_of_state_red (whd_betadeltaiota_nolet_state env)
-(* 3. Eta reduction Functions *)
+(* 4. Eta reduction Functions *)
let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack))
+(* 5. Zeta Reduction Functions *)
+
+let whd_zeta c = app_stack (local_whd_state_gen zeta Evd.empty (c,empty_stack))
+
(****************************************************************************)
(* Reduction Functions *)
(****************************************************************************)
@@ -517,8 +515,8 @@ let rec whd_evar sigma c =
(match safe_evar_value sigma ev with
Some c -> whd_evar sigma c
| None -> c)
- | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
- | _ -> collapse_appl c
+ | Sort s -> whd_sort_variable sigma c
+ | _ -> c
let nf_evar =
local_strong whd_evar
@@ -537,53 +535,53 @@ let nf_betadeltaiota env sigma =
clos_norm_flags Closure.betadeltaiota env sigma
-(* Attention reduire un beta-redexe avec un argument qui n'est pas
+(* Attention reduire un beta-redexe avec un argument qui n'est pas
une variable, peut changer enormement le temps de conversion lors
du type checking :
(fun x => x + x) M
*)
-let rec whd_betaiota_preserving_vm_cast env sigma t =
- let rec stacklam_var subst t stack =
- match (decomp_stack stack,kind_of_term t) with
- | Some (h,stacktl), Lambda (_,_,c) ->
- begin match kind_of_term h with
- | Rel i when not (evaluable_rel i env) ->
- stacklam_var (h::subst) c stacktl
- | Var id when not (evaluable_named id env)->
- stacklam_var (h::subst) c stacktl
- | _ -> whrec (substl subst t, stack)
- end
- | _ -> whrec (substl subst t, stack)
- and whrec (x, stack as s) =
- match kind_of_term x with
- | Evar ev ->
- (match safe_evar_value sigma ev with
- | Some body -> whrec (body, stack)
- | None -> s)
- | Cast (c,VMcast,t) ->
- let c = app_stack (whrec (c,empty_stack)) in
- let t = app_stack (whrec (t,empty_stack)) in
- (mkCast(c,VMcast,t),stack)
- | Cast (c,DEFAULTcast,_) ->
- whrec (c, stack)
- | App (f,cl) -> whrec (f, append_stack cl stack)
- | Lambda (na,t,c) ->
- (match decomp_stack stack with
- | Some (a,m) -> stacklam_var [a] c m
- | _ -> s)
- | Case (ci,p,d,lf) ->
- let (c,cargs) = whrec (d, empty_stack) in
- if reducible_mind_case c then
- whrec (reduce_mind_case
- {mP=p; mconstr=c; mcargs=list_of_stack cargs;
- mci=ci; mlf=lf}, stack)
- else
- (mkCase (ci, p, app_stack (c,cargs), lf), stack)
- | x -> s
- in
+let rec whd_betaiota_preserving_vm_cast env sigma t =
+ let rec stacklam_var subst t stack =
+ match (decomp_stack stack,kind_of_term t) with
+ | Some (h,stacktl), Lambda (_,_,c) ->
+ begin match kind_of_term h with
+ | Rel i when not (evaluable_rel i env) ->
+ stacklam_var (h::subst) c stacktl
+ | Var id when not (evaluable_named id env)->
+ stacklam_var (h::subst) c stacktl
+ | _ -> whrec (substl subst t, stack)
+ end
+ | _ -> whrec (substl subst t, stack)
+ and whrec (x, stack as s) =
+ match kind_of_term x with
+ | Evar ev ->
+ (match safe_evar_value sigma ev with
+ | Some body -> whrec (body, stack)
+ | None -> s)
+ | Cast (c,VMcast,t) ->
+ let c = app_stack (whrec (c,empty_stack)) in
+ let t = app_stack (whrec (t,empty_stack)) in
+ (mkCast(c,VMcast,t),stack)
+ | Cast (c,DEFAULTcast,_) ->
+ whrec (c, stack)
+ | App (f,cl) -> whrec (f, append_stack cl stack)
+ | Lambda (na,t,c) ->
+ (match decomp_stack stack with
+ | Some (a,m) -> stacklam_var [a] c m
+ | _ -> s)
+ | Case (ci,p,d,lf) ->
+ let (c,cargs) = whrec (d, empty_stack) in
+ if reducible_mind_case c then
+ whrec (reduce_mind_case
+ {mP=p; mconstr=c; mcargs=list_of_stack cargs;
+ mci=ci; mlf=lf}, stack)
+ else
+ (mkCase (ci, p, app_stack (c,cargs), lf), stack)
+ | x -> s
+ in
app_stack (whrec (t,empty_stack))
-let nf_betaiota_preserving_vm_cast =
+let nf_betaiota_preserving_vm_cast =
strong whd_betaiota_preserving_vm_cast
(* lazy weak head reduction functions *)
@@ -631,26 +629,26 @@ let test_trans_conversion f reds env sigma x y =
try let _ = f reds env (nf_evar sigma x) (nf_evar sigma y) in true
with NotConvertible -> false
-let is_trans_conv env sigma = test_trans_conversion Reduction.trans_conv env sigma
-let is_trans_conv_leq env sigma = test_trans_conversion Reduction.trans_conv_leq env sigma
+let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv reds env sigma
+let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq reds env sigma
let is_trans_fconv = function | CONV -> is_trans_conv | CUMUL -> is_trans_conv_leq
(********************************************************************)
(* Special-Purpose Reduction *)
(********************************************************************)
-let whd_meta metamap c = match kind_of_term c with
- | Meta p -> (try List.assoc p metamap with Not_found -> c)
+let whd_meta sigma c = match kind_of_term c with
+ | Meta p -> (try meta_value sigma p with Not_found -> c)
| _ -> c
(* Try to replace all metas. Does not replace metas in the metas' values
* Differs from (strong whd_meta). *)
-let plain_instance s c =
+let plain_instance s c =
let rec irec n u = match kind_of_term u with
| Meta p -> (try lift n (List.assoc p s) with Not_found -> u)
| App (f,l) when isCast f ->
let (f,_,t) = destCast f in
- let l' = Array.map (irec n) l in
+ let l' = Array.map (irec n) l in
(match kind_of_term f with
| Meta p ->
(* Don't flatten application nodes: this is used to extract a
@@ -658,21 +656,21 @@ let plain_instance s c =
of the proof-tree *)
(try let g = List.assoc p s in
match kind_of_term g with
- | App _ ->
+ | App _ ->
let h = id_of_string "H" in
mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
| _ -> mkApp (g,l')
with Not_found -> mkApp (f,l'))
- | _ -> mkApp (irec n f,l'))
+ | _ -> mkApp (irec n f,l'))
| Cast (m,_,_) when isMeta m ->
(try lift n (List.assoc (destMeta m) s) with Not_found -> u)
| _ ->
map_constr_with_binders succ irec n u
- in
+ in
if s = [] then c else irec 0 c
(* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota]
- has (unfortunately) different subtle side effects:
+ has (unfortunately) different subtle side effects:
- ** Order of subgoals **
If the lemma is a case analysis with parameters, it will move the
@@ -689,7 +687,7 @@ let plain_instance s c =
been contracted). A goal to rewrite may then fail or succeed
differently.
- - ** Naming of hypotheses **
+ - ** Naming of hypotheses **
If a lemma is a function of the form "fun H:(forall a:A, P a)
=> .. F H .." where the expected type of H is "forall b:A, P b",
then, without reduction, the application of the lemma will
@@ -705,9 +703,9 @@ let plain_instance s c =
empty map).
*)
-let instance s c =
+let instance sigma s c =
(* if s = [] then c else *)
- local_strong whd_betaiota Evd.empty (plain_instance s c)
+ local_strong whd_betaiota sigma (plain_instance s c)
(* pseudo-reduction rule:
* [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -720,24 +718,24 @@ let hnf_prod_app env sigma t n =
| Prod (_,_,b) -> subst1 n b
| _ -> anomaly "hnf_prod_app: Need a product"
-let hnf_prod_appvect env sigma t nl =
+let hnf_prod_appvect env sigma t nl =
Array.fold_left (hnf_prod_app env sigma) t nl
-let hnf_prod_applist env sigma t nl =
+let hnf_prod_applist env sigma t nl =
List.fold_left (hnf_prod_app env sigma) t nl
-
+
let hnf_lam_app env sigma t n =
match kind_of_term (whd_betadeltaiota env sigma t) with
| Lambda (_,_,b) -> subst1 n b
| _ -> anomaly "hnf_lam_app: Need an abstraction"
-let hnf_lam_appvect env sigma t nl =
+let hnf_lam_appvect env sigma t nl =
Array.fold_left (hnf_lam_app env sigma) t nl
-let hnf_lam_applist env sigma t nl =
+let hnf_lam_applist env sigma t nl =
List.fold_left (hnf_lam_app env sigma) t nl
-let splay_prod env sigma =
+let splay_prod env sigma =
let rec decrec env m c =
let t = whd_betadeltaiota env sigma c in
match kind_of_term t with
@@ -745,10 +743,10 @@ let splay_prod env sigma =
decrec (push_rel (n,None,a) env)
((n,a)::m) c0
| _ -> m,t
- in
+ in
decrec env []
-let splay_lambda env sigma =
+let splay_lam env sigma =
let rec decrec env m c =
let t = whd_betadeltaiota env sigma c in
match kind_of_term t with
@@ -756,23 +754,23 @@ let splay_lambda env sigma =
decrec (push_rel (n,None,a) env)
((n,a)::m) c0
| _ -> m,t
- in
+ in
decrec env []
-let splay_prod_assum env sigma =
+let splay_prod_assum env sigma =
let rec prodec_rec env l c =
let t = whd_betadeltaiota_nolet env sigma c in
match kind_of_term t with
| Prod (x,t,c) ->
prodec_rec (push_rel (x,None,t) env)
- (Sign.add_rel_decl (x, None, t) l) c
+ (add_rel_decl (x, None, t) l) c
| LetIn (x,b,t,c) ->
prodec_rec (push_rel (x, Some b, t) env)
- (Sign.add_rel_decl (x, Some b, t) l) c
+ (add_rel_decl (x, Some b, t) l) c
| Cast (c,_,_) -> prodec_rec env l c
| _ -> l,t
in
- prodec_rec env Sign.empty_rel_context
+ prodec_rec env empty_rel_context
let splay_arity env sigma c =
let l, c = splay_prod env sigma c in
@@ -782,15 +780,25 @@ let splay_arity env sigma c =
let sort_of_arity env c = snd (splay_arity env Evd.empty c)
-let decomp_n_prod env sigma n =
- let rec decrec env m ln c = if m = 0 then (ln,c) else
+let splay_prod_n env sigma n =
+ let rec decrec env m ln c = if m = 0 then (ln,c) else
match kind_of_term (whd_betadeltaiota env sigma c) with
| Prod (n,a,c0) ->
decrec (push_rel (n,None,a) env)
- (m-1) (Sign.add_rel_decl (n,None,a) ln) c0
- | _ -> invalid_arg "decomp_n_prod"
- in
- decrec env n Sign.empty_rel_context
+ (m-1) (add_rel_decl (n,None,a) ln) c0
+ | _ -> invalid_arg "splay_prod_n"
+ in
+ decrec env n empty_rel_context
+
+let splay_lam_n env sigma n =
+ let rec decrec env m ln c = if m = 0 then (ln,c) else
+ match kind_of_term (whd_betadeltaiota env sigma c) with
+ | Lambda (n,a,c0) ->
+ decrec (push_rel (n,None,a) env)
+ (m-1) (add_rel_decl (n,None,a) ln) c0
+ | _ -> invalid_arg "splay_lam_n"
+ in
+ decrec env n empty_rel_context
exception NotASort
@@ -800,22 +808,22 @@ let decomp_sort env sigma t =
| _ -> raise NotASort
let is_sort env sigma arity =
- try let _ = decomp_sort env sigma arity in true
+ try let _ = decomp_sort env sigma arity in true
with NotASort -> false
(* reduction to head-normal-form allowing delta/zeta only in argument
of case/fix (heuristic used by evar_conv) *)
let whd_betaiota_deltazeta_for_iota_state env sigma s =
- let rec whrec s =
+ let rec whrec s =
let (t, stack as s) = whd_betaiota_state sigma s in
match kind_of_term t with
| Case (ci,p,d,lf) ->
let (cr,crargs) = whd_betadeltaiota_stack env sigma d in
let rslt = mkCase (ci, p, applist (cr,crargs), lf) in
- if reducible_mind_case cr then
+ if reducible_mind_case cr then
whrec (rslt, stack)
- else
+ else
s
| Fix fix ->
(match reduce_fix (whd_betadeltaiota_state env) sigma fix stack with
@@ -829,15 +837,15 @@ let whd_betaiota_deltazeta_for_iota_state env sigma s =
* Used in Correctness.
* Added by JCF, 29/1/98. *)
-let whd_programs_stack env sigma =
+let whd_programs_stack env sigma =
let rec whrec (x, stack as s) =
match kind_of_term x with
| App (f,cl) ->
let n = Array.length cl - 1 in
let c = cl.(n) in
- if occur_existential c then
- s
- else
+ if occur_existential c then
+ s
+ else
whrec (mkApp (f, Array.sub cl 0 n), append_stack [|c|] stack)
| LetIn (_,b,_,c) ->
if occur_existential b then
@@ -864,7 +872,7 @@ let whd_programs_stack env sigma =
| Reduced s' -> whrec s'
| NotReducible -> s)
| _ -> s
- in
+ in
whrec
let whd_programs env sigma x =
@@ -879,7 +887,7 @@ let find_conclusion env sigma =
| Prod (x,t,c0) -> decrec (push_rel (x,None,t) env) c0
| Lambda (x,t,c0) -> decrec (push_rel (x,None,t) env) c0
| t -> t
- in
+ in
decrec env
let is_arity env sigma c =
@@ -890,44 +898,44 @@ let is_arity env sigma c =
(*************************************)
(* Metas *)
-let meta_value evd mv =
+let meta_value evd mv =
let rec valrec mv =
match meta_opt_fvalue evd mv with
- | Some (b,_) ->
- instance
+ | Some (b,_) ->
+ instance evd
(List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
b.rebus
| None -> mkMeta mv
- in
+ in
valrec mv
-let meta_instance env b =
+let meta_instance sigma b =
let c_sigma =
- List.map
- (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
- in
- if c_sigma = [] then b.rebus else instance c_sigma b.rebus
+ List.map
+ (fun mv -> (mv,meta_value sigma mv)) (Metaset.elements b.freemetas)
+ in
+ if c_sigma = [] then b.rebus else instance sigma c_sigma b.rebus
-let nf_meta env c = meta_instance env (mk_freelisted c)
+let nf_meta sigma c = meta_instance sigma (mk_freelisted c)
(* Instantiate metas that create beta/iota redexes *)
-let meta_value evd mv =
+let meta_value evd mv =
let rec valrec mv =
match meta_opt_fvalue evd mv with
| Some (b,_) ->
- instance
+ instance evd
(List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
b.rebus
| None -> mkMeta mv
- in
+ in
valrec mv
let meta_reducible_instance evd b =
let fm = Metaset.elements b.freemetas in
- let metas = List.fold_left (fun l mv ->
+ let metas = List.fold_left (fun l mv ->
match (try meta_opt_fvalue evd mv with Not_found -> None) with
- | Some (g,(_,s)) -> (mv,(g.rebus,s))::l
+ | Some (g,(_,s)) -> (mv,(g.rebus,s))::l
| None -> l) [] fm in
let rec irec u =
let u = whd_betaiota Evd.empty u in
@@ -956,5 +964,23 @@ let meta_reducible_instance evd b =
(try let g,s = List.assoc m metas in if s<>CoerceToType then irec g else u
with Not_found -> u)
| _ -> map_constr irec u
- in
+ in
if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus
+
+
+let head_unfold_under_prod ts env _ c =
+ let unfold cst =
+ if Cpred.mem cst (snd ts) then
+ match constant_opt_value env cst with
+ | Some c -> c
+ | None -> mkConst cst
+ else mkConst cst in
+ let rec aux c =
+ match kind_of_term c with
+ | Prod (n,t,c) -> mkProd (n,aux t, aux c)
+ | _ ->
+ let (h,l) = decompose_app c in
+ match kind_of_term h with
+ | Const cst -> beta_applist (unfold cst,l)
+ | _ -> c in
+ aux c