From e7ffa1bfa25300a25c1e81583b77d2d7587bbb5d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 31 May 2019 14:27:36 +0200 Subject: Do not substitute opaque constants when discharging. Instead we do that on a by-need basis by reusing the section info already stored in the opaque proof. --- checker/check.ml | 15 ++++++++++++--- checker/mod_checking.ml | 12 ++++++------ checker/mod_checking.mli | 2 +- checker/values.ml | 20 ++++++++++++++++++-- 4 files changed, 37 insertions(+), 12 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index c5bc59e72a..747d7c43a1 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -51,7 +51,7 @@ let pr_path sp = type compilation_unit_name = DirPath.t type seg_univ = Univ.ContextSet.t * bool -type seg_proofs = Constr.constr option array +type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr) option array type library_t = { library_name : compilation_unit_name; @@ -98,9 +98,18 @@ let access_opaque_table dp i = with Not_found -> assert false in assert (i < Array.length t); - t.(i) + match t.(i) with + | None -> None + | Some (info, n, c) -> Some (Cooking.cook_constr info n c) -let () = Mod_checking.set_indirect_accessor access_opaque_table +let access_discharge = Cooking.cook_constr + +let indirect_accessor = { + Opaqueproof.access_proof = access_opaque_table; + Opaqueproof.access_discharge = access_discharge; +} + +let () = Mod_checking.set_indirect_accessor indirect_accessor let check_one_lib admit senv (dir,m) = let md = m.library_compiled in diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index ccce0bd9a7..0684623a81 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -8,13 +8,13 @@ open Environ (** {6 Checking constants } *) -let get_proof = ref (fun _ _ -> assert false) -let set_indirect_accessor f = get_proof := f - -let indirect_accessor = { - Opaqueproof.access_proof = (fun dp n -> !get_proof dp n); +let indirect_accessor = ref { + Opaqueproof.access_proof = (fun _ _ -> assert false); + Opaqueproof.access_discharge = (fun _ _ _ -> assert false); } +let set_indirect_accessor f = indirect_accessor := f + let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn); (* Locally set the oracle for further typechecking *) @@ -40,7 +40,7 @@ let check_constant_declaration env kn cb = let body = match cb.const_body with | Undef _ | Primitive _ -> None | Def c -> Some (Mod_subst.force_constr c) - | OpaqueDef o -> Some (Opaqueproof.force_proof indirect_accessor otab o) + | OpaqueDef o -> Some (Opaqueproof.force_proof !indirect_accessor otab o) in let () = match body with diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli index dbc81c8507..7aa1f837a0 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -8,6 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val set_indirect_accessor : (Names.DirPath.t -> int -> Constr.t option) -> unit +val set_indirect_accessor : Opaqueproof.indirect_accessor -> unit val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit diff --git a/checker/values.ml b/checker/values.ml index 031f05dd6b..6dbf281f49 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -131,7 +131,7 @@ let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|] let rec v_constr = Sum ("constr",0,[| [|Int|]; (* Rel *) - [|Fail "Var"|]; (* Var *) + [|v_id|]; (* Var *) [|Fail "Meta"|]; (* Meta *) [|Fail "Evar"|]; (* Evar *) [|v_sort|]; (* Sort *) @@ -383,6 +383,22 @@ let v_libsum = let v_lib = Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) -let v_opaques = Array (Opt v_constr) +let v_ndecl = v_sum "named_declaration" 0 + [| [|v_binder_annot v_id; v_constr|]; (* LocalAssum *) + [|v_binder_annot v_id; v_constr; v_constr|] |] (* LocalDef *) + +let v_nctxt = List v_ndecl + +let v_work_list = + let v_abstr = v_pair v_instance (Array v_id) in + Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|]) + +let v_abstract = + Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |]) + +let v_cooking_info = + Tuple ("cooking_info", [|v_work_list; v_abstract|]) + +let v_opaques = Array (Opt (Tuple ("opaque", [| List v_cooking_info; Int; v_constr |]))) let v_univopaques = Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) -- cgit v1.2.3 From 0f54a91eac98baf076d8be8f52bccdb1de17ea46 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jun 2019 10:19:02 +0200 Subject: Slightly tweak the representation of dischargeable opaque proofs. This will allow an easier removal of the discharge segment in a later commit. --- checker/check.ml | 7 ++++--- checker/values.ml | 2 +- 2 files changed, 5 insertions(+), 4 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 747d7c43a1..030b605e3f 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -51,7 +51,7 @@ let pr_path sp = type compilation_unit_name = DirPath.t type seg_univ = Univ.ContextSet.t * bool -type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr) option array +type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr option) array type library_t = { library_name : compilation_unit_name; @@ -98,9 +98,10 @@ let access_opaque_table dp i = with Not_found -> assert false in assert (i < Array.length t); - match t.(i) with + let (info, n, c) = t.(i) in + match c with | None -> None - | Some (info, n, c) -> Some (Cooking.cook_constr info n c) + | Some c -> Some (Cooking.cook_constr info n c) let access_discharge = Cooking.cook_constr diff --git a/checker/values.ml b/checker/values.ml index 6dbf281f49..4a4c8d803c 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -399,6 +399,6 @@ let v_abstract = let v_cooking_info = Tuple ("cooking_info", [|v_work_list; v_abstract|]) -let v_opaques = Array (Opt (Tuple ("opaque", [| List v_cooking_info; Int; v_constr |]))) +let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt v_constr |])) let v_univopaques = Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) -- cgit v1.2.3 From 1cdfb1f9270e399a784b346c3f8d6abbc4477552 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jun 2019 10:35:14 +0200 Subject: Remove the discharge segment from vo files. Since the introduction of delayed section substitution, the opaque table was already containing the same information. --- checker/check.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 030b605e3f..903258daef 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -337,7 +337,6 @@ let intern_from_file ~intern_mode (dir, f) = let (sd:summary_disk), _, digest = marshal_in_segment f ch in let (md:library_disk), _, digest = marshal_in_segment f ch in let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in - let (discharging:'a option), _, _ = marshal_in_segment f ch in let (tasks:'a option), _, _ = marshal_in_segment f ch in let (table:seg_proofs option), pos, checksum = marshal_or_skip ~intern_mode f ch in @@ -350,7 +349,7 @@ let intern_from_file ~intern_mode (dir, f) = if dir <> sd.md_name then user_err ~hdr:"intern_from_file" (name_clash_message dir sd.md_name f); - if tasks <> None || discharging <> None then + if tasks <> None then user_err ~hdr:"intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin -- cgit v1.2.3