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

11 files changed, 59 insertions, 54 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a4d0b25ce9..00df4c87a2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1425,10 +1425,10 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
       match b with
       | Some c ->
 	  assert (isRel c);
-	  let p = n + destRel c in aux p (lookup_rel p (rel_context extenv))
+	  let p = n + destRel c in aux p (lookup_rel p extenv)
       | None ->
 	  (n,ty) in
-    let (p,ty) = aux p (lookup_rel p (rel_context extenv)) in
+    let (p,ty) = aux p (lookup_rel p extenv) in
     if noccur_between_without_evar 1 (n'-p-n+1) ty
     then
       let u = lift (n'-n) u in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d161ce612b..8fe807f2ee 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -370,7 +370,7 @@ let set_pattern_names env ind brv =
   let arities =
     Array.map
       (fun c ->
-        rel_context_length (fst (decompose_prod_assum c)) -
+        rel_context_length ((prod_assum c)) -
         mib.mind_nparams)
       mip.mind_nf_lc in
   array_map2 (set_names env) arities brv
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7e7b49d263..5d416cedee 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -75,7 +75,7 @@ type constructor_summary = {
   cs_cstr : constructor;
   cs_params : constr list;
   cs_nargs : int;
-  cs_args : Sign.rel_context;
+  cs_args : rel_context;
   cs_concl_realargs : constr array;
 }
 val lift_constructor : int -> constructor_summary -> constructor_summary
@@ -86,7 +86,7 @@ val get_arity        : env -> inductive_family -> rel_context * sorts_family
 val get_constructors : env -> inductive_family -> constructor_summary array
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr
-val make_arity_signature : env -> bool -> inductive_family -> Sign.rel_context
+val make_arity_signature : env -> bool -> inductive_family -> rel_context
 val make_arity : env -> bool -> inductive_family -> sorts -> types
 val build_branch_type : env -> bool -> constr -> constructor_summary -> types
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7fe358e323..35c5d376ba 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -264,7 +264,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let s' = mkProd (Anonymous, ind, s) in
     let ccl = lift 1 (decomp n pj.uj_val) in
     let ccl' = mkLambda (Anonymous, ind, ccl) in
-      {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} 
+      {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign} 
 
   let evar_kind_of_term sigma c =
     kind_of_term (whd_evar (Evd.evars_of sigma) c)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 99f439224c..e8860c065c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -163,7 +163,7 @@ let cs_pattern_of_constr t =
 let compute_canonical_projections (con,ind) =
   let v = mkConst con in
   let c = Environ.constant_value (Global.env()) con in
-  let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in
+  let lt,t = Reductionops.splay_lam (Global.env()) Evd.empty c in
   let lt = List.rev (List.map snd lt) in
   let args = snd (decompose_app t) in
   let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = 
@@ -234,7 +234,7 @@ let check_and_decompose_canonical_structure ref =
   let vc = match Environ.constant_opt_value env sp with
     | Some vc -> vc
     | None -> error_not_structure ref in
-  let body = snd (splay_lambda (Global.env()) Evd.empty vc) in
+  let body = snd (splay_lam (Global.env()) Evd.empty vc) in
   let f,args = match kind_of_term body with
     | App (f,args) -> f,args
     | _ -> error_not_structure ref in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4bb9a9a5dc..f51820bf62 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
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 371a66a9d5..edbb4f90ca 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -156,13 +156,13 @@ val hnf_lam_appvect  : env ->  evar_map -> constr -> constr array -> constr
 val hnf_lam_applist  : env ->  evar_map -> constr -> constr list -> constr
 
 val splay_prod : env ->  evar_map -> constr -> (name * constr) list * constr
-val splay_lambda : env ->  evar_map -> constr -> (name * constr) list * constr
+val splay_lam : env ->  evar_map -> constr -> (name * constr) list * constr
 val splay_arity : env ->  evar_map -> constr -> (name * constr) list * sorts
 val sort_of_arity : env -> constr -> sorts
-val decomp_n_prod : 
-  env ->  evar_map -> int -> constr -> Sign.rel_context * constr
+val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
+val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_prod_assum :
-  env ->  evar_map -> constr -> Sign.rel_context * constr
+  env ->  evar_map -> constr -> rel_context * constr
 val decomp_sort : env -> evar_map -> types -> sorts
 val is_sort : env -> evar_map -> types -> bool
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 418bb5d2f1..2c2bddb459 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -674,7 +674,7 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
            with Redelimination ->
              match reference_opt_value sigma env ref with
 	       | Some c ->
-		   (match kind_of_term (snd (decompose_lam c)) with 
+		   (match kind_of_term ((strip_lam c)) with 
                      | CoFix _ | Fix _ -> s
 		     | _ -> redrec (c, stack))
 	       | None -> s)
@@ -692,7 +692,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
     if isEvalRef env constr then
       match reference_opt_value sigma env (destEvalRef constr) with
 	| Some c ->
-	    (match kind_of_term (snd (decompose_lam c)) with 
+	    (match kind_of_term ((strip_lam c)) with 
               | CoFix _ | Fix _ -> s'
 	      | _ -> redrec (c, stack))
 	| None -> s'
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 24ab23f4ae..987db88b18 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -180,12 +180,6 @@ let new_sort_in_family = function
 
 
 
-(* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *)
-let prod_it ~init = List.fold_left (fun c (n,t)  -> mkProd (n, t, c)) init
-
-(* lam_it b [xn:Tn;..;x1:T1] = [x1:T1]..[xn:Tn]b *)
-let lam_it ~init = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) init
-
 (* [Rel (n+m);...;Rel(n+1)] *)
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
 
@@ -232,34 +226,30 @@ let rec lookup_rel_id id sign =
   in 
   lookrec (1,sign)
 
-(* Constructs either [(x:t)c] or [[x=b:t]c] *)
+(* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
 let mkProd_or_LetIn (na,body,t) c =
   match body with
     | None -> mkProd (na, t, c)
     | Some b -> mkLetIn (na, b, t, c)
 
-(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
+(* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *)
 let mkProd_wo_LetIn (na,body,t) c =
   match body with
     | None -> mkProd (na,  t, c)
     | Some b -> subst1 b c
 
-let it_mkProd_wo_LetIn ~init = 
-  List.fold_left (fun c d -> mkProd_wo_LetIn d c) init
-
-let it_mkProd_or_LetIn ~init = 
-  List.fold_left (fun c d -> mkProd_or_LetIn d c) init
-
-let it_mkLambda_or_LetIn ~init =
-  List.fold_left (fun c d -> mkLambda_or_LetIn d c) init
+let it_mkProd ~init = List.fold_left (fun c (n,t)  -> mkProd (n, t, c)) init
+let it_mkLambda ~init = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) init
 
 let it_named_context_quantifier f ~init = 
   List.fold_left (fun c d -> f d c) init
 
+let it_mkProd_or_LetIn = it_named_context_quantifier mkProd_or_LetIn
+let it_mkProd_wo_LetIn = it_named_context_quantifier mkProd_wo_LetIn
+let it_mkLambda_or_LetIn = it_named_context_quantifier mkLambda_or_LetIn
 let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn
-let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn
-
 let it_mkNamedProd_wo_LetIn = it_named_context_quantifier mkNamedProd_wo_LetIn
+let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn
 
 (* *)
 
@@ -794,9 +784,9 @@ let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
 let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
 
 let it_mkProd_or_LetIn_name env b hyps =
-  it_mkProd_or_LetIn b (name_context env hyps)
+  it_mkProd_or_LetIn ~init:b (name_context env hyps)
 let it_mkLambda_or_LetIn_name env b hyps =
-  it_mkLambda_or_LetIn b (name_context env hyps)
+  it_mkLambda_or_LetIn ~init:b (name_context env hyps)
 
 (*************************)
 (*   Names environments  *)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index ccdb980319..9163a1d9e5 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -35,27 +35,32 @@ val pr_rel_decl : env -> rel_declaration -> std_ppcmds
 val print_rel_context : env -> std_ppcmds
 val print_env : env -> std_ppcmds
 
-(* iterators on terms *)
-val prod_it : init:types -> (name * types) list -> types
-val lam_it : init:constr -> (name * types) list -> constr
-val rel_vect : int -> int -> constr array
-val rel_list : int -> int -> constr list
-val extended_rel_list : int -> rel_context -> constr list
-val extended_rel_vect : int -> rel_context -> constr array
+(* about contexts *)
 val push_rel_assum : name * types -> env -> env
 val push_rels_assum : (name * types) list -> env -> env
 val push_named_rec_types : name array * types array * 'a -> env -> env
 val lookup_rel_id : identifier -> rel_context -> int * types
+
+(* builds argument lists matching a block of binders or a context *)
+val rel_vect : int -> int -> constr array
+val rel_list : int -> int -> constr list
+val extended_rel_list : int -> rel_context -> constr list
+val extended_rel_vect : int -> rel_context -> constr array
+
+(* iterators/destructors on terms *)
 val mkProd_or_LetIn : rel_declaration -> types -> types
 val mkProd_wo_LetIn : rel_declaration -> types -> types
-val it_mkProd_wo_LetIn : init:types -> rel_context -> types
+val it_mkProd : init:types -> (name * types) list -> types
+val it_mkLambda : init:constr -> (name * types) list -> constr
 val it_mkProd_or_LetIn   : init:types -> rel_context -> types
+val it_mkProd_wo_LetIn : init:types -> rel_context -> types
 val it_mkLambda_or_LetIn : init:constr -> rel_context -> constr
-val it_named_context_quantifier :
-  (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a
 val it_mkNamedProd_or_LetIn   : init:types -> named_context -> types
-val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr
 val it_mkNamedProd_wo_LetIn   : init:types -> named_context -> types
+val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr
+
+val it_named_context_quantifier :
+  (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a
 
 (**********************************************************************)
 (* Generic iterators on constr                                        *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f7762afbeb..80d7d34a93 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -43,7 +43,7 @@ let abstract_scheme env c l lname_typ =
     lname_typ
 
 let abstract_list_all env evd typ c l =
-  let ctxt,_ = decomp_n_prod env (evars_of evd) (List.length l) typ in
+  let ctxt,_ = splay_prod_n env (evars_of evd) (List.length l) typ in
   let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in
   let p = abstract_scheme env c l_with_all_occs ctxt in 
   try