Moving Dnet-related code to tactics/.

3 files changed, 0 insertions, 477 deletions

diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 469be6d9ea..a4c72f4828 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -11,7 +11,6 @@ Cbv
 Pretype_errors
 Evarutil
 Evarsolve
-Term_dnet
 Recordops
 Evarconv
 Arguments_renaming
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
deleted file mode 100644
index e05f4bcfe8..0000000000
--- a/pretyping/term_dnet.ml
+++ /dev/null
@@ -1,388 +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        *)
-(************************************************************************)
-
-(*i*)
-open Util
-open Term
-open Names
-open Globnames
-open Mod_subst
-open Pp (* debug *)
-(*i*)
-
-
-(* Representation/approximation of terms to use in the dnet:
- *
- * - no meta or evar (use ['a pattern] for that)
- *
- * - [Rel]s and [Sort]s are not taken into account (that's why we need
- *   a second pass of linear filterin on the results - it's not a perfect
- *   term indexing structure)
-
- * - Foralls and LetIns are represented by a context DCtx (a list of
- *   generalization, similar to rel_context, and coded with DCons and
- *   DNil). This allows for matching under an unfinished context
- *)
-
-module DTerm =
-struct
-
-  type 't t =
-    | DRel
-    | DSort
-    | DRef    of global_reference
-    | DCtx    of 't * 't (* (binding list, subterm) = Prods and LetIns *)
-    | DLambda of 't * 't
-    | DApp    of 't * 't (* binary app *)
-    | DCase   of case_info * 't * 't * 't array
-    | DFix    of int array * int * 't array * 't array
-    | DCoFix  of int * 't array * 't array
-
-    (* special constructors only inside the left-hand side of DCtx or
-       DApp. Used to encode lists of foralls/letins/apps as contexts *)
-    | DCons   of ('t * 't option) * 't
-    | DNil
-
-  (* debug *)
-  let pr_dconstr f : 'a t -> std_ppcmds = function
-    | DRel -> str "*"
-    | DSort -> str "Sort"
-    | DRef _ -> str "Ref"
-    | DCtx (ctx,t) -> f ctx ++ spc() ++ str "|-" ++ spc () ++ f t
-    | DLambda (t1,t2) -> str "fun"++ spc() ++ f t1 ++ spc() ++ str"->" ++ spc() ++ f t2
-    | DApp (t1,t2) -> f t1 ++ spc() ++ f t2
-    | DCase (_,t1,t2,ta) -> str "case"
-    | DFix _ -> str "fix"
-    | DCoFix _ -> str "cofix"
-    | DCons ((t,dopt),tl) -> f t ++ (match dopt with
-	  Some t' -> str ":=" ++ f t'
-	| None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl
-    | DNil -> str "[]"
-
-  (*
-   * Functional iterators for the t datatype
-   * a.k.a boring and error-prone boilerplate code
-   *)
-
-  let map f = function
-    | (DRel | DSort | DNil | DRef _) as c -> c
-    | DCtx (ctx,c) -> DCtx (f ctx, f c)
-    | DLambda (t,c) -> DLambda (f t, f c)
-    | DApp (t,u) -> DApp (f t,f u)
-    | DCase (ci,p,c,bl) -> DCase (ci, f p, f c, Array.map f bl)
-    | DFix (ia,i,ta,ca) ->
-	DFix (ia,i,Array.map f ta,Array.map f ca)
-    | DCoFix(i,ta,ca) ->
-	DCoFix (i,Array.map f ta,Array.map f ca)
-    | DCons ((t,topt),u) -> DCons ((f t,Option.map f topt), f u)
-
-  let compare_ci ci1 ci2 =
-    let c = ind_ord ci1.ci_ind ci2.ci_ind in
-    if c = 0 then
-      let c = Int.compare ci1.ci_npar ci2.ci_npar in
-      if c = 0 then
-        let c = Array.compare Int.compare ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls in
-        if c = 0 then
-          Array.compare Int.compare ci1.ci_cstr_nargs ci2.ci_cstr_nargs
-        else c
-      else c
-    else c
-
-  let compare cmp t1 t2 = match t1, t2 with
-  | DRel, DRel -> 0
-  | DSort, DSort -> 0
-  | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2
-  | DCtx (tl1, tr1), DCtx (tl2, tr2)
-  | DLambda (tl1, tr1), DCtx (tl2, tr2)
-  | DApp (tl1, tr1), DCtx (tl2, tr2) ->
-    let c = cmp tl1 tl2 in
-    if c = 0 then cmp tr1 tr2 else c
-
-  | DCase (ci1, c1, t1, p1), DCase (ci2, c2, t2, p2) ->
-    let c = cmp c1 c2 in
-    if c = 0 then
-      let c = cmp t1 t2 in
-      if c = 0 then
-        let c = Array.compare cmp p1 p2 in
-        if c = 0 then compare_ci ci1 ci2
-        else c
-      else c
-    else c
-
-  | DFix (i1, j1, tl1, pl1), DFix (i2, j2, tl2, pl2) ->
-    let c = Int.compare j1 j2 in
-    if c = 0 then
-      let c = Array.compare Int.compare i1 i2 in
-      if c = 0 then
-        let c = Array.compare cmp tl1 tl2 in
-        if c = 0 then Array.compare cmp pl1 pl2
-        else c
-      else c
-    else c
-  | DCoFix (i1, tl1, pl1), DCoFix (i2, tl2, pl2) ->
-    let c = Int.compare i1 i2 in
-    if c = 0 then
-      let c = Array.compare cmp tl1 tl2 in
-      if c = 0 then Array.compare cmp pl1 pl2
-      else c
-    else c
-  | _ -> Pervasives.compare t1 t2 (** OK **)
-
-  let fold f acc = function
-    | (DRel | DNil | DSort | DRef _) -> acc
-    | DCtx (ctx,c) -> f (f acc ctx) c
-    | DLambda (t,c) -> f (f acc t) c
-    | DApp (t,u) -> f (f acc t) u
-    | DCase (ci,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
-    | DFix (ia,i,ta,ca) ->
-	Array.fold_left f (Array.fold_left f acc ta) ca
-    | DCoFix(i,ta,ca) ->
-	Array.fold_left f (Array.fold_left f acc ta) ca
-    | DCons ((t,topt),u) -> f (Option.fold_left f (f acc t) topt) u
-
-  let choose f = function
-    | (DRel | DSort | DNil | DRef _) -> invalid_arg "choose"
-    | DCtx (ctx,c) -> f ctx
-    | DLambda (t,c) -> f t
-    | DApp (t,u) -> f u
-    | DCase (ci,p,c,bl) -> f c
-    | DFix (ia,i,ta,ca) -> f ta.(0)
-    | DCoFix (i,ta,ca) -> f ta.(0)
-    | DCons ((t,topt),u) -> f u
-
-  let dummy_cmp () () = 0
-
-  let fold2 (f:'a -> 'b -> 'c -> 'a) (acc:'a) (c1:'b t) (c2:'c t) : 'a =
-    let head w = map (fun _ -> ()) w in
-    if not (Int.equal (compare dummy_cmp (head c1) (head c2)) 0)
-    then invalid_arg "fold2:compare" else
-      match c1,c2 with
-	| (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _) -> acc
-	| (DCtx (c1,t1), DCtx (c2,t2)
-	  | DApp (c1,t1), DApp (c2,t2)
-	  | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2
-	| DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) ->
-	    Array.fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2
-	| DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
-	    Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
-	| DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) ->
-	    Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
-	| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
-	    f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2
-	| _ -> assert false
-
-  let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t =
-    let head w = map (fun _ -> ()) w in
-    if not (Int.equal (compare dummy_cmp (head c1) (head c2)) 0)
-    then invalid_arg "map2_t:compare" else
-      match c1,c2 with
-	| (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _) as cc ->
-	    let (c,_) = cc in c
-	| DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2)
-	| DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2)
-	| DApp (t1,u1), DApp (t2,u2) -> DApp (f t1 t2,f u1 u2)
-	| DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) ->
-	    DCase (ci, f p1 p2, f c1 c2, Array.map2 f bl1 bl2)
-	| DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
-	    DFix (ia,i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
-	| DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) ->
-	    DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
-	| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
-	    DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2)
-	| _ -> assert false
-
-  let terminal = function
-    | (DRel | DSort | DNil | DRef _) -> true
-    | _ -> false
-
-  let compare t1 t2 = compare dummy_cmp t1 t2
-
-end
-
-(*
- * Terms discrimination nets
- * Uses the general dnet datatype on DTerm.t
- * (here you can restart reading)
- *)
-
-(*
- * Construction of the module
- *)
-
-module type IDENT =
-sig
-  type t
-  val compare : t -> t -> int
-  val subst : substitution -> t -> t
-  val constr_of : t -> constr
-end
-
-module type OPT =
-sig
-  val reduce : constr -> constr
-  val direction : bool
-end
-
-module Make =
-  functor (Ident : IDENT) ->
-  functor (Opt : OPT) ->
-struct
-
-  module TDnet : Dnet.S with type ident=Ident.t
-			and  type 'a structure = 'a DTerm.t
-			and  type meta = int
-    = Dnet.Make(DTerm)(Ident)(Int)
-
-  type t = TDnet.t
-
-  type ident = TDnet.ident
-
-  (** We will freshen metas on the fly, to cope with the implementation defect
-      of Term_dnet which requires metas to be all distinct. *)
-  let fresh_meta =
-    let index = ref 0 in
-    fun () ->
-      let ans = !index in
-      let () = index := succ ans in
-      ans
-
-  open DTerm
-  open TDnet
-
-  let pat_of_constr c : term_pattern =
-    (** To each evar we associate a unique identifier. *)
-    let metas = ref Evar.Map.empty in
-    let rec pat_of_constr c = match kind_of_term c with
-    | Rel _          -> Term DRel
-    | Sort _         -> Term DSort
-    | Var i          -> Term (DRef (VarRef i))
-    | Const (c,u)    -> Term (DRef (ConstRef c))
-    | Ind (i,u)      -> Term (DRef (IndRef i))
-    | Construct (c,u)-> Term (DRef (ConstructRef c))
-    | Term.Meta _    -> assert false
-    | Evar (i,_)     ->
-      let meta =
-        try Evar.Map.find i !metas
-        with Not_found ->
-          let meta = fresh_meta () in
-          let () = metas := Evar.Map.add i meta !metas in
-          meta
-      in
-      Meta meta
-    | Case (ci,c1,c2,ca)     ->
-      Term(DCase(ci,pat_of_constr c1,pat_of_constr c2,Array.map pat_of_constr ca))
-    | Fix ((ia,i),(_,ta,ca)) ->
-      Term(DFix(ia,i,Array.map pat_of_constr ta, Array.map pat_of_constr ca))
-    | CoFix (i,(_,ta,ca))    ->
-      Term(DCoFix(i,Array.map pat_of_constr ta,Array.map pat_of_constr ca))
-    | Cast (c,_,_)   -> pat_of_constr c
-    | Lambda (_,t,c) -> Term(DLambda (pat_of_constr t, pat_of_constr c))
-    | (Prod (_,_,_) | LetIn(_,_,_,_))   ->
-      let (ctx,c) = ctx_of_constr (Term DNil) c in Term (DCtx (ctx,c))
-    | App (f,ca)     ->
-      Array.fold_left (fun c a -> Term (DApp (c,a)))
-        (pat_of_constr f) (Array.map pat_of_constr ca)
-    | Proj (p,c) -> 
-        Term (DApp (Term (DRef (ConstRef p)), pat_of_constr c))
-
-    and ctx_of_constr ctx c = match kind_of_term c with
-    | Prod (_,t,c)   -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c
-    | LetIn(_,d,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t, Some (pat_of_constr d)),ctx))) c
-    | _ -> ctx,pat_of_constr c
-    in
-    pat_of_constr c
-
-  let empty_ctx : term_pattern -> term_pattern = function
-    | Meta _ as c -> c
-    | Term (DCtx(_,_)) as c -> c
-    | c -> Term (DCtx (Term DNil, c))
-
-  (*
-   * Basic primitives
-   *)
-
-  let empty = TDnet.empty
-
-  let subst s t =
-    let sleaf id = Ident.subst s id in
-    let snode = function
-      | DTerm.DRef gr -> DTerm.DRef (fst (subst_global s gr))
-      | n -> n in
-    TDnet.map sleaf snode t
-
-  let union = TDnet.union
-
-  let add (c:constr) (id:Ident.t) (dn:t) =
-    let c = Opt.reduce c in
-    let c = empty_ctx (pat_of_constr c) in
-    TDnet.add dn c id
-
-
-  let new_meta () = Meta (fresh_meta ())
-
-  let rec remove_cap : term_pattern -> term_pattern = function
-    | Term (DCons (t,u)) -> Term (DCons (t,remove_cap u))
-    | Term DNil -> new_meta()
-    | Meta _ as m -> m
-    | _ -> assert false
-
-  let under_prod : term_pattern -> term_pattern = function
-    | Term (DCtx (t,u)) -> Term (DCtx (remove_cap t,u))
-    | Meta m -> Term (DCtx(new_meta(), Meta m))
-    | _ -> assert false
-
-  (* debug *)
-  let rec pr_term_pattern p =
-    (fun pr_t -> function
-       | Term t -> pr_t t
-       | Meta m -> str"["++Pp.int (Obj.magic m)++str"]"
-    ) (pr_dconstr pr_term_pattern) p
-
-  let search_pat cpat dpat dn =
-    let whole_c = cpat in
-    (* if we are at the root, add an empty context *)
-    let dpat = under_prod (empty_ctx dpat) in
-    TDnet.Idset.fold
-      (fun id acc ->
-	 let c_id = Opt.reduce (Ident.constr_of id) in
-	 let (ctx,wc) =
-	   try Termops.align_prod_letin whole_c c_id
-	   with Invalid_argument _ -> [],c_id in
-	 let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
-	 try
-          let _ = Termops.filtering ctx Reduction.CUMUL wc whole_c in
-          id :: acc
-	 with Termops.CannotFilter -> (* msgnl(str"recon "++Termops.print_constr_env (Global.env()) wc); *) acc
-      ) (TDnet.find_match dpat dn) []
-
-  (*
-   * High-level primitives describing specific search problems
-   *)
-
-  let search_pattern dn pat =
-    let pat = Opt.reduce pat in
-    search_pat pat (empty_ctx (pat_of_constr pat)) dn
-
-  let find_all dn = Idset.elements (TDnet.find_all dn)
-
-  let map f dn = TDnet.map f (fun x -> x) dn
-end
-
-module type S =
-sig
-  type t
-  type ident
-
-  val empty : t
-  val add : constr -> ident -> t -> t
-  val union : t -> t -> t
-  val subst : substitution -> t -> t
-  val search_pattern : t -> constr -> ident list
-  val find_all : t -> ident list
-  val map : (ident -> ident) -> t -> t
-end
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
deleted file mode 100644
index 7825ebdf1a..0000000000
--- a/pretyping/term_dnet.mli
+++ /dev/null
@@ -1,88 +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 Mod_subst
-
-(** Dnets on constr terms.
-
-   An instantiation of Dnet on (an approximation of) constr. It
-   associates a term (possibly with Evar) with an
-   identifier. Identifiers must be unique (no two terms sharing the
-   same ident), and there must be a way to recover the full term from
-   the identifier (function constr_of).
-
-   Optionally, a pre-treatment on terms can be performed before adding
-   or searching (reduce). Practically, it is used to do some kind of
-   delta-reduction on terms before indexing them.
-
-   The results returned here are perfect, since post-filtering is done
-   inside here.
-
-   See lib/dnet.mli for more details.
-*)
-
-(** Identifiers to store (right hand side of the association) *)
-module type IDENT = sig
-  type t
-  val compare : t -> t -> int
-
-  (** how to substitute them for storage *)
-  val subst : substitution -> t -> t
-
-  (** how to recover the term from the identifier *)
-  val constr_of : t -> constr
-end
-
-(** Options : *)
-module type OPT = sig
-
-  (** pre-treatment to terms before adding or searching *)
-  val reduce : constr -> constr
-
-  (** direction of post-filtering w.r.t sort subtyping :
-     - true means query <= terms in the structure
-     - false means terms <= query
- *)
-  val direction : bool
-end
-
-module type S =
-sig
-  type t
-  type ident
-
-  val empty : t
-
-  (** [add c i dn] adds the binding [(c,i)] to [dn]. [c] can be a
-     closed term or a pattern (with untyped Evars). No Metas accepted *)
-  val add : constr -> ident -> t -> t
-
-  (** merge of dnets. Faster than re-adding all terms *)
-  val union : t -> t -> t
-
-  val subst : substitution -> t -> t
-
-  (*
-   * High-level primitives describing specific search problems
-   *)
-
-  (** [search_pattern dn c] returns all terms/patterns in dn
-     matching/matched by c *)
-  val search_pattern : t -> constr -> ident list
-
-  (** [find_all dn] returns all idents contained in dn *)
-  val find_all : t -> ident list
-
-  val map : (ident -> ident) -> t -> t
-end
-
-module Make :
-  functor (Ident : IDENT) ->
-  functor (Opt : OPT) ->
-    S with type ident = Ident.t