Modules dans COQ\!\!\!\!

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

.cvsignore

@@ -3,3 +3,5 @@ coqtop
 minicoq
 coqtop.opt
 glob.dump
+tmp
+.depend.devel

.depend.camlp4

@@ -26,6 +26,7 @@ parsing/g_vernac.ml: parsing/grammar.cma
 parsing/g_proofs.ml: parsing/grammar.cma
 parsing/g_cases.ml: parsing/grammar.cma
 parsing/g_constr.ml: parsing/grammar.cma
+parsing/g_module.ml: parsing/grammar.cma
 parsing/g_tactic.ml: parsing/grammar.cma
 parsing/g_ltac.ml: parsing/grammar.cma
 parsing/argextend.ml: 

.depend.coq

@@ -33,13 +33,15 @@ theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v
 theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/R_sqrt.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/Rderiv.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rcomplet.vo theories/Reals/Alembert_compl.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Ranalysis.vo theories/Reals/DiscrR.vo theories/Reals/SplitRmult.vo theories/Reals/SplitAbsolu.vo
 theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
 theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Ranalysis4.vo
-theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Sqrt_reg.vo
+theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Sqrt_reg.vo
 theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rderiv.vo theories/Reals/R_sqr.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
 theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
 theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo
 theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
 theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rsqrt_def.vo
 theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Rcomplet.vo theories/Reals/AltSeries.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cv_prop.vo theories/Reals/Ranalysis1.vo
+theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo
+theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rsigma.vo theories/Reals/Alembert.vo theories/Reals/Alembert_compl.vo theories/Reals/Binome.vo theories/Reals/Cv_prop.vo theories/Reals/Rcomplet.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo
 theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo
 theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rfunctions.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo
 theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Arith/Max.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Rprod.vo theories/Reals/Cv_prop.vo theories/Reals/Cos_rel.vo

Makefile

@@ -81,14 +81,17 @@ LIBREP=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
 KERNEL=kernel/names.cmo kernel/univ.cmo \
        kernel/esubst.cmo kernel/term.cmo kernel/sign.cmo \
        kernel/declarations.cmo kernel/environ.cmo kernel/closure.cmo \
-       kernel/conv_oracle.cmo kernel/reduction.cmo \
+       kernel/conv_oracle.cmo kernel/reduction.cmo kernel/entries.cmo \
+       kernel/modops.cmo \
        kernel/type_errors.cmo kernel/inductive.cmo kernel/typeops.cmo \
-       kernel/indtypes.cmo kernel/cooking.cmo kernel/safe_typing.cmo
+       kernel/indtypes.cmo kernel/cooking.cmo kernel/term_typing.cmo \
+       kernel/subtyping.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo
 
-LIBRARY=library/nameops.cmo library/libobject.cmo library/summary.cmo \
-        library/nametab.cmo library/lib.cmo library/global.cmo \
-	library/goptions.cmo library/library.cmo library/states.cmo \
-	library/impargs.cmo library/declare.cmo 
+LIBRARY=library/libnames.cmo library/nameops.cmo library/libobject.cmo \
+	library/summary.cmo \
+        library/nametab.cmo library/global.cmo library/lib.cmo \
+	library/declaremods.cmo library/library.cmo library/states.cmo \
+	library/impargs.cmo library/declare.cmo library/goptions.cmo 
 
 PRETYPING=pretyping/termops.cmo \
           pretyping/evd.cmo pretyping/instantiate.cmo \
@@ -103,14 +106,15 @@ PRETYPING=pretyping/termops.cmo \
 
 PARSING=parsing/lexer.cmo parsing/coqast.cmo \
         parsing/genarg.cmo proofs/tacexpr.cmo parsing/ast.cmo \
