From b6f3c8e4f173e3f272f966e1061e7112bf5d1b4a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 25 Jul 2017 15:11:22 +0200 Subject: [api] Put modules in order in API.{mli,ml} We sort the dependency graph of API by following a logical declaration order in `API.{ml,mli}` related to the actual dependency order of Coq modules. Things are a bit tricky here as Coq itself relies on the fact that OCaml treats module interface and implementation separately dependency-wise; however, when resorting module alias the design seems to become more coupled. Currently, API exposes both "namespaces", asserting a large number of type equality between them, however the `API` namespace is not self-contained. In particular, this is a first step to solve problems such as `Summary.frozen` being used in `API.mli` but not declared by the `API.Summary` module, etc... In general we follow the invariant that a type used in `API` must have been declared before. Keep in mind that OCaml upstream has warned that it maybe tricky to alias objects in this way. In particular, after API the old `mli` only files have become full compilation units so we may want to be more careful here. The more "correct" declaration order allows us to remove the `API.Prelude` module, as well as some other declarations that I consider as spurious. We still maintain the large number of type aliases which will be removed in a future patch. We follow linking order except for files in `intf`, which are conceptually wrongly placed in the linking hierarchy but this doesn't matter as the files don't contain any implementation. We also move a couple of `.mli` only files to `.ml` so we are consistent, and correct their linking order in `mllib`, even if that doesn't matter as such `.ml`-only files contain no implementations. --- kernel/kernel.mllib | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'kernel/kernel.mllib') diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 0813315b5..dd3f9a2f8 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -9,6 +9,8 @@ Constr Context Vars Term +Declarations +Entries Mod_subst Cbytecodes Copcodes @@ -41,5 +43,4 @@ Nativelibrary Safe_typing Vm Csymtable -Declarations Vconv -- cgit v1.2.3