aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/declarations.mli4
-rw-r--r--kernel/declareops.ml4
-rw-r--r--kernel/safe_typing.ml6
-rw-r--r--kernel/safe_typing.mli3
-rw-r--r--kernel/term_typing.ml37
-rw-r--r--library/declare.ml32
-rw-r--r--library/declare.mli5
-rw-r--r--toplevel/ind_tables.ml24
8 files changed, 77 insertions, 38 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 6a5b0dbb2..d74c9a0d5 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -59,7 +59,9 @@ type constant_body = {
const_native_name : native_name ref;
const_inline_code : bool }
-type side_effect = NewConstant of constant * constant_body
+type side_effect =
+ | SEsubproof of constant * constant_body
+ | SEscheme of (inductive * constant * constant_body) list * string
(** {6 Representation of mutual inductive types in the kernel } *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 518a40a6e..9f981f482 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -254,7 +254,9 @@ let prune_constant_body cb =
else {cb with const_constraints = cst'; const_body = cbo'}
let string_of_side_effect = function
- | NewConstant (c,_) -> Names.string_of_con c
+ | SEsubproof (c,_) -> Names.string_of_con c
+ | SEscheme (cl,_) ->
+ String.concat ", " (List.map (fun (_,c,_) -> Names.string_of_con c) cl)
type side_effects = side_effect list
let no_seff = ([] : side_effects)
let iter_side_effects f l = List.iter f (List.rev l)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 7a25cc5f8..3cde1538d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -169,8 +169,10 @@ let check_engagement env c =
(** {6 Stm machinery } *)
-type side_effect = Declarations.side_effect
-let sideff_of_con env c = NewConstant (c, Environ.lookup_constant c env.env)
+let sideff_of_con env c = SEsubproof (c, Environ.lookup_constant c env.env)
+let sideff_of_scheme kind env cl =
+ SEscheme(
+ List.map (fun (i,c) -> i, c, Environ.lookup_constant c env.env) cl,kind)
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5d1c98de5..a56bb8578 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -34,6 +34,9 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
(** {6 Stm machinery } *)
val sideff_of_con : safe_environment -> constant -> Declarations.side_effect
+val sideff_of_scheme :
+ string -> safe_environment -> (inductive * constant) list ->
+ Declarations.side_effect
val is_curmod_library : safe_environment -> bool
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c65ca8fc0..ef0270e9d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -47,27 +47,32 @@ let translate_local_assum env t =
(* Insertion of constants and parameters in environment. *)
let handle_side_effects env body side_eff =
- let handle_sideff t (NewConstant (c,cb)) =
- let cname =
+ let handle_sideff t se =
+ let cbl = match se with
+ | SEsubproof (c,cb) -> [c,cb]
+ | SEscheme (cl,_) -> List.map (fun (_,c,cb) -> c,cb) cl in
+ let cname c =
let name = string_of_con c in
for i = 0 to String.length name - 1 do
if name.[i] = '.' || name.[i] = '#' then name.[i] <- '_' done;
Name (id_of_string name) in
- let rec sub i x = match kind_of_term x with
+ let rec sub c i x = match kind_of_term x with
| Const c' when eq_constant c c' -> mkRel i
- | _ -> map_constr_with_binders ((+) 1) sub i x in
- match cb.const_body with
- | Undef _ -> assert false
- | Def b ->
- let b = Lazyconstr.force b in
- let b_ty = Typeops.type_of_constant_type env cb.const_type in
- let t = sub 1 (Vars.lift 1 t) in
- mkLetIn (cname, b, b_ty, t)
- | OpaqueDef b ->
- let b = Lazyconstr.force_opaque (Future.force b) in
- let b_ty = Typeops.type_of_constant_type env cb.const_type in
- let t = sub 1 (Vars.lift 1 t) in
- mkApp (mkLambda (cname, b_ty, t), [|b|])
+ | _ -> map_constr_with_binders ((+) 1) (sub c) i x in
+ let fix_body (c,cb) t =
+ match cb.const_body with
+ | Undef _ -> assert false
+ | Def b ->
+ let b = Lazyconstr.force b in
+ let b_ty = Typeops.type_of_constant_type env cb.const_type in
+ let t = sub c 1 (Vars.lift 1 t) in
+ mkLetIn (cname c, b, b_ty, t)
+ | OpaqueDef b ->
+ let b = Lazyconstr.force_opaque (Future.force b) in
+ let b_ty = Typeops.type_of_constant_type env cb.const_type in
+ let t = sub c 1 (Vars.lift 1 t) in
+ mkApp (mkLambda (cname c, b_ty, t), [|b|]) in
+ List.fold_right fix_body cbl t
in
(* CAVEAT: we assure a proper order *)
Declareops.fold_side_effects handle_sideff body
diff --git a/library/declare.ml b/library/declare.ml
index c4651f0de..96bbf07d5 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -181,22 +181,30 @@ let declare_constant_common id cst =
Notation.declare_ref_arguments_scope (ConstRef c);
c
-let declare_sideff (NewConstant (c, cb)) =
- let id = Names.Label.to_id (Names.Constant.label c) in
- let pt, opaque =
+let declare_scheme = ref (fun _ _ -> assert false)
+let set_declare_scheme f = declare_scheme := f
+let declare_sideff se =
+ let cbl, scheme = match se with
+ | SEsubproof (c, cb) -> [c, cb], None
+ | SEscheme (cbl, k) ->
+ List.map (fun (_,c,cb) -> c,cb) cbl, Some (List.map pi1 cbl,k) in
+ let id_of c = Names.Label.to_id (Names.Constant.label c) in
+ let pt_opaque_of cb =
match cb with
| { const_body = Def sc } -> Lazyconstr.force sc, false
| { const_body = OpaqueDef fc } ->
Lazyconstr.force_opaque (Future.force fc), true
| { const_body = Undef _ } -> anomaly(str"Undefined side effect")
in
- let ty =
+ let ty_of cb =
match cb.Declarations.const_type with
| Declarations.NonPolymorphicType t -> Some t
| _ -> None in
- let cst = {
- cst_decl = ConstantEntry (DefinitionEntry {
- const_entry_body = Future.from_val (pt,Declareops.no_seff);
+ let cst_of cb =
+ let pt, opaque = pt_opaque_of cb in
+ let ty = ty_of cb in
+ { cst_decl = ConstantEntry (DefinitionEntry {
+ const_entry_body = Future.from_here (pt, Declareops.no_seff);
const_entry_secctx = Some cb.Declarations.const_hyps;
const_entry_type = ty;
const_entry_opaque = opaque;
@@ -206,7 +214,13 @@ let declare_sideff (NewConstant (c, cb)) =
cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition;
cst_locl = true;
} in
- ignore(declare_constant_common id cst)
+ let knl =
+ List.map (fun (c,cb) ->
+ declare_constant_common (id_of c) (cst_of cb)) cbl in
+ match scheme with
+ | None -> ()
+ | Some (inds,kind) ->
+ !declare_scheme kind (Array.of_list (List.combine inds knl))
let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
let cd = (* We deal with side effects of non-opaque constants *)
@@ -215,7 +229,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
const_entry_opaque = false; const_entry_body = bo } as de) ->
let pt, seff = Future.force bo in
if seff = Declareops.no_seff then cd
- else begin
+ else begin
Declareops.iter_side_effects declare_sideff seff;
Entries.DefinitionEntry { de with
const_entry_body = Future.from_val (pt, Declareops.no_seff) }
diff --git a/library/declare.mli b/library/declare.mli
index ff4e20ad2..f33077ddb 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -61,6 +61,11 @@ val declare_definition :
?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
?local:bool -> Id.t -> ?types:constr -> Entries.const_entry_body -> constant
+(** Since transparent constant's side effects are globally declared, we
+ * need that *)
+val set_declare_scheme :
+ (string -> (inductive * constant) array -> unit) -> unit
+
(** [declare_mind me] declares a block of inductive types with
their constructors in the current section; it returns the path of
the whole block (boolean must be true iff it is a record) *)
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 0a5f7d25f..45621ced8 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -99,6 +99,8 @@ let declare_individual_scheme_object s ?(aux="") f =
let declare_scheme kind indcl =
Lib.add_anonymous_leaf (inScheme (kind,indcl))
+let () = Declare.set_declare_scheme declare_scheme
+
let is_visible_name id =
try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true
with Not_found -> false
@@ -134,7 +136,8 @@ let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
| None -> add_suffix mib.mind_packets.(i).mind_typename suff in
let const = define internal id c in
declare_scheme kind [|ind,const|];
- const, Declareops.cons_side_effects (Safe_typing.sideff_of_con (Global.safe_env()) const) eff
+ const, Declareops.cons_side_effects
+ (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff
let define_individual_scheme kind internal names (mind,i as ind) =
match Hashtbl.find scheme_object_table kind with
@@ -149,13 +152,13 @@ let define_mutual_scheme_base kind suff f internal names mind =
try List.assoc i names
with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
let consts = Array.map2 (define internal) ids cl in
- declare_scheme kind (Array.mapi (fun i cst -> ((mind,i),cst)) consts);
+ let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
+ declare_scheme kind schemes;
consts,
- Declareops.union_side_effects eff
- (Declareops.side_effects_of_list
- (List.map
- (fun x -> Safe_typing.sideff_of_con (Global.safe_env()) x)
- (Array.to_list consts)))
+ Declareops.cons_side_effects
+ (Safe_typing.sideff_of_scheme
+ kind (Global.safe_env()) (Array.to_list schemes))
+ eff
let define_mutual_scheme kind internal names mind =
match Hashtbl.find scheme_object_table kind with
@@ -163,9 +166,12 @@ let define_mutual_scheme kind internal names mind =
| s,MutualSchemeFunction f ->
define_mutual_scheme_base kind s f internal names mind
+let find_scheme_on_env_too kind ind =
+ String.Map.find kind (Indmap.find ind !scheme_map)
+
let find_scheme kind (mind,i as ind) =
try
- let s = String.Map.find kind (Indmap.find ind !scheme_map) in
+ let s = find_scheme_on_env_too kind ind in
s, Declareops.no_seff
with Not_found ->
match Hashtbl.find scheme_object_table kind with
@@ -176,6 +182,6 @@ let find_scheme kind (mind,i as ind) =
ca.(i), eff
let check_scheme kind ind =
- try let _ = String.Map.find kind (Indmap.find ind !scheme_map) in true
+ try let _ = find_scheme_on_env_too kind ind in true
with Not_found -> false
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-18 15:22:19 +0000