[checker] Refactor by sharing code with the kernel

For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.

With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.

We also rename some files from the checker so that they don't clash with
kernel files.

1 files changed, 0 insertions, 151 deletions

diff --git a/checker/modops.ml b/checker/modops.ml
deleted file mode 100644
index 541d009ff9..0000000000
--- a/checker/modops.ml
+++ /dev/null
@@ -1,151 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(*i*)
-open CErrors
-open Util
-open Pp
-open Names
-open Cic
-open Declarations
-(*i*)
-
-let error_not_a_constant l =
-  user_err Pp.(str ("\""^(Label.to_string l)^"\" is not a constant"))
-
-let error_not_a_functor () = user_err Pp.(str "Application of not a functor")
-
-let error_incompatible_modtypes _ _ = user_err Pp.(str "Incompatible module types")
-
-let error_not_match l _ =
-  user_err Pp.(str ("Signature components for label "^Label.to_string l^" do not match"))
-
-let error_no_such_label l = user_err Pp.(str ("No such label "^Label.to_string l))
-
-let error_no_such_label_sub l l1 =
-  let l1 = ModPath.to_string l1 in
-  user_err Pp.(str ("The field "^
-         Label.to_string l^" is missing in "^l1^"."))
-
-let error_not_a_module_loc ?loc s =
-  user_err ?loc  (str ("\""^Label.to_string s^"\" is not a module"))
-
-let error_not_a_module s = error_not_a_module_loc s
-
-let error_with_module () =
-  user_err Pp.(str "Unsupported 'with' constraint in module implementation")
-
-let is_functor = function
-  | MoreFunctor _ -> true
-  | NoFunctor _ -> false
-
-let destr_functor = function
-  | MoreFunctor (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
-  | NoFunctor _ -> error_not_a_functor ()
-
-let module_body_of_type mp mtb =
-  { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] }
-
-let rec add_structure mp sign resolver env =
-  let add_one env (l,elem) =
-    let kn = KerName.make mp l in
-    let con = Constant.make1 kn in
-    let mind = mind_of_delta resolver (MutInd.make1 kn) in
-      match elem with
-	| SFBconst cb ->
-	   (* let con =  constant_of_delta resolver con in*)
-	      Environ.add_constant con cb env
-	| SFBmind mib ->
-	   (* let mind =  mind_of_delta resolver mind in*)
-	    Environ.add_mind mind mib env
-	| SFBmodule mb -> add_module mb env
-	      (* adds components as well *)
-	| SFBmodtype mtb -> Environ.add_modtype mtb.mod_mp mtb env
-  in
-  List.fold_left add_one env sign
-
-and add_module mb env =
-  let mp = mb.mod_mp in
-  let env = Environ.shallow_add_module mp mb env in
-  match mb.mod_type with
-  | NoFunctor struc -> add_structure mp struc mb.mod_delta env
-  | MoreFunctor _ -> env
-
-let add_module_type mp mtb env = add_module (module_body_of_type mp mtb) env
-
-let strengthen_const mp_from l cb =
-  match cb.const_body with
-    | Def _ -> cb
-    | _ ->
-      let con = Constant.make2 mp_from l in
-      let u =
-        match cb.const_universes with
-      | Monomorphic_const _ -> Univ.Instance.empty
-      | Polymorphic_const auctx -> Univ.make_abstract_instance auctx
-      in
-      { cb with
-	const_body = Def (Declarations.from_val (Const (con,u))) }
-
-let rec strengthen_mod mp_from mp_to mb =
-  if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb
-  else
-    let mk_expr mp_to = Algebraic (NoFunctor (MEident mp_to)) in
-    strengthen_body mk_expr mp_from mp_to mb
-
-and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a generic_module_body =
-  fun mk_expr mp_from mp_to mb ->
-  match mb.mod_type with
-  | MoreFunctor _ -> mb
-  | NoFunctor sign ->
-    let resolve_out,sign_out = strengthen_sig mp_from sign mp_to
-    in
-    { mb with
-      mod_expr = mk_expr mp_to;
-      mod_type = NoFunctor sign_out;
-      mod_delta = resolve_out }
-
-and strengthen_sig mp_from sign mp_to =
-  match sign with
-    | [] -> empty_delta_resolver,[]
-    | (l,SFBconst cb) :: rest ->
-        let item' = l,SFBconst (strengthen_const mp_from l cb) in
-        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
-	resolve_out,item'::rest'
-    | (_,SFBmind _ as item):: rest ->
-        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
-	  resolve_out,item::rest'
-    | (l,SFBmodule mb) :: rest ->
-	let mp_from' = MPdot (mp_from,l) in
-	let mp_to' = MPdot(mp_to,l) in
-	let mb_out = strengthen_mod mp_from' mp_to' mb in
-	let item' = l,SFBmodule (mb_out) in
-        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
-	resolve_out (*add_delta_resolver resolve_out mb.mod_delta*),
-        item':: rest'
-    | (_,SFBmodtype _ as item) :: rest ->
-        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
-        resolve_out,item::rest'
-
-let strengthen mtb mp =
-  strengthen_body ignore mtb.mod_mp mp mtb
-
-let subst_and_strengthen mb mp =
-  strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
-
-let module_type_of_module mp mb =
-  let mtb =
-    { mb with
-      mod_expr = ();
-      mod_type_alg = None;
-      mod_retroknowledge = ModTypeRK }
-  in
-  match mp with
-  | Some mp -> strengthen {mtb with mod_mp = mp} mp
-  | None -> mtb