aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml6
-rw-r--r--kernel/cClosure.mli4
-rw-r--r--kernel/clambda.ml5
-rw-r--r--kernel/constr.ml44
-rw-r--r--kernel/constr.mli6
-rw-r--r--kernel/declarations.ml4
-rw-r--r--kernel/declareops.ml4
-rw-r--r--kernel/environ.ml20
-rw-r--r--kernel/environ.mli4
-rw-r--r--kernel/inferCumulativity.ml5
-rw-r--r--kernel/mod_subst.ml2
-rw-r--r--kernel/mod_typing.ml71
-rw-r--r--kernel/mod_typing.mli8
-rw-r--r--kernel/modops.ml3
-rw-r--r--kernel/nativelambda.ml2
-rw-r--r--kernel/nativelib.ml2
-rw-r--r--kernel/nativevalues.ml4
-rw-r--r--kernel/reduction.ml13
-rw-r--r--kernel/safe_typing.ml237
-rw-r--r--kernel/safe_typing.mli4
-rw-r--r--kernel/section.ml2
-rw-r--r--kernel/section.mli3
-rw-r--r--kernel/sorts.ml2
-rw-r--r--kernel/sorts.mli2
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--kernel/uGraph.ml2
-rw-r--r--kernel/uGraph.mli4
27 files changed, 259 insertions, 206 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 1316dfe069..de02882370 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -613,7 +613,7 @@ let rec to_constr lfts v =
subst_constr subs f)
| FEvar ((ev,args),env) ->
let subs = comp_subs lfts env in
- mkEvar(ev,Array.map (fun a -> subst_constr subs a) args)
+ mkEvar(ev,List.map (fun a -> subst_constr subs a) args)
| FLIFT (k,a) -> to_constr (el_shft k lfts) a
| FInt i ->
@@ -678,6 +678,8 @@ let rec zip m stk =
let fapp_stack (m,stk) = zip m stk
+let term_of_process c stk = term_of_fconstr (zip c stk)
+
(*********************************************************************)
(* The assertions in the functions below are granted because they are
@@ -1406,7 +1408,7 @@ and norm_head info tab m =
Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
| FEvar((i,args),env) ->
- mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
+ mkEvar(i, List.map (fun a -> kl info tab (mk_clos env a)) args)
| FProj (p,c) ->
mkProj (p, kl info tab c)
| FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 9e94248113..79092813bc 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -227,6 +227,10 @@ val kni: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val knr: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val kl : clos_infos -> clos_tab -> fconstr -> constr
+val zip : fconstr -> stack -> fconstr
+
+val term_of_process : fconstr -> stack -> constr
+
val to_constr : lift -> fconstr -> constr
(** End of cbn debug section i*)
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 8c7aa6b17a..65de52c0f6 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -670,7 +670,7 @@ let rec lambda_of_constr env c =
match Constr.kind c with
| Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta")
| Evar (evk, args) ->
- let args = lambda_of_args env 0 args in
+ let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
Levar (evk, args)
| Cast (c, _, _) -> lambda_of_constr env c
@@ -799,9 +799,6 @@ and lambda_of_args env start args =
(fun i -> lambda_of_constr env args.(start + i))
else empty_args
-
-
-
(*********************************)
let dump_lambda = ref false
diff --git a/kernel/constr.ml b/kernel/constr.ml
index ade03fdf93..703e3616a0 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -71,7 +71,7 @@ type case_info =
(* [constr array] is an instance matching definitional [named_context] in
the same order (i.e. last argument first) *)
-type 'constr pexistential = existential_key * 'constr array
+type 'constr pexistential = existential_key * 'constr list
type ('constr, 'types) prec_declaration =
Name.t binder_annot array * 'types array * 'constr array
type ('constr, 'types) pfixpoint =
@@ -110,7 +110,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
type t = (t, t, Sorts.t, Instance.t) kind_of_term
type constr = t
-type existential = existential_key * constr array
+type existential = existential_key * constr list
type types = constr
@@ -470,7 +470,7 @@ let fold f acc c = match kind c with
| LetIn (_,b,t,c) -> f (f (f acc b) t) c
| App (c,l) -> Array.fold_left f (f acc c) l
| Proj (_p,c) -> f acc c
- | Evar (_,l) -> Array.fold_left f acc l
+ | Evar (_,l) -> List.fold_left f acc l
| Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
| Fix (_,(_lna,tl,bl)) ->
Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
@@ -490,7 +490,7 @@ let iter f c = match kind c with
| LetIn (_,b,t,c) -> f b; f t; f c
| App (c,l) -> f c; Array.iter f l
| Proj (_p,c) -> f c
- | Evar (_,l) -> Array.iter f l
+ | Evar (_,l) -> List.iter f l
| Case (_,p,c,bl) -> f p; f c; Array.iter f bl
| Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
| CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
@@ -509,7 +509,7 @@ let iter_with_binders g f n c = match kind c with
| Lambda (_,t,c) -> f n t; f (g n) c
| LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
| App (c,l) -> f n c; Array.Fun1.iter f n l
- | Evar (_,l) -> Array.Fun1.iter f n l
+ | Evar (_,l) -> List.iter (fun c -> f n c) l
| Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
| Proj (_p,c) -> f n c
| Fix (_,(_,tl,bl)) ->
@@ -536,7 +536,7 @@ let fold_constr_with_binders g f n acc c =
| LetIn (_na,b,t,c) -> f (g n) (f n (f n acc b) t) c
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
| Proj (_p,c) -> f n acc c
- | Evar (_,l) -> Array.fold_left (f n) acc l
+ | Evar (_,l) -> List.fold_left (f n) acc l
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
| Fix (_,(_,tl,bl)) ->
let n' = iterate g (Array.length tl) n in
@@ -657,7 +657,7 @@ let map_gen userview f c = match kind c with
if t' == t then c
else mkProj (p, t')
| Evar (e,l) ->
- let l' = Array.Smart.map f l in
+ let l' = List.Smart.map f l in
if l'==l then c
else mkEvar (e, l')
| Case (ci,p,b,bl) when userview ->
@@ -722,7 +722,8 @@ let fold_map f accu c = match kind c with
if t' == t then accu, c
else accu, mkProj (p, t')
| Evar (e,l) ->
- let accu, l' = Array.Smart.fold_left_map f accu l in
+ (* Doesn't matter, we should not hashcons evars anyways *)
+ let accu, l' = List.fold_left_map f accu l in
if l'==l then accu, c
else accu, mkEvar (e, l')
| Case (ci,p,b,bl) ->
@@ -782,7 +783,7 @@ let map_with_binders g f l c0 = match kind c0 with
if t' == t then c0
else mkProj (p, t')
| Evar (e, al) ->
- let al' = Array.Fun1.Smart.map f l al in
+ let al' = List.Smart.map (fun c -> f l c) al in
if al' == al then c0
else mkEvar (e, al')
| Case (ci, p, c, bl) ->
@@ -834,7 +835,7 @@ let fold_with_full_binders g f n acc c =
| LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
| Proj (_,c) -> f n acc c
- | Evar (_,l) -> Array.fold_left (f n) acc l
+ | Evar (_,l) -> List.fold_left (f n) acc l
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
| Fix (_,(lna,tl,bl)) ->
let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
@@ -880,7 +881,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
Int.equal len (Array.length l2) &&
leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2
| Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2
- | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2
+ | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2
| Const (c1,u1), Const (c2,u2) ->
(* The args length currently isn't used but may as well pass it. *)
Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2
@@ -1039,7 +1040,7 @@ let constr_ord_int f t1 t2 =
| Meta m1, Meta m2 -> Int.compare m1 m2
| Meta _, _ -> -1 | _, Meta _ -> 1
| Evar (e1,l1), Evar (e2,l2) ->
- (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
+ (Evar.compare =? (List.compare f)) e1 e2 l1 l2
| Evar _, _ -> -1 | _, Evar _ -> 1
| Sort s1, Sort s2 -> Sorts.compare s1 s2
| Sort _, _ -> -1 | _, Sort _ -> 1
@@ -1141,7 +1142,7 @@ let hasheq t1 t2 =
n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2
| App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2
| Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2
- | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2
+ | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && List.equal (==) l1 l2
| Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2
| Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2
| Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2
@@ -1221,7 +1222,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
let l, hl = hash_term_array l in
(App (c,l), combinesmall 7 (combine hl hc))
| Evar (e,l) ->
- let l, hl = hash_term_array l in
+ let l, hl = hash_list_array l in
(Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
| Const (c,u) ->
let c' = sh_con c in
@@ -1289,6 +1290,14 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
let h = !accu land 0x3FFFFFFF in
(HashsetTermArray.repr h t term_array_table, h)
+ and hash_list_array l =
+ let fold accu c =
+ let c, h = sh_rec c in
+ (combine accu h, c)
+ in
+ let h, l = List.fold_left_map fold 0 l in
+ (l, h land 0x3FFFFFFF)
+
in
(* Make sure our statically allocated Rels (1 to 16) are considered
as canonical, and hence hash-consed to themselves *)
@@ -1316,7 +1325,7 @@ let rec hash t =
| App (c,l) ->
combinesmall 7 (combine (hash_term_array l) (hash c))
| Evar (e,l) ->
- combinesmall 8 (combine (Evar.hash e) (hash_term_array l))
+ combinesmall 8 (combine (Evar.hash e) (hash_term_list l))
| Const (c,u) ->
combinesmall 9 (combine (Constant.hash c) (Instance.hash u))
| Ind (ind,u) ->
@@ -1339,6 +1348,9 @@ let rec hash t =
and hash_term_array t =
Array.fold_left (fun acc t -> combine acc (hash t)) 0 t
+and hash_term_list t =
+ List.fold_left (fun acc t -> combine (hash t) acc) 0 t
+
module CaseinfoHash =
struct
type t = case_info
@@ -1458,7 +1470,7 @@ let rec debug_print c =
prlist_with_sep spc debug_print (Array.to_list l) ++ str")")
| Evar (e,l) -> hov 1
(str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
- prlist_with_sep spc debug_print (Array.to_list l) ++str"}")
+ prlist_with_sep spc debug_print l ++str"}")
| Const (c,u) -> str"Cst(" ++ pr_puniverses (Constant.debug_print c) u ++ str")"
| Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")"
| Construct (((sp,i),j),u) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 16919b705a..00051d7551 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -83,7 +83,7 @@ val mkFloat : Float64.t -> constr
val mkMeta : metavariable -> constr
(** Constructs an existential variable *)
-type existential = Evar.t * constr array
+type existential = Evar.t * constr list
val mkEvar : existential -> constr
(** Construct a sort *)
@@ -203,9 +203,9 @@ val mkCoFix : cofixpoint -> constr
(** {6 Concrete type for making pattern-matching. } *)
-(** [constr array] is an instance matching definitional [named_context] in
+(** [constr list] is an instance matching definitional [named_context] in
the same order (i.e. last argument first) *)
-type 'constr pexistential = Evar.t * 'constr array
+type 'constr pexistential = Evar.t * 'constr list
type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 244cd2865d..2f6a870c8a 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -92,6 +92,8 @@ type typing_flags = {
indices_matter: bool;
(** The universe of an inductive type must be above that of its indices. *)
+ cumulative_sprop : bool;
+ (** SProp <= Type *)
}
(* some contraints are in constant_constraints, some other may be in
@@ -293,8 +295,6 @@ and 'a generic_module_body =
mod_expr : 'a; (** implementation *)
mod_type : module_signature; (** expanded type *)
mod_type_alg : module_expression option; (** algebraic type *)
- mod_constraints : Univ.ContextSet.t; (**
- set of all universes constraints in the module *)
mod_delta : Mod_subst.delta_resolver; (**
quotiented set of equivalent constants and inductive names *)
mod_retroknowledge : 'a module_retroknowledge }
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 20dc21900c..0ab99cab35 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,6 +26,7 @@ let safe_flags oracle = {
enable_VM = true;
enable_native_compiler = true;
indices_matter = true;
+ cumulative_sprop = false;
}
(** {6 Arities } *)
@@ -390,7 +391,6 @@ and hcons_generic_module_body :
let expr' = hcons_impl mb.mod_expr in
let type' = hcons_module_signature mb.mod_type in
let type_alg' = mb.mod_type_alg in
- let constraints' = Univ.hcons_universe_context_set mb.mod_constraints in
let delta' = mb.mod_delta in
let retroknowledge' = mb.mod_retroknowledge in
@@ -399,7 +399,6 @@ and hcons_generic_module_body :
mb.mod_expr == expr' &&
mb.mod_type == type' &&
mb.mod_type_alg == type_alg' &&
- mb.mod_constraints == constraints' &&
mb.mod_delta == delta' &&
mb.mod_retroknowledge == retroknowledge'
then mb
@@ -408,7 +407,6 @@ and hcons_generic_module_body :
mod_expr = expr';
mod_type = type';
mod_type_alg = type_alg';
- mod_constraints = constraints';
mod_delta = delta';
mod_retroknowledge = retroknowledge';
}
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2d2c9a454b..d6d52dbc2b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -128,7 +128,7 @@ let empty_env = {
env_nb_rel = 0;
env_stratification = {
env_universes = UGraph.initial_universes;
- env_sprop_allowed = false;
+ env_sprop_allowed = true;
env_universes_lbound = Univ.Level.set;
env_engagement = PredicativeSet };
env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
@@ -279,6 +279,9 @@ let indices_matter env = env.env_typing_flags.indices_matter
let universes env = env.env_stratification.env_universes
let universes_lbound env = env.env_stratification.env_universes_lbound
+let set_universes g env =
+ {env with env_stratification = {env.env_stratification with env_universes=g}}
+
let set_universes_lbound env lbound =
let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in
{ env with env_stratification }
@@ -431,7 +434,7 @@ let push_subgraph (levels,csts) env =
in
map_universes add_subgraph env
-let set_engagement c env = (* Unsafe *)
+let set_engagement c env =
{ env with env_stratification =
{ env.env_stratification with env_engagement = c } }
@@ -445,6 +448,7 @@ let same_flags {
share_reduction;
enable_VM;
enable_native_compiler;
+ cumulative_sprop;
} alt =
check_guarded == alt.check_guarded &&
check_positive == alt.check_positive &&
@@ -453,14 +457,18 @@ let same_flags {
indices_matter == alt.indices_matter &&
share_reduction == alt.share_reduction &&
enable_VM == alt.enable_VM &&
- enable_native_compiler == alt.enable_native_compiler
+ enable_native_compiler == alt.enable_native_compiler &&
+ cumulative_sprop == alt.cumulative_sprop
[@warning "+9"]
-let set_typing_flags c env = (* Unsafe *)
+let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b)
+
+let set_typing_flags c env =
if same_flags env.env_typing_flags c then env
- else { env with env_typing_flags = c }
+ else set_cumulative_sprop c.cumulative_sprop { env with env_typing_flags = c }
-let make_sprop_cumulative = map_universes UGraph.make_sprop_cumulative
+let set_cumulative_sprop b env =
+ set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
let set_allow_sprop b env =
{ env with env_stratification =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 25ecdfd852..7a46538772 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -102,6 +102,8 @@ val rel_context : env -> Constr.rel_context
val named_context : env -> Constr.named_context
val named_context_val : env -> named_context_val
+val set_universes : UGraph.t -> env -> env
+
val opaque_tables : env -> Opaqueproof.opaquetab
val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
@@ -310,7 +312,7 @@ val push_subgraph : Univ.ContextSet.t -> env -> env
val set_engagement : engagement -> env -> env
val set_typing_flags : typing_flags -> env -> env
-val make_sprop_cumulative : env -> env
+val set_cumulative_sprop : bool -> env -> env
val set_allow_sprop : bool -> env -> env
val sprop_allowed : env -> bool
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index f987164d52..662ad550b8 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
end
| FEvar ((_,args),e) ->
let variances = infer_stack infos variances stk in
- infer_vect infos variances (Array.map (mk_clos e) args)
+ infer_list infos variances (List.map (mk_clos e) args)
| FRel _ -> infer_stack infos variances stk
| FInt _ -> infer_stack infos variances stk
| FFloat _ -> infer_stack infos variances stk
@@ -168,6 +168,9 @@ and infer_stack infos variances (stk:CClosure.stack) =
and infer_vect infos variances v =
Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
+and infer_list infos variances v =
+ List.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
+
let infer_term cv_pb env variances c =
let open CClosure in
let infos = (create_clos_infos all env, create_tab ()) in
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index aa513c1536..317141e324 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -405,7 +405,7 @@ let rec map_kn f f' c =
if (ct'== ct && l'==l) then c
else mkApp (ct',l')
| Evar (e,l) ->
- let l' = Array.Smart.map func l in
+ let l' = List.Smart.map func l in
if (l'==l) then c
else mkEvar (e,l')
| Fix (ln,(lna,tl,bl)) ->
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 76e2a584bd..44b010204b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -23,7 +23,7 @@ open Modops
open Mod_subst
type 'alg translation =
- module_signature * 'alg * delta_resolver * Univ.ContextSet.t
+ module_signature * 'alg * delta_resolver * Univ.Constraint.t
let rec mp_from_mexpr = function
| MEident mp -> mp
@@ -54,8 +54,6 @@ let rec rebuild_mp mp l =
| []-> mp
| i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r
-let (+++) = Univ.ContextSet.union
-
let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let lab,idl = match idl with
| [] -> assert false
@@ -173,10 +171,10 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
| Abstract ->
let mtb_old = module_type_of_module old in
let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
- Univ.ContextSet.add_constraints chk_cst old.mod_constraints
+ chk_cst
| Algebraic (NoFunctor (MEident(mp'))) ->
check_modpath_equiv env' mp1 mp';
- old.mod_constraints
+ Univ.Constraint.empty
| _ -> error_generative_module_expected lab
in
let mp' = MPdot (mp,lab) in
@@ -185,7 +183,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
{ new_mb with
mod_mp = mp';
mod_expr = Algebraic (NoFunctor (MEident mp1));
- mod_constraints = cst }
+ }
in
let new_equiv = add_delta_resolver equiv new_mb.mod_delta in
(* we propagate the new equality in the rest of the signature
@@ -219,7 +217,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
| Algebraic (NoFunctor (MEident mp0)) ->
let mpnew = rebuild_mp mp0 idl in
check_modpath_equiv env' mpnew mp;
- before@(lab,spec)::after, equiv, Univ.ContextSet.empty
+ before@(lab,spec)::after, equiv, Univ.Constraint.empty
| _ -> error_generative_module_expected lab
end
with
@@ -231,11 +229,11 @@ let check_with env mp (sign,alg,reso,cst) = function
let struc = destr_nofunctor sign in
let struc', c', cst' = check_with_def env struc (idl, (c, ctx)) mp reso in
let wd' = WithDef (idl, (c', ctx)) in
- NoFunctor struc', MEwith (alg,wd'), reso, Univ.ContextSet.add_constraints cst' cst
+ NoFunctor struc', MEwith (alg,wd'), reso, Univ.Constraint.union cst' cst
|WithMod(idl,mp1) as wd ->
let struc = destr_nofunctor sign in
let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
- NoFunctor struc', MEwith (alg,wd), reso', cst+++cst'
+ NoFunctor struc', MEwith (alg,wd), reso', Univ.Constraint.union cst' cst
let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
let farg_id, farg_b, fbody_b = destr_functor sign in
@@ -247,7 +245,7 @@ let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
let body = subst_signature subst fbody_b in
let alg' = mkalg alg mp1 in
let reso' = subst_codom_delta_resolver subst reso in
- body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
+ body,alg',reso', Univ.Constraint.union cst2 cst1
(** Translation of a module struct entry :
- We translate to a module when a [module_path] is given,
@@ -266,7 +264,7 @@ let rec translate_mse env mpo inl = function
let mt = lookup_modtype mp1 env in
module_body_of_type mt.mod_mp mt
in
- mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty
+ mb.mod_type, me, mb.mod_delta, Univ.Constraint.empty
|MEapply (fe,mp1) ->
translate_apply env inl (translate_mse env mpo inl fe) mp1 mk_alg_app
|MEwith(me, with_decl) ->
@@ -274,17 +272,16 @@ let rec translate_mse env mpo inl = function
let mp = mp_from_mexpr me in
check_with env mp (translate_mse env None inl me) with_decl
-let mk_mod mp e ty cst reso =
+let mk_mod mp e ty reso =
{ mod_mp = mp;
mod_expr = e;
mod_type = ty;
mod_type_alg = None;
- mod_constraints = cst;
mod_delta = reso;
mod_retroknowledge = ModBodyRK []; }
-let mk_modtype mp ty cst reso =
- let mb = mk_mod mp Abstract ty cst reso in
+let mk_modtype mp ty reso =
+ let mb = mk_mod mp Abstract ty reso in
{ mb with mod_expr = (); mod_retroknowledge = ModTypeRK }
let rec translate_mse_funct env mpo inl mse = function
@@ -293,45 +290,45 @@ let rec translate_mse_funct env mpo inl mse = function
sign, NoFunctor alg, reso, cst
|(mbid, ty) :: params ->
let mp_id = MPbound mbid in
- let mtb = translate_modtype env mp_id inl ([],ty) in
+ let mtb, cst = translate_modtype env mp_id inl ([],ty) in
let env' = add_module_type mp_id mtb env in
- let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in
+ let sign,alg,reso,cst' = translate_mse_funct env' mpo inl mse params in
let alg' = MoreFunctor (mbid,mtb,alg) in
- MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.mod_constraints
+ MoreFunctor (mbid, mtb, sign), alg',reso, Univ.Constraint.union cst cst'
and translate_modtype env mp inl (params,mte) =
let sign,alg,reso,cst = translate_mse_funct env None inl mte params in
- let mtb = mk_modtype (mp_from_mexpr mte) sign cst reso in
+ let mtb = mk_modtype (mp_from_mexpr mte) sign reso in
let mtb' = subst_modtype_and_resolver mtb mp in
- { mtb' with mod_type_alg = Some alg }
+ { mtb' with mod_type_alg = Some alg }, cst
(** [finalize_module] :
from an already-translated (or interactive) implementation and
an (optional) signature entry, produces a final [module_body] *)
-let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
- |None ->
+let finalize_module env mp (sign,alg,reso,cst1) restype = match restype with
+ | None ->
let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
- mk_mod mp impl sign cst reso
- |Some (params_mte,inl) ->
- let res_mtb = translate_modtype env mp inl params_mte in
- let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in
- let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in
+ mk_mod mp impl sign reso, cst1
+ | Some (params_mte,inl) ->
+ let res_mtb, cst2 = translate_modtype env mp inl params_mte in
+ let auto_mtb = mk_modtype mp sign reso in
+ let cst3 = Subtyping.check_subtypes env auto_mtb res_mtb in
let impl = match alg with Some e -> Algebraic e | None -> Struct sign in
{ res_mtb with
mod_mp = mp;
mod_expr = impl;
mod_retroknowledge = ModBodyRK [];
- (** cst from module body typing,
- cst' from subtyping,
- constraints from module type. *)
- mod_constraints =
- Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
+ },
+ (** cst from module body typing,
+ cst' from subtyping,
+ constraints from module type. *)
+ Univ.Constraint.(union cst1 (union cst2 cst3))
let translate_module env mp inl = function
|MType (params,ty) ->
- let mtb = translate_modtype env mp inl (params,ty) in
- module_body_of_type mp mtb
+ let mtb, cst = translate_modtype env mp inl (params,ty) in
+ module_body_of_type mp mtb, cst
|MExpr (params,mse,oty) ->
let (sg,alg,reso,cst) = translate_mse_funct env (Some mp) inl mse params in
let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
@@ -364,7 +361,7 @@ let rec translate_mse_inclmod env mp inl = function
|MEident mp1 ->
let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
let sign = clean_bounded_mod_expr mb.mod_type in
- sign,(),mb.mod_delta,Univ.ContextSet.empty
+ sign,(),mb.mod_delta,Univ.Constraint.empty
|MEapply (fe,arg) ->
let ftrans = translate_mse_inclmod env mp inl fe in
translate_apply env inl ftrans arg (fun _ _ -> ())
@@ -375,6 +372,6 @@ let translate_mse_incl is_mod env mp inl me =
let () = forbid_incl_signed_functor env me in
translate_mse_inclmod env mp inl me
else
- let mtb = translate_modtype env mp inl ([],me) in
+ let mtb, cst = translate_modtype env mp inl ([],me) in
let sign = clean_bounded_mod_expr mtb.mod_type in
- sign,(),mtb.mod_delta,mtb.mod_constraints
+ sign, (), mtb.mod_delta, cst
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index fd5421aefe..94a4b17df3 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -23,13 +23,13 @@ open Names
*)
val translate_module :
- env -> ModPath.t -> inline -> module_entry -> module_body
+ env -> ModPath.t -> inline -> module_entry -> module_body * Univ.Constraint.t
(** [translate_modtype] produces a [module_type_body] whose [mod_type_alg]
cannot be [None] (and of course [mod_expr] is [Abstract]). *)
val translate_modtype :
- env -> ModPath.t -> inline -> module_type_entry -> module_type_body
+ env -> ModPath.t -> inline -> module_type_entry -> module_type_body * Univ.Constraint.t
(** Low-level function for translating a module struct entry :
- We translate to a module when a [ModPath.t] is given,
@@ -39,7 +39,7 @@ val translate_modtype :
the extraction. *)
type 'alg translation =
- module_signature * 'alg * delta_resolver * Univ.ContextSet.t
+ module_signature * 'alg * delta_resolver * Univ.Constraint.t
val translate_mse :
env -> ModPath.t option -> inline -> module_struct_entry ->
@@ -51,7 +51,7 @@ val translate_mse :
val finalize_module :
env -> ModPath.t -> (module_expression option) translation ->
(module_type_entry * inline) option ->
- module_body
+ module_body * Univ.Constraint.t
(** [translate_mse_incl] translate the mse of a module or
module type given to an Include *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 301af328e4..77ef38dfd5 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -225,8 +225,7 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body ->
&& retro==retro' && delta'==mb.mod_delta
then mb
else
- { mb with
- mod_mp = mp';
+ { mod_mp = mp';
mod_expr = me';
mod_type = ty';
mod_type_alg = aty';
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 9ed0f6f411..02ee501f5f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -474,7 +474,7 @@ let rec lambda_of_constr cache env sigma c =
| Evar (evk,args as ev) ->
(match evar_value sigma ev with
| None ->
- let args = Array.map (lambda_of_constr cache env sigma) args in
+ let args = Array.map_of_list (fun c -> lambda_of_constr cache env sigma c) args in
Levar(evk, args)
| Some t -> lambda_of_constr cache env sigma t)
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index dde1274152..494282d4e1 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -37,7 +37,7 @@ let ( / ) = Filename.concat
let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "")
let () = at_exit (fun () ->
- if Lazy.is_val my_temp_dir then
+ if not !Flags.debug && Lazy.is_val my_temp_dir then
try
let d = Lazy.force my_temp_dir in
Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d);
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 6cfe44c5ff..a5fcfae1fc 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -96,14 +96,14 @@ let mk_accu (a : atom) : t =
else
let data = { data with acc_arg = x :: data.acc_arg } in
let ans = Obj.repr (accumulate data) in
- let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in
+ let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] in
ans
in
let acc = { acc_atm = a; acc_arg = [] } in
let ans = Obj.repr (accumulate acc) in
(** FIXME: use another representation for accumulators, this causes naked
pointers. *)
- let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in
+ let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] in
(Obj.obj ans : t)
let get_accu (k : accumulator) =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7574d7b21e..4ff90dd70d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -367,9 +367,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let el1 = el_stack lft1 v1 in
let el2 = el_stack lft2 v2 in
let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
- convert_vect l2r infos el1 el2
- (Array.map (mk_clos env1) args1)
- (Array.map (mk_clos env2) args2) cuniv
+ convert_list l2r infos el1 el2
+ (List.map (mk_clos env1) args1)
+ (List.map (mk_clos env2) args2) cuniv
else raise NotConvertible
(* 2 index known to be bound to no constant *)
@@ -702,6 +702,13 @@ and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv =
in
Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv
+and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
+| [], [] -> cuniv
+| c1 :: v1, c2 :: v2 ->
+ let cuniv = ccnv CONV l2r infos lft1 lft2 c1 c2 cuniv in
+ convert_list l2r infos lft1 lft2 v1 v2 cuniv
+| _, _ -> raise NotConvertible
+
let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
let infos = create_clos_infos ~evars reds env in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 181ec4860c..93337fca5d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -113,11 +113,23 @@ type library_info = DirPath.t * vodigest
(** Functor and funsig parameters, most recent first *)
type module_parameters = (MBId.t * module_type_body) list
+type compiled_library = {
+ comp_name : DirPath.t;
+ comp_mod : module_body;
+ comp_univs : Univ.ContextSet.t;
+ comp_deps : library_info array;
+ comp_enga : engagement;
+ comp_natsymbs : Nativevalues.symbols
+}
+
+type reimport = compiled_library * Univ.ContextSet.t * vodigest
+
(** Part of the safe_env at a section opening time to be backtracked *)
type section_data = {
rev_env : Environ.env;
rev_univ : Univ.ContextSet.t;
rev_objlabels : Label.Set.t;
+ rev_reimport : reimport list;
}
type safe_environment =
@@ -232,8 +244,6 @@ let set_native_compiler b senv =
let flags = Environ.typing_flags senv.env in
set_typing_flags { flags with enable_native_compiler = b } senv
-let make_sprop_cumulative senv = { senv with env = Environ.make_sprop_cumulative senv.env }
-
let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env }
(** Check that the engagement [c] expected by a library matches
@@ -301,6 +311,7 @@ sig
type t
val repr : t -> side_effect list
val empty : t
+ val is_empty : t -> bool
val add : side_effect -> t -> t
val concat : t -> t -> t
end =
@@ -319,6 +330,7 @@ type t = { seff : side_effect list; elts : SeffSet.t }
let repr eff = eff.seff
let empty = { seff = []; elts = SeffSet.empty }
+let is_empty { seff; elts } = List.is_empty seff && SeffSet.is_empty elts
let add x es =
if SeffSet.mem x es.elts then es
else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
@@ -349,6 +361,7 @@ let push_private_constants env eff =
List.fold_left add_if_undefined env eff
let empty_private_constants = SideEffects.empty
+let is_empty_private_constants c = SideEffects.is_empty c
let concat_private = SideEffects.concat
let universes_of_private eff =
@@ -552,8 +565,7 @@ let constraints_of_sfb sfb =
match sfb with
| SFBconst cb -> globalize_constant_universes cb
| SFBmind mib -> globalize_mind_universes mib
- | SFBmodtype mtb -> [mtb.mod_constraints]
- | SFBmodule mb -> [mb.mod_constraints]
+ | SFBmodtype _ | SFBmodule _ -> []
let add_retroknowledge pttc senv =
{ senv with
@@ -972,103 +984,35 @@ let add_mind l mie senv =
let add_modtype l params_mte inl senv =
let mp = MPdot(senv.modpath, l) in
- let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte in
+ let mtb, cst = Mod_typing.translate_modtype senv.env mp inl params_mte in
+ let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
let mtb = Declareops.hcons_module_type mtb in
- let senv' = add_field (l,SFBmodtype mtb) MT senv in
- mp, senv'
+ let senv = add_field (l,SFBmodtype mtb) MT senv in
+ mp, senv
(** full_add_module adds module with universes and constraints *)
let full_add_module mb senv =
- let senv = add_constraints (Now mb.mod_constraints) senv in
let dp = ModPath.dp mb.mod_mp in
let linkinfo = Nativecode.link_info_of_dirpath dp in
{ senv with env = Modops.add_linked_module mb linkinfo senv.env }
let full_add_module_type mp mt senv =
- let senv = add_constraints (Now mt.mod_constraints) senv in
{ senv with env = Modops.add_module_type mp mt senv.env }
(** Insertion of modules *)
let add_module l me inl senv =
let mp = MPdot(senv.modpath, l) in
- let mb = Mod_typing.translate_module senv.env mp inl me in
+ let mb, cst = Mod_typing.translate_module senv.env mp inl me in
+ let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
let mb = Declareops.hcons_module_body mb in
- let senv' = add_field (l,SFBmodule mb) M senv in
- let senv'' =
- if Modops.is_functor mb.mod_type then senv'
- else update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv'
- in
- (mp,mb.mod_delta),senv''
-
-(** {6 Interactive sections *)
-
-let open_section senv =
- let custom = {
- rev_env = senv.env;
- rev_univ = senv.univ;
- rev_objlabels = senv.objlabels;
- } in
- let sections = Section.open_section ~custom senv.sections in
- { senv with sections=Some sections }
-
-let close_section senv =
- let open Section in
- let sections0 = get_section senv.sections in
- let env0 = senv.env in
- (* First phase: revert the declarations added in the section *)
- let sections, entries, cstrs, revert = Section.close_section sections0 in
- let rec pop_revstruct accu entries revstruct = match entries, revstruct with
- | [], revstruct -> accu, revstruct
- | _ :: _, [] ->
- CErrors.anomaly (Pp.str "Unmatched section data")
- | entry :: entries, (lbl, leaf) :: revstruct ->
- let data = match entry, leaf with
- | SecDefinition kn, SFBconst cb ->
- let () = assert (Label.equal lbl (Constant.label kn)) in
- `Definition (kn, cb)
- | SecInductive ind, SFBmind mib ->
- let () = assert (Label.equal lbl (MutInd.label ind)) in
- `Inductive (ind, mib)
- | (SecDefinition _ | SecInductive _), (SFBconst _ | SFBmind _) ->
- CErrors.anomaly (Pp.str "Section content mismatch")
- | (SecDefinition _ | SecInductive _), (SFBmodule _ | SFBmodtype _) ->
- CErrors.anomaly (Pp.str "Module inside a section")
- in
- pop_revstruct (data :: accu) entries revstruct
- in
- let redo, revstruct = pop_revstruct [] entries senv.revstruct in
- (* Don't revert the delayed constraints. If some delayed constraints were
- forced inside the section, they have been turned into global monomorphic
- that are going to be replayed. Those that are not forced are not readded
- by {!add_constant_aux}. *)
- let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels } = revert in
- (* Do not revert the opaque table, the discharged opaque constants are
- referring to it. *)
- let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) in
- let senv = { senv with env; revstruct; sections; univ; objlabels; } in
- (* Second phase: replay the discharged section contents *)
- let senv = push_context_set ~strict:true cstrs senv in
- let modlist = Section.replacement_context env0 sections0 in
- let cooking_info seg =
- let { abstr_ctx; abstr_subst; abstr_uctx } = seg in
- let abstract = (abstr_ctx, abstr_subst, abstr_uctx) in
- { Opaqueproof.modlist; abstract }
- in
- let fold senv = function
- | `Definition (kn, cb) ->
- let info = cooking_info (Section.segment_of_constant env0 kn sections0) in
- let r = { Cooking.from = cb; info } in
- let cb = Term_typing.translate_recipe senv.env kn r in
- (* Delayed constants are already in the global environment *)
- add_constant_aux senv (kn, cb)
- | `Inductive (ind, mib) ->
- let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
- let mib = Cooking.cook_inductive info mib in
- add_checked_mind ind mib senv
+ let senv = add_field (l,SFBmodule mb) M senv in
+ let senv =
+ if Modops.is_functor mb.mod_type then senv
+ else update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv
in
- List.fold_left fold senv redo
+ (mp,mb.mod_delta),senv
(** {6 Starting / ending interactive modules and module types } *)
@@ -1100,7 +1044,8 @@ let start_modtype l senv =
let add_module_parameter mbid mte inl senv =
let () = check_empty_struct senv in
let mp = MPbound mbid in
- let mtb = Mod_typing.translate_modtype senv.env mp inl ([],mte) in
+ let mtb, cst = Mod_typing.translate_modtype senv.env mp inl ([],mte) in
+ let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
let senv = full_add_module_type mp mtb senv in
let new_variant = match senv.modvariant with
| STRUCT (params,oldenv) -> STRUCT ((mbid,mtb) :: params, oldenv)
@@ -1138,12 +1083,12 @@ let functorize_module params mb =
let build_module_body params restype senv =
let struc = NoFunctor (List.rev senv.revstruct) in
let restype' = Option.map (fun (ty,inl) -> (([],ty),inl)) restype in
- let mb =
+ let mb, cst =
Mod_typing.finalize_module senv.env senv.modpath
- (struc,None,senv.modresolver,senv.univ) restype'
+ (struc,None,senv.modresolver,Univ.Constraint.empty) restype'
in
let mb' = functorize_module params mb in
- { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge }
+ { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge }, cst
(** Returning back to the old pre-interactive-module environment,
with one extra component and some updated fields
@@ -1183,15 +1128,13 @@ let end_module l restype senv =
let () = check_current_label l mp in
let () = check_empty_context senv in
let mbids = List.rev_map fst params in
- let mb = build_module_body params restype senv in
+ let mb, cst = build_module_body params restype senv in
+ let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in
let newenv = set_engagement_opt newenv senv.engagement in
- let senv'=
- propagate_loads { senv with
- env = newenv;
- univ = Univ.ContextSet.union senv.univ mb.mod_constraints} in
- let newenv = Environ.push_context_set ~strict:true mb.mod_constraints senv'.env in
+ let newenv = Environ.set_universes (Environ.universes senv.env) newenv in
+ let senv' = propagate_loads { senv with env = newenv } in
let newenv = Modops.add_module mb newenv in
let newresolver =
if Modops.is_functor mb.mod_type then oldsenv.modresolver
@@ -1200,12 +1143,11 @@ let end_module l restype senv =
(mp,mbids,mb.mod_delta),
propagate_senv (l,SFBmodule mb) newenv newresolver senv' oldsenv
-let build_mtb mp sign cst delta =
+let build_mtb mp sign delta =
{ mod_mp = mp;
mod_expr = ();
mod_type = sign;
mod_type_alg = None;
- mod_constraints = cst;
mod_delta = delta;
mod_retroknowledge = ModTypeRK }
@@ -1217,11 +1159,11 @@ let end_modtype l senv =
let mbids = List.rev_map fst params in
let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in
- let newenv = Environ.push_context_set ~strict:true senv.univ newenv in
let newenv = set_engagement_opt newenv senv.engagement in
+ let newenv = Environ.set_universes (Environ.universes senv.env) newenv in
let senv' = propagate_loads {senv with env=newenv} in
let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in
- let mtb = build_mtb mp auto_tb senv'.univ senv.modresolver in
+ let mtb = build_mtb mp auto_tb senv.modresolver in
let newenv = Environ.add_modtype mtb senv'.env in
let newresolver = oldsenv.modresolver in
(mp,mbids),
@@ -1235,7 +1177,7 @@ let add_include me is_module inl senv =
let sign,(),resolver,cst =
translate_mse_incl is_module senv.env mp_sup inl me
in
- let senv = add_constraints (Now cst) senv in
+ let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
(* Include Self support *)
let rec compute_sign sign mb resolver senv =
match sign with
@@ -1255,7 +1197,7 @@ let add_include me is_module inl senv =
in
let resolver,str,senv =
let struc = NoFunctor (List.rev senv.revstruct) in
- let mtb = build_mtb mp_sup struc Univ.ContextSet.empty senv.modresolver in
+ let mtb = build_mtb mp_sup struc senv.modresolver in
compute_sign sign mtb resolver senv
in
let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv
@@ -1275,16 +1217,10 @@ let add_include me is_module inl senv =
(** {6 Libraries, i.e. compiled modules } *)
-type compiled_library = {
- comp_name : DirPath.t;
- comp_mod : module_body;
- comp_deps : library_info array;
- comp_enga : engagement;
- comp_natsymbs : Nativevalues.symbols
-}
-
let module_of_library lib = lib.comp_mod
+let univs_of_library lib = lib.comp_univs
+
type native_library = Nativecode.global list
(** FIXME: MS: remove?*)
@@ -1313,7 +1249,6 @@ let export ?except ~output_native_objects senv dir =
mod_expr = FullStruct;
mod_type = str;
mod_type_alg = None;
- mod_constraints = senv.univ;
mod_delta = senv.modresolver;
mod_retroknowledge = ModBodyRK senv.local_retroknowledge
}
@@ -1326,6 +1261,7 @@ let export ?except ~output_native_objects senv dir =
let lib = {
comp_name = dir;
comp_mod = mb;
+ comp_univs = senv.univ;
comp_deps = Array.of_list (DPmap.bindings senv.required);
comp_enga = Environ.engagement senv.env;
comp_natsymbs = symbols }
@@ -1333,7 +1269,7 @@ let export ?except ~output_native_objects senv dir =
mp, lib, ast
(* cst are the constraints that were computed by the vi2vo step and hence are
- * not part of the mb.mod_constraints field (but morally should be) *)
+ * not part of the [lib.comp_univs] field (but morally should be) *)
let import lib cst vodigest senv =
check_required senv.required lib.comp_deps;
check_engagement senv.env lib.comp_enga;
@@ -1343,22 +1279,101 @@ let import lib cst vodigest senv =
let mp = MPfile lib.comp_name in
let mb = lib.comp_mod in
let env = Environ.push_context_set ~strict:true
- (Univ.ContextSet.union mb.mod_constraints cst)
- senv.env
+ (Univ.ContextSet.union lib.comp_univs cst)
+ senv.env
in
let env =
let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in
Modops.add_linked_module mb linkinfo env
in
let env = Environ.add_native_symbols lib.comp_name lib.comp_natsymbs env in
+ let sections =
+ Option.map (Section.map_custom (fun custom ->
+ {custom with rev_reimport = (lib,cst,vodigest) :: custom.rev_reimport}))
+ senv.sections
+ in
mp,
{ senv with
env;
modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
required = DPmap.add lib.comp_name vodigest senv.required;
loads = (mp,mb)::senv.loads;
+ sections;
}
+(** {6 Interactive sections *)
+
+let open_section senv =
+ let custom = {
+ rev_env = senv.env;
+ rev_univ = senv.univ;
+ rev_objlabels = senv.objlabels;
+ rev_reimport = [];
+ } in
+ let sections = Section.open_section ~custom senv.sections in
+ { senv with sections=Some sections }
+
+let close_section senv =
+ let open Section in
+ let sections0 = get_section senv.sections in
+ let env0 = senv.env in
+ (* First phase: revert the declarations added in the section *)
+ let sections, entries, cstrs, revert = Section.close_section sections0 in
+ let rec pop_revstruct accu entries revstruct = match entries, revstruct with
+ | [], revstruct -> accu, revstruct
+ | _ :: _, [] ->
+ CErrors.anomaly (Pp.str "Unmatched section data")
+ | entry :: entries, (lbl, leaf) :: revstruct ->
+ let data = match entry, leaf with
+ | SecDefinition kn, SFBconst cb ->
+ let () = assert (Label.equal lbl (Constant.label kn)) in
+ `Definition (kn, cb)
+ | SecInductive ind, SFBmind mib ->
+ let () = assert (Label.equal lbl (MutInd.label ind)) in
+ `Inductive (ind, mib)
+ | (SecDefinition _ | SecInductive _), (SFBconst _ | SFBmind _) ->
+ CErrors.anomaly (Pp.str "Section content mismatch")
+ | (SecDefinition _ | SecInductive _), (SFBmodule _ | SFBmodtype _) ->
+ CErrors.anomaly (Pp.str "Module inside a section")
+ in
+ pop_revstruct (data :: accu) entries revstruct
+ in
+ let redo, revstruct = pop_revstruct [] entries senv.revstruct in
+ (* Don't revert the delayed constraints. If some delayed constraints were
+ forced inside the section, they have been turned into global monomorphic
+ that are going to be replayed. Those that are not forced are not readded
+ by {!add_constant_aux}. *)
+ let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels; rev_reimport } = revert in
+ (* Do not revert the opaque table, the discharged opaque constants are
+ referring to it. *)
+ let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) in
+ let senv = { senv with env; revstruct; sections; univ; objlabels; } in
+ (* Second phase: replay Requires *)
+ let senv = List.fold_left (fun senv (lib,cst,vodigest) -> snd (import lib cst vodigest senv))
+ senv (List.rev rev_reimport)
+ in
+ (* Third phase: replay the discharged section contents *)
+ let senv = push_context_set ~strict:true cstrs senv in
+ let modlist = Section.replacement_context env0 sections0 in
+ let cooking_info seg =
+ let { abstr_ctx; abstr_subst; abstr_uctx } = seg in
+ let abstract = (abstr_ctx, abstr_subst, abstr_uctx) in
+ { Opaqueproof.modlist; abstract }
+ in
+ let fold senv = function
+ | `Definition (kn, cb) ->
+ let info = cooking_info (Section.segment_of_constant env0 kn sections0) in
+ let r = { Cooking.from = cb; info } in
+ let cb = Term_typing.translate_recipe senv.env kn r in
+ (* Delayed constants are already in the global environment *)
+ add_constant_aux senv (kn, cb)
+ | `Inductive (ind, mib) ->
+ let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
+ let mib = Cooking.cook_inductive info mib in
+ add_checked_mind ind mib senv
+ in
+ List.fold_left fold senv redo
+
(** {6 Safe typing } *)
type judgment = Environ.unsafe_judgment
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index f8d5d319a9..b601279e87 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -50,6 +50,8 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
type private_constants
val empty_private_constants : private_constants
+val is_empty_private_constants : private_constants -> bool
+
val concat_private : private_constants -> private_constants -> private_constants
(** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
[e1] must be more recent than those of [e2]. *)
@@ -133,7 +135,6 @@ val set_check_positive : bool -> safe_transformer0
val set_check_universes : bool -> safe_transformer0
val set_VM : bool -> safe_transformer0
val set_native_compiler : bool -> safe_transformer0
-val make_sprop_cumulative : safe_transformer0
val set_allow_sprop : bool -> safe_transformer0
val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
@@ -193,6 +194,7 @@ type compiled_library
type native_library = Nativecode.global list
val module_of_library : compiled_library -> Declarations.module_body
+val univs_of_library : compiled_library -> Univ.ContextSet.t
val start_library : DirPath.t -> ModPath.t safe_transformer
diff --git a/kernel/section.ml b/kernel/section.ml
index 948a967f96..8c36f16799 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -45,6 +45,8 @@ let has_poly_univs sec = sec.has_poly_univs
let all_poly_univs sec = sec.all_poly_univs
+let map_custom f sec = {sec with sec_custom = f sec.sec_custom}
+
let find_emap e (cmap, imap) = match e with
| SecDefinition con -> Cmap.find con cmap
| SecInductive ind -> Mindmap.find ind imap
diff --git a/kernel/section.mli b/kernel/section.mli
index 89739c7da2..2ebb4564b3 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -19,6 +19,9 @@ type 'a t
val depth : 'a t -> int
(** Number of nested sections. *)
+val map_custom : ('a -> 'a) -> 'a t -> 'a t
+(** Modify the custom data *)
+
(** {6 Manipulating sections} *)
type section_entry =
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 466fbacca4..3a89b73bd5 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -12,6 +12,8 @@ open Univ
type family = InSProp | InProp | InSet | InType
+let all_families = [InSProp; InProp; InSet; InType]
+
type t =
| SProp
| Prop
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 49549e224d..fe939b1d95 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -12,6 +12,8 @@
type family = InSProp | InProp | InSet | InType
+val all_families : family list
+
type t = private
| SProp
| Prop
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 3f81a62956..28baa82666 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -336,7 +336,6 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
mod_expr = Abstract;
mod_type = subst_signature subst1 body_t1;
mod_type_alg = None;
- mod_constraints = mtb1.mod_constraints;
mod_retroknowledge = ModBodyRK [];
mod_delta = mtb1.mod_delta} env
in
@@ -347,7 +346,6 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
let check_subtypes env sup super =
let env = add_module_type sup.mod_mp sup env in
- let env = Environ.push_context_set ~strict:true super.mod_constraints env in
check_modtypes Univ.Constraint.empty env
(strengthen sup sup.mod_mp) super empty_subst
(map_mp super.mod_mp sup.mod_mp sup.mod_delta) false
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 449cd0f0f9..5f5f0ef8cd 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -37,7 +37,7 @@ let g_map f g =
if g.graph == g' then g
else {g with graph=g'}
-let make_sprop_cumulative g = {g with sprop_cumulative=true}
+let set_cumulative_sprop b g = {g with sprop_cumulative=b}
let check_smaller_expr g (u,n) (v,m) =
let diff = n - m in
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 8a8c09e911..8d9afb0990 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -13,8 +13,8 @@ open Univ
(** {6 Graphs of universes. } *)
type t
-val make_sprop_cumulative : t -> t
-(** Don't use this in the kernel, it makes the system incomplete. *)
+val set_cumulative_sprop : bool -> t -> t
+(** Makes the system incomplete. *)
type 'a check_function = t -> 'a -> 'a -> bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 14:06:25 +0000