Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Reductionops refactoring

Semantic changes are :
- whd_nored_stack remplaces a defined meta by its value whereas the old whd_stack
  didn't.
- Zcase and Zfix are alwais put on stack. iota_flag is checked by constructors and
  cofix.
- simpl uses its own whd_ function that do not touch at matched term

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15634 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit 57128547546baa38ab436c87ed66361342c36cb8 1 parent 1982377
@pirbo pirbo authored
View
2  lib/option.mli
@@ -67,7 +67,7 @@ val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
(** [fold_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *)
val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option
-(** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
+(** [cata f e x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
val cata : ('a -> 'b) -> 'b -> 'a option -> 'b
(** {6 More Specific Operations} ***)
View
2  pretyping/evarconv.ml
@@ -60,7 +60,7 @@ let evar_apprec ts env evd stack c =
decompose_app (zip (whd_betaiota_deltazeta_for_iota_state ts env evd (c,append_stack_app_list stack empty_stack)))
let apprec_nohdbeta ts env evd c =
- match kind_of_term (fst (Reductionops.whd_stack evd c)) with
+ match kind_of_term (fst (Reductionops.whd_nored_stack evd c)) with
| (Case _ | Fix _) -> applist (evar_apprec ts env evd [] c)
| _ -> c
View
67 pretyping/reductionops.ml
@@ -71,9 +71,10 @@ let strip_n_app n s =
let nfirsts_app_of_stack n s =
let (args, _) = strip_app s in list_firstn n args
let list_of_app_stack s =
- let (out,s') = strip_app s in assert (s' = []); out
+ let (out,s') = strip_app s in
+ Option.init (s' = []) out
let array_of_app_stack s =
- Array.of_list (list_of_app_stack s)
+ Option.map Array.of_list (list_of_app_stack s)
let rec zip = function
| f, [] -> f
| f, (Zapp [] :: s) -> zip (f, s)
@@ -136,26 +137,12 @@ let safe_evar_value sigma ev =
try Some (Evd.existential_value sigma ev)
with NotInstantiatedEvar | Not_found -> None
-let rec whd_app_state sigma (x, stack as s) =
- match kind_of_term x with
- | App (f,cl) -> whd_app_state sigma (f, append_stack_app cl stack)
- | Cast (c,_,_) -> whd_app_state sigma (c, stack)
- | Evar ev ->
- (match safe_evar_value sigma ev with
- 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 t = decompose_app (zip t)
-let whd_stack sigma x =
- appterm_of_stack (whd_app_state sigma (x, empty_stack))
-let whd_castapp_stack = whd_stack
-
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
@@ -214,6 +201,7 @@ end : RedFlagsSig)
open RedFlags
(* Local *)
+let nored = mkflags []
let beta = mkflags [fbeta]
let eta = mkflags [feta]
let zeta = mkflags [fzeta]
@@ -341,30 +329,32 @@ let rec whd_state_gen flags ts env sigma =
| _ -> s)
| _ -> s)
- | Case (ci,p,d,lf) when red_iota flags ->
+ | Case (ci,p,d,lf) ->
whrec (d, Zcase (ci,p,lf) :: stack)
- | Fix ((ri,n),_ as f) when red_iota flags ->
+ | Fix ((ri,n),_ as f) ->
(match strip_n_app ri.(n) stack with
|None -> s
|Some (bef,arg,s') -> whrec (arg, Zfix(f,bef)::s'))
- | Construct (ind,c) -> begin
- match strip_app stack with
+ | Construct (ind,c) ->
+ if red_iota flags then
+ match strip_app stack with
|args, (Zcase(ci, _, lf)::s') ->
whrec (lf.(c-1), append_stack_app_list (list_skipn ci.ci_npar args) s')
|args, (Zfix (f,s')::s'') ->
let x' = applist(x,args) in
whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
|_ -> s
- end
+ else s
- | CoFix cofix -> begin
- match strip_app stack with
+ | CoFix cofix ->
+ if red_iota flags then
+ match strip_app stack with
|args, (Zcase(ci, _, lf)::s') ->
- whrec (contract_cofix cofix, stack)
+ whrec (contract_cofix cofix, stack)
|_ -> s
- end
+ else s
| x -> s
in
@@ -395,10 +385,10 @@ let local_whd_state_gen flags sigma =
| _ -> s)
| _ -> s)
- | Case (ci,p,d,lf) when red_iota flags ->
+ | Case (ci,p,d,lf) ->
whrec (d, Zcase (ci,p,lf) :: stack)
- | Fix ((ri,n),_ as f) when red_iota flags ->
+ | Fix ((ri,n),_ as f) ->
(match strip_n_app ri.(n) stack with
|None -> s
|Some (bef,arg,s') -> whrec (arg, Zfix(f,bef)::s'))
@@ -413,22 +403,24 @@ let local_whd_state_gen flags sigma =
Some c -> whrec (c,stack)
| None -> s)
- | Construct (ind,c) -> begin
- match strip_app stack with
+ | Construct (ind,c) ->
+ if red_iota flags then
+ match strip_app stack with
|args, (Zcase(ci, _, lf)::s') ->
whrec (lf.(c-1), append_stack_app_list (list_skipn ci.ci_npar args) s')
|args, (Zfix (f,s')::s'') ->
let x' = applist(x,args) in
whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
|_ -> s
- end
+ else s
- | CoFix cofix -> begin
- match strip_app stack with
- |args, (Zcase(ci, _, lf)::s') ->
- whrec (contract_cofix cofix, stack)
+ | CoFix cofix ->
+ if red_iota flags then
+ match strip_app stack with
+ |args, (Zcase(ci, _, lf)::s') when red_iota flags ->
+ whrec (contract_cofix cofix, stack)
|_ -> s
- end
+ else s
| x -> s
in
@@ -441,6 +433,11 @@ let stack_red_of_state_red f sigma x =
let red_of_state_red f sigma x =
zip (f sigma (x,empty_stack))
+(* 0. No Reduction Functions *)
+
+let whd_nored_state = local_whd_state_gen nored
+let whd_nored_stack = stack_red_of_state_red whd_nored_state
+
(* 1. Beta Reduction Functions *)
let whd_beta_state = local_whd_state_gen beta
View
15 pretyping/reductionops.mli
@@ -39,8 +39,10 @@ val decomp_stack : 'a stack -> ('a * 'a stack) option
(** Takes the n first arguments of application put on the stack. Fails is the
stack does not start by n arguments of application. *)
val nfirsts_app_of_stack : int -> 'a stack -> 'a list
-val list_of_app_stack : 'a stack -> 'a list
-val array_of_app_stack : 'a stack -> 'a array
+(** @return (the nth first elements, the (n+1)th element, the remaining stack) *)
+val strip_n_app : int -> 'a stack -> ('a list * 'a * 'a stack) option
+val list_of_app_stack : 'a stack -> 'a list option
+val array_of_app_stack : 'a stack -> 'a array option
val stack_assign : 'a stack -> int -> 'a -> 'a stack
val stack_args_size : 'a stack -> int
val zip : constr * constr stack -> constr
@@ -66,12 +68,6 @@ type contextual_state_reduction_function =
type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
-(** Removes cast and put into applicative form *)
-val whd_stack : local_stack_reduction_function
-
-(** For compatibility: alias for whd\_stack *)
-val whd_castapp_stack : local_stack_reduction_function
-
(** {6 Reduction Function Operators } *)
val strong : reduction_function -> reduction_function
@@ -106,6 +102,8 @@ val whd_betadeltaiota_nolet : contextual_reduction_function
val whd_betaetalet : local_reduction_function
val whd_betalet : local_reduction_function
+(** Removes cast and put into applicative form *)
+val whd_nored_stack : local_stack_reduction_function
val whd_beta_stack : local_stack_reduction_function
val whd_betaiota_stack : local_stack_reduction_function
val whd_betaiotazeta_stack : local_stack_reduction_function
@@ -114,6 +112,7 @@ val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function
val whd_betaetalet_stack : local_stack_reduction_function
val whd_betalet_stack : local_stack_reduction_function
+val whd_nored_state : local_state_reduction_function
val whd_beta_state : local_state_reduction_function
val whd_betaiota_state : local_state_reduction_function
val whd_betaiotazeta_state : local_state_reduction_function
View
41 pretyping/tacred.ml
@@ -617,6 +617,39 @@ let recargs r =
let dont_expose_case r =
try (get_behaviour r).b_dont_expose_case with Not_found -> false
+let whd_nothing_for_iota env sigma s =
+ let rec whrec (x, stack as s) =
+ match kind_of_term x with
+ | Rel n ->
+ (match lookup_rel n env with
+ | (_,Some body,_) -> whrec (lift n body, stack)
+ | _ -> s)
+ | Var id ->
+ (match lookup_named id env with
+ | (_,Some body,_) -> whrec (body, stack)
+ | _ -> s)
+ | Evar ev ->
+ (try whrec (Evd.existential_value sigma ev, stack)
+ with Evd.NotInstantiatedEvar | Not_found -> s)
+ | Meta ev ->
+ (try whrec (Evd.meta_value sigma ev, stack)
+ with Not_found -> s)
+ | Const const when is_transparent_constant full_transparent_state const ->
+ (match constant_opt_value env const with
+ | Some body -> whrec (body, stack)
+ | None -> s)
+ | LetIn (_,b,_,c) -> stacklam whrec [b] c stack
+ | Cast (c,_,_) -> whrec (c, stack)
+ | App (f,cl) -> whrec (f, append_stack_app cl stack)
+ | Lambda (na,t,c) ->
+ (match decomp_stack stack with
+ | Some (a,m) -> stacklam whrec [a] c m
+ | _ -> s)
+
+ | x -> s
+ in
+ decompose_app (zip (whrec (s,empty_stack)))
+
(* [red_elim_const] contracts iota/fix/cofix redexes hidden behind
constants by keeping the name of the constants in the recursive calls;
it fails if no redex is around *)
@@ -640,12 +673,12 @@ let rec red_elim_const env sigma ref largs =
try match reference_eval sigma env ref with
| EliminationCases n when nargs >= n ->
let c = reference_value sigma env ref in
- let c', lrest = whd_betadelta_stack env sigma (applist(c,largs)) in
+ let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
let whfun = whd_simpl_stack env sigma in
(special_red_case env sigma whfun (destCase c'), lrest)
| EliminationFix (min,minfxargs,infos) when nargs >= min ->
let c = reference_value sigma env ref in
- let d, lrest = whd_betadelta_stack env sigma (applist(c,largs)) in
+ let d, lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in
let whfun = whd_construct_stack env sigma in
(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
@@ -660,7 +693,7 @@ let rec red_elim_const env sigma ref largs =
let c', lrest = whd_betalet_stack sigma (applist(c,args)) in
descend (destEvalRef c') lrest in
let (_, midargs as s) = descend ref largs in
- let d, lrest = whd_betadelta_stack env sigma (applist s) in
+ let d, lrest = whd_nothing_for_iota env sigma (applist s) in
let f = make_elim_fun refinfos midargs in
let whfun = whd_construct_stack env sigma in
(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
@@ -1082,7 +1115,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
else
(* lazily reduces to match the head of [t] with the expected [ref] *)
let rec elimrec env t l =
- let c, _ = Reductionops.whd_stack sigma t in
+ let c, _ = Reductionops.whd_nored_stack sigma t in
match kind_of_term c with
| Prod (n,ty,t') ->
if allow_product then
View
12 pretyping/unification.ml
@@ -967,12 +967,12 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
types of metavars are unifiable with the types of their instances *)
let check_types env flags (sigma,_,_ as subst) m n =
- if isEvar_or_Meta (fst (whd_stack sigma m)) then
+ if isEvar_or_Meta (fst (whd_nored_stack sigma m)) then
unify_0_with_initial_metas subst true env CUMUL
flags
(get_type_of env sigma n)
(get_type_of env sigma m)
- else if isEvar_or_Meta (fst (whd_stack sigma n)) then
+ else if isEvar_or_Meta (fst (whd_nored_stack sigma n)) then
unify_0_with_initial_metas subst true env CUMUL
flags
(get_type_of env sigma m)
@@ -1193,8 +1193,8 @@ let secondOrderAbstractionAlgo dep =
if dep then secondOrderDependentAbstraction else secondOrderAbstraction
let w_unify2 env evd flags dep cv_pb ty1 ty2 =
- let c1, oplist1 = whd_stack evd ty1 in
- let c2, oplist2 = whd_stack evd ty2 in
+ let c1, oplist1 = whd_nored_stack evd ty1 in
+ let c2, oplist2 = whd_nored_stack evd ty2 in
match kind_of_term c1, kind_of_term c2 with
| Meta p1, _ ->
(* Find the predicate *)
@@ -1225,8 +1225,8 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
convertible and first-order otherwise. But if failed if e.g. the type of
Meta(1) had meta-variables in it. *)
let w_unify env evd cv_pb ?(flags=default_unify_flags) ty1 ty2 =
- let hd1,l1 = whd_stack evd ty1 in
- let hd2,l2 = whd_stack evd ty2 in
+ let hd1,l1 = whd_nored_stack evd ty1 in
+ let hd2,l2 = whd_nored_stack evd ty2 in
match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
(* Pattern case *)
| (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
View
4 proofs/clenv.ml
@@ -276,7 +276,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
let clenv_unique_resolver ?(flags=default_unify_flags) clenv gl =
let concl = Goal.V82.concl clenv.evd (sig_it gl) in
- if isMeta (fst (whd_stack clenv.evd clenv.templtyp.rebus)) then
+ if isMeta (fst (whd_nored_stack clenv.evd clenv.templtyp.rebus)) then
clenv_unify CUMUL ~flags (clenv_type clenv) concl
(clenv_unify_meta_types ~flags clenv)
else
@@ -429,7 +429,7 @@ let error_already_defined b =
(str "Position " ++ int n ++ str" already defined.")
let clenv_unify_binding_type clenv c t u =
- if isMeta (fst (whd_stack clenv.evd u)) then
+ if isMeta (fst (whd_nored_stack clenv.evd u)) then
(* Not enough information to know if some subtyping is needed *)
CoerceToType, clenv, c
else
View
2  tactics/tactics.ml
@@ -1163,7 +1163,7 @@ let specialize mopt (c,lbind) g =
let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
let flags = { default_unify_flags with resolve_evars = true } in
let clause = clenv_unify_meta_types ~flags clause in
- let (thd,tstack) = whd_stack clause.evd (clenv_value clause) in
+ let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
let nargs = List.length tstack in
let tstack = match mopt with
| Some m ->
Please sign in to comment.
Something went wrong with that request. Please try again.