aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/nbtermdn.ml131
-rw-r--r--tactics/termdn.ml136
2 files changed, 0 insertions, 267 deletions
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
deleted file mode 100644
index b07aff99b..000000000
--- a/tactics/nbtermdn.ml
+++ /dev/null
@@ -1,131 +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 Globnames
-
-(* Named, bounded-depth, term-discrimination nets.
- Implementation:
- Term-patterns are stored in discrimination-nets, which are
- themselves stored in a hash-table, indexed by the first label.
- They are also stored by name in a table on-the-side, so that we can
- override them if needed. *)
-
-(* The former comments are from Chet.
- See the module dn.ml for further explanations.
- Eduardo (5/8/97) *)
-module Make =
- functor (Y:Map.OrderedType) ->
-struct
- module X = struct
- type t = constr_pattern*int
- let compare = Pervasives.compare
- end
-
- module Term_dn = Termdn.Make(Y)
- open Term_dn
- module Z = struct
- type t = Term_dn.term_label
- let compare x y =
- let make_name n =
- match n with
- | GRLabel(ConstRef con) ->
- GRLabel(ConstRef(constant_of_kn(canonical_con con)))
- | GRLabel(IndRef (kn,i)) ->
- GRLabel(IndRef(mind_of_kn(canonical_mind kn),i))
- | GRLabel(ConstructRef ((kn,i),j ))->
- GRLabel(ConstructRef((mind_of_kn(canonical_mind kn),i),j))
- | k -> k
- in
- Pervasives.compare (make_name x) (make_name y)
- end
-
- module Dn = Dn.Make(X)(Z)(Y)
- module Bounded_net = Btermdn.Make(Y)
-
-
-type 'na t = {
- mutable table : ('na,constr_pattern * Y.t) Gmap.t;
- mutable patterns : (Term_dn.term_label option,Bounded_net.t) Gmap.t }
-
-
-type 'na frozen_t =
- ('na,constr_pattern * Y.t) Gmap.t
- * (Term_dn.term_label option, Bounded_net.t) Gmap.t
-
-let create () =
- { table = Gmap.empty;
- patterns = Gmap.empty }
-
-let get_dn dnm hkey =
- try Gmap.find hkey dnm with Not_found -> Bounded_net.create ()
-
-let add dn (na,(pat,valu)) =
- let hkey = Option.map fst (Term_dn.constr_pat_discr pat) in
- dn.table <- Gmap.add na (pat,valu) dn.table;
- let dnm = dn.patterns in
- dn.patterns <- Gmap.add hkey (Bounded_net.add None (get_dn dnm hkey) (pat,valu)) dnm
-
-let rmv dn na =
- let (pat,valu) = Gmap.find na dn.table in
- let hkey = Option.map fst (Term_dn.constr_pat_discr pat) in
- dn.table <- Gmap.remove na dn.table;
- let dnm = dn.patterns in
- dn.patterns <- Gmap.add hkey (Bounded_net.rmv None (get_dn dnm hkey) (pat,valu)) dnm
-
-let in_dn dn na = Gmap.mem na dn.table
-
-let remap ndn na (pat,valu) =
- rmv ndn na;
- add ndn (na,(pat,valu))
-
-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,_) -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
- | Construct (cstr_sp,_) -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
- | Var id -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
- | Const _ -> Dn.Everything
- | _ -> Dn.Nothing
-
-let lookup dn valu =
- let hkey =
- match (constr_val_discr valu) with
- | Dn.Label(l,_) -> Some l
- | _ -> None
- in
- try Bounded_net.lookup None (Gmap.find hkey dn.patterns) valu with Not_found -> []
-
-let app f dn = Gmap.iter f dn.table
-
-let dnet_depth = Btermdn.dnet_depth
-
-let freeze dn = (dn.table, dn.patterns)
-
-let unfreeze (fnm,fdnm) dn =
- dn.table <- fnm;
- dn.patterns <- fdnm
-
-let empty dn =
- dn.table <- Gmap.empty;
- dn.patterns <- Gmap.empty
-
-let to2lists dn =
- (Gmap.to_list dn.table, Gmap.to_list dn.patterns)
-end
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
deleted file mode 100644
index 1c4c4b648..000000000
--- a/tactics/termdn.ml
+++ /dev/null
@@ -1,136 +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
-
-(* Discrimination nets of terms.
- See the module dn.ml for further explanations.
- Eduardo (5/8/97) *)
-module Make =
- functor (Z : Map.OrderedType) ->
-struct
-
- module X = struct
- type t = constr_pattern
- let compare = Pervasives.compare (** FIXME *)
- end
-
- type term_label =
- | GRLabel of global_reference
- | ProdLabel
- | LambdaLabel
- | SortLabel
-
- module Y = struct
- type t = term_label
- let compare x y =
- let make_name n =
- match n with
- | GRLabel(ConstRef con) ->
- GRLabel(ConstRef(constant_of_kn(canonical_con con)))
- | GRLabel(IndRef (kn,i)) ->
- GRLabel(IndRef(mind_of_kn(canonical_mind kn),i))
- | GRLabel(ConstructRef ((kn,i),j ))->
- GRLabel(ConstructRef((mind_of_kn(canonical_mind kn),i),j))
- | k -> k
- in
- Pervasives.compare (make_name x) (make_name y)
- end
-
-
- module Dn = Dn.Make(X)(Y)(Z)
-
- type t = Dn.t
-
- type 'a lookup_res = 'a Dn.lookup_res
-
-(*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
- | Proj (p, c) -> decrec (c :: acc) (mkConst p)
- | _ -> (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,u) -> Label(GRLabel (IndRef ind_sp),l)
- | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
- | Var id -> Label(GRLabel (VarRef id),l)
- | Const _ -> Everything
- | Proj _ -> 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)
- | Proj (p,c) -> if Cpred.mem p cpred then Everything else Label(GRLabel (ConstRef p),c::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 create = Dn.create
-
-let add dn st = Dn.add dn (constr_pat_discr_st st)
-
-let rmv dn st = Dn.rmv dn (constr_pat_discr_st st)
-
-let lookup dn st t = Dn.lookup dn (constr_val_discr_st st) t
-
-let app f dn = Dn.app f dn
-
-end
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 19:05:32 +0000