diff options
Diffstat (limited to 'tactics/dn.mli')
| -rw-r--r-- | tactics/dn.mli | 10 |
1 files changed, 8 insertions, 2 deletions
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 |