aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml4
-rw-r--r--interp/constrexpr_ops.ml4
-rw-r--r--interp/constrextern.ml2
-rw-r--r--interp/constrintern.ml14
-rw-r--r--interp/declare.ml74
-rw-r--r--interp/declare.mli5
-rw-r--r--interp/impargs.ml4
-rw-r--r--interp/impargs.mli6
-rw-r--r--interp/implicit_quantifiers.ml59
-rw-r--r--interp/syntax_def.ml2
10 files changed, 90 insertions, 84 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 9f778d99e9..3ebbbdfb88 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -40,8 +40,8 @@ type explicitation =
type binder_kind =
| Default of binding_kind
- | Generalized of binding_kind * binding_kind * bool
- (** Inner binding, outer bindings, typeclass-specific flag
+ | Generalized of binding_kind * bool
+ (** (Inner binding always Implicit) Outer bindings, typeclass-specific flag
for implicit generalization of superclasses *)
type abstraction_kind = AbsLambda | AbsPi
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 443473d5b6..bcb2f34377 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -34,8 +34,8 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with
let binder_kind_eq b1 b2 = match b1, b2 with
| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
-| Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) ->
- binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 &&
+| Generalized (ck1, b1), Generalized (ck2, b2) ->
+ binding_kind_eq ck1 ck2 &&
(if b1 then b2 else not b2)
| _ -> false
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bb66658a37..fe50bd4b08 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -107,7 +107,7 @@ let _show_inactive_notations () =
let deactivate_notation nr =
match nr with
| SynDefRule kn ->
- (* shouldn't we check wether it is well defined? *)
+ (* shouldn't we check whether it is well defined? *)
inactive_notations_table := IRuleSet.add nr !inactive_notations_table
| NotationRule (scopt, ntn) ->
match availability_of_notation (scopt, ntn) (scopt, []) with
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f06493b374..31f3736bae 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -389,7 +389,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env =
{env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
let intern_generalized_binder ?(global_level=false) intern_type ntnvars
- env {loc;v=na} b b' t ty =
+ env {loc;v=na} b' t ty =
let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
let ty, ids' =
if t then ty, ids else
@@ -403,7 +403,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
env fvs in
let bl = List.map
CAst.(map (fun id ->
- (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
+ (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
fvs
in
let na = match na with
@@ -433,8 +433,8 @@ let intern_assumption intern ntnvars env nal bk ty =
(push_name_env ntnvars impls env locna,
(make ?loc (na,k,locate_if_hole ?loc na ty))::bl))
(env, []) nal
- | Generalized (b,b',t) ->
- let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in
+ | Generalized (b',t) ->
+ let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b' t ty in
env, b
let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
@@ -1229,7 +1229,7 @@ let add_local_defs_and_check_length loc env g pl args = match g with
let maxargs = Inductiveops.constructor_nalldecls env cstr in
if List.length pl' + List.length args > maxargs then
error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr);
- (* Two possibilities: either the args are given with explict
+ (* Two possibilities: either the args are given with explicit
variables for local definitions, then we give the explicit args
extended with local defs, so that there is nothing more to be
added later on; or the args are not enough to have all arguments,
@@ -1467,7 +1467,7 @@ let alias_of als = match als.alias_ids with
@returns a raw_case_pattern_expr :
- no notations and syntactic definition
- - global reference and identifeir instead of reference
+ - global reference and identifier instead of reference
*)
@@ -1642,7 +1642,7 @@ let drop_notations_pattern looked_for genv =
| CPatCast (_,_) ->
(* We raise an error if the pattern contains a cast, due to
current restrictions on casts in patterns. Cast in patterns
- are supportted only in local binders and only at top
+ are supported only in local binders and only at top
level. In fact, they are currently eliminated by the
parser. The only reason why they are in the
[cases_pattern_expr] type is that the parser needs to factor
diff --git a/interp/declare.ml b/interp/declare.ml
index 76b4bab2ce..7ee7ecb5e8 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -36,9 +36,8 @@ type internal_flag =
(** Declaration of constants and parameters *)
type constant_obj = {
- cst_decl : global_declaration option;
- (** [None] when the declaration is a side-effect and has already been defined
- in the global environment. *)
+ cst_decl : Cooking.recipe option;
+ (** Non-empty only when rebuilding a constant after a section *)
cst_kind : logical_kind;
cst_locl : bool;
}
@@ -65,21 +64,21 @@ let open_constant i ((sp,kn), obj) =
let exists_name id =
variable_exists id || Global.exists_objlabel (Label.of_id id)
-let check_exists sp =
- let id = basename sp in
+let check_exists id =
if exists_name id then alreadydeclared (Id.print id ++ str " already exists")
let cache_constant ((sp,kn), obj) =
+ (* Invariant: the constant must exist in the logical environment, except when
+ redefining it when exiting a section. See [discharge_constant]. *)
let id = basename sp in
let kn' =
match obj.cst_decl with
| None ->
if Global.exists_objlabel (Label.of_id (basename sp))
then Constant.make1 kn
- else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
- | Some decl ->
- let () = check_exists sp in
- Global.add_constant ~in_section:(Lib.sections_are_opened ()) id decl
+ else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(basename sp) ++ str".")
+ | Some r ->
+ Global.add_recipe ~in_section:(Lib.sections_are_opened ()) id r
in
assert (Constant.equal kn' (Constant.make1 kn));
Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
@@ -93,7 +92,9 @@ let discharge_constant ((sp, kn), obj) =
let modlist = replacement_context () in
let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in
let abstract = (named_of_variable_context hyps, subst, uctx) in
- let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
+ let new_decl = { from; info = { Opaqueproof.modlist; abstract } } in
+ (* This is a hack: when leaving a section, we lose the constant definition, so
+ we have to store it in the libobject to be able to retrieve it after. *)
Some { obj with cst_decl = Some new_decl; }
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
@@ -121,27 +122,22 @@ let update_tables c =
declare_constant_implicits c;
Notation.declare_ref_arguments_scope Evd.empty (ConstRef c)
-let register_side_effect (c, role) =
+let register_constant kn kind local =
let o = inConstant {
cst_decl = None;
- cst_kind = IsProof Theorem;
- cst_locl = false;
+ cst_kind = kind;
+ cst_locl = local;
} in
- let id = Label.to_id (Constant.label c) in
- ignore(add_leaf id o);
- update_tables c;
+ let id = Label.to_id (Constant.label kn) in
+ let _ = add_leaf id o in
+ update_tables kn
+
+let register_side_effect (c, role) =
+ let () = register_constant c (IsProof Theorem) false in
match role with
| Subproof -> ()
| Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
-let declare_constant_common id cst =
- let o = inConstant cst in
- let _, kn as oname = add_leaf id o in
- pull_to_head oname;
- let c = Global.constant_of_delta_kn kn in
- update_tables c;
- c
-
let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
@@ -153,7 +149,8 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
const_entry_feedback = None;
const_entry_inline_code = inline}
-let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let define_constant ?role ?(export_seff=false) id cd =
+ (* Logically define the constant and its subproofs, no libobject tampering *)
let is_poly de = match de.const_entry_universes with
| Monomorphic_entry _ -> false
| Polymorphic_entry _ -> true
@@ -165,20 +162,27 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
export_seff ||
not de.const_entry_opaque ||
is_poly de ->
- (* This globally defines the side-effects in the environment. We mark
- exported constants as being side-effect not to redeclare them at
- caching time. *)
+ (* This globally defines the side-effects in the environment. *)
let de, export = Global.export_private_constants ~in_section de in
export, ConstantEntry (PureEntry, DefinitionEntry de)
| _ -> [], ConstantEntry (EffectEntry, cd)
in
+ let kn, eff = Global.add_constant ?role ~in_section id decl in
+ kn, eff, export
+
+let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+ let () = check_exists id in
+ let kn, _eff, export = define_constant ~export_seff id cd in
+ (* Register the libobjects attached to the constants and its subproofs *)
let () = List.iter register_side_effect export in
- let cst = {
- cst_decl = Some decl;
- cst_kind = kind;
- cst_locl = local;
- } in
- declare_constant_common id cst
+ let () = register_constant kn kind local in
+ kn
+
+let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = false) id (cd, kind) =
+ let kn, eff, export = define_constant ~role id cd in
+ let () = assert (List.is_empty export) in
+ let () = register_constant kn kind local in
+ kn, eff
let declare_definition ?(internal=UserIndividualRequest)
?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
@@ -297,7 +301,7 @@ let open_inductive i ((sp,kn),mie) =
let cache_inductive ((sp,kn),mie) =
let names = inductive_names sp kn mie in
- List.iter check_exists (List.map fst names);
+ List.iter check_exists (List.map (fun p -> basename (fst p)) names);
let id = basename sp in
let kn' = Global.add_mind id mie in
assert (MutInd.equal kn' (MutInd.make1 kn));
diff --git a/interp/declare.mli b/interp/declare.mli
index 8f1e73c88c..795d9a767d 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -40,7 +40,7 @@ type internal_flag =
| InternalTacticRequest
| UserIndividualRequest
-(* Defaut definition entries, transparent with no secctx or proj information *)
+(* Default definition entries, transparent with no secctx or proj information *)
val definition_entry : ?fix_exn:Future.fix_exn ->
?opaque:bool -> ?inline:bool -> ?types:types ->
?univs:Entries.universes_entry ->
@@ -55,6 +55,9 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
val declare_constant :
?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
+val declare_private_constant :
+ role:side_effect_role -> ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants
+
val declare_definition :
?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
?local:bool -> Id.t -> ?types:constr ->
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 806fe93297..f3cdd64633 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -96,11 +96,11 @@ let set_maximality imps b =
this kind if there is enough arguments to infer them)
- [DepFlex] means that the implicit argument can be found by unification
- along a collapsable path only (e.g. as x in (P x) where P is another
+ along a collapsible path only (e.g. as x in (P x) where P is another
argument) (we do (defensively) print the arguments of this kind)
- [DepFlexAndRigid] means that the least argument from which the
- implicit argument can be inferred is following a collapsable path
+ implicit argument can be inferred is following a collapsible path
but there is a greater argument from where the implicit argument is
inferable following a rigid path (useful to know how to print a
partial application)
diff --git a/interp/impargs.mli b/interp/impargs.mli
index ccdd448460..1099074c63 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -34,7 +34,7 @@ val with_implicit_protection : ('a -> 'b) -> 'a -> 'b
(** {6 ... } *)
(** An [implicits_list] is a list of positions telling which arguments
- of a reference can be automatically infered *)
+ of a reference can be automatically inferred *)
type argument_position =
@@ -50,11 +50,11 @@ type implicit_explanation =
this kind if there is enough arguments to infer them) *)
| DepFlex of argument_position
(** means that the implicit argument can be found by unification
- along a collapsable path only (e.g. as x in (P x) where P is another
+ along a collapsible path only (e.g. as x in (P x) where P is another
argument) (we do (defensively) print the arguments of this kind) *)
| DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
(** means that the least argument from which the
- implicit argument can be inferred is following a collapsable path
+ implicit argument can be inferred is following a collapsible path
but there is a greater argument from where the implicit argument is
inferable following a rigid path (useful to know how to print a
partial application) *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 6277d874dd..bac46c2d2f 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -196,10 +196,9 @@ let combine_params avoid fn applied needed =
user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
in aux [] avoid applied needed
-let combine_params_freevar =
- fun avoid (_, decl) ->
- let id' = next_name_away_from (RelDecl.get_name decl) avoid in
- (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
+let combine_params_freevar avoid (_, decl) =
+ let id' = next_name_away_from (RelDecl.get_name decl) avoid in
+ (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
let destClassApp cl =
let open CAst in
@@ -222,34 +221,34 @@ let implicit_application env ?(allow_partial=true) f ty =
let is_class =
try
let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
- let gr = Nametab.locate qid in
- if Typeclasses.is_class gr then Some (clapp, gr) else None
+ if Libnames.idset_mem_qualid qid env then None
+ else
+ let gr = Nametab.locate qid in
+ if Typeclasses.is_class gr then Some (clapp, gr) else None
with Not_found -> None
in
- match is_class with
- | None -> ty, env
- | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
- let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
- let c, avoid =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- let c = class_info env sigma gr in
- let (ci, rd) = c.cl_context in
- if not allow_partial then
- begin
- let opt_succ x n = match x with
- | None -> succ n
- | Some _ -> n
- in
- let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
- let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
- if not (Int.equal needlen applen) then
- mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
- end;
- let pars = List.rev (List.combine ci rd) in
- let args, avoid = combine_params avoid f par pars in
- CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
- in c, avoid
+ match is_class with
+ | None -> ty, env
+ | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
+ let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let c = class_info env sigma gr in
+ let (ci, rd) = c.cl_context in
+ if not allow_partial then
+ begin
+ let opt_succ x n = match x with
+ | None -> succ n
+ | Some _ -> n
+ in
+ let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
+ let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
+ if not (Int.equal needlen applen) then
+ mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
+ end;
+ let pars = List.rev (List.combine ci rd) in
+ let args, avoid = combine_params avoid f par pars in
+ CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
let warn_ignoring_implicit_status =
CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits"
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 49273c4146..a7e1de736c 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -48,7 +48,7 @@ let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
match onlyparse with
| None ->
(* Redeclare it to be used as (short) name in case an other (distfix)
- notation was declared inbetween *)
+ notation was declared in between *)
Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
| _ -> ()
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 07:02:56 +0000