From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 27 Jun 2005 12:24:32 +0000 (+0000)
Subject: support for _ in binders, and a more coplex pattern that should help if
X-Git-Tag: INDEXING_NO_PROOFS~50
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=180f30d039f1d2894c6a118ecee5549835127c72;p=helm.git

support for _ in binders, and a more coplex pattern that should help if
patterns will be used on subterms.
match pattern, term with
| Binder Anonymous, Binder name -> recursion
| Binder name1, Binder name2 when name1 = name2 -> recursion
| Binder name1, Binder name2 -> []
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 9443a35d1..1b67821c1 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -229,10 +229,12 @@ EXTEND
     ]];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
   binder_vars: [
-      [ vars = LIST1 IDENT SEP SYMBOL ",";
+      [ vars = [ l = LIST1 IDENT SEP SYMBOL "," -> l | SYMBOL "_" -> ["_"]];
         typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
-      | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
-        typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
+      | PAREN "("; 
+          vars = [ l =  LIST1 IDENT SEP SYMBOL "," -> l | SYMBOL "_" -> ["_"]];
+          typ = OPT [ SYMBOL ":"; t = term -> t ]; 
+        PAREN ")" -> (vars, typ)
       ]
   ];
   term0: [ [ t = term; EOI -> return_term loc t ] ];
diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 3382c4c98..20e8341a6 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -170,11 +170,22 @@ let select ~term ~pattern =
               (match (t1, t2) with Some t1, Some t2 -> aux i t1 t2 | _ -> []))
             ctxt1 ctxt2)
     | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux i te1 te2 @ aux i ty1 ty2
-    | Cic.Prod (_, s1, t1), Cic.Prod (name, s2, t2)
-    | Cic.Lambda (_, s1, t1), Cic.Lambda (name, s2, t2) ->
+    | Cic.Prod (Cic.Anonymous, s1, t1), Cic.Prod (name, s2, t2)
+    | Cic.Lambda (Cic.Anonymous, s1, t1), Cic.Lambda (name, s2, t2) ->
         aux i s1 s2 @ aux (add_ctx i name (Cic.Decl s2)) t1 t2
-    | Cic.LetIn (_, s1, t1), Cic.LetIn (name, s2, t2) -> 
+    | Cic.Prod (Cic.Name n1, s1, t1), 
+      Cic.Prod ((Cic.Name n2) as name , s2, t2)
+    | Cic.Lambda (Cic.Name n1, s1, t1), 
+      Cic.Lambda ((Cic.Name n2) as name, s2, t2) when n1 = n2->
+        aux i s1 s2 @ aux (add_ctx i name (Cic.Decl s2)) t1 t2
+    | Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2)
+    | Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> []
+    | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) -> 
+        aux i s1 s2 @ aux (add_ctx i name (Cic.Def (s2,None))) t1 t2
+    | Cic.LetIn (Cic.Name n1, s1, t1), 
+      Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2-> 
         aux i s1 s2 @ aux (add_ctx i name (Cic.Def (s2,None))) t1 t2
+    | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> []
     | Cic.Appl terms1, Cic.Appl terms2 -> auxs i terms1 terms2
     | Cic.Var (_, subst1), Cic.Var (_, subst2)
     | Cic.Const (_, subst1), Cic.Const (_, subst2)