-        parsing/termast.cmo parsing/astterm.cmo \
+        parsing/termast.cmo parsing/astterm.cmo parsing/astmod.cmo \
 	parsing/extend.cmo parsing/esyntax.cmo \
         parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo \
 	parsing/coqlib.cmo parsing/prettyp.cmo parsing/search.cmo
 
 HIGHPARSING= parsing/g_prim.cmo parsing/g_basevernac.cmo \
 	parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \
 	parsing/g_ltac.cmo parsing/g_constr.cmo parsing/g_cases.cmo \
+	parsing/g_module.cmo \
 	parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo
 
 ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo
@@ -181,10 +185,14 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \
         kernel/term.cmo kernel/sign.cmo kernel/declarations.cmo \
 	kernel/environ.cmo \
 	kernel/closure.cmo kernel/conv_oracle.cmo kernel/reduction.cmo \
+	kernel/modops.cmo \
 	kernel/type_errors.cmo kernel/inductive.cmo kernel/typeops.cmo \
-	kernel/indtypes.cmo kernel/cooking.cmo kernel/safe_typing.cmo \
+	kernel/indtypes.cmo kernel/cooking.cmo kernel/term_typing.cmo \
+        kernel/subtyping.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo \
+	library/libnames.cmo \
 	library/nameops.cmo library/libobject.cmo library/summary.cmo \
 	library/nametab.cmo library/lib.cmo library/global.cmo \
+	library/declaremods.cmo \
 	library/library.cmo lib/options.cmo library/impargs.cmo \
         library/goptions.cmo \
 	pretyping/evd.cmo pretyping/instantiate.cmo \
@@ -203,7 +211,7 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \
 	parsing/g_prim.cmo parsing/g_basevernac.cmo \
 	parsing/extend.cmo \
 	parsing/coqlib.cmo pretyping/detyping.cmo \
-	parsing/termast.cmo parsing/astterm.cmo \
+	parsing/termast.cmo parsing/astterm.cmo parsing/astmod.cmo \
 	parsing/egrammar.cmo parsing/esyntax.cmo toplevel/metasyntax.cmo \
 	parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo \
 	lib/stamps.cmo pretyping/typing.cmo \
@@ -272,9 +280,11 @@ JPROVERCMO=contrib/jprover/opname.cmo \
 
 ML4FILES += contrib/jprover/jprover.ml4
 
-CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) $(XMLCMO) \
-	$(FOURIERCMO) \
-	$(EXTRACTIONCMO) $(CORRECTNESSCMO) $(JPROVERCMO)
+CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \
+	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO)
+
+#later $(CORRECTNESSCMO) 
+#later :) 
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
@@ -368,7 +378,7 @@ bin/coq-interface$(EXE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(INTERFACE)
 	$(COQMKTOP) -top $(BYTEFLAGS) -o $@ $(INTERFACE)
 
 bin/parser$(EXE): contrib/interface/ctast.cmo contrib/interface/parse.cmo contrib/interface/line_parser.cmo $(PARSERREQUIRES) contrib/interface/xlate.cmo contrib/interface/vtp.cmo
-	$(OCAMLC) -cclib -lunix -custom $(MLINCLUDES) -o $@ $(CMA) \
+	$(OCAMLC) -cclib -lunix -custom $(BYTEFLAGS) -o $@ $(CMA) \
 	$(PARSERREQUIRES) \
 	ctast.cmo line_parser.cmo vtp.cmo xlate.cmo parse.cmo
 
@@ -394,6 +404,10 @@ SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v
 states/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP)
 	$(BESTCOQTOP) -boot -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq
 
+#       theories/Init/DatatypesHints.vo   theories/Init/PeanoHints.vo \
+#       theories/Init/LogicHints.vo       theories/Init/SpecifHints.vo \
+#       theories/Init/Logic_TypeHints.vo \
+
 INITVO=theories/Init/Datatypes.vo         theories/Init/Peano.vo         \
        theories/Init/DatatypesSyntax.vo   theories/Init/Prelude.vo       \
        theories/Init/Logic.vo             theories/Init/Specif.vo        \
@@ -784,7 +798,7 @@ clean::
 # NB: the -maxdepth 3 is for excluding files from contrib/extraction/test
 
 tags:
-	find . -maxdepth 3 -name "*.ml*" | sort -r | xargs \
+	find . -maxdepth 3 -regex ".*\.ml[i4]?" | sort -r | xargs \
 	etags --language=none\
 	      "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
@@ -822,10 +836,13 @@ CAMLP4EXTENSIONS= parsing/argextend.cmo parsing/tacextend.cmo \
 
 GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
 	   lib/dyn.cmo lib/options.cmo \
-	   lib/hashcons.cmo lib/predicate.cmo lib/rtree.cmo $(KERNEL) \
-	   library/summary.cmo library/nameops.cmo library/nametab.cmo \
-	   library/libobject.cmo library/lib.cmo library/global.cmo \
-	   library/goptions.cmo pretyping/rawterm.cmo pretyping/evd.cmo \
+	   lib/hashcons.cmo lib/predicate.cmo lib/rtree.cmo \
+	   $(KERNEL) \
+	   library/libnames.cmo \
+	   library/summary.cmo library/nameops.cmo \
+	   library/nametab.cmo \
+	   library/libobject.cmo library/lib.cmo library/goptions.cmo \
+	   pretyping/rawterm.cmo pretyping/evd.cmo \
 	   parsing/coqast.cmo parsing/genarg.cmo \
 	   proofs/tacexpr.cmo proofs/proof_type.cmo parsing/ast.cmo \
            parsing/lexer.cmo parsing/q_util.cmo parsing/extend.cmo \
@@ -839,9 +856,12 @@ clean::
 	rm -f parsing/grammar.cma
 
 ML4FILES +=parsing/g_basevernac.ml4 parsing/g_minicoq.ml4 \
-	   parsing/g_vernac.ml4 parsing/g_proofs.ml4 parsing/g_cases.ml4 \
-	   parsing/g_constr.ml4 parsing/g_tactic.ml4 parsing/g_ltac.ml4 \
-	   parsing/argextend.ml4 parsing/tacextend.ml4 parsing/vernacextend.ml4
+	   parsing/g_vernac.ml4 parsing/g_proofs.ml4 \
+	   parsing/g_cases.ml4 \
+	   parsing/g_constr.ml4 parsing/g_module.ml4 \
+	   parsing/g_tactic.ml4 parsing/g_ltac.ml4 \
+	   parsing/argextend.ml4 parsing/tacextend.ml4 \
+	   parsing/vernacextend.ml4
 
 # beforedepend:: $(GRAMMARCMO)
 
@@ -1002,6 +1022,9 @@ depend: beforedepend
 	done
 # 5. Finally, we erase the generated .ml files
 	rm -f $(ML4FILESML)
+# 6. Since .depend contains correct dependencies .depend.devel can be deleted
+# (see dev/Makefile.dir for details about this file)
+	if [ -e makefile ]; then >.depend.devel; else rm -f .depend.devel; fi
 
 ml4clean::
 	rm -f $(ML4FILESML)
@@ -1011,3 +1034,10 @@ clean::
 
 include .depend
 include .depend.coq
+
+
+# this sets up developper supporting stuff
+devel:	
+	touch .depend.devel
+	$(MAKE) -f dev/Makefile.devel setup-devel
+	$(MAKE) dev/top_printers.cmo

contrib/correctness/ptactic.ml

@@ -229,7 +229,7 @@ let correctness_hook _ ref =
   register pf_id None
 
 let correctness s p opttac =
-  Library.check_required_module ["Coq";"correctness";"Correctness"];
+  Library.check_required_library ["Coq";"correctness";"Correctness"];
   Pmisc.reset_names();
   let p,oc,cty,v = coqast_of_prog p in
   let env = Global.env () in

contrib/extraction/common.ml

@@ -16,9 +16,10 @@ open Table
 open Mlutil
 open Extraction
 open Ocaml
