Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 137 insertions, 166 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index e366bc97..a384c836 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -1,12 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mod_typing.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of
+   the Coq module system *)
+
+(* This module provides the main functions for type-checking module
+   declarations *)
 
 open Util
 open Names
@@ -25,18 +29,17 @@ 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
   | h::tail -> list_split_assoc k (h::rev_before) tail
 
-let rec list_fold_map2 f e = function
-  |  []  -> (e,[],[])
-  |  h::t ->
-       let e',h1',h2' = f e h in
-       let e'',t1',t2' = list_fold_map2 f e' t in
-	 e'',h1'::t1',h2'::t2'
-
 let discr_resolver env mtb =
      match mtb.typ_expr with
 	SEBstruct _ -> 
@@ -81,40 +84,41 @@ and check_with_aux_def env sign with_decl mp equiv =
           | With_Definition ([],_) -> assert false
 	  | With_Definition ([id],c) ->
 	      let cb = match spec with
-		  SFBconst cb -> cb
+		| SFBconst cb -> cb
 		| _ -> error_not_a_constant l
 	      in
-		begin
-		  match cb.const_body with
-		    | None ->
-			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 =
-			  Constraint.union
-			    (Constraint.union cb.const_constraints cst1)
-			    cst2 in
-			let body = Some (Declarations.from_val j.uj_val) in
-			let cb' = {cb with
-				     const_body = body;
-				     const_body_code = Cemitcodes.from_val
-                            (compile_constant_body env' body false false);
-                                     const_constraints = cst} in
-			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
-		    | Some b ->
-			let cst1 = Reduction.conv env' c (Declarations.force b) in
-			let cst = Constraint.union cb.const_constraints cst1 in
-			let body = Some (Declarations.from_val c) in
-			let cb' = {cb with
-				     const_body = body;
-				     const_body_code = Cemitcodes.from_val
-                            (compile_constant_body env' body false false);
-                                     const_constraints = cst} in
-			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
-	      end
+	      (* 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 cb.const_constraints cst1)
+			cst2
+		    in
+		    let def = Def (Declarations.from_val j.uj_val) in
+		    def,cst
+		| Def cs ->
+		    let cst1 = Reduction.conv env' c (Declarations.force cs) in
+		    let cst = union_constraints cb.const_constraints cst1 in
+		    let def = Def (Declarations.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 = cst }
+	      in
+	      SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
 	  | With_Definition (_::_,c) ->
 	      let old = match spec with
-		  SFBmodule msb -> msb
+		| SFBmodule msb -> msb
 		| _ -> error_not_a_module (string_of_label l)
 	      in
 		begin
@@ -129,12 +133,12 @@ and check_with_aux_def env sign with_decl mp equiv =
 						    mod_type_alg = None}) in
 			  SEBstruct(before@((l,new_spec)::after)),cb,cst
                     | Some msb ->
-			error_a_generative_module_expected l
+			error_generative_module_expected l
 		end
 	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
-	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_with_incorrect l
+      | Not_found -> error_no_such_label l
+      | Reduction.NotConvertible -> error_incorrect_with_constraint l
 
 and check_with_aux_mod env sign with_decl mp equiv = 
   let sig_b = match sign with 
@@ -163,24 +167,24 @@ and check_with_aux_mod env sign with_decl mp equiv =
 	      in
 	      let mb_mp1 = (lookup_module mp1 env) in
 	      let mtb_mp1 = 
-		module_type_of_module env' None mb_mp1  in
+		module_type_of_module None mb_mp1  in
 	      let cst =
 		match old.mod_expr with
 		    None ->
 		      begin
