Helping issue #11659 by leaving only the Cast hack in the grammar.

We clean the hack bypassing the interpretation of "'pat" in binders
and move it to comDefinition.ml. In particular, we fix the exact
subterm to which Eval has to apply in the hack, and remove the
artificial cast we had introduced.

2 files changed, 45 insertions, 19 deletions

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 dd75693c5b..a6bbc2377e 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) } ] ]
   ;