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