X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.mli;h=4a9d4a27548b5e1a5e809a45915de74485148ba6;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=e999b3c6a296be7e5c6386f2b85c6804e5e6f8be;hpb=50377dde5b5b1a8e5c7b2fb48b47defde9508b50;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.mli b/helm/ocaml/cic_notation/cicNotationMatcher.mli
index e999b3c6a..4a9d4a275 100644
--- a/helm/ocaml/cic_notation/cicNotationMatcher.mli
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.mli
@@ -23,10 +23,38 @@
  * 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