diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-26 09:50:56 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-26 09:50:56 +0000 |
commit | 80297f53a4a43aff327426a08ffd58236ec4d56d (patch) | |
tree | b6543d840f01a018db828e3058148a0a942fdfa0 /tactics/dn.mli | |
parent | 99cda3324ad90fc77e810f0412f44bf81df99371 (diff) |
Nettoyage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@367 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |