La notation 'with'. L'interpretation - version preliminaire

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

9 files changed, 146 insertions, 44 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 8b1170597..05989bc82 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -148,7 +148,8 @@ and module_expr_body =
   | MEBapply of module_expr_body * module_expr_body
       * constraints
 
-and module_specification_body = module_type_body * module_path option
+and module_specification_body = 
+    module_type_body * module_path option * constraints
 
 and structure_elem_body = 
   | SEBconst of constant_body
@@ -160,6 +161,7 @@ and module_structure_body = (label * structure_elem_body) list
 
 and module_body = 
     { mod_expr : module_expr_body option;
-      mod_user_type : (module_type_body * constraints) option;
+      mod_user_type : module_type_body option;
       mod_type : module_type_body;
-      mod_equiv : module_path option }
+      mod_equiv : module_path option;
+      mod_constraints : constraints }
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 574cb04fa..eeec64875 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -107,7 +107,8 @@ and module_expr_body =
   | MEBapply of module_expr_body * module_expr_body
       * constraints
 
-and module_specification_body = module_type_body * module_path option
+and module_specification_body = 
+    module_type_body * module_path option * constraints
 
 and structure_elem_body = 
   | SEBconst of constant_body
@@ -119,9 +120,10 @@ and module_structure_body = (label * structure_elem_body) list
 
 and module_body = 
     { mod_expr : module_expr_body option;
-      mod_user_type : (module_type_body * constraints) option;
+      mod_user_type : module_type_body option;
       mod_type : module_type_body;
-      mod_equiv : module_path option }
+      mod_equiv : module_path option;
+      mod_constraints : constraints }
 
 
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 4d86d6d2c..edba6e608 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -78,10 +78,13 @@ and module_type_entry =
     MTEident of kernel_name
   | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
   | MTEsig of mod_self_id * module_signature_entry
+  | MTEwith of module_type_entry * with_declaration
 
 and module_signature_entry = (label * specification_entry) list
 
-
+and with_declaration = 
+    With_Module of identifier * module_path
+  | With_Definition of identifier * constr
 
 and module_expr = 
     MEident of module_path
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 4d86d6d2c..edba6e608 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -78,10 +78,13 @@ and module_type_entry =
     MTEident of kernel_name
   | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
   | MTEsig of mod_self_id * module_signature_entry
+  | MTEwith of module_type_entry * with_declaration
 
 and module_signature_entry = (label * specification_entry) list
 
-
+and with_declaration = 
+    With_Module of identifier * module_path
+  | With_Definition of identifier * constr
 
 and module_expr = 
     MEident of module_path
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 1eb74ffef..2c00fe52e 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -24,6 +24,15 @@ let path_of_mexpr = function
   | MEident mb -> mb
   | _ -> raise Not_path
 
+let rec replace_first p k = function 
+  | [] -> [] 
+  | h::t when p h -> k::t
+  | h::t -> h::(replace_first p k t)
+
+let rec list_split_assoc k rev_before = function
+  | [] -> raise Not_found
+  | (k',b)::after when k=k' -> rev_before,b,after
+  | h::tail -> list_split_assoc k (h::rev_before) tail
 
 let rec list_fold_map2 f e = function 
   |  []  -> (e,[],[])
@@ -47,6 +56,70 @@ let rec translate_modtype env mte =
     | MTEsig (msid,sig_e) ->
 	let str_b,sig_b = translate_entry_list env msid false sig_e in
 	  MTBsig (msid,sig_b)
+    | MTEwith (mte, with_decl) ->
+	let mtb = translate_modtype env mte in
+	  merge_with env mtb with_decl
+
+and merge_with env mtb with_decl = 
+  let msid,sig_b = match (Modops.scrape_modtype env mtb) with 
+    | MTBsig(msid,sig_b) -> msid,sig_b 
+    | _ -> error_signature_expected mtb
+  in
+  let id = match with_decl with 
+    | With_Definition (id,_) | With_Module (id,_) -> id
+  in
+  let l = label_of_id id in
+    try
+      let rev_before,spec,after = list_split_assoc l [] sig_b in
+      let before = List.rev rev_before in
+      let env' = Modops.add_signature (MPself msid) before env in
+      let new_spec = match with_decl with
+	| With_Definition (id,c) -> 
+	    let cb = match spec with
+		SPBconst cb -> cb
+	      | _ -> error_not_a_constant l
+	    in 
+	      begin
+		match cb.const_body with
+		  | None -> 
+		      let (j,cst1) = Typeops.infer env' c in
+		      let cst2 = 
+			Reduction.conv_leq env' j.uj_type cb.const_type in
+		      let cst = 
+			Constraint.union 
+			  (Constraint.union cb.const_constraints cst1)
+			  cst2
+		      in
+			SPBconst {cb with 
+				    const_body = Some j.uj_val;
+				    const_constraints = cst}
+		  | Some b -> 
+		      let cst1 = Reduction.conv env' c b in 
+		      let cst = Constraint.union cb.const_constraints cst1 in
+			SPBconst {cb with 
+				    const_body = Some c;
+				    const_constraints = cst}
+	      end	
+	| With_Module (id, mp) ->
+	    let (oldmtb,oldequiv,oldcst) = match spec with
+		SPBmodule (mtb,equiv,cst) -> (mtb,equiv,cst)
+	      | _ -> error_not_a_module (string_of_label l)
+	    in
+	    let mtb = type_modpath env' mp in
+	    let cst = check_subtypes env' mtb oldmtb in
+	    let equiv = 
+ 	      match oldequiv with
+		| None -> Some mp
+		| Some mp' -> 
+		    check_modpath_equiv env' mp mp';
+		    Some mp
+	    in
+	      SPBmodule (mtb, equiv, Constraint.union oldcst cst)
+      in
+	MTBsig(msid,  before@(l,new_spec)::after)
+    with
+	Not_found -> error_no_such_label l
+      | Reduction.NotConvertible -> error_with_incorrect l
 
 and translate_entry_list env msid is_definition sig_e = 
   let mp = MPself msid in
@@ -61,7 +134,7 @@ and translate_entry_list env msid is_definition sig_e =
 	    add_mind kn mib env, (l, SEBmind mib), (l, SPBmind mib)
       | SPEmodule me ->
 	  let mb = translate_module env is_definition me in
-	  let mspec = mb.mod_type, mb.mod_equiv in
+	  let mspec = mb.mod_type, mb.mod_equiv, mb.mod_constraints in
 	  let mp' = MPdot (mp,l) in
 	    add_module mp' mb env, (l, SEBmodule mb), (l, SPBmodule mspec)
       | SPEmodtype mte ->
@@ -82,9 +155,10 @@ and translate_module env is_definition me =
     | None, Some mte -> 
 	let mtb = translate_modtype env mte in
 	{ mod_expr = None;
-	  mod_user_type = Some (mtb, Constraint.empty);
+	  mod_user_type = Some mtb;
 	  mod_type = mtb;
-	  mod_equiv = None }
+	  mod_equiv = None;
+	  mod_constraints = Constraint.empty }
     | Some mexpr, _ -> 
 	let meq_o = (* do we have a transparent module ? *)
 	  try       (* TODO: transparent field in module_entry *)
