aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml10
-rw-r--r--vernac/classes.mli2
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comDefinition.ml2
-rw-r--r--vernac/comFixpoint.ml5
-rw-r--r--vernac/comInductive.ml12
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/egramcoq.ml4
-rw-r--r--vernac/g_vernac.ml44
-rw-r--r--vernac/himsg.ml3
-rw-r--r--vernac/indschemes.ml4
-rw-r--r--vernac/indschemes.mli8
-rw-r--r--vernac/metasyntax.ml2
-rw-r--r--vernac/obligations.ml13
-rw-r--r--vernac/ppvernac.ml37
-rw-r--r--vernac/record.ml270
-rw-r--r--vernac/record.mli11
-rw-r--r--vernac/vernacentries.ml199
-rw-r--r--vernac/vernacentries.mli4
-rw-r--r--vernac/vernacexpr.ml78
20 files changed, 400 insertions, 272 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 8cf3895fb..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
@@ -229,10 +228,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
let sigma, c = interp_casted_constr_evars env' sigma term cty in
Some (Inr (c, subst)), sigma
| Some (Inl props) ->
- let get_id = CAst.map (function
- | Ident id' -> id'
- | Qualid id' -> snd (repr_qualid id'))
- in
+ let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
let props, rest =
List.fold_left
(fun (props, rest) decl ->
diff --git a/vernac/classes.mli b/vernac/classes.mli
index eea2a211d..bd30b2d60 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,7 +22,7 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
(** Instance declaration *)
-val existing_instance : bool -> reference -> Hints.hint_info_expr option -> unit
+val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
(** globality, reference, optional priority and pattern information *)
val declare_instance_constant :
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 b93e8d9ac..0387b32ba 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -44,8 +44,8 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
user_err ?loc
(strbrk"Cannot infer the non constant arguments of the conclusion of "
++ Id.print cs ++ str ".");
- let args = List.map (fun id -> CAst.(make ?loc @@ CRef(make ?loc @@ Ident id,None))) params in
- CAppExpl ((None,CAst.make ?loc @@ Ident name,None),List.rev args)
+ let args = List.map (fun id -> CAst.(make ?loc @@ CRef(qualid_of_ident ?loc id,None))) params in
+ CAppExpl ((None,qualid_of_ident ?loc name,None),List.rev args)
| c -> c
)
@@ -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/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index a6d7fccf3..eef7afbfb 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -44,7 +44,7 @@ let mkSubset sigma name typ prop =
let sigT = Lazy.from_fun build_sigma_type
-let make_qref s = CAst.make @@ Qualid (qualid_of_string s)
+let make_qref s = qualid_of_string s
let lt_ref = make_qref "Init.Peano.lt"
let rec telescope sigma l =
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 434e836d8..cc9be7b0e 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -229,7 +229,7 @@ type prod_info = production_level * production_position
type (_, _) entry =
| TTName : ('self, lname) entry
-| TTReference : ('self, reference) entry
+| TTReference : ('self, qualid) entry
| TTBigint : ('self, Constrexpr.raw_natural_number) entry
| TTConstr : prod_info * 'r target -> ('r, 'r) entry
| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
@@ -312,7 +312,7 @@ let interp_entry forpat e = match e with
let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with
| Anonymous -> CPatAtom None
- | Name id -> CPatAtom (Some (CAst.make ?loc @@ Ident id))
+ | Name id -> CPatAtom (Some (qualid_of_ident ?loc id))
type 'r env = {
constrs : 'r list;
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index 3a59242de..16934fc86 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -549,7 +549,7 @@ GEXTEND Gram
] ]
;
module_expr_atom:
- [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ]
+ [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid | "("; me = module_expr; ")" -> me ] ]
;
with_declaration:
[ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
@@ -559,7 +559,7 @@ GEXTEND Gram
] ]
;
module_type:
- [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v)
+ [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid
| "("; mt = module_type; ")" -> mt
| mty = module_type; me = module_expr_atom ->
CAst.make ~loc:!@loc @@ CMapply (mty,me)
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/indschemes.ml b/vernac/indschemes.ml
index 2deca1e06..e86e10877 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -370,7 +370,7 @@ requested
| InductionScheme (x,y,z) -> names "_ind" "_rec" x y z
| EqualityScheme x -> l1,((None,smart_global_inductive x)::l2)
-let do_mutual_induction_scheme lnamedepindsort =
+let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let lrecnames = List.map (fun ({CAst.v},_,_,_) -> v) lnamedepindsort
and env0 = Global.env() in
let sigma, lrecspec, _ =
@@ -388,7 +388,7 @@ let do_mutual_induction_scheme lnamedepindsort =
(evd, (indu,dep,sort) :: l, inst))
lnamedepindsort (Evd.from_env env0,[],None)
in
- let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
+ let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma ~force_mutual lrecspec in
let declare decl fi lrecref =
let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
let decltype = EConstr.to_constr sigma decltype in
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index 261c3d813..ebfc76de9 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -29,9 +29,13 @@ val declare_congr_scheme : inductive -> unit
val declare_rewriting_schemes : inductive -> unit
-(** Mutual Minimality/Induction scheme *)
+(** Mutual Minimality/Induction scheme.
+ [force_mutual] forces the construction of eliminators having the same predicates and
+ methods even if some of the inductives are not recursive.
+ By default it is [false] and some of the eliminators are defined as simple case analysis.
+ *)
-val do_mutual_induction_scheme :
+val do_mutual_induction_scheme : ?force_mutual:bool ->
(lident * bool * inductive * Sorts.family) list -> unit
(** Main calls to interpret the Scheme command *)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8f64f5519..da14358ef 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1449,7 +1449,7 @@ let add_notation_extra_printing_rule df k v =
(* Infix notations *)
-let inject_var x = CAst.make @@ CRef (CAst.make @@ Ident (Id.of_string x),None)
+let inject_var x = CAst.make @@ CRef (qualid_of_ident (Id.of_string x),None)
let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
check_infix_modifiers modifiers;
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/ppvernac.ml b/vernac/ppvernac.ml
index d0c423650..56dfaa54a 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -16,7 +16,6 @@ open Util
open CAst
open Extend
-open Libnames
open Decl_kinds
open Constrexpr
open Constrexpr_ops
@@ -79,13 +78,13 @@ open Pputils
let pr_lname_decl (n, u) =
pr_lname n ++ pr_universe_decl u
- let pr_smart_global = Pputils.pr_or_by_notation pr_reference
+ let pr_smart_global = Pputils.pr_or_by_notation pr_qualid
- let pr_ltac_ref = Libnames.pr_reference
+ let pr_ltac_ref = Libnames.pr_qualid
- let pr_module = Libnames.pr_reference
+ let pr_module = Libnames.pr_qualid
- let pr_import_module = Libnames.pr_reference
+ let pr_import_module = Libnames.pr_qualid
let sep_end = function
| VernacBullet _
@@ -157,7 +156,7 @@ open Pputils
let pr_locality local = if local then keyword "Local" else keyword "Global"
let pr_option_ref_value = function
- | QualidRefValue id -> pr_reference id
+ | QualidRefValue id -> pr_qualid id
| StringRefValue s -> qs s
let pr_printoption table b =
@@ -180,7 +179,7 @@ open Pputils
| _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
let pr_reference_or_constr pr_c = function
- | HintsReference r -> pr_reference r
+ | HintsReference r -> pr_qualid r
| HintsConstr c -> pr_c c
let pr_hint_mode = function
@@ -202,24 +201,24 @@ open Pputils
l
| HintsResolveIFF (l2r, l, n) ->
keyword "Resolve " ++ str (if l2r then "->" else "<-")
- ++ prlist_with_sep sep pr_reference l
+ ++ prlist_with_sep sep pr_qualid l
| HintsImmediate l ->
keyword "Immediate" ++ spc() ++
prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l
| HintsUnfold l ->
- keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_reference l
+ keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_qualid l
| HintsTransparency (l, b) ->
keyword (if b then "Transparent" else "Opaque")
++ spc ()
- ++ prlist_with_sep sep pr_reference l
+ ++ prlist_with_sep sep pr_qualid l
| HintsMode (m, l) ->
keyword "Mode"
++ spc ()
- ++ pr_reference m ++ spc() ++
+ ++ pr_qualid m ++ spc() ++
prlist_with_sep spc pr_hint_mode l
| HintsConstructors c ->
keyword "Constructors"
- ++ spc() ++ prlist_with_sep spc pr_reference c
+ ++ spc() ++ prlist_with_sep spc pr_qualid c
| HintsExtern (n,c,tac) ->
let pat = match c with None -> mt () | Some pat -> pr_pat pat in
keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
@@ -233,7 +232,7 @@ open Pputils
keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p
| CWith_Module (id,qid) ->
keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
- pr_ast pr_qualid qid
+ pr_qualid qid
let rec pr_module_ast leading_space pr_c = function
| { loc ; v = CMident qid } ->
@@ -451,7 +450,7 @@ open Pputils
| PrintFullContext ->
keyword "Print All"
| PrintSectionContext s ->
- keyword "Print Section" ++ spc() ++ Libnames.pr_reference s
+ keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s
| PrintGrammar ent ->
keyword "Print Grammar" ++ spc() ++ str ent
| PrintLoadPath dir ->
@@ -499,9 +498,9 @@ open Pputils
| PrintName (qid,udecl) ->
keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl
| PrintModuleType qid ->
- keyword "Print Module Type" ++ spc() ++ pr_reference qid
+ keyword "Print Module Type" ++ spc() ++ pr_qualid qid
| PrintModule qid ->
- keyword "Print Module" ++ spc() ++ pr_reference qid
+ keyword "Print Module" ++ spc() ++ pr_qualid qid
| PrintInspect n ->
keyword "Inspect" ++ spc() ++ int n
| PrintScopes ->
@@ -604,7 +603,7 @@ open Pputils
| ShowUniverses -> keyword "Show Universes"
| ShowProofNames -> keyword "Show Conjectures"
| ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
- | ShowMatch id -> keyword "Show Match " ++ pr_reference id
+ | ShowMatch id -> keyword "Show Match " ++ pr_qualid id
in
return (pr_showable s)
| VernacCheckGuard ->
@@ -901,7 +900,7 @@ open Pputils
| VernacDeclareInstances insts ->
let pr_inst (id, info) =
- pr_reference id ++ pr_hint_info pr_constr_pattern_expr info
+ pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info
in
return (
hov 1 (keyword "Existing" ++ spc () ++
@@ -911,7 +910,7 @@ open Pputils
| VernacDeclareClass id ->
return (
- hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id)
+ hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id)
)
(* Modules and Module Types *)
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 94eb45fd3..43c974846 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -183,29 +183,27 @@ let print_modules () =
pr_vertical_list DirPath.print only_loaded
-let print_module r =
- let qid = qualid_of_reference r in
+let print_module qid =
try
- let globdir = Nametab.locate_dir qid.v in
+ let globdir = Nametab.locate_dir qid in
match globdir with
DirModule { obj_dir; obj_mp; _ } ->
Printmod.print_module (Printmod.printable_body obj_dir) obj_mp
| _ -> raise Not_found
with
- Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid.v)
+ Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid)
-let print_modtype r =
- let qid = qualid_of_reference r in
+let print_modtype qid =
try
- let kn = Nametab.locate_modtype qid.v in
+ let kn = Nametab.locate_modtype qid in
Printmod.print_modtype kn
with Not_found ->
(* Is there a module of this name ? If yes we display its type *)
try
- let mp = Nametab.locate_module qid.v in
+ let mp = Nametab.locate_module qid in
Printmod.print_module false mp
with Not_found ->
- user_err (str"Unknown Module Type or Module " ++ pr_qualid qid.v)
+ user_err (str"Unknown Module Type or Module " ++ pr_qualid qid)
let print_namespace ns =
let ns = List.rev (Names.DirPath.repr ns) in
@@ -367,33 +365,32 @@ let msg_found_library = function
| Library.LibInPath, fulldir, file ->
hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file)
-let err_unmapped_library ?loc ?from qid =
+let err_unmapped_library ?from qid =
let dir = fst (repr_qualid qid) in
let prefix = match from with
| None -> str "."
| Some from ->
str " and prefix " ++ DirPath.print from ++ str "."
in
- user_err ?loc
+ user_err ?loc:qid.CAst.loc
~hdr:"locate_library"
(strbrk "Cannot find a physical path bound to logical path matching suffix " ++
DirPath.print dir ++ prefix)
-let err_notfound_library ?loc ?from qid =
+let err_notfound_library ?from qid =
let prefix = match from with
| None -> str "."
| Some from ->
str " with prefix " ++ DirPath.print from ++ str "."
in
- user_err ?loc ~hdr:"locate_library"
+ user_err ?loc:qid.CAst.loc ~hdr:"locate_library"
(strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
-let print_located_library r =
- let {loc;v=qid} = qualid_of_reference r in
+let print_located_library qid =
try msg_found_library (Library.locate_qualified_library ~warn:false qid)
with
- | Library.LibUnmappedDir -> err_unmapped_library ?loc qid
- | Library.LibNotFound -> err_notfound_library ?loc qid
+ | Library.LibUnmappedDir -> err_unmapped_library qid
+ | Library.LibNotFound -> err_notfound_library qid
let smart_global r =
let gr = Smartlocate.smart_global r in
@@ -542,25 +539,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
@@ -570,35 +578,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
@@ -636,7 +694,7 @@ let vernac_scheme l =
let vernac_combined_scheme lid l =
if Dumpglob.dump () then
(Dumpglob.dump_definition lid false "def";
- List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (make ?loc @@ Ident id))) l);
+ List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (qualid_of_ident ?loc id))) l);
Indschemes.do_combined_scheme lid l
let vernac_universe ~atts l =
@@ -657,7 +715,7 @@ let vernac_constraint ~atts l =
(* Modules *)
let vernac_import export refl =
- Library.import_module export (List.map qualid_of_reference refl)
+ Library.import_module export refl
let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
(* We check the state of the system (in section, in module type)
@@ -675,7 +733,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
in
Dumpglob.dump_moddef ?loc mp "mod";
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
- Option.iter (fun export -> vernac_import export [make @@ Ident id]) export
+ Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export
let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
(* We check the state of the system (in section, in module type)
@@ -700,7 +758,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
List.iter
(fun (export,id) ->
Option.iter
- (fun export -> vernac_import export [make @@ Ident id]) export
+ (fun export -> vernac_import export [qualid_of_ident id]) export
) argsexport
| _::_ ->
let binders_ast = List.map
@@ -715,14 +773,14 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
Dumpglob.dump_moddef ?loc mp "mod";
Flags.if_verbose Feedback.msg_info
(str "Module " ++ Id.print id ++ str " is defined");
- Option.iter (fun export -> vernac_import export [make @@ Ident id])
+ Option.iter (fun export -> vernac_import export [qualid_of_ident id])
export
let vernac_end_module export {loc;v=id} =
let mp = Declaremods.end_module () in
Dumpglob.dump_modref ?loc mp "mod";
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
- Option.iter (fun export -> vernac_import export [make ?loc @@ Ident id]) export
+ Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
if Lib.sections_are_opened () then
@@ -747,7 +805,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
List.iter
(fun (export,id) ->
Option.iter
- (fun export -> vernac_import export [make ?loc @@ Ident id]) export
+ (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
) argsexport
| _ :: _ ->
@@ -809,22 +867,20 @@ let warn_require_in_section =
let vernac_require from import qidl =
if Lib.sections_are_opened () then warn_require_in_section ();
- let qidl = List.map qualid_of_reference qidl in
let root = match from with
| None -> None
| Some from ->
- let qid = Libnames.qualid_of_reference from in
- let (hd, tl) = Libnames.repr_qualid qid.v in
+ let (hd, tl) = Libnames.repr_qualid from in
Some (Libnames.add_dirpath_suffix hd tl)
in
- let locate {loc;v=qid} =
+ let locate qid =
try
let warn = not !Flags.quiet in
let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in
(dir, f)
with
- | Library.LibUnmappedDir -> err_unmapped_library ?loc ?from:root qid
- | Library.LibNotFound -> err_notfound_library ?loc ?from:root qid
+ | Library.LibUnmappedDir -> err_unmapped_library ?from:root qid
+ | Library.LibNotFound -> err_notfound_library ?from:root qid
in
let modrefl = List.map locate qidl in
if Dumpglob.dump () then
@@ -1687,10 +1743,10 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
let glnumopt = query_command_selector ?loc glopt in
let gl,id =
match glnumopt, ref_or_by_not.v with
- | None,AN {v=Ident id} -> (* goal number not given, catch any failure *)
- (try get_nth_goal 1,id with _ -> raise NoHyp)
- | Some n,AN {v=Ident id} -> (* goal number given, catch if wong *)
- (try get_nth_goal n,id
+ | None,AN qid when qualid_is_ident qid -> (* goal number not given, catch any failure *)
+ (try get_nth_goal 1, qualid_basename qid with _ -> raise NoHyp)
+ | Some n,AN qid when qualid_is_ident qid -> (* goal number given, catch if wong *)
+ (try get_nth_goal n, qualid_basename qid
with
Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs"
(str "No such goal: " ++ int n ++ str "."))
@@ -1771,11 +1827,10 @@ let vernac_print ~atts env sigma =
Printer.pr_assumptionset env sigma nassums
| PrintStrategy r -> print_strategy r
-let global_module r =
- let {loc;v=qid} = qualid_of_reference r in
+let global_module qid =
try Nametab.full_name_module qid
with Not_found ->
- user_err ?loc ~hdr:"global_module"
+ user_err ?loc:qid.CAst.loc ~hdr:"global_module"
(str "Module/section " ++ pr_qualid qid ++ str " not found.")
let interp_search_restriction = function
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 3c88a3443..02a3b2bd6 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -8,11 +8,11 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit
+val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
(** Vernacular entries *)
val vernac_require :
- Libnames.reference option -> bool option -> Libnames.reference list -> unit
+ Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
(** The main interpretation function of vernacular expressions *)
val interp :
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 5acac9e25..f74383b02 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -13,7 +13,7 @@ open Constrexpr
open Libnames
(** Vernac expressions, produced by the parser *)
-type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
+type class_rawexpr = FunClass | SortClass | RefClass of qualid or_by_notation
type goal_selector = Goal_select.t =
| SelectAlreadyFocused
@@ -37,37 +37,37 @@ type univ_name_list = UnivNames.univ_name_list
type printable =
| PrintTables
| PrintFullContext
- | PrintSectionContext of reference
+ | PrintSectionContext of qualid
| PrintInspect of int
| PrintGrammar of string
| PrintLoadPath of DirPath.t option
| PrintModules
- | PrintModule of reference
- | PrintModuleType of reference
+ | PrintModule of qualid
+ | PrintModuleType of qualid
| PrintNamespace of DirPath.t
| PrintMLLoadPath
| PrintMLModules
| PrintDebugGC
- | PrintName of reference or_by_notation * UnivNames.univ_name_list option
+ | PrintName of qualid or_by_notation * UnivNames.univ_name_list option
| PrintGraph
| PrintClasses
| PrintTypeClasses
- | PrintInstances of reference or_by_notation
+ | PrintInstances of qualid or_by_notation
| PrintCoercions
| PrintCoercionPaths of class_rawexpr * class_rawexpr
| PrintCanonicalConversions
| PrintUniverses of bool * string option
- | PrintHint of reference or_by_notation
+ | PrintHint of qualid or_by_notation
| PrintHintGoal
| PrintHintDbName of string
| PrintHintDb
| PrintScopes
| PrintScope of string
| PrintVisibility of string option
- | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
- | PrintImplicit of reference or_by_notation
- | PrintAssumptions of bool * bool * reference or_by_notation
- | PrintStrategy of reference or_by_notation option
+ | PrintAbout of qualid or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
+ | PrintImplicit of qualid or_by_notation
+ | PrintAssumptions of bool * bool * qualid or_by_notation
+ | PrintStrategy of qualid or_by_notation option
type search_about_item =
| SearchSubPattern of constr_pattern_expr
@@ -80,11 +80,11 @@ type searchable =
| SearchAbout of (bool * search_about_item) list
type locatable =
- | LocateAny of reference or_by_notation
- | LocateTerm of reference or_by_notation
- | LocateLibrary of reference
- | LocateModule of reference
- | LocateOther of string * reference
+ | LocateAny of qualid or_by_notation
+ | LocateTerm of qualid or_by_notation
+ | LocateLibrary of qualid
+ | LocateModule of qualid
+ | LocateOther of string * qualid
| LocateFile of string
type showable =
@@ -95,7 +95,7 @@ type showable =
| ShowUniverses
| ShowProofNames
| ShowIntros of bool
- | ShowMatch of reference
+ | ShowMatch of qualid
type comment =
| CommentConstr of constr_expr
@@ -103,7 +103,7 @@ type comment =
| CommentInt of int
type reference_or_constr = Hints.reference_or_constr =
- | HintsReference of reference
+ | HintsReference of qualid
| HintsConstr of constr_expr
[@@ocaml.deprecated "Please use [Hints.reference_or_constr]"]
@@ -123,18 +123,18 @@ type hint_info_expr = Hints.hint_info_expr
type hints_expr = Hints.hints_expr =
| HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list
- | HintsResolveIFF of bool * reference list * int option
+ | HintsResolveIFF of bool * qualid list * int option
| HintsImmediate of Hints.reference_or_constr list
- | HintsUnfold of reference list
- | HintsTransparency of reference list * bool
- | HintsMode of reference * Hints.hint_mode list
- | HintsConstructors of reference list
+ | HintsUnfold of qualid list
+ | HintsTransparency of qualid list * bool
+ | HintsMode of qualid * Hints.hint_mode list
+ | HintsConstructors of qualid list
| HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
type search_restriction =
- | SearchInside of reference list
- | SearchOutside of reference list
+ | SearchInside of qualid list
+ | SearchOutside of qualid list
type rec_flag = bool (* true = Rec; false = NoRec *)
type verbose_flag = bool (* true = Verbose; false = Silent *)
@@ -159,7 +159,7 @@ type option_value = Goptions.option_value =
type option_ref_value =
| StringRefValue of string
- | QualidRefValue of reference
+ | QualidRefValue of qualid
(** Identifier and optional list of bound universes and constraints. *)
@@ -222,9 +222,9 @@ type proof_end =
| Proved of Proof_global.opacity_flag * lident option
type scheme =
- | InductionScheme of bool * reference or_by_notation * sort_expr
- | CaseScheme of bool * reference or_by_notation * sort_expr
- | EqualityScheme of reference or_by_notation
+ | InductionScheme of bool * qualid or_by_notation * sort_expr
+ | CaseScheme of bool * qualid or_by_notation * sort_expr
+ | EqualityScheme of qualid or_by_notation
type section_subset_expr =
| SsEmpty
@@ -348,10 +348,10 @@ type nonrec vernac_expr =
| VernacBeginSection of lident
| VernacEndSegment of lident
| VernacRequire of
- reference option * export_flag option * reference list
- | VernacImport of export_flag * reference list
- | VernacCanonical of reference or_by_notation
- | VernacCoercion of reference or_by_notation *
+ qualid option * export_flag option * qualid list
+ | VernacImport of export_flag * qualid list
+ | VernacCanonical of qualid or_by_notation
+ | VernacCoercion of qualid or_by_notation *
class_rawexpr * class_rawexpr
| VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr
| VernacNameSectionHypSet of lident * section_subset_expr
@@ -367,9 +367,9 @@ type nonrec vernac_expr =
| VernacContext of local_binder_expr list
| VernacDeclareInstances of
- (reference * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
+ (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
- | VernacDeclareClass of reference (* inductive or definition name *)
+ | VernacDeclareClass of qualid (* inductive or definition name *)
(* Modules and Module Types *)
| VernacDeclareModule of bool option * lident *
@@ -403,11 +403,11 @@ type nonrec vernac_expr =
(* Commands *)
| VernacCreateHintDb of string * bool
- | VernacRemoveHints of string list * reference list
+ | VernacRemoveHints of string list * qualid list
| VernacHints of string list * Hints.hints_expr
| VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
onlyparsing_flag
- | VernacArguments of reference or_by_notation *
+ | VernacArguments of qualid or_by_notation *
vernac_argument_status list (* Main arguments status list *) *
(Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
int option (* Number of args to trigger reduction *) *
@@ -416,9 +416,9 @@ type nonrec vernac_expr =
`DefaultImplicits ] list
| VernacReserve of simple_binder list
| VernacGeneralizable of (lident list) option
- | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list)
+ | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list)
| VernacSetStrategy of
- (Conv_oracle.level * reference or_by_notation list) list
+ (Conv_oracle.level * qualid or_by_notation list) list
| VernacUnsetOption of export_flag * Goptions.option_name
| VernacSetOption of export_flag * Goptions.option_name * option_value
| VernacAddOption of Goptions.option_name * option_ref_value list
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 21:50:39 +0000