Declarations.mli: reorganization of modular structures

 The earlier type [struct_expr_body] was far too broad,
 leading to code with unclear invariants, many "assert false", etc etc.
 Its replacement [module_alg_expr] has only three constructors:
   * MEident
   * MEapply : note the module_path as 2nd arg, no more constraints here
   * MEwith : no more constant_body inside, constr is just fine
 But no more SEBfunctor or SEBstruct constructor here (see below).
 This way, this datatype corresponds to algebraic expressions,
 i.e. anything that can appear in non-interactive modules.
 In fact, it even coincides now with [Entries.module_struct_entry].

 - Functor constructors are now necessarily on top of other
   structures thanks to a generic [functorize] datatype.

 - Structures are now separated from algebraic expressions by design :
   the [mod_type] and [typ_expr] fields now only contain structures
   (or functorized structures), while [mod_type_alg] and [typ_expr_alg]
   are restricted to algebraic expressions only.

 - Only the implementation field [mod_expr] could be either algebraic
   or structural. We handle this via a specialized datatype
   [module_implementation] with four constructors:

    * Abstract : no implementation (cf. for instance Declare Module)
    * Algebraic(_) : for non-interactive modules, e.g. Module M := N.
    * Struct(_) : for interactive module, e.g. Module M : T. ... End M.
    * FullStruct : for interactive module with no type restriction.

   The [FullStruct] is a particular case of [Struct] where the implementation
   need not be stored at all, since it is exactly equal to its expanded
   type present in [mod_type]. This is less fragile than hoping as earlier
   that pointer equality between [mod_type] and [mod_expr] will be
   preserved...

 - We clearly emphasize that only [mod_type] and [typ_expr] are
   relevant for the kernel, while [mod_type_alg] and [typ_expr_alg]
   are there only for a nicer extraction and shorter module printing.
   [mod_expr] is also not accessed by the kernel, but it is important
   for Print Assumptions later.

 - A few implicit invariants remain, for instance "no MEwith in mod_expr",
   see the final comment in Declarations

 - Heavy refactoring of module-related files : modops, mod_typing,
   safe_typing, declaremods, extraction/extract_env.ml ...

 - Coqchk has been adapted accordingly. The code concerning MEwith
   in Mod_checking is now gone, since we cannot have any in mod_expr.

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

1 files changed, 64 insertions, 309 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 66f1194d3..b0f20da70 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -13,8 +13,7 @@ open Subtyping
 open Declarations
 open Environ
 
-(************************************************************************)
-(* Checking constants *)
+(** {6 Checking constants } *)
 
 let refresh_arity ar =
   let ctxt, hd = decompose_prod_assum ar in
@@ -43,339 +42,95 @@ let check_constant_declaration env kn cb =
         check_polymorphic_arity env ctxt par);
   add_constant kn cb env
 
-(************************************************************************)
-(* Checking modules *)
 
+(** {6 Checking modules } *)
 
