Nettoyage

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

5 files changed, 75 insertions, 60 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 3015e651b..e6a4b43dd 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -26,27 +26,18 @@ let bounded_constr_val_discr (t,depth) =
       | None -> None
       | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
 
-type 'a t = (lbl,constr * int,'a) Dn.under_t
+type 'a t = (lbl,constr * int,'a) Dn.t
 
-let newdn () = Dn.create bounded_constr_pat_discr
+let create = Dn.create
 
-let ex_termdn = newdn()
+let add dn (c,v) = Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)
 
-let inDN tdn = { 
-  Dn.args = ex_termdn.Dn.args;
-  Dn.tm = tdn }
+let rmv dn (c,v) = Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v)
 
-let outDN dn = dn.Dn.tm
-
-let create () = outDN (newdn())
-
-let add dn (c,v) = outDN (Dn.add (inDN dn) ((c,!dnet_depth),v))
-
-let rmv dn (c,v) = outDN (Dn.rmv (inDN dn) ((c,!dnet_depth),v))
-
-let lookup dn t = 
+let lookup dn t =
   List.map 
     (fun ((c,_),v) -> (c,v)) 
-    (Dn.lookup (inDN dn) bounded_constr_val_discr (t,!dnet_depth))
+    (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth))
+
+let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn
 
-let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) (inDN dn)
diff --git a/tactics/dn.ml b/tactics/dn.ml
index 33ce0df5d..b53fb2661 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 (* This file implements the basic structure of what Chet called
-   ``discrimination nets''. If my understanding is wright, it serves
+   ``discrimination nets''. If my understanding is right, it serves
    to associate actions (for example, tactics) with a priority to term
    patterns, so that if a hypothesis matches a pattern in the net,
    then the associated tactic is applied. Discrimination nets are used
@@ -23,15 +23,14 @@
 
 (* Definition of the basic structure *)
 
-type ('lbl,'pat) dn_args = 'pat -> ('lbl * 'pat list) option
+type ('lbl,'pat) decompose_fun = 'pat -> ('lbl * 'pat list) option
 
-type ('lbl,'pat,'inf) under_t = (('lbl * int) option,'pat * 'inf) Tlm.t
+type ('lbl,'pat,'inf) t = (('lbl * int) option,'pat * 'inf) Tlm.t
 
