From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- tactics/dn.mli | 41 ++++++++++++++++------------------------- 1 file changed, 16 insertions(+), 25 deletions(-) (limited to 'tactics/dn.mli') diff --git a/tactics/dn.mli b/tactics/dn.mli index 662ac19a..20407e9d 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -1,48 +1,39 @@ +type 'res lookup_res = Label of 'res | Nothing | Everything - - - - - -module Make : - functor (X : Set.OrderedType) -> +module Make : functor (Y : Map.OrderedType) -> functor (Z : Map.OrderedType) -> sig - type decompose_fun = X.t -> (Y.t * X.t list) option - + type 'a decompose_fun = 'a -> (Y.t * 'a 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 - + + val add : t -> 'a decompose_fun -> 'a * Z.t -> t + + val rmv : t -> 'a decompose_fun -> 'a * Z.t -> t + 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 - + -> Z.t list + + val app : (Z.t -> unit) -> t -> unit + end -- cgit v1.2.3