aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml12
-rw-r--r--library/declare.mli2
-rw-r--r--library/impargs.ml76
-rw-r--r--library/impargs.mli3
-rw-r--r--library/lib.ml21
-rw-r--r--library/lib.mli2
-rw-r--r--library/libobject.ml15
-rw-r--r--library/libobject.mli6
8 files changed, 78 insertions, 59 deletions
diff --git a/library/declare.ml b/library/declare.ml
index da2c1b778..278acc665 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -57,7 +57,7 @@ let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
type section_variable_entry =
| SectionLocalDef of constr * types option * bool (* opacity *)
- | SectionLocalAssum of types
+ | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
type variable_declaration = dir_path * section_variable_entry * logical_kind
@@ -84,17 +84,17 @@ let cache_variable ((sp,_),o) =
(* Constr raisonne sur les noms courts *)
if Idmap.mem id !vartab then
errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
- let vd = match d with (* Fails if not well-typed *)
- | SectionLocalAssum ty ->
+ let vd,impl,keep = match d with (* Fails if not well-typed *)
+ | SectionLocalAssum (ty, impl, keep) ->
let cst = Global.push_named_assum (id,ty) in
let (_,bd,ty) = Global.lookup_named id in
- CheckedSectionLocalAssum (ty,cst)
+ CheckedSectionLocalAssum (ty,cst), impl, if keep then Some ty else None
| SectionLocalDef (c,t,opaq) ->
let cst = Global.push_named_def (id,c,t) in
let (_,bd,ty) = Global.lookup_named id in
- CheckedSectionLocalDef (Option.get bd,ty,cst,opaq) in
+ CheckedSectionLocalDef (Option.get bd,ty,cst,opaq), false, None in
Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
- add_section_variable id;
+ add_section_variable id impl keep;
Dischargedhypsmap.set_discharged_hyps sp [];
vartab := Idmap.add id (p,vd,mk) !vartab
diff --git a/library/declare.mli b/library/declare.mli
index f04170b34..96fd5eb9b 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -34,7 +34,7 @@ open Nametab
type section_variable_entry =
| SectionLocalDef of constr * types option * bool (* opacity *)
- | SectionLocalAssum of types
+ | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
type variable_declaration = dir_path * section_variable_entry * logical_kind
diff --git a/library/impargs.ml b/library/impargs.ml
index 9ffd103de..fc2d63ca8 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -240,12 +240,6 @@ let compute_implicits_flags env f all t =
(f.strict or f.strongly_strict) f.strongly_strict
f.reversible_pattern f.contextual all env t
-let compute_implicits_auto env f t =
- let l = compute_implicits_flags env f false t in
- prepare_implicits f l
-
-let compute_implicits env t = compute_implicits_auto env !implicit_args t
-
let set_implicit id imp insmax =
(id,(match imp with None -> Manual false | Some imp -> imp),insmax)
@@ -258,7 +252,7 @@ let rec assoc_by_pos k = function
| hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
| [] -> raise Not_found
-let compute_manual_implicits flags env t enriching l =
+let compute_manual_implicits env flags t enriching l =
let autoimps =
if enriching then compute_implicits_flags env flags true t
else compute_implicits_gen false false false true true env t in
@@ -296,8 +290,9 @@ let compute_manual_implicits flags env t enriching l =
forced :: merge (k+1) l' imps
| [] when l = [] -> []
| [] ->
- match List.hd l with
- | ExplByName id,b ->
+ List.iter (function
+ | ExplByName id,(b,forced) ->
+ if not forced then
error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
| ExplByPos (i,_id),_t ->
if i<1 or i>n then
@@ -305,10 +300,19 @@ let compute_manual_implicits flags env t enriching l =
else
errorlabstrm ""
(str "Cannot set implicit argument number " ++ int i ++
- str ": it has no name")
+ str ": it has no name"))
+ l; []
in
merge 1 l autoimps
+let compute_implicits_auto env f manual t =
+ match manual with
+ [] -> let l = compute_implicits_flags env f false t in
+ prepare_implicits f l
+ | _ -> compute_manual_implicits env f t true manual
+
+let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
+
type maximal_insertion = bool (* true = maximal contextual insertion *)
type implicit_status =
@@ -353,16 +357,16 @@ let positions_of_implicits =
(*s Constants. *)
-let compute_constant_implicits flags cst =
+let compute_constant_implicits flags manual cst =
let env = Global.env () in
- compute_implicits_auto env flags (Typeops.type_of_constant env cst)
+ compute_implicits_auto env flags manual (Typeops.type_of_constant env cst)
(*s Inductives and constructors. Their implicit arguments are stored
in an array, indexed by the inductive number, of pairs $(i,v)$ where
$i$ are the implicit arguments of the inductive and $v$ the array of
implicit arguments of the constructors. *)
-let compute_mib_implicits flags kn =
+let compute_mib_implicits flags manual kn =
let env = Global.env () in
let mib = lookup_mind kn env in
let ar =
@@ -375,34 +379,34 @@ let compute_mib_implicits flags kn =
let imps_one_inductive i mip =
let ind = (kn,i) in
let ar = type_of_inductive env (mib,mip) in
- ((IndRef ind,compute_implicits_auto env flags ar),
+ ((IndRef ind,compute_implicits_auto env flags manual ar),
Array.mapi (fun j c ->
- (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags c))
+ (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags manual c))
mip.mind_nf_lc)
in
Array.mapi imps_one_inductive mib.mind_packets
-let compute_all_mib_implicits flags kn =
- let imps = compute_mib_implicits flags kn in
+let compute_all_mib_implicits flags manual kn =
+ let imps = compute_mib_implicits flags manual kn in
List.flatten
(array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps)
(*s Variables. *)
-let compute_var_implicits flags id =
+let compute_var_implicits flags manual id =
let env = Global.env () in
let (_,_,ty) = lookup_named id env in
- compute_implicits_auto env flags ty
+ compute_implicits_auto env flags manual ty
(* Implicits of a global reference. *)
-let compute_global_implicits flags = function
- | VarRef id -> compute_var_implicits flags id
- | ConstRef kn -> compute_constant_implicits flags kn
+let compute_global_implicits flags manual = function
+ | VarRef id -> compute_var_implicits flags manual id
+ | ConstRef kn -> compute_constant_implicits flags manual kn
| IndRef (kn,i) ->
- let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps
+ let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps
| ConstructRef ((kn,i),j) ->
- let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1)
+ let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1)
(* Merge a manual explicitation with an implicit_status list *)
@@ -459,19 +463,23 @@ let discharge_implicits (_,(req,l)) =
| ImplMutualInductive (kn,flags) ->
Some (ImplMutualInductive (pop_kn kn,flags),l)
-let rebuild_implicits (req,l) =
+let rebuild_implicits (info,(req,l)) =
+ let manual = List.fold_left (fun acc (id, impl, keep) ->
+ if impl then (ExplByName id, (true, true)) :: acc else acc)
+ [] info
+ in
let l' = match req with
| ImplNoDischarge -> assert false
| ImplConstant (con,flags) ->
- [ConstRef con,compute_constant_implicits flags con]
+ [ConstRef con, compute_constant_implicits flags manual con]
| ImplMutualInductive (kn,flags) ->
- compute_all_mib_implicits flags kn
+ compute_all_mib_implicits flags manual kn
| ImplInteractive (ref,flags,o) ->
match o with
- | ImplAuto -> [ref,compute_global_implicits flags ref]
+ | ImplAuto -> [ref,compute_global_implicits flags manual ref]
| ImplManual l ->
- let auto = compute_global_implicits flags ref in
- let auto = if flags.main then auto else List.map (fun _ -> None) auto in
+ let auto = compute_global_implicits flags manual ref in
+(* let auto = if flags.main then auto else List.map (fun _ -> None) auto in *)
let l' = merge_impls auto l in [ref,l']
in (req,l')
@@ -487,7 +495,7 @@ let (inImplicits, _) =
export_function = (fun x -> Some x) }
let declare_implicits_gen req flags ref =
- let imps = compute_global_implicits flags ref in
+ let imps = compute_global_implicits flags [] ref in
add_anonymous_leaf (inImplicits (req,[ref,imps]))
let declare_implicits local ref =
@@ -510,7 +518,7 @@ let declare_mib_implicits kn =
let flags = !implicit_args in
let imps = array_map_to_list
(fun (ind,cstrs) -> ind::(Array.to_list cstrs))
- (compute_mib_implicits flags kn) in
+ (compute_mib_implicits flags [] kn) in
add_anonymous_leaf
(inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
@@ -518,13 +526,13 @@ let declare_mib_implicits kn =
type manual_explicitation = Topconstr.explicitation * (bool * bool)
let compute_implicits_with_manual env typ enriching l =
- compute_manual_implicits !implicit_args env typ enriching l
+ compute_manual_implicits env !implicit_args typ enriching l
let declare_manual_implicits local ref enriching l =
let flags = !implicit_args in
let env = Global.env () in
let t = Global.type_of_global ref in
- let l' = compute_manual_implicits flags env t enriching l in
+ let l' = compute_manual_implicits env flags t enriching l in
let req =
if local or isVarRef ref then ImplNoDischarge
else ImplInteractive(ref,flags,ImplManual l')
diff --git a/library/impargs.mli b/library/impargs.mli
index e7b05f422..120660027 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -59,7 +59,8 @@ val compute_implicits : env -> types -> implicits_list
maximal insertion and forcing flags. *)
type manual_explicitation = Topconstr.explicitation * (bool * bool)
-val compute_implicits_with_manual : env -> types -> bool -> manual_explicitation list -> implicits_list
+val compute_implicits_with_manual : env -> types -> bool ->
+ manual_explicitation list -> implicits_list
(*s Computation of implicits (done using the global environment). *)
diff --git a/library/lib.ml b/library/lib.ml
index 4acdba88c..1db433c19 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -214,9 +214,9 @@ let add_leaf id obj =
add_entry oname (Leaf obj);
oname
-let add_discharged_leaf id obj =
+let add_discharged_leaf id varinfo obj =
let oname = make_oname id in
- let newobj = rebuild_object obj in
+ let newobj = rebuild_object (varinfo, obj) in
cache_object (oname,newobj);
add_entry oname (Leaf newobj)
@@ -440,18 +440,19 @@ let what_is_opened () = find_entry_p is_something_opened
type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t
let sectab =
- ref ([] : (identifier list * Cooking.work_list * abstr_list) list)
+ ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list)
let add_section () =
sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
-let add_section_variable id =
+let add_section_variable id impl keep =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
- | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl
+ | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
let rec extract_hyps = function
- | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
+ | ((id,impl,keep)::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
+ | ((id,impl,Some ty)::idl,hyps) -> (id,None,ty) :: extract_hyps (idl,hyps)
| (id::idl,hyps) -> extract_hyps (idl,hyps)
| [], _ -> []
@@ -473,6 +474,8 @@ let add_section_constant kn =
let replacement_context () = pi2 (List.hd !sectab)
+let variables_context () = pi1 (List.hd !sectab)
+
let section_segment_of_constant con =
Cmap.find con (fst (pi3 (List.hd !sectab)))
@@ -548,6 +551,10 @@ let close_section id =
with Not_found ->
error "no opened section"
in
+ let var_info = List.map
+ (fun (x, y, z) -> (x, y, match z with Some _ -> true | None -> false))
+ (variables_context ())
+ in
let (secdecls,secopening,before) = split_lib oname in
lib_stk := before;
let full_olddir = fst !path_prefix in
@@ -556,7 +563,7 @@ let close_section id =
if !Flags.xml_export then !xml_close_section id;
let newdecls = List.map discharge_item secdecls in
Summary.section_unfreeze_summaries fs;
- List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
+ List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id var_info o)) newdecls;
Cooking.clear_cooking_sharing ();
Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
diff --git a/library/lib.mli b/library/lib.mli
index 6c826af63..da8ace048 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -175,7 +175,7 @@ val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context
val section_instance : global_reference -> identifier array
-val add_section_variable : identifier -> unit
+val add_section_variable : identifier -> bool -> Term.types option -> unit
val add_section_constant : constant -> Sign.named_context -> unit
val add_section_kn : kernel_name -> Sign.named_context -> unit
val replacement_context : unit ->
diff --git a/library/libobject.ml b/library/libobject.ml
index 7c74d402b..b24a46e38 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -28,6 +28,7 @@ let relax b = relax_flag := b;;
type 'a substitutivity =
Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
+type discharge_info = (identifier * bool * bool) list
type 'a object_declaration = {
object_name : string;
@@ -37,7 +38,7 @@ type 'a object_declaration = {
classify_function : object_name * 'a -> 'a substitutivity;
subst_function : object_name * substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
- rebuild_function : 'a -> 'a;
+ rebuild_function : discharge_info * 'a -> 'a;
export_function : 'a -> 'a option }
let yell s = anomaly s
@@ -51,7 +52,7 @@ let default_object s = {
yell ("The object "^s^" does not know how to substitute!"));
classify_function = (fun (_,obj) -> Keep obj);
discharge_function = (fun _ -> None);
- rebuild_function = (fun x -> x);
+ rebuild_function = (fun (_,x) -> x);
export_function = (fun _ -> None)}
@@ -77,7 +78,7 @@ type dynamic_object_declaration = {
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_rebuild_function : obj -> obj;
+ dyn_rebuild_function : discharge_info * obj -> obj;
dyn_export_function : obj -> obj option }
let object_tag lobj = Dyn.tag lobj
@@ -115,8 +116,8 @@ let declare_object odecl =
Option.map infun (odecl.discharge_function (oname,outfun lobj))
else
anomaly "somehow we got the wrong dynamic object in the dischargefun"
- and rebuild lobj =
- if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
+ and rebuild (varinfo,lobj) =
+ if Dyn.tag lobj = na then infun (odecl.rebuild_function (varinfo,outfun lobj))
else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
and exporter lobj =
if Dyn.tag lobj = na then
@@ -173,8 +174,8 @@ let classify_object ((_,lobj) as node) =
let discharge_object ((_,lobj) as node) =
apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
-let rebuild_object lobj =
- apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj
+let rebuild_object ((_,lobj) as node) =
+ apply_dyn_fun lobj (fun d -> d.dyn_rebuild_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 540b69feb..15de388ea 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -63,6 +63,8 @@ open Mod_subst
type 'a substitutivity =
Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
+type discharge_info = (identifier * bool * bool) list
+
type 'a object_declaration = {
object_name : string;
cache_function : object_name * 'a -> unit;
@@ -71,7 +73,7 @@ type 'a object_declaration = {
classify_function : object_name * 'a -> 'a substitutivity;
subst_function : object_name * substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
- rebuild_function : 'a -> 'a;
+ rebuild_function : discharge_info * 'a -> 'a;
export_function : 'a -> 'a option }
(* The default object is a "Keep" object with empty methods.
@@ -106,5 +108,5 @@ 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 rebuild_object : obj -> obj
+val rebuild_object : discharge_info * obj -> obj
val relax : bool -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 22:13:13 +0000