Mod_typing : code cleanup

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

1 files changed, 181 insertions, 196 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index befa822ce..d5555c624 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -12,15 +12,12 @@
 (* This module provides the main functions for type-checking module
    declarations *)
 
-open Errors
 open Util
 open Names
-open Univ
 open Declarations
 open Entries
 open Environ
 open Modops
-open Subtyping
 open Mod_subst
 
 exception Not_path
@@ -39,10 +36,16 @@ let is_modular = function
   | SFBmodule _ | SFBmodtype _ -> true
   | SFBconst _ | SFBmind _ -> false
 
-let rec list_split_assoc ((k,m) as km) rev_before = function
-  | [] -> raise Not_found
-  | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) -> rev_before,b,after
-  | h::tail -> list_split_assoc km (h::rev_before) tail
+(** Split a [structure_body] at some label corresponding to
+    a modular definition or not. *)
+
+let split_sign k m struc =
+  let rec split rev_before = function
+    | [] -> raise Not_found
+    | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) ->
+      List.rev rev_before,b,after
+    | h::tail -> split (h::rev_before) tail
+  in split [] struc
 
 let discr_resolver mtb = match mtb.typ_expr with
   | SEBstruct _ -> mtb.typ_delta
@@ -50,184 +53,170 @@ let discr_resolver mtb = match mtb.typ_expr with
 
 let rec rebuild_mp mp l =
   match l with
-      []-> mp
-    | i::r -> rebuild_mp (MPdot(mp,i)) r 
-	
-let rec check_with env sign with_decl alg_sign mp equiv = 
-  let sign,wd,equiv,cst= match with_decl with
-    | With_Definition (idl,c) ->
-	let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in
-	sign,With_definition_body(idl,cb),equiv,cst
-    | With_Module (idl,mp1) ->
-	let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in
-	sign,With_module_body(idl,mp1),equiv,cst
-  in
-  match alg_sign with
-  | None ->
-    sign, None, equiv, cst
-  | Some s ->
-    sign,Some (SEBwith(s, wd)),equiv,cst
+  | []-> mp
+  | i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r
+
+let (+++) = Univ.union_constraints
 
-and check_with_def env sign (idl,c) mp equiv =
-  let sig_b = match sign with 
+let rec check_with_def env sign (idl,c) mp equiv =
+  let sig_b = match sign with
     | SEBstruct(sig_b) -> sig_b
     | _ -> error_signature_expected sign
   in
-  let id,idl = match idl with
+  let lab,idl = match idl with
     | [] -> assert false
-    | id::idl -> id,idl
+    | id::idl -> Label.of_id id, idl
   in
-  let l = Label.of_id id in
-    try
-      let not_empty = match idl with [] -> false | _ :: _ -> true in
-      let rev_before,spec,after = list_split_assoc (l, not_empty) [] sig_b in
-      let before = List.rev rev_before in
-      let env' = Modops.add_signature mp before equiv env in
-      match idl with [] ->
-	      (* Toplevel definition *)
-	      let cb = match spec with
-		| SFBconst cb -> cb
-		| _ -> error_not_a_constant l
-	      in
-	      (* In the spirit of subtyping.check_constant, we accept
-                 any implementations of parameters and opaques terms,
-	         as long as they have the right type *)
-	      let def,cst = match cb.const_body with
-		| Undef _ | OpaqueDef _ ->
-		    let (j,cst1) = Typeops.infer env' c in
-		    let typ = Typeops.type_of_constant_type env' cb.const_type in
-		    let cst2 = Reduction.conv_leq env' j.uj_type typ in
-		    let cst = union_constraints
-			(union_constraints
-                          (Future.force cb.const_constraints) cst1)
-			cst2
-		    in
-		    let def = Def (Lazyconstr.from_val j.uj_val) in
-		    def,cst
-		| Def cs ->
-		    let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
-		    let cst = union_constraints
-                      (Future.force cb.const_constraints) cst1 in
-		    let def = Def (Lazyconstr.from_val c) in
-		    def,cst
-	      in
-	      let cb' =
-		{ cb with
-		  const_body = def;
-		  const_body_code =
-		    Cemitcodes.from_val (compile_constant_body env' def);
-		  const_constraints = Future.from_val cst }
-	      in
-	      SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst
-      | _ ->
-	      (* Definition inside a sub-module *)
-	      let old = match spec with
-		| SFBmodule msb -> msb
-		| _ -> error_not_a_module (Label.to_string l)
-	      in
-		begin
-		  match old.mod_expr with
-                    | None ->
-			let sign,cb,cst = 
-			  check_with_def env' old.mod_type (idl,c)
-			    (MPdot(mp,l)) old.mod_delta in
-			let new_spec = SFBmodule({old with
-						    mod_type = sign;
-						    mod_type_alg = None}) in
-			  SEBstruct(before@(l,new_spec)::after),cb,cst
-                    | Some msb ->
-			error_generative_module_expected l
-		end
-    with
-      | Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_incorrect_with_constraint l
-
-and check_with_mod env sign (idl,mp1) mp equiv = 
-  let sig_b = match sign with 
-    | SEBstruct(sig_b) ->sig_b
+  try
+    let modular = not (List.is_empty idl) in
+    let before,spec,after = split_sign lab modular sig_b in
+    let env' = Modops.add_signature mp before equiv env in
+    if List.is_empty idl then
+      (* Toplevel definition *)
+      let cb = match spec with
+	| SFBconst cb -> cb
+	| _ -> error_not_a_constant lab
+      in
+      (* In the spirit of subtyping.check_constant, we accept
+         any implementations of parameters and opaques terms,
+	 as long as they have the right type *)
+      let def,cst = match cb.const_body with
+	| Undef _ | OpaqueDef _ ->
+	  let j,cst1 = Typeops.infer env' c in
+	  let typ = Typeops.type_of_constant_type env' cb.const_type in
+	  let cst2 = Reduction.conv_leq env' j.uj_type typ in
+	  let cst = Future.force cb.const_constraints +++ cst1 +++ cst2 in
+	  let def = Def (Lazyconstr.from_val j.uj_val) in
+	  def,cst
+	| Def cs ->
+	  let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
+	  let cst = Future.force cb.const_constraints +++ cst1 in
+	  let def = Def (Lazyconstr.from_val c) in
+	  def,cst
+      in
+      let cb' =
+	{ cb with
+	  const_body = def;
+	  const_body_code = Cemitcodes.from_val (compile_constant_body env' def);
+	  const_constraints = Future.from_val cst }
+      in
+      SEBstruct(before@(lab,SFBconst(cb'))::after),cb',cst
+    else
+      (* Definition inside a sub-module *)
+      let mb = match spec with
+	| SFBmodule mb -> mb
+	| _ -> error_not_a_module (Label.to_string lab)
+      in
+      begin match mb.mod_expr with
+      | Some _ -> error_generative_module_expected lab
+      | None ->
+	let sign,cb,cst =
+          check_with_def env' mb.mod_type (idl,c) (MPdot(mp,lab)) mb.mod_delta
+        in
+        let mb' = { mb with
+          mod_type = sign;
+	  mod_type_alg = None }
+        in
+	SEBstruct(before@(lab,SFBmodule mb')::after),cb,cst
+      end
+  with
+  | Not_found -> error_no_such_label lab
+  | Reduction.NotConvertible -> error_incorrect_with_constraint lab
+
+let rec check_with_mod env sign (idl,mp1) mp equiv =
+  let sig_b = match sign with
+    | SEBstruct(sig_b) -> sig_b
     | _ -> error_signature_expected sign
   in
-  let id,idl = match idl with
+  let lab,idl = match idl with
     | [] -> assert false
-    | id::idl -> id,idl
+    | id::idl -> Label.of_id id, idl
   in
-  let l = Label.of_id id in
-    try
-      let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in
-      let before = List.rev rev_before in
-      let env' = Modops.add_signature mp before equiv env in
-      match idl with [] ->
-	      (* Toplevel module definition *)
-	      let old = match spec with
-		  SFBmodule msb -> msb
-		| _ -> error_not_a_module (Label.to_string l)
-	      in
-	      let mb_mp1 = (lookup_module mp1 env) in
-	      let mtb_mp1 = 
-		module_type_of_module None mb_mp1  in
-	      let cst =
-		match old.mod_expr with
-		    None ->
-		      begin
-			try union_constraints
-			  (check_subtypes env' mtb_mp1 
-			     (module_type_of_module None old))
-			  old.mod_constraints
-			with Failure _ -> error_incorrect_with_constraint (Label.of_id id)
-		      end
-		  | Some (SEBident(mp')) ->
-		      check_modpath_equiv env' mp1 mp';
-		      old.mod_constraints
-		  | _ ->  error_generative_module_expected l
-	      in
-	      let new_mb = strengthen_and_subst_mb mb_mp1 (MPdot(mp,l)) false
-	      in
-	      let new_spec = SFBmodule {new_mb with 
-					  mod_mp = MPdot(mp,l);
-					  mod_expr = Some (SEBident mp1);
-					  mod_constraints = cst} in
-		(* we propagate the new equality in the rest of the signature
-		   with the identity substitution accompagned by the new resolver*)
-	      let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in
-		SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
-	      add_delta_resolver equiv new_mb.mod_delta,cst
-      | _ ->
-	      (* Module definition of a sub-module *)
-	      let old = match spec with
-		  SFBmodule msb -> msb
-		| _ -> error_not_a_module (Label.to_string l)
-	      in
-	      begin
-		match old.mod_expr with
-		    None ->
-		      let sign,equiv',cst =
-			check_with_mod env'
-			  old.mod_type (idl,mp1) (MPdot(mp,l)) old.mod_delta in
-		      let new_equiv = add_delta_resolver equiv equiv' in
-		      let new_spec = SFBmodule {old with 
-						  mod_type = sign;
-						  mod_type_alg = None;
-						  mod_delta = equiv'}
-		      in
-		      let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) equiv' in
-			SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
-		      new_equiv,cst
-		  | Some (SEBident(mp')) ->
-		      let mpnew = rebuild_mp mp' (List.map Label.of_id idl) in
-			check_modpath_equiv env' mpnew mp;
-			  SEBstruct(before@(l,spec)::after)
-			    ,equiv,empty_constraint
-		  | _ ->
-		      error_generative_module_expected l
-              end
-    with
-	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_incorrect_with_constraint l
-
-and translate_module env mp inl me =
+  try
+    let before,spec,after = split_sign lab true sig_b in
+    let env' = Modops.add_signature mp before equiv env in
+    let old = match spec with
+      | SFBmodule mb -> mb
+      | _ -> error_not_a_module (Label.to_string lab)
+    in
+    if List.is_empty idl then
+      (* Toplevel module definition *)
+      let mb_mp1 = lookup_module mp1 env in
+      let mtb_mp1 = module_type_of_module None mb_mp1  in
+      let cst = match old.mod_expr with
+	| None ->
+	  begin
+            try
+              let mtb_old = module_type_of_module None old in
+              Subtyping.check_subtypes env' mtb_mp1 mtb_old
+                +++ old.mod_constraints
+	    with Failure _ -> error_incorrect_with_constraint lab
+	  end
+	| Some (SEBident(mp')) ->
+	  check_modpath_equiv env' mp1 mp';
+	  old.mod_constraints
+	| _ ->  error_generative_module_expected lab
+      in
+      let mp' = MPdot (mp,lab) in
+      let new_mb = strengthen_and_subst_mb mb_mp1 mp' false in
+      let new_mb' = {new_mb with
+        mod_mp = mp';
+        mod_expr = Some (SEBident mp1);
+        mod_constraints = cst }
+      in
+      (* we propagate the new equality in the rest of the signature
+	 with the identity substitution accompagned by the new resolver*)
+      let id_subst = map_mp mp' mp' new_mb.mod_delta in
+      SEBstruct(before@(lab,SFBmodule new_mb')::subst_signature id_subst after),
+      add_delta_resolver equiv new_mb.mod_delta,cst
+    else
+      (* Module definition of a sub-module *)
+      let mp' = MPdot (mp,lab) in
+      let old = match spec with
+        | SFBmodule msb -> msb
+	| _ -> error_not_a_module (Label.to_string lab)
+      in
+      begin match old.mod_expr with
+      | None ->
+	let sign,equiv',cst =
+	  check_with_mod env' old.mod_type (idl,mp1) mp' old.mod_delta in
+	let new_equiv = add_delta_resolver equiv equiv' in
+	let new_mb = { old with
+          mod_type = sign;
+          mod_type_alg = None;
+          mod_delta = equiv'}
+	in
+	let id_subst = map_mp mp' mp' equiv' in
+	SEBstruct(before@(lab,SFBmodule new_mb)::subst_signature id_subst after),
+	new_equiv,cst
+      | Some (SEBident mp0) ->
+	let mpnew = rebuild_mp mp0 idl in
+	check_modpath_equiv env' mpnew mp;
+	SEBstruct(before@(lab,spec)::after),equiv,Univ.empty_constraint
+      | _ -> error_generative_module_expected lab
+      end
+  with
+  | Not_found -> error_no_such_label lab
+  | Reduction.NotConvertible -> error_incorrect_with_constraint lab
+
+let check_with env sign with_decl alg_sign mp equiv =
+  let sign,wd,equiv,cst= match with_decl with
+    | With_Definition (idl,c) ->
+	let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in
+	sign,With_definition_body(idl,cb),equiv,cst
+    | With_Module (idl,mp1) ->
+	let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in
+	sign,With_module_body(idl,mp1),equiv,cst
+  in
+  match alg_sign with
+  | None -> sign, None, equiv, cst
+  | Some s -> sign, Some (SEBwith(s, wd)), equiv, cst
+
+let rec translate_module env mp inl me =
   match me.mod_entry_expr, me.mod_entry_type with
     | None, None ->
-	anomaly ~label:"Mod_typing.translate_module" (Pp.str "empty type and expr in module entry")
+	Errors.anomaly ~label:"Mod_typing.translate_module"
+          (Pp.str "empty type and expr in module entry")
     | None, Some mte ->
 	let mtb = translate_module_type env mp inl mte in
 	  { mod_mp = mp;
@@ -243,14 +232,14 @@ and translate_module env mp inl me =
 	let sign,alg1,resolver,cst2 =
 	  match me.mod_entry_type with
 	    | None ->
-		sign,None,resolver,empty_constraint
+		sign,None,resolver,Univ.empty_constraint
 	    | Some mte ->
 		let mtb = translate_module_type env mp inl mte in
-                let cst = check_subtypes env
+                let cst = Subtyping.check_subtypes env
 		  {typ_mp = mp;
 		   typ_expr = sign;
 		   typ_expr_alg = None;
-		   typ_constraints = empty_constraint;
+		   typ_constraints = Univ.empty_constraint;
 		   typ_delta = resolver;}
 		  mtb
 		in
@@ -260,7 +249,7 @@ and translate_module env mp inl me =
 	    mod_type = sign;
 	    mod_expr = alg_implem;
 	    mod_type_alg = alg1;
-	    mod_constraints = Univ.union_constraints cst1 cst2;
+	    mod_constraints = cst1 +++ cst2;
 	    mod_delta = resolver;
 	    mod_retroknowledge = []} 
 	    (* spiwack: not so sure about that. It may
@@ -276,15 +265,14 @@ and translate_apply env inl ftrans mexpr mkalg =
     with Not_path -> error_application_to_not_path mexpr
   in
   let mtb = module_type_of_module None (lookup_module mp1 env) in
-  let cst2 = check_subtypes env mtb farg_b in
+  let cst2 = Subtyping.check_subtypes env mtb farg_b in
   let mp_delta = discr_resolver mtb in
   let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
-  let subst = map_mbid farg_id mp1 mp_delta
-  in
+  let subst = map_mbid farg_id mp1 mp_delta in
   subst_struct_expr subst fbody_b,
   mkalg alg mp1 cst2,
   subst_codom_delta_resolver subst resolver,
-  Univ.union_constraints cst1 cst2
+  cst1 +++ cst2
 
 and translate_functor env inl arg_id arg_e trans mkalg =
   let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
@@ -294,7 +282,7 @@ and translate_functor env inl arg_id arg_e trans mkalg =
   SEBfunctor (arg_id, mtb, sign),
   mkalg alg arg_id mtb,
   resolver,
-  Univ.union_constraints cst mtb.typ_constraints
+  cst +++ mtb.typ_constraints
 
 and translate_struct_module_entry env mp inl = function
   | MSEident mp1 ->
@@ -314,7 +302,7 @@ and translate_struct_module_entry env mp inl = function
 	translate_struct_module_entry env mp inl mte in
       let sign,alg,resolve,cst2 =
 	check_with env sign with_decl alg mp resolve in
-      sign,alg,resolve,Univ.union_constraints cst1 cst2
+      sign,alg,resolve, cst1 +++ cst2
 
 and translate_struct_type_entry env inl = function
   | MSEident mp1 ->
@@ -331,7 +319,7 @@ and translate_struct_type_entry env inl = function
       let sign,alg,resolve,cst2 =
 	check_with env sign with_decl alg (mp_from_mexpr mte) resolve
       in
-      sign,alg,resolve,Univ.union_constraints cst1 cst2
+      sign,alg,resolve, cst1 +++ cst2
 
 and translate_module_type env mp inl mte =
   let mp_from = mp_from_mexpr mte in
@@ -415,16 +403,14 @@ let rec struct_expr_constraints cst = function
         structure_body
 
   | SEBapply (meb1,meb2,cst1) ->
-      struct_expr_constraints
-	(struct_expr_constraints (Univ.union_constraints cst1 cst) meb1)
-	meb2
+      struct_expr_constraints (struct_expr_constraints (cst1 +++ cst) meb1)
+        meb2
   | SEBwith(meb,With_definition_body(_,cb))->
-      struct_expr_constraints
-        (Univ.union_constraints (Future.force cb.const_constraints) cst) meb
+      struct_expr_constraints ((Future.force cb.const_constraints) +++ cst) meb
   | SEBwith(meb,With_module_body(_,_))->
-      struct_expr_constraints  cst meb	
-		
-and struct_elem_constraints cst = function 
+      struct_expr_constraints  cst meb
+
+and struct_elem_constraints cst = function
   | SFBconst cb -> cst
   | SFBmind mib -> cst
   | SFBmodule mb -> module_constraints cst mb
@@ -434,12 +420,11 @@ and module_constraints cst mb =
   let cst = match mb.mod_expr with
     | None -> cst
     | Some meb -> struct_expr_constraints cst meb in
-  let cst = 
-      struct_expr_constraints cst mb.mod_type in
-  Univ.union_constraints mb.mod_constraints cst
+  let cst = struct_expr_constraints cst mb.mod_type in
+  mb.mod_constraints +++ cst
 
 and modtype_constraints cst mtb =
-  struct_expr_constraints  (Univ.union_constraints mtb.typ_constraints cst) mtb.typ_expr
+  struct_expr_constraints (mtb.typ_constraints +++ cst) mtb.typ_expr
 
 
 let struct_expr_constraints = struct_expr_constraints Univ.empty_constraint