From c6d9d4fb142ef42634be25b60c0995b541e86629 Mon Sep 17 00:00:00 2001
From: Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr>
Date: Mon, 15 Feb 2016 16:22:45 +0100
Subject: Adding ability to put any pattern in binders, prefixed by a quote.

Cf CHANGES for details.
---
 parsing/g_constr.ml4 | 15 +++++++++++++++
 parsing/g_vernac.ml4 | 16 +++++++++++++++-
 2 files changed, 30 insertions(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 243f71416..014b41ae9 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -401,6 +401,14 @@ GEXTEND Gram
               CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
                 CPatNotation(!@loc,"( _ )",([p],[]),[])
             | _ -> p)
+      | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
+          let p =
+            match p with
+              CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
+                CPatNotation(!@loc,"( _ )",([p],[]),[])
+            | _ -> p
+          in
+	  CPatCast (!@loc, p, ty)
       | n = INT -> CPatPrim (!@loc, Numeral (Bigint.of_string n))
       | s = string -> CPatPrim (!@loc, String s) ] ]
   ;
@@ -476,6 +484,13 @@ GEXTEND Gram
 	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
       | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
 	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+      | "'"; p = pattern LEVEL "0" ->
+          let (p, ty) =
+            match p with
+            | CPatCast (_, p, ty) -> (p, Some ty)
+            | _ -> (p, None)
+          in
+          [LocalPattern (!@loc, p, ty)]
     ] ]
   ;
   typeclass_constraint:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 9c1f5afb8..f0475ee25 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -135,6 +135,12 @@ let test_plural_form_types = function
    (strbrk "Keywords Implicit Types expect more than one type")
   | _ -> ()
 
+let fresh_var env c =
+  Namegen.next_ident_away (Id.of_string "pat")
+    (env @ Id.Set.elements (Topconstr.free_vars_of_constr_expr c))
+
+let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var
+
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
@@ -235,11 +241,19 @@ GEXTEND Gram
   (* Simple definitions *)
   def_body:
     [ [ bl = binders; ":="; red = reduce; c = lconstr ->
+      let (bl, c) = expand_pattern_binders mkCLambdaN bl c in
       (match c with
           CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
     | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
-	DefineBody (bl, red, c, Some t)
+        let ((bl, c), tyo) =
+          if List.exists (function LocalPattern _ -> true | _ -> false) bl
+          then
+            let c = CCast (!@loc, c, CastConv t) in
+            (expand_pattern_binders mkCLambdaN bl c, None)
+          else ((bl, c), Some t)
+        in
+	DefineBody (bl, red, c, tyo)
     | bl = binders; ":"; t = lconstr ->
         ProveBody (bl, t) ] ]
   ;
-- 
cgit v1.2.3