aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/comInductive.ml26
-rw-r--r--vernac/egramcoq.ml8
-rw-r--r--vernac/g_vernac.mlg4
-rw-r--r--vernac/metasyntax.ml17
-rw-r--r--vernac/ppvernac.ml6
-rw-r--r--vernac/vernacentries.ml43
-rw-r--r--vernac/vernacexpr.ml7
7 files changed, 59 insertions, 52 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/egramcoq.ml b/vernac/egramcoq.ml
index 5e98f5ddc0..3181bcc4bc 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -249,7 +249,6 @@ type (_, _) entry =
| TTName : ('self, lname) entry
| TTReference : ('self, qualid) entry
| TTBigint : ('self, string) entry
-| TTString : ('self, string) entry
| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
| TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
| TTPattern : int -> ('self, cases_pattern_expr) entry
@@ -370,14 +369,12 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
| TTName -> MayRecNo (Aentry Prim.name)
| TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders)
| TTBigint -> MayRecNo (Aentry Prim.bigint)
-| TTString -> MayRecNo (Aentry Prim.string)
| TTReference -> MayRecNo (Aentry Constr.global)
let interp_entry forpat e = match e with
| ETProdName -> TTAny TTName
| ETProdReference -> TTAny TTReference
| ETProdBigint -> TTAny TTBigint
-| ETProdString -> TTAny TTString
| ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
| ETProdPattern p -> TTAny (TTPattern p)
| ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat))
@@ -417,11 +414,6 @@ match e with
| ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v)))
| ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v)))
end
-| TTString ->
- begin match forpat with
- | ForConstr -> push_constr subst (CAst.make @@ CPrim (String v))
- | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (String v))
- end
| TTReference ->
begin match forpat with
| ForConstr -> push_constr subst (CAst.make @@ CRef (v, None))
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 97c9d23c68..d597707d12 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 }
@@ -1234,7 +1235,6 @@ GRAMMAR EXTEND Gram
syntax_extension_type:
[ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
| IDENT "bigint" -> { ETBigint }
- | IDENT "string" -> { ETString }
| IDENT "binder" -> { ETBinder true }
| IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
| IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index d39ee60c25..7794b0a37a 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -396,7 +396,7 @@ let unparsing_metavar i from typs =
let x = List.nth typs (i-1) in
let prec = unparsing_precedence_of_entry_type from x in
match x with
- | ETConstr _ | ETGlobal | ETBigint | ETString ->
+ | ETConstr _ | ETGlobal | ETBigint ->
UnpMetaVar (i,prec)
| ETPattern _ ->
UnpBinderMetaVar (i,prec)
@@ -686,7 +686,6 @@ let prod_entry_type = function
| ETIdent -> ETProdName
| ETGlobal -> ETProdReference
| ETBigint -> ETProdBigint
- | ETString -> ETProdString
| ETBinder _ -> assert false (* See check_binder_type *)
| ETConstr (s,_,p) -> ETProdConstr (s,p)
| ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
@@ -990,7 +989,7 @@ let set_entry_type from n etyps (x,typ) =
| ETConstr (s,bko,n), InternalProd ->
ETConstr (s,bko,(n,InternalProd))
| ETPattern (b,n), _ -> ETPattern (b,n)
- | (ETIdent | ETBigint | ETString | ETGlobal | ETBinder _ as x), _ -> x
+ | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
with Not_found ->
ETConstr (from,None,(make_lev n from,typ))
in (x,typ)
@@ -1012,7 +1011,7 @@ let join_auxiliary_recursive_types recvars etyps =
let internalization_type_of_entry_type = function
| ETBinder _ -> NtnInternTypeOnlyBinder
- | ETConstr _ | ETBigint | ETString | ETGlobal
+ | ETConstr _ | ETBigint | ETGlobal
| ETIdent | ETPattern _ -> NtnInternTypeAny
let set_internalization_type typs =
@@ -1034,7 +1033,7 @@ let make_interpretation_type isrec isonlybinding = function
(* Others *)
| ETIdent -> NtnTypeBinder NtnParsedAsIdent
| ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *)
- | ETBigint | ETString | ETGlobal -> NtnTypeConstr
+ | ETBigint | ETGlobal -> NtnTypeConstr
| ETBinder _ ->
if isrec then NtnTypeBinderList
else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
@@ -1098,8 +1097,6 @@ type entry_coercion_kind =
| IsEntryCoercion of notation_entry_level
| IsEntryGlobal of string * int
| IsEntryIdent of string * int
- | IsEntryNumeral of string * int
- | IsEntryString of string * int
let is_coercion = function
| Some (custom,n,_,[e]) ->
@@ -1111,8 +1108,6 @@ let is_coercion = function
else Some (IsEntryCoercion subentry)
| ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n))
| ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n))
- | ETBigint, InCustomEntry s -> Some (IsEntryNumeral (s,n))
- | ETString, InCustomEntry s -> Some (IsEntryString (s,n))
| _ -> None)
| Some _ -> assert false
| None -> None
@@ -1154,7 +1149,7 @@ let find_precedence custom lev etyps symbols onlyprint =
user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
(try match List.assoc x etyps, custom with
| ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test ()
- | (ETIdent | ETBigint | ETString | ETGlobal), _ ->
+ | (ETIdent | ETBigint | ETGlobal), _ ->
begin match lev with
| None ->
([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
@@ -1380,8 +1375,6 @@ let open_notation i (_, nobj) =
| Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry
| Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
| Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
- | Some (IsEntryNumeral (entry,n)) -> Notation.declare_custom_entry_has_numeral entry n
- | Some (IsEntryString (entry,n)) -> Notation.declare_custom_entry_has_string entry n
| None -> ())
end
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 0cf407619b..314c423f65 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -126,7 +126,6 @@ open Pputils
| ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n)
| ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
| ETBigint -> str "bigint"
- | ETString -> str "string"
| ETBinder true -> str "binder"
| ETBinder false -> str "closed binder"
@@ -811,11 +810,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 06:39:02 +0000