changed select so that it returns a list of pairs <number of binders crossed, term>

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index a3649ca36ed312874b333d39696a9a2c5bbf8ef0..289d6d9838595eeafb59c7c9624a0fea6dd97015 100644 (file)
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -174,43 +174,46 @@ let uri_of_term = function
   | _ -> raise (Invalid_argument "uri_of_term")
 
 let select ~term ~context =
-  let rec aux context term =
+  (* i is the number of binder traversed *) 
+  let rec aux i context term =
     match (context, term) with
-    | Cic.Implicit (Some `Hole), t -> [t]
+    | Cic.Implicit (Some `Hole), t -> [i,t]
     | Cic.Implicit None,_ -> []
     | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) ->
         List.concat
           (List.map2
             (fun t1 t2 ->
-              (match (t1, t2) with Some t1, Some t2 -> aux t1 t2 | _ -> []))
+              (match (t1, t2) with Some t1, Some t2 -> aux i t1 t2 | _ -> []))
             ctxt1 ctxt2)
-    | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux te1 te2 @ aux ty1 ty2
+    | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux i te1 te2 @ aux i ty1 ty2
     | Cic.Prod (_, s1, t1), Cic.Prod (_, s2, t2)
     | Cic.Lambda (_, s1, t1), Cic.Lambda (_, s2, t2)
-    | Cic.LetIn (_, s1, t1), Cic.LetIn (_, s2, t2) -> aux s1 s2 @ aux t1 t2
-    | Cic.Appl terms1, Cic.Appl terms2 -> auxs terms1 terms2
+    | Cic.LetIn (_, s1, t1), Cic.LetIn (_, s2, t2) -> 
+        aux i s1 s2 @ aux (i+1) t1 t2
+    | Cic.Appl terms1, Cic.Appl terms2 -> auxs i terms1 terms2
     | Cic.Var (_, subst1), Cic.Var (_, subst2)
     | Cic.Const (_, subst1), Cic.Const (_, subst2)
     | Cic.MutInd (_, _, subst1), Cic.MutInd (_, _, subst2)
     | Cic.MutConstruct (_, _, _, subst1), Cic.MutConstruct (_, _, _, subst2) ->
-        auxs (List.map snd subst1) (List.map snd subst2)
+        auxs i (List.map snd subst1) (List.map snd subst2)
     | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) ->
-        aux out1 out2 @ aux t1 t2 @ auxs pat1 pat2
+        aux i out1 out2 @ aux i t1 t2 @ auxs i pat1 pat2
     | Cic.Fix (_, funs1), Cic.Fix (_, funs2) ->
         List.concat
           (List.map2
-            (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> aux ty1 ty2 @ aux bo1 bo2)
+            (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> 
+              aux i ty1 ty2 @ aux i bo1 bo2)
             funs1 funs2)
     | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) ->
         List.concat
           (List.map2
-            (fun (_, ty1, bo1) (_, ty2, bo2) -> aux ty1 ty2 @ aux bo1 bo2)
+            (fun (_, ty1, bo1) (_, ty2, bo2) -> aux i ty1 ty2 @ aux i bo1 bo2)
             funs1 funs2)
     | _ -> assert false
-  and auxs terms1 terms2 =  (* as aux for list of terms *)
-    List.concat (List.map2 aux terms1 terms2)
+  and auxs i terms1 terms2 =  (* as aux for list of terms *)
+    List.concat (List.map2 (fun t1 t2 -> aux i t1 t2) terms1 terms2)
   in
-  aux context term
+  aux 0 context term
 
 let context_of ?(equality=(==)) ~term terms =
   let (===) x y = equality x y in
@@ -282,7 +285,6 @@ let attributes_of_obj = function
   | Cic.CurrentProof (_, _, _, _, _, attributes)
   | Cic.InductiveDefinition (_, _, _, attributes) ->
       attributes
-      
 let rec mk_rels howmany from =
   match howmany with 
   | 0 -> []

diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli
index a64a983f7c3033ca60afb792bc345fecec7e4828..60c14f8a6c03e5e0d9736a3a22c9275eda047ed0 100644 (file)
--- a/helm/ocaml/cic/cicUtil.mli
+++ b/helm/ocaml/cic/cicUtil.mli
@@ -67,8 +67,9 @@ val context_of:
     Cic.term
 
 (** select all subterms of a given term matching a given context (i.e. subtrees
-* rooted at context's holes *)
-val select: term:Cic.term -> context:Cic.term -> Cic.term list
+* rooted at context's holes. The first component is the number of binder the
+* term is below *)
+val select: term:Cic.term -> context:Cic.term -> (int * Cic.term) list
 
 (** mk_rels [howmany] [from] 
  * creates a list of [howmany] rels starting from [from] in decreasing order *)