Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]

Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot

5 files changed, 54 insertions, 30 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index d711c9aea0..85f2bf3708 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -456,9 +456,19 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in
   let arities, relevances, arityconcl, indimpls = List.split4 arities in
 
-  let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in
+  let lift1_ctx ctx =
+    let t = EConstr.it_mkProd_or_LetIn EConstr.mkProp ctx in
+    let t = EConstr.Vars.lift 1 t in
+    let ctx, _ = EConstr.decompose_prod_assum sigma t in
+    ctx
+  in
+  let ctx_params_lifted, fullarities = CList.fold_left_map
+      (fun ctx_params c -> lift1_ctx ctx_params, EConstr.it_mkProd_or_LetIn c ctx_params)
+      ctx_params
+      arities
+  in
   let env_ar = push_types env_uparams indnames relevances fullarities in
-  let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
+  let env_ar_params = EConstr.push_rel_context ctx_params_lifted env_ar in
 
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in
@@ -509,6 +519,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
 let eq_local_binders bl1 bl2 =
   List.equal local_binder_eq bl1 bl2
 
+let eq_params (up1,p1) (up2,p2) =
+  eq_local_binders up1 up2 && Option.equal eq_local_binders p1 p2
+
 let extract_coercions indl =
   let mkqid (_,({CAst.v=id},_)) = qualid_of_ident id in
   let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in
@@ -519,7 +532,7 @@ let extract_params indl =
   match paramsl with
   | [] -> anomaly (Pp.str "empty list of inductive types.")
   | params::paramsl ->
-      if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str
+      if not (List.for_all (eq_params params) paramsl) then user_err Pp.(str
         "Parameters should be syntactically the same for each inductive type.");
       params
 
@@ -544,7 +557,12 @@ type uniform_inductive_flag =
 let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite =
   let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
-  let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
+  let indl = match params with
+    | uparams, Some params -> (uparams, params, indl)
+    | params, None -> match uniform with
+      | UniformParameters -> (params, [], indl)
+      | NonUniformParameters -> ([], params, indl)
+  in
   let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls);
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 97c9d23c68..882be6449d 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -395,9 +395,10 @@ GRAMMAR EXTEND Gram
   ;
   inductive_definition:
     [ [ oc = opt_coercion; id = ident_decl; indpar = binders;
+        extrapar = OPT [ "|"; p = binders -> { p } ];
         c = OPT [ ":"; c = lconstr -> { c } ];
         lc=opt_constructors_or_fields; ntn = decl_notation ->
-           { (((oc,id),indpar,c,lc),ntn) } ] ]
+           { (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ]
   ;
   constructor_list_or_record_decl:
     [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 0cf407619b..c6ba4e2c29 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -811,11 +811,12 @@ let string_of_definition_object_kind = let open Decls in function
           | RecordDecl (c,fs) ->
             pr_record_decl c fs
         in
-        let pr_oneind key (((coe,iddecl),indpar,s,lc),ntn) =
+        let pr_oneind key (((coe,iddecl),(indupar,indpar),s,lc),ntn) =
           hov 0 (
             str key ++ spc() ++
               (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
-              pr_and_type_binders_arg indpar ++
+              pr_and_type_binders_arg indupar ++
+              pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++
               pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++
               str" :=") ++ pr_constructor_list lc ++
             prlist (pr_decl_notation @@ pr_constr env sigma) ntn
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e469323f50..63fc587f71 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -623,18 +623,16 @@ let should_treat_as_cumulative cum poly =
     else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
   | None -> poly && is_polymorphic_inductive_cumulativity ()
 
-let uniform_att =
-  let get_uniform_inductive_parameters =
-    Goptions.declare_bool_option_and_ref
-      ~depr:false
-      ~key:["Uniform"; "Inductive"; "Parameters"]
-      ~value:false
-  in
-  let open Attributes.Notations in
-  Attributes.bool_attribute ~name:"uniform" ~on:"uniform" ~off:"nonuniform" >>= fun u ->
-  let u = match u with Some u -> u | None -> get_uniform_inductive_parameters () in
-  let u = if u then ComInductive.UniformParameters else ComInductive.NonUniformParameters in
-  return u
+let get_uniform_inductive_parameters =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Uniform"; "Inductive"; "Parameters"]
+    ~value:false
+
+let should_treat_as_uniform () =
+  if get_uniform_inductive_parameters ()
+  then ComInductive.UniformParameters
+  else ComInductive.NonUniformParameters
 
 let vernac_record ~template udecl cum k poly finite records =
   let cumulative = should_treat_as_cumulative cum poly in
@@ -682,6 +680,7 @@ let finite_of_kind = let open Declarations in function
     indicates whether the type is inductive, co-inductive or
     neither. *)
 let vernac_inductive ~atts cum lo kind indl =
+  let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
   let open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
@@ -710,12 +709,14 @@ let vernac_inductive ~atts cum lo kind indl =
   if Option.has_some is_defclass then
     (* Definitional class case *)
     let (id, bl, c, l) = Option.get is_defclass in
+    let bl = match bl with
+      | bl, None -> bl
+      | _ -> CErrors.user_err Pp.(str "Definitional classes do not support the \"|\" syntax.")
+    in
     let (coe, (lid, ce)) = l in
     let coe' = if coe then Some true else None in
     let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
-            { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true }
-    in
-    let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
+            { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
     vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (* Mutual record case *)
@@ -732,12 +733,15 @@ let vernac_inductive ~atts cum lo kind indl =
     let () = List.iter check_where indl in
     let unpack ((id, bl, c, decl), _) = match decl with
     | RecordDecl (oc, fs) ->
+      let bl = match bl with
+        | bl, None -> bl
+        | _ -> CErrors.user_err Pp.(str "Records do not support the \"|\" syntax.")
+      in
       (id, bl, c, oc, fs)
     | Constructors _ -> assert false (* ruled out above *)
     in
     let kind = match kind with Class _ -> Class false | _ -> kind in
     let recordl = List.map unpack indl in
-    let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
     vernac_record ~template udecl cum kind poly finite recordl
   else if List.for_all is_constructor indl then
     (* Mutual inductive case *)
@@ -761,12 +765,9 @@ let vernac_inductive ~atts cum lo kind indl =
     | RecordDecl _ -> assert false (* ruled out above *)
     in
     let indl = List.map unpack indl in
-    let (template, poly), uniform =
-      Attributes.(parse Notations.(template ++ polymorphic ++ uniform_att) atts)
-    in
     let cumulative = should_treat_as_cumulative cum poly in
-    ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly
-      ~private_ind:lo ~uniform finite
+    let uniform = should_treat_as_uniform () in
+    ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")
 
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 3610240634..45018a246c 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -163,12 +163,15 @@ type constructor_expr = (lident * constr_expr) with_coercion
 type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
   | RecordDecl of lident option * (local_decl_expr * record_field_attr) list
+type inductive_params_expr = local_binder_expr list * local_binder_expr list option
+(** If the option is nonempty the "|" marker was used *)
+
 type inductive_expr =
-  ident_decl with_coercion * local_binder_expr list * constr_expr option *
+  ident_decl with_coercion * inductive_params_expr * constr_expr option *
     constructor_list_or_record_decl_expr
 
 type one_inductive_expr =
-  lident * local_binder_expr list * constr_expr option * constructor_expr list
+  lident * inductive_params_expr * constr_expr option * constructor_expr list
 
 type typeclass_constraint = name_decl * Glob_term.binding_kind * constr_expr
 and typeclass_context = typeclass_constraint list