aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml28
-rw-r--r--checker/cic.mli15
-rw-r--r--checker/declarations.ml13
-rw-r--r--checker/declarations.mli2
-rw-r--r--checker/mod_checking.ml3
-rw-r--r--checker/values.ml7
-rw-r--r--checker/votour.ml50
7 files changed, 79 insertions, 39 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 5a1671fe6..85324ec44 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -81,6 +81,7 @@ let register_loaded_library m =
(* Map from library names to table of opaque terms *)
let opaque_tables = ref LibraryMap.empty
+let opaque_univ_tables = ref LibraryMap.empty
let access_opaque_table dp i =
let t =
@@ -88,9 +89,18 @@ let access_opaque_table dp i =
with Not_found -> assert false
in
assert (i < Array.length t);
- t.(i)
+ Future.force t.(i)
+
+let access_opaque_univ_table dp i =
+ try
+ let t = LibraryMap.find dp !opaque_univ_tables in
+ assert (i < Array.length t);
+ Future.force t.(i)
+ with Not_found -> Univ.empty_constraint
+
let _ = Declarations.indirect_opaque_access := access_opaque_table
+let _ = Declarations.indirect_opaque_univ_access := access_opaque_univ_table
let check_one_lib admit (dir,m) =
let file = m.library_filename in
@@ -298,10 +308,12 @@ let depgraph = ref LibraryMap.empty
let intern_from_file (dir, f) =
Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
- let (md,table,digest) =
+ let (md,table,opaque_csts,digest) =
try
let ch = with_magic_number_check raw_intern_library f in
let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
+ let (opaque_csts:'a option), _, _ = System.marshal_in_segment f ch in
+ let (discharging:'a option), _, _ = System.marshal_in_segment f ch in
let (tasks:'a option), _, _ = System.marshal_in_segment f ch in
let (table:Cic.opaque_table), pos, checksum =
System.marshal_in_segment f ch in
@@ -314,17 +326,25 @@ let intern_from_file (dir, f) =
if dir <> md.md_name then
errorlabstrm "intern_from_file"
(name_clash_message dir md.md_name f);
- if tasks <> None then
+ if tasks <> None || discharging <> None then
errorlabstrm "intern_from_file"
(str "The file "++str f++str " contains unfinished tasks");
+ if opaque_csts <> None then begin
+ pp (str " (was a vi file) ");
+ Validate.validate !Flags.debug Values.v_univopaques opaque_csts
+ end;
(* Verification of the unmarshalled values *)
Validate.validate !Flags.debug Values.v_lib md;
Validate.validate !Flags.debug Values.v_opaques table;
Flags.if_verbose ppnl (str" done]"); pp_flush ();
- md,table,digest
+ md,table,opaque_csts,digest
with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
opaque_tables := LibraryMap.add md.md_name table !opaque_tables;
+ Option.iter (fun opaque_csts ->
+ opaque_univ_tables :=
+ LibraryMap.add md.md_name opaque_csts !opaque_univ_tables)
+ opaque_csts;
mk_library md f table digest
let get_deps (dir, f) =
diff --git a/checker/cic.mli b/checker/cic.mli
index 93dc84fa5..8e6c5580d 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -182,14 +182,14 @@ type inline = int option
type constant_def =
| Undef of inline
| Def of constr_substituted
- | OpaqueDef of lazy_constr Future.computation
+ | OpaqueDef of lazy_constr
type constant_body = {
const_hyps : section_context; (** New: younger hyp at top *)
const_body : constant_def;
const_type : constant_type;
const_body_code : to_patch_substituted;
- const_constraints : Univ.constraints Future.computation;
+ const_constraints : Univ.constraints;
const_native_name : native_name ref;
const_inline_code : bool }
@@ -387,13 +387,20 @@ type library_disk = {
md_deps : library_deps;
md_imports : compilation_unit_name array }
-type opaque_table = constr array
+type opaque_table = constr Future.computation array
+type univ_table = Univ.constraints Future.computation array option
(** A .vo file is currently made of :
1) a magic number (4 bytes, cf output_binary_int)
2) a marshalled [library_disk] structure
3) a [Digest.t] string (16 bytes)
- 4) a marshalled [opaque_table]
+ 4) a marshalled [univ_table] (* Some if vo was obtained from vi *)
5) a [Digest.t] string (16 bytes)
+ 6) a marshalled [None] discharge_table (* Some in vi files *)
+ 7) a [Digest.t] string (16 bytes)
+ 8) a marshalled [None] todo_table (* Some in vi files *)
+ 9) a [Digest.t] string (16 bytes)
+ 10) a marshalled [opaque_table]
+ 11) a [Digest.t] string (16 bytes)
*)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 97958c2b7..79ba6de22 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -416,24 +416,27 @@ let subst_lazy_constr sub = function
let indirect_opaque_access =
ref ((fun dp i -> assert false) : DirPath.t -> int -> constr)
+let indirect_opaque_univ_access =
+ ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.constraints)
let force_lazy_constr = function
| Indirect (l,dp,i) ->
let c = !indirect_opaque_access dp i in
force_constr (List.fold_right subst_constr_subst l (from_val c))
+let force_lazy_constr_univs = function
+ | OpaqueDef (Indirect (l,dp,i)) -> !indirect_opaque_univ_access dp i
+ | _ -> Univ.empty_constraint
+
let subst_constant_def sub = function
| Undef inl -> Undef inl
| Def c -> Def (subst_constr_subst sub c)
- | OpaqueDef lc ->
- OpaqueDef (Future.from_val (subst_lazy_constr sub (Future.join lc)))
-
-type constant_constraints = Univ.constraints Future.computation
+ | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
let body_of_constant cb = match cb.const_body with
| Undef _ -> None
| Def c -> Some (force_constr c)
- | OpaqueDef c -> Some (force_lazy_constr (Future.join c))
+ | OpaqueDef c -> Some (force_lazy_constr c)
let constant_has_body cb = match cb.const_body with
| Undef _ -> false
diff --git a/checker/declarations.mli b/checker/declarations.mli
index a5785b52a..3c6db6ab7 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -2,9 +2,11 @@ open Names
open Cic
val force_constr : constr_substituted -> constr
+val force_lazy_constr_univs : Cic.constant_def -> Univ.constraints
val from_val : constr -> constr_substituted
val indirect_opaque_access : (DirPath.t -> int -> constr) ref
+val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.constraints) ref
(** Constant_body *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index b0f20da70..c2016ba1b 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -27,6 +27,9 @@ let refresh_arity ar =
let check_constant_declaration env kn cb =
Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn);
(* let env = add_constraints cb.const_constraints env in*)
+ (* Constraints of an opauqe proof are not in the module *)
+ let env =
+ add_constraints (Declarations.force_lazy_constr_univs cb.const_body) env in
(match cb.const_type with
NonPolymorphicType ty ->
let ty, cu = refresh_arity ty in
diff --git a/checker/values.ml b/checker/values.ml
index a047c8005..0a2e53799 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -191,14 +191,14 @@ let v_cst_type =
let v_cst_def =
v_sum "constant_def" 0
- [|[|Opt Int|]; [|v_cstr_subst|]; [|v_computation v_lazy_constr|]|]
+ [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
let v_cb = v_tuple "constant_body"
[|v_section_ctxt;
v_cst_def;
v_cst_type;
Any;
- v_computation v_cstrs;
+ v_cstrs;
v_bool|]
let v_recarg = v_sum "recarg" 1 (* Norec *)
@@ -300,7 +300,8 @@ let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|])
let v_lib =
Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|])
-let v_opaques = Array v_constr
+let v_opaques = Array (v_computation v_constr)
+let v_univopaques = Opt (Array (v_computation v_cstrs))
(** Registering dynamic values *)
diff --git a/checker/votour.ml b/checker/votour.ml
index 2634e8448..136f7d29e 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -152,31 +152,35 @@ let visit_vo f =
"At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
let segments = [|
{name="library"; pos=0; typ=Values.v_lib};
+ {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques};
+ {name="discharging info"; pos=0; typ=Opt Any};
{name="STM tasks"; pos=0; typ=Opt Any};
- {name="opaque proof terms"; pos=0; typ=Values.v_opaques};
+ {name="opaque proofs"; pos=0; typ=Values.v_opaques};
|] in
- let ch = open_in_bin f in
- let magic = input_binary_int ch in
- Printf.printf "File format: %d\n%!" magic;
- for i=0 to Array.length segments - 1 do
- let pos = input_binary_int ch in
- segments.(i).pos <- pos_in ch;
- seek_in ch pos;
- ignore(Digest.input ch);
- done;
- Printf.printf "The file has %d segments, choose the one to visit:\n"
- (Array.length segments);
- Array.iteri (fun i { name; pos } ->
- Printf.printf " %d: %s, starting at byte %d\n" i name pos)
- segments;
- Printf.printf "# %!";
- let l = read_line () in
- let seg = int_of_string l in
- seek_in ch segments.(seg).pos;
- let o = (input_value ch : Obj.t) in
- let () = CObj.register_shared_size o in
- let () = init () in
- visit segments.(seg).typ o []
+ while true do
+ let ch = open_in_bin f in
+ let magic = input_binary_int ch in
+ Printf.printf "File format: %d\n%!" magic;
+ for i=0 to Array.length segments - 1 do
+ let pos = input_binary_int ch in
+ segments.(i).pos <- pos_in ch;
+ seek_in ch pos;
+ ignore(Digest.input ch);
+ done;
+ Printf.printf "The file has %d segments, choose the one to visit:\n"
+ (Array.length segments);
+ Array.iteri (fun i { name; pos } ->
+ Printf.printf " %d: %s, starting at byte %d\n" i name pos)
+ segments;
+ Printf.printf "# %!";
+ let l = read_line () in
+ let seg = int_of_string l in
+ seek_in ch segments.(seg).pos;
+ let o = (input_value ch : Obj.t) in
+ let () = CObj.register_shared_size o in
+ let () = init () in
+ visit segments.(seg).typ o []
+ done
let main =
if not !Sys.interactive then
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 14:56:12 +0000