-			try Constraint.union
+			try union_constraints
 			  (check_subtypes env' mtb_mp1 
-			     (module_type_of_module env' None old))
+			     (module_type_of_module None old))
 			  old.mod_constraints
-			with Failure _ -> error_with_incorrect (label_of_id id)
+			with Failure _ -> error_incorrect_with_constraint (label_of_id id)
 		      end
 		  | Some (SEBident(mp')) ->
 		      check_modpath_equiv env' mp1 mp';
 		      old.mod_constraints
-		  | _ ->  error_a_generative_module_expected l
+		  | _ ->  error_generative_module_expected l
+	      in
+	      let new_mb = strengthen_and_subst_mb mb_mp1 (MPdot(mp,l)) false
 	      in
-	      let new_mb = strengthen_and_subst_mb mb_mp1
-		(MPdot(mp,l)) env false in
 	      let new_spec = SFBmodule {new_mb with 
 					  mod_mp = MPdot(mp,l);
 					  mod_expr = Some (SEBident mp1);
@@ -215,14 +219,14 @@ and check_with_aux_mod env sign with_decl mp equiv =
 		      let mpnew = rebuild_mp mp' (List.map label_of_id idl) in
 			check_modpath_equiv env' mpnew mp;
 			  SEBstruct(before@(l,spec)::after)
-			    ,equiv,Constraint.empty
+			    ,equiv,empty_constraint
 		  | _ ->
-		      error_a_generative_module_expected l
+		      error_generative_module_expected l
               end
 	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
 	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_with_incorrect l
+      | Reduction.NotConvertible -> error_incorrect_with_constraint l
 
 and translate_module env mp inl me =
   match me.mod_entry_expr, me.mod_entry_type with
@@ -243,14 +247,14 @@ and translate_module env mp inl me =
 	let sign,alg1,resolver,cst2 =
 	  match me.mod_entry_type with
 	    | None ->
-		sign,None,resolver,Constraint.empty
+		sign,None,resolver,empty_constraint
 	    | Some mte ->
 		let mtb = translate_module_type env mp inl mte in
                 let cst = check_subtypes env
 		  {typ_mp = mp;
 		   typ_expr = sign;
 		   typ_expr_alg = None;
-		   typ_constraints = Constraint.empty;
+		   typ_constraints = empty_constraint;
 		   typ_delta = resolver;}
 		  mtb
 		in
@@ -258,9 +262,9 @@ 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.Constraint.union cst1 cst2;
+	    mod_constraints = Univ.union_constraints cst1 cst2;
 	    mod_delta = resolver;
 	    mod_retroknowledge = []} 
 	    (* spiwack: not so sure about that. It may
@@ -268,125 +272,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 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' = strengthen_and_subst_mb mb mp env false in
-	mb'.mod_type, SEBident mp1, mb'.mod_delta,Univ.Constraint.empty
+      let mb = lookup_module mp1 env in
+      let mb' = strengthen_and_subst_mb mb mp false in
+      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.Constraint.union 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 = if not inl then mp_delta else
-	complete_inline_delta_resolver env 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.Constraint.union 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.Constraint.union 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.Constraint.empty
+      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.Constraint.union 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 = if not inl then mp_delta else
-	complete_inline_delta_resolver env 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.Constraint.union 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.Constraint.union 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
+  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' = 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.Constraint.empty
+      let mb = lookup_module mp1 env in
+      let mb' = strengthen_and_subst_mb mb mp true in
+      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 = if not inl then mp_delta else
-	complete_inline_delta_resolver env 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.Constraint.union 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
@@ -448,11 +419,11 @@ let rec struct_expr_constraints cst = function
 
   | SEBapply (meb1,meb2,cst1) ->
       struct_expr_constraints
-	(struct_expr_constraints (Univ.Constraint.union cst1 cst) meb1)
+	(struct_expr_constraints (Univ.union_constraints cst1 cst) meb1)
 	meb2
   | SEBwith(meb,With_definition_body(_,cb))->
       struct_expr_constraints
-        (Univ.Constraint.union cb.const_constraints cst) meb
+        (Univ.union_constraints cb.const_constraints cst) meb
   | SEBwith(meb,With_module_body(_,_))->
       struct_expr_constraints  cst meb	
 		
@@ -468,11 +439,11 @@ and module_constraints cst mb =
     | Some meb -> struct_expr_constraints cst meb in
   let cst = 
       struct_expr_constraints cst mb.mod_type in
-  Univ.Constraint.union mb.mod_constraints cst
+  Univ.union_constraints mb.mod_constraints cst
 
 and modtype_constraints cst mtb =
-  struct_expr_constraints  (Univ.Constraint.union mtb.typ_constraints cst) mtb.typ_expr
+  struct_expr_constraints  (Univ.union_constraints mtb.typ_constraints cst) mtb.typ_expr
 
 
-let struct_expr_constraints = struct_expr_constraints Univ.Constraint.empty
-let module_constraints = module_constraints Univ.Constraint.empty
+let struct_expr_constraints = struct_expr_constraints Univ.empty_constraint
+let module_constraints = module_constraints Univ.empty_constraint