diff options
author | 2008-12-31 10:57:09 +0000 | |
---|---|---|
committer | 2008-12-31 10:57:09 +0000 | |
commit | 0d03f17a33b43aa87bb201953e4e1a567aac6355 (patch) | |
tree | bfb3179e3de28fee2d900b202de3a4281a062eda /pretyping/reductionops.ml | |
parent | d3c49a6e536006ff121f01303ddc0a43b4c90e23 (diff) |
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added
shortcuts for "fst (decompose_prod t)" and co.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/reductionops.ml')
-rw-r--r-- | pretyping/reductionops.ml | 26 |
1 files changed, 18 insertions, 8 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 4bb9a9a5d..f51820bf6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -750,7 +750,7 @@ let splay_prod env sigma = 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 @@ -767,14 +767,14 @@ let splay_prod_assum env sigma = 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 @@ -784,15 +784,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 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" + (m-1) (add_rel_decl (n,None,a) ln) c0 + | _ -> invalid_arg "splay_prod_n" in - decrec env n Sign.empty_rel_context + 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 |