From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 kernel/safe_typing.ml | 584 ++++++++++++++++++++++++++++++++++----------------
 1 file changed, 396 insertions(+), 188 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5f01613c..6906fb29 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml 10276 2007-10-30 11:37:54Z barras $ *)
+(* $Id: safe_typing.ml 11170 2008-06-25 08:31:04Z soubiran $ *)
 
 open Util
 open Names
@@ -25,6 +25,7 @@ open Term_typing
 open Modops
 open Subtyping
 open Mod_typing
+open Mod_subst
 
 type modvariant = 
   | NONE 
@@ -37,7 +38,8 @@ type module_info =
       modpath : module_path;
       seed : dir_path; (* the "seed" of unique identifier generator *)
       label : label;
-      variant : modvariant}
+      variant : modvariant;
+      alias_subst : substitution}
 
 let check_label l labset = 
   if Labset.mem l labset then error_existing_label l
@@ -54,12 +56,12 @@ type safe_environment =
       env : env;
       modinfo : module_info;
       labset : Labset.t;
-      revsign : module_signature_body;
-      revstruct : module_structure_body;
+      revstruct : structure_body;
       univ : Univ.constraints;
       engagement : engagement option;
       imports : library_info list;
-      loads : (module_path * module_body) list }
+      loads : (module_path * module_body) list;
+      local_retroknowledge : Retroknowledge.action list}
 
 (*
   { old = senv.old;
@@ -81,19 +83,75 @@ let rec empty_environment =
       modpath = initial_path;
       seed = initial_dir;
       label = mk_label "_";
-      variant = NONE};
+      variant = NONE;
+      alias_subst = empty_subst};
     labset = Labset.empty;
-    revsign = [];
     revstruct = [];
     univ = Univ.Constraint.empty;
     engagement = None;
     imports = [];
-    loads = [] }
+    loads = [];
+    local_retroknowledge = [] }
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
 
+
+
+
+
+
+let add_constraints cst senv = 
+  {senv with
+    env = Environ.add_constraints cst senv.env;
+    univ = Univ.Constraint.union cst senv.univ }
+
+
+(*spiwack: functions for safe retroknowledge *)
+
+(* terms which are closed under the environnement env, i.e
+   terms which only depends on constant who are themselves closed *)
+let closed env term = 
+  ContextObjectMap.is_empty (assumptions env term)
+
+(* the set of safe terms in an environement any recursive set of
+   terms who are known not to prove inconsistent statement. It should
+   include at least all the closed terms. But it could contain other ones
+   like the axiom of excluded middle for instance *)
+let safe =
+  closed
+
+
+
+(* universal lifting, used for the "get" operations mostly *)
+let retroknowledge f senv = 
+  Environ.retroknowledge f (env_of_senv senv)
+
+let register senv field value by_clause = 
+  (* todo : value closed, by_clause safe, by_clause of the proper type*)
+  (* spiwack : updates the safe_env with the information that the register
+     action has to be performed (again) when the environement is imported *)
+  {senv with env = Environ.register senv.env field value;
+             local_retroknowledge = 
+      Retroknowledge.RKRegister (field,value)::senv.local_retroknowledge
+  }
+
+(* spiwack : currently unused *)
+let unregister senv field  =
+  (*spiwack: todo: do things properly or delete *)
+  {senv with env = Environ.unregister senv.env field}
+(* /spiwack *)
+
+
+
+
+
+
+
+
+
+
 (* Insertion of section variables. They are now typed before being
    added to the environment. *)
 
@@ -111,15 +169,15 @@ let safe_push_named (id,_,_ as 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 senv' = add_constraints cst senv in
+  let env'' = safe_push_named (id,Some c,typ) senv'.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''})
+  let senv' = add_constraints cst senv in
+  let env'' = safe_push_named (id,None,t) senv'.env in
+  (cst, {senv' with env=env''})
 
 
 (* Insertion of constants and parameters in environment. *)
@@ -154,18 +212,18 @@ let add_constant dir l decl senv =
 	  let cb = translate_recipe senv.env kn r in
 	    if dir = empty_dirpath then hcons_constant_body cb else cb
   in
-  let env' = Environ.add_constraints cb.const_constraints senv.env in
-  let env'' = Environ.add_constant kn cb env' in
-    kn, { old = senv.old;
+  let senv' = add_constraints cb.const_constraints senv in
+  let env'' = Environ.add_constant kn cb senv'.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;
-          univ = senv.univ;
-          engagement = senv.engagement;
-	  imports = senv.imports;
-	  loads = senv.loads }
+	  modinfo = senv'.modinfo;
+	  labset = Labset.add l senv'.labset;
+	  revstruct = (l,SFBconst cb)::senv'.revstruct;
+          univ = senv'.univ;
+          engagement = senv'.engagement;
+	  imports = senv'.imports;
+	  loads = senv'.loads ;
+	  local_retroknowledge = senv'.local_retroknowledge }
     
 
 (* Insertion of inductive types. *)
@@ -182,67 +240,99 @@ let add_mind dir l mie senv =
     (* 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 senv' = add_constraints mib.mind_constraints senv in
   let kn = make_kn senv.modinfo.modpath dir l in
-  let env'' = Environ.add_mind kn mib env' in
-  kn, { old = senv.old;
+  let env'' = Environ.add_mind kn mib senv'.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;
-        univ = senv.univ;
-        engagement = senv.engagement;
-	imports = senv.imports;
-	loads = senv.loads }
-
+	modinfo = senv'.modinfo;
+	labset = Labset.add l senv'.labset;  (* TODO: the same as above *)
+	revstruct = (l,SFBmind mib)::senv'.revstruct;
+        univ = senv'.univ;
+        engagement = senv'.engagement;
+	imports = senv'.imports;
+	loads = senv'.loads;
+        local_retroknowledge = senv'.local_retroknowledge }
 
 (* 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;
+  let mtb_expr,sub = translate_struct_entry senv.env mte  in
+  let mtb = { typ_expr = mtb_expr;
+	      typ_strength = None;
+	      typ_alias = sub} in
+  let senv' = add_constraints 
+    (struct_expr_constraints mtb_expr) senv in
+  let mp = MPdot(senv.modinfo.modpath, l) in
+  let env'' = Environ.add_modtype mp mtb senv'.env in
+  mp, { 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;
-        univ = senv.univ;
-        engagement = senv.engagement;
-	imports = senv.imports;
-	loads = senv.loads }
-
+	modinfo = senv'.modinfo;
+	labset = Labset.add l senv'.labset;
+	revstruct = (l,SFBmodtype mtb)::senv'.revstruct;
+        univ = senv'.univ;
+        engagement = senv'.engagement;
+	imports = senv'.imports;
+	loads = senv'.loads;
+        local_retroknowledge = senv'.local_retroknowledge }
 
 
 (* 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
-
+let full_add_module mp mb senv =
+  let senv = add_constraints (module_constraints mb) senv in
+  let env = Modops.add_module mp mb senv.env in
+    {senv with env = 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;
+  let senv' = full_add_module mp mb senv in
+  let is_functor,sub = Modops.update_subst senv'.env mb mp in
+  mp, { old = senv'.old;
+	env = senv'.env;
+	modinfo = 
+      if is_functor then
+	senv'.modinfo
+      else
+	{senv'.modinfo with 
+	   alias_subst = join senv'.modinfo.alias_subst sub};
+	labset = Labset.add l senv'.labset;
+	revstruct = (l,SFBmodule mb)::senv'.revstruct;
+        univ = senv'.univ;
+        engagement = senv'.engagement;
+	imports = senv'.imports;
+	loads = senv'.loads;
+        local_retroknowledge = senv'.local_retroknowledge }
+    
+let add_alias l mp senv =
+  check_label l senv.labset; 
+  let mp' = MPdot(senv.modinfo.modpath, l) in
+  let mp1 = scrape_alias mp senv.env in
+    (* we get all updated alias substitution {mp1.K\M}  that comes from mp1 *)
+  let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in
+    (* transformation of {mp1.K\M} to {mp.K\M}*)
+  let sub = update_subst sub (map_mp mp' mp1) in
+   (* transformation of {mp.K\M}  to {mp.K\M'} where M'=M{mp1\mp'}*)
+  let sub = join_alias sub (map_mp mp' mp1) in
+    (* we add the alias substitution  *)
+  let sub = add_mp mp' mp1 sub in
+  let env' = register_alias mp' mp senv.env in
+    mp', { old = senv.old;
 	env = env';
-	modinfo = senv.modinfo;
+	modinfo = { senv.modinfo with 
+		      alias_subst = join 
+	    senv.modinfo.alias_subst sub};
 	labset = Labset.add l senv.labset;
-	revsign = (l,SPBmodule mspec)::senv.revsign;
-	revstruct = (l,SEBmodule mb)::senv.revstruct;
+	revstruct = (l,SFBalias (mp,None))::senv.revstruct;
         univ = senv.univ;
         engagement = senv.engagement;
 	imports = senv.imports;
-	loads = senv.loads }
-
+	loads = senv.loads;
+        local_retroknowledge = senv.local_retroknowledge }
 
 (* Interactive modules *)
 
@@ -254,96 +344,213 @@ let start_module l senv =
 		  modpath = mp;
 		  seed = senv.modinfo.seed;
 		  label = l;
-		  variant = STRUCT [] }
+		  variant = STRUCT [];
+		  alias_subst = empty_subst}
   in
   mp, { old = senv;
 	env = senv.env;
 	modinfo = modinfo;
 	labset = Labset.empty;
-	revsign = [];
 	revstruct = [];
         univ = Univ.Constraint.empty;
         engagement = None;
 	imports = senv.imports;
-	loads = [] }
+	loads = [];
+	(* spiwack : not sure, but I hope it's correct *)
+        local_retroknowledge = [] }
 
 let end_module l restype senv = 
   let oldsenv = senv.old in
   let modinfo = senv.modinfo in
-  let restype = option_map (translate_modtype senv.env) restype in
-  let params = 
+  let restype = Option.map (translate_struct_entry senv.env) restype in
+  let params,is_functor = 
     match modinfo.variant with
       | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
-      | STRUCT params -> params
+      | STRUCT params -> params, (List.length params > 0)
   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 tb = 
+  let functorize_struct tb = 
     List.fold_left
-      (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb))
+      (fun mtb (arg_id,arg_b) -> 
+	SEBfunctor(arg_id,arg_b,mtb))
       tb
       params
   in
-  let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
-  let mtb, mod_user_type, cst = 
+   let auto_tb = 
+     SEBstruct (modinfo.msid, List.rev senv.revstruct)
+  in
+  let mod_typ,subst,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
+      | None ->  None,modinfo.alias_subst,Constraint.empty
+      | Some (res_tb,subst) -> 
+	  let cst = check_subtypes senv.env
+	    {typ_expr = auto_tb;
+	     typ_strength = None;
+	     typ_alias = modinfo.alias_subst}
+	    {typ_expr = res_tb;
+	     typ_strength = None;
+	     typ_alias = subst} in
+	  let mtb = functorize_struct res_tb in
+	    Some mtb,subst,cst
   in
+  let mexpr = functorize_struct auto_tb in
   let cst = Constraint.union cst senv.univ in
-  let mexpr = 
-    List.fold_left
-      (fun mtb (arg_id,arg_b) -> MEBfunctor (arg_id,arg_b,mtb))
-      (MEBstruct (modinfo.msid, List.rev senv.revstruct)) 
-      params
-  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 } 
+      mod_type = mod_typ;
+      mod_constraints = cst;
+      mod_alias = subst;
+      mod_retroknowledge = senv.local_retroknowledge }
   in
   let mp = MPdot (oldsenv.modinfo.modpath, l) in
   let newenv = oldsenv.env in
   let newenv = set_engagement_opt senv.engagement newenv in
-  let newenv = 
+  let senv'= {senv with env=newenv} in
+  let senv' = 
     List.fold_left
       (fun env (mp,mb) -> full_add_module mp mb env) 
-      newenv
-      senv.loads
+      senv'
+      (List.rev senv'.loads)
   in
+  let newenv = Environ.add_constraints cst senv'.env in
   let newenv = 
-    full_add_module mp mb newenv
+    Modops.add_module mp mb newenv
   in 
-  mp, { old = oldsenv.old;
+  let is_functor,subst = Modops.update_subst newenv mb mp in
+  let newmodinfo = 
+    if is_functor then
+      oldsenv.modinfo
+    else
+      { oldsenv.modinfo with 
+	  alias_subst = join 
+	  oldsenv.modinfo.alias_subst 
+	  subst };
+  in
+    mp, { old = oldsenv.old;
 	env = newenv;
-	modinfo = oldsenv.modinfo;
+	modinfo = newmodinfo;
 	labset = Labset.add l oldsenv.labset;
-	revsign = (l,SPBmodule mspec)::oldsenv.revsign;
-	revstruct = (l,SEBmodule mb)::oldsenv.revstruct;
-        univ = oldsenv.univ;
+	revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
+        univ = Univ.Constraint.union senv'.univ oldsenv.univ;
         (* engagement is propagated to the upper level *)
-        engagement = senv.engagement;
-	imports = senv.imports;
-	loads = senv.loads@oldsenv.loads }
-
-
+        engagement = senv'.engagement;
+	imports = senv'.imports;
+	loads = senv'.loads@oldsenv.loads;
+	local_retroknowledge = senv'.local_retroknowledge@oldsenv.local_retroknowledge }
+
+
+(* Include for module and module type*)
+ let add_include me senv =
+   let struct_expr,_ =  translate_struct_entry senv.env me in
+   let senv = add_constraints (struct_expr_constraints struct_expr) senv in
+   let msid,str = match (eval_struct senv.env struct_expr) with
+     | SEBstruct(msid,str_l) -> msid,str_l
+     | _ -> error ("You cannot Include a higher-order Module or Module Type" )
+   in
+   let mp_sup = senv.modinfo.modpath in
+   let str1 = subst_signature_msid msid mp_sup str in
+   let add senv (l,elem)  = 
+     check_label l senv.labset;
+     match elem with
+       | SFBconst cb ->
+	   let con = make_con mp_sup empty_dirpath l in
+	   let senv' = add_constraints cb.const_constraints senv in
+	   let env'' = Environ.add_constant con cb senv'.env in
+	     { old = senv'.old;
+	       env = env'';
+	       modinfo = senv'.modinfo;
+	       labset = Labset.add l senv'.labset;
+	       revstruct = (l,SFBconst cb)::senv'.revstruct;
+               univ = senv'.univ;
+               engagement = senv'.engagement;
+	       imports = senv'.imports;
+	       loads = senv'.loads ;
+	       local_retroknowledge = senv'.local_retroknowledge }
+	       	     
+       | SFBmind mib ->
+	   let kn = make_kn mp_sup empty_dirpath l in
+	   let senv' = add_constraints mib.mind_constraints senv in
+	   let env'' = Environ.add_mind kn mib senv'.env in
+	     { old = senv'.old;
+	       env = env'';
+	       modinfo = senv'.modinfo;
+	       labset = Labset.add l senv'.labset;  
+	       revstruct = (l,SFBmind mib)::senv'.revstruct;
+               univ = senv'.univ;
+               engagement = senv'.engagement;
+	       imports = senv'.imports;
+	       loads = senv'.loads;
+               local_retroknowledge = senv'.local_retroknowledge }
+	       
+       | SFBmodule mb ->
+	   let mp = MPdot(senv.modinfo.modpath, l) in
+	   let is_functor,sub = Modops.update_subst senv.env mb mp in
+	   let senv' = full_add_module mp mb senv in
+	     { old = senv'.old;
+	       env = senv'.env;
+	       modinfo = 
+		 if is_functor then
+		   senv'.modinfo
+		 else
+		   {senv'.modinfo with 
+		      alias_subst = join senv'.modinfo.alias_subst sub};
+	       labset = Labset.add l senv'.labset;
+	       revstruct = (l,SFBmodule mb)::senv'.revstruct;
+	       univ = senv'.univ;
+	       engagement = senv'.engagement;
+	       imports = senv'.imports;
+	       loads = senv'.loads;
+	       local_retroknowledge = senv'.local_retroknowledge }
+       | SFBalias (mp',cst) ->
+	   let env' = Option.fold_right 
+	     Environ.add_constraints cst senv.env in
+	   let mp = MPdot(senv.modinfo.modpath, l) in
+	   let mp1 = scrape_alias mp' senv.env in
+	   let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in
+	   let sub = update_subst sub (map_mp mp mp1) in
+	   let sub = join_alias sub (map_mp mp mp1) in
+	   let sub = add_mp mp mp1 sub in
+	   let env' = register_alias mp mp' env' in
+	     { old = senv.old;
+	       env = env';
+	       modinfo =  { senv.modinfo with 
+			      alias_subst = join 
+		   senv.modinfo.alias_subst sub};
+	       labset = Labset.add l senv.labset;
+	       revstruct = (l,SFBalias (mp',cst))::senv.revstruct;
+               univ = senv.univ;
+               engagement = senv.engagement;
+	       imports = senv.imports;
+	       loads = senv.loads;
+               local_retroknowledge = senv.local_retroknowledge }
+       | SFBmodtype mtb ->
+	   let env' = add_modtype_constraints senv.env mtb in
+	   let mp = MPdot(senv.modinfo.modpath, l) in
+	   let env'' = Environ.add_modtype mp mtb env' in
+	     { old = senv.old;
+	       env = env'';
+	       modinfo = senv.modinfo;
+	       labset = Labset.add l senv.labset;
+	       revstruct = (l,SFBmodtype mtb)::senv.revstruct;
+               univ = senv.univ;
+               engagement = senv.engagement;
+	       imports = senv.imports;
+	       loads = senv.loads;
+               local_retroknowledge = senv.local_retroknowledge }
+   in
+     List.fold_left add senv str1
+	   
 (* Adding parameters to modules or module types *)
 
 let add_module_parameter mbid mte senv =
-  if senv.revsign <> [] or senv.revstruct <> [] or senv.loads <> [] then
+  if  senv.revstruct <> [] or senv.loads <> [] then
     anomaly "Cannot add a module parameter to a non empty module";
-  let mtb = translate_modtype senv.env mte in
-  let env = full_add_module (MPbound mbid) (module_body_of_type mtb) senv.env 
+  let mtb_expr,sub = translate_struct_entry senv.env mte in
+  let mtb = {typ_expr = mtb_expr;
+	    typ_strength = None;
+	    typ_alias = sub} in
+  let senv = full_add_module (MPbound mbid) (module_body_of_type mtb) senv 
   in
   let new_variant = match senv.modinfo.variant with
     | STRUCT params -> STRUCT ((mbid,mtb) :: params)
@@ -352,15 +559,15 @@ let add_module_parameter mbid mte senv =
 	anomaly "Module parameters can only be added to modules or signatures"
   in
   { old = senv.old;
-    env = env;
+    env = senv.env;
     modinfo = { senv.modinfo with variant = new_variant };
     labset = senv.labset;
-    revsign = [];
     revstruct = [];
     univ = senv.univ;
     engagement = senv.engagement;
     imports = senv.imports;
-    loads = [] }
+    loads = [];
+    local_retroknowledge = senv.local_retroknowledge }
 
 
 (* Interactive module types *)
@@ -373,18 +580,20 @@ let start_modtype l senv =
 		  modpath = mp;
 		  seed = senv.modinfo.seed;
 		  label = l;
-		  variant = SIG [] }
+		  variant = SIG [];
+		  alias_subst = empty_subst }
   in
   mp, { old = senv;
 	env = senv.env;
 	modinfo = modinfo;
 	labset = Labset.empty;
-	revsign = [];
 	revstruct = [];
         univ = Univ.Constraint.empty;
         engagement = None;
 	imports = senv.imports;
-	loads = [] }
+	loads = [] ;
+	(* spiwack: not 100% sure, but I think it should be like that *)
+        local_retroknowledge = []}
 
 let end_modtype l senv = 
   let oldsenv = senv.old in
@@ -396,52 +605,55 @@ let end_modtype l senv =
   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 = 
+  let auto_tb = 
+     SEBstruct (modinfo.msid, List.rev senv.revstruct)
+  in
+  let mtb_expr = 
     List.fold_left
-      (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb))
-      res_tb
+      (fun mtb (arg_id,arg_b) -> 
+	 SEBfunctor(arg_id,arg_b,mtb))
+      auto_tb
       params
   in
-  let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in
+  let mp = MPdot (oldsenv.modinfo.modpath, l) in
   let newenv = oldsenv.env in
   (* since universes constraints cannot be stored in the modtype,
      they are propagated to the upper level *)
-  let newenv = add_constraints senv.univ  newenv in
+  let newenv = Environ.add_constraints senv.univ  newenv in
   let newenv = set_engagement_opt senv.engagement newenv in
-  let newenv = 
+  let senv = {senv with env=newenv} in
+  let senv = 
     List.fold_left
       (fun env (mp,mb) -> full_add_module mp mb env) 
-      newenv
-      senv.loads
-  in
-  let newenv = 
-    add_modtype_constraints newenv mtb 
+      senv
+      (List.rev senv.loads)
   in
+  let subst = senv.modinfo.alias_subst in
+  let mtb = {typ_expr = mtb_expr;
+	    typ_strength = None;
+	    typ_alias = subst} in
   let newenv = 
-    Environ.add_modtype kn mtb newenv
+    Environ.add_modtype mp mtb senv.env
   in 
-  kn, { old = oldsenv.old;
-	env = newenv;
+    mp, { 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;
+	revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
         univ = Univ.Constraint.union senv.univ oldsenv.univ;
         engagement = senv.engagement;
 	imports = senv.imports;
-	loads = senv.loads@oldsenv.loads }
+	loads = senv.loads@oldsenv.loads;
+        (* spiwack : if there is a bug with retroknowledge in nested modules
+                     it's likely to come from here *)
+        local_retroknowledge = 
+                   senv.local_retroknowledge@oldsenv.local_retroknowledge}
   
 
 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;
-    univ = Univ.Constraint.union cst senv.univ }
-
 (* Check that the engagement expected by a library matches the initial one *)
 let check_engagement env c =
   match Environ.engagement env, c with
@@ -460,12 +672,11 @@ let set_engagement c senv =
 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 is_empty senv =
-  senv.revsign = [] &&
+  senv.revstruct = [] &&
   senv.modinfo.msid = initial_msid &&
   senv.modinfo.variant = NONE
 
@@ -484,18 +695,20 @@ let start_library dir senv =
 		  modpath = mp;
 		  seed = dir;
 		  label = l;
-		  variant = LIBRARY dir }
+		  variant = LIBRARY dir;
+		  alias_subst = empty_subst }
   in
   mp, { old = senv;
 	env = senv.env;
 	modinfo = modinfo;
 	labset = Labset.empty;
-	revsign = [];
 	revstruct = [];
         univ = Univ.Constraint.empty;
         engagement = None;
 	imports = senv.imports;
-	loads = [] }
+	loads = [];
+        local_retroknowledge = [] }
+
 
 
 let export senv dir = 
@@ -511,11 +724,11 @@ let export senv dir =
   (*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 = senv.univ }
+    { mod_expr = Some (SEBstruct (modinfo.msid, List.rev senv.revstruct));
+      mod_type = None;
+      mod_constraints = senv.univ;
+      mod_alias = senv.modinfo.alias_subst;
+      mod_retroknowledge = senv.local_retroknowledge}
   in
     modinfo.msid, (dir,mb,senv.imports,engagement senv.env)
 
@@ -532,6 +745,8 @@ let check_imports senv needed =
   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:
@@ -550,56 +765,46 @@ let import (dp,mb,depends,engmt) digest senv =
   check_engagement senv.env engmt;
   let mp = MPfile dp in
   let env = senv.env in
+  let env = Environ.add_constraints mb.mod_constraints env in
+  let env = Modops.add_module mp mb env in
   mp, { senv with 
-	  env = full_add_module mp mb env; 
+	  env = env; 
 	  imports = (dp,digest)::senv.imports;
 	  loads = (mp,mb)::senv.loads }
 
 
 (* Remove the body of opaque constants in modules *)
- 
-let rec lighten_module mb =
+ let rec lighten_module mb =
   { mb with
-    mod_expr = option_map lighten_modexpr mb.mod_expr;
-    mod_type = lighten_modtype mb.mod_type;
-    mod_user_type = option_map 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
-
+    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
-    | 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))
+    | 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
-  | 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)
-
+  | 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)
 
 
@@ -611,3 +816,6 @@ 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)
+
+
+
-- 
cgit v1.2.3