From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- tactics/dn.mli | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'tactics/dn.mli') diff --git a/tactics/dn.mli b/tactics/dn.mli index f8efd053..62e37a73 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: dn.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: dn.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (* Discrimination nets. *) @@ -28,13 +28,19 @@ val add : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf 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 ('lbl,'tree) lookup_fun = 'tree -> ('lbl * '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) decompose_fun -> 'term +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 -- cgit v1.2.3