diff options
Diffstat (limited to 'tactics/dn.mli')
-rw-r--r-- | tactics/dn.mli | 36 |
1 files changed, 22 insertions, 14 deletions
diff --git a/tactics/dn.mli b/tactics/dn.mli index 211b75a36..42c6303a0 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -3,23 +3,31 @@ (* Discrimination nets. *) -type ('lbl,'pat) dn_args = 'pat -> ('lbl * 'pat list) option +type ('lbl,'tree) decompose_fun = 'tree -> ('lbl * 'tree list) option -type ('lbl,'pat,'inf) t = { - tm : (('lbl * int) option,'pat * 'inf) Tlm.t; - args : ('lbl,'pat) dn_args } +type ('lbl,'pat,'inf) t (* = (('lbl * int) option,'pat * 'inf) Tlm.t *) -type ('lbl,'pat,'inf) under_t = (('lbl * int) option,'pat * 'inf) Tlm.t - -val create : ('lbl,'pat) dn_args -> ('lbl,'pat,'inf) t - -val add : ('lbl,'pat,'inf) t -> 'pat * 'inf -> ('lbl,'pat,'inf) t +val create : unit -> ('lbl,'pat,'inf) t -val rmv : ('lbl,'pat,'inf) t -> 'pat * 'inf -> ('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 path_of : ('lbl,'pat) dn_args -> 'pat -> ('lbl * int) option list - -val lookup : - ('lbl,'pat,'inf) t -> ('lbl,'term) dn_args -> 'term -> ('pat * 'inf) list +val add : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf + -> ('lbl,'pat,'inf) t + +val rmv : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf + -> ('lbl,'pat,'inf) t + +(* [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 + -> ('pat * 'inf) list val app : (('pat * 'inf) -> unit) -> ('lbl,'pat,'inf) t -> unit |