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

[helm.git] / helm / ocaml / cic / cicUtil.ml

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 -> []