diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-28 00:16:46 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-23 16:23:49 +0200 |
commit | 7dfac786626f8f6775dadc0df85360759584c976 (patch) | |
tree | 9c0355fb0dba4a48e14d0e5b316c66dfd416d685 | |
parent | 5c34cfa54ec1959758baa3dd283e2e30853380db (diff) |
[api] Relocate `intf` modules according to dependency-order.
In a component-based source code organization of Coq `intf` doesn't
fit very well, as it sits in bit of "limbo" between different
components, and indeed, encourages developers to place types in
sometimes random places wrt the hierarchy. For example, lower parts of
the system reference `Vernacexpr`, which morally lives in a pretty
higher part of the system.
We move all the files in `intf` to the lowest place their dependencies
can accommodate:
- `Misctypes`: is used by Declaremod, thus it has to go in `library`
or below. Ideally, this file would disappear.
- `Evar_kinds`: it is used by files in `engine`, so that seems its
proper placement.
- `Decl_kinds`: used in `library`, seems like the right place. [could
also be merged.
- `Glob_term`: belongs to pretyping, where it is placed.
- `Locus`: ditto.
- `Pattern`: ditto.
- `Genredexpr`: depended by a few modules in `pretyping`, seems like
the righ place.
- `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and
could be fixed, as this module should be declared in `interp` which
is the one eliminating it.
- `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed
as it contains stuff it shouldn't. The right place should be `parsing`.
- `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`.
- `Notation_term`: First place used is `interp`, seems like the right place.
Additionally, for some files it could be worth to merge files of the
form `Foo` with `Foo_ops` in the medium term, as to create proper ADT
modules as done in the kernel with `Name`, etc...
-rw-r--r-- | .github/CODEOWNERS | 5 | ||||
-rw-r--r-- | .merlin | 2 | ||||
-rw-r--r-- | META.coq | 13 | ||||
-rw-r--r-- | Makefile.common | 4 | ||||
-rw-r--r-- | configure.ml | 2 | ||||
-rw-r--r-- | dev/base_include | 1 | ||||
-rw-r--r-- | dev/core.dbg | 1 | ||||
-rw-r--r-- | dev/doc/coq-src-description.txt | 6 | ||||
-rw-r--r-- | dev/ocamldebug-coq.run | 2 | ||||
-rw-r--r-- | engine/engine.mllib | 1 | ||||
-rw-r--r-- | engine/evar_kinds.ml (renamed from intf/evar_kinds.ml) | 0 | ||||
-rw-r--r-- | interp/interp.mllib | 1 | ||||
-rw-r--r-- | interp/notation_term.ml (renamed from intf/notation_term.ml) | 0 | ||||
-rw-r--r-- | intf/intf.mllib | 11 | ||||
-rw-r--r-- | library/decl_kinds.ml (renamed from intf/decl_kinds.ml) | 0 | ||||
-rw-r--r-- | library/library.mllib | 2 | ||||
-rw-r--r-- | library/misctypes.ml (renamed from intf/misctypes.ml) | 0 | ||||
-rw-r--r-- | pretyping/constrexpr.ml (renamed from intf/constrexpr.ml) | 0 | ||||
-rw-r--r-- | pretyping/extend.ml (renamed from intf/extend.ml) | 0 | ||||
-rw-r--r-- | pretyping/genredexpr.ml (renamed from intf/genredexpr.ml) | 0 | ||||
-rw-r--r-- | pretyping/glob_term.ml (renamed from intf/glob_term.ml) | 0 | ||||
-rw-r--r-- | pretyping/locus.ml (renamed from intf/locus.ml) | 0 | ||||
-rw-r--r-- | pretyping/pattern.ml (renamed from intf/pattern.ml) | 0 | ||||
-rw-r--r-- | pretyping/pretyping.mllib | 9 | ||||
-rw-r--r-- | pretyping/vernacexpr.ml (renamed from intf/vernacexpr.ml) | 0 |
25 files changed, 16 insertions, 44 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 029b55b9a..7f3ee5c37 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -86,11 +86,6 @@ /interp/ @herbelin # Secondary maintainer @ejgallego -########## Interfaces ########## - -/intf/ @letouzey -# Secondary maintainer @ppedrot - ########## Kernel ########## /kernel/ @maximedenes @@ -10,8 +10,6 @@ S kernel B kernel S kernel/byterun B kernel/byterun -S intf -B intf S library B library S engine @@ -90,19 +90,6 @@ package "library" ( ) -package "intf" ( - - description = "Coq Public Data Types" - version = "8.8" - - requires = "coq.library" - - directory = "intf" - - archive(byte) = "intf.cma" - archive(native) = "intf.cmxa" -) - package "engine" ( description = "Coq Tactic Engine" diff --git a/Makefile.common b/Makefile.common index 9a30e2a4c..eed41fbe7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -75,7 +75,7 @@ INSTALLSH:=./install.sh MKDIR:=install -d CORESRCDIRS:=\ - config clib lib kernel intf kernel/byterun library \ + config clib lib kernel kernel/byterun library \ engine pretyping interp proofs parsing printing \ tactics vernac stm toplevel @@ -102,7 +102,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ # respecting this order is useful for developers that want to load or link # the libraries directly -CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \ +CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ stm/stm.cma toplevel/toplevel.cma diff --git a/configure.ml b/configure.ml index 6c052b63b..2ac705ad2 100644 --- a/configure.ml +++ b/configure.ml @@ -1212,7 +1212,7 @@ let write_configml f = let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "parsing"; "proofs"; - "tactics"; "toplevel"; "printing"; "intf"; + "tactics"; "toplevel"; "printing"; "grammar"; "ide"; "stm"; "vernac" ] in let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") "" diff --git a/dev/base_include b/dev/base_include index e76044f41..2f7183dd6 100644 --- a/dev/base_include +++ b/dev/base_include @@ -15,7 +15,6 @@ #directory "tactics";; #directory "printing";; #directory "grammar";; -#directory "intf";; #directory "stm";; #directory "vernac";; diff --git a/dev/core.dbg b/dev/core.dbg index 57c136900..edf67020a 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -16,5 +16,4 @@ load_printer tactics.cma load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma -load_printer intf.cma load_printer ltac_plugin.cmo diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index b3d49b7e5..764d48295 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -17,12 +17,6 @@ toplevel Special components ------------------ -intf : - - Contains mli-only interfaces, many of them providing a.s.t. - used for dialog bewteen coq components. Ex: Constrexpr.constr_expr - produced by parsing and transformed by interp. - grammar : Camlp5 syntax extensions. The file grammar/grammar.cma is used diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index f3e60edea..8f1c165dd 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -18,7 +18,7 @@ exec $OCAMLDEBUG \ -I $CAMLP5LIB -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ - -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ + -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ diff --git a/engine/engine.mllib b/engine/engine.mllib index a3614f6c4..a5df5a9fa 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -2,6 +2,7 @@ Universes Univops UState Nameops +Evar_kinds Evd EConstr Namegen diff --git a/intf/evar_kinds.ml b/engine/evar_kinds.ml index c964ecf1f..c964ecf1f 100644 --- a/intf/evar_kinds.ml +++ b/engine/evar_kinds.ml diff --git a/interp/interp.mllib b/interp/interp.mllib index bb22cf468..61313acc4 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,6 +1,7 @@ Tactypes Stdarg Genintern +Notation_term Notation_ops Notation Syntax_def diff --git a/intf/notation_term.ml b/interp/notation_term.ml index a9c2e2a53..a9c2e2a53 100644 --- a/intf/notation_term.ml +++ b/interp/notation_term.ml diff --git a/intf/intf.mllib b/intf/intf.mllib deleted file mode 100644 index 2b8960d3f..000000000 --- a/intf/intf.mllib +++ /dev/null @@ -1,11 +0,0 @@ -Constrexpr -Evar_kinds -Genredexpr -Locus -Extend -Notation_term -Decl_kinds -Glob_term -Misctypes -Pattern -Vernacexpr diff --git a/intf/decl_kinds.ml b/library/decl_kinds.ml index 0d3285311..0d3285311 100644 --- a/intf/decl_kinds.ml +++ b/library/decl_kinds.ml diff --git a/library/library.mllib b/library/library.mllib index e43bfb5a1..1c0368847 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -4,7 +4,9 @@ Libobject Summary Nametab Global +Decl_kinds Lib +Misctypes Declaremods Loadpath Library diff --git a/intf/misctypes.ml b/library/misctypes.ml index 72db3b31c..72db3b31c 100644 --- a/intf/misctypes.ml +++ b/library/misctypes.ml diff --git a/intf/constrexpr.ml b/pretyping/constrexpr.ml index fda31756a..fda31756a 100644 --- a/intf/constrexpr.ml +++ b/pretyping/constrexpr.ml diff --git a/intf/extend.ml b/pretyping/extend.ml index 734b859f6..734b859f6 100644 --- a/intf/extend.ml +++ b/pretyping/extend.ml diff --git a/intf/genredexpr.ml b/pretyping/genredexpr.ml index 80697461a..80697461a 100644 --- a/intf/genredexpr.ml +++ b/pretyping/genredexpr.ml diff --git a/intf/glob_term.ml b/pretyping/glob_term.ml index 84be15552..84be15552 100644 --- a/intf/glob_term.ml +++ b/pretyping/glob_term.ml diff --git a/intf/locus.ml b/pretyping/locus.ml index 95a2e495b..95a2e495b 100644 --- a/intf/locus.ml +++ b/pretyping/locus.ml diff --git a/intf/pattern.ml b/pretyping/pattern.ml index 76367b612..76367b612 100644 --- a/intf/pattern.ml +++ b/pretyping/pattern.ml diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index ae4ad0be7..d98026bc6 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,5 +1,5 @@ Geninterp -Ltac_pretype +Locus Locusops Pretype_errors Reductionops @@ -16,12 +16,19 @@ Evarsolve Recordops Evarconv Typing +Constrexpr +Genredexpr Miscops +Glob_term +Ltac_pretype Glob_ops Redops +Pattern Patternops Constr_matching Tacred +Extend +Vernacexpr Typeclasses_errors Typeclasses Classops diff --git a/intf/vernacexpr.ml b/pretyping/vernacexpr.ml index 4e1c986f1..4e1c986f1 100644 --- a/intf/vernacexpr.ml +++ b/pretyping/vernacexpr.ml |