[stm] Break stm/toplevel dependency loop.

Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.

This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.

As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.

Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.

1 files changed, 176 insertions, 0 deletions

diff --git a/vernac/command.mli b/vernac/command.mli
new file mode 100644
index 000000000..616afb91f
--- /dev/null
+++ b/vernac/command.mli
@@ -0,0 +1,176 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Term
+open Entries
+open Libnames
+open Globnames
+open Vernacexpr
+open Constrexpr
+open Decl_kinds
+open Redexpr
+open Pfedit
+
+(** This file is about the interpretation of raw commands into typed
+    ones and top-level declaration of the main Gallina objects *)
+
+val do_universe : polymorphic -> Id.t Loc.located list -> unit
+val do_constraint : polymorphic ->
+  (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit
+
+(** {6 Hooks for Pcoq} *)
+
+val set_declare_definition_hook : (Safe_typing.private_constants definition_entry -> unit) -> unit
+val get_declare_definition_hook : unit -> (Safe_typing.private_constants definition_entry -> unit)
+
+(** {6 Definitions/Let} *)
+
+val interp_definition :
+  lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr ->
+  constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
+      Universes.universe_binders * Impargs.manual_implicits
+
+val declare_definition : Id.t -> definition_kind ->
+  Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
+    Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
+
+val do_definition : Id.t -> definition_kind -> lident list option ->
+  local_binder list -> red_expr option -> constr_expr ->
+  constr_expr option -> unit Lemmas.declaration_hook -> unit
+
+(** {6 Parameters/Assumptions} *)
+
+(* val interp_assumption : env -> evar_map ref -> *)
+(*   local_binder list -> constr_expr ->  *)
+(*   types Univ.in_universe_context_set * Impargs.manual_implicits *)
+
+(** returns [false] if the assumption is neither local to a section,
+    nor in a module type and meant to be instantiated. *)
+val declare_assumption : coercion_flag -> assumption_kind -> 
+  types Univ.in_universe_context_set ->
+  Universes.universe_binders -> Impargs.manual_implicits ->
+  bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
+  global_reference * Univ.Instance.t * bool
+
+val do_assumptions : locality * polymorphic * assumption_object_kind ->
+  Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool
+
+(* val declare_assumptions : variable Loc.located list -> *)
+(*   coercion_flag -> assumption_kind -> types Univ.in_universe_context_set ->  *)
+(*   Impargs.manual_implicits -> bool -> Vernacexpr.inline -> bool *)
+
+(** {6 Inductive and coinductive types} *)
+
+(** Extracting the semantical components out of the raw syntax of mutual
+   inductive declarations *)
+
+type structured_one_inductive_expr = {
+  ind_name : Id.t;
+  ind_univs : lident list option;
+  ind_arity : constr_expr;
+  ind_lc : (Id.t * constr_expr) list
+}
+
+type structured_inductive_expr =
+  local_binder list * structured_one_inductive_expr list
+
+val extract_mutual_inductive_declaration_components :
+  (one_inductive_expr * decl_notation list) list ->
+    structured_inductive_expr * (*coercions:*) qualid list * decl_notation list
+
+(** Typing mutual inductive definitions *)
+
+type one_inductive_impls =
+  Impargs.manual_implicits (** for inds *)*
+  Impargs.manual_implicits list (** for constrs *)
+
+val interp_mutual_inductive :
+  structured_inductive_expr -> decl_notation list -> polymorphic ->
+    private_flag -> Decl_kinds.recursivity_kind ->
+    mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
+
+(** Registering a mutual inductive definition together with its
+   associated schemes *)
+
+val declare_mutual_inductive_with_eliminations :
+  mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
+  mutual_inductive
+
+(** Entry points for the vernacular commands Inductive and CoInductive *)
+
+val do_mutual_inductive :
+  (one_inductive_expr * decl_notation list) list -> polymorphic -> 
+  private_flag -> Decl_kinds.recursivity_kind -> unit
+
+(** {6 Fixpoints and cofixpoints} *)
+
+type structured_fixpoint_expr = {
+  fix_name : Id.t;
+  fix_univs : lident list option;
+  fix_annot : Id.t Loc.located option;
+  fix_binders : local_binder list;
+  fix_body : constr_expr option;
+  fix_type : constr_expr
+}
+
+(** Extracting the semantical components out of the raw syntax of
+   (co)fixpoints declarations *)
+
+val extract_fixpoint_components : bool ->
+  (fixpoint_expr * decl_notation list) list ->
+    structured_fixpoint_expr list * decl_notation list
+
+val extract_cofixpoint_components :
+  (cofixpoint_expr * decl_notation list) list ->
+    structured_fixpoint_expr list * decl_notation list
+
+(** Typing global fixpoints and cofixpoint_expr *)
+
+type recursive_preentry =
+  Id.t list * constr option list * types list
+
+val interp_fixpoint :
+  structured_fixpoint_expr list -> decl_notation list ->
+    recursive_preentry * lident list option * Evd.evar_universe_context * 
+    (Name.t list * Impargs.manual_implicits * int option) list
+
+val interp_cofixpoint :
+  structured_fixpoint_expr list -> decl_notation list ->
+    recursive_preentry * lident list option * Evd.evar_universe_context * 
+    (Name.t list * Impargs.manual_implicits * int option) list
+
+(** Registering fixpoints and cofixpoints in the environment *)
+
+val declare_fixpoint :
+  locality -> polymorphic ->
+  recursive_preentry * lident list option * Evd.evar_universe_context * 
+  (Name.t list * Impargs.manual_implicits * int option) list ->
+  lemma_possible_guards -> decl_notation list -> unit
+
+val declare_cofixpoint : locality -> polymorphic -> 
+  recursive_preentry * lident list option * Evd.evar_universe_context * 
+  (Name.t list * Impargs.manual_implicits * int option) list ->
+  decl_notation list -> unit
+
+(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
+
+val do_fixpoint :
+  (* When [false], assume guarded. *)
+  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
+
+val do_cofixpoint :
+  (* When [false], assume guarded. *)
+  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
+
+(** Utils *)
+
+val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
+
+val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
+  Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference