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.ml2
-rw-r--r--kernel/declareops.ml1
-rw-r--r--kernel/environ.ml17
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/inferCumulativity.ml5
-rw-r--r--kernel/mod_subst.ml2
-rw-r--r--kernel/nativelambda.ml2
-rw-r--r--kernel/nativelib.ml2
-rw-r--r--kernel/nativevalues.ml4
-rw-r--r--kernel/reduction.ml19
-rw-r--r--kernel/safe_typing.ml171
-rw-r--r--kernel/safe_typing.mli3
-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/uGraph.ml2
-rw-r--r--kernel/uGraph.mli4
23 files changed, 185 insertions, 125 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..11d4120d7c 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
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 20dc21900c..b347152c16 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 } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2d2c9a454b..cf01711fe7 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;
@@ -431,7 +431,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 +445,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 +454,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..4195f112ca 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -310,7 +310,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/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 469d5ccaa2..4ff90dd70d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -354,7 +354,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(match kind a1, kind a2 with
| (Sort s1, Sort s2) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
- anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
+ (* May happen because we convert application right to left *)
+ raise NotConvertible;
sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv
| (Meta n, Meta m) ->
if Int.equal n m
@@ -366,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 *)
@@ -471,7 +472,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| (FProd (x1, c1, c2, e), FProd (_, c'1, c'2, e')) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
- anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
+ (* May happen because we convert application right to left *)
+ raise NotConvertible;
(* Luo's system *)
let el1 = el_stack lft1 v1 in
let el2 = el_stack lft2 v2 in
@@ -700,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..9fabb441d1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -113,11 +113,22 @@ 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_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 +243,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 +310,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 +329,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 +360,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 =
@@ -1002,74 +1014,6 @@ let add_module l me inl 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
- in
- List.fold_left fold senv redo
-
(** {6 Starting / ending interactive modules and module types } *)
let start_module l senv =
@@ -1275,14 +1219,6 @@ 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
type native_library = Nativecode.global list
@@ -1351,14 +1287,93 @@ let import lib cst vodigest senv =
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..f5bd27ca12 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
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/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-03-08 01:43:59 +0000