From 7acb63cad5f92c2618f99ca2a812a465092a523f Mon Sep 17 00:00:00 2001
From: soubiran
Date: Fri, 1 Feb 2008 12:18:37 +0000
Subject: Beaoucoup de changements dans la representation interne des modules.

kernel:

-declaration.ml
   unification des representations pour les modules et modules types.
     (type struct_expr_body)

-mod_typing.ml
   le typage des modules est separe de l'evaluation des modules

-modops.ml
   nouvelle fonction qui pour toutes expressions de structure calcule
   sa forme evaluee.(eval_struct)

-safe_typing.ml
  ajout du support du nouvel operateur Include.(add_include).


library:

-declaremods.ml
   nouveaux objets Include et Module-alias et gestion de la resolution de noms pour
   les alias via la nametab.

parsing:

-g_vernac.ml4:
   nouvelles regles pour le support des Includes et pour l'application des signatures
   fonctorielles.


extraction:
  Adaptation a la nouvelle representation des modules et support de l'operateur with.




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.mli | 63 +++++++++++++++++--------------------------------
 1 file changed, 22 insertions(+), 41 deletions(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 2f32d86392..544cea246c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -177,51 +177,32 @@ val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
 (*s Modules: signature component specifications, module types, and
   module declarations *)
 
-type specification_body = 
-  | SPBconst of constant_body
-  | SPBmind of mutual_inductive_body
-  | SPBmodule of module_specification_body
-  | SPBmodtype of module_type_body
-
-and module_signature_body = (label * specification_body) list
-
-and module_type_body = 
-  | MTBident of kernel_name
-  | MTBfunsig of mod_bound_id * module_type_body * module_type_body
-  | MTBsig of mod_self_id * module_signature_body
-
-and module_specification_body = 
-    { msb_modtype : module_type_body;
-      msb_equiv : module_path option; 
-      msb_constraints : constraints }
-    (*    [type_of](equiv) <: modtype  (if given)  
-       +  substyping of past [With_Module] mergers *)
-
-
-type structure_elem_body = 
-  | SEBconst of constant_body
-  | SEBmind of mutual_inductive_body
-  | SEBmodule of module_body
-  | SEBmodtype of module_type_body
-
-and module_structure_body = (label * structure_elem_body) list
-
-and module_expr_body =
-  | MEBident of module_path
-  | MEBfunctor of mod_bound_id * module_type_body * module_expr_body 
-  | MEBstruct of mod_self_id * module_structure_body
-  | MEBapply of module_expr_body * module_expr_body  (* (F A) *)
-      * constraints  (* [type_of](A) <: [input_type_of](F) *)
+type structure_field_body = 
+  | SFBconst of constant_body
+  | SFBmind of mutual_inductive_body
+  | SFBmodule of module_body
+  | SFBmodtype of struct_expr_body
+
+and structure_body = (label * structure_field_body) list
+
+and struct_expr_body =
+  | SEBident of module_path
+  | SEBfunctor of mod_bound_id * struct_expr_body * struct_expr_body 
+  | SEBstruct of mod_self_id * structure_body
+  | SEBapply of struct_expr_body * struct_expr_body
+      * constraints
+  | SEBwith of struct_expr_body * with_declaration_body
+
+and with_declaration_body =
+    With_module_body of identifier list * module_path * constraints
+  | With_definition_body of identifier list * constant_body
 
 and module_body = 
-    { mod_expr : module_expr_body option;
-      mod_user_type : module_type_body option;
-      mod_type : module_type_body;
+    { mod_expr : struct_expr_body option;
+      mod_type : struct_expr_body option;
       mod_equiv : module_path option;
       mod_constraints : constraints;
       mod_retroknowledge : Retroknowledge.action list}
-    (*    [type_of(mod_expr)]  <: [mod_user_type] (if given)  *)
-    (*  if equiv given then constraints are empty *)
-
 
 
+type module_type_body = struct_expr_body * module_path option
-- 
cgit v1.2.3