From 180f30d039f1d2894c6a118ecee5549835127c72 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 27 Jun 2005 12:24:32 +0000 Subject: [PATCH] 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 -> [] --- .../cic_disambiguation/cicTextualParser2.ml | 8 +++++--- helm/ocaml/tactics/proofEngineHelpers.ml | 17 ++++++++++++++--- 2 files changed, 19 insertions(+), 6 deletions(-) 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) -- 2.39.2