merged cic_notation with disambiguation: good luck!

[helm.git] / helm / ocaml / cic_notation / cicNotationFwd.ml

diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml
index 8e955c0b10a8d562647833d501477c3aa87a28ff..93a4c684d019de589035215efcb4506c474da3db 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationFwd.ml
+++ b/helm/ocaml/cic_notation/cicNotationFwd.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
 open CicNotationEnv
 open CicNotationPt
 
@@ -246,3 +248,18 @@ let instantiate_level2 env term =
   in
   aux env term
 
+let instantiate_appl_pattern env appl_pattern =
+  let lookup name =
+    try List.assoc name env
+    with Not_found ->
+      prerr_endline (sprintf "Name %s not found" name);
+      assert false
+  in
+  let rec aux = function
+    | UriPattern uri -> CicUtil.term_of_uri uri
+    | ImplicitPattern -> Cic.Implicit None
+    | VarPattern name -> lookup name
+    | ApplPattern terms -> Cic.Appl (List.map aux terms)
+  in
+  aux appl_pattern
+