* http://helm.cs.unibo.it/
*)
-module T21 :
- sig
- val compiler :
- (CicNotationPt.term * int) list ->
+type pattern_kind = Variable | Constructor
+type tag_t = int
+
+module type PATTERN =
+sig
+ type pattern_t
+ type term_t
+ val classify : pattern_t -> pattern_kind
+ val tag_of_pattern : pattern_t -> tag_t * pattern_t list
+ val tag_of_term : term_t -> tag_t * term_t list
+end
+
+module Matcher (P: PATTERN) :
+sig
+ val compiler:
+ (P.pattern_t * int) list ->
+ ((P.pattern_t list * int) list -> P.term_t list -> 'a option) ->
+ (unit -> 'a option) ->
+ (P.term_t -> 'a option)
+end
+
+module Matcher21:
+sig
+ val compiler :
+ (CicNotationPt.term * int) list ->
(CicNotationPt.term -> (CicNotationEnv.t * int) option)
- end
+end
+
+module Matcher32:
+sig
+ val compiler :
+ (CicNotationPt.cic_appl_pattern * int) list ->
+ (Cic.annterm -> ((string * Cic.annterm) list * int) option)
+end