Ajout fonctions sur les arités

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

1 files changed, 19 insertions, 0 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index de4d6cbce0..8b5b05679f 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -66,6 +66,8 @@ let print_sort = function
 
 type constr = sorts oper term
 
+type flat_arity = (name * constr) list * sorts
+
 type 'a judge = { body : constr; typ : 'a }
 
 (*
@@ -733,6 +735,23 @@ let prod_applist t nL = List.fold_left prod_app t nL
 
 (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
+let destArity = 
+  let rec prodec_rec l = function
+    | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) c
+    | DOP2(Cast,c,_)         -> prodec_rec l c
+    | DOP0(Sort s)           -> l,s
+    | _                      -> anomaly "decompose_arity: not an arity"
+  in 
+  prodec_rec [] 
+
+let rec isArity = function
+  | DOP2(Prod,_,DLAM(_,c)) -> isArity c
+  | DOP2(Cast,c,_)         -> isArity c
+  | DOP0(Sort _)           -> true
+  | _ -> false
+
+(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
+   ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
 let decompose_prod = 
   let rec prodec_rec l = function
     | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) c