-type ('lbl,'pat,'inf) t = {
-  tm   : ('lbl,'pat,'inf) under_t; 
-  args : ('lbl,'pat) dn_args }
+let create () = Tlm.empty
 
-let create dna = { tm = Tlm.empty; args = dna }
+(* [path_of dna pat] returns the list of nodes of the pattern [pat] read in 
+prefix ordering, [dna] is the function returning the main node of a pattern *)
 
 let path_of dna =
   let rec path_of_deferred = function
@@ -52,28 +51,23 @@ let path_of dna =
 let tm_of tm lbl =
   try [Tlm.map tm lbl] with Not_found -> []
 
-let lookup dnm dna' t =
+let lookup tm dna t =
   let rec lookrec t tm =
     (tm_of tm None)@
-    (match dna' t with
+    (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)
   in 
-  List.flatten(List.map Tlm.xtract (lookrec t dnm.tm))
+  List.flatten(List.map Tlm.xtract (lookrec t tm))
 
-let upd dnm f = { args = dnm.args; tm = f dnm.args dnm.tm }
-
-let add dnm (pat,inf) =
-  upd dnm
-    (fun dna tm ->
-       let p = path_of dna pat in Tlm.add tm (p,(pat,inf)))
+let add tm dna (pat,inf) =
+  let p = path_of dna pat in Tlm.add tm (p,(pat,inf))
     
-let rmv dnm (pat,inf) =
-  upd dnm
-    (fun dna tm ->
-       let p = path_of dna pat in Tlm.rmv tm (p,(pat,inf)))
+let rmv tm dna (pat,inf) =
+  let p = path_of dna pat in Tlm.rmv tm (p,(pat,inf))
     
-let app f dnm = Tlm.app (fun (_,p) -> f p) dnm.tm
+let app f tm = Tlm.app (fun (_,p) -> f p) tm
+
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 211b75a36..42c6303a0 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -3,23 +3,31 @@
 
 (* Discrimination nets. *)
 
-type ('lbl,'pat) dn_args = 'pat -> ('lbl * 'pat list) option
+type ('lbl,'tree) decompose_fun = 'tree -> ('lbl * 'tree list) option
 
-type ('lbl,'pat,'inf) t = {
-  tm : (('lbl * int) option,'pat * 'inf) Tlm.t;
-  args : ('lbl,'pat) dn_args }
+type ('lbl,'pat,'inf) t (* = (('lbl * int) option,'pat * 'inf) Tlm.t *)
 
-type ('lbl,'pat,'inf) under_t = (('lbl * int) option,'pat * 'inf) Tlm.t
-				  
-val create : ('lbl,'pat) dn_args -> ('lbl,'pat,'inf) t
-    
-val add : ('lbl,'pat,'inf) t -> 'pat * 'inf -> ('lbl,'pat,'inf) t
+val create : unit -> ('lbl,'pat,'inf) t
 
-val rmv : ('lbl,'pat,'inf) t -> 'pat * 'inf -> ('lbl,'pat,'inf) t
+(* [add t f (tree,inf)] adds a structured object [tree] together with
+   the associated information [inf] to the table [t]; the function
+   [f] is used to translated [tree] into its prefix decomposition: [f]
+   must decompose any tree into a label characterizing its root node and
+   the list of its subtree *)
 
-val path_of : ('lbl,'pat) dn_args -> 'pat -> ('lbl * int) option list
-    
-val lookup : 
-  ('lbl,'pat,'inf) t -> ('lbl,'term) dn_args -> 'term -> ('pat * 'inf) list
+val add : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf
+  -> ('lbl,'pat,'inf) t
+
+val rmv : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf 
+  -> ('lbl,'pat,'inf) t
+
+(* [lookup t f tree] looks for trees (and their associated
+   information) in table [t] such that the structured object [tree]
+   matches against them; [f] is used to translated [tree] into its
+   prefix decomposition: [f] must decompose any tree into a label
+   characterizing its root node and the list of its subtree *)
+
+val lookup : ('lbl,'pat,'inf) t -> ('lbl,'term) decompose_fun -> 'term
+  -> ('pat * 'inf) list
 
 val app : (('pat * 'inf) -> unit) -> ('lbl,'pat,'inf) t -> unit
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index f1f8374c9..fda033f26 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -26,6 +26,7 @@ let decomp =
   in 
   decrec []   
 
+
 let constr_pat_discr t =
   if not(occur_meta t) then 
     None
@@ -58,10 +59,11 @@ let constr_val_discr_nil t =
     | None -> None
     | Some (c,_) -> Some(c,[])
 
-let create () = Dn.create constr_pat_discr
+let create = Dn.create 
+
+let add dn = Dn.add dn constr_pat_discr
 
-let add = Dn.add
-let rmv = Dn.rmv
+let rmv dn = Dn.rmv dn constr_pat_discr
 
 let lookup dn t = Dn.lookup dn constr_val_discr t
 
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 95cfc6243..62066f604 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -8,20 +8,40 @@ open Term
   
 (* Discrimination nets of terms. *)
 
-type lbl =
-  | TERM of constr
-  | DOPER of sorts oper
-  | DLAMBDA
+(* This module registers actions (typically tactics) mapped to patterns *)
+
+(* Patterns are stocked linearly as the list of its node in prefix
+order in such a way patterns having the same prefix have this common
+prefix shared and the seek for the action associated to the patterns
+that a term matches are found in time proportional to the maximal
+number of nodes of the patterns matching the term *)
 
-type 'a t = (lbl,constr,'a) Dn.t
+type 'a t
 
 val create : unit -> 'a t
 
+(* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *)
+
 val add : 'a t -> (constr * 'a) -> 'a t
+
 val rmv : 'a t -> (constr * 'a) -> 'a t
 
+(* [lookup t c] looks for patterns (with their action) matching term [c] *)
+
 val lookup : 'a t -> constr -> (constr * 'a) list
+
 val app : ((constr * 'a) -> unit) -> 'a t -> unit
 
+
+(*i*)
+(* These are for Nbtermdn *)
+
+type lbl =
+  | TERM of constr
+  | DOPER of sorts oper
+  | DLAMBDA
+
 val constr_pat_discr : constr -> (lbl * constr list) option
 val constr_val_discr : constr -> (lbl * constr list) option
+
+(*i*)