doc of coqchk + improved module cache and computation of module sets

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10979 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 119 deletions

diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 4bed9796a..4b156e7ec 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -15,125 +15,6 @@ open Declarations
 open Environ
 open Mod_checking
 
-(*
-let type_modpath env mp = 
-  strengthen env (lookup_module mp env).mod_type mp
-
-let rec check_spec_body env mp lab = function
-  | SPBconst cb ->
-      let kn = mp, empty_dirpath, lab in
-      check_constant_declaration env kn cb
-  | SPBmind mib ->
-      let kn = mp, empty_dirpath, lab in
-      Indtypes.check_inductive env kn mib
-  | SPBmodule msb ->
-      check_mod_spec env msb;
-      Modops.add_module (MPdot(mp,lab)) (module_body_of_type msb.msb_modtype)
-        (add_modtype_constraints env msb.msb_modtype)
-  | SPBmodtype mty ->
-      let kn = mp, empty_dirpath, lab in
-      check_modtype env mty;
-      add_modtype kn mty (add_modtype_constraints env mty)
-
-and check_mod_spec env msb =
-  let env' = add_constraints msb.msb_constraints env in
-  check_modtype env' msb.msb_modtype;
-
-(*  Subtyping.check_equal env' msb.msb_modtype (MTBident *)
-  (* TODO: check equiv *)
-  env'
-
-(* !!!: modtype needs mp (the name it will be given) because
-   submodule should be added without reference to self *)
-and check_modtype env = function
-  | MTBident kn ->
-      (try let _ = lookup_modtype kn env in ()
-      with Not_found -> failwith ("unbound module type "(*^string_of_kn kn*)))
-  | MTBfunsig (mbid,marg,mbody) ->
-      check_modtype env marg;
-      let env' = 
-	add_module (MPbound mbid) (module_body_of_type marg)
-          (add_modtype_constraints env marg) in
-      check_modtype env' mbody
-  | MTBsig (msid,sign) ->
-      let _ =
-        List.fold_left (fun env (lab,mb) ->
-          check_spec_body env (MPself msid) lab mb) env sign in
-      ()
-
-
-let elem_spec_of_body (lab,e) =
-  lab,
-  match e with
-      SEBconst cb -> SPBconst cb
-    | SEBmind mind -> SPBmind mind
-    | SEBmodule msb -> SPBmodule (module_spec_of_body msb)
-    | SEBmodtype mtb -> SPBmodtype mtb
-
-let rec check_module env mb =
-  let env' = add_module_constraints env mb in
-  (* mod_type *)
-  check_modtype env' mb.mod_type;
-  (* mod_expr *)
-  let msig =
-    match mb.mod_expr with
-        Some mex ->
-          let msig = infer_mod_expr env' mex in
-          Subtyping.check_subtypes env' msig mb.mod_type;
-          msig
-      | None -> mb.mod_type in
-  (* mod_user_type *)
-  (match mb.mod_user_type with
-      Some usig -> Subtyping.check_subtypes env' msig usig
-    | None -> ());
-  (* mod_equiv *)
-  (match mb.mod_equiv with
-      Some mid ->
-        if mb.mod_expr <> Some(MEBident mid) then
-          failwith "incorrect module alias"
-    | None -> ());
-
-and infer_mod_expr env = function
-    MEBident mp -> type_modpath env mp
-  | MEBstruct(msid,msb) ->
-      let mp = MPself msid in
-      let _ =
-        List.fold_left (fun env (lab,mb) ->
-          struct_elem_body env mp lab mb) env msb in
-      MTBsig(msid,List.map elem_spec_of_body msb)
-  | MEBfunctor (arg_id, arg, body) ->
-      check_modtype env arg;
-      let env' = add_module (MPbound arg_id) (module_body_of_type arg) env in
-      let body_ty = infer_mod_expr env' body in
-      MTBfunsig (arg_id, arg, body_ty)
-  | MEBapply (fexpr,MEBident mp,_) ->
-      let ftb = infer_mod_expr env fexpr in
-      let ftb = scrape_modtype env ftb in
-      let farg_id, farg_b, fbody_b = destr_functor ftb in
-      let mtb = type_modpath env mp in
-      Subtyping.check_subtypes env mtb farg_b;
-      subst_modtype (map_mbid farg_id mp) fbody_b
-  | MEBapply _ ->
-      failwith "functor argument must be a module variable"
-
-and struct_elem_body env mp lab = function
-  | SEBconst cb ->
-      let kn = mp, empty_dirpath, lab in
-      check_constant_declaration env kn cb
-  | SEBmind mib ->
-      let kn = mp, empty_dirpath, lab in
-      Indtypes.check_inductive env kn mib
-  | SEBmodule msb ->
-      check_module env msb;
-(*msgnl(str"MODULE OK: "++prkn(make_kn mp empty_dirpath lab)++fnl());*)
-      Modops.add_module (MPdot(mp,lab)) msb 
-        (add_module_constraints env msb)
-  | SEBmodtype mty ->
-      check_modtype env mty;
-      add_modtype (mp, empty_dirpath, lab) mty
-        (add_modtype_constraints env mty)
-*)
-
 (************************************************************************)
 (*
  * Global environment