diff options
Diffstat (limited to 'tactics/btermdn.ml')
| -rw-r--r-- | tactics/btermdn.ml | 62 |
1 files changed, 50 insertions, 12 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index f0b23b8d..a0aecbbc 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: btermdn.ml 6427 2004-12-07 17:41:10Z sacerdot $ *) +(* $Id: btermdn.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Term +open Names open Termdn open Pattern open Libnames @@ -19,6 +20,23 @@ open Libnames 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 @@ -29,24 +47,44 @@ let bounded_constr_pat_discr (t,depth) = let bounded_constr_val_discr (t,depth) = if depth = 0 then - None + Dn.Nothing else match constr_val_discr t with - | None -> None - | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) + | 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 + +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 add dn (c,v) = Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v) - -let rmv dn (c,v) = Dn.rmv dn bounded_constr_pat_discr ((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 dn t = - List.map - (fun ((c,_),v) -> (c,v)) - (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth)) +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 |