diff options
Diffstat (limited to 'tactics/termdn.ml')
| -rw-r--r-- | tactics/termdn.ml | 101 |
1 files changed, 75 insertions, 26 deletions
diff --git a/tactics/termdn.ml b/tactics/termdn.ml index bd439fb4..7b6d3ea7 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: termdn.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id$ *) open Util open Names @@ -20,25 +20,60 @@ open Nametab (* Discrimination nets of terms. See the module dn.ml for further explanations. Eduardo (5/8/97) *) +module Make = + functor (Z : Map.OrderedType) -> +struct -type 'a t = (global_reference,constr_pattern,'a) Dn.t + module X = struct + type t = constr_pattern + let compare = Pervasives.compare + end + + type term_label = + | GRLabel of global_reference + | ProdLabel + | LambdaLabel + | SortLabel of sorts option + + 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 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 + in decrec [] -let decomp_pat = +let decomp_pat = let rec decrec acc = function | PApp (f,args) -> decrec (Array.to_list args @ acc) f | c -> (c,acc) - in - decrec [] + in + decrec [] let constr_pat_discr t = if not (occur_meta_pattern t) then @@ -46,49 +81,63 @@ let constr_pat_discr t = else match decomp_pat t with | PRef ((IndRef _) as ref), args - | PRef ((ConstructRef _ ) as ref), args -> Some (ref,args) - | PRef ((VarRef v) as ref), args -> Some(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 (ref,args) - | PRef ((VarRef v) as ref), args when not (Idpred.mem v idpred) -> - Some(ref,args) + | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) + | PRef ((VarRef v) as ref), args when not (Idpred.mem v idpred) -> + Some(GRLabel ref,args) | PVar v, args when not (Idpred.mem v idpred) -> - Some(VarRef v,args) + Some(GRLabel (VarRef v),args) | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) -> - Some (ref, args) + Some (GRLabel ref, args) + | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c]) + | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l) + | PSort s, [] -> + let s' = match s with + | RProp c -> Some (Prop c) + | RType _ -> None + (* Don't try to be clever about type levels here *) + in Some (SortLabel s', []) | _ -> None open Dn -let constr_val_discr t = +let constr_val_discr t = let c, l = decomp t in match kind_of_term c with - | Ind ind_sp -> Label(IndRef ind_sp,l) - | Construct cstr_sp -> Label((ConstructRef cstr_sp),l) - | Var id -> Label(VarRef id,l) + | 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 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(ConstRef c,l) - | Ind ind_sp -> Label(IndRef ind_sp,l) - | Construct cstr_sp -> Label((ConstructRef cstr_sp),l) - | Var id when not (Idpred.mem id idpred) -> Label(VarRef id,l) + | 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 (Idpred.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 s when is_small s -> Label(SortLabel (Some s), []) + | Sort _ -> Label (SortLabel None, []) | Evar _ -> Everything | _ -> Nothing -let create = Dn.create +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 |