aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile7
-rw-r--r--interp/notation.ml71
-rw-r--r--kernel/cooking.ml223
-rw-r--r--kernel/cooking.mli16
-rw-r--r--library/declare.ml222
-rw-r--r--library/declare.mli18
-rw-r--r--library/dischargedhypsmap.ml7
-rw-r--r--library/impargs.ml40
-rw-r--r--library/impargs.mli2
-rw-r--r--library/lib.ml134
-rw-r--r--library/lib.mli24
-rw-r--r--library/libobject.ml12
-rw-r--r--library/libobject.mli2
-rw-r--r--library/library.ml3
-rw-r--r--library/library.mli6
-rwxr-xr-xpretyping/classops.ml149
-rw-r--r--pretyping/classops.mli19
-rwxr-xr-xpretyping/recordops.ml190
-rwxr-xr-xpretyping/recordops.mli36
-rw-r--r--toplevel/class.ml172
-rw-r--r--toplevel/class.mli17
-rw-r--r--toplevel/discharge.ml349
-rw-r--r--toplevel/discharge.mli13
-rwxr-xr-xtoplevel/recordobj.ml65
-rwxr-xr-xtoplevel/recordobj.mli2
25 files changed, 738 insertions, 1061 deletions
diff --git a/Makefile b/Makefile
index dc366cd91..e9c7e0bdb 100644
--- a/Makefile
+++ b/Makefile
@@ -161,7 +161,7 @@ INTERP=\
interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \
library/impargs.cmo interp/constrintern.cmo \
interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \
- library/declare.cmo
+ toplevel/discharge.cmo library/declare.cmo
PROOFS=\
proofs/tacexpr.cmo proofs/proof_type.cmo proofs/redexpr.cmo \
@@ -206,9 +206,8 @@ TACTICS=\
TOPLEVEL=\
toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \
toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \
- toplevel/command.cmo \
- toplevel/record.cmo toplevel/recordobj.cmo \
- toplevel/discharge.cmo translate/ppvernacnew.cmo \
+ toplevel/command.cmo toplevel/record.cmo \
+ translate/ppvernacnew.cmo \
toplevel/vernacinterp.cmo toplevel/mltop.cmo \
toplevel/vernacentries.cmo toplevel/vernac.cmo \
toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \
diff --git a/interp/notation.ml b/interp/notation.ml
index f90219b24..c3903cfc1 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -13,6 +13,7 @@ open Util
open Pp
open Bigint
open Names
+open Term
open Nametab
open Libnames
open Summary
@@ -93,9 +94,14 @@ let current_scopes () = !scope_stack
(* TODO: push nat_scope, z_scope, ... in scopes summary *)
(* Exportation of scopes *)
-let cache_scope (_,(local,op,sc)) =
+let open_scope i (_,(local,op,sc)) =
+ if i=1 then begin
(match sc with Scope sc -> check_scope sc | _ -> ());
scope_stack := if op then sc :: !scope_stack else list_except sc !scope_stack
+ end
+
+let cache_scope o =
+ open_scope 1 o
let subst_scope (_,subst,sc) = sc
@@ -109,7 +115,7 @@ let export_scope (local,_,_ as x) = if local then None else Some x
let (inScope,outScope) =
declare_object {(default_object "SCOPE") with
cache_function = cache_scope;
- open_function = (fun i o -> if i=1 then cache_scope o);
+ open_function = open_scope;
subst_function = subst_scope;
classify_function = classify_scope;
export_function = export_scope }
@@ -361,31 +367,6 @@ let exists_notation_in_scope scopt ntn r =
r' = r, pp8only
with Not_found -> false, false
-(* Special scopes associated to arguments of a global reference *)
-
-let arguments_scope = ref Refmap.empty
-
-let cache_arguments_scope (_,(r,scl)) =
- List.iter (option_iter check_scope) scl;
- arguments_scope := Refmap.add r scl !arguments_scope
-
-let subst_arguments_scope (_,subst,(r,scl)) = (fst (subst_global subst r),scl)
-
-let (inArgumentsScope,outArgumentsScope) =
- declare_object {(default_object "ARGUMENTS-SCOPE") with
- cache_function = cache_arguments_scope;
- load_function = (fun _ o -> cache_arguments_scope o);
- subst_function = subst_arguments_scope;
- classify_function = (fun (_,o) -> Substitute o);
- export_function = (fun x -> Some x) }
-
-let declare_arguments_scope r scl =
- Lib.add_anonymous_leaf (inArgumentsScope (r,scl))
-
-let find_arguments_scope r =
- try Refmap.find r !arguments_scope
- with Not_found -> []
-
(**********************************************************************)
(* Mapping classes to scopes *)
@@ -401,8 +382,6 @@ let declare_class_scope sc cl =
let find_class_scope cl =
Gmap.find cl !class_scope_map
-open Term
-
let find_class t =
let t, _ = decompose_app (Reductionops.whd_betaiotazeta t) in
match kind_of_term t with
@@ -413,6 +392,9 @@ let find_class t =
| Sort _ -> CL_SORT
| _ -> raise Not_found
+(**********************************************************************)
+(* Special scopes associated to arguments of a global reference *)
+
let rec compute_arguments_scope t =
match kind_of_term (Reductionops.whd_betaiotazeta t) with
| Prod (_,t,u) ->
@@ -421,6 +403,37 @@ let rec compute_arguments_scope t =
sc :: compute_arguments_scope u
| _ -> []
+let arguments_scope = ref Refmap.empty
+
+let load_arguments_scope _ (_,(r,scl)) =
+ List.iter (option_iter check_scope) scl;
+ arguments_scope := Refmap.add r scl !arguments_scope
+
+let cache_arguments_scope o =
+ load_arguments_scope 1 o
+
+let subst_arguments_scope (_,subst,(r,scl)) = (fst (subst_global subst r),scl)
+
+let discharge_arguments_scope (r,_) =
+ match r with
+ | VarRef _ -> None
+ | _ -> Some (r,compute_arguments_scope (Global.type_of_global r))
+
+let (inArgumentsScope,outArgumentsScope) =
+ declare_object {(default_object "ARGUMENTS-SCOPE") with
+ cache_function = cache_arguments_scope;
+ load_function = load_arguments_scope;
+ subst_function = subst_arguments_scope;
+ classify_function = (fun (_,o) -> Substitute o);
+ export_function = (fun x -> Some x) }
+
+let declare_arguments_scope r scl =
+ Lib.add_anonymous_leaf (inArgumentsScope (r,scl))
+
+let find_arguments_scope r =
+ try Refmap.find r !arguments_scope
+ with Not_found -> []
+
let declare_ref_arguments_scope ref =
let t = Global.type_of_global ref in
declare_arguments_scope ref (compute_arguments_scope t)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 9869afcf5..53a9b9644 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -19,155 +19,110 @@ open Reduction
(*s Cooking the constants. *)
-type 'a modification =
- | NOT_OCCUR
- | DO_ABSTRACT of 'a * constr array
- | DO_REPLACE of constant_body
+type work_list = identifier array Cmap.t * identifier array KNmap.t
-type work_list =
- (constant * constant modification) list
- * (inductive * inductive modification) list
- * (constructor * constructor modification) list
+let dirpath_prefix p = match repr_dirpath p with
+ | [] -> anomaly "dirpath_prefix: empty dirpath"
+ | _::l -> make_dirpath l
-type recipe = {
- d_from : constant_body;
- d_abstract : identifier list;
- d_modlist : work_list }
+let pop_kn kn =
+ let (mp,dir,l) = Names.repr_kn kn in
+ Names.make_kn mp (dirpath_prefix dir) l
+
+let pop_con con =
+ let (mp,dir,l) = Names.repr_con con in
+ Names.make_con mp (dirpath_prefix dir) l
+
+type my_global_reference =
+ | ConstRef of constant
+ | IndRef of inductive
+ | ConstructRef of constructor
+
+let cache = (Hashtbl.create 13 : (my_global_reference, constr) Hashtbl.t)
+
+let clear_cooking_sharing () = Hashtbl.clear cache
+
+let share r (cstl,knl) =
+ try Hashtbl.find cache r
+ with Not_found ->
+ let f,l =
+ match r with
+ | IndRef (kn,i) ->
+ mkInd (pop_kn kn,i), KNmap.find kn knl
+ | ConstructRef ((kn,i),j) ->
+ mkConstruct ((pop_kn kn,i),j), KNmap.find kn knl
+ | ConstRef cst ->
+ mkConst (pop_con cst), Cmap.find cst cstl in
+ let c = mkApp (f, Array.map mkVar l) in
+ Hashtbl.add cache r c;
+ (* has raised Not_found if not in work_list *)
+ c
-let failure () =
- anomalylabstrm "generic__modify_opers"
- (str"An oper which was never supposed to appear has just appeared" ++
- spc () ++ str"Either this is in system code, and you need to" ++ spc () ++
- str"report this error," ++ spc () ++
- str"Or you are using a user-written tactic which calls" ++ spc () ++
- str"generic__modify_opers, in which case the user-written code" ++
- spc () ++ str"is broken - this function is an internal system" ++
- spc () ++ str"for internal system use only")
-
-let modify_opers replfun (constl,indl,cstrl) =
+let update_case_info ci modlist =
+ try
+ let ind, n =
+ match kind_of_term (share (IndRef ci.ci_ind) modlist) with
+ | App (f,l) -> (destInd f, Array.length l)
+ | Ind ind -> ind, 0
+ | _ -> assert false in
+ { ci with ci_ind = ind; ci_npar = ci.ci_npar + n }
+ with Not_found ->
+ ci
+
+let empty_modlist = (Cmap.empty, KNmap.empty)
+
+let expmod_constr modlist c =
let rec substrec c =
- let c' = map_constr substrec c in
- match kind_of_term c' with
+ match kind_of_term c with
| Case (ci,p,t,br) ->
+ map_constr substrec (mkCase (update_case_info ci modlist,p,t,br))
+
+ | Ind ind ->
(try
- match List.assoc ci.ci_ind indl with
- | DO_ABSTRACT (ind,abs_vars) ->
- let n' = Array.length abs_vars + ci.ci_npar in
- let ci' = { ci with
- ci_ind = ind;
- ci_npar = n' } in
- mkCase (ci',p,t,br)
- | _ -> raise Not_found
- with
- | Not_found -> c')
-
- | Ind spi ->
- (try
- (match List.assoc spi indl with
- | NOT_OCCUR -> failure ()
- | DO_ABSTRACT (oper',abs_vars) ->
- mkApp (mkInd oper', abs_vars)
- | DO_REPLACE _ -> assert false)
+ share (IndRef ind) modlist
with
- | Not_found -> c')
-
- | Construct spi ->
+ | Not_found -> map_constr substrec c)
+
+ | Construct cstr ->
(try
- (match List.assoc spi cstrl with
- | NOT_OCCUR -> failure ()
- | DO_ABSTRACT (oper',abs_vars) ->
- mkApp (mkConstruct oper', abs_vars)
- | DO_REPLACE _ -> assert false)
+ share (ConstructRef cstr) modlist
with
- | Not_found -> c')
-
- | Const kn ->
+ | Not_found -> map_constr substrec c)
+
+ | Const cst ->
(try
- (match List.assoc kn constl with
- | NOT_OCCUR -> failure ()
- | DO_ABSTRACT (oper',abs_vars) ->
- mkApp (mkConst oper', abs_vars)
- | DO_REPLACE cb -> substrec (replfun (kn,cb)))
+ share (ConstRef cst) modlist
with
- | Not_found -> c')
-
- | _ -> c'
- in
- if (constl,indl,cstrl) = ([],[],[]) then fun x -> x else substrec
+ | Not_found -> map_constr substrec c)
+
+ | _ -> map_constr substrec c
-let expmod_constr modlist c =
- let simpfun =
- if modlist = ([],[],[]) then fun x -> x else nf_betaiota in
- let expfun (kn,cb) =
- if cb.const_opaque then
- errorlabstrm "expmod_constr"
- (str"Cannot unfold the value of " ++
- str(string_of_con kn) ++ spc () ++
- str"You cannot declare local lemmas as being opaque" ++ spc () ++
- str"and then require that theorems which use them" ++ spc () ++
- str"be transparent");
- match cb.const_body with
- | Some body -> Declarations.force body
- | None -> assert false
- in
- let c' = modify_opers expfun modlist c in
- match kind_of_term c' with
- | Cast (value,typ) -> mkCast (simpfun value,simpfun typ)
- | _ -> simpfun c'
-
-let expmod_type modlist c =
- type_app (expmod_constr modlist) c
-
-let abstract_constant ids_to_abs hyps (body,typ) =
- let abstract_once_typ ((hyps,typ) as sofar) id =
- match hyps with
- | (hyp,c,t as decl)::rest when hyp = id ->
- let typ' = mkNamedProd_wo_LetIn decl typ in
- (rest, typ')
- | _ ->
- sofar
- in
- let abstract_once_body ((hyps,body) as sofar) id =
- match hyps with
- | (hyp,c,t as decl)::rest when hyp = id ->
- let body' = mkNamedLambda_or_LetIn decl body in
- (rest, body')
- | _ ->
- sofar
- in
- let (_,typ') =
- List.fold_left abstract_once_typ (hyps,typ) ids_to_abs
- in
- let body' = match body with
- None -> None
- | Some l_body ->
- Some (Declarations.from_val
- (let body = Declarations.force l_body in
- let (_,body') =
- List.fold_left abstract_once_body (hyps,body) ids_to_abs
- in
- body'))
in
- (body',typ')
+ if modlist = empty_modlist then c
+ else under_outer_cast nf_betaiota (substrec c)
+
+let abstract_constant_type =
+ List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c)
+
+let abstract_constant_body =
+ List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
+
+type recipe = {
+ d_from : constant_body;
+ d_abstract : named_context;
+ d_modlist : work_list }
+
+let on_body f =
+ option_app (fun c -> Declarations.from_val (f (Declarations.force c)))
let cook_constant env r =
let cb = r.d_from in
- let typ = expmod_type r.d_modlist cb.const_type in
- let body =
- option_app
- (fun lconstr ->
- Declarations.from_val
- (expmod_constr r.d_modlist (Declarations.force lconstr)))
- cb.const_body
- in
- let hyps =
- Sign.fold_named_context
- (fun d ctxt ->
- Sign.add_named_decl
- (map_named_declaration (expmod_constr r.d_modlist) d)
- ctxt)
- cb.const_hyps
- ~init:empty_named_context in
- let body,typ = abstract_constant r.d_abstract hyps (body,typ) in
+ let hyps = Sign.map_named_context (expmod_constr r.d_modlist) r.d_abstract in
+ let body =
+ on_body (fun c ->
+ abstract_constant_body (expmod_constr r.d_modlist c) hyps)
+ cb.const_body in
+ let typ =
+ abstract_constant_type (expmod_constr r.d_modlist cb.const_type) hyps in
let boxed = Cemitcodes.is_boxed cb.const_body_code in
(body, typ, cb.const_constraints, cb.const_opaque, boxed)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 289373eff..2e7a3639a 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -16,19 +16,11 @@ open Univ
(*s Cooking the constants. *)
-type 'a modification =
- | NOT_OCCUR
- | DO_ABSTRACT of 'a * constr array
- | DO_REPLACE of constant_body
-
-type work_list =
- (constant * constant modification) list
- * (inductive * inductive modification) list
- * (constructor * constructor modification) list
+type work_list = identifier array Cmap.t * identifier array KNmap.t
type recipe = {
d_from : constant_body;
- d_abstract : identifier list;
+ d_abstract : Sign.named_context;
d_modlist : work_list }
val cook_constant :
@@ -38,6 +30,8 @@ val cook_constant :
(*s Utility functions used in module [Discharge]. *)
val expmod_constr : work_list -> constr -> constr
-val expmod_type : work_list -> types -> types
+
+val clear_cooking_sharing : unit -> unit
+
diff --git a/library/declare.ml b/library/declare.ml
index 2109c6325..6bace2654 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -31,11 +31,7 @@ open Decl_kinds
(**********************************************)
-(* For [DischargeAt (dir,n)], [dir] is the minimum prefix that a
- construction keeps in its name (if persistent), or the section name
- beyond which it is discharged (if volatile); the integer [n]
- (useful only for persistent constructions), is the length of the section
- part in [dir] *)
+(* Strength *)
open Nametab
@@ -75,13 +71,16 @@ type checked_variable_declaration =
let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t)
let _ = Summary.declare_summary "VARIABLE"
- { Summary.freeze_function = (fun () -> !vartab);
- Summary.unfreeze_function = (fun ft -> vartab := ft);
- Summary.init_function = (fun () -> vartab := Idmap.empty);
- Summary.survive_module = false;
- Summary.survive_section = false }
-
-let cache_variable ((sp,_),(id,(p,d,mk))) =
+ { Summary.freeze_function = (fun () -> !vartab);
+ Summary.unfreeze_function = (fun ft -> vartab := ft);
+ Summary.init_function = (fun () -> vartab := Idmap.empty);
+ Summary.survive_module = false;
+ Summary.survive_section = false }
+
+let cache_variable ((sp,_),o) =
+ match o with
+ | Inl cst -> Global.add_constraints cst
+ | Inr (id,(p,d,mk)) ->
(* Constr raisonne sur les noms courts *)
if Idmap.mem id !vartab then
errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
@@ -95,31 +94,33 @@ let cache_variable ((sp,_),(id,(p,d,mk))) =
let (_,bd,ty) = Global.lookup_named id in
CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in
Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
+ add_section_variable id;
+ Dischargedhypsmap.set_discharged_hyps sp [];
vartab := Idmap.add id (p,vd,mk) !vartab
+let get_variable_constraints id =
+ match pi2 (Idmap.find id !vartab) with
+ | CheckedSectionLocalDef (c,ty,cst,opaq) -> cst
+ | CheckedSectionLocalAssum (ty,cst) -> cst
+
+let discharge_variable (_,o) = match o with
+ | Inr (id,_) -> Some (Inl (get_variable_constraints id))
+ | Inl _ -> Some o
+
let (in_variable, out_variable) =
declare_object { (default_object "VARIABLE") with
cache_function = cache_variable;
+ discharge_function = discharge_variable;
classify_function = (fun _ -> Dispose) }
-let declare_variable_common id obj =
- let oname = add_leaf id (in_variable (id,obj)) in
- declare_var_implicits id;
- Notation.declare_ref_arguments_scope (VarRef id);
- oname
-
(* for initial declaration *)
let declare_variable id obj =
- let (sp,kn as oname) = declare_variable_common id obj in
+ let oname = add_leaf id (in_variable (Inr (id,obj))) in
+ declare_var_implicits id;
+ Notation.declare_ref_arguments_scope (VarRef id);
!xml_declare_variable oname;
- Dischargedhypsmap.set_discharged_hyps sp [];
oname
-(* when coming from discharge: no xml output *)
-let redeclare_variable id discharged_hyps obj =
- let oname = declare_variable_common id obj in
- Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps
-
(* Globals: constants and parameters *)
type constant_declaration = constant_entry * global_kind
@@ -133,37 +134,56 @@ let _ = Summary.declare_summary "CONSTANT"
Summary.survive_module = false;
Summary.survive_section = false }
-let cache_constant ((sp,kn),(cdt,kind)) =
- (if Idmap.mem (basename sp) !vartab then
- errorlabstrm "cache_constant"
- (pr_id (basename sp) ++ str " already exists"));
- (if Nametab.exists_cci sp then
- let (_,id) = repr_path sp in
- errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
- let _,dir,_ = repr_kn kn in
- let kn' = Global.add_constant dir (basename sp) cdt in
- if kn' <> (constant_of_kn kn) then
- anomaly "Kernel and Library names do not match";
- Nametab.push (Nametab.Until 1) sp (ConstRef kn');
- csttab := Spmap.add sp kind !csttab
-
(* At load-time, the segment starting from the module name to the discharge *)
(* section (if Remark or Fact) is needed to access a construction *)
-let load_constant i ((sp,kn),(_,kind)) =
- (if Nametab.exists_cci sp then
- let (_,id) = repr_path sp in
- errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
- csttab := Spmap.add sp kind !csttab;
- Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn))
+let load_constant i ((sp,kn),(_,_,_,kind)) =
+ if Nametab.exists_cci sp then
+ errorlabstrm "cache_constant"
+ (pr_id (basename sp) ++ str " already exists");
+ Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn));
+ csttab := Spmap.add sp kind !csttab
(* Opening means making the name without its module qualification available *)
let open_constant i ((sp,kn),_) =
Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
+let cache_constant ((sp,kn),(cdt,dhyps,imps,kind) as o) =
+ let id = basename sp in
+ let _,dir,_ = repr_kn kn in
+ if Idmap.mem id !vartab then
+ errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+ if Nametab.exists_cci sp then
+ errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+ let kn' = Global.add_constant dir id cdt in
+ assert (kn' = constant_of_kn kn);
+ Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
+ add_section_constant kn' (Global.lookup_constant kn').const_hyps;
+ Dischargedhypsmap.set_discharged_hyps sp dhyps;
+ with_implicits imps declare_constant_implicits kn';
+ Notation.declare_ref_arguments_scope (ConstRef kn');
+ csttab := Spmap.add sp kind !csttab
+
+(*s Registration as global tables and rollback. *)
+
+open Cooking
+
+let discharged_hyps kn sechyps =
+ let (_,dir,_) = repr_kn kn in
+ let args = array_map_to_list destVar (instance_from_named_context sechyps) in
+ List.rev (List.map (Libnames.make_path dir) args)
+
+let discharge_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
+ let con = constant_of_kn kn in
+ let cb = Global.lookup_constant con in
+ let (repl1,_ as repl) = replacement_context () in
+ let sechyps = section_segment (ConstRef con) in
+ let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in
+ Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,imps,kind)
+
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp)
-let dummy_constant (ce,mk) = dummy_constant_entry,mk
+let dummy_constant (ce,_,imps,mk) = dummy_constant_entry,[],imps,mk
let export_constant cst = Some (dummy_constant cst)
@@ -176,6 +196,7 @@ let (in_constant, out_constant) =
open_function = open_constant;
classify_function = classify_constant;
subst_function = ident_subst_function;
+ discharge_function = discharge_constant;
export_function = export_constant }
let hcons_constant_declaration = function
@@ -188,12 +209,10 @@ let hcons_constant_declaration = function
const_entry_boxed = ce.const_entry_boxed }
| cd -> cd
-let declare_constant_common id discharged_hyps (cd,kind) =
- let (sp,kn as oname) = add_leaf id (in_constant (cd,kind)) in
+let declare_constant_common id dhyps (cd,kind) =
+ let imps = implicits_flags () in
+ let (sp,kn as oname) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in
let kn = constant_of_kn kn in
- declare_constant_implicits kn;
- Notation.declare_ref_arguments_scope (ConstRef kn);
- Dischargedhypsmap.set_discharged_hyps sp discharged_hyps;
kn
let declare_constant_gen internal id (cd,kind) =
@@ -205,13 +224,15 @@ let declare_constant_gen internal id (cd,kind) =
let declare_internal_constant = declare_constant_gen true
let declare_constant = declare_constant_gen false
-(* when coming from discharge *)
-let redeclare_constant id discharged_hyps (cd,kind) =
- let _ = declare_constant_common id discharged_hyps (GlobalRecipe cd,kind) in
- ()
-
(* Inductives. *)
+let declare_inductive_argument_scopes kn mie =
+ list_iter_i (fun i {mind_entry_consnames=lc} ->
+ Notation.declare_ref_arguments_scope (IndRef (kn,i));
+ for j=1 to List.length lc do
+ Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
+ done) mie.mind_entry_inds
+
let inductive_names sp kn mie =
let (dp,_) = repr_path sp in
let names, _ =
@@ -232,37 +253,43 @@ let inductive_names sp kn mie =
([], 0) mie.mind_entry_inds
in names
-
let check_exists_inductive (sp,_) =
(if Idmap.mem (basename sp) !vartab then
- errorlabstrm "cache_inductive"
+ errorlabstrm ""
(pr_id (basename sp) ++ str " already exists"));
if Nametab.exists_cci sp then
let (_,id) = repr_path sp in
- errorlabstrm "cache_inductive" (pr_id id ++ str " already exists")
-
-let cache_inductive ((sp,kn),mie) =
- let names = inductive_names sp kn mie in
- List.iter check_exists_inductive names;
- let _,dir,_ = repr_kn kn in
- let kn' = Global.add_mind dir (basename sp) mie in
- if kn' <> kn then
- anomaly "Kernel and Library names do not match";
-
- List.iter
- (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref)
- names
+ errorlabstrm "" (pr_id id ++ str " already exists")
-let load_inductive i ((sp,kn),mie) =
+let load_inductive i ((sp,kn),(_,_,mie)) =
let names = inductive_names sp kn mie in
List.iter check_exists_inductive names;
List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names
-let open_inductive i ((sp,kn),mie) =
+let open_inductive i ((sp,kn),(_,_,mie)) =
let names = inductive_names sp kn mie in
-(* List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names*)
List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
+let cache_inductive ((sp,kn),(dhyps,imps,mie)) =
+ let names = inductive_names sp kn mie in
+ List.iter check_exists_inductive names;
+ let id = basename sp in
+ let _,dir,_ = repr_kn kn in
+ let kn' = Global.add_mind dir id mie in
+ assert (kn'=kn);
+ add_section_kn kn (Global.lookup_mind kn').mind_hyps;
+ Dischargedhypsmap.set_discharged_hyps sp dhyps;
+ with_implicits imps declare_mib_implicits kn;
+ declare_inductive_argument_scopes kn mie;
+ List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
+
+let discharge_inductive ((sp,kn),(dhyps,imps,mie)) =
+ let mie = Global.lookup_mind kn in
+ let repl = replacement_context () in
+ let sechyps = section_segment (IndRef (kn,0)) in
+ Some (discharged_hyps kn sechyps,imps,
+ Discharge.process_inductive sechyps repl mie)
+
let dummy_one_inductive_entry mie = {
mind_entry_params = [];
mind_entry_typename = mie.mind_entry_typename;
@@ -272,10 +299,10 @@ let dummy_one_inductive_entry mie = {
}
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_inductive_entry m = {
+let dummy_inductive_entry (_,imps,m) = ([],imps,{
mind_entry_record = false;
mind_entry_finite = true;
- mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }
+ mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
let export_inductive x = Some (dummy_inductive_entry x)
@@ -286,38 +313,19 @@ let (in_inductive, out_inductive) =
open_function = open_inductive;
classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a));
subst_function = ident_subst_function;
+ discharge_function = discharge_inductive;
export_function = export_inductive }
-let declare_inductive_argument_scopes kn mie =
- list_iter_i (fun i {mind_entry_consnames=lc} ->
- Notation.declare_ref_arguments_scope (IndRef (kn,i));
- for j=1 to List.length lc do
- Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
- done) mie.mind_entry_inds
-
-let declare_inductive_common mie =
- let id = match mie.mind_entry_inds with
- | ind::_ -> ind.mind_entry_typename
- | [] -> anomaly "cannot declare an empty list of inductives"
- in
- let oname = add_leaf id (in_inductive mie) in
- declare_mib_implicits (snd oname);
- declare_inductive_argument_scopes (snd oname) mie;
- oname
-
(* for initial declaration *)
let declare_mind isrecord mie =
- let (sp,kn as oname) = declare_inductive_common mie in
- Dischargedhypsmap.set_discharged_hyps sp [] ;
+ let imps = implicits_flags () in
+ let id = match mie.mind_entry_inds with
+ | ind::_ -> ind.mind_entry_typename
+ | [] -> anomaly "cannot declare an empty list of inductives" in
+ let oname = add_leaf id (in_inductive ([],imps,mie)) in
!xml_declare_inductive (isrecord,oname);
oname
-(* when coming from discharge: no xml output *)
-let redeclare_inductive discharged_hyps mie =
- let oname = declare_inductive_common mie in
- Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps ;
- oname
-
(*s Test and access functions. *)
let is_constant sp =
@@ -332,12 +340,6 @@ let get_variable id =
| CheckedSectionLocalDef (c,ty,cst,opaq) -> (id,Some c,ty)
| CheckedSectionLocalAssum (ty,cst) -> (id,None,ty)
-let get_variable_with_constraints id =
- let (p,x,_) = Idmap.find id !vartab in
- match x with
- | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst)
- | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst)
-
let variable_strength _ = Local
let find_section_variable id =
@@ -380,12 +382,6 @@ let mind_oper_of_id sp id mib =
mip.mind_consnames)
mib.mind_packets
-let context_of_global_reference = function
- | VarRef id -> []
- | ConstRef sp -> (Global.lookup_constant sp).const_hyps
- | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps
- | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps
-
let last_section_hyps dir =
fold_named_context
(fun (id,_,_) sec_ids ->
diff --git a/library/declare.mli b/library/declare.mli
index 6af513888..c141985be 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -40,10 +40,6 @@ type variable_declaration = dir_path * section_variable_entry * local_kind
val declare_variable : variable -> variable_declaration -> object_name
-(* Declaration from Discharge *)
-val redeclare_variable :
- variable -> Dischargedhypsmap.discharged_hyps -> variable_declaration -> unit
-
(* Declaration of global constructions *)
(* i.e. Definition/Theorem/Axiom/Parameter/... *)
@@ -58,21 +54,11 @@ val declare_constant :
val declare_internal_constant :
identifier -> constant_declaration -> constant
-val redeclare_constant :
- identifier -> Dischargedhypsmap.discharged_hyps ->
- Cooking.recipe * global_kind -> 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) *)
val declare_mind : bool -> mutual_inductive_entry -> object_name
-(* Declaration from Discharge *)
-val redeclare_inductive :
- Dischargedhypsmap.discharged_hyps -> mutual_inductive_entry -> object_name
-
-val out_inductive : Libobject.obj -> mutual_inductive_entry
-
val strength_min : strength * strength -> strength
val string_of_strength : strength -> string
@@ -82,10 +68,7 @@ val is_constant : section_path -> bool
val constant_strength : section_path -> strength
val constant_kind : section_path -> global_kind
-val out_variable : Libobject.obj -> identifier * variable_declaration
val get_variable : variable -> named_declaration
-val get_variable_with_constraints :
- variable -> named_declaration * Univ.constraints
val variable_strength : variable -> strength
val variable_kind : variable -> local_kind
val find_section_variable : variable -> section_path
@@ -94,7 +77,6 @@ val clear_proofs : named_context -> named_context
(*s Global references *)
-val context_of_global_reference : global_reference -> section_context
val strength_of_global : global_reference -> strength
(* hooks for XML output *)
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 96ed944b2..0e7bdef30 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -24,13 +24,16 @@ type discharged_hyps = section_path list
let discharged_hyps_map = ref Spmap.empty
-let cache_discharged_hyps_map (_,(sp,hyps)) =
+let load_discharged_hyps_map _ (_,(sp,hyps)) =
discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
+let cache_discharged_hyps_map o =
+ load_discharged_hyps_map 1 o
+
let (in_discharged_hyps_map, _) =
declare_object { (default_object "DISCHARGED-HYPS-MAP") with
cache_function = cache_discharged_hyps_map;
- load_function = (fun _ -> cache_discharged_hyps_map);
+ load_function = load_discharged_hyps_map;
export_function = (fun x -> Some x) }
let set_discharged_hyps sp hyps =
diff --git a/library/impargs.ml b/library/impargs.ml
index 8daf939ef..f41d26c99 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -55,6 +55,14 @@ let is_contextual_implicit_args () = !contextual_implicit_args
type implicits_flags = (bool * bool * bool) * (bool * bool * bool)
+let implicits_flags () =
+ (!implicit_args,
+ !strict_implicit_args,
+ !contextual_implicit_args),
+ (!implicit_args_out,
+ !strict_implicit_args_out,
+ !contextual_implicit_args_out)
+
let with_implicits ((a,b,c),(d,e,g)) f x =
let oa = !implicit_args in
let ob = !strict_implicit_args in
@@ -342,6 +350,16 @@ let compute_var_implicits id =
let var_implicits id =
try Idmap.find id !var_table with Not_found -> No_impl,No_impl
+(* Implicits of a global reference. *)
+
+let compute_global_implicits = function
+ | VarRef id -> compute_var_implicits id
+ | ConstRef kn -> compute_constant_implicits kn
+ | IndRef (kn,i) ->
+ let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps
+ | ConstructRef ((kn,i),j) ->
+ let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1)
+
(* Caching implicits *)
let cache_implicits_decl (r,imps) =
@@ -355,7 +373,15 @@ let cache_implicits_decl (r,imps) =
| ConstructRef consp ->
constructors_table := Constrmap.add consp imps !constructors_table
-let cache_implicits (_,l) = List.iter cache_implicits_decl l
+let load_implicits _ (_,l) = List.iter cache_implicits_decl l
+
+let cache_implicits o =
+ load_implicits 1 o
+
+(*
+let discharge_implicits (_,(r,imps)) =
+ match r with VarRef _ -> None | _ -> Some (r,compute_global_implicits r)
+*)
let subst_implicits_decl subst (r,imps as o) =
let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
@@ -366,21 +392,11 @@ let subst_implicits (_,subst,l) =
let (in_implicits, _) =
declare_object {(default_object "IMPLICITS") with
cache_function = cache_implicits;
- load_function = (fun _ -> cache_implicits);
+ load_function = load_implicits;
subst_function = subst_implicits;
classify_function = (fun (_,x) -> Substitute x);
export_function = (fun x -> Some x) }
-(* Implicits of a global reference. *)
-
-let compute_global_implicits = function
- | VarRef id -> compute_var_implicits id
- | ConstRef kn -> compute_constant_implicits kn
- | IndRef (kn,i) ->
- let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps
- | ConstructRef ((kn,i),j) ->
- let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1)
-
let declare_implicits_gen r =
add_anonymous_leaf (in_implicits [r,compute_global_implicits r])
diff --git a/library/impargs.mli b/library/impargs.mli
index c1eba6923..212a93a0f 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -64,6 +64,8 @@ val is_implicit_var : variable -> implicits_flags
val implicits_of_global : global_reference -> implicits_list
+val implicits_flags : unit -> implicits_flags
+
(* For translator *)
val implicits_of_global_out : global_reference -> implicits_list
val is_implicit_args_out : unit -> bool
diff --git a/library/lib.ml b/library/lib.ml
index babb3863b..548b80d42 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -215,6 +215,7 @@ let is_something_opened = function
| (_,OpenedModtype _) -> true
| _ -> false
+(*
let export_segment seg =
let rec clean acc = function
| (_,CompilingLibrary _) :: _ | [] -> acc
@@ -229,7 +230,7 @@ let export_segment seg =
| (_,FrozenState _) :: stk -> clean acc stk
in
clean [] seg
-
+*)
let start_module export id mp nametab =
let dir = extend_dirpath (fst !path_prefix) id in
@@ -383,6 +384,70 @@ let is_module () =
(* Returns the most recent OpenedThing node *)
let what_is_opened () = find_entry_p is_something_opened
+(* Discharge tables *)
+
+let sectab =
+ ref ([] : (identifier list *
+ (identifier array Cmap.t * identifier array KNmap.t) *
+ (Sign.named_context Cmap.t * Sign.named_context KNmap.t)) list)
+
+let add_section () =
+ sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
+
+let add_section_variable id =
+ match !sectab with
+ | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
+ | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl
+
+let rec extract_hyps = function
+ | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
+ | (id::idl,hyps) -> extract_hyps (idl,hyps)
+ | [], _ -> []
+
+let add_section_replacement f g hyps =
+ match !sectab with
+ | [] -> ()
+ | (vars,exps,abs)::sl ->
+ let sechyps = extract_hyps (vars,hyps) in
+ let args = Sign.instance_from_named_context (List.rev sechyps) in
+ sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl
+
+let add_section_kn kn =
+ let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in
+ add_section_replacement f f
+
+let add_section_constant kn =
+ let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in
+ add_section_replacement f f
+
+let replacement_context () = pi2 (List.hd !sectab)
+
+let section_segment = function
+ | VarRef id ->
+ []
+ | ConstRef con ->
+ Cmap.find con (fst (pi3 (List.hd !sectab)))
+ | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+ KNmap.find kn (snd (pi3 (List.hd !sectab)))
+
+let section_instance r =
+ Sign.instance_from_named_context (List.rev (section_segment r))
+
+let init () = sectab := []
+let freeze () = !sectab
+let unfreeze s = sectab := s
+
+let _ =
+ Summary.declare_summary "section-context"
+ { Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init;
+ Summary.survive_module = false;
+ Summary.survive_section = false }
+
+(*************)
+(* Sections. *)
+
(* XML output hooks *)
let xml_open_section = ref (fun id -> ())
let xml_close_section = ref (fun id -> ())
@@ -390,8 +455,6 @@ let xml_close_section = ref (fun id -> ())
let set_xml_open_section f = xml_open_section := f
let set_xml_close_section f = xml_close_section := f
-(* Sections. *)
-
let open_section id =
let olddir,(mp,oldsec) = !path_prefix in
let dir = extend_dirpath olddir id in
@@ -405,11 +468,19 @@ let open_section id =
Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
path_prefix := prefix;
if !Options.xml_export then !xml_open_section id;
+ add_section ();
prefix
(* Restore lib_stk and summaries as before the section opening, and
add a ClosedSection object. *)
+
+let discharge_item = function
+ | ((sp,_ as oname),Leaf lobj) ->
+ option_app (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+ | _ ->
+ None
+
let close_section ~export id =
let oname,fs =
try match find_entry_p is_something_opened with
@@ -421,25 +492,31 @@ let close_section ~export id =
with Not_found ->
error "no opened section"
in
- let (after,_,before) = split_lib oname in
+ let (secdecls,_,before) = split_lib oname in
lib_stk := before;
- let prefix = !path_prefix in
+ let full_olddir = fst !path_prefix in
pop_path_prefix ();
+(*
let closed_sec =
- ClosedSection (export, (fst prefix), export_segment after)
- in
+ ClosedSection (export, full_olddir, export_segment secdecls) in
let name = make_path id, make_kn id in
add_entry name closed_sec;
+*)
if !Options.xml_export then !xml_close_section id;
- (prefix, after, fs)
+ let newdecls = List.map discharge_item secdecls in
+ Summary.section_unfreeze_summaries fs;
+ List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls;
+ Cooking.clear_cooking_sharing ();
+ Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
+(*****************)
(* Backtracking. *)
let recache_decl = function
| (sp, Leaf o) -> cache_object (sp,o)
+ | (_,OpenedSection _) -> add_section ()
| _ -> ()
-
let recache_context ctx =
List.iter recache_decl ctx
@@ -475,7 +552,7 @@ let is_mod_node = function
the same name *)
let reset_mod (loc,id) =
- let (ent,before) =
+ let (_,before) =
try
find_split_p (fun (sp,node) ->
let (_,spi) = repr_path (fst sp) in id = spi
@@ -583,3 +660,40 @@ let library_part ref =
else
(* Theorem/Lemma outside its outer section of definition *)
dir
+
+(************************)
+(* Discharging names *)
+
+let pop_kn kn =
+ let (mp,dir,l) = Names.repr_kn kn in
+ Names.make_kn mp (dirpath_prefix dir) l
+
+let pop_con con =
+ let (mp,dir,l) = Names.repr_con con in
+ Names.make_con mp (dirpath_prefix dir) l
+
+let con_defined_in_sec kn =
+ let _,dir,_ = repr_con kn in
+ dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+
+let defined_in_sec kn =
+ let _,dir,_ = repr_kn kn in
+ dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+
+let discharge_global = function
+ | ConstRef kn when con_defined_in_sec kn ->
+ ConstRef (pop_con kn)
+ | IndRef (kn,i) when defined_in_sec kn ->
+ IndRef (pop_kn kn,i)
+ | ConstructRef ((kn,i),j) when defined_in_sec kn ->
+ ConstructRef ((pop_kn kn,i),j)
+ | r -> r
+
+let discharge_kn kn =
+ if defined_in_sec kn then pop_kn kn else kn
+
+let discharge_con cst =
+ if con_defined_in_sec cst then pop_con cst else cst
+
+let discharge_inductive (kn,i) =
+ (discharge_kn kn,i)
diff --git a/library/lib.mli b/library/lib.mli
index 0433897ba..9a4a810ae 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -128,8 +128,7 @@ val library_part : global_reference -> dir_path
val open_section : identifier -> object_prefix
-val close_section : export:bool -> identifier ->
- object_prefix * library_segment * Summary.frozen
+val close_section : export:bool -> identifier -> unit
(*s Backtracking (undo). *)
@@ -157,3 +156,24 @@ val reset_initial : unit -> unit
(* XML output hooks *)
val set_xml_open_section : (identifier -> unit) -> unit
val set_xml_close_section : (identifier -> unit) -> unit
+
+
+(*s Section management for discharge *)
+
+val section_segment : global_reference -> Sign.named_context
+val section_instance : global_reference -> Term.constr array
+
+val add_section_variable : identifier -> unit
+val add_section_constant : constant -> Sign.named_context -> unit
+val add_section_kn : kernel_name -> Sign.named_context -> unit
+val replacement_context : unit ->
+ (identifier array Cmap.t * identifier array KNmap.t)
+
+(*s Discharge: decrease the section level if in the current section *)
+
+val discharge_kn : kernel_name -> kernel_name
+val discharge_con : constant -> constant
+val discharge_global : global_reference -> global_reference
+val discharge_inductive : inductive -> inductive
+
+
diff --git a/library/libobject.ml b/library/libobject.ml
index 25d5a329f..d84e0bc26 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -36,6 +36,7 @@ type 'a object_declaration = {
open_function : int -> object_name * 'a -> unit;
classify_function : object_name * 'a -> 'a substitutivity;
subst_function : object_name * substitution * 'a -> 'a;
+ discharge_function : object_name * 'a -> 'a option;
export_function : 'a -> 'a option }
let yell s = anomaly s
@@ -48,6 +49,7 @@ let default_object s = {
subst_function = (fun _ ->
yell ("The object "^s^" does not know how to substitute!"));
classify_function = (fun (_,obj) -> Keep obj);
+ discharge_function = (fun _ -> None);
export_function = (fun _ -> None)}
@@ -72,6 +74,7 @@ type dynamic_object_declaration = {
dyn_open_function : int -> object_name * obj -> unit;
dyn_subst_function : object_name * substitution * obj -> obj;
dyn_classify_function : object_name * obj -> obj substitutivity;
+ dyn_discharge_function : object_name * obj -> obj option;
dyn_export_function : obj -> obj option }
let object_tag lobj = Dyn.tag lobj
@@ -104,6 +107,11 @@ let declare_object odecl =
| Anticipate (obj) -> Anticipate (infun obj)
else
anomaly "somehow we got the wrong dynamic object in the classifyfun"
+ and discharge (oname,lobj) =
+ if Dyn.tag lobj = na then
+ option_app infun (odecl.discharge_function (oname,outfun lobj))
+ else
+ anomaly "somehow we got the wrong dynamic object in the dischargefun"
and exporter lobj =
if Dyn.tag lobj = na then
option_app infun (odecl.export_function (outfun lobj))
@@ -116,6 +124,7 @@ let declare_object odecl =
dyn_open_function = opener;
dyn_subst_function = substituter;
dyn_classify_function = classifier;
+ dyn_discharge_function = discharge;
dyn_export_function = exporter };
(infun,outfun)
@@ -154,5 +163,8 @@ let subst_object ((_,_,lobj) as node) =
let classify_object ((_,lobj) as node) =
apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj
+let discharge_object ((_,lobj) as node) =
+ apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
+
let export_object lobj =
apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index 37447ffbe..3d60e48ad 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -70,6 +70,7 @@ type 'a object_declaration = {
open_function : int -> object_name * 'a -> unit;
classify_function : object_name * 'a -> 'a substitutivity;
subst_function : object_name * substitution * 'a -> 'a;
+ discharge_function : object_name * 'a -> 'a option;
export_function : 'a -> 'a option }
(* The default object is a "Keep" object with empty methods.
@@ -103,4 +104,5 @@ val open_object : int -> object_name * obj -> unit
val subst_object : object_name * substitution * obj -> obj
val classify_object : object_name * obj -> obj substitutivity
val export_object : obj -> obj option
+val discharge_object : object_name * obj -> obj option
val relax : bool -> unit
diff --git a/library/library.ml b/library/library.ml
index fee383233..09169c4ae 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -554,11 +554,14 @@ let load_require _ (_,(modl,_)) =
OS dependent fields from .vo files for cross-platform compatibility *)
let export_require (l,e) = Some (l,e)
+let discharge_require (_,o) = Some o
+
let (in_require, out_require) =
declare_object {(default_object "REQUIRE") with
cache_function = cache_require;
load_function = load_require;
export_function = export_require;
+ discharge_function = discharge_require;
classify_function = (fun (_,o) -> Anticipate o) }
(* Require libraries, import them if [export <> None], mark them for export
diff --git a/library/library.mli b/library/library.mli
index 4ecc76809..bfcc04eb9 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -76,9 +76,3 @@ val locate_qualified_library :
(*s Statistics: display the memory use of a library. *)
val mem : dir_path -> Pp.std_ppcmds
-
-(*s For discharge *)
-type library_reference
-
-val out_require : Libobject.obj -> library_reference
-val reload_library : library_reference -> unit
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 66ed81d02..6d49baf52 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -36,14 +36,14 @@ type cl_typ =
| CL_IND of inductive
type cl_info_typ = {
- cl_strength : strength;
cl_param : int
}
type coe_typ = global_reference
type coe_info_typ = {
- coe_value : unsafe_judgment;
+ coe_value : constr;
+ coe_type : types;
coe_strength : strength;
coe_is_identity : bool;
coe_param : int }
@@ -92,11 +92,7 @@ let unfreeze (fcl,fco,fig) =
(* ajout de nouveaux "objets" *)
let add_new_class cl s =
- try
- let n,s' = Bijint.revmap cl !class_tab in
- if s.cl_strength = Global & s'.cl_strength <> Global then
- class_tab := Bijint.replace n cl s !class_tab
- with Not_found ->
+ if not (Bijint.mem cl !class_tab) then
class_tab := Bijint.add cl s !class_tab
let add_new_coercion coe s =
@@ -107,11 +103,19 @@ let add_new_path x y =
let init () =
class_tab:= Bijint.empty;
- add_new_class CL_FUN { cl_param = 0; cl_strength = Global };
- add_new_class CL_SORT { cl_param = 0; cl_strength = Global };
+ add_new_class CL_FUN { cl_param = 0 };
+ add_new_class CL_SORT { cl_param = 0 };
coercion_tab:= Gmap.empty;
inheritance_graph:= Gmap.empty
+let _ =
+ Summary.declare_summary "inh_graph"
+ { Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init;
+ Summary.survive_module = false;
+ Summary.survive_section = false }
+
let _ = init()
(* class_info : cl_typ -> int * cl_info_typ *)
@@ -147,7 +151,7 @@ let lookup_pattern_path_between (s,t) =
(fun coe ->
let c, _ =
Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty
- coe.coe_value.uj_val
+ coe.coe_value
in
match kind_of_term c with
| Construct sp -> (sp, coe.coe_param)
@@ -183,44 +187,6 @@ let subst_cl_typ subst ct = match ct with
to declare any term as a coercion *)
let subst_coe_typ subst t = fst (subst_global subst t)
-let subst_coe_info subst info =
- let jud = info.coe_value in
- let val' = subst_mps subst (j_val jud) in
- let type' = subst_mps subst (j_type jud) in
- if val' == j_val jud && type' == j_type jud then info else
- {info with coe_value = make_judge val' type'}
-
-(* library, summary *)
-
-(*val inClass : (cl_typ * cl_info_typ) -> Libobject.object = <fun>
- val outClass : Libobject.object -> (cl_typ * cl_info_typ) = <fun> *)
-
-let cache_class (_,(x,y)) = add_new_class x y
-
-let subst_class (_,subst,(ct,ci as obj)) =
- let ct' = subst_cl_typ subst ct in
- if ct' == ct then obj else
- (ct',ci)
-
-let (inClass,outClass) =
- declare_object {(default_object "CLASS") with
- load_function = (fun _ o -> cache_class o);
- cache_function = cache_class;
- subst_function = subst_class;
- classify_function = (fun (_,x) -> Substitute x);
- export_function = (function x -> Some x) }
-
-let declare_class (cl,stre,p) =
- Lib.add_anonymous_leaf (inClass ((cl,{ cl_strength = stre; cl_param = p })))
-
-let _ =
- Summary.declare_summary "inh_graph"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init;
- Summary.survive_module = false;
- Summary.survive_section = false }
-
(* classe d'un terme *)
(* class_of : Term.constr -> int *)
@@ -257,7 +223,8 @@ let pr_class x = str (string_of_class x)
(* coercion_value : coe_index -> unsafe_judgment * bool *)
-let coercion_value { coe_value = j; coe_is_identity = b } = (j,b)
+let coercion_value { coe_value = c; coe_type = t; coe_is_identity = b } =
+ (make_judge c t, b)
(* pretty-print functions are now in Pretty *)
(* rajouter une coercion dans le graphe *)
@@ -322,49 +289,81 @@ let add_coercion_in_graph (ic,source,target) =
if (!ambig_paths <> []) && is_verbose () then
ppnl (message_ambig !ambig_paths)
-type coercion = coe_typ * coe_info_typ * cl_typ * cl_typ
+type coercion = coe_typ * strength * bool * cl_typ * cl_typ * int
-let cache_coercion (_,(coe,xf,cls,clt)) =
+(* Calcul de l'arité d'une classe *)
+
+let reference_arity_length ref =
+ let t = Global.type_of_global ref in
+ List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty t))
+
+let class_params = function
+ | CL_FUN | CL_SORT -> 0
+ | CL_CONST sp -> reference_arity_length (ConstRef sp)
+ | CL_SECVAR sp -> reference_arity_length (VarRef sp)
+ | CL_IND sp -> reference_arity_length (IndRef sp)
+
+(* add_class : cl_typ -> strength option -> bool -> unit *)
+
+let add_class cl =
+ add_new_class cl { cl_param = class_params cl }
+
+let load_coercion i (_,(coe,stre,isid,cls,clt,ps)) =
+ add_class cls;
+ add_class clt;
let is,_ = class_info cls in
let it,_ = class_info clt in
+ let xf =
+ { coe_value = constr_of_global coe;
+ coe_type = Global.type_of_global coe;
+ coe_strength = stre;
+ coe_is_identity = isid;
+ coe_param = ps } in
add_new_coercion coe xf;
add_coercion_in_graph (xf,is,it)
-let subst_coercion (_,subst,(coe,xf,cls,clt as obj)) =
+let cache_coercion o =
+ load_coercion 1 o
+
+let subst_coercion (_,subst,(coe,stre,isid,cls,clt,ps as obj)) =
let coe' = subst_coe_typ subst coe in
- let xf' = subst_coe_info subst xf in
let cls' = subst_cl_typ subst cls in
let clt' = subst_cl_typ subst clt in
- if coe' == coe && xf' == xf && cls' == cls & clt' == clt then obj else
- (coe',xf',cls',clt')
-
-
-(* val inCoercion : coercion -> Libobject.object
- val outCoercion : Libobject.object -> coercion *)
+ if coe' == coe && cls' == cls & clt' == clt then obj else
+ (coe',stre,isid,cls',clt',ps)
+
+let discharge_cl = function
+ | CL_CONST kn -> CL_CONST (Lib.discharge_con kn)
+ | CL_IND ind -> CL_IND (Lib.discharge_inductive ind)
+ | cl -> cl
+
+let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) =
+ if stre = Local then None else
+ let n = try Array.length (Lib.section_instance coe) with Not_found -> 0 in
+ Some (Lib.discharge_global coe,
+ stre,
+ isid,
+ discharge_cl cls,
+ discharge_cl clt,
+ n + ps)
let (inCoercion,outCoercion) =
declare_object {(default_object "COERCION") with
- load_function = (fun _ o -> cache_coercion o);
- cache_function = cache_coercion;
- subst_function = subst_coercion;
- classify_function = (fun (_,x) -> Substitute x);
- export_function = (function x -> Some x) }
-
-let declare_coercion coef v stre ~isid ~src:cls ~target:clt ~params:ps =
- Lib.add_anonymous_leaf
- (inCoercion
- (coef,
- { coe_value = v;
- coe_strength = stre;
- coe_is_identity = isid;
- coe_param = ps },
- cls, clt))
+ load_function = load_coercion;
+ cache_function = cache_coercion;
+ subst_function = subst_coercion;
+ classify_function = (fun (_,x) -> Substitute x);
+ discharge_function = discharge_coercion;
+ export_function = (function x -> Some x) }
+
+let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps =
+ Lib.add_anonymous_leaf (inCoercion (coef,stre,isid,cls,clt,ps))
let coercion_strength v = v.coe_strength
let coercion_identity v = v.coe_is_identity
(* For printing purpose *)
-let get_coercion_value v = v.coe_value.uj_val
+let get_coercion_value v = v.coe_value
let classes () = Bijint.dom !class_tab
let coercions () = Gmap.rng !coercion_tab
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index c1590f6a8..dd51ee970 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -30,7 +30,6 @@ val subst_cl_typ : substitution -> cl_typ -> cl_typ
(* This is the type of infos for declared classes *)
type cl_info_typ = {
- cl_strength : strength;
cl_param : int }
(* This is the type of coercion kinds *)
@@ -48,9 +47,6 @@ type coe_index
(* This is the type of paths from a class to another *)
type inheritance_path = coe_index list
-(*s [declare_class] adds a class to the set of declared classes *)
-val declare_class : cl_typ * strength * int -> unit
-
(*s Access to classes infos *)
val class_info : cl_typ -> (cl_index * cl_info_typ)
val class_exists : cl_typ -> bool
@@ -70,7 +66,7 @@ val class_args_of : constr -> constr list
(*s [declare_coercion] adds a coercion in the graph of coercion paths *)
val declare_coercion :
- coe_typ -> unsafe_judgment -> strength -> isid:bool ->
+ coe_typ -> strength -> isid:bool ->
src:cl_typ -> target:cl_typ -> params:int -> unit
(*s Access to coercions infos *)
@@ -85,19 +81,6 @@ val lookup_path_to_sort_from : cl_index -> inheritance_path
val lookup_pattern_path_between :
cl_index * cl_index -> (constructor * int) list
-(*i Pour le discharge *)
-type coercion = coe_typ * coe_info_typ * cl_typ * cl_typ
-
-open Libobject
-val inClass : (cl_typ * cl_info_typ) -> Libobject.obj
-val outClass : Libobject.obj -> (cl_typ * cl_info_typ)
-val inCoercion : coercion -> Libobject.obj
-val outCoercion : Libobject.obj -> coercion
-val coercion_strength : coe_info_typ -> strength
-val coercion_identity : coe_info_typ -> bool
-val coercion_params : coe_info_typ -> int
-(*i*)
-
(*i Crade *)
open Pp
val install_path_printer :
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index cfccdb5e6..7f557d9b3 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -21,17 +21,19 @@ open Library
open Classops
open Mod_subst
-(*s Une structure S est un type inductif non récursif à un seul
- constructeur (de nom par défaut Build_S) *)
+(*s A structure S is a non recursive inductive type with a single
+ constructor (the name of which defaults to Build_S) *)
(* Table des structures: le nom de la structure (un [inductive]) donne
le nom du constructeur, le nombre de paramètres et pour chaque
- argument réels du constructeur, le noms de la projection
- correspondante, si valide *)
+ argument réel du constructeur, le nom de la projection
+ correspondante, si valide, et un booléen disant si c'est une vraie
+ projection ou bien une fonction constante (associée à un LetIn) *)
type struc_typ = {
s_CONST : identifier;
s_PARAM : int;
+ s_PROJKIND : bool list;
s_PROJ : constant option list }
let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
@@ -39,121 +41,177 @@ let projection_table = ref Cmap.empty
let option_fold_right f p e = match p with Some a -> f a e | None -> e
-let cache_structure (_,(ind,struc)) =
+let load_structure i (_,(ind,id,kl,projs)) =
+ let n = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
+ let struc =
+ { s_CONST = id; s_PARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
structure_table := Indmap.add ind struc !structure_table;
projection_table :=
List.fold_right (option_fold_right (fun proj -> Cmap.add proj struc))
- struc.s_PROJ !projection_table
+ projs !projection_table
-let subst_structure (_,subst,((kn,i),struc as obj)) =
+let cache_structure o =
+ load_structure 1 o
+
+let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
let kn' = subst_kn subst kn in
- let proj' =
+ let projs' =
(* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
(* the first component of subst_con. *)
list_smartmap
- (option_smartmap (fun kn -> fst (subst_con subst kn)))
- struc.s_PROJ
+ (option_smartmap (fun kn -> fst (subst_con subst kn)))
+ projs
in
- if proj' == struc.s_PROJ && kn' == kn then obj else
- (kn',i),{struc with s_PROJ = proj'}
+ if projs' == projs && kn' == kn then obj else
+ ((kn',i),id,kl,projs')
+
+let discharge_structure (_,(ind,id,kl,projs)) =
+ Some (Lib.discharge_inductive ind, id, kl,
+ List.map (option_app Lib.discharge_con) projs)
let (inStruc,outStruc) =
declare_object {(default_object "STRUCTURE") with
- cache_function = cache_structure;
- load_function = (fun _ o -> cache_structure o);
- subst_function = subst_structure;
- classify_function = (fun (_,x) -> Substitute x);
- export_function = (function x -> Some x) }
+ cache_function = cache_structure;
+ load_function = load_structure;
+ subst_function = subst_structure;
+ classify_function = (fun (_,x) -> Substitute x);
+ discharge_function = discharge_structure;
+ export_function = (function x -> Some x) }
-let add_new_struc (s,c,n,l) =
- Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
+let declare_structure (s,c,_,kl,pl) =
+ Lib.add_anonymous_leaf (inStruc (s,c,kl,pl))
-let find_structure indsp = Indmap.find indsp !structure_table
+let lookup_structure indsp = Indmap.find indsp !structure_table
let find_projection_nparams = function
| ConstRef cst -> (Cmap.find cst !projection_table).s_PARAM
| _ -> raise Not_found
-(*s Un "object" est une fonction construisant une instance d'une structure *)
+
+(************************************************************************)
+(*s A canonical structure declares "canonical" conversion hints between *)
+(* the effective components of a structure and the projections of the *)
+(* structure *)
(* Table des definitions "object" : pour chaque object c,
c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n)
- avec ti = (ci ui1...uir)
+ If ti has the form (ci ui1...uir) where ci is a global reference and
+if the corresponding projection Li of the structure R is defined, one
+declare a "conversion" between ci and Li
+
+ x1:B1..xk:Bk |- (Li a1..am (c x1..xk)) =_conv (ci ui1...uir)
- Pour tout ci, et Li, la ième projection de la structure R (si
- définie), on déclare une "coercion"
+that maps the pair (Li,ci) to the following data
o_DEF = c
o_TABS = B1...Bk
o_PARAMS = a1...am
o_TCOMP = ui1...uir
+
*)
type obj_typ = {
o_DEF : constr;
- o_TABS : constr list; (* dans l'ordre *)
- o_TPARAMS : constr list; (* dans l'ordre *)
- o_TCOMPS : constr list } (* dans l'ordre *)
-
-let subst_obj subst obj =
- let o_DEF' = subst_mps subst obj.o_DEF in
- let o_TABS' = list_smartmap (subst_mps subst) obj.o_TABS in
- let o_TPARAMS' = list_smartmap (subst_mps subst) obj.o_TPARAMS in
- let o_TCOMPS' = list_smartmap (subst_mps subst) obj.o_TCOMPS in
- if o_DEF' == obj.o_DEF
- && o_TABS' == obj.o_TABS
- && o_TPARAMS' == obj.o_TPARAMS
- && o_TCOMPS' == obj.o_TCOMPS
- then
- obj
- else
- { o_DEF = o_DEF' ;
- o_TABS = o_TABS' ;
- o_TPARAMS = o_TPARAMS' ;
- o_TCOMPS = o_TCOMPS' }
+ o_TABS : constr list; (* ordered *)
+ o_TPARAMS : constr list; (* ordered *)
+ o_TCOMPS : constr list } (* ordered *)
let object_table =
(ref [] : ((global_reference * global_reference) * obj_typ) list ref)
-let canonical_structures () = !object_table
-
-let cache_canonical_structure (_,(cst,lo)) =
- List.iter (fun (o,_ as x) ->
- if not (List.mem_assoc o !object_table) then
- object_table := x :: (!object_table)) lo
-
-let subst_object subst ((r1,r2),o as obj) =
- (* invariant: r1 and r2 are evaluable references. Thus subst_global *)
- (* cannot instantiate them. Hence we can use just the first component *)
- (* of the answer. *)
- let r1',_ = subst_global subst r1 in
- let r2',_ = subst_global subst r2 in
- let o' = subst_obj subst o in
- if r1' == r1 && r2' == r2 && o' == o then obj
- else (r1',r2'),o'
-
-let subst_canonical_structure (_,subst,(cst,lo as obj)) =
+let canonical_projections () = !object_table
+
+let keep_true_projections projs kinds =
+ map_succeed (function (p,true) -> p | _ -> failwith "")
+ (List.combine projs kinds)
+
+(* Intended to always success *)
+let compute_canonical_projections (con,ind) =
+ let v = mkConst con in
+ let c = Environ.constant_value (Global.env()) con in
+ let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in
+ let lt = List.rev (List.map snd lt) in
+ let args = snd (decompose_app t) in
+ let { s_PARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in
+ let params, projs = list_chop p args in
+ let lpj = keep_true_projections lpj kl in
+ let lps = List.combine lpj projs in
+ let comp =
+ List.fold_left
+ (fun l (spopt,t) -> (* comp=components *)
+ match spopt with
+ | Some proji_sp ->
+ let c, args = decompose_app t in
+ (try (ConstRef proji_sp, reference_of_constr c, args) :: l
+ with Not_found -> l)
+ | _ -> l)
+ [] lps in
+ List.map (fun (refi,c,argj) ->
+ (refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj})
+ comp
+
+let open_canonical_structure i (_,o) =
+ if i=1 then
+ let lo = compute_canonical_projections o in
+ List.iter (fun (o,_ as x) ->
+ if not (List.mem_assoc o !object_table) then
+ object_table := x :: (!object_table)) lo
+
+let cache_canonical_structure o =
+ open_canonical_structure 1 o
+
+let subst_canonical_structure (_,subst,(cst,ind as obj)) =
(* invariant: cst is an evaluable reference. Thus we can take *)
(* the first component of subst_con. *)
let cst' = fst (subst_con subst cst) in
- let lo' = list_smartmap (subst_object subst) lo in
- if cst' == cst & lo' == lo then obj else (cst',lo')
+ let ind' = Inductiveops.subst_inductive subst ind in
+ if cst' == cst & ind' == ind then obj else (cst',ind')
+
+let discharge_canonical_structure (_,(cst,ind)) =
+ Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
let (inCanonStruc,outCanonStruct) =
declare_object {(default_object "CANONICAL-STRUCTURE") with
- open_function = (fun i o -> if i=1 then cache_canonical_structure o);
+ open_function = open_canonical_structure;
cache_function = cache_canonical_structure;
subst_function = subst_canonical_structure;
classify_function = (fun (_,x) -> Substitute x);
+ discharge_function = discharge_canonical_structure;
export_function = (function x -> Some x) }
let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
+(*s High-level declaration of a canonical structure *)
+
+let error_not_structure ref =
+ errorlabstrm "object_declare"
+ (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object")
+
+let check_and_decompose_canonical_structure ref =
+ let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
+ let env = Global.env () in
+ let vc = match Environ.constant_opt_value env sp with
+ | Some vc -> vc
+ | None -> error_not_structure ref in
+ let f,args = match kind_of_term (snd (decompose_lam vc)) with
+ | App (f,args) -> f,args
+ | _ -> error_not_structure ref in
+ let indsp = match kind_of_term f with
+ | Construct (indsp,1) -> indsp
+ | _ -> error_not_structure ref in
+ let s = try lookup_structure indsp with Not_found -> error_not_structure ref in
+ if s.s_PARAM + List.length s.s_PROJ > Array.length args then
+ error_not_structure ref;
+ (sp,indsp)
+
+let declare_canonical_structure ref =
+ add_canonical_structure (check_and_decompose_canonical_structure ref)
+
let outCanonicalStructure x = fst (outCanonStruct x)
-let canonical_structure_info o = List.assoc o !object_table
+let lookup_canonical_conversion o = List.assoc o !object_table
let freeze () =
!structure_table, !projection_table, !object_table
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 7402f74c9..d6f90e11e 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -18,36 +18,36 @@ open Libobject
open Library
(*i*)
+(*s A structure S is a non recursive inductive type with a single
+ constructor (the name of which defaults to Build_S) *)
+
type struc_typ = {
s_CONST : identifier;
s_PARAM : int;
+ s_PROJKIND : bool list;
s_PROJ : constant option list }
-val add_new_struc :
- inductive * identifier * int * constant option list -> unit
+val declare_structure :
+ inductive * identifier * int * bool list * constant option list -> unit
-(* [find_structure isp] returns the infos associated to inductive path
+(* [lookup_structure isp] returns the infos associated to inductive path
[isp] if it corresponds to a structure, otherwise fails with [Not_found] *)
-val find_structure : inductive -> struc_typ
+val lookup_structure : inductive -> struc_typ
(* raise [Not_found] if not a projection *)
val find_projection_nparams : global_reference -> int
+(*s A canonical structure declares "canonical" conversion hints between *)
+(* the effective components of a structure and the projections of the *)
+(* structure *)
+
type obj_typ = {
o_DEF : constr;
- o_TABS : constr list; (* dans l'ordre *)
- o_TPARAMS : constr list; (* dans l'ordre *)
- o_TCOMPS : constr list } (* dans l'ordre *)
+ o_TABS : constr list; (* ordered *)
+ o_TPARAMS : constr list; (* ordered *)
+ o_TCOMPS : constr list } (* ordered *)
-val canonical_structure_info :
- (global_reference * global_reference) -> obj_typ
-val add_canonical_structure :
- constant * ((global_reference * global_reference) * obj_typ) list -> unit
-
-val inStruc : inductive * struc_typ -> obj
-val outStruc : obj -> inductive * struc_typ
-
-val outCanonicalStructure : obj -> constant
-
-val canonical_structures : unit ->
+val lookup_canonical_conversion : (global_reference * global_reference) -> obj_typ
+val declare_canonical_structure : global_reference -> unit
+val canonical_projections : unit ->
((global_reference * global_reference) * obj_typ) list
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 9d288c81e..88983637a 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -92,42 +92,16 @@ let explain_coercion_error g = function
(* Verifications pour l'ajout d'une classe *)
-let rec arity_sort (ctx,a) = match kind_of_term a with
- | Sort (Prop _ | Type _) -> List.length ctx
- | _ -> raise Not_found
-
let check_reference_arity ref =
- let t = Global.type_of_global ref in
- try arity_sort (Reductionops.splay_prod (Global.env()) Evd.empty t)
- with Not_found -> raise (CoercionError (NotAClass ref))
+ if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global ref)) then
+ raise (CoercionError (NotAClass ref))
let check_arity = function
- | CL_FUN | CL_SORT -> 0
+ | CL_FUN | CL_SORT -> ()
| CL_CONST sp -> check_reference_arity (ConstRef sp)
| CL_SECVAR sp -> check_reference_arity (VarRef sp)
| CL_IND sp -> check_reference_arity (IndRef sp)
-(* try_add_class : cl_typ -> strength option -> bool -> unit *)
-
-let strength_of_cl = function
- | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
- | CL_SECVAR sp -> variable_strength sp
- | _ -> Global
-
-let try_add_class cl streopt fail_if_exists =
- if not (class_exists cl) then
- let p = check_arity cl in
- let stre' = strength_of_cl cl in
- let stre = match streopt with
- | Some stre -> strength_min (stre,stre')
- | None -> stre'
- in
- declare_class (cl,stre,p)
- else
- if fail_if_exists then errorlabstrm "try_add_new_class"
- (pr_class cl ++ str " is already a class")
-
-
(* Coercions *)
(* check that the computed target is the provided one *)
@@ -154,12 +128,12 @@ let id_of_cl = function
mip.mind_typename
| CL_SECVAR id -> id
-let class_of_ref = function
+let class_of_global = function
| ConstRef sp -> CL_CONST sp
| IndRef sp -> CL_IND sp
| VarRef id -> CL_SECVAR id
| ConstructRef _ as c ->
- errorlabstrm "class_of_ref"
+ errorlabstrm "class_of_global"
(str "Constructors, such as " ++ Printer.pr_global c ++
str " cannot be used as class")
@@ -209,9 +183,14 @@ let prods_of t =
in
aux [] t
+let strength_of_cl = function
+ | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
+ | CL_SECVAR sp -> variable_strength sp
+ | _ -> Global
+
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 stres = strength_of_cl cls in
+ let stret = strength_of_cl clt 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
@@ -290,10 +269,10 @@ lorque source est None alors target est None aussi.
let add_new_coercion_core coef stre source target isid =
check_source source;
let env = Global.env () in
- let v = constr_of_reference coef in
- let vj = Retyping.get_judgment_of env Evd.empty v in
+ let v = constr_of_global coef in
+ let t = Global.type_of_global coef in
if coercion_exists coef then raise (CoercionError AlreadyExists);
- let tg,lp = prods_of (vj.uj_type) in
+ let tg,lp = prods_of t in
let llp = List.length lp in
if llp = 0 then raise (CoercionError NotAFunction);
let (cls,lvs,ind) =
@@ -312,10 +291,10 @@ let add_new_coercion_core coef stre source target isid =
raise (CoercionError NoTarget)
in
check_target clt target;
- try_add_class cls None false;
- try_add_class clt None false;
+ check_arity cls;
+ check_arity clt;
let stre' = get_strength stre coef cls clt in
- declare_coercion coef vj stre' isid cls clt (List.length lvs)
+ declare_coercion coef stre' isid cls clt (List.length lvs)
let try_add_new_coercion_core ref b c d e =
try add_new_coercion_core ref b c d e
@@ -346,118 +325,5 @@ let add_coercion_hook stre ref =
^ " is now a coercion")
let add_subclass_hook stre ref =
- let cl = class_of_ref ref in
+ let cl = class_of_global ref in
try_add_new_coercion_subclass cl stre
-
-(* try_add_new_class : global_reference -> strength -> unit *)
-
-let class_of_global = function
- | VarRef sp -> CL_SECVAR sp
- | ConstRef sp -> CL_CONST sp
- | IndRef sp -> CL_IND sp
- | ConstructRef _ as ref -> raise (CoercionError (NotAClass ref))
-
-let try_add_new_class ref stre =
- try try_add_class (class_of_global ref) (Some stre) true
- with CoercionError e ->
- errorlabstrm "try_add_new_class" (explain_coercion_error ref e)
-
-(* fonctions pour le discharge: encore un peu sale mais ça s'améliore *)
-
-type coercion_entry =
- global_reference * strength * bool * cl_typ * cl_typ * int
-
-let add_new_coercion (ref,stre,isid,cls,clt,n) =
- (* Un peu lourd, tout cela pour trouver l'instance *)
- let env = Global.env () in
- let v = constr_of_reference ref in
- let vj = Retyping.get_judgment_of env Evd.empty v in
- declare_coercion ref vj stre isid cls clt n
-
-let count_extra_abstractions hyps ids_to_discard =
- let _,n =
- List.fold_left
- (fun (hyps,n as sofar) id ->
- match hyps with
- | (hyp,None,_)::rest when id = hyp ->(rest, n+1)
- | _ -> sofar)
- (hyps,0) ids_to_discard
- in n
-
-let defined_in_sec kn olddir =
- let _,dir,_ = repr_kn kn in
- dir = olddir
-
-let con_defined_in_sec kn olddir =
- let _,dir,_ = repr_con kn in
- dir = olddir
-
-(* This moves the global path one step below *)
-let process_global olddir = function
- | VarRef _ ->
- anomaly "process_global only processes global surviving the section"
- | ConstRef kn as x ->
- if con_defined_in_sec kn olddir then
- let newkn = Lib.make_con (id_of_label (con_label kn)) in
- ConstRef newkn
- else x
- | IndRef (kn,i) as x ->
- if defined_in_sec kn olddir then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
- IndRef (newkn,i)
- else x
- | ConstructRef ((kn,i),j) as x ->
- if defined_in_sec kn olddir then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
- ConstructRef ((newkn,i),j)
- else x
-
-let process_class olddir ids_to_discard x =
- let (cl,{cl_strength=stre; cl_param=p}) = x in
-(* let env = Global.env () in*)
- match cl with
- | CL_SECVAR _ -> x
- | CL_CONST kn ->
- if con_defined_in_sec kn olddir then
- let newkn = Lib.make_con (id_of_label (con_label kn)) in
- let hyps = (Global.lookup_constant kn).const_hyps in
- let n = count_extra_abstractions hyps ids_to_discard in
- (CL_CONST newkn,{cl_strength=stre;cl_param=p+n})
- else
- x
- | CL_IND (kn,i) ->
- if defined_in_sec kn olddir then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
- let hyps = (Global.lookup_mind kn).mind_hyps in
- let n = count_extra_abstractions hyps ids_to_discard in
- (CL_IND (newkn,i),{cl_strength=stre;cl_param=p+n})
- else
- x
- | _ -> anomaly "process_class"
-
-let process_cl sec_sp cl =
- match cl with
- | CL_SECVAR id -> cl
- | CL_CONST kn ->
- if con_defined_in_sec kn sec_sp then
- let newkn = Lib.make_con (id_of_label (con_label kn)) in
- CL_CONST newkn
- else
- cl
- | CL_IND (kn,i) ->
- if defined_in_sec kn sec_sp then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
- CL_IND (newkn,i)
- else
- cl
- | _ -> cl
-
-let process_coercion olddir ids_to_discard (coe,coeinfo,cls,clt) =
- let hyps = context_of_global_reference coe in
- let nargs = count_extra_abstractions hyps ids_to_discard in
- (process_global olddir coe,
- coercion_strength coeinfo,
- coercion_identity coeinfo,
- process_cl olddir cls,
- process_cl olddir clt,
- nargs + coercion_params coeinfo)
diff --git a/toplevel/class.mli b/toplevel/class.mli
index bf3425102..34af2e326 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -50,19 +50,4 @@ val add_coercion_hook : Tacexpr.declaration_hook
val add_subclass_hook : Tacexpr.declaration_hook
-(* [try_add_new_class ref] declares [ref] as a new class; usually,
- this is done implicitely by [try_add_new_coercion]'s functions *)
-val try_add_new_class : global_reference -> strength -> unit
-
-(*s This is used for the discharge *)
-type coercion_entry
-
-val add_new_coercion : coercion_entry -> unit
-
-val process_class :
- dir_path -> identifier list ->
- (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ)
-val process_coercion :
- dir_path -> identifier list -> coercion -> coercion_entry
-
-val class_of_ref : global_reference -> cl_typ
+val class_of_global : global_reference -> cl_typ
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index adca0d47d..8c71c0513 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -8,326 +8,75 @@
(* $Id$ *)
-open Pp
-open Util
open Names
-open Nameops
+open Util
open Sign
open Term
-open Declarations
open Entries
-open Inductive
-open Reduction
+open Declarations
open Cooking
-open Typeops
-open Libnames
-open Libobject
-open Lib
-open Nametab
-open Declare
-open Impargs
-open Classops
-open Class
-open Recordops
-open Library
-open Indtypes
-open Nametab
-open Decl_kinds
-let recalc_sp dir sp =
- let (_,spid) = repr_path sp in Libnames.make_path dir spid
+(********************************)
+(* Discharging mutual inductive *)
-let recalc_kn dir kn =
- let (mp,_,l) = Names.repr_kn kn in
- Names.make_kn mp dir l
+let detype_param = function
+ | (Name id,None,p) -> id, Entries.LocalAssum p
+ | (Name id,Some p,_) -> id, Entries.LocalDef p
+ | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable"
-let recalc_con dir con =
- let (mp,_,l) = Names.repr_con con in
- Names.make_con mp dir l
+(* Replace
-let rec find_var id = function
- | [] -> false
- | (x,b,_)::l -> if x = id then b=None else find_var id l
+ Var(y1)..Var(yq):C1..Cq |- Ij:Bj
+ Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti
-let build_abstract_list sec_sp hyps ids_to_discard =
- let l1,l2 =
- List.split
- (List.fold_left
- (fun vars id ->
- if find_var id hyps then (mkVar id, Libnames.make_path sec_sp id)::vars
- else vars)
- [] ids_to_discard) in
- Array.of_list l1, l2
+ by
-(* Discharge of inductives is done here (while discharge of constants
- is done by the kernel for efficiency). *)
+ |- Ij: (y1..yq:C1..Cq)Bj
+ I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
+*)
-let abstract_inductive sec_sp ids_to_abs hyps inds =
- let abstract_one_assum id t inds =
- let ntyp = List.length inds in
- let new_refs =
- list_tabulate (fun k -> applist(mkRel (k+2),[mkRel 1])) ntyp in
- let inds' =
- List.map
- (function (np,tname,arity,cnames,lc) ->
- let arity' = mkNamedProd id t arity in
- let lc' =
- List.map (fun b -> mkNamedProd id t (substl new_refs b)) lc
- in
- (np,tname,arity',cnames,lc'))
- inds
- in
- inds' in
- let abstract_one_def id c inds =
+let abstract_inductive hyps inds =
+ let ntyp = List.length inds in
+ let nhyp = named_context_length hyps in
+ let args = instance_from_named_context (List.rev hyps) in
+ let subs = list_tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in
+ let inds' =
List.map
(function (np,tname,arity,cnames,lc) ->
- let arity' = replace_vars [id, c] arity in
- let lc' = List.map (replace_vars [id, c]) lc in
- (np,tname,arity',cnames,lc'))
- inds in
- let abstract_once ((hyps,inds,vars) as sofar) id =
- match hyps with
- | (hyp,None,t as d)::rest when id = hyp ->
- let inds' = abstract_one_assum hyp t inds in
- (rest, inds', (mkVar id, Libnames.make_path sec_sp id)::vars)
- | (hyp,Some b,t as d)::rest when id = hyp ->
- let inds' = abstract_one_def hyp b inds in
- (rest, inds', vars)
- | _ -> sofar in
- let (_,inds',vars) =
- List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in
- let inds'' =
- List.map
- (fun (nparams,a,arity,c,lc) ->
- let nparams' = nparams + (List.length vars) in
- let params, short_arity = decompose_prod_n_assum nparams' arity in
- let shortlc =
- List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in
- let params' =
- List.map
- (function
- | (Name id,None,p) -> id, Entries.LocalAssum p
- | (Name id,Some p,_) -> id, Entries.LocalDef p
- | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable")
- params in
- { mind_entry_params = params';
- mind_entry_typename = a;
- mind_entry_arity = short_arity;
- mind_entry_consnames = c;
- mind_entry_lc = shortlc })
- inds' in
- let l1,l2 = List.split vars in
- (inds'', Array.of_list l1, l2)
-
-let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
- assert (Array.length mib.mind_packets > 0);
- let record = mib.mind_record in
- let finite = mib.mind_finite in
+ let lc' = List.map (substl subs) lc in
+ let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in
+ let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in
+ (np,tname,arity',cnames,lc''))
+ inds in
+ List.map
+ (fun (nparams,a,arity,c,lc) ->
+ let nparams' = nparams + Array.length args in
+ let params, short_arity = decompose_prod_n_assum nparams' arity in
+ let shortlc =
+ List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in
+ let params' = List.map detype_param params in
+ { mind_entry_params = params';
+ mind_entry_typename = a;
+ mind_entry_arity = short_arity;
+ mind_entry_consnames = c;
+ mind_entry_lc = shortlc })
+ inds'
+
+let process_inductive sechyps modlist mib =
let inds =
array_map_to_list
(fun mip ->
let nparams = mip.mind_nparams in
- let arity = expmod_type modlist mip.mind_user_arity in
- let lc = Array.map (expmod_type modlist) mip.mind_user_lc in
+ let arity = expmod_constr modlist mip.mind_user_arity in
+ let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
(nparams,
mip.mind_typename,
arity,
Array.to_list mip.mind_consnames,
Array.to_list lc))
- mib.mind_packets
- in
- let hyps = mib.mind_hyps in
- let hyps' =
- Sign.fold_named_context
- (fun (x,b,t) sgn ->
- Sign.add_named_decl
- (x, option_app (expmod_constr modlist) b,expmod_constr modlist t)
- sgn)
- mib.mind_hyps ~init:empty_named_context in
- let (inds',abs_vars,discharged_hyps ) =
- abstract_inductive sec_sp ids_to_discard hyps' inds in
- let lmodif_one_mind i =
- let nbc = Array.length mib.mind_packets.(i).mind_consnames in
- (((osecsp,i), DO_ABSTRACT ((nsecsp,i),abs_vars)),
- list_tabulate
- (function j ->
- let j' = j + 1 in
- (((osecsp,i),j'), DO_ABSTRACT (((nsecsp,i),j'),abs_vars)))
- nbc)
- in
- let indmodifs,cstrmodifs =
- List.split (list_tabulate lmodif_one_mind mib.mind_ntypes) in
- ({ mind_entry_record = record;
- mind_entry_finite = finite;
- mind_entry_inds = inds' },
- indmodifs,
- List.flatten cstrmodifs,
- discharged_hyps)
-
-(* Discharge messages. *)
-
-let constant_message id =
- Options.if_verbose ppnl (pr_id id ++ str " is discharged.")
-
-let inductive_message inds =
- Options.if_verbose
- ppnl
- (hov 0
- (match inds with
- | [] -> assert false
- | [ind] ->
- (pr_id ind.mind_entry_typename ++ str " is discharged.")
- | l ->
- (prlist_with_sep pr_coma
- (fun ind -> pr_id ind.mind_entry_typename) l ++
- spc () ++ str "are discharged.")))
-
-(* Discharge operations for the various objects of the environment. *)
-
-type opacity = bool
-
-type discharge_operation =
- | Variable of identifier * section_variable_entry * local_kind *
- implicits_flags * Dischargedhypsmap.discharged_hyps
- | Constant of identifier * recipe * global_kind * constant *
- implicits_flags * Dischargedhypsmap.discharged_hyps
- | Inductive of mutual_inductive_entry * implicits_flags *
- Dischargedhypsmap.discharged_hyps
- | Class of cl_typ * cl_info_typ
- | Struc of inductive * (unit -> struc_typ)
- | CanonStruc of constant
- | Coercion of coercion_entry
- | Require of library_reference
- | Constraints of Univ.constraints
-
-(* Main function to traverse the library segment and compute the various
- discharge operations. *)
-
-let process_object oldenv olddir full_olddir newdir
-(* {dir -> newdir} {sec_sp -> full_olddir, olddir} *)
- (ops,ids_to_discard,(constl,indl,cstrl as work_alist)) ((sp,kn),lobj) =
- let tag = object_tag lobj in
- match tag with
- | "VARIABLE" ->
- let ((id,c,t),cst) = get_variable_with_constraints (basename sp) in
- (* VARIABLE means local (entry Variable/Hypothesis/Local and are *)
- (* always discharged *)
- (Constraints cst :: ops, id :: ids_to_discard, work_alist)
-
- | "CONSTANT" ->
- (* CONSTANT means never discharge (though visibility may vary) *)
- let kind = constant_kind sp in
- let kn = Nametab.locate_constant (qualid_of_sp sp) in
- let lab = con_label kn in
- let cb = Environ.lookup_constant kn oldenv in
- let imp = is_implicit_constant kn in
- let newkn = recalc_con newdir kn in
- let abs_vars,discharged_hyps0 =
- build_abstract_list full_olddir cb.const_hyps ids_to_discard in
- (* let's add the new discharged hypothesis to those already discharged*)
- let discharged_hyps =
- discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in
- let mods = [ (kn, DO_ABSTRACT(newkn,abs_vars)) ]
- in
- let r = { d_from = cb;
- d_modlist = work_alist;
- d_abstract = ids_to_discard } in
- let op = Constant (id_of_label lab,r,kind,newkn,imp,discharged_hyps) in
- (op :: ops, ids_to_discard, (mods@constl, indl, cstrl))
-
- | "INDUCTIVE" ->
- let kn = Nametab.locate_mind (qualid_of_sp sp) in
- let mib = Environ.lookup_mind kn oldenv in
- let newkn = recalc_kn newdir kn in
- let imp = is_implicit_inductive_definition kn in
-(* let imp = is_implicit_args (* CHANGE *) in*)
- let (mie,indmods,cstrmods,discharged_hyps0) =
- process_inductive full_olddir kn newkn oldenv (ids_to_discard,work_alist) mib in
- (* let's add the new discharged hypothesis to those already discharged*)
- let discharged_hyps =
- discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in
- ((Inductive(mie,imp,discharged_hyps)) :: ops, ids_to_discard,
- (constl,indmods@indl,cstrmods@cstrl))
-
- | "CLASS" ->
- let ((cl,clinfo) as x) = outClass lobj in
- if clinfo.cl_strength = Local then
- (ops,ids_to_discard,work_alist)
- else
- let (y1,y2) = process_class olddir ids_to_discard x in
- ((Class (y1,y2))::ops, ids_to_discard, work_alist)
-
- | "COERCION" ->
- let (_,coeinfo,_,_ as x) = outCoercion lobj in
- if coercion_strength coeinfo = Local then
- (ops,ids_to_discard,work_alist)
- else
- let y = process_coercion olddir ids_to_discard x in
- ((Coercion y)::ops, ids_to_discard, work_alist)
-
- | "STRUCTURE" ->
- let ((kn,i),info) = outStruc lobj in
- let newkn = recalc_kn newdir kn in
- let strobj () =
- let mib = Environ.lookup_mind newkn (Global.env ()) in
- { s_CONST = info.s_CONST;
- s_PARAM = mib.mind_packets.(0).mind_nparams;
- s_PROJ = List.map (option_app (fun kn -> recalc_con newdir kn)) info.s_PROJ } in
- ((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist)
-
- | "CANONICAL-STRUCTURE" ->
- let kn = outCanonicalStructure lobj in
- let new_kn = recalc_con newdir kn in
- ((CanonStruc new_kn)::ops, ids_to_discard, work_alist)
-
- | "REQUIRE" ->
- let c = out_require lobj in
- ((Require c)::ops, ids_to_discard, work_alist)
-
- | _ -> (ops,ids_to_discard,work_alist)
-
-let process_item oldenv olddir full_olddir newdir acc = function
- | (sp,Leaf lobj) ->
- process_object oldenv olddir full_olddir newdir acc (sp,lobj)
- | (_,_) -> acc
-
-let process_operation = function
- | Variable (id,expmod_a,stre,imp,discharged_hyps) ->
- (* Warning:parentheses needed to get a side-effect from with_implicits *)
- with_implicits imp (redeclare_variable id discharged_hyps)
- (Lib.cwd(),expmod_a,stre)
- | Constant (id,r,stre,kn,imp,discharged_hyps) ->
- with_implicits imp (redeclare_constant id discharged_hyps) (r,stre);
- constant_message id
- | Inductive (mie,imp,discharged_hyps) ->
- let _ = with_implicits imp (redeclare_inductive discharged_hyps) 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 ()))
- | CanonStruc newsp ->
- begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end
- | Coercion y -> add_new_coercion y
- | Require y -> reload_library y
- | Constraints y -> Global.add_constraints y
-
-let catch_not_found f x =
- try f x
- with Not_found ->
- error ("Something is missing; perhaps a reference to a"^
- " module required inside the section")
-
-let close_section _ s =
- let oldenv = Global.env() in
- let prefix,decls,fs = close_section false s in
- let full_olddir, (_,olddir) = prefix in
- let newdir = fst (split_dirpath olddir) in
- let (ops,ids,_) =
- List.fold_left
- (process_item oldenv olddir full_olddir newdir) ([],[],([],[],[])) decls
- in
- let ids = last_section_hyps olddir in
- Summary.section_unfreeze_summaries fs;
- catch_not_found (List.iter process_operation) (List.rev ops);
- Nametab.push_dir (Until 1) full_olddir (DirClosedSection full_olddir)
+ mib.mind_packets in
+ let sechyps' = map_named_context (expmod_constr modlist) sechyps in
+ let inds' = abstract_inductive sechyps' inds in
+ { mind_entry_record = mib.mind_record;
+ mind_entry_finite = mib.mind_finite;
+ mind_entry_inds = inds' }
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index b8db027ba..c8af4d1da 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -8,11 +8,10 @@
(*i $Id$ i*)
-open Names
+open Sign
+open Cooking
+open Declarations
+open Entries
-(* This module implements the discharge mechanism. It provides a function to
- close the last opened section. That function calls [Lib.close_section] and
- then re-introduce all the discharged versions of the objects that were
- defined in the section. *)
-
-val close_section : bool -> identifier -> unit
+val process_inductive :
+ named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
index 6457fb538..4c1e2210a 100755
--- a/toplevel/recordobj.ml
+++ b/toplevel/recordobj.ml
@@ -8,68 +8,3 @@
(* $Id$ *)
-open Util
-open Pp
-open Names
-open Libnames
-open Nameops
-open Term
-open Lib
-open Declare
-open Recordops
-open Classops
-open Nametab
-
-(***** object definition ******)
-
-let typ_lams_of t =
- let rec aux acc c = match kind_of_term c with
- | Lambda (x,c1,c2) -> aux (c1::acc) c2
- | Cast (c,_) -> aux acc c
- | t -> acc,t
- in aux [] t
-
-let objdef_err ref =
- errorlabstrm "object_declare"
- (pr_id (id_of_global ref) ++
- str" is not a structure object")
-
-let objdef_declare ref =
- let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in
- let env = Global.env () in
- let v = constr_of_reference ref in
- let vc = match Environ.constant_opt_value env sp with
- | Some vc -> vc
- | None -> objdef_err ref in
- let lt,t = decompose_lam vc in
- let lt = List.rev (List.map snd lt) in
- let f,args = match kind_of_term t with
- | App (f,args) -> f,args
- | _ -> objdef_err ref in
- let { s_PARAM = p; s_PROJ = lpj } =
- try (find_structure
- (match kind_of_term f with
- | Construct (indsp,1) -> indsp
- | _ -> objdef_err ref))
- with Not_found -> objdef_err ref in
- let params, projs =
- try list_chop p (Array.to_list args)
- with _ -> objdef_err ref in
- let lps =
- try List.combine lpj projs
- with _ -> objdef_err ref in
- let comp =
- List.fold_left
- (fun l (spopt,t) -> (* comp=components *)
- match spopt with
- | None -> l
- | Some proji_sp ->
- let c, args = decompose_app t in
- try (ConstRef proji_sp, reference_of_constr c, args) :: l
- with Not_found -> l)
- [] lps in
- let comp' = List.map (fun (refi,c,argj) ->
- (refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj}) comp in
- add_canonical_structure (sp, comp')
-
-let add_object_hook _ = objdef_declare
diff --git a/toplevel/recordobj.mli b/toplevel/recordobj.mli
index 02c3126dd..5bbeecc2c 100755
--- a/toplevel/recordobj.mli
+++ b/toplevel/recordobj.mli
@@ -8,5 +8,3 @@
(*i $Id$ i*)
-val objdef_declare : Libnames.global_reference -> unit
-val add_object_hook : Tacexpr.declaration_hook
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 04:44:50 +0000