snapshot (first version with working pattern matching both 3->2 and 2->1)

[helm.git] / helm / ocaml / cic_notation / cicNotationMatcher.mli

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.mli b/helm/ocaml/cic_notation/cicNotationMatcher.mli
index e999b3c6a296be7e5c6386f2b85c6804e5e6f8be..55de82999f9aa8537637a7838a0c374324570719 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationMatcher.mli
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.mli
@@ -23,10 +23,37 @@
  * 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) ->
+    (unit -> 'a) ->
+      (P.term_t -> 'a)
+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