aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml5
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comDefinition.ml2
-rw-r--r--vernac/comFixpoint.ml5
-rw-r--r--vernac/comInductive.ml8
-rw-r--r--vernac/himsg.ml3
-rw-r--r--vernac/obligations.ml13
-rw-r--r--vernac/record.ml270
-rw-r--r--vernac/record.mli11
-rw-r--r--vernac/vernacentries.ml145
10 files changed, 298 insertions, 166 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 382d18b09..26d105ecf 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -116,9 +116,8 @@ let instance_hook k info global imps ?hook cst =
let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
let kind = IsDefinition Instance in
let sigma =
- let env = Global.env () in
- let levels = Univ.LSet.union (Univops.universes_of_constr env termtype)
- (Univops.universes_of_constr env term) in
+ let levels = Univ.LSet.union (Univops.universes_of_constr termtype)
+ (Univops.universes_of_constr term) in
Evd.restrict_universe_context sigma levels
in
let uctx = Evd.check_univ_decl ~poly sigma decl in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index a8ac52846..750ed35cb 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -163,7 +163,7 @@ let do_assumptions kind nl l =
let nf_evar c = EConstr.to_constr sigma c in
let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
let t = nf_evar t in
- let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in
+ let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in
uvars, (coe,t,imps))
Univ.LSet.empty l
in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index f55c852c0..a8d794642 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -93,7 +93,7 @@ let interp_definition pl bl poly red_option c ctypopt =
let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in
(* Keep only useful universes. *)
let uvars_fold uvars c =
- Univ.LSet.union uvars (universes_of_constr env evd (of_constr c))
+ Univ.LSet.union uvars (universes_of_constr evd (of_constr c))
in
let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in
let evd = Evd.restrict_universe_context evd uvars in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 1d1cc62de..37258c2d4 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -262,7 +262,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
let env = Global.env() in
let indexes = search_guard env indexes fixdecls in
let fiximps = List.map (fun (n,r,p) -> r) fiximps in
- let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in
+ let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
let fixdecls =
List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
let evd = Evd.from_ctx ctx in
@@ -295,8 +295,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
let fixdefs = List.map Option.get fixdefs in
let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
- let env = Global.env () in
- let vars = Univops.universes_of_constr env (List.hd fixdecls) in
+ let vars = Univops.universes_of_constr (List.hd fixdecls) in
let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
let evd = Evd.from_ctx ctx in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 6057c05f5..0387b32ba 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -126,7 +126,7 @@ let make_conclusion_flexible sigma ty poly =
else sigma
let is_impredicative env u =
- u = Prop Null || (is_impredicative_set env && u = Prop Pos)
+ u = Prop || (is_impredicative_set env && u = Set)
let interp_ind_arity env sigma ind =
let c = intern_gen IsType env sigma ind.ind_arity in
@@ -245,7 +245,7 @@ let solve_constraints_system levels level_bounds =
let inductive_levels env evd poly arities inds =
let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
let levels = List.map (fun (x,(ctx,a)) ->
- if a = Prop Null then None
+ if a = Prop then None
else Some (univ_of_sort a)) destarities
in
let cstrs_levels, min_levels, sizes =
@@ -298,14 +298,14 @@ let inductive_levels env evd poly arities inds =
(** "Polymorphic" type constraint and more than one constructor,
should not land in Prop. Add constraint only if it would
land in Prop directly (no informative arguments as well). *)
- Evd.set_leq_sort env evd (Prop Pos) du
+ Evd.set_leq_sort env evd Set du
else evd
in
let duu = Sorts.univ_of_sort du in
let evd =
if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
- Evd.set_eq_sort env evd (Prop Null) du
+ Evd.set_eq_sort env evd Prop du
else evd
else Evd.set_eq_sort env evd (Type cu) du
in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 5d671ef52..534e58f9c 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -871,9 +871,6 @@ let explain_not_match_error = function
pr_enum (function Name id -> Id.print id | _ -> str "_") nal
| NotEqualInductiveAliases ->
str "Aliases to inductive types do not match"
- | NoTypeConstraintExpected ->
- strbrk "a definition whose type is constrained can only be subtype " ++
- strbrk "of a definition whose type is itself constrained"
| CumulativeStatusExpected b ->
let status b = if b then str"cumulative" else str"non-cumulative" in
str "a " ++ status b ++ str" declaration was expected, but a " ++
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1ab24b670..fa6a9adf1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -480,10 +480,9 @@ let declare_definition prg =
let fix_exn = Hook.get get_fix_exn () in
let typ = nf typ in
let body = nf body in
- let env = Global.env () in
let uvars = Univ.LSet.union
- (Univops.universes_of_constr env typ)
- (Univops.universes_of_constr env body) in
+ (Univops.universes_of_constr typ)
+ (Univops.universes_of_constr body) in
let uctx = UState.restrict prg.prg_ctx uvars in
let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in
let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
@@ -865,7 +864,7 @@ let obligation_terminator name num guard hook auto pf =
else UState.union prg.prg_ctx ctx
in
let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
- let (_, obl) = declare_obligation prg obl body ty uctx in
+ let (defined, obl) = declare_obligation prg obl body ty uctx in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
let prg_ctx =
@@ -874,10 +873,12 @@ let obligation_terminator name num guard hook auto pf =
polymorphic obligation with the existing ones *)
UState.union prg.prg_ctx ctx
else
- (** The first obligation declares the univs of the constant,
+ (** The first obligation, if defined,
+ declares the univs of the constant,
each subsequent obligation declares its own additional
universes and constraints if any *)
- UState.make (Global.universes ())
+ if defined then UState.make (Global.universes ())
+ else ctx
in
let prg = { prg with prg_ctx } in
try
diff --git a/vernac/record.ml b/vernac/record.ml
index 940859723..7a8ce7d25 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -100,7 +100,7 @@ let binder_of_decl = function
let binders_of_decls = List.map binder_of_decl
-let typecheck_params_and_fields finite def id poly pl t ps nots fs =
+let typecheck_params_and_fields finite def poly pl ps records =
let env0 = Global.env () in
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
let _ =
@@ -117,7 +117,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps
in
let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in
- let sigma, typ, sort, template = match t with
+ let fold (sigma, template) (_, t, _, _) = match t with
| Some t ->
let env = EConstr.push_rel_context newps env0 in
let poly =
@@ -132,28 +132,36 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
match Evd.is_sort_variable sigma s' with
| Some l ->
let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in
- sigma, s, s', true
+ (sigma, template), (s, s')
| None ->
- sigma, s, s', false
- else sigma, s, s', false)
+ (sigma, false), (s, s')
+ else (sigma, false), (s, s'))
| _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
| None ->
let uvarkind = Evd.univ_flexible_alg in
let sigma, s = Evd.new_sort_variable uvarkind sigma in
- sigma, EConstr.mkSort s, s, true
+ (sigma, template), (EConstr.mkSort s, s)
in
- let arity = EConstr.it_mkProd_or_LetIn typ newps in
- let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in
+ let (sigma, template), typs = List.fold_left_map fold (sigma, true) records in
+ let arities = List.map (fun (typ, _) -> EConstr.it_mkProd_or_LetIn typ newps) typs in
+ let fold accu (id, _, _, _) arity = EConstr.push_rel (LocalAssum (Name id,arity)) accu in
+ let env_ar = EConstr.push_rel_context newps (List.fold_left2 fold env0 records arities) in
let assums = List.filter is_local_assum newps in
- let params = List.map (RelDecl.get_name %> Name.get_id) assums in
- let ty = Inductive (params,(finite != Declarations.BiFinite)) in
- let impls_env = compute_internalization_env env0 sigma ~impls:impls_env ty [id] [arity] [imps] in
- let env2,sigma,impls,newfs,data =
- interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs)
+ let impls_env =
+ let params = List.map (RelDecl.get_name %> Name.get_id) assums in
+ let ty = Inductive (params, (finite != Declarations.BiFinite)) in
+ let ids = List.map (fun (id, _, _, _) -> id) records in
+ let imps = List.map (fun _ -> imps) arities in
+ compute_internalization_env env0 sigma ~impls:impls_env ty ids arities imps
in
+ let fold sigma (_, _, nots, fs) arity =
+ let _, sigma, impls, newfs, _ = interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) in
+ (sigma, (impls, newfs))
+ in
+ let (sigma, data) = List.fold_left2_map fold sigma records arities in
let sigma =
Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma (Evd.from_env env_ar) in
- let sigma, typ =
+ let fold sigma (typ, sort) (_, newfs) =
let _, univ = compute_constructor_level sigma env_ar newfs in
if not def && (Sorts.is_prop sort ||
(Sorts.is_set sort && is_impredicative_set env0)) then
@@ -164,20 +172,24 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
(* We can assume that the level in aritysort is not constrained
and clear it, if it is flexible *)
- Evd.set_eq_sort env_ar sigma (Prop Pos) sort,
- EConstr.mkSort (Sorts.sort_of_univ univ)
+ Evd.set_eq_sort env_ar sigma Set sort, EConstr.mkSort (Sorts.sort_of_univ univ)
else sigma, typ
in
+ let (sigma, typs) = List.fold_left2_map fold sigma typs data in
let sigma = Evd.minimize_universes sigma in
- let newfs = List.map (EConstr.to_rel_decl sigma) newfs in
let newps = List.map (EConstr.to_rel_decl sigma) newps in
- let typ = EConstr.to_constr sigma typ in
- let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in
let univs = Evd.check_univ_decl ~poly sigma decl in
let ubinders = Evd.universe_binders sigma in
- List.iter (iter_constr ce) (List.rev newps);
+ let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in
+ let () = List.iter (iter_constr ce) (List.rev newps) in
+ let map (impls, newfs) typ =
+ let newfs = List.map (EConstr.to_rel_decl sigma) newfs in
+ let typ = EConstr.to_constr sigma typ in
List.iter (iter_constr ce) (List.rev newfs);
- ubinders, univs, typ, template, imps, newps, impls, newfs
+ (typ, impls, newfs)
+ in
+ let ans = List.map2 map data typs in
+ ubinders, univs, template, newps, imps, ans
let degenerate_decl decl =
let id = match RelDecl.get_name decl with
@@ -261,9 +273,10 @@ let subst_projection fid l c =
raise (NotDefinable (MissingProj (fid,List.rev !bad_projs)));
c''
-let instantiate_possibly_recursive_type indu paramdecls fields =
+let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in
- Termops.substl_rel_context (subst@[mkIndU indu]) fields
+ let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in
+ Termops.substl_rel_context (subst @ subst') fields
let warn_non_primitive_record =
CWarnings.create ~name:"non-primitive-record" ~category:"record"
@@ -281,19 +294,18 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
| Monomorphic_const_entry ctx -> Univ.Instance.empty
in
let paramdecls = Inductive.inductive_paramdecls (mib, u) in
- let indu = indsp, u in
let r = mkIndU (indsp,u) in
let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*)
let x = Name binder_name in
- let fields = instantiate_possibly_recursive_type indu paramdecls fields in
+ let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
let primitive =
if !primitive_flag then
let is_primitive =
match mib.mind_record with
- | Some (Some _) -> true
- | Some None | None -> false
+ | PrimRecord _ -> true
+ | FakeRecord | NotRecord -> false
in
if not is_primitive then
warn_non_primitive_record (env,indsp);
@@ -374,12 +386,9 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
open Typeclasses
-let declare_structure finite ubinders univs id idbuild paramimpls params arity template
- fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers =
- let nparams = List.length params and nfields = List.length fields in
- let args = Context.Rel.to_extended_list mkRel nfields params in
- let ind = applist (mkRel (1+nparams+nfields), args) in
- let type_constructor = it_mkProd_or_LetIn ind fields in
+
+let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
+ let nparams = List.length params in
let template, ctx =
match univs with
| Monomorphic_ind_entry ctx ->
@@ -389,37 +398,51 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
| Cumulative_ind_entry cumi ->
false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
in
- let binder_name =
+ let binder_name =
match name with
- | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id))
+ | None ->
+ let map (id, _, _, _, _, _, _) =
+ Id.of_string (Unicode.lowercase_first_char (Id.to_string id))
+ in
+ Array.map_of_list map record_data
| Some n -> n
in
- let mie_ind =
+ let ntypes = List.length record_data in
+ let mk_block i (id, idbuild, arity, _, fields, _, _) =
+ let nfields = List.length fields in
+ let args = Context.Rel.to_extended_list mkRel nfields params in
+ let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
+ let type_constructor = it_mkProd_or_LetIn ind fields in
{ mind_entry_typename = id;
mind_entry_arity = arity;
mind_entry_template = template;
mind_entry_consnames = [idbuild];
mind_entry_lc = [type_constructor] }
in
+ let blocks = List.mapi mk_block record_data in
let mie =
{ mind_entry_params = List.map degenerate_decl params;
mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
mind_entry_finite = finite;
- mind_entry_inds = [mie_ind];
+ mind_entry_inds = blocks;
mind_entry_private = None;
mind_entry_universes = univs;
}
in
let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
- let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in
- let rsp = (kn,0) in (* This is ind path of idstruc *)
- let cstr = (rsp,1) in
- let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in
- let build = ConstructRef cstr in
- let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in
- let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
- Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
- rsp
+ let impls = List.map (fun _ -> paramimpls, []) record_data in
+ let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls in
+ let map i (_, _, _, fieldimpls, fields, is_coe, coers) =
+ let rsp = (kn, i) in (* This is ind path of idstruc *)
+ let cstr = (rsp, 1) in
+ let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in
+ let build = ConstructRef cstr in
+ let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in
+ let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
+ let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in
+ rsp
+ in
+ List.mapi map record_data
let implicits_of_context ctx =
List.map_i (fun i name ->
@@ -431,22 +454,22 @@ let implicits_of_context ctx =
1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
let declare_class finite def cum ubinders univs id idbuild paramimpls params arity
- template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities =
+ template fieldimpls fields ?(kind=StructureComponent) coers priorities =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
let len = List.length params in
let impls = implicits_of_context params in
List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
in
- let binder_name = Namegen.next_ident_away (snd id) (Termops.vars_of_env (Global.env())) in
- let impl, projs =
+ let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in
+ let data =
match fields with
| [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def ->
let class_body = it_mkLambda_or_LetIn field params in
let class_type = it_mkProd_or_LetIn arity params in
let class_entry =
Declare.definition_entry ~types:class_type ~univs class_body in
- let cst = Declare.declare_constant (snd id)
+ let cst = Declare.declare_constant id
(DefinitionEntry class_entry, IsDefinition Definition)
in
let cstu = (cst, match univs with
@@ -473,7 +496,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
| Some b -> Some ((if b then Backward else Forward), List.hd priorities)
| None -> None
in
- cref, [Name proj_name, sub, Some proj_cst]
+ [cref, [Name proj_name, sub, Some proj_cst]]
| _ ->
let univs =
match univs with
@@ -485,18 +508,21 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
| Monomorphic_const_entry univs ->
Monomorphic_ind_entry univs
in
- let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls
- params arity template fieldimpls fields
- ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields)
- in
+ let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in
+ let inds = declare_structure Declarations.BiFinite ubinders univs paramimpls
+ params template ~kind:Method ~name:[|binder_name|] record_data
+ in
let coers = List.map2 (fun coe pri ->
Option.map (fun b ->
if b then Backward, pri else Forward, pri) coe)
coers priorities
in
- let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y)
- (List.rev fields) coers (Recordops.lookup_projections ind)
- in IndRef ind, l
+ let map ind =
+ let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y)
+ (List.rev fields) coers (Recordops.lookup_projections ind)
+ in IndRef ind, l
+ in
+ List.map map inds
in
let ctx_context =
List.map (fun decl ->
@@ -517,16 +543,19 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
| Monomorphic_const_entry _ ->
Univ.AUContext.empty, ctx_context, fields
in
- let k =
- { cl_univs = univs;
- cl_impl = impl;
- cl_strict = !typeclasses_strict;
- cl_unique = !typeclasses_unique;
- cl_context = ctx_context;
- cl_props = fields;
- cl_projs = projs }
- in
+ let map (impl, projs) =
+ let k =
+ { cl_univs = univs;
+ cl_impl = impl;
+ cl_strict = !typeclasses_strict;
+ cl_unique = !typeclasses_unique;
+ cl_context = ctx_context;
+ cl_props = fields;
+ cl_projs = projs }
+ in
add_class k; impl
+ in
+ List.map map data
let add_constant_class cst =
@@ -562,48 +591,87 @@ let add_inductive_class ind =
cl_unique = !typeclasses_unique }
in add_class k
+let warn_already_existing_class =
+ CWarnings.create ~name:"already-existing-class" ~category:"automation" Pp.(fun g ->
+ Printer.pr_global g ++ str " is already declared as a typeclass.")
+
let declare_existing_class g =
- match g with
- | ConstRef x -> add_constant_class x
- | IndRef x -> add_inductive_class x
- | _ -> user_err ~hdr:"declare_existing_class"
- (Pp.str"Unsupported class type, only constants and inductives are allowed")
+ if Typeclasses.is_class g then warn_already_existing_class g
+ else
+ match g with
+ | ConstRef x -> add_constant_class x
+ | IndRef x -> add_inductive_class x
+ | _ -> user_err ~hdr:"declare_existing_class"
+ (Pp.str"Unsupported class type, only constants and inductives are allowed")
open Vernacexpr
-(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
- list telling if the corresponding fields must me declared as coercions
- or subinstances. *)
-let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl)),ps,cfs,idbuild,s) =
- let cfs,notations = List.split cfs in
- let cfs,priorities = List.split cfs in
- let coers,fs = List.split cfs in
- let extract_name acc = function
+let check_unique_names records =
+ let extract_name acc (((_, bnd), _), _) = match bnd with
Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc
| Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc
| _ -> acc in
- let allnames = idstruc::(List.fold_left extract_name [] fs) in
- let () = match List.duplicates Id.equal allnames with
+ let allnames =
+ List.fold_left (fun acc (_, id, _, _, cfs, _, _) ->
+ id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records
+ in
+ match List.duplicates Id.equal allnames with
| [] -> ()
| id :: _ -> user_err (str "Two objects have the same name" ++ spc () ++ quote (Id.print id))
- in
+
+let check_priorities kind records =
let isnot_class = match kind with Class false -> false | _ -> true in
- if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
- user_err Pp.(str "Priorities only allowed for type class substructures");
- (* Now, younger decl in params and fields is on top *)
- let pl, univs, arity, template, implpars, params, implfs, fields =
+ let has_priority (_, _, _, _, cfs, _, _) =
+ List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs
+ in
+ if isnot_class && List.exists has_priority records then
+ user_err Pp.(str "Priorities only allowed for type class substructures")
+
+let extract_record_data records =
+ let map (is_coe, id, _, _, cfs, idbuild, s) =
+ let fs = List.map (fun (((_, f), _), _) -> f) cfs in
+ id.CAst.v, s, List.map snd cfs, fs
+ in
+ let data = List.map map records in
+ let pss = List.map (fun (_, _, _, ps, _, _, _) -> ps) records in
+ let ps = match pss with
+ | [] -> CErrors.anomaly (str "Empty record block")
+ | ps :: rem ->
+ let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 in
+ let () =
+ if not (List.for_all (eq_local_binders ps) rem) then
+ user_err (str "Parameters should be syntactically the \
+ same for each inductive type.")
+ in
+ ps
+ in
+ (** FIXME: Same issue as #7754 *)
+ let _, _, pl, _, _, _, _ = List.hd records in
+ pl, ps, data
+
+(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
+ list telling if the corresponding fields must me declared as coercions
+ or subinstances. *)
+let definition_structure kind cum poly finite records =
+ let () = check_unique_names records in
+ let () = check_priorities kind records in
+ let pl, ps, data = extract_record_data records in
+ let pl, univs, template, params, implpars, data =
States.with_state_protection (fun () ->
- typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in
+ typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in
match kind with
| Class def ->
- let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
- declare_class finite def cum pl univs (loc,idstruc) idbuild
- implpars params arity template implfs fields is_coe coers priorities
+ let (_, id, _, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
+ | [r], [d] -> r, d
+ | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
+ in
+ let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in
+ let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
+ declare_class finite def cum pl univs id.CAst.v idbuild
+ implpars params arity template implfs fields coers priorities
| _ ->
- let implfs = List.map
- (fun impls -> implpars @ Impargs.lift_implicits
- (succ (List.length params)) impls) implfs
- in
+ let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
+ let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
let univs =
match univs with
| Polymorphic_const_entry univs ->
@@ -614,7 +682,11 @@ let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl)
| Monomorphic_const_entry univs ->
Monomorphic_ind_entry univs
in
- let ind = declare_structure finite pl univs idstruc
- idbuild implpars params arity template implfs
- fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) in
- IndRef ind
+ let map (arity, implfs, fields) (is_coe, id, _, _, cfs, idbuild, _) =
+ let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
+ let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in
+ id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
+ in
+ let data = List.map2 map data records in
+ let inds = declare_structure finite pl univs implpars params template data in
+ List.map (fun ind -> IndRef ind) inds
diff --git a/vernac/record.mli b/vernac/record.mli
index b2c039f0b..7cf7da1e2 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,9 +26,14 @@ val declare_projections :
(Name.t * bool) list * Constant.t option list
val definition_structure :
- inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
- Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
+ inductive_kind -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
+ Declarations.recursivity_kind ->
+ (coercion_flag *
+ Names.lident *
+ universe_decl_expr option *
+ local_binder_expr list *
(local_decl_expr with_instance with_priority with_notation) list *
- Id.t * constr_expr option -> GlobRef.t
+ Id.t * constr_expr option) list ->
+ GlobRef.t list
val declare_existing_class : GlobRef.t -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 479482095..6d1abeca1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -263,15 +263,13 @@ let print_namespace ns =
let matches mp = match match_modulepath ns mp with
| Some [] -> true
| _ -> false in
- let constants = (Global.env ()).Environ.env_globals.Environ.env_constants in
let constants_in_namespace =
- Cmap_env.fold (fun c (body,_) acc ->
- let kn = Constant.user c in
- if matches (KerName.modpath kn) then
- acc++fnl()++hov 2 (print_constant kn body)
- else
- acc
- ) constants (str"")
+ Environ.fold_constants (fun c body acc ->
+ let kn = Constant.user c in
+ if matches (KerName.modpath kn)
+ then acc++fnl()++hov 2 (print_constant kn body)
+ else acc)
+ (Global.env ()) (str"")
in
(print_list Id.print ns)++str":"++fnl()++constants_in_namespace
@@ -539,25 +537,36 @@ 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 && Flags.is_polymorphic_inductive_cumulativity ()
-let vernac_record cum k poly finite struc binders sort nameopt cfs =
+let vernac_record cum k poly finite records =
let is_cumulative = should_treat_as_cumulative cum poly in
- let const = match nameopt with
- | None -> add_prefix "Build_" (fst (snd struc)).v
- | Some ({v=id} as lid) ->
- Dumpglob.dump_definition lid false "constr"; id in
- if Dumpglob.dump () then (
- Dumpglob.dump_definition (fst (snd struc)) false "rec";
- List.iter (fun (((_, x), _), _) ->
- match x with
- | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> Dumpglob.dump_definition (make ?loc id) false "proj"
- | _ -> ()) cfs);
- ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort))
+ let map ((coe, (id, pl)), binders, sort, nameopt, cfs) =
+ let const = match nameopt with
+ | None -> add_prefix "Build_" id.v
+ | Some lid ->
+ let () = Dumpglob.dump_definition lid false "constr" in
+ lid.v
+ in
+ let () =
+ if Dumpglob.dump () then
+ let () = Dumpglob.dump_definition id false "rec" in
+ let iter (((_, x), _), _) = match x with
+ | Vernacexpr.AssumExpr ({loc;v=Name id}, _) ->
+ Dumpglob.dump_definition (make ?loc id) false "proj"
+ | _ -> ()
+ in
+ List.iter iter cfs
+ in
+ coe, id, pl, binders, cfs, const, sort
+ in
+ let records = List.map map records in
+ ignore(Record.definition_structure k is_cumulative poly finite records)
(** When [poly] is true the type is declared polymorphic. When [lo] is true,
then the type is declared private (as per the [Private] keyword). [finite]
indicates whether the type is inductive, co-inductive or
neither. *)
let vernac_inductive ~atts cum lo finite indl =
+ let open Pp in
if Dumpglob.dump () then
List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
match cstrs with
@@ -567,35 +576,85 @@ let vernac_inductive ~atts cum lo finite indl =
Dumpglob.dump_definition lid false "constr") cstrs
| _ -> () (* dumping is done by vernac_record (called below) *) )
indl;
+ let is_record = function
+ | ((_ , _ , _ , _, RecordDecl _), _) -> true
+ | _ -> false
+ in
+ let is_constructor = function
+ | ((_ , _ , _ , _, Constructors _), _) -> true
+ | _ -> false
+ in
+ let is_defclass = match indl with
+ | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l)
+ | _ -> None
+ in
+ if Option.has_some is_defclass then
+ (** Definitional class case *)
+ let (id, bl, c, l) = Option.get is_defclass in
+ let (coe, (lid, ce)) = l in
+ let coe' = if coe then Some true else None in
+ let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
+ vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
+ else if List.for_all is_record indl then
+ (** Mutual record case *)
+ let check_kind ((_, _, _, kind, _), _) = match kind with
+ | Variant ->
+ user_err (str "The Variant keyword does not support syntax { ... }.")
+ | Record | Structure | Class _ | Inductive_kw | CoInductive -> ()
+ in
+ let () = List.iter check_kind indl in
+ let check_where ((_, _, _, _, _), wh) = match wh with
+ | [] -> ()
+ | _ :: _ ->
+ user_err (str "where clause not supported for records")
+ in
+ let () = List.iter check_where indl in
+ let unpack ((id, bl, c, _, decl), _) = match decl with
+ | RecordDecl (oc, fs) ->
+ (id, bl, c, oc, fs)
+ | Constructors _ -> assert false (** ruled out above *)
+ in
+ let ((_, _, _, kind, _), _) = List.hd indl in
+ let kind = match kind with Class _ -> Class false | _ -> kind in
+ let recordl = List.map unpack indl in
+ vernac_record cum kind atts.polymorphic finite recordl
+ else if List.for_all is_constructor indl then
+ (** Mutual inductive case *)
+ let check_kind ((_, _, _, kind, _), _) = match kind with
+ | (Record | Structure) ->
+ user_err (str "The Record keyword is for types defined using the syntax { ... }.")
+ | Class _ ->
+ user_err (str "Inductive classes not supported")
+ | Variant | Inductive_kw | CoInductive -> ()
+ in
+ let () = List.iter check_kind indl in
+ let check_name ((na, _, _, _, _), _) = match na with
+ | (true, _) ->
+ user_err (str "Variant types do not handle the \"> Name\" \
+ syntax, which is reserved for records. Use the \":>\" \
+ syntax on constructors instead.")
+ | _ -> ()
+ in
+ let () = List.iter check_name indl in
+ let unpack (((_, id) , bl, c, _, decl), ntn) = match decl with
+ | Constructors l -> (id, bl, c, l), ntn
+ | RecordDecl _ -> assert false (* ruled out above *)
+ in
+ let indl = List.map unpack indl in
+ let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
+ ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite
+ else
+ user_err (str "Mixed record-inductive definitions are not allowed")
+(*
+
match indl with
- | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] ->
- user_err Pp.(str "The Record keyword is for types defined using the syntax { ... }.")
- | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
- user_err Pp.(str "The Variant keyword does not support syntax { ... }.")
- | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
- vernac_record cum (match b with Class _ -> Class false | _ -> b)
- atts.polymorphic finite id bl c oc fs
| [ ( id , bl , c , Class _, Constructors [l]), [] ] ->
let f =
let (coe, ({loc;v=id}, ce)) = l in
let coe' = if coe then Some true else None in
(((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), [])
- in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f]
- | [ ( _ , _, _, Class _, Constructors _), [] ] ->
- user_err Pp.(str "Inductive classes not supported")
- | [ ( id , bl , c , Class _, _), _ :: _ ] ->
- user_err Pp.(str "where clause not supported for classes")
- | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] ->
- user_err Pp.(str "where clause not supported for (co)inductive records")
- | _ -> let unpack = function
- | ( (false, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn
- | ( (true,_),_,_,_,Constructors _),_ ->
- user_err Pp.(str "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead.")
- | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
- in
- let indl = List.map unpack indl in
- let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
- ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite
+ in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
+ *)
let vernac_fixpoint ~atts discharge l =
let local = enforce_locality_exp atts.locality discharge in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 15:16:12 +0000