1 files changed, 572 insertions, 0 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
new file mode 100644
index 00000000..4f180599
--- /dev/null
+++ b/kernel/safe_typing.ml
@@ -0,0 +1,572 @@
+(************************************************************************)
+(*  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,v 1.76.2.1 2004/07/16 19:30:26 herbelin Exp $ *)
+
+open Util
+open Names
+open Univ
+open Term
+open Reduction
+open Sign
+open Declarations
+open Inductive
+open Environ
+open Entries
+open Typeops
+open Type_errors
+open Indtypes
+open Term_typing
+open Modops
+open Subtyping
+open Mod_typing
+
+type modvariant = 
+  | NONE 
+  | SIG of (* funsig params *) (mod_bound_id * module_type_body) list 
+  | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list
+      * (* optional result type *) module_type_body option
+  | LIBRARY of dir_path
+
+type module_info = 
+    { msid : mod_self_id;
+      modpath : module_path;
+      seed : dir_path; (* the "seed" of unique identifier generator *)
+      label : label;
+      variant : modvariant}
+
+let check_label l labset = 
+  if Labset.mem l labset then error_existing_label l
+
+type library_info = dir_path * Digest.t
+
+type safe_environment = 
+    { old : safe_environment;
+      env : env;
+      modinfo : module_info;
+      labset : Labset.t;
+      revsign : module_signature_body;
+      revstruct : module_structure_body;
+      imports : library_info list;
+      loads : (module_path * module_body) list }
+
+(*
+  { old = senv.old;
+    env = ;
+    modinfo = senv.modinfo;
+    labset = ;
+    revsign = ;
+    imports = senv.imports ;
+    loads = senv.loads }
+*)
+
+
+(* a small hack to avoid variants and an unused case in all functions *)
+let rec empty_environment = 
+  { old = empty_environment; 
+    env = empty_env;
+    modinfo = {
+      msid = initial_msid;
+      modpath = initial_path;
+      seed = initial_dir;
+      label = mk_label "_";
+      variant = NONE};
+    labset = Labset.empty;
+    revsign = [];
+    revstruct = [];
+    imports = [];
+    loads = [] }
+
+let env_of_safe_env senv = senv.env
+let env_of_senv = env_of_safe_env
+
+
+(* Insertion of section variables. They are now typed before being
+   added to the environment. *)
+
+(* Same as push_named, but check that the variable is not already
+   there. Should *not* be done in Environ because tactics add temporary
+   hypothesis many many times, and the check performed here would
+   cost too much. *)
+let safe_push_named (id,_,_ as d) env =
+  let _ =
+    try
+      let _ = lookup_named id env in 
+      error ("identifier "^string_of_id id^" already defined")
+    with Not_found -> () in
+  Environ.push_named d env
+
+let push_named_def (id,b,topt) senv =
+  let (c,typ,cst) = translate_local_def senv.env (b,topt) in
+  let env' = add_constraints cst senv.env in
+  let env'' = safe_push_named (id,Some c,typ) env' in
+  (cst, {senv with env=env''})
+
+let push_named_assum (id,t) senv =
+  let (t,cst) = translate_local_assum senv.env t in
+  let env' = add_constraints cst senv.env in
+  let env'' = safe_push_named (id,None,t) env' in
+  (cst, {senv with env=env''})
+
+
+(* Insertion of constants and parameters in environment. *)
+
+type global_declaration = 
+  | ConstantEntry of constant_entry
+  | GlobalRecipe of Cooking.recipe
+
+let hcons_constant_body cb =
+  let body = match cb.const_body with
+      None -> None
+    | Some l_constr -> let constr = Declarations.force l_constr in
+	Some (Declarations.from_val (hcons1_constr constr))
+  in
+    { cb with
+	const_body = body;
+	const_type = hcons1_constr cb.const_type }
+
+let add_constant dir l decl senv =
+  check_label l senv.labset;
+  let cb = match decl with 
+      ConstantEntry ce -> translate_constant senv.env ce
+    | GlobalRecipe r ->
+        let cb = translate_recipe senv.env r in
+        if dir = empty_dirpath then hcons_constant_body cb else cb
+  in
+(*  let cb = if dir = empty_dirpath then hcons_constant_body cb else cb in*)
+  let env' = Environ.add_constraints cb.const_constraints senv.env in
+  let kn = make_kn senv.modinfo.modpath dir l in
+  let env'' = Environ.add_constant kn cb env' in
+  kn, { old = senv.old;
+	env = env'';
+	modinfo = senv.modinfo;
+	labset = Labset.add l senv.labset;
+	revsign = (l,SPBconst cb)::senv.revsign;
+	revstruct = (l,SEBconst cb)::senv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads }
+    
+
+(* Insertion of inductive types. *)
+
+let add_mind dir l mie senv =
+  if mie.mind_entry_inds = [] then 
+    anomaly "empty inductive types declaration"; 
+            (* this test is repeated by translate_mind *)
+  let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in
+  if l <> label_of_id id then
+    anomaly ("the label of inductive packet and its first inductive"^
+	     " type do not match");
+  check_label l senv.labset; 
+    (* TODO: when we will allow reorderings we will have to verify 
+       all labels *)
+  let mib = translate_mind senv.env mie in
+  let env' = Environ.add_constraints mib.mind_constraints senv.env in
+  let kn = make_kn senv.modinfo.modpath dir l in
+  let env'' = Environ.add_mind kn mib env' in
+  kn, { old = senv.old;
+	env = env'';
+	modinfo = senv.modinfo;
+	labset = Labset.add l senv.labset;  (* TODO: the same as above *)
+	revsign = (l,SPBmind mib)::senv.revsign;
+	revstruct = (l,SEBmind mib)::senv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads }
+
+
+(* Insertion of module types *)
+
+let add_modtype l mte senv = 
+  check_label l senv.labset; 
+  let mtb = translate_modtype senv.env mte in
+  let env' = add_modtype_constraints senv.env mtb in
+  let kn = make_kn senv.modinfo.modpath empty_dirpath l in
+  let env'' = Environ.add_modtype kn mtb env' in
+  kn, { old = senv.old;
+	env = env'';
+	modinfo = senv.modinfo;
+	labset = Labset.add l senv.labset;
+	revsign = (l,SPBmodtype mtb)::senv.revsign;
+	revstruct = (l,SEBmodtype mtb)::senv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads }
+
+
+
+(* full_add_module adds module with universes and constraints *)
+let full_add_module mp mb env =
+  let env = add_module_constraints env mb in
+  let env = Modops.add_module mp mb env in
+    env
+
+(* Insertion of modules *)
+
+let add_module l me senv = 
+  check_label l senv.labset; 
+  let mb = translate_module senv.env me in
+  let mspec = module_spec_of_body mb in
+  let mp = MPdot(senv.modinfo.modpath, l) in
+  let env' = full_add_module mp mb senv.env in
+  mp, { old = senv.old;
+	env = env';
+	modinfo = senv.modinfo;
+	labset = Labset.add l senv.labset;
+	revsign = (l,SPBmodule mspec)::senv.revsign;
+	revstruct = (l,SEBmodule mb)::senv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads }
+
+
+(* Interactive modules *)
+
+let start_module l params result senv = 
+  check_label l senv.labset; 
+  let rec trans_params env = function 
+    | [] -> env,[] 
+    | (mbid,mte)::rest -> 
+	let mtb = translate_modtype env mte in
+	let env = 
+	  full_add_module (MPbound mbid) (module_body_of_type mtb) env 
+	in
+	let env,transrest = trans_params env rest in
+	env, (mbid,mtb)::transrest
+  in
+  let env,params_body = trans_params senv.env params in
+  let check_sig mtb = match scrape_modtype env mtb with
+    | MTBsig _ -> ()
+    | MTBfunsig _ -> error_result_must_be_signature mtb 
+    | _ -> anomaly "start_module: modtype not scraped"
+  in
+  let result_body = option_app (translate_modtype env) result in
+  ignore (option_app check_sig result_body);
+  let msid = make_msid senv.modinfo.seed (string_of_label l) in
+  let mp = MPself msid in
+  let modinfo = { msid = msid;
+		  modpath = mp;
+		  seed = senv.modinfo.seed;
+		  label = l;
+		  variant = STRUCT(params_body,result_body) }
+  in
+  mp, { old = senv;
+	env = env;
+	modinfo = modinfo;
+	labset = Labset.empty;
+	revsign = [];
+	revstruct = [];
+	imports = senv.imports;
+	loads = [] }
+
+
+
+let end_module l senv = 
+  let oldsenv = senv.old in
+  let modinfo = senv.modinfo in
+  let params, restype = 
+    match modinfo.variant with
+      | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
+      | STRUCT(params,restype) -> (params,restype)
+  in
+  if l <> modinfo.label then error_incompatible_labels l modinfo.label;
+  if not (empty_context senv.env) then error_local_context None;
+  let functorize_type = 
+    List.fold_right 
+      (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb))
+      params
+  in
+  let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
+  let mtb, mod_user_type, cst = 
+    match restype with
+      | None -> functorize_type auto_tb, None, Constraint.empty
+      | Some res_tb -> 
+	  let cst = check_subtypes senv.env auto_tb res_tb in
+	  let mtb = functorize_type res_tb in
+	    mtb, Some mtb, cst
+  in
+  let mexpr = 
+    List.fold_right
+      (fun (arg_id,arg_b) mtb -> MEBfunctor (arg_id,arg_b,mtb))
+      params
+      (MEBstruct (modinfo.msid, List.rev senv.revstruct)) 
+  in
+  let mb = 
+    { mod_expr = Some mexpr;
+      mod_user_type = mod_user_type;
+      mod_type = mtb;
+      mod_equiv = None;
+      mod_constraints = cst }
+  in
+  let mspec = 
+    { msb_modtype = mtb;
+      msb_equiv = None;
+      msb_constraints = Constraint.empty } 
+  in
+  let mp = MPdot (oldsenv.modinfo.modpath, l) in
+  let newenv = oldsenv.env in
+  let newenv = 
+    List.fold_left
+      (fun env (mp,mb) -> full_add_module mp mb env) 
+      newenv
+      senv.loads
+  in
+  let newenv = 
+    full_add_module mp mb newenv
+  in 
+  mp, { old = oldsenv.old;
+	env = newenv;
+	modinfo = oldsenv.modinfo;
+	labset = Labset.add l oldsenv.labset;
+	revsign = (l,SPBmodule mspec)::oldsenv.revsign;
+	revstruct = (l,SEBmodule mb)::oldsenv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads@oldsenv.loads }
+
+
+(* Interactive module types *)
+
+let start_modtype l params senv = 
+  check_label l senv.labset; 
+  let rec trans_params env = function 
+    | [] -> env,[] 
+    | (mbid,mte)::rest -> 
+	let mtb = translate_modtype env mte in
+	let env = 
+	  full_add_module (MPbound mbid) (module_body_of_type mtb) env 
+	in
+	let env,transrest = trans_params env rest in
+	env, (mbid,mtb)::transrest
+  in
+  let env,params_body = trans_params senv.env params in
+  let msid = make_msid senv.modinfo.seed (string_of_label l) in
+  let mp = MPself msid in
+  let modinfo = { msid = msid;
+		  modpath = mp;
+		  seed = senv.modinfo.seed;
+		  label = l;
+		  variant = SIG params_body }
+  in
+  mp, { old = senv;
+	env = env;
+	modinfo = modinfo;
+	labset = Labset.empty;
+	revsign = [];
+	revstruct = [];
+	imports = senv.imports;
+	loads = [] }
+
+let end_modtype l senv = 
+  let oldsenv = senv.old in
+  let modinfo = senv.modinfo in
+  let params = 
+    match modinfo.variant with
+      | LIBRARY _ | NONE | STRUCT _ -> error_no_modtype_to_end ()
+      | SIG params -> params
+  in
+  if l <> modinfo.label then error_incompatible_labels l modinfo.label;
+  if not (empty_context senv.env) then error_local_context None;
+  let res_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
+  let mtb = 
+    List.fold_right 
+      (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb))
+      params
+      res_tb
+  in
+  let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in
+  let newenv = oldsenv.env in
+  let newenv = 
+    List.fold_left
+      (fun env (mp,mb) -> full_add_module mp mb env) 
+      newenv
+      senv.loads
+  in
+  let newenv = 
+    add_modtype_constraints newenv mtb 
+  in
+  let newenv = 
+    Environ.add_modtype kn mtb newenv
+  in 
+  kn, { old = oldsenv.old;
+	env = newenv;
+	modinfo = oldsenv.modinfo;
+	labset = Labset.add l oldsenv.labset;
+	revsign = (l,SPBmodtype mtb)::oldsenv.revsign;
+	revstruct = (l,SEBmodtype mtb)::oldsenv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads@oldsenv.loads }
+  
+
+let current_modpath senv = senv.modinfo.modpath
+let current_msid senv = senv.modinfo.msid
+
+
+let add_constraints cst senv = 
+  {senv with env = Environ.add_constraints cst senv.env}
+
+(* Check that the engagement expected by a library matches the initial one *)
+let check_engagement env c =
+  match Environ.engagement env, c with
+    | Some ImpredicativeSet, Some ImpredicativeSet -> ()
+    | _, None -> ()
+    | _, Some ImpredicativeSet ->
+        error "Needs option -impredicative-set"
+
+let set_engagement c senv =
+  {senv with env = Environ.set_engagement c senv.env}
+
+
+(* Libraries = Compiled modules *)
+
+type compiled_library = 
+    dir_path * module_body * library_info list * engagement option
+
+
+(* We check that only initial state Require's were performed before 
+   [start_library] was called *)
+
+let start_library dir senv =
+  if not (senv.revsign = [] &&
+	  senv.modinfo.msid = initial_msid &&
+	  senv.modinfo.variant = NONE)
+  then
+    anomaly "Safe_typing.start_library: environment should be empty";
+  let dir_path,l = 
+    match (repr_dirpath dir) with
+	[] -> anomaly "Empty dirpath in Safe_typing.start_library"
+      | hd::tl ->
+	  make_dirpath tl, label_of_id hd
+  in
+  let msid = make_msid dir_path (string_of_label l) in
+  let mp = MPself msid in
+  let modinfo = { msid = msid;
+		  modpath = mp;
+		  seed = dir;
+		  label = l;
+		  variant = LIBRARY dir }
+  in
+  mp, { old = senv;
+	env = senv.env;
+	modinfo = modinfo;
+	labset = Labset.empty;
+	revsign = [];
+	revstruct = [];
+	imports = senv.imports;
+	loads = [] }
+
+
+let export senv dir = 
+  let modinfo = senv.modinfo in
+  begin
+    match modinfo.variant with
+      | LIBRARY dp -> 
+	  if dir <> dp then
+	    anomaly "We are not exporting the right library!"
+      | _ ->
+	  anomaly "We are not exporting the library"
+  end;
+  (*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then
+    (* error_export_simple *) (); *)
+  let mb = 
+    { mod_expr = Some (MEBstruct (modinfo.msid, List.rev senv.revstruct));
+      mod_type = MTBsig (modinfo.msid, List.rev senv.revsign);
+      mod_user_type = None;
+      mod_equiv = None;
+      mod_constraints = Constraint.empty }
+  in
+    modinfo.msid, (dir,mb,senv.imports,engagement senv.env)
+
+
+let check_imports senv needed =
+  let imports = senv.imports in
+  let check (id,stamp) =
+    try
+      let actual_stamp = List.assoc id imports in
+      if stamp <> actual_stamp then
+	error ("Inconsistent assumptions over module " ^(string_of_dirpath id))
+    with Not_found -> 
+      error ("Reference to unknown module " ^ (string_of_dirpath id))
+  in
+  List.iter check needed
+
+(* we have an inefficiency: Since loaded files are added to the
+environment every time a module is closed, their components are
+calculated many times. Thic could be avoided in several ways:
+
+1 - for each file create a dummy environment containing only this
+file's components, merge this environment with the global
+environment, and store for the future (instead of just its type)
+
+2 - create "persistent modules" environment table in Environ add put
+loaded by side-effect once and for all (like it is done in OCaml).
+Would this be correct with respect to undo's and stuff ?
+*)
+ 
+let import (dp,mb,depends,engmt) digest senv = 
+  check_imports senv depends;
+  check_engagement senv.env engmt;
+  let mp = MPfile dp in
+  let env = senv.env in
+  mp, { senv with 
+	  env = full_add_module mp mb env; 
+	  imports = (dp,digest)::senv.imports;
+	  loads = (mp,mb)::senv.loads }
+
+
+(** Remove the body of opaque constants in modules *)
+ 
+let rec lighten_module mb =
+  { mb with
+    mod_expr = option_app lighten_modexpr mb.mod_expr;
+    mod_type = lighten_modtype mb.mod_type;
+    mod_user_type = option_app lighten_modtype mb.mod_user_type }
+
+and lighten_modtype = function
+  | MTBident kn as x -> x
+  | MTBfunsig (mbid,mtb1,mtb2) ->
+      MTBfunsig (mbid, lighten_modtype mtb1, lighten_modtype mtb2)
+  | MTBsig (msid,sign) -> MTBsig (msid, lighten_sig sign)
+
+and lighten_modspec ms =
+  { ms with msb_modtype = lighten_modtype ms.msb_modtype }
+
+and lighten_sig sign = 
+  let lighten_spec (l,spec) = (l,match spec with
+    | SPBconst ({const_opaque=true} as x) -> SPBconst {x with const_body=None}
+    | (SPBconst _ | SPBmind _) as x -> x
+    | SPBmodule m -> SPBmodule (lighten_modspec m)
+    | SPBmodtype m -> SPBmodtype (lighten_modtype m))
+  in
+    List.map lighten_spec sign
+
+and lighten_struct struc = 
+  let lighten_body (l,body) = (l,match body with
+    | SEBconst ({const_opaque=true} as x) -> SEBconst {x with const_body=None}
+    | (SEBconst _ | SEBmind _) as x -> x
+    | SEBmodule m -> SEBmodule (lighten_module m)
+    | SEBmodtype m -> SEBmodtype (lighten_modtype m))
+  in
+    List.map lighten_body struc
+
+and lighten_modexpr = function
+  | MEBfunctor (mbid,mty,mexpr) ->
+      MEBfunctor (mbid,lighten_modtype mty,lighten_modexpr mexpr)
+  | MEBident mp as x -> x
+  | MEBstruct (msid, struc) ->
+      MEBstruct (msid, lighten_struct struc)
+  | MEBapply (mexpr,marg,u) ->
+      MEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
+
+let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)
+
+
+type judgment = unsafe_judgment
+
+let j_val j = j.uj_val
+let j_type j = j.uj_type
+
+let safe_infer senv = infer (env_of_senv senv)
+    
+let typing senv = Typeops.typing (env_of_senv senv)