Removing Termdn, and putting the relevant code in Btermdn. The current Termdn

file was useless and duplicated code from Btermdn itself.

5 files changed, 119 insertions, 205 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 1751d4138..b93be6fc2 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -18,11 +18,117 @@ open Globnames
 
 let dnet_depth = ref 8
 
+type term_label =
+| GRLabel of global_reference
+| ProdLabel
+| LambdaLabel
+| SortLabel
+
+let compare_term_label t1 t2 = match t1, t2 with
+| GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2
+| _ -> Pervasives.compare t1 t2 (** OK *)
+
+type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
+
+let decomp_pat =
+  let rec decrec acc = function
+    | PApp (f,args) -> decrec (Array.to_list args @ acc) f
+    | c -> (c,acc)
+  in
+  decrec []
+
+let decomp =
+  let rec decrec acc c = match kind_of_term c with
+    | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
+    | Cast (c1,_,_) -> decrec acc c1
+    | _ -> (c,acc)
+  in
+    decrec []
+
+let constr_val_discr t =
+  let c, l = decomp t in
+    match kind_of_term c with
+    | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l)
+    | Var id -> Label(GRLabel (VarRef id),l)
+    | Const _ -> Everything
+    | _ -> Nothing
+
+let constr_pat_discr t =
+  if not (Patternops.occur_meta_pattern t) then
+    None
+  else
+    match decomp_pat t with
+    | PRef ((IndRef _) as ref), args
+    | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
+    | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args)
+    | _ -> None
+
+let constr_val_discr_st (idpred,cpred) t =
+  let c, l = decomp t in
+    match kind_of_term c with
+    | Const c -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l)
+    | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l)
+    | Var id when not (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l)
+    | Prod (n, d, c) -> Label(ProdLabel, [d; c])
+    | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l)
+    | Sort _ -> Label(SortLabel, [])
+    | Evar _ -> Everything
+    | _ -> Nothing
+
+let constr_pat_discr_st (idpred,cpred) t =
+  match decomp_pat t with
+  | PRef ((IndRef _) as ref), args
+  | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
+  | PRef ((VarRef v) as ref), args when not (Id.Pred.mem v idpred) ->
+      Some(GRLabel ref,args)
+  | PVar v, args when not (Id.Pred.mem v idpred) ->
+      Some(GRLabel (VarRef v),args)
+  | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) ->
+      Some (GRLabel ref, args)
+  | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
+  | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l)
+  | PSort s, [] -> Some (SortLabel, [])
+  | _ -> None
+
+let bounded_constr_pat_discr_st st (t,depth) =
+  if Int.equal depth 0 then
+    None
+  else
+    match constr_pat_discr_st st t with
+      | None -> None
+      | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+
+let bounded_constr_val_discr_st st (t,depth) =
+  if Int.equal depth 0 then
+    Nothing
+  else
+    match constr_val_discr_st st t with
+      | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l)
+      | Nothing -> Nothing
+      | Everything -> Everything
+
+let bounded_constr_pat_discr (t,depth) =
+  if Int.equal depth 0 then
+    None
+  else
+    match constr_pat_discr t with
+      | None -> None
+      | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+
+let bounded_constr_val_discr (t,depth) =
+  if Int.equal depth 0 then
+    Nothing
+  else
+    match constr_val_discr t with
+      | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l)
+      | Nothing -> Nothing
+      | Everything -> Everything
 
 module Make =
   functor (Z : Map.OrderedType) ->
 struct
-  open Termdn
 
   module X = struct
     type t = constr_pattern*int
@@ -34,79 +140,12 @@ struct
     let compare = compare_term_label
  end
 
- type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
-
  module Dn = Dn.Make(X)(Y)(Z)
 
  type t = Dn.t
 
   let create = Dn.create
 
