Merge PR #9292: Fixing some wrong scopes of variables in the interpretation of the "in" clause of a "match"

4 files changed, 39 insertions, 29 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 7bc5d090b4..95a0039b0a 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -293,9 +293,6 @@ let ids_of_pattern_list =
     (List.fold_left (cases_pattern_fold_names Id.Set.add))
     Id.Set.empty
 
-let ids_of_cases_indtype p =
-  cases_pattern_fold_names Id.Set.add Id.Set.empty p
-
 let ids_of_cases_tomatch tms =
   List.fold_right
     (fun (_, ona, indnal) l ->
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 8c735edfc9..f1a8ed202f 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -113,9 +113,6 @@ val map_constr_expr_with_binders :
 val replace_vars_constr_expr :
   Id.t Id.Map.t -> constr_expr -> constr_expr
 
-(** Specific function for interning "in indtype" syntax of "match" *)
-val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
-
 val free_vars_of_constr_expr : constr_expr -> Id.Set.t
 val occur_var_constr_expr : Id.t -> constr_expr -> bool
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7aa85a0810..c8c38ffe05 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -573,12 +573,17 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id =
   (* TODO binders *)
   next_ident_away_from id (fun id -> Id.Set.mem id fvs3)
 
-let is_var store pat =
+let is_patvar c =
+  match DAst.get c with
+  | PatVar _ -> true
+  | _ -> false
+
+let is_patvar_store store pat =
   match DAst.get pat with
   | PatVar na -> ignore(store na); true
   | _ -> false
 
-let out_var pat =
+let out_patvar pat =
   match pat.v with
   | CPatAtom (Some qid) when qualid_is_ident qid ->
     Name (qualid_basename qid)
@@ -600,7 +605,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in
     let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
     let pat, na = match disjpat with
-    | [pat] when is_var store pat -> let na = get () in None, na
+    | [pat] when is_patvar_store store pat -> let na = get () in None, na
     | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
     (renaming,env), pat, na
   with Not_found ->
@@ -610,7 +615,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     let env = set_env_scopes env scopes in
     if onlyident then
       (* Do not try to interpret a variable as a constructor *)
-      let na = out_var pat in
+      let na = out_patvar pat in
       let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in
       (renaming,env), None, na
     else
@@ -618,7 +623,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
       let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
       let pat, na =
         match disjpat with
-        | [pat] when is_var store pat -> let na = get () in None, na
+        | [pat] when is_patvar_store store pat -> let na = get () in None, na
         | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
       (renaming,env), pat, na
   with Not_found ->
@@ -743,7 +748,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
         let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
           let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
           if onlyident then
-            let na = out_var c in term_of_name na, None
+            let na = out_patvar c in term_of_name na, None
           else
             let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
             match disjpat with
@@ -805,7 +810,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
       (* and since we are only interested in the pattern as a term *)
       let env = reset_hidden_inductive_implicit_test env in
       if onlyident then
-        term_of_name (out_var pat)
+        term_of_name (out_patvar pat)
       else
         let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
         match disjpat with
@@ -1741,7 +1746,7 @@ let intern_ind_pattern genv ntnvars scopes pat =
       let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in
       (with_letin,
        match product_of_cases_patterns empty_alias idslpl with
-       | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
+       | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin)
        | _ -> error_bad_inductive_type ?loc)
     | x -> error_bad_inductive_type ?loc
 
@@ -1979,30 +1984,30 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	end
     | CCases (sty, rtnpo, tms, eqns) ->
         let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
-	  Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc)
-            (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na)
-	    inb) Id.Set.empty tms in
+          (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na))
+          Id.Set.empty tms in
         (* as, in & return vars *)
         let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in
-        let tms,ex_ids,match_from_in = List.fold_right
-	  (fun citm (inds,ex_ids,matchs) ->
-	    let ((tm,ind),extra_id,match_td) = intern_case_item env forbidden_vars citm in
-	    (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs)
-	  tms ([],Id.Set.empty,[]) in
+        let tms,ex_ids,aliases,match_from_in = List.fold_right
+          (fun citm (inds,ex_ids,asubst,matchs) ->
+            let ((tm,ind),extra_id,(ind_ids,alias_subst,match_td)) =
+              intern_case_item env forbidden_vars citm in
+            (tm,ind)::inds,
+            Id.Set.union ind_ids (Option.fold_right Id.Set.add extra_id ex_ids),
+            merge_subst alias_subst asubst,
+            List.rev_append match_td matchs)
+          tms ([],Id.Set.empty,Id.Map.empty,[]) in
         let env' = Id.Set.fold
           (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var))
 	  (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
         (* PatVars before a real pattern do not need to be matched *)
         let stripped_match_from_in =
-          let is_patvar c = match DAst.get c with
-          | PatVar _ -> true
-          | _ -> false
-          in
           let rec aux = function
 	    | [] -> []
 	    | (_, c) :: q when is_patvar c -> aux q
 	    | l -> l
 	  in aux match_from_in in
+        let rtnpo = Option.map (replace_vars_constr_expr aliases) rtnpo in
         let rtnpo = match stripped_match_from_in with
 	  | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *)
 	  | l ->
@@ -2150,7 +2155,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     (* the "in" part *)
     let match_td,typ = match t with
     | Some t ->
-        let with_letin,(ind,l) = intern_ind_pattern globalenv ntnvars (None,env.scopes) t in
+        let with_letin,(ind,ind_ids,alias_subst,l) =
+          intern_ind_pattern globalenv ntnvars (None,env.scopes) t in
 	let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in
 	let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in
 	(* for "in Vect n", we answer (["n","n"],[(loc,"n")])
@@ -2186,9 +2192,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	  let _,args_rel =
 	    List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
 	  canonize_args args_rel l forbidden_names_for_gen [] [] in
-        match_to_do, Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal))
+        (Id.Set.of_list (List.map (fun id -> id.CAst.v) ind_ids),alias_subst,match_to_do),
+        Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal))
     | None ->
-      [], None in
+      (Id.Set.empty,Id.Map.empty,[]), None in
     (tm',(na.CAst.v, typ)), extra_id, match_td
 
   and intern_impargs c env l subscopes args =
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 52fe98ac07..232ac17cbf 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1873,3 +1873,12 @@ Check match niln in listn O return O=O with niln => eq_refl end.
 (* (was failing up to May 2017) *)
 
 Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end.
+
+(* A test about binding variables of "in" clause of "match" *)
+(* (was failing from 8.5 to Dec 2018) *)
+
+Check match O in nat return nat with O => O | _ => O end.
+
+(* Checking that aliases are substituted in the correct order *)
+
+Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0.