aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/correctness/psyntax.ml46
-rw-r--r--kernel/safe_typing.ml38
-rw-r--r--kernel/safe_typing.mli15
-rw-r--r--library/declare.ml76
-rw-r--r--library/declare.mli13
-rw-r--r--library/global.ml3
-rw-r--r--library/global.mli5
-rwxr-xr-xpretyping/classops.ml2
-rw-r--r--tactics/setoid_replace.ml18
-rw-r--r--tactics/tactics.ml5
-rw-r--r--toplevel/class.ml7
-rw-r--r--toplevel/command.ml3
-rw-r--r--toplevel/discharge.ml8
13 files changed, 56 insertions, 143 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index b85a50790..77d261653 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -546,9 +546,11 @@ let _ =
let ren = update empty_ren "" [] in
let v = Ptyping.cic_type_v env ren v in
if not (is_mutable v) then begin
- let c = trad_ml_type_v ren env v in
+ let c =
+ Safe_typing.ParameterEntry (trad_ml_type_v ren env v),
+ Declare.NeverDischarge in
List.iter
- (fun id -> ignore (Declare.declare_parameter id c)) ids;
+ (fun id -> ignore (Declare.declare_constant id c)) ids;
if_verbose (is_assumed false) ids
end;
if not (is_pure v) then begin
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fec53beaa..23b2ecdc7 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -71,12 +71,15 @@ type constant_entry = {
const_entry_type : types option;
const_entry_opaque : bool }
-type global_declaration = Def of constant_entry | Assum of types
+type global_declaration =
+ | ConstantEntry of constant_entry
+ | ParameterEntry of types
+ | GlobalRecipe of Cooking.recipe
(* Definition always declared transparent *)
let safe_infer_declaration env dcl =
match dcl with
- | Def c ->
+ | ConstantEntry c ->
let (j,cst) = safe_infer env c.const_entry_body in
let typ,cst = match c.const_entry_type with
| None -> j.uj_type,cst
@@ -87,9 +90,11 @@ let safe_infer_declaration env dcl =
with NotConvertible -> error_actual_type env j tj.utj_val in
tj.utj_val, Constraint.union (Constraint.union cst cst2) cst3 in
Some j.uj_val, typ, cst, c.const_entry_opaque
- | Assum t ->
+ | ParameterEntry t ->
let (j,cst) = safe_infer env t in
None, Typeops.assumption_of_judgment env j, cst, false
+ | GlobalRecipe r ->
+ Cooking.cook_constant env r
let add_global_declaration sp env (body,typ,cst,op) =
let env' = add_constraints cst env in
@@ -106,35 +111,10 @@ let add_global_declaration sp env (body,typ,cst,op) =
const_opaque = op } in
Environ.add_constant sp cb env'
-let add_parameter sp t env =
- add_global_declaration sp env (safe_infer_declaration env (Assum t))
-
(*s Global and local constant declaration. *)
let add_constant sp ce env =
- add_global_declaration sp env (safe_infer_declaration env (Def ce))
-
-let add_discharged_constant sp r env =
- let (body,typ,cst,op) = Cooking.cook_constant env r in
- match body with
- | None ->
- add_parameter sp typ (* Bricolage avant poubelle *) env
- | Some c ->
- (* let c = hcons1_constr c in *)
- let ids =
- Idset.union (global_vars_set env c)
- (global_vars_set env (body_of_type typ))
- in
- let hyps = keep_hyps env ids in
- let env' = Environ.add_constraints cst env in
- let cb =
- { const_body = Some c;
- const_type = typ;
- const_hyps = hyps;
- const_constraints = cst;
- const_opaque = op } in
- Environ.add_constant sp cb env'
-
+ add_global_declaration sp env (safe_infer_declaration env ce)
(* Insertion of inductive types. *)
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 36c2bbb23..853bc7ccd 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -35,21 +35,18 @@ val push_named_def :
val pop_named_decls : identifier list -> safe_environment -> safe_environment
(* Adding global axioms or definitions *)
-
-val add_parameter :
- section_path -> constr -> safe_environment -> safe_environment
-
-(*s Global and local constant declaration. *)
-
type constant_entry = {
const_entry_body : constr;
const_entry_type : types option;
const_entry_opaque : bool }
+type global_declaration =
+ | ConstantEntry of constant_entry
+ | ParameterEntry of types
+ | GlobalRecipe of Cooking.recipe
+
val add_constant :
- section_path -> constant_entry -> safe_environment -> safe_environment
-val add_discharged_constant :
- section_path -> Cooking.recipe -> safe_environment -> safe_environment
+ section_path -> global_declaration -> safe_environment -> safe_environment
(* Adding an inductive type *)
val add_mind :
diff --git a/library/declare.ml b/library/declare.ml
index 542bd6b94..c87ec0d34 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -110,50 +110,9 @@ let declare_variable id obj =
if is_implicit_args() then declare_var_implicits id;
sp
-(* Parameters. *)
+(* Globals: constants and parameters *)
-let cache_parameter (sp,c) =
- (if Nametab.exists_cci sp then
- let (_,id) = repr_path sp in
- errorlabstrm "cache_parameter" [< pr_id id; 'sTR " already exists" >]);
- Global.add_parameter sp c;
- Nametab.push 0 sp (ConstRef sp)
-
-let load_parameter (sp,_) =
- (if Nametab.exists_cci sp then
- let (_,id) = repr_path sp in
- errorlabstrm "cache_parameter" [< pr_id id; 'sTR " already exists" >]);
- Nametab.push 1 sp (ConstRef sp)
-
-let open_parameter (sp,_) =
- Nametab.push 0 (restrict_path 0 sp) (ConstRef sp)
-
-(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_parameter_entry = mkProp
-
-let export_parameter c = Some dummy_parameter_entry
-
-let (in_parameter, out_parameter) =
- let od = {
- cache_function = cache_parameter;
- load_function = load_parameter;
- open_function = open_parameter;
- export_function = export_parameter }
- in
- declare_object ("PARAMETER", od)
-
-let declare_parameter id c =
- let sp = add_leaf id (in_parameter c) in
- if is_implicit_args() then declare_constant_implicits sp;
- sp
-
-(* Constants. *)
-
-type constant_declaration_type =
- | ConstantEntry of constant_entry
- | ConstantRecipe of Cooking.recipe
-
-type constant_declaration = constant_declaration_type * strength
+type constant_declaration = global_declaration * strength
let csttab = ref (Spmap.empty : strength Spmap.t)
@@ -167,10 +126,7 @@ let cache_constant (sp,(cdt,stre)) =
(if Nametab.exists_cci sp then
let (_,id) = repr_path sp in
errorlabstrm "cache_constant" [< pr_id id; 'sTR " already exists" >]);
- begin match cdt with
- | ConstantEntry ce -> Global.add_constant sp ce
- | ConstantRecipe r -> Global.add_discharged_constant sp r
- end;
+ Global.add_constant sp cdt;
(match stre with
| DischargeAt (dp,n) when not (is_dirpath_prefix_of dp (Lib.cwd ())) ->
(* Only qualifications including the sections segment from the current
@@ -197,10 +153,7 @@ let open_constant (sp,(_,stre)) =
Nametab.push n (restrict_path n sp) (ConstRef sp)
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = ConstantEntry {
- const_entry_body = mkProp;
- const_entry_type = None;
- const_entry_opaque = false }
+let dummy_constant_entry = ParameterEntry mkProp
let export_constant (ce,stre) = Some (dummy_constant_entry,stre)
@@ -215,11 +168,10 @@ let (in_constant, out_constant) =
let hcons_constant_declaration = function
| (ConstantEntry ce, stre) ->
- (ConstantEntry
- { const_entry_body = hcons1_constr ce.const_entry_body;
- const_entry_type = option_app hcons1_constr ce.const_entry_type;
- const_entry_opaque = ce.const_entry_opaque },
- stre)
+ (ConstantEntry
+ { const_entry_body = hcons1_constr ce.const_entry_body;
+ const_entry_type = option_app hcons1_constr ce.const_entry_type;
+ const_entry_opaque = ce.const_entry_opaque }, stre)
| cd -> cd
let declare_constant id cd =
@@ -228,8 +180,8 @@ let declare_constant id cd =
if is_implicit_args() then declare_constant_implicits sp;
sp
-let redeclare_constant sp cd =
- add_absolutely_named_leaf sp (in_constant cd);
+let redeclare_constant sp (cd,stre) =
+ add_absolutely_named_leaf sp (in_constant (GlobalRecipe cd,stre));
if is_implicit_args() then declare_constant_implicits sp
(* Inductives. *)
@@ -315,9 +267,6 @@ let is_constant sp =
let constant_strength sp = Spmap.find sp !csttab
-let constant_or_parameter_strength sp =
- try constant_strength sp with Not_found -> NeverDischarge
-
let get_variable id =
let (p,(c,ty,cst),str) = Idmap.find id !vartab in
((id,c,ty),str)
@@ -431,3 +380,8 @@ let is_global id =
is_dirpath_prefix_of (dirpath_of_global osp) (Lib.cwd())
with Not_found ->
false
+
+let strength_of_global = function
+ | ConstRef sp -> constant_strength sp
+ | VarRef id -> variable_strength id
+ | IndRef _ | ConstructRef _ -> NeverDischarge
diff --git a/library/declare.mli b/library/declare.mli
index bb903a9c4..e8da45a57 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -39,20 +39,14 @@ type variable_declaration = dir_path * section_variable_entry * strength
val declare_variable : variable -> variable_declaration -> section_path
-type constant_declaration_type =
- | ConstantEntry of constant_entry
- | ConstantRecipe of Cooking.recipe
-
-type constant_declaration = constant_declaration_type * strength
+type constant_declaration = global_declaration * strength
(* [declare_constant id cd] declares a global declaration
(constant/parameter) with name [id] in the current section; it returns
the full path of the declaration *)
val declare_constant : identifier -> constant_declaration -> constant
-val redeclare_constant : constant -> constant_declaration -> unit
-
-val declare_parameter : identifier -> constr -> constant
+val redeclare_constant : constant -> Cooking.recipe * strength -> unit
(* [declare_mind me] declares a block of inductive types with
their constructors in the current section; it returns the path of
@@ -69,7 +63,6 @@ val make_strength_2 : unit -> strength
val is_constant : section_path -> bool
val constant_strength : constant -> strength
-val constant_or_parameter_strength : constant -> strength
val out_variable : Libobject.obj -> identifier * variable_declaration
val get_variable : variable -> named_declaration * strength
@@ -105,3 +98,5 @@ val global_reference : identifier -> constr
val construct_reference : Environ.env -> identifier -> constr
val is_global : identifier -> bool
+
+val strength_of_global : global_reference -> strength
diff --git a/library/global.ml b/library/global.ml
index bbb77c853..b929ad78f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -47,10 +47,7 @@ let push_named_def d =
cst
let pop_named_decls ids = global_env := pop_named_decls ids !global_env
-let add_parameter sp c = global_env := add_parameter sp c !global_env
let add_constant sp ce = global_env := add_constant sp ce !global_env
-let add_discharged_constant sp r =
- global_env := add_discharged_constant sp r !global_env
let add_mind sp mie = global_env := add_mind sp mie !global_env
let add_constraints c = global_env := add_constraints c !global_env
diff --git a/library/global.mli b/library/global.mli
index f10ab98a5..48b647c6a 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,10 +32,7 @@ val push_named_assum : (identifier * types) -> Univ.constraints
val push_named_def : (identifier * constr * types option) -> Univ.constraints
val pop_named_decls : identifier list -> unit
-val add_parameter : constant -> types -> unit
-val add_constant : constant -> constant_entry -> unit
-val add_discharged_constant : constant -> Cooking.recipe -> unit
-
+val add_constant : constant -> global_declaration -> unit
val add_mind : mutual_inductive -> mutual_inductive_entry -> unit
val add_constraints : constraints -> unit
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 4628f66e1..4220b7b9e 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -222,7 +222,7 @@ let class_of env sigma t =
let class_args_of c = snd (decompose_app c)
let strength_of_cl = function
- | CL_CONST sp -> constant_or_parameter_strength sp
+ | CL_CONST sp -> constant_strength sp
| CL_SECVAR sp -> variable_strength sp
| _ -> NeverDischarge
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index f83436e16..0f1b749a6 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -234,14 +234,14 @@ let add_setoid a aeq th =
let eq_ext_name = gen_eq_lem_name () in
let eq_ext_name2 = gen_eq_lem_name () in
let _ = Declare.declare_constant eq_ext_name
- ((Declare.ConstantEntry {const_entry_body = eq_morph;
- const_entry_type = None;
- const_entry_opaque = true}),
+ ((ConstantEntry {const_entry_body = eq_morph;
+ const_entry_type = None;
+ const_entry_opaque = true}),
Declare.NeverDischarge) in
let _ = Declare.declare_constant eq_ext_name2
- ((Declare.ConstantEntry {const_entry_body = eq_morph2;
- const_entry_type = None;
- const_entry_opaque = true}),
+ ((ConstantEntry {const_entry_body = eq_morph2;
+ const_entry_type = None;
+ const_entry_opaque = true}),
Declare.NeverDischarge) in
let eqmorph = (current_constant eq_ext_name) in
let eqmorph2 = (current_constant eq_ext_name2) in
@@ -459,9 +459,9 @@ let add_morphism lem_name (m,profil) =
(let lem_2 = gen_lem_iff env m mext args_t poss in
let lem2_name = add_suffix lem_name "2" in
let _ = Declare.declare_constant lem2_name
- ((Declare.ConstantEntry {const_entry_body = lem_2;
- const_entry_type = None;
- const_entry_opaque = true}),
+ ((ConstantEntry {const_entry_body = lem_2;
+ const_entry_type = None;
+ const_entry_opaque = true}),
Declare.NeverDischarge) in
let lem2 = (current_constant lem2_name) in
(Lib.add_anonymous_leaf
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e7d61a79a..dc87c10f2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -422,7 +422,7 @@ let hide_ident_or_numarg_tactic s tac =
| _ -> assert false in
add_tactic s tacfun;
fun id -> vernac_tactic(s,[Identifier id])
-
+
(* Obsolete, remplace par intros_unitl_n ?
let intros_do n g =
@@ -1844,7 +1844,8 @@ let abstract_subproof name tac gls =
with e when catchable_exception e ->
(delete_current_proof(); raise e)
in (* Faudrait un peu fonctionnaliser cela *)
- let sp = Declare.declare_constant na (ConstantEntry const,strength) in
+ let cd = Safe_typing.ConstantEntry const in
+ let sp = Declare.declare_constant na (cd,strength) in
let newenv = Global.env() in
Declare.constr_of_reference (ConstRef sp)
in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 561175013..8ffb08c55 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -69,11 +69,6 @@ let rec stre_unif_cond = function
and stre2 = (variable_strength v2) in
stre_max (stre1,stre2)
-let stre_of_global = function
- | ConstRef sp -> constant_or_parameter_strength sp
- | VarRef id -> variable_strength id
- | IndRef _ | ConstructRef _ -> NeverDischarge
-
(* Errors *)
type coercion_error_kind =
@@ -235,7 +230,7 @@ let prods_of t =
let get_strength stre ref cls clt =
let stres = (snd (class_info cls)).cl_strength in
let stret = (snd (class_info clt)).cl_strength in
- let stref = stre_of_global ref in
+ let stref = strength_of_global ref in
(* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ?
let streunif = stre_unif_cond (s_vardep,f_vardep) in
*)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5906d7520..0ff52efda 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -33,7 +33,6 @@ open Nametab
open Typeops
open Indtypes
-let mkCastC(c,t) = ope("CAST",[c;t])
let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some x,b)])
let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
let mkProdC (x,a,b) = ope("PROD",[a;slam(Some x,b)])
@@ -103,7 +102,7 @@ let syntax_definition ident com =
let parameter_def_var ident c =
let c = interp_type Evd.empty (Global.env()) c in
- let sp = declare_parameter ident c in
+ let sp = declare_constant ident (ParameterEntry c, NeverDischarge) in
if_verbose message ((string_of_id ident) ^ " is assumed");
sp
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index a6fbb7283..4c5e21b0a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -170,7 +170,6 @@ type opacity = bool
type discharge_operation =
| Variable of identifier * section_variable_entry * strength * bool
- | Parameter of identifier * constr * bool
| Constant of section_path * recipe * strength * bool
| Inductive of mutual_inductive_entry * bool
| Class of cl_typ * cl_info_typ
@@ -215,7 +214,7 @@ let process_object oldenv dir sec_sp
| ("CONSTANT" | "PARAMETER") ->
(* CONSTANT/PARAMETER means never discharge (though visibility *)
(* may vary) *)
- let stre = constant_or_parameter_strength sp in
+ let stre = constant_strength sp in
(*
if stre = (DischargeAt sec_sp) then
let cb = Environ.lookup_constant sp oldenv in
@@ -294,11 +293,8 @@ let process_operation = function
let _ =
with_implicits imp (declare_variable id) (Lib.cwd(),expmod_a,stre) in
()
- | Parameter (spid,typ,imp) ->
- let _ = with_implicits imp (declare_parameter spid) typ in
- constant_message spid
| Constant (sp,r,stre,imp) ->
- with_implicits imp (redeclare_constant sp) (ConstantRecipe r,stre);
+ with_implicits imp (redeclare_constant sp) (r,stre);
constant_message (basename sp)
| Inductive (mie,imp) ->
let _ = with_implicits imp declare_mind mie in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 11:21:49 +0000