- répertoire tactics/

 - discrimination nets (début) : modules Tlm et Dn


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

3 files changed, 115 insertions, 0 deletions

diff --git a/tactics/dn.ml b/tactics/dn.ml
new file mode 100644
index 000000000..cc811735a
--- /dev/null
+++ b/tactics/dn.ml
@@ -0,0 +1,79 @@
+
+(* $Id$ *)
+
+(* This file implements the basic structure of what Chet called
+   ``discrimination nets''. If my understanding is wright, 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
+   (only) to implement the tactics Auto, DHyp and Point.
+
+   A discrimination net is a tries structure, that is, a tree structure 
+   specially conceived for searching patterns, like for example strings
+   --see the file Tlm.ml in the directory lib/util--. Here the tries
+   structure are used for looking for term patterns.
+
+   This module is then used in :
+     - termdn.ml   (discrimination nets of terms);
+     - btermdn.ml  (discrimination nets of terms with bounded depth,
+                    used in the tactic auto);
+     - nbtermdn.ml (named discrimination nets with bounded depth, used
+                    in the tactics Dhyp and Point).
+  Eduardo (4/8/97) *)
+
+(* Definition of the basic structure *)
+
+type ('lbl,'pat) dn_args = 'pat -> ('lbl * 'pat list) option
+
+type ('lbl,'pat,'inf) under_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 dna = {tm = Tlm.create(); args = dna}
+
+let path_of dna =
+  let rec path_of_deferred = function
+    | [] -> []
+    | h::tl -> pathrec tl h
+	    
+  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)
+  in 
+  pathrec []
+    
+let tm_of tm lbl =
+  try [Tlm.map tm lbl] with Not_found -> []
+
+let lookup dnm 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)
+    in 
+  List.flatten(List.map Tlm.xtract (lookrec t dnm.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 rmv dnm (pat,inf) =
+  upd dnm
+    (fun dna tm ->
+       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
diff --git a/tactics/dn.mli b/tactics/dn.mli
new file mode 100644
index 000000000..211b75a36
--- /dev/null
+++ b/tactics/dn.mli
@@ -0,0 +1,25 @@
+
+(* $Id$ *)
+
+(* Discrimination nets. *)
+
+type ('lbl,'pat) dn_args = 'pat -> ('lbl * 'pat list) option
+
+type ('lbl,'pat,'inf) t = {
+  tm : (('lbl * int) option,'pat * 'inf) Tlm.t;
+  args : ('lbl,'pat) dn_args }
+
+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 rmv : ('lbl,'pat,'inf) t -> 'pat * 'inf -> ('lbl,'pat,'inf) t
+
+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 app : (('pat * 'inf) -> unit) -> ('lbl,'pat,'inf) t -> unit
diff --git a/tactics/doc.tex b/tactics/doc.tex
new file mode 100644
index 000000000..d44cc14a5
--- /dev/null
+++ b/tactics/doc.tex
@@ -0,0 +1,11 @@
+
+\newpage
+\section*{The Tactics}
+
+\ocwsection \label{tactics}
+This chapter describes the \Coq\ main tactics.
+The modules of that chapter are organized as follows.
+
+\bigskip
+\begin{center}\epsfig{file=tactics.dep.ps,width=\linewidth}\end{center}
+