added the .vo checker (with independent Makefile)

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

1 files changed, 248 insertions, 0 deletions

diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
new file mode 100644
index 0000000000..c6388499a7
--- /dev/null
+++ b/checker/safe_typing.ml
@@ -0,0 +1,248 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: safe_typing.ml 10275 2007-10-30 11:01:24Z barras $ *)
+
+open Pp
+open Util
+open Names
+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
+ *)
+
+let genv = ref empty_env
+let reset () = genv := empty_env
+let get_env () = !genv
+
+let set_engagement c =
+  genv := set_engagement c !genv
+
+(* full_add_module adds module with universes and constraints *)
+let full_add_module dp mb digest =
+  let env = !genv in
+  let mp = MPfile dp in
+  let env = add_module_constraints env mb in
+  let env = Modops.add_module mp mb env in
+  genv := add_digest env dp digest
+
+(* Check that the engagement expected by a library matches the initial one *)
+let check_engagement env c =
+  match engagement env, c with
+    | Some ImpredicativeSet, Some ImpredicativeSet -> ()
+    | _, None -> ()
+    | _, Some ImpredicativeSet ->
+        error "Needs option -impredicative-set"
+
+(* Libraries = Compiled modules *)
+
+let report_clash f caller dir =
+  let msg =
+    str "compiled library " ++ str(string_of_dirpath caller) ++
+    spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++
+    str(string_of_dirpath dir) ++ fnl() in
+  f msg
+
+
+let check_imports f caller env needed =
+  let check (dp,stamp) =
+    try
+      let actual_stamp = lookup_digest env dp in
+      if stamp <> actual_stamp then report_clash f caller dp
+    with Not_found -> 
+      error ("Reference to unknown module " ^ (string_of_dirpath dp))
+  in
+  List.iter check needed
+
+
+
+(* Remove the body of opaque constants in modules *)
+(* also remove mod_expr ? *)
+let rec lighten_module mb =
+  { mb with
+    mod_expr = Option.map lighten_modexpr mb.mod_expr;
+    mod_type = Option.map lighten_modexpr mb.mod_type }
+
+and lighten_struct struc = 
+  let lighten_body (l,body) = (l,match body with
+    | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None}
+    | (SFBconst _ | SFBmind _ | SFBalias _) as x -> x
+    | SFBmodule m -> SFBmodule (lighten_module m)
+    | SFBmodtype m -> SFBmodtype 
+	({m with 
+	    typ_expr = lighten_modexpr m.typ_expr}))
+  in
+    List.map lighten_body struc
+
+and lighten_modexpr = function
+  | SEBfunctor (mbid,mty,mexpr) ->
+      SEBfunctor (mbid, 
+		    ({mty with 
+			typ_expr = lighten_modexpr mty.typ_expr}),
+		  lighten_modexpr mexpr)
+  | SEBident mp as x -> x
+  | SEBstruct (msid, struc) ->
+      SEBstruct (msid, lighten_struct struc)
+  | SEBapply (mexpr,marg,u) ->
+      SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
+  | SEBwith (seb,wdcl) ->
+      SEBwith (lighten_modexpr seb,wdcl) 
+ 
+let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)
+
+
+type compiled_library = 
+    dir_path *
+    module_body *
+    (dir_path * Digest.t) list *
+    engagement option
+ 
+(* When the module is checked, digests do not need to match, but a
+   warning is issued in case of mismatch *)
+let import (dp,mb,depends,engmt as vo) digest = 
+Validate.val_vo (Obj.repr vo);
+prerr_endline "*** vo validated ***";
+  let env = !genv in
+  check_imports msg_warning dp env depends;
+  check_engagement env engmt;
+  check_module env mb;
+  (* We drop proofs once checked *)
+(*  let mb = lighten_module mb in*)
+  full_add_module dp mb digest
+
+(* When the module is admitted, digests *must* match *)
+let unsafe_import (dp,mb,depends,engmt) digest = 
+  let env = !genv in
+  check_imports (errorlabstrm"unsafe_import") dp env depends;
+  check_engagement env engmt;
+  (* We drop proofs once checked *)
+(*  let mb = lighten_module mb in*)
+  full_add_module dp mb digest