diff options
Diffstat (limited to 'tactics/termdn.ml')
| -rw-r--r-- | tactics/termdn.ml | 136 |
1 files changed, 0 insertions, 136 deletions
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 |