-  let decomp =
-    let rec decrec acc c = match kind_of_term c with
-      | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
-      | Cast (c1,_,_) -> decrec acc c1
-      | _ -> (c,acc)
-    in
-      decrec []
-
-  let constr_val_discr t =
-    let c, l = decomp t in
-      match kind_of_term c with
-      | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l)
-      | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l)
-      | Var id -> Label(GRLabel (VarRef id),l)
-      | Const _ -> Everything
-      | _ -> Nothing
-
-  let constr_val_discr_st (idpred,cpred) t =
-    let c, l = decomp t in
-      match kind_of_term c with
-      | Const c -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l)
-      | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l)
-      | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l)
-      | Var id when not (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l)
-      | Prod (n, d, c) -> Label(ProdLabel, [d; c])
-      | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l)
-      | Sort _ -> Label(SortLabel, [])
-      | Evar _ -> Everything
-      | _ -> Nothing
-
-  let bounded_constr_pat_discr_st st (t,depth) =
-    if Int.equal depth 0 then
-      None
-    else
-      match constr_pat_discr_st st t with
-	| None -> None
-	| Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
-
-  let bounded_constr_val_discr_st st (t,depth) =
-    if Int.equal depth 0 then
-      Nothing
-    else
-      match constr_val_discr_st st t with
-	| Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l)
-	| Nothing -> Nothing
-	| Everything -> Everything
-
-  let bounded_constr_pat_discr (t,depth) =
-    if Int.equal depth 0 then
-      None
-    else
-      match constr_pat_discr t with
-	| None -> None
-	| Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
-
-  let bounded_constr_val_discr (t,depth) =
-    if Int.equal depth 0 then
-      Nothing
-    else
-      match constr_val_discr t with
-	| Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l)
-	| Nothing -> Nothing
-	| Everything -> Everything
-
-
   let add = function
     | None ->
 	(fun dn (c,v) ->
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index fedc68047..575502026 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -11,6 +11,18 @@ open Pattern
 open Names
 
 (** Discrimination nets with bounded depth. *)
+
+(** 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. The [transparent_state]
+indicates which constants and variables can be considered as rigid.
+These dnets are able to cope with existential variables as well, which match
+[Everything]. *)
+
 module Make :
   functor (Z : Map.OrderedType) ->
 sig
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index a4de9e2b4..27ded2357 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,6 +1,5 @@
 Geninterp
 Dn
-Termdn
 Btermdn
 Tacticals
 Hipattern
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
deleted file mode 100644
index 7eff2909f..000000000
--- a/tactics/termdn.ml
+++ /dev/null
@@ -1,92 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Util
-open Names
-open Term
-open Pattern
-open Patternops
-open Globnames
-
-type term_label =
-| GRLabel of global_reference
-| ProdLabel
-| LambdaLabel
-| SortLabel
-
-let compare_term_label t1 t2 = match t1, t2 with
-| GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2
-| _ -> Pervasives.compare t1 t2 (** OK *)
-
-type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
-
-(*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*)
-
-let decomp =
-  let rec decrec acc c = match kind_of_term c with
-    | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
-    | Cast (c1,_,_) -> decrec acc c1
-    | _ -> (c,acc)
-  in
-  decrec []
-
-let decomp_pat =
-  let rec decrec acc = function
-    | PApp (f,args) -> decrec (Array.to_list args @ acc) f
-    | c -> (c,acc)
-  in
-  decrec []
-
-let constr_pat_discr t =
-  if not (occur_meta_pattern t) then
-    None
-  else
-    match decomp_pat t with
-    | PRef ((IndRef _) as ref), args
-    | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
-    | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args)
-    | _ -> None
-
-let constr_pat_discr_st (idpred,cpred) t =
-  match decomp_pat t with
-  | PRef ((IndRef _) as ref), args
-  | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
-  | PRef ((VarRef v) as ref), args when not (Id.Pred.mem v idpred) ->
-      Some(GRLabel ref,args)
-  | PVar v, args when not (Id.Pred.mem v idpred) ->
-      Some(GRLabel (VarRef v),args)
-  | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) ->
-      Some (GRLabel ref, args)
-  | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
-  | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l)
-  | PSort s, [] -> Some (SortLabel, [])
-  | _ -> None
-
-open Dn
-
-let constr_val_discr t =
-  let c, l = decomp t in
-    match kind_of_term c with
-    | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l)
-    | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l)
-    | Var id -> Label(GRLabel (VarRef id),l)
-    | Const _ -> Everything
-    | _ -> Nothing
-
-let constr_val_discr_st (idpred,cpred) t =
-  let c, l = decomp t in
-    match kind_of_term c with
-    | Const c -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l)
-    | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l)
-    | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l)
-    | Var id when not (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l)
-    | Prod (n, d, c) -> Label(ProdLabel, [d; c])
-    | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l)
-    | Sort _ -> Label (SortLabel, [])
-    | Evar _ -> Everything
-    | _ -> Nothing
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
deleted file mode 100644
index 16be2e1c9..000000000
--- a/tactics/termdn.mli
+++ /dev/null
@@ -1,44 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Term
-open Pattern
-open Globnames
-open Names
-
-type term_label =
-| GRLabel of global_reference
-| ProdLabel
-| LambdaLabel
-| SortLabel
-
-val compare_term_label : term_label -> term_label -> int
-
-(** Discrimination nets of terms. *)
-
-(** 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. The [transparent_state]
-indicates which constants and variables can be considered as rigid.
-These dnets are able to cope with existential variables as well, which match
-[Everything]. *)
-
-(**/**)
-(** These are for Nbtermdn *)
-
-val constr_pat_discr_st : transparent_state ->
-  constr_pattern -> (term_label * constr_pattern list) option
-val constr_val_discr_st : transparent_state ->
-  constr -> (term_label * constr list) Dn.lookup_res
-
-val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option
-val constr_val_discr : constr -> (term_label * constr list) Dn.lookup_res