Use "-as" to put CompCert modules in a compcert.xxx namespace.

Simplified the scripts "coq" and "pg".
Updated deps.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

5 files changed, 50 insertions, 28 deletions

diff --git a/.depend b/.depend
index e55e84c..057f4f9 100644
--- a/.depend
+++ b/.depend
@@ -31,7 +31,7 @@ backend/CminorSel.vo backend/CminorSel.glob backend/CminorSel.v.beautified: back
 $(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob $(ARCH)/SelectOp.v.beautified: $(ARCH)/SelectOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo
 backend/SelectLong.vo backend/SelectLong.glob backend/SelectLong.v.beautified: backend/SelectLong.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo common/Errors.vo
 backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo
-$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
+$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
 backend/SelectLongproof.vo backend/SelectLongproof.glob backend/SelectLongproof.v.beautified: backend/SelectLongproof.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectLong.vo
 backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectLongproof.vo
 backend/Registers.vo backend/Registers.glob backend/Registers.v.beautified: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo
@@ -51,13 +51,13 @@ backend/Kildall.vo backend/Kildall.glob backend/Kildall.v.beautified: backend/Ki
 backend/Liveness.vo backend/Liveness.glob backend/Liveness.v.beautified: backend/Liveness.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo
 $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob $(ARCH)/ConstpropOp.v.beautified: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo
 backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo $(ARCH)/ConstpropOp.vo
-$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo
+$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo
 backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo
 $(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob $(ARCH)/CombineOp.v.beautified: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo $(ARCH)/SelectOp.vo
 backend/CSE.vo backend/CSE.glob backend/CSE.v.beautified: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo
-$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/CombineOp.vo backend/CSE.vo
+$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/RTL.vo $(ARCH)/CombineOp.vo backend/CSE.vo
 backend/CSEproof.vo backend/CSEproof.glob backend/CSEproof.v.beautified: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo
-$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo
+$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo
 backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: backend/Locations.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo
 $(ARCH)/$(VARIANT)/Conventions1.vo $(ARCH)/$(VARIANT)/Conventions1.glob $(ARCH)/$(VARIANT)/Conventions1.v.beautified: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo
 backend/Conventions.vo backend/Conventions.glob backend/Conventions.v.beautified: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions1.vo
@@ -78,10 +78,10 @@ $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Stacklayout.glob $(ARCH)/$(
 backend/Stacking.vo backend/Stacking.glob backend/Stacking.v.beautified: backend/Stacking.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Lineartyping.vo
 backend/Stackingproof.vo backend/Stackingproof.glob backend/Stackingproof.v.beautified: backend/Stackingproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo
 $(ARCH)/Asm.vo $(ARCH)/Asm.glob $(ARCH)/Asm.v.beautified: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo
-$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo
+$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo
 backend/Asmgenproof0.vo backend/Asmgenproof0.glob backend/Asmgenproof0.v.beautified: backend/Asmgenproof0.v lib/Coqlib.vo lib/Intv.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo
-$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo backend/Asmgenproof0.vo
-$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo
+$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo backend/Conventions.vo
+$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo
 cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo
 cfrontend/Cop.vo cfrontend/Cop.glob cfrontend/Cop.v.beautified: cfrontend/Cop.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo cfrontend/Ctypes.vo
 cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo
diff --git a/Makefile b/Makefile
index 0db4118..cced7da 100644
--- a/Makefile
+++ b/Makefile
@@ -13,22 +13,28 @@
 include Makefile.config
 
 DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver \
-  flocq/Core flocq/Prop flocq/Calc flocq/Appli
+  flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight
 
-INCLUDES=$(patsubst %,-I %, $(DIRS))
+RECDIRS=lib common backend cfrontend driver flocq exportclight
 
-COQC=coqc -q $(INCLUDES)
-COQDEP=coqdep $(INCLUDES)
+COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) \
+  -I $(ARCH)/$(VARIANT) -as compcert.$(ARCH).$(VARIANT) \
+  -I $(ARCH) -as compcert.$(ARCH)
+
+CAMLINCLUDES=$(patsubst %,-I %, $(DIRS)) -I extraction -I cparser
+
+COQC=coqc -q $(COQINCLUDES)
+COQDEP=coqdep $(COQINCLUDES)
 COQDOC=coqdoc
-COQEXEC=coqtop $(INCLUDES) -batch -load-vernac-source
-COQCHK=coqchk $(INCLUDES)
+COQEXEC=coqtop $(COQINCLUDES) -batch -load-vernac-source
+COQCHK=coqchk $(COQINCLUDES)
 
 OCAMLBUILD=ocamlbuild
 OCB_OPTIONS=\
   -j 2 \
   -no-hygiene \
   -no-links \
-  -I extraction -I cparser $(INCLUDES)
+  $(CAMLINCLUDES)
 OCB_OPTIONS_CHECKLINK=\
   $(OCB_OPTIONS) \
   -I checklink \
@@ -251,6 +257,9 @@ check-admitted: $(FILES)
 check-proof: $(FILES)
 	$(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements 
 
+print-includes:
+	@echo $(COQINCLUDES)
+
 include .depend
 
 FORCE:
diff --git a/coq b/coq
index ce3e1ed..ea08805 100755
--- a/coq
+++ b/coq
@@ -3,8 +3,7 @@
 # Use the Makefile to rebuild dependencies if needed
 # Recompile the modified file after coqide editing
 
-ARCH=`sed -n -e 's/^ARCH=//p' Makefile.config`
-VARIANT=`sed -n -e 's/^VARIANT=//p' Makefile.config`
+INCLUDES=`make print-includes`
 
 make -q ${1}o || {
   make -n ${1}o | grep -v "\\b${1}\\b" | \
@@ -13,5 +12,4 @@ make -q ${1}o || {
    done)
 }
 
-coqide -I lib -I common -I $ARCH/$VARIANT -I $ARCH -I backend -I cfrontend -I flocq -I flocq/Appli -I flocq/Calc -I flocq/Core -I flocq/Prop $1 \
-&& make ${1}o
+coqide $INCLUDES $1 && make ${1}o
diff --git a/doc/coq2html.mll b/doc/coq2html.mll
index 9c30bea..4f04f98 100644
--- a/doc/coq2html.mll
+++ b/doc/coq2html.mll
@@ -35,9 +35,11 @@ let path sp id =
   | _   , _    -> sp ^ "." ^ id
 
 let add_module m =
+  (*eprintf "add_module %s\n" m;*)
   Hashtbl.add xref_modules m ()
 
 let add_reference curmod pos dp sp id ty =
+  (*eprintf "add_reference %s %d %s %s %s %s\n" curmod pos dp sp id ty;*)
   if not (Hashtbl.mem xref_table (curmod, pos))
   then Hashtbl.add xref_table (curmod, pos) (Ref(dp, path sp id, ty))
 
@@ -51,15 +53,19 @@ let coqlib_url = "http://coq.inria.fr/library/"
 
 let re_coqlib = Str.regexp "Coq\\."
 let re_sane_path = Str.regexp "[A-Za-z0-9_.]+$"
+let re_shortname = Str.regexp "^.*\\."
+
+let shortname m = Str.replace_first re_shortname "" m
 
 let crossref m pos =
+  (*eprintf "crossref %s %d\n" m pos;*)
   try match Hashtbl.find xref_table (m, pos) with
   | Def(p, ty) ->
       Anchor p
   | Ref(m', p, ty) ->
       let url =
         if Hashtbl.mem xref_modules m' then
-          m' ^ ".html"
+          shortname m' ^ ".html"
         else if Str.string_match re_coqlib m' 0 then
           coqlib_url ^ m' ^ ".html"
         else
@@ -367,7 +373,7 @@ and verbatim = parse
 and globfile = parse
   | eof
       { () }
-  | "F" (ident as m) space* "\n"
+  | "F" (path as m) space* "\n"
       { current_module := m; add_module m;
         globfile lexbuf }
   | "R" (integer as pos) ":" (integer as pos2)
@@ -394,14 +400,16 @@ let output_name = ref "-"
 
 let process_file f =
   if Filename.check_suffix f ".v" then begin
-    current_module := Filename.chop_suffix (Filename.basename f) ".v";
+    let pref_f = Filename.chop_suffix f ".v" in
+    let base_f = Filename.basename pref_f in
+    current_module := 
+      "compcert." ^ Str.global_replace (Str.regexp "/") "." pref_f;
     let ic = open_in f in
     if !output_name = "-" then
       oc := stdout
     else
-      oc := open_out (Str.global_replace (Str.regexp "%") !current_module
-                                                          !output_name);
-    start_html_page !current_module;
+      oc := open_out (Str.global_replace (Str.regexp "%") base_f !output_name);
+    start_html_page base_f;
     coq_bol (Lexing.from_channel ic);
     end_html_page();
     if !output_name <> "-" then (close_out !oc; oc := stdout);
diff --git a/pg b/pg
index 9242303..33a70ce 100755
--- a/pg
+++ b/pg
@@ -4,9 +4,7 @@
 # Recompile the modified file after coqide editing
 
 PWD=`pwd`
-ARCH=$PWD/`sed -n -e 's/^ARCH=//p' Makefile.config`
-VARIANT=$ARCH/`sed -n -e 's/^VARIANT=//p' Makefile.config`
-
+INCLUDES=`make print-includes`
 
 make -q ${1}o || {
   make -n ${1}o | grep -v "\\b${1}\\b" | \
@@ -14,9 +12,18 @@ make -q ${1}o || {
     sh -c "$cmd" || exit 2
    done)
 }
+
 COQPROGNAME="coqtop"
-COQPROGARGS="\"-I\" \"$PWD/lib\" \"-I\" \"$PWD/common\" \"-I\" \"$VARIANT\" \"-I\" \"$ARCH\" \"-I\" \"$PWD/backend\" \"-I\" \"$PWD/cfrontend\" \"-I\" \"$PWD/flocq\" \"-I\" \"$PWD/flocq/Appli\" \"-I\" \"$PWD/flocq/Calc\" \"-I\" \"$PWD/flocq/Core\" \"-I\" \"$PWD/flocq/Prop\""
 
+COQPROGARGS=""
+for arg in $INCLUDES; do
+  case "$arg" in
+    -I|-R|-as|compcert*)
+      COQPROGARGS="$COQPROGARGS \"$arg\"";;
+    *)
+      COQPROGARGS="$COQPROGARGS \"$PWD/$arg\"";;
+  esac
+done
 
 emacs --eval "(setq coq-prog-name \"$COQPROGNAME\")" \
  --eval "(setq coq-prog-args '($COQPROGARGS))" $1 \