-exception Not_path
-
-let path_of_mexpr = function
-  | SEBident mp -> mp
-  | _ -> raise Not_path
-
-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 k=k' && is_modular b = m -> rev_before,b,after
-  | h::tail -> list_split_assoc km (h::rev_before) tail
-
-let check_definition_sub env cb1 cb2 =
-  let check_type env t1 t2 =
-
-    (* If the type of a constant is generated, it may mention
-       non-variable algebraic universes that the general conversion
-       algorithm is not ready to handle. Anyway, generated types of
-       constants are functions of the body of the constant. If the
-       bodies are the same in environments that are subtypes one of
-       the other, the types are subtypes too (i.e. if Gamma <= Gamma',
-       Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
-       Hence they don't have to be checked again *)
-
-    let t1,t2 =
-      if isArity t2 then
-        let (ctx2,s2) = destArity t2 in
-        match s2 with
-        | Type v when not (Univ.is_univ_variable v) ->
-          (* The type in the interface is inferred and is made of algebraic
-             universes *)
-          begin try
-            let (ctx1,s1) = dest_arity env t1 in
-            match s1 with
-            | Type u when not (Univ.is_univ_variable u) ->
-              (* Both types are inferred, no need to recheck them. We
-                 cheat and collapse the types to Prop *)
-                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
-            | Prop _ ->
-              (* The type in the interface is inferred, it may be the case
-                 that the type in the implementation is smaller because
-                 the body is more reduced. We safely collapse the upper
-                 type to Prop *)
-                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
-            | Type _ ->
-              (* The type in the interface is inferred and the type in the
-                 implementation is not inferred or is inferred but from a
-                 more reduced body so that it is just a variable. Since
-                 constraints of the form "univ <= max(...)" are not
-                 expressible in the system of algebraic universes: we fail
-                 (the user has to use an explicit type in the interface *)
-                raise Reduction.NotConvertible
-          with UserError _ (* "not an arity" *) ->
-            raise Reduction.NotConvertible end
-        | _ -> t1,t2
-      else
-        (t1,t2) in
-    Reduction.conv_leq env t1 t2
-  in
-  (*Start by checking types*)
-  let typ1 = Typeops.type_of_constant_type env cb1.const_type in
-  let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-  check_type env typ1 typ2;
-  (* In the spirit of subtyping.check_constant, we accept
-     any implementations of parameters and opaques terms,
-     as long as they have the right type *)
-  (match cb2.const_body with
-    | Undef _ | OpaqueDef _ -> ()
-    | Def lc2 ->
-	(match cb1.const_body with
-	  | Def lc1 ->
-	    let c1 = force_constr lc1 in
-            let c2 = force_constr lc2 in
-	    Reduction.conv env c1 c2
-	  (* Coq only places transparent cb in With_definition_body *)
-	  | _ -> assert false))
-
-let lookup_modtype mp env =
-  try Environ.lookup_modtype mp env
-  with Not_found ->
-    failwith ("Unknown module type: "^string_of_mp mp)
+(** We currently ignore the [mod_type_alg] and [typ_expr_alg] fields.
+    The only delicate part is when [mod_expr] is an algebraic expression :
+    we need to expand it before checking it is indeed a subtype of [mod_type].
+    Fortunately, [mod_expr] cannot contain any [MEwith]. *)
 
 let lookup_module mp env =
   try Environ.lookup_module mp env
   with Not_found ->
     failwith ("Unknown module: "^string_of_mp mp)
 
-let rec check_with env mtb with_decl mp=
-  match with_decl with
-    | With_definition_body (idl,c) ->
-	check_with_def env mtb (idl,c) mp;
-	mtb
-    | With_module_body (idl,mp1) ->
-	check_with_mod env mtb (idl,mp1) mp;
-	mtb
-
-and check_with_def env mtb (idl,c) mp =
-  let sig_b = match mtb with
-    | SEBstruct(sig_b) ->
-	sig_b
-    | _ -> error_signature_expected mtb
+let rec check_module env mp mb =
+  let (_:module_signature) =
+    check_signature env mb.mod_type mb.mod_mp mb.mod_delta
   in
-  let id,idl = match idl with
-    | [] -> assert false
-    | id::idl -> id,idl
+  let optsign = match mb.mod_expr with
+    |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta)
+    |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta)
+    |Abstract|FullStruct -> None
   in
-  let l = Label.of_id id in
-    try
-      let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
-      let before = List.rev rev_before in
-      let env' = Modops.add_signature mp before empty_delta_resolver env in
-      if idl = [] then
-	      let cb = match spec with
-		  SFBconst cb -> cb
-		| _ -> error_not_a_constant l
-	      in
-              check_definition_sub env' c cb
-      else
-	      let old = match spec with
-		  SFBmodule msb -> msb
-		| _ -> error_not_a_module l
-	      in
-		begin
-		  match old.mod_expr with
-                    | None ->
-		        check_with_def env' old.mod_type (idl,c) (MPdot(mp,l))
-                    | Some msb ->
-			error_a_generative_module_expected l
-		end
-    with
-	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_with_incorrect l
-
-and check_with_mod env mtb (idl,mp1) mp =
-  let sig_b =
-    match mtb with
-    | SEBstruct(sig_b) ->
-	sig_b
-    | _ -> error_signature_expected mtb in
-  let id,idl = match idl with
-    | [] -> assert false
-    | id::idl -> id,idl
-  in
-  let l = Label.of_id id in
-    try
-      let rev_before,spec,after = list_split_assoc (l,false) [] sig_b in
-      let before = List.rev rev_before in
-      let env' = Modops.add_signature mp before empty_delta_resolver env in
-      if idl = [] then
-	      let _ = match spec with
-		  SFBmodule msb -> msb
-		| _ -> error_not_a_module l
-	      in
-	      let (_:module_body) = (Environ.lookup_module mp1 env) in ()
-      else
-	    let old = match spec with
-		SFBmodule msb -> msb
-	      | _ -> error_not_a_module l
-	    in
-	      begin
-		match old.mod_expr with
-                    None ->
-		      check_with_mod env'
-			  old.mod_type (idl,mp1) (MPdot(mp,l))
-                  | Some msb ->
-                      error_a_generative_module_expected l
-              end
-    with
-	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_with_incorrect l
+  match optsign with
+  |None -> ()
+  |Some sign ->
+    let mtb1 =
+      {typ_mp=mp;
+       typ_expr=sign;
+       typ_expr_alg=None;
+       typ_constraints=Univ.empty_constraint;
+       typ_delta = mb.mod_delta;}
+    and mtb2 =
+      {typ_mp=mp;
+       typ_expr=mb.mod_type;
+       typ_expr_alg=None;
+       typ_constraints=Univ.empty_constraint;
+       typ_delta = mb.mod_delta;}
+    in
+    let env = add_module_type mp mtb1 env in
+    Subtyping.check_subtypes env mtb1 mtb2
 
 and check_module_type env mty =
-  let (_:struct_expr_body) =
-    check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in
+  let (_:module_signature) =
+    check_signature env mty.typ_expr mty.typ_mp mty.typ_delta in
   ()
 
-							 
-and check_module env mp mb =
-  match mb.mod_expr, mb.mod_type with
-    | None,mtb -> 
-	let (_:struct_expr_body) =
-	  check_modtype env mtb mb.mod_mp mb.mod_delta in ()
-    | Some mexpr, mtb when mtb==mexpr ->
-	let (_:struct_expr_body) =
-	  check_modtype env mtb mb.mod_mp mb.mod_delta in ()
-    | Some mexpr, _ ->
-	let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in
-	let (_:struct_expr_body) =
-	  check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in
-	let mtb1 =
-	  {typ_mp=mp;
-	   typ_expr=sign;
-	   typ_expr_alg=None;
-	   typ_constraints=Univ.empty_constraint;
-	   typ_delta = mb.mod_delta;}
-	and mtb2 =
-	  {typ_mp=mp;
-	   typ_expr=mb.mod_type;
-	   typ_expr_alg=None;
-	   typ_constraints=Univ.empty_constraint;
-	   typ_delta = mb.mod_delta;}
-	in
-	let env = add_module (module_body_of_type mp mtb1) env in
-	check_subtypes env mtb1 mtb2
-
 and check_structure_field env mp lab res = function
   | SFBconst cb ->
       let c = Constant.make2 mp lab in
-	check_constant_declaration env c cb
+      check_constant_declaration env c cb
   | SFBmind mib ->
       let kn = MutInd.make2 mp lab in
       let kn = mind_of_delta res kn in
-	Indtypes.check_inductive env kn mib
+      Indtypes.check_inductive env kn mib
   | SFBmodule msb ->
-      let (_:unit) = check_module env (MPdot(mp,lab)) msb in
-	Modops.add_module msb env
+      let () = check_module env (MPdot(mp,lab)) msb in
+      Modops.add_module msb env
   | SFBmodtype mty ->
       check_module_type env mty;
       add_modtype (MPdot(mp,lab)) mty env
-	
-and check_modexpr env mse mp_mse res = match mse with
-  | SEBident mp ->
+
+and check_mexpr env mse mp_mse res = match mse with
+  | MEident mp ->
       let mb = lookup_module mp env in
       (subst_and_strengthen mb mp_mse).mod_type
-  | SEBfunctor (arg_id, mtb, body) ->
-      check_module_type env mtb ;
-      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
-      let sign = check_modexpr env' body mp_mse res in
-	SEBfunctor (arg_id, mtb, sign)
-  | SEBapply (f,m,cst) ->
-      let sign = check_modexpr env f mp_mse res in
-      let farg_id, farg_b, fbody_b = destr_functor env sign in
-      let mp =
-	try (path_of_mexpr m)
-	with Not_path -> error_application_to_not_path m
-	  (* place for nondep_supertype *) in
-      let mtb = module_type_of_module (Some mp) (lookup_module mp env) in
-	check_subtypes env mtb farg_b;
-	(subst_struct_expr (map_mbid farg_id mp) fbody_b)
-  | SEBwith(mte, with_decl) ->
-      let sign = check_modexpr env mte mp_mse res in
-      let sign = check_with env sign with_decl mp_mse in 
-	sign
-  | SEBstruct(msb) ->
-      let (_:env) = List.fold_left (fun env (lab,mb) ->
-		   check_structure_field env mp_mse lab res mb) env msb in
-	SEBstruct(msb)
-	
-and check_modtype env mse mp_mse res = match mse with
-  | SEBident mp ->
-      let mtb = lookup_modtype mp env in
-	mtb.typ_expr
-  | SEBfunctor (arg_id, mtb, body) ->
-      check_module_type env mtb;
-      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
-      let body = check_modtype env' body mp_mse res in
-	SEBfunctor(arg_id,mtb,body)
-  | SEBapply (f,m,cst) ->
-      let sign = check_modtype env f mp_mse res in
-      let farg_id, farg_b, fbody_b = destr_functor env sign in
-      let mp =
-	try (path_of_mexpr m)
-	with Not_path -> error_application_to_not_path m
-	  (* place for nondep_supertype *) in
+  | MEapply (f,mp) ->
+      let sign = check_mexpr env f mp_mse res in
+      let farg_id, farg_b, fbody_b = destr_functor sign in
       let mtb = module_type_of_module (Some mp) (lookup_module mp env) in
-	check_subtypes env mtb farg_b;
-	subst_struct_expr (map_mbid farg_id mp) fbody_b
-  | SEBwith(mte, with_decl) ->
-      let sign = check_modtype env mte mp_mse res in
-      let sign = check_with env sign with_decl mp_mse in
-	sign
-  | SEBstruct(msb) ->
-      let (_:env) = List.fold_left (fun env (lab,mb) ->
-		   check_structure_field env mp_mse lab res mb) env msb in
-      SEBstruct(msb)
-	
-(*
-  let rec add_struct_expr_constraints env = function
-  | SEBident _ -> env
-  
-  | SEBfunctor (_,mtb,meb) ->
-  add_struct_expr_constraints
-  (add_modtype_constraints env mtb) meb
-
-  | SEBstruct (_,structure_body) ->
-      List.fold_left
-        (fun env (l,item) -> add_struct_elem_constraints env item)
-        env
-        structure_body
-
-  | SEBapply (meb1,meb2,cst) ->
-(*  let g = Univ.merge_constraints cst Univ.initial_universes in
-msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
-      Univ.pr_universes g++str"============="++fnl());
-*)
-      Environ.add_constraints cst
-        (add_struct_expr_constraints
-	  (add_struct_expr_constraints env meb1)
-	  meb2)
-  | SEBwith(meb,With_definition_body(_,cb))->
-      Environ.add_constraints cb.const_constraints
-	(add_struct_expr_constraints env meb)
-  | SEBwith(meb,With_module_body(_,_,cst))->
-      Environ.add_constraints cst
-	(add_struct_expr_constraints env meb)
+      check_subtypes env mtb farg_b;
+      subst_signature (map_mbid farg_id mp) fbody_b
+  | MEwith _ -> error_with_module ()
 
-and add_struct_elem_constraints env = function
-  | SFBconst cb -> Environ.add_constraints cb.const_constraints env
-  | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
-  | SFBmodule mb -> add_module_constraints env mb
-  | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
-  | SFBalias (mp,None) -> env
-  | SFBmodtype mtb -> add_modtype_constraints env mtb
-
-and add_module_constraints env mb =
-  let env = match mb.mod_expr with
-    | None -> env
-    | Some meb -> add_struct_expr_constraints env meb
-  in
-  let env = match mb.mod_type with
-    | None -> env
-    | Some mtb ->
-	add_struct_expr_constraints env mtb
-  in
-    Environ.add_constraints mb.mod_constraints env
+and check_mexpression env sign mp_mse res = match sign with
+  | MoreFunctor (arg_id, mtb, body) ->
+      check_module_type env mtb;
+      let env' = add_module_type (MPbound arg_id) mtb env in
+      let body = check_mexpression env' body mp_mse res in
+      MoreFunctor(arg_id,mtb,body)
+  | NoFunctor me -> check_mexpr env me mp_mse res
 
-and add_modtype_constraints env mtb =
-  add_struct_expr_constraints env mtb.typ_expr
-*)
+and check_signature env sign mp_mse res = match sign with
+  | MoreFunctor (arg_id, mtb, body) ->
+      check_module_type env mtb;
+      let env' = add_module_type (MPbound arg_id) mtb env in
+      let body = check_signature env' body mp_mse res in
+      MoreFunctor(arg_id,mtb,body)
+  | NoFunctor struc ->
+      let (_:env) = List.fold_left (fun env (lab,mb) ->
+	check_structure_field env mp_mse lab res mb) env struc
+      in
+      NoFunctor struc