-open Nametab
+open Libnames
 open Util
 open Declare
+open Nametab
 
 (*s Modules considerations *)
 
@@ -34,7 +35,7 @@ let qualid_of_dirpath d =
 
 let is_long_module d r = 
   let dir = repr_dirpath d 
-  and dir' = repr_dirpath (dirpath (sp_of_r r)) in 
+  and dir' = repr_dirpath (fst (decode_kn (kn_of_r r))) in 
   let l = List.length dir 
   and l' = List.length dir' in 
   if l' < l then false 
@@ -106,7 +107,7 @@ let cache r f =
 
 module ToplevelParams = struct
   let globals () = Idset.empty
-  let rename_global r _ = Termops.id_of_global (Global.env()) r
+  let rename_global r _ = id_of_global None r
   let pp_global r _ _ = Printer.pr_global r
 end
 
@@ -124,7 +125,7 @@ module MonoParams = struct
   let rename_global r upper = 
     cache r
       (fun r -> 
-	 let id = Termops.id_of_global (Global.env()) r in
+	 let id = id_of_global None r in
 	 rename_global_id 
 	   (if upper || (is_construct r) 
 	    then uppercase_id id else lowercase_id id))
@@ -143,7 +144,7 @@ module ModularParams = struct
 
   let clash r id = 
     try 
-      let _ = locate (make_qualid (dirpath (sp_of_r r)) id)
+      let _ = locate (make_qualid (fst (decode_kn (kn_of_r r))) id)
       in true
     with _ -> false
 
@@ -160,7 +161,7 @@ module ModularParams = struct
   let rename_global r upper =
     cache r 
       (fun r -> 
-	 let id = Termops.id_of_global (Global.env()) r in 
+	 let id = id_of_global None r in 
 	 if upper || (is_construct r) then 
 	   rename_global_id r id (uppercase_id id) "Coq_"
 	 else rename_global_id r id (lowercase_id id) "coq_")

contrib/extraction/common.mli

@@ -12,7 +12,7 @@ open Pp
 open Miniml
 open Mlutil
 open Names
-open Nametab
+open Libnames
 
 val is_long_module : dir_path -> global_reference -> bool
 

contrib/extraction/extract_env.ml

@@ -18,6 +18,7 @@ open Extraction
 open Miniml
 open Table
 open Mlutil
+open Libnames
 open Nametab
 open Vernacinterp
 open Common
@@ -83,12 +84,12 @@ let check_modules m =
   We just keep constants and inductives. *)
 
 let extract_module m =
-  let seg = Library.module_segment (Some m) in
+  let seg = Declaremods.module_objects (MPfile m) in
   let get_reference = function
-    | sp, Leaf o ->
+    | (_,kn), Leaf o ->
 	(match Libobject.object_tag o with
-	   | "CONSTANT" | "PARAMETER" -> ConstRef sp
-	   | "INDUCTIVE" -> IndRef (sp,0)
+	   | "CONSTANT" | "PARAMETER" -> ConstRef kn
+	   | "INDUCTIVE" -> IndRef (kn,0)
 	   | _ -> failwith "caught")
     | _ -> failwith "caught"
   in
@@ -204,7 +205,7 @@ let print_user_extract r =
 let decl_in_r r0 = function 
   | Dterm (r,_) -> r = r0
   | Dtype (r,_,_) -> r = r0
-  | Dind ((_,r,_)::_, _) -> sp_of_r r = sp_of_r r0
+  | Dind ((_,r,_)::_, _) -> kn_of_r r = kn_of_r r0
   | Dind ([],_) -> false
   | DdummyType r -> r = r0
   | DcustomTerm (r,_) ->  r = r0 

contrib/extraction/extract_env.mli

@@ -12,7 +12,7 @@
 
 open Util
 open Names
-open Nametab
+open Libnames
 
 val extraction : qualid located -> unit
 val extraction_rec : qualid located list -> unit