(************************************************************************)
(*  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