Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

1 files changed, 37 insertions, 17 deletions

diff --git a/tactics/dn.ml b/tactics/dn.ml
index ab908ff9..2a8166dc 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dn.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: dn.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 (* This file implements the basic structure of what Chet called
    ``discrimination nets''. If my understanding is right, it serves
@@ -32,6 +33,10 @@
 
 type ('lbl,'pat) decompose_fun = 'pat -> ('lbl * 'pat list) option
 
+type 'res lookup_res = Label of 'res | Nothing | Everything
+    
+type ('lbl,'tree) lookup_fun = 'tree -> ('lbl * 'tree list) lookup_res
+
 type ('lbl,'pat,'inf) t = (('lbl * int) option,'pat * 'inf) Tlm.t
 
 let create () = Tlm.empty
@@ -46,29 +51,44 @@ let path_of dna =
 	    
   and pathrec deferred t =
     match dna t with
-      | None -> 
-	  None :: (path_of_deferred deferred)
-      | Some (lbl,[]) ->
-	  (Some (lbl,0))::(path_of_deferred deferred)
-      | Some (lbl,(h::def_subl as v)) ->
-	  (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
+    | None -> 
+	None :: (path_of_deferred deferred)
+    | Some (lbl,[]) ->
+	(Some (lbl,0))::(path_of_deferred deferred)
+    | Some (lbl,(h::def_subl as v)) ->
+	(Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
   in 
   pathrec []
     
 let tm_of tm lbl =
-  try [Tlm.map tm lbl] with Not_found -> []
-
+  try [Tlm.map tm lbl, true] with Not_found -> []
+    
+let rec skip_arg n tm =
+  if n = 0 then [tm,true]
+  else
+    List.flatten 
+      (List.map 
+	  (fun a -> match a with
+	  | None -> skip_arg (pred n) (Tlm.map tm a)
+	  | Some (lbl,m) -> 
+	      skip_arg (pred n + m) (Tlm.map tm a)) 
+	  (Tlm.dom tm))
+      
 let lookup tm dna t =
   let rec lookrec t tm =
-    (tm_of tm None)@
-    (match dna t with
-       | None -> []
-       | Some(lbl,v) ->
-	   List.fold_left 
-	     (fun l c -> List.flatten(List.map (lookrec c) l))
-             (tm_of tm (Some(lbl,List.length v))) v)
+    match dna t with
+    | Nothing -> tm_of tm None
+    | Label(lbl,v) ->
+	tm_of tm None@
+	  (List.fold_left 
+	      (fun l c -> 
+		List.flatten(List.map (fun (tm, b) ->
+		  if b then lookrec c tm
+		  else [tm,b]) l))
+              (tm_of tm (Some(lbl,List.length v))) v)
+    | Everything -> skip_arg 1 tm
   in 
-  List.flatten(List.map Tlm.xtract (lookrec t tm))
+    List.flatten (List.map (fun (tm,b) -> Tlm.xtract tm) (lookrec t tm))
 
 let add tm dna (pat,inf) =
   let p = path_of dna pat in Tlm.add tm (p,(pat,inf))