diff options
Diffstat (limited to 'tactics/termdn.mli')
-rw-r--r-- | tactics/termdn.mli | 75 |
1 files changed, 41 insertions, 34 deletions
diff --git a/tactics/termdn.mli b/tactics/termdn.mli index e60aea6b4..aea49b073 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -28,38 +28,45 @@ indicates which constants and variables can be considered as rigid. These dnets are able to cope with existential variables as well, which match [Everything]. *) -type 'a t - -val create : unit -> 'a t - -(* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *) - -val add : 'a t -> transparent_state -> (constr_pattern * 'a) -> 'a t - -val rmv : 'a t -> transparent_state -> (constr_pattern * 'a) -> 'a t - -(* [lookup t c] looks for patterns (with their action) matching term [c] *) - -val lookup : 'a t -> transparent_state -> constr -> (constr_pattern * 'a) list - -val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit - - -(*i*) -(* These are for Nbtermdn *) - -type term_label = - | GRLabel of global_reference - | ProdLabel - | LambdaLabel - | SortLabel of sorts option - -val constr_pat_discr_st : transparent_state -> - constr_pattern -> (term_label * constr_pattern list) option -val constr_val_discr_st : transparent_state -> - constr -> (term_label * constr list) Dn.lookup_res - -val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option -val constr_val_discr : constr -> (term_label * constr list) Dn.lookup_res - +module Make : + functor (Z : Map.OrderedType) -> +sig + + type t + + type 'a lookup_res + + val create : unit -> t + + (* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *) + + val add : t -> transparent_state -> (constr_pattern * Z.t) -> t + + val rmv : t -> transparent_state -> (constr_pattern * Z.t) -> t + + (* [lookup t c] looks for patterns (with their action) matching term [c] *) + + val lookup : t -> transparent_state -> constr -> (constr_pattern * Z.t) list + + val app : ((constr_pattern * Z.t) -> unit) -> t -> unit + + + (*i*) + (* These are for Nbtermdn *) + + type term_label = + | GRLabel of global_reference + | ProdLabel + | LambdaLabel + | SortLabel of sorts option + + val constr_pat_discr_st : transparent_state -> + constr_pattern -> (term_label * constr_pattern list) option + val constr_val_discr_st : transparent_state -> + constr -> (term_label * constr list) lookup_res + + val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option + val constr_val_discr : constr -> (term_label * constr list) lookup_res + (*i*) +end |