diff options
| author | Pierre-Marie Pédrot | 2019-05-21 19:22:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-24 09:00:10 +0200 |
| commit | d3c931cd8c84d1b7d9d5763e20221d51700f0709 (patch) | |
| tree | 58ca99c4f6007bc66294c41354bb68bf9d71044b /checker | |
| parent | 2fa3dc389a58ca4a390b99995d82e6c089add163 (diff) | |
Remove the indirect opaque accessor hooks from Opaqueproof.
We simply pass them as arguments, now that they are not called by the
kernel anymore.
The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 11 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 10 | ||||
| -rw-r--r-- | checker/mod_checking.mli | 2 |
3 files changed, 12 insertions, 11 deletions
diff --git a/checker/check.ml b/checker/check.ml index cc5ad0af4c..76f40dbac2 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -100,16 +100,7 @@ let access_opaque_table dp i = assert (i < Array.length t); t.(i) -let access_opaque_univ_table dp i = - try - let t = LibraryMap.find dp !opaque_univ_tables in - assert (i < Array.length t); - Some t.(i) - with Not_found -> None - -let () = - Opaqueproof.set_indirect_opaque_accessor access_opaque_table; - Opaqueproof.set_indirect_univ_accessor access_opaque_univ_table +let () = Mod_checking.set_indirect_accessor access_opaque_table 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 a3f151ef86..1cf07e7cc7 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -8,6 +8,14 @@ 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); + Opaqueproof.access_constraints = (fun _ _ -> assert false); +} + 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 *) @@ -33,7 +41,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 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 6cff3e6b8c..dbc81c8507 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -8,4 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +val set_indirect_accessor : (Names.DirPath.t -> int -> Constr.t option) -> unit + val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit |