Mod_typing: some refactoring (common parts about MSEapply and co)

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

3 files changed, 104 insertions, 120 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 13ac21437..bbcabd72a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -29,6 +29,12 @@ let path_of_mexpr = function
   | MSEident mp -> mp
   | _ -> raise Not_path
 
+let rec mp_from_mexpr = function
+  | MSEident mp -> mp
+  | MSEapply (expr,_) -> mp_from_mexpr expr
+  | MSEfunctor (_,_,expr) -> mp_from_mexpr expr
+  | MSEwith (expr,_) -> mp_from_mexpr expr
+
 let rec list_split_assoc k rev_before = function
   | [] -> raise Not_found
   | (k',b)::after when k=k' -> rev_before,b,after
@@ -255,7 +261,7 @@ and translate_module env mp inl me =
 	in
 	  { mod_mp = mp;
 	    mod_type = sign;
-	    mod_expr = Some alg_implem;
+	    mod_expr = alg_implem;
 	    mod_type_alg = alg1;
 	    mod_constraints = Univ.union_constraints cst1 cst2;
 	    mod_delta = resolver;
@@ -265,126 +271,92 @@ and translate_module env mp inl me =
 	       If it does, I don't really know how to
 	       fix the bug.*)
 
+and translate_apply env inl ftrans mexpr mkalg =
+  let sign,alg,resolver,cst1 = ftrans in
+  let farg_id, farg_b, fbody_b = destr_functor env sign in
+  let mp1 =
+    try path_of_mexpr mexpr
+    with Not_path -> error_application_to_not_path mexpr
+  in
+  let mtb = module_type_of_module env None (lookup_module mp1 env) in
+  let cst2 = check_subtypes env mtb farg_b in
+  let mp_delta = discr_resolver env 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
+  subst_struct_expr subst fbody_b,
+  mkalg alg mp1 cst2,
+  subst_codom_delta_resolver subst resolver,
+  Univ.union_constraints 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
+  let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+  let sign,alg,resolver,cst = trans env'
+  in
+  SEBfunctor (arg_id, mtb, sign),
+  mkalg alg arg_id mtb,
+  resolver,
+  Univ.union_constraints cst mtb.typ_constraints
 
-and translate_struct_module_entry env mp inl mse  = match mse with
+and translate_struct_module_entry env mp inl = function
   | MSEident mp1 ->
-      let mb = lookup_module mp1 env in 
+      let mb = lookup_module mp1 env in
       let mb' = strengthen_and_subst_mb mb mp env false in
-	mb'.mod_type, SEBident mp1, mb'.mod_delta,Univ.empty_constraint
+      mb'.mod_type, Some (SEBident mp1), mb'.mod_delta,Univ.empty_constraint
   | MSEfunctor (arg_id, arg_e, body_expr) ->
-      let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
-      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) 
-	env in
-      let sign,alg,resolver,cst =
-	translate_struct_module_entry env' mp inl body_expr in
-      SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver,
-      Univ.union_constraints cst mtb.typ_constraints
+      let trans env' = translate_struct_module_entry env' mp inl body_expr in
+      let mkalg a id m = Option.map (fun a -> SEBfunctor (id,m,a)) a in
+      translate_functor env inl arg_id arg_e trans mkalg
   | MSEapply (fexpr,mexpr) ->
-      let sign,alg,resolver,cst1 =
-	translate_struct_module_entry env mp inl fexpr
-      in
-      let farg_id, farg_b, fbody_b = destr_functor env sign in
-      let mtb,mp1 = 
-	try
-	  let mp1 = path_of_mexpr mexpr in
-	      let mtb = module_type_of_module env None (lookup_module mp1 env) in
-		mtb,mp1
-	with
-	  | Not_path -> error_application_to_not_path mexpr
-	      (* place for nondep_supertype *) in
-      let cst = check_subtypes env mtb farg_b in
-      let mp_delta = discr_resolver env 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
-      (subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst),
-      (subst_codom_delta_resolver subst resolver),
-      Univ.union_constraints cst1 cst
+      let trans = translate_struct_module_entry env mp inl fexpr in
+      let mkalg a mp c = Option.map (fun a -> SEBapply(a,SEBident mp,c)) a in
+      translate_apply env inl trans mexpr mkalg
   | MSEwith(mte, with_decl) ->
-      let sign,alg,resolve,cst1 = translate_struct_module_entry env mp inl mte in
-      let sign,alg,resolve,cst2 = check_with env sign with_decl (Some alg) mp resolve in
-	sign,Option.get alg,resolve,Univ.union_constraints cst1 cst2
-	  
-and translate_struct_type_entry env inl mse = match mse with
+      let sign,alg,resolve,cst1 =
+	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
+
+and translate_struct_type_entry env inl = function
   | MSEident mp1 ->
-      let mtb = lookup_modtype mp1 env in 
-	mtb.typ_expr,
-      Some (SEBident mp1),mtb.typ_delta,mp1,Univ.empty_constraint
+      let mtb = lookup_modtype mp1 env in
+      mtb.typ_expr,Some (SEBident mp1),mtb.typ_delta,Univ.empty_constraint
   | MSEfunctor (arg_id, arg_e, body_expr) ->
-      let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
-      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env  in
-      let sign,alg,resolve,mp_from,cst =
-	translate_struct_type_entry env' inl body_expr in
-	SEBfunctor (arg_id, mtb, sign),None,resolve,mp_from,
-      Univ.union_constraints cst mtb.typ_constraints
+      let trans env' = translate_struct_type_entry env' inl body_expr in
+      translate_functor env inl arg_id arg_e trans (fun _ _ _ -> None)
   | MSEapply (fexpr,mexpr) ->
-      let sign,alg,resolve,mp_from,cst1 =
-	translate_struct_type_entry env inl fexpr
-      in
-      let farg_id, farg_b, fbody_b = destr_functor env sign in
-      let mtb,mp1 = 
-	try
-	  let mp1 = path_of_mexpr mexpr in
-	  let mtb = module_type_of_module env None (lookup_module mp1 env) in
-	    mtb,mp1
-	with
-	  | Not_path -> error_application_to_not_path mexpr
-	      (* place for nondep_supertype *) in
-      let cst2 = check_subtypes env mtb farg_b in
-      let mp_delta = discr_resolver env 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
-      (subst_struct_expr subst fbody_b),None,
-      (subst_codom_delta_resolver subst resolve),mp_from,
-      Univ.union_constraints cst1 cst2
+      let trans = translate_struct_type_entry env inl fexpr in
+      translate_apply env inl trans mexpr (fun _ _ _ -> None)
   | MSEwith(mte, with_decl) ->
-      let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
-      let sign,alg,resolve,cst1 = 
-	check_with env sign with_decl alg mp_from resolve in
-	sign,alg,resolve,mp_from,Univ.union_constraints cst cst1    
+      let sign,alg,resolve,cst1 = translate_struct_type_entry env inl mte in
+      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
 
 and translate_module_type env mp inl mte =
-	let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
-	let mtb = subst_modtype_and_resolver
-	  {typ_mp = mp_from;
-	   typ_expr = sign;
-	   typ_expr_alg = None;
-	   typ_constraints = cst;
-	   typ_delta = resolve} mp env
-	in {mtb with typ_expr_alg = alg}
+  let mp_from = mp_from_mexpr mte in
+  let sign,alg,resolve,cst = translate_struct_type_entry env inl mte in
+  let mtb = subst_modtype_and_resolver
+    {typ_mp = mp_from;
+     typ_expr = sign;
+     typ_expr_alg = None;
+     typ_constraints = cst;
+     typ_delta = resolve} mp env
+  in {mtb with typ_expr_alg = alg}
 
-let rec translate_struct_include_module_entry env mp inl mse  = match mse with
+let rec translate_struct_include_module_entry env mp inl = function
   | MSEident mp1 ->
-      let mb = lookup_module mp1 env in 
+      let mb = lookup_module mp1 env in
       let mb' = strengthen_and_subst_mb mb mp env true in
-      let mb_typ = clean_bounded_mod_expr mb'.mod_type in 
-	mb_typ, mb'.mod_delta,Univ.empty_constraint
+      let mb_typ = clean_bounded_mod_expr mb'.mod_type in
+      mb_typ,None,mb'.mod_delta,Univ.empty_constraint
   | MSEapply (fexpr,mexpr) ->
-      let sign,resolver,cst1 =
-	translate_struct_include_module_entry env mp inl fexpr in
-      let farg_id, farg_b, fbody_b = destr_functor env sign in
-      let mtb,mp1 = 
-	try
-	  let mp1 = path_of_mexpr mexpr in
-	      let mtb = module_type_of_module env None (lookup_module mp1 env) in
-		mtb,mp1
-	with
-	  | Not_path -> error_application_to_not_path mexpr
-	      (* place for nondep_supertype *) in
-      let cst = check_subtypes env mtb farg_b in
-      let mp_delta =  discr_resolver env 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
-      (subst_struct_expr subst fbody_b),
-      (subst_codom_delta_resolver subst resolver),
-      Univ.union_constraints cst1 cst
+      let ftrans = translate_struct_include_module_entry env mp inl fexpr in
+      translate_apply env inl ftrans mexpr (fun _ _ _ -> None)
   | _ -> error ("You cannot Include a high-order structure.")
-  
 
 let rec add_struct_expr_constraints env = function
   | SEBident _ -> env
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 81974edfa..0987ca5b6 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -13,20 +13,32 @@ open Mod_subst
 open Names
 
 
-val translate_module : env -> module_path -> inline -> module_entry
-  -> module_body
-
-val translate_module_type : env -> module_path -> inline -> module_struct_entry ->
-  module_type_body
-
-val translate_struct_module_entry : env -> module_path -> inline -> module_struct_entry ->
-  struct_expr_body * struct_expr_body * delta_resolver * Univ.constraints
-
-val translate_struct_type_entry : env -> inline -> module_struct_entry ->
-  struct_expr_body * struct_expr_body option * delta_resolver * module_path * Univ.constraints
-
-val translate_struct_include_module_entry : env -> module_path -> inline ->
-  module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints
+val translate_module :
+  env -> module_path -> inline -> module_entry -> module_body
+
+val translate_module_type :
+  env -> module_path -> inline -> module_struct_entry -> module_type_body
+
+val translate_struct_module_entry :
+  env -> module_path -> inline -> module_struct_entry ->
+  struct_expr_body (* Signature *)
+  * struct_expr_body option  (* Algebraic expr, in fact never None *)
+  * delta_resolver
+  * Univ.constraints
+
+val translate_struct_type_entry :
+  env -> inline -> module_struct_entry ->
+  struct_expr_body
+  * struct_expr_body option
+  * delta_resolver
+  * Univ.constraints
+
+val translate_struct_include_module_entry :
+  env -> module_path -> inline -> module_struct_entry ->
+  struct_expr_body
+  * struct_expr_body option (* Algebraic expr, always None *)
+  * delta_resolver
+  * Univ.constraints
 
 val add_modtype_constraints : env -> module_type_body -> env
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 52a162bd4..66c731a9d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -444,8 +444,8 @@ let end_module l restype senv =
  let add_include me is_module inl senv =
    let sign,cst,resolver =
      if is_module then
-       let sign,resolver,cst =  
-	 translate_struct_include_module_entry senv.env 
+       let sign,_,resolver,cst =
+	 translate_struct_include_module_entry senv.env
 	   senv.modinfo.modpath inl me in
 	 sign,cst,resolver
      else