Merge PR #11668: Helping issue #11659 by leaving only the Cast hack in the grammar.

Reviewed-by: ejgallego
Reviewed-by: maximedenes

3 files changed, 47 insertions, 22 deletions

diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 4f09f00c56..bdfa8afb6a 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -4,7 +4,7 @@ fun '(x, y) => (y, x)
      : A * B -> B * A
 forall '(x, y), swap (x, y) = (y, x)
      : Prop
-proj_informative = fun '(exist _ x _) => x : A
+proj_informative = fun '(exist _ x _) => x
      : {x : A | P x} -> A
 foo = fun '(Bar n b tt p) => if b then n + p else n - p
      : Foo -> nat
@@ -29,8 +29,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w)
 ∀ '(x, y), swap (x, y) = (y, x)
      : Prop
 both_z = 
-fun pat : nat * nat =>
-let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p)
+fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p)
      : forall pat : nat * nat, F pat
 fun '(x, y) '(z, t) => swap (x, y) = (z, t)
      : A * B -> B * A -> Prop
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index ba2c1ac115..d50edbad4d 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -40,10 +40,50 @@ let check_imps ~impsty ~impsbody =
   | [], [] -> () in
   aux impsty impsbody
 
+let protect_pattern_in_binder bl c ctypopt =
+  (* We turn "Definition d binders := body : typ" into *)
+  (* "Definition d := fun binders => body:type" *)
+  (* This is a hack while waiting for LocalPattern in regular environments *)
+  if List.exists (function Constrexpr.CLocalPattern _ -> true | _ -> false) bl
+  then
+    let t = match ctypopt with
+      | None -> CAst.make ?loc:c.CAst.loc (Constrexpr.CHole (None,Namegen.IntroAnonymous,None))
+      | Some t -> t in
+    let loc = Loc.merge_opt c.CAst.loc t.CAst.loc in
+    let c = CAst.make ?loc @@ Constrexpr.CCast (c, Glob_term.CastConv t) in
+    let loc = match List.hd bl with
+      | Constrexpr.CLocalAssum (a::_,_,_) | Constrexpr.CLocalDef (a,_,_) -> a.CAst.loc
+      | Constrexpr.CLocalPattern {CAst.loc} -> loc
+      | Constrexpr.CLocalAssum ([],_,_) -> assert false in
+    let apply_under_binders f env evd c =
+      let rec aux env evd c =
+        let open Constr in
+        let open EConstr in
+        let open Context.Rel.Declaration in
+        match kind evd c with
+        | Lambda (x,t,c)  ->
+          let evd,c = aux (push_rel (LocalAssum (x,t)) env) evd c in
+          evd, mkLambda (x,t,c)
+        | LetIn (x,b,t,c) ->
+          let evd,c = aux (push_rel (LocalDef (x,b,t)) env) evd c in
+          evd, mkLetIn (x,t,b,c)
+        | Case (ci,p,a,bl) ->
+          let evd,bl = Array.fold_left_map (aux env) evd bl in
+          evd, mkCase (ci,p,a,bl)
+        | Cast (c,_,_)    -> f env evd c  (* we remove the cast we had set *)
+        (* This last case may happen when reaching the proof of an
+           impossible case, as when pattern-matching on a vector of length 1 *)
+        | _ -> (evd,c) in
+      aux env evd c in
+    ([], Constrexpr_ops.mkLambdaCN ?loc:(Loc.merge_opt loc c.CAst.loc) bl c, None, apply_under_binders)
+  else
+    (bl, c, ctypopt, fun f env evd c -> f env evd c)
+
 let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
   let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
+  let (bl, c, ctypopt, apply_under_binders) = protect_pattern_in_binder bl c ctypopt in
   (* Build the parameters *)
   let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in
   (* Build the type *)
@@ -63,7 +103,7 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
       evd, c, imps1@impsty, Some ty
   in
   (* Do the reduction *)
-  let evd, c = red_constant_body red_option env_bl evd c in
+  let evd, c = apply_under_binders (red_constant_body red_option) env_bl evd c in
 
   (* Declare the definition *)
   let c = EConstr.it_mkLambda_or_LetIn c ctx in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index a8f1a49086..a1cdc718d7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -348,25 +348,11 @@ GRAMMAR EXTEND Gram
   (* Simple definitions *)
   def_body:
     [ [ bl = binders; ":="; red = reduce; c = lconstr ->
-      { if List.exists (function CLocalPattern _ -> true | _ -> false) bl
-      then
-        (* FIXME: "red" will be applied to types in bl and Cast with remain *)
-        let c = mkLambdaCN ~loc bl c in
-        DefineBody ([], red, c, None)
-      else
-        (match c with
-        | { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t)
-        | _ -> DefineBody (bl, red, c, None)) }
+        { match c.CAst.v with
+          | CCast(c, Glob_term.CastConv t) -> DefineBody (bl, red, c, Some t)
+          | _ -> DefineBody (bl, red, c, None) }
     | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
-        { let ((bl, c), tyo) =
-          if List.exists (function CLocalPattern _ -> true | _ -> false) bl
-          then
-            (* FIXME: "red" will be applied to types in bl and Cast with remain *)
-            let c = CAst.make ~loc @@ CCast (c, CastConv t) in
-            (([],mkLambdaCN ~loc bl c), None)
-          else ((bl, c), Some t)
-        in
-        DefineBody (bl, red, c, tyo) }
+        { DefineBody (bl, red, c, Some t) }
     | bl = binders; ":"; t = lconstr ->
         { ProveBody (bl, t) } ] ]
   ;