diff options
Diffstat (limited to 'tactics/dn.mli')
| -rw-r--r-- | tactics/dn.mli | 63 |
1 files changed, 32 insertions, 31 deletions
diff --git a/tactics/dn.mli b/tactics/dn.mli index 62e37a73..3cb52a56 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -1,46 +1,47 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(*i $Id: dn.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) -(* Discrimination nets. *) -type ('lbl,'tree) decompose_fun = 'tree -> ('lbl * 'tree list) option -type ('lbl,'pat,'inf) t (* = (('lbl * int) option,'pat * 'inf) Tlm.t *) -val create : unit -> ('lbl,'pat,'inf) 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 : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf - -> ('lbl,'pat,'inf) t +module Make : + functor (X : Set.OrderedType) -> + functor (Y : Map.OrderedType) -> + functor (Z : Map.OrderedType) -> +sig -val rmv : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf - -> ('lbl,'pat,'inf) t - -type 'res lookup_res = Label of 'res | Nothing | Everything + type decompose_fun = X.t -> (Y.t * X.t list) option -type ('lbl,'tree) lookup_fun = 'tree -> ('lbl * 'tree list) lookup_res + 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 : ('lbl,'pat,'inf) t -> ('lbl,'term) lookup_fun -> 'term - -> ('pat * 'inf) list - -val app : (('pat * 'inf) -> unit) -> ('lbl,'pat,'inf) t -> unit - -val skip_arg : int -> ('lbl,'pat,'inf) t -> (('lbl,'pat,'inf) t * bool) list + + 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 |