From 37f624d80e82d655021f2beb7d72794a120ff8b5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 3 Mar 2014 02:22:56 +0100 Subject: Extruding code not depending of the functor argument in Termdn. --- tactics/btermdn.ml | 128 ++++++++++++++++++++++++++--------------------------- tactics/dn.ml | 4 +- tactics/dn.mli | 30 +++++-------- tactics/termdn.ml | 50 ++++----------------- tactics/termdn.mli | 58 +++++++----------------- 5 files changed, 103 insertions(+), 167 deletions(-) diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 76119a2ec..1751d4138 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -22,120 +22,120 @@ let dnet_depth = ref 8 module Make = functor (Z : Map.OrderedType) -> struct - module Term_dn = Termdn.Make(Z) + open Termdn module X = struct type t = constr_pattern*int let compare = Pervasives.compare (** FIXME *) end - module Y = struct - type t = Term_dn.term_label - let compare t1 t2 = match t1, t2 with - | Term_dn.GRLabel gr1, Term_dn.GRLabel gr2 -> RefOrdered.compare gr1 gr2 - | _ -> Pervasives.compare t1 t2 (** OK *) + module Y = struct + type t = term_label + let compare = compare_term_label end - + + type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything + module Dn = Dn.Make(X)(Y)(Z) - + type t = Dn.t let create = Dn.create - 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 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 - + | 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 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 (Id.Pred.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 _ -> Dn.Label(Term_dn.SortLabel, []) - | Evar _ -> Dn.Everything - | _ -> Dn.Nothing + | 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 let bounded_constr_pat_discr_st st (t,depth) = - if Int.equal depth 0 then - None + if Int.equal depth 0 then + None else - match Term_dn.constr_pat_discr_st st t with + 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 Int.equal depth 0 then - Dn.Nothing + if Int.equal depth 0 then + 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 + | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l) + | Nothing -> Nothing + | Everything -> Everything let bounded_constr_pat_discr (t,depth) = - if Int.equal depth 0 then - None + if Int.equal depth 0 then + None else - match Term_dn.constr_pat_discr t with + 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 Int.equal depth 0 then - Dn.Nothing + if Int.equal depth 0 then + 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 - - + | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l) + | Nothing -> Nothing + | Everything -> Everything + + let add = function - | None -> - (fun dn (c,v) -> + | None -> + (fun dn (c,v) -> Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)) - | Some st -> - (fun dn (c,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) -> + | None -> + (fun dn (c,v) -> Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v)) - | Some st -> - (fun dn (c,v) -> + | Some st -> + (fun dn (c,v) -> Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) - + let lookup = function - | None -> + | None -> (fun dn t -> - List.map - (fun ((c,_),v) -> (c,v)) + List.map + (fun ((c,_),v) -> (c,v)) (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth))) - | Some st -> + | Some st -> (fun dn t -> - List.map - (fun ((c,_),v) -> (c,v)) + 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 - + diff --git a/tactics/dn.ml b/tactics/dn.ml index 069e84fad..e0f2016c7 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -1,6 +1,6 @@ open Util - +type 'res lookup_res = Label of 'res | Nothing | Everything module Make = functor (X : Set.OrderedType) -> @@ -42,8 +42,6 @@ struct type decompose_fun = X.t -> (Y.t * X.t list) option - type 'res lookup_res = Label of 'res | Nothing | Everything - type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res type t = Trie.t diff --git a/tactics/dn.mli b/tactics/dn.mli index 662ac19af..bab925a20 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -1,48 +1,42 @@ +type 'res lookup_res = Label of 'res | Nothing | Everything - - - - - -module Make : +module Make : functor (X : Set.OrderedType) -> functor (Y : Map.OrderedType) -> functor (Z : Map.OrderedType) -> sig type decompose_fun = X.t -> (Y.t * X.t list) option - + type t val create : unit -> t - + (** [add t f (tree,inf)] adds a structured object [tree] together with the associated information [inf] to the table [t]; the function [f] is used to translated [tree] into its prefix decomposition: [f] must decompose any tree into a label characterizing its root node and the list of its subtree *) - + val add : t -> decompose_fun -> X.t * Z.t -> t - + val rmv : t -> decompose_fun -> X.t * Z.t -> t - - type 'res lookup_res = Label of 'res | Nothing | Everything - + type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res - + (** [lookup t f tree] looks for trees (and their associated information) in table [t] such that the structured object [tree] matches against them; [f] is used to translated [tree] into its prefix decomposition: [f] must decompose any tree into a label characterizing its root node and the list of its subtree *) - + val lookup : t -> 'term lookup_fun -> 'term -> (X.t * Z.t) list - + val app : ((X.t * Z.t) -> unit) -> t -> unit - + val skip_arg : int -> t -> (t * bool) list - + end diff --git a/tactics/termdn.ml b/tactics/termdn.ml index b5a7359d6..7eff2909f 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -13,37 +13,17 @@ 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 +type term_label = +| GRLabel of global_reference +| ProdLabel +| LambdaLabel +| SortLabel - module X = struct - type t = constr_pattern - let compare = Pervasives.compare (** FIXME *) - end +let compare_term_label t1 t2 = match t1, t2 with +| GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2 +| _ -> Pervasives.compare t1 t2 (** OK *) - type term_label = - | GRLabel of global_reference - | ProdLabel - | LambdaLabel - | SortLabel - - module Y = struct - type t = term_label - let compare t1 t2 = match t1, t2 with - | GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2 - | _ -> Pervasives.compare t1 t2 (** OK *) - end - - - module Dn = Dn.Make(X)(Y)(Z) - - type t = Dn.t - - type 'a lookup_res = 'a Dn.lookup_res +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;...])*) @@ -110,15 +90,3 @@ let constr_val_discr_st (idpred,cpred) t = | 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 diff --git a/tactics/termdn.mli b/tactics/termdn.mli index 2da0d94ff..16be2e1c9 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -11,6 +11,14 @@ open Pattern open Globnames open Names +type term_label = +| GRLabel of global_reference +| ProdLabel +| LambdaLabel +| SortLabel + +val compare_term_label : term_label -> term_label -> int + (** Discrimination nets of terms. *) (** This module registers actions (typically tactics) mapped to patterns *) @@ -24,45 +32,13 @@ indicates which constants and variables can be considered as rigid. These dnets are able to cope with existential variables as well, which match [Everything]. *) -module Make : - functor (Z : Map.OrderedType) -> -sig - - type t - - type 'a lookup_res - - val create : unit -> t - - (** [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *) - - val add : t -> transparent_state -> (constr_pattern * Z.t) -> t - - val rmv : t -> transparent_state -> (constr_pattern * Z.t) -> t - - (** [lookup t c] looks for patterns (with their action) matching term [c] *) - - val lookup : t -> transparent_state -> constr -> (constr_pattern * Z.t) list - - val app : ((constr_pattern * Z.t) -> unit) -> t -> unit +(**/**) +(** These are for Nbtermdn *) + +val constr_pat_discr_st : transparent_state -> + constr_pattern -> (term_label * constr_pattern list) option +val constr_val_discr_st : transparent_state -> + constr -> (term_label * constr list) Dn.lookup_res - - (**/**) - (** These are for Nbtermdn *) - - type term_label = - | GRLabel of global_reference - | ProdLabel - | LambdaLabel - | SortLabel - - val constr_pat_discr_st : transparent_state -> - constr_pattern -> (term_label * constr_pattern list) option - val constr_val_discr_st : transparent_state -> - constr -> (term_label * constr list) lookup_res - - val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option - val constr_val_discr : constr -> (term_label * constr list) lookup_res - - (**/**) -end +val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option +val constr_val_discr : constr -> (term_label * constr list) Dn.lookup_res -- cgit v1.2.3