aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/constant.ml19
-rw-r--r--kernel/constant.mli12
-rw-r--r--kernel/instantiate.ml3
-rw-r--r--kernel/safe_typing.ml32
-rw-r--r--kernel/safe_typing.mli6
-rw-r--r--library/declare.ml5
-rw-r--r--library/lib.ml18
-rw-r--r--library/lib.mli5
-rw-r--r--library/library.ml1
-rw-r--r--library/redinfo.ml2
-rw-r--r--parsing/pretty.ml17
-rw-r--r--proofs/pfedit.ml9
-rw-r--r--toplevel/class.ml3
-rw-r--r--toplevel/command.ml35
-rw-r--r--toplevel/discharge.ml194
15 files changed, 223 insertions, 138 deletions
diff --git a/kernel/constant.ml b/kernel/constant.ml
index c93d486fa..dda7274af 100644
--- a/kernel/constant.ml
+++ b/kernel/constant.ml
@@ -7,13 +7,15 @@ open Generic
open Term
open Sign
-type constant_entry = {
- const_entry_body : constr;
- const_entry_type : constr option }
+type lazy_constant_value =
+ | Cooked of constr
+ | Recipe of (unit -> constr)
+
+type constant_value = lazy_constant_value ref
type constant_body = {
const_kind : path_kind;
- const_body : constr option;
+ const_body : constant_value option;
const_type : typed_type;
const_hyps : typed_type signature;
const_constraints : constraints;
@@ -23,3 +25,12 @@ let is_defined cb =
match cb.const_body with Some _ -> true | _ -> false
let is_opaque cb = cb.const_opaque
+
+let cook_constant = function
+ | { contents = Cooked c } -> c
+ | { contents = Recipe f } as v -> let c = f () in v := Cooked c; c
+
+type constant_entry = {
+ const_entry_body : lazy_constant_value;
+ const_entry_type : constr option }
+
diff --git a/kernel/constant.mli b/kernel/constant.mli
index 800f95811..c24280c40 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -10,9 +10,15 @@ open Sign
(* Constants (internal representation). *)
+type lazy_constant_value =
+ | Cooked of constr
+ | Recipe of (unit -> constr)
+
+type constant_value = lazy_constant_value ref
+
type constant_body = {
const_kind : path_kind;
- const_body : constr option;
+ const_body : constant_value option;
const_type : typed_type;
const_hyps : typed_type signature;
const_constraints : constraints;
@@ -22,9 +28,11 @@ val is_defined : constant_body -> bool
val is_opaque : constant_body -> bool
+val cook_constant : constant_value -> constr
+
(*s Constant declaration. *)
type constant_entry= {
- const_entry_body : constr;
+ const_entry_body : lazy_constant_value;
const_entry_type : constr option }
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index f3634eac5..e2afdb2a7 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -43,7 +43,8 @@ let constant_value env k =
let cb = lookup_constant sp env in
if not cb.const_opaque & defined_constant env k then
match cb.const_body with
- | Some body ->
+ | Some v ->
+ let body = cook_constant v in
instantiate_constr
(ids_of_sign cb.const_hyps) body (Array.to_list args)
| None ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index efa860fa2..a4cde0371 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -262,11 +262,11 @@ let push_rels vars env =
(* Insertion of constants and parameters in environment. *)
-let add_constant sp ce env =
- let (jb,cst) = safe_machine env ce.const_entry_body in
+let add_constant_with_value sp body typ env =
+ let (jb,cst) = safe_machine env body in
let env' = add_constraints cst env in
let (env'',ty,cst') =
- match ce.const_entry_type with
+ match typ with
| None ->
env', typed_type_of_judgment env' Evd.empty jb, Constraint.empty
| Some ty ->
@@ -281,11 +281,11 @@ let add_constant sp ce env =
error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
in
let ids =
- Idset.union (global_vars_set ce.const_entry_body) (global_vars_set ty.body)
+ Idset.union (global_vars_set body) (global_vars_set ty.body)
in
let cb = {
const_kind = kind_of_path sp;
- const_body = Some ce.const_entry_body;
+ const_body = Some (ref (Cooked body));
const_type = ty;
const_hyps = keep_hyps (var_context env) ids;
const_constraints = Constraint.union cst cst';
@@ -293,6 +293,28 @@ let add_constant sp ce env =
in
add_constant sp cb env''
+let add_lazy_constant sp f t env =
+ let (jt,cst) = safe_machine env t in
+ let env' = add_constraints cst env in
+ let ids = global_vars_set jt.uj_val in
+ let cb = {
+ const_kind = kind_of_path sp;
+ const_body = Some (ref (Recipe f));
+ const_type = assumption_of_judgment env' Evd.empty jt;
+ const_hyps = keep_hyps (var_context env) ids;
+ const_constraints = cst;
+ const_opaque = false }
+ in
+ add_constant sp cb env'
+
+let add_constant sp ce env =
+ match ce.const_entry_body with
+ | Cooked c -> add_constant_with_value sp c ce.const_entry_type env
+ | Recipe f ->
+ (match ce.const_entry_type with
+ | Some typ -> add_lazy_constant sp f typ env
+ | None -> error "you cannot declare a lazy constant without type")
+
let add_parameter sp t env =
let (jt,cst) = safe_machine env t in
let env' = add_constraints cst env in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index eae3f77df..314796ee6 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -30,10 +30,14 @@ val push_var : identifier * constr -> safe_environment -> safe_environment
val push_rel : name * constr -> safe_environment -> safe_environment
val add_constant :
section_path -> constant_entry -> safe_environment -> safe_environment
+val add_lazy_constant :
+ section_path -> (unit -> constr) -> constr -> safe_environment
+ -> safe_environment
val add_parameter :
section_path -> constr -> safe_environment -> safe_environment
val add_mind :
- section_path -> mutual_inductive_entry -> safe_environment -> safe_environment
+ section_path -> mutual_inductive_entry -> safe_environment
+ -> safe_environment
val add_constraints : constraints -> safe_environment -> safe_environment
val lookup_var : identifier -> safe_environment -> name * typed_type
diff --git a/library/declare.ml b/library/declare.ml
index b0ec97632..8da775362 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -98,7 +98,7 @@ let (in_parameter, out_parameter) =
let declare_parameter id c =
let _ = add_leaf id CCI (in_parameter c) in ()
-
+
(* Constants. *)
type constant_declaration = constant_entry * strength
@@ -294,7 +294,8 @@ let declare_eliminations sp i =
let mindstr = string_of_id (mis_typename mispec) in
let declare na c =
declare_constant (id_of_string na)
- ({ const_entry_body = c; const_entry_type = None }, NeverDischarge);
+ ({ const_entry_body = Cooked c; const_entry_type = None },
+ NeverDischarge);
pPNL [< 'sTR na; 'sTR " is defined" >]
in
let env = Global.env () in
diff --git a/library/lib.ml b/library/lib.ml
index 457a27f6e..f7f6f1a51 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -8,8 +8,7 @@ open Summary
type node =
| Leaf of obj
- | OpenedSection of string
- | ClosedSection of string * library_segment
+ | OpenedSection of string * Summary.frozen
| FrozenState of Summary.frozen
and library_segment = (section_path * node) list
@@ -101,7 +100,8 @@ let contents_after = function
let open_section s =
let sp = make_path (id_of_string s) OBJ in
- add_entry sp (OpenedSection s);
+ let fs = freeze_summaries () in
+ add_entry sp (OpenedSection (s,fs));
path_prefix := !path_prefix @ [s];
sp
@@ -120,20 +120,18 @@ let open_module s =
let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
let close_section s =
- let sp =
+ let (sp,frozen) =
try match find_entry_p is_opened_section with
- | sp,OpenedSection s' ->
- if s <> s' then error "this is not the last opened section"; sp
+ | sp,OpenedSection (s',fs) ->
+ if s <> s' then error "this is not the last opened section"; (sp,fs)
| _ -> assert false
with Not_found ->
error "no opened section"
in
let (after,_,before) = split_lib sp in
lib_stk := before;
- add_entry sp (ClosedSection (s,after));
- add_frozen_state ();
pop_path_prefix ();
- (sp,after)
+ (sp,after,frozen)
(* The following function exports the whole library segment, that will be
saved as a module. Objects are presented in chronological order, and
@@ -145,7 +143,7 @@ let export_module () =
| [] -> acc
| (_,Leaf _) as node :: stk -> export (node::acc) stk
| (_,OpenedSection _) :: _ -> error "there are still opened sections"
- | (_,(FrozenState _ | ClosedSection _)) :: stk -> export acc stk
+ | (_,FrozenState _) :: stk -> export acc stk
in
export [] !lib_stk
diff --git a/library/lib.mli b/library/lib.mli
index 3d87abe4d..7261ba7e6 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -13,8 +13,7 @@ open Summary
type node =
| Leaf of obj
- | OpenedSection of string
- | ClosedSection of string * library_segment
+ | OpenedSection of string * Summary.frozen
| FrozenState of Summary.frozen
and library_segment = (section_path * node) list
@@ -34,7 +33,7 @@ val contents_after : section_path option -> library_segment
(*s Opening and closing a section. *)
val open_section : string -> section_path
-val close_section : string -> section_path * library_segment
+val close_section : string -> section_path * library_segment * Summary.frozen
val make_path : identifier -> path_kind -> section_path
val cwd : unit -> string list
diff --git a/library/library.ml b/library/library.ml
index 6edc044a4..cbd478953 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -62,7 +62,6 @@ let (raw_extern_module, raw_intern_module) =
let segment_iter f =
let rec apply = function
| sp,Leaf obj -> f (sp,obj)
- | _,ClosedSection (_,mseg) -> iter mseg
| _,OpenedSection _ -> assert false
| _,FrozenState _ -> ()
and iter seg =
diff --git a/library/redinfo.ml b/library/redinfo.ml
index 7cc35efca..f289273ec 100644
--- a/library/redinfo.ml
+++ b/library/redinfo.ml
@@ -68,7 +68,7 @@ let constant_eval sp =
let cb = Global.lookup_constant sp in
match cb.const_body with
| None -> NotAnElimination
- | Some c -> compute_consteval c
+ | Some v -> let c = cook_constant v in compute_consteval c
in
eval_table := Spmap.add sp v !eval_table;
v
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index f12f5edec..848a2132e 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -49,7 +49,8 @@ let print_typed_value_in_env env (trm,typ) =
let print_typed_value x = print_typed_value_in_env (Global.env ()) x
let print_recipe = function
- | Some c -> prterm c
+ | Some { contents = Cooked c } -> prterm c
+ | Some { contents = Recipe _ } -> [< 'sTR"<recipe>" >]
| None -> [< 'sTR"<uncookable>" >]
let fprint_recipe = function
@@ -280,13 +281,7 @@ let rec print_library_entry with_values ent =
match ent with
| (sp,Lib.Leaf lobj) ->
[< print_leaf_entry with_values sep (sp,lobj) >]
- | (s,Lib.ClosedSection(_,ctxt)) ->
- [< 'sTR"Closed Section " ; 'sTR (string_of_path s) ; 'fNL ;
- if !print_closed_sections then
- [< 'sTR " " ; hOV 0 [< print_context with_values ctxt >] >]
- else
- [< >] >]
- | (_,Lib.OpenedSection str) ->
+ | (_,Lib.OpenedSection (str,_)) ->
[< 'sTR(" >>>>>>> Section " ^ str) ; 'fNL >]
| (_,Lib.FrozenState _) ->
[< >]
@@ -379,8 +374,7 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name =
crible_rec rest
| _ -> crible_rec rest)
- | (_, (Lib.OpenedSection _ | Lib.ClosedSection _
- | Lib.FrozenState _))::rest ->
+ | (_, (Lib.OpenedSection _ | Lib.FrozenState _))::rest ->
crible_rec rest
| [] -> ()
in
@@ -396,7 +390,7 @@ let print_crible name =
let read_sec_context sec =
let rec get_cxt in_cxt = function
- | ((sp,Lib.OpenedSection str) as hd)::rest ->
+ | ((sp,Lib.OpenedSection (str,_)) as hd)::rest ->
if str = sec then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
| [] -> []
| hd::rest -> get_cxt (hd::in_cxt) rest
@@ -495,7 +489,6 @@ let print_local_context () =
[< print_last_const rest;print_mutual sp mib; 'fNL >]
| "VARIABLE" -> [< >]
| _ -> print_last_const rest)
- | (sp,Lib.ClosedSection _)::rest -> print_last_const rest
| _ -> [< >]
in
[< print_var_rec env; print_last_const env >]
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 12f53c685..e2f5ce94b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -175,7 +175,8 @@ let save_named opacity =
and strength = ts.top_strength in
let pfterm = extract_pftreestate pfs in
declare_constant (id_of_string ident)
- ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength);
+ ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl },
+ strength);
del_proof ident;
message(ident ^ " is defined")
@@ -187,11 +188,13 @@ let save_anonymous opacity save_ident n =
let pfterm = extract_pftreestate pfs in
if ident = "Unnamed_thm" then
declare_constant (id_of_string save_ident)
- ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength)
+ ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl },
+ strength)
else begin
message("Overriding name " ^ ident ^ " and using " ^ save_ident);
declare_constant (id_of_string save_ident)
- ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength)
+ ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl },
+ strength)
end;
del_proof ident;
message(save_ident ^ " is defined")
diff --git a/toplevel/class.ml b/toplevel/class.ml
index d4cd6fec6..7912b2fdf 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -289,7 +289,8 @@ let build_id_coercion idf_opt ids =
id_of_string ("Id_"^(string_of_id ids)^"_"^
(string_of_cl (fst (constructor_at_head t))))
in
- let constr_entry = {const_entry_body = constr_f; const_entry_type = None } in
+ let constr_entry =
+ { const_entry_body = Cooked constr_f; const_entry_type = None } in
declare_constant idf (constr_entry,NeverDischarge);
idf
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 882033919..776864d70 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -32,10 +32,10 @@ let constant_entry_of_com com =
let env = Global.env() in
match com with
| Node(_,"CAST",[_;t]) ->
- { const_entry_body = constr_of_com sigma env com;
+ { const_entry_body = Cooked (constr_of_com sigma env com);
const_entry_type = Some (constr_of_com1 true sigma env t) }
| _ ->
- { const_entry_body = constr_of_com sigma env com;
+ { const_entry_body = Cooked (constr_of_com sigma env com);
const_entry_type = None }
let definition_body ident n com =
@@ -44,9 +44,13 @@ let definition_body ident n com =
let red_constant_entry ce = function
| None -> ce
- | Some red ->
+ | Some red ->
+ let body = match ce.const_entry_body with
+ | Cooked c -> c
+ | Recipe _ -> assert false
+ in
{ const_entry_body =
- reduction_of_redexp red (Global.env()) Evd.empty ce.const_entry_body;
+ Cooked (reduction_of_redexp red (Global.env()) Evd.empty body);
const_entry_type =
ce.const_entry_type }
@@ -233,9 +237,11 @@ let build_recursive lnameargsardef =
let varrec = Array.of_list larrec in
let rec declare i = function
| fi::lf ->
- let ce = { const_entry_body =
- mkFixDlam (Array.of_list nvrec) i varrec recvec;
- const_entry_type = None } in
+ let ce =
+ { const_entry_body =
+ Cooked (mkFixDlam (Array.of_list nvrec) i varrec recvec);
+ const_entry_type = None }
+ in
declare_constant fi (ce, n);
declare (i+1) lf
| _ -> ()
@@ -249,7 +255,7 @@ let build_recursive lnameargsardef =
let _ =
List.fold_left
(fun subst (f,def) ->
- let ce = { const_entry_body = Generic.replace_vars subst def;
+ let ce = { const_entry_body = Cooked (Generic.replace_vars subst def);
const_entry_type = None } in
declare_constant f (ce,n);
warning ((string_of_id f)^" is non-recursively defined");
@@ -297,9 +303,11 @@ let build_corecursive lnameardef =
in
let rec declare i = function
| fi::lf ->
- let ce = { const_entry_body =
- mkCoFixDlam i (Array.of_list larrec) recvec;
- const_entry_type = None } in
+ let ce =
+ { const_entry_body =
+ Cooked (mkCoFixDlam i (Array.of_list larrec) recvec);
+ const_entry_type = None }
+ in
declare_constant fi (ce,n);
declare (i+1) lf
| _ -> ()
@@ -312,7 +320,7 @@ let build_corecursive lnameardef =
let _ =
List.fold_left
(fun subst (f,def) ->
- let ce = { const_entry_body = Generic.replace_vars subst def;
+ let ce = { const_entry_body = Cooked (Generic.replace_vars subst def);
const_entry_type = None } in
declare_constant f (ce,n);
warning ((string_of_id f)^" is non-recursively defined");
@@ -337,7 +345,8 @@ let build_scheme lnamedepindsort =
let rec declare i = function
| fi::lf ->
let ce =
- { const_entry_body = listdecl.(i); const_entry_type = None } in
+ { const_entry_body = Cooked listdecl.(i); const_entry_type = None }
+ in
declare_constant fi (ce,n);
declare (i+1) lf
| _ -> ()
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 84b357c5d..f0a97c218 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -74,7 +74,14 @@ let abstract_constant ids_to_abs hyps (body,typ) =
let name = Name id in
let var = snd (hd_sign hyps) in
let cvar = incast_type var in
- let body' = mkLambda name cvar (subst_var id body) in
+ let body' = match body with
+ | None -> None
+ | Some { contents = Cooked c } ->
+ Some (ref (Cooked (mkLambda name cvar (subst_var id c))))
+ | Some { contents = Recipe f } ->
+ Some (ref (Recipe
+ (fun () -> mkLambda name cvar (subst_var id (f())))))
+ in
let typ' =
{ body = mkProd name cvar (subst_var id typ.body);
typ = sort_of_product_without_univ var.typ typ.typ }
@@ -88,29 +95,21 @@ let abstract_constant ids_to_abs hyps (body,typ) =
(* Substitutions. *)
-let expmod_constr modlist c =
- let env = Global.env() in
+let expmod_constr oldenv modlist c =
let sigma = Evd.empty in
- let simpfun = if modlist = [] then fun x -> x else nf_betaiota env sigma in
- let expfun c =
- let (sp,_) = destConst c in
+ let simpfun =
+ if modlist = [] then fun x -> x else nf_betaiota oldenv sigma in
+ let expfun cst =
try
- constant_value env c
- with Failure _ -> begin
- mSGERRNL
+ constant_value oldenv cst
+ with Failure _ ->
+ let (sp,_) = destConst cst in
+ errorlabstrm "expmod_constr"
[< 'sTR"Cannot unfold the value of " ;
'sTR(string_of_path sp) ; 'sPC;
'sTR"You cannot declare local lemmas as being opaque"; 'sPC;
'sTR"and then require that theorems which use them"; 'sPC;
'sTR"be transparent" >];
- let cb = Global.lookup_constant sp in
- cb.const_opaque <- false;
- (try
- let v = constant_value env c in
- cb.const_opaque <- true;
- v
- with _ -> anomaly "expmod_constr")
- end
in
let under_casts f = function
| DOP2(Cast,c,t) -> (DOP2(Cast,f c,f t))
@@ -118,27 +117,34 @@ let expmod_constr modlist c =
in
let c' = modify_opers expfun (fun a b -> mkAppL [|a; b|]) modlist c in
match c' with
- | DOP2(Cast,val_0,typ) -> DOP2(Cast,simpfun val_0,simpfun typ)
- | DOP2(XTRA "IND",c,DLAMV(na,lc)) ->
- DOP2(XTRA "IND",under_casts simpfun c,
- DLAMV(na,Array.map (under_casts simpfun) lc))
+ | DOP2 (Cast,val_0,typ) -> DOP2 (Cast,simpfun val_0,simpfun typ)
| _ -> simpfun c'
-let expmod_type modlist {body=c;typ=s} = {body=expmod_constr modlist c;typ=s}
+let expmod_type oldenv modlist {body=c;typ=s} =
+ { body = expmod_constr oldenv modlist c; typ = s }
+let expmod_constant_value opaque oldenv modlist = function
+ | None -> None
+ | Some { contents = Cooked c } ->
+ if opaque then
+ Some (ref (Recipe (fun () -> expmod_constr oldenv modlist c)))
+ else
+ Some (ref (Cooked (expmod_constr oldenv modlist c)))
+ | Some { contents = Recipe f } ->
+ Some (ref (Recipe (fun () -> expmod_constr oldenv modlist (f ()))))
(* Discharge of inductive types. *)
-let process_inductive osecsp nsecsp (ids_to_discard,modlist) mib =
+let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
assert (Array.length mib.mind_packets > 0);
let finite = mib.mind_packets.(0).mind_finite in
let inds =
array_map_to_list
(fun mip ->
(mip.mind_typename,
- expmod_type modlist mip.mind_arity,
+ expmod_type oldenv modlist mip.mind_arity,
Array.to_list mip.mind_consnames,
- under_dlams (expmod_constr modlist) mip.mind_lc))
+ under_dlams (expmod_constr oldenv modlist) mip.mind_lc))
mib.mind_packets
in
let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in
@@ -162,22 +168,22 @@ let process_inductive osecsp nsecsp (ids_to_discard,modlist) mib =
(* Discharge of constants. *)
-let process_constant osecsp nsecsp (ids_to_discard,modlist) cb =
- let body = global_reference CCI (basename osecsp) in
- let typ = expmod_type modlist cb.const_type in
+let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb =
+ let body =
+ expmod_constant_value cb.const_opaque oldenv modlist cb.const_body in
+ let typ = expmod_type oldenv modlist cb.const_type in
let (body',typ',modl) =
abstract_constant ids_to_discard cb.const_hyps (body,typ)
in
let mods = (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) :: modlist in
- ({ const_entry_body = body'; const_entry_type = Some typ'.body },
- mods)
+ (body', typ'.body, mods)
(* Discharge of the various objects of the environment. *)
-let constant_message sp =
+let constant_message id =
if Options.verbose() then
- pPNL [< print_id (basename sp); 'sTR " is discharged." >]
+ pPNL [< print_id id; 'sTR " is discharged." >]
let inductive_message inds =
if Options.verbose() then
@@ -189,74 +195,80 @@ let inductive_message inds =
(fun (id,_,_,_) -> print_id id) l;
'sPC; 'sTR "are discharged.">]))
-let process_object sec_sp (ids_to_discard,work_alist) (sp,lobj) =
+type discharge_operation =
+ | Variable of identifier * constr * strength * bool
+ | Parameter of identifier * constr
+ | Constant of identifier * constant_entry * strength
+ | Inductive of mutual_inductive_entry
+ | Class of cl_typ * cl_info_typ
+ | Struc of section_path * struc_typ
+ | Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ)
+ * identifier * int
+
+let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
let tag = object_tag lobj in
match tag with
| "VARIABLE" ->
let (id,a,stre,sticky) = out_variable sp in
if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then
- (id::ids_to_discard,work_alist)
- else begin
- let expmod_a = expmod_constr work_alist a.body in
- declare_variable id (expmod_a,stre,sticky);
- (ids_to_discard,work_alist)
- end
+ (ops,id::ids_to_discard,work_alist)
+ else
+ let expmod_a = expmod_constr oldenv work_alist a.body in
+ (Variable (id,expmod_a,stre,sticky) :: ops,
+ ids_to_discard,work_alist)
| "CONSTANT" ->
let stre = constant_strength sp in
if stre = (DischargeAt sec_sp) then
- (ids_to_discard, (Const sp, DO_REPLACE) :: work_alist)
- else begin
- let cb = Global.lookup_constant sp in
+ (ops, ids_to_discard, (Const sp, DO_REPLACE) :: work_alist)
+ else
+ let cb = Environ.lookup_constant sp oldenv in
let spid = basename sp in
let newsp = recalc_sp sp in
- let (ce,mods) =
- process_constant sp newsp (ids_to_discard,work_alist) cb in
- declare_constant spid (ce,stre);
- constant_message sp;
- (ids_to_discard,mods@work_alist)
- end
+ let (body,typ,mods) =
+ process_constant sp newsp oldenv (ids_to_discard,work_alist) cb in
+ let op = match body with
+ | None ->
+ Parameter (spid,typ)
+ | Some { contents = b } ->
+ let ce =
+ { const_entry_body = b; const_entry_type = Some typ } in
+ Constant (spid,ce,stre)
+ in
+ (op::ops, ids_to_discard, mods@work_alist)
| "INDUCTIVE" ->
- let mib = Global.lookup_mind sp in
+ let mib = Environ.lookup_mind sp oldenv in
let newsp = recalc_sp sp in
let (mie,mods) =
- process_inductive sp newsp (ids_to_discard,work_alist) mib in
- let _ = declare_mind mie in
- inductive_message mie.mind_entry_inds;
- (ids_to_discard,mods@work_alist)
+ process_inductive sp newsp oldenv (ids_to_discard,work_alist) mib in
+ ((Inductive mie)::ops, ids_to_discard, mods@work_alist)
| "CLASS" ->
let ((cl,clinfo) as x) = outClass lobj in
if clinfo.cL_STRE = (DischargeAt sec_sp) then
- (ids_to_discard,work_alist)
- else begin
- let y = process_class sec_sp x in
- Lib.add_anonymous_leaf (inClass y);
- (ids_to_discard,work_alist)
- end
+ (ops,ids_to_discard,work_alist)
+ else
+ let (y1,y2) = process_class sec_sp x in
+ ((Class (y1,y2))::ops, ids_to_discard, work_alist)
| "COERCION" ->
let (((_,coeinfo),_,_)as x) = outCoercion lobj in
if coeinfo.cOE_STRE = (DischargeAt sec_sp) then
- (ids_to_discard,work_alist)
- else begin
- let ((_,_,clt) as y),idf,ps = process_coercion sec_sp x in
- Lib.add_anonymous_leaf (inCoercion y);
- coercion_syntax idf ps clt;
- (ids_to_discard,work_alist)
- end
+ (ops,ids_to_discard,work_alist)
+ else
+ let (y,idf,ps) = process_coercion sec_sp x in
+ ((Coercion (y,idf,ps))::ops, ids_to_discard, work_alist)
| "STRUCTURE" ->
let (sp,info) = outStruc lobj in
let newsp = recalc_sp sp in
- let mib = Global.lookup_mind (ccisp_of newsp) in
+ let mib = Environ.lookup_mind newsp oldenv in
let strobj =
- { s_CONST= info.s_CONST;
- s_PARAM= mib.mind_nparams;
- s_PROJ= List.map (option_app recalc_sp) info.s_PROJ} in
- Lib.add_anonymous_leaf (inStruc (newsp,strobj));
- (ids_to_discard,work_alist)
+ { s_CONST = info.s_CONST;
+ s_PARAM = mib.mind_nparams;
+ s_PROJ = List.map (option_app recalc_sp) info.s_PROJ } in
+ ((Struc (newsp,strobj))::ops, ids_to_discard, work_alist)
(***TODO
| "OBJDEF1" ->
@@ -266,14 +278,38 @@ let process_object sec_sp (ids_to_discard,work_alist) (sp,lobj) =
(ids_to_discard,work_alist)
***)
- | _ ->
- (ids_to_discard,work_alist)
+ | _ -> (ops,ids_to_discard,work_alist)
-let process_item sec_sp acc = function
- | (sp,Leaf lobj) -> process_object sec_sp acc (sp,lobj)
+let process_item oldenv sec_sp acc = function
+ | (sp,Leaf lobj) -> process_object oldenv sec_sp acc (sp,lobj)
| (_,_) -> acc
+let process_operation = function
+ | Variable (id,expmod_a,stre,sticky) ->
+ declare_variable id (expmod_a,stre,sticky)
+ | Parameter (spid,typ) ->
+ declare_parameter spid typ;
+ constant_message spid
+ | Constant (spid,ce,stre) ->
+ declare_constant spid (ce,stre);
+ constant_message spid
+ | Inductive mie ->
+ let _ = declare_mind mie in
+ inductive_message mie.mind_entry_inds
+ | Class (y1,y2) ->
+ Lib.add_anonymous_leaf (inClass (y1,y2))
+ | Struc (newsp,strobj) ->
+ Lib.add_anonymous_leaf (inStruc (newsp,strobj))
+ | Coercion ((_,_,clt) as y,idf,ps) ->
+ Lib.add_anonymous_leaf (inCoercion y);
+ coercion_syntax idf ps clt
+
let close_section _ s =
- let (sec_sp,decls) = close_section s in
- let _ = List.fold_left (process_item sec_sp) ([],[]) decls in
- ()
+ let oldenv = Global.env() in
+ let (sec_sp,decls,frozen) = close_section s in
+ let (ops,_,_) =
+ List.fold_left (process_item oldenv sec_sp) ([],[],[]) decls in
+ Summary.unfreeze_summaries frozen;
+ List.iter process_operation (List.rev ops)
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 04:35:23 +0000