From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- tactics/btermdn.ml | 189 +++++++++++++++++++++++++++++++++++------------------ 1 file changed, 126 insertions(+), 63 deletions(-) (limited to 'tactics/btermdn.ml') diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index a0aecbbc..bcb9a411 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: btermdn.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id$ *) open Term open Names @@ -19,72 +19,135 @@ open Libnames Eduardo (5/8/97). *) let dnet_depth = ref 8 - -let bounded_constr_pat_discr_st st (t,depth) = - if depth = 0 then - None - else - match constr_pat_discr_st st t with - | None -> None - | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) - -let bounded_constr_val_discr_st st (t,depth) = - if depth = 0 then - Dn.Nothing - else - match constr_val_discr_st st t with - | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l) - | Dn.Nothing -> Dn.Nothing - | Dn.Everything -> Dn.Everything -let bounded_constr_pat_discr (t,depth) = - if depth = 0 then - None - else - match constr_pat_discr t with - | None -> None - | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) - -let bounded_constr_val_discr (t,depth) = - if depth = 0 then - Dn.Nothing - else - match constr_val_discr t with - | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l) - | Dn.Nothing -> Dn.Nothing - | Dn.Everything -> Dn.Everything -type 'a t = (global_reference,constr_pattern * int,'a) Dn.t - -let create = Dn.create +module Make = + functor (Z : Map.OrderedType) -> +struct + module Term_dn = Termdn.Make(Z) + + module X = struct + type t = constr_pattern*int + let compare = Pervasives.compare + end + + module Y = struct + type t = Term_dn.term_label + let compare x y = + let make_name n = + match n with + | Term_dn.GRLabel(ConstRef con) -> + Term_dn.GRLabel(ConstRef(constant_of_kn(canonical_con con))) + | Term_dn.GRLabel(IndRef (kn,i)) -> + Term_dn.GRLabel(IndRef(mind_of_kn(canonical_mind kn),i)) + | Term_dn.GRLabel(ConstructRef ((kn,i),j ))-> + Term_dn.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) -let add = function - | None -> - (fun dn (c,v) -> - Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)) - | Some st -> - (fun dn (c,v) -> - Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) + type t = Dn.t -let rmv = function - | None -> - (fun dn (c,v) -> - Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v)) - | Some st -> - (fun dn (c,v) -> - Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) + let create = Dn.create -let lookup = function - | None -> - (fun dn t -> - List.map - (fun ((c,_),v) -> (c,v)) - (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth))) - | Some st -> - (fun dn t -> - List.map - (fun ((c,_),v) -> (c,v)) - (Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth))) + 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 app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn + 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 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 Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l) + | 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 when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l) + | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c]) + | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l) + | Sort s when is_small s -> Dn.Label(Term_dn.SortLabel (Some s), []) + | Sort _ -> Dn.Label(Term_dn.SortLabel None, []) + | Evar _ -> Dn.Everything + | _ -> Dn.Nothing + let bounded_constr_pat_discr_st st (t,depth) = + if depth = 0 then + None + else + match Term_dn.constr_pat_discr_st st t with + | None -> None + | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) + + let bounded_constr_val_discr_st st (t,depth) = + if depth = 0 then + Dn.Nothing + else + match constr_val_discr_st st t with + | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l) + | Dn.Nothing -> Dn.Nothing + | Dn.Everything -> Dn.Everything + + let bounded_constr_pat_discr (t,depth) = + if depth = 0 then + None + else + match Term_dn.constr_pat_discr t with + | None -> None + | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) + + let bounded_constr_val_discr (t,depth) = + if depth = 0 then + Dn.Nothing + else + match constr_val_discr t with + | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l) + | Dn.Nothing -> Dn.Nothing + | Dn.Everything -> Dn.Everything + + + let add = function + | None -> + (fun dn (c,v) -> + Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)) + | Some st -> + (fun dn (c,v) -> + Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) + + let rmv = function + | None -> + (fun dn (c,v) -> + Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v)) + | Some st -> + (fun dn (c,v) -> + Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) + + let lookup = function + | None -> + (fun dn t -> + List.map + (fun ((c,_),v) -> (c,v)) + (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth))) + | Some st -> + (fun dn t -> + List.map + (fun ((c,_),v) -> (c,v)) + (Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth))) + + let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn + +end + -- cgit v1.2.3