@@ -104,17 +178,18 @@ and translate_module env is_definition me =
 	    in
 	      MEBident mp, type_modpath env mp
 	in
-	let mtb,mod_user_type =
+	let mtb, mod_user_type, cst =
 	  match me.mod_entry_type with
-	    | None -> mtb1, None
+	    | None -> mtb1, None, Constraint.empty
 	    | Some mte -> 
 		let mtb2 = translate_modtype env mte in
-		  mtb2, Some (mtb2, check_subtypes env mtb1 mtb2)
+		  mtb2, Some mtb2, check_subtypes env mtb1 mtb2
 	in
 	  { mod_type = mtb;
 	    mod_user_type = mod_user_type;
 	    mod_expr = Some meb;
-	    mod_equiv = meq_o }
+	    mod_equiv = meq_o;
+	    mod_constraints = cst }
 
 (* translate_mexpr : env -> module_expr -> module_expr_body * module_type_body *)
 and translate_mexpr env mexpr = match mexpr with
@@ -180,12 +255,7 @@ and add_module_constraints env mb =
     | None -> env
     | Some meb -> add_module_expr_constraints env meb
   in
-  let env = match mb.mod_user_type with
-    | None -> env
-    | Some (mtb,cst) -> 
-	Environ.add_constraints cst (add_modtype_constraints env mtb)
-  in
-    env
+    Environ.add_constraints mb.mod_constraints env
 
 and add_modtype_constraints env = function
   | MTBident _ -> env
@@ -202,7 +272,8 @@ and add_modtype_constraints env = function
 and add_sig_elem_constraints env = function 
   | SPBconst cb -> Environ.add_constraints cb.const_constraints env
   | SPBmind mib -> Environ.add_constraints mib.mind_constraints env
-  | SPBmodule (mtb,_) -> add_modtype_constraints env mtb
+  | SPBmodule (mtb,_,cst) -> 
+      add_modtype_constraints (Environ.add_constraints cst env) mtb
   | SPBmodtype mtb -> add_modtype_constraints env mtb
 
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index ea8a2c4e2..d4338f0fb 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -11,6 +11,7 @@
 (*i*)
 open Util
 open Names
+open Univ
 open Term
 open Declarations
 open Environ
@@ -41,6 +42,9 @@ let error_incompatible_labels l l' =
 let error_result_must_be_signature mtb = 
   error "The result module type must be a signature"
 
+let error_signature_expected mtb =
+  error "Signature expected"
+
 let error_no_module_to_end _ = 
   error "No open module to end"
 
@@ -53,25 +57,33 @@ let error_not_a_modtype s =
 let error_not_a_module s = 
   error ("\""^s^"\" is not a module")
 
+let error_not_a_constant l = 
+  error ("\""^(string_of_label l)^"\" is not a constant")
+
+let error_with_incorrect l =
+  error ("Incorrect constraint for label \""^(string_of_label l)^"\"")
 
 let rec scrape_modtype env = function
   | MTBident kn -> scrape_modtype env (lookup_modtype kn env)
   | mtb -> mtb
 
 
-let module_body_of_spec spec = 
-  { mod_type = fst spec;
-    mod_equiv = snd spec;
-    mod_expr = None;
-    mod_user_type = None}
+let module_body_of_spec (mty,mpo,cst) = 
+    { mod_type = mty;
+      mod_equiv = mpo;
+      mod_expr = None;
+      mod_user_type = None;
+      mod_constraints = cst}
 
 let module_body_of_type mtb = 
   { mod_type = mtb;
     mod_equiv = None;
     mod_expr = None;
-    mod_user_type = None}
+    mod_user_type = None;
+    mod_constraints = Constraint.empty}
+
 
-let module_spec_of_body mb = mb.mod_type, mb.mod_equiv
+let module_spec_of_body mb = mb.mod_type, mb.mod_equiv, mb.mod_constraints
 
 let destr_functor = function
   | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
@@ -114,11 +126,11 @@ and subst_signature sub sign =
   in
     List.map (fun (l,b) -> (l,subst_body b)) sign
 
-and subst_module sub (mtb,mpo as mb) =
+and subst_module sub (mtb,mpo,cst as mb) =
   let mtb' = subst_modtype sub mtb in
   let mpo' = option_smartmap (subst_mp sub) mpo in
     if mtb'==mtb && mpo'==mpo then mb else
-      (mtb',mpo')
+      (mtb',mpo',cst)
 
 let subst_signature_msid msid mp = 
   subst_signature (map_msid msid mp)
@@ -161,13 +173,13 @@ let rec strengthen_mtb env mp mtb = match scrape_modtype env mtb with
   | MTBident _ -> anomaly "scrape_modtype does not work!"
   | MTBfunsig _ -> mtb
   | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp)
-and strengthen_mod env mp (mtb,mpo) = 
+and strengthen_mod env mp (mtb,mpo,cst) = 
   let mtb' = strengthen_mtb env mp mtb in
   let mpo' = match mpo with
     | Some _ -> mpo
     | None -> Some mp
   in
-    (mtb',mpo')
+    (mtb',mpo',cst)
 and strengthen_sig env msid sign mp = match sign with
   | [] -> []
   | (l,SPBconst cb) :: rest ->
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 7cd22c57c..68f8ea38a 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -74,6 +74,8 @@ val error_no_such_label : label -> 'a
 
 val error_result_must_be_signature : module_type_body -> 'a
 
+val error_signature_expected : module_type_body -> 'a
+
 val error_no_module_to_end : unit -> 'a 
 
 val error_no_modtype_to_end : unit -> 'a
@@ -81,3 +83,7 @@ val error_no_modtype_to_end : unit -> 'a
 val error_not_a_modtype : string -> 'a 
 
 val error_not_a_module : string -> 'a 
+
+val error_not_a_constant : label -> 'a
+
+val error_with_incorrect : label -> 'a
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 909b12704..22d45861e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -262,13 +262,13 @@ let end_module l senv =
       params
   in
   let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
-  let mtb, mod_user_type = 
+  let mtb, mod_user_type, cst = 
     match restype with
-      | None -> functorize_type auto_tb, None
+      | None -> functorize_type auto_tb, None, Constraint.empty
       | Some res_tb -> 
-	  let cnstrs = check_subtypes senv.env auto_tb res_tb in
+	  let cst = check_subtypes senv.env auto_tb res_tb in
 	  let mtb = functorize_type res_tb in
-	    mtb, Some (mtb, cnstrs)
+	    mtb, Some mtb, cst
   in
   let mexpr = 
     List.fold_right
@@ -280,9 +280,10 @@ let end_module l senv =
     { mod_expr = Some mexpr;
       mod_user_type = mod_user_type;
       mod_type = mtb;
-      mod_equiv = None }
+      mod_equiv = None;
+      mod_constraints = cst }
   in
-  let mspec = mtb , None in
+  let mspec = mtb, None, Constraint.empty in
   let mp = MPdot (oldsenv.modinfo.modpath, l) in
   let newenv = oldsenv.env in
   let newenv = 
@@ -438,7 +439,8 @@ let export senv dir =
     { 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_equiv = None;
+      mod_constraints = Constraint.empty }
   in
     modinfo.msid, (dir,mb,senv.imports)
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index f62725c70..fa024b7f2 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -182,12 +182,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
 	    c2
 *)
 
-let rec check_modules cst env msid1 l msb1 msb2 =
+let rec check_modules cst env msid1 l 
+  (mtb1,mpo1,cst1 as msb1) (mtb2,mpo2,cst2 as msb2) =
   let mp = (MPdot(MPself msid1,l)) in
-  let mty1 = strengthen env (fst msb1) mp in
-  let cst = check_modtypes cst env mty1 (fst msb2) false in
+  let mty1 = strengthen env mtb1 mp in
+  let cst = check_modtypes cst env mty1 mtb2 false in
   begin
-    match (snd msb1), (snd msb2) with
+    match mpo1, mpo2 with
       | _, None -> ()
       | None, Some mp2 -> 
 	  check_modpath_equiv env mp mp2