Retrait des lam_and_pop and co; ajout d'un destructeur 'lispien' de constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@497 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 66 insertions, 3 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index e97a2b2193..27f7d7a11c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -802,7 +802,7 @@ let nb_prod =
   in 
   nbrec 0
 
-
+(* Trop compliqué...
 (********************************************************************)
 (*   various utility functions for implementing terms with bindings *)
 (********************************************************************)
@@ -933,6 +933,7 @@ let lambda_ize n t endpt =
   match lam_and_popl n env t [] with
     | (_,t,[]) -> t
     | _ -> anomaly "bud in Term.lamda_ize"
+*)
 	  
 let sort_hdchar = function
   | Prop(_) -> "P"
@@ -1672,3 +1673,51 @@ let sub_term_with_unif cref ceq=
           None
         else
           Some ((subst_with_lmeta l ceq),nb)
+
+type constr_operator =
+  | OpMeta of int
+  | OpSort of sorts
+  | OpRel of int | OpVar of identifier
+  | OpCast | OpProd of name | OpLambda of name
+  | OpAppL | OpConst of section_path | OpAbst of section_path
+  | OpEvar of existential_key
+  | OpMutInd of inductive_path
+  | OpMutConstruct of constructor_path
+  | OpMutCase of case_info
+  | OpRec of fix_kind
+
+let splay_constr = function
+  | Rel n                            -> OpRel n, []
+  | VAR id                           -> OpVar id, [] 
+  | DOP0 (Meta n)                    -> OpMeta n, []
+  | DOP0 (Sort s)                    -> OpSort s, []
+  | DOP2 (Cast, t1, t2)              -> OpCast, [t1;t2]
+  | DOP2 (Prod, t1, (DLAM (x,t2)))   -> OpProd x, [t1;t2]
+  | DOP2 (Lambda, t1, (DLAM (x,t2))) -> OpLambda x, [t1;t2]
+  | DOPN (AppL,a)                 -> OpAppL, Array.to_list a
+  | DOPN (Const sp, a)            -> OpConst sp, Array.to_list a
+  | DOPN (Evar sp, a)             -> OpEvar sp, Array.to_list a
+  | DOPN (MutInd ind_sp, l)       -> OpMutInd ind_sp, Array.to_list l
+  | DOPN (MutConstruct cstr_sp,l) -> OpMutConstruct cstr_sp, Array.to_list l
+  | DOPN (MutCase ci,v)           -> OpMutCase ci, Array.to_list v
+  | DOPN ((Fix (f,i),a))          -> OpRec (RFix (f,i)), Array.to_list a
+  | DOPN ((CoFix i),a)            -> OpRec (RCofix i), Array.to_list a
+  | _ -> errorlabstrm "Term.splay_term" [< 'sTR "ill-formed constr" >]
+
+let gather_constr = function
+  | OpRel n, []  -> Rel n
+  | OpVar id, [] -> VAR id
+  | OpMeta n, [] -> DOP0 (Meta n)
+  | OpSort s, [] -> DOP0 (Sort s)
+  | OpCast, [t1;t2]     -> DOP2 (Cast, t1, t2)
+  | OpProd x, [t1;t2]   -> DOP2 (Prod, t1, (DLAM (x,t2)))
+  | OpLambda x, [t1;t2] -> DOP2 (Lambda, t1, (DLAM (x,t2))) 
+  | OpAppL, a     -> DOPN (AppL,Array.of_list a)
+  | OpConst sp, a -> DOPN (Const sp,Array.of_list a)
+  | OpEvar sp, a  -> DOPN (Evar sp, Array.of_list a) 
+  | OpMutInd ind_sp, l        -> DOPN (MutInd ind_sp, Array.of_list l) 
+  | OpMutConstruct cstr_sp, l -> DOPN (MutConstruct cstr_sp,Array.of_list l)
+  | OpMutCase ci,  v    -> DOPN (MutCase ci,Array.of_list v)   
+  | OpRec (RFix (f,i)), a  -> DOPN ((Fix (f,i),Array.of_list a))
+  | OpRec (RCofix i), a -> DOPN ((CoFix i),Array.of_list a) 
+  | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed constr" >]
diff --git a/kernel/term.mli b/kernel/term.mli
index 69bd7d644f..bfeccb0c72 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -428,7 +428,7 @@ val nb_lam : constr -> int
 (* similar to [nb_lam], but gives the number of products instead *)
 val nb_prod : constr -> int
 
-
+(* Trop compliqué
 (*s Various utility functions for implementing terms with bindings. *)
 
 val extract_lifted : int * constr -> constr
@@ -502,7 +502,7 @@ val lam_and_popl_named :
    properly lifted, and then push back the products, but as lambda-
    abstractions *)
 val lambda_ize : int ->'a oper term -> 'a oper term -> 'a oper term
-
+*)
 
 (*s Flattening and unflattening of embedded applications and casts. *)
 
@@ -573,6 +573,20 @@ val subst_term_occ : int list -> constr -> constr -> constr
 
 val subst_meta : (int * constr) list -> constr -> constr
 
+type constr_operator =
+  | OpMeta of int
+  | OpSort of sorts
+  | OpRel of int | OpVar of identifier
+  | OpCast | OpProd of name | OpLambda of name
+  | OpAppL | OpConst of section_path | OpAbst of section_path
+  | OpEvar of existential_key
+  | OpMutInd of inductive_path
+  | OpMutConstruct of constructor_path
+  | OpMutCase of case_info
+  | OpRec of fix_kind
+
+val splay_constr : constr -> constr_operator * constr list
+val gather_constr : constr_operator * constr list -> constr
 
 (*s Hash-consing functions for constr. *)