Integration du front-end CIL developpe par Thomas Moniot

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

2 files changed, 45 insertions, 29 deletions

diff --git a/extraction/.depend b/extraction/.depend
index e18eef8..aa7e42a 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -8,6 +8,10 @@
     BinInt.cmi 
 ../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CList.cmx BinPos.cmx \
     BinInt.cmx 
+../caml/Cil2Csyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
+    CList.cmi BinInt.cmi AST.cmi 
+../caml/Cil2Csyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
+    CList.cmx BinInt.cmx AST.cmx 
 ../caml/CMlexer.cmo: ../caml/Camlcoq.cmo ../caml/CMparser.cmi \
     ../caml/CMlexer.cmi 
 ../caml/CMlexer.cmx: ../caml/Camlcoq.cmx ../caml/CMparser.cmx \
@@ -30,10 +34,20 @@
     ../caml/Camlcoq.cmx BinPos.cmx BinInt.cmx AST.cmx ../caml/Coloringaux.cmi 
 ../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo 
 ../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx 
-../caml/Main2.cmo: ../caml/PrintPPC.cmi Main.cmi Datatypes.cmi \
-    ../caml/CMtypecheck.cmi ../caml/CMparser.cmi ../caml/CMlexer.cmi 
-../caml/Main2.cmx: ../caml/PrintPPC.cmx Main.cmx Datatypes.cmx \
-    ../caml/CMtypecheck.cmx ../caml/CMparser.cmx ../caml/CMlexer.cmx 
+../caml/Main2.cmo: ../caml/PrintPPC.cmi ../caml/PrintCsyntax.cmo Main.cmi \
+    Datatypes.cmi Csyntax.cmi ../caml/Cil2Csyntax.cmo ../caml/CMtypecheck.cmi \
+    ../caml/CMparser.cmi ../caml/CMlexer.cmi 
+../caml/Main2.cmx: ../caml/PrintPPC.cmx ../caml/PrintCsyntax.cmx Main.cmx \
+    Datatypes.cmx Csyntax.cmx ../caml/Cil2Csyntax.cmx ../caml/CMtypecheck.cmx \
+    ../caml/CMparser.cmx ../caml/CMlexer.cmx 
+../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \
+    ../caml/Camlcoq.cmo CList.cmi AST.cmi 
+../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \
+    ../caml/Camlcoq.cmx CList.cmx AST.cmx 
+../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
+    CList.cmi AST.cmi 
+../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
+    CList.cmx AST.cmx 
 ../caml/PrintPPC.cmo: PPC.cmi Datatypes.cmi ../caml/Camlcoq.cmo CList.cmi \
     AST.cmi ../caml/PrintPPC.cmi 
 ../caml/PrintPPC.cmx: PPC.cmx Datatypes.cmx ../caml/Camlcoq.cmx CList.cmx \
@@ -76,11 +90,11 @@ CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \
 Csharpminor.cmi: Zmax.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \
     Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \
     AST.cmi 
-cshmgen.cmi: Peano.cmi Integers.cmi Floats.cmi Datatypes.cmi csyntax.cmi \
+Cshmgen.cmi: Peano.cmi Integers.cmi Floats.cmi Datatypes.cmi Csyntax.cmi \
     Csharpminor.cmi CList.cmi AST.cmi 
-csyntax.cmi: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \
+Csyntax.cmi: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \
     Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
-ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi csyntax.cmi Coqlib.cmi \
+Ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \
     CList.cmi AST.cmi 
 Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi 
 FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi \
@@ -113,7 +127,7 @@ Mach.cmi: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi \
     Locations.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi \
     CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
 Main.cmi: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \
-    Linearize.cmi Datatypes.cmi ctyping.cmi csyntax.cmi cshmgen.cmi \
+    Linearize.cmi Datatypes.cmi Ctyping.cmi Csyntax.cmi Cshmgen.cmi \
     Constprop.cmi Cminorgen.cmi Cminor.cmi CSE.cmi Allocation.cmi AST.cmi 
 Maps.cmi: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \
     BinInt.cmi 
@@ -227,18 +241,18 @@ Csharpminor.cmo: Zmax.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \
 Csharpminor.cmx: Zmax.cmx Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx \
     Globalenvs.cmx Floats.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx \
     AST.cmx Csharpminor.cmi 
-cshmgen.cmo: Peano.cmi Integers.cmi Floats.cmi Datatypes.cmi csyntax.cmi \
-    Csharpminor.cmi CList.cmi AST.cmi cshmgen.cmi 
-cshmgen.cmx: Peano.cmx Integers.cmx Floats.cmx Datatypes.cmx csyntax.cmx \
-    Csharpminor.cmx CList.cmx AST.cmx cshmgen.cmi 
-csyntax.cmo: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \
-    Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi csyntax.cmi 
-csyntax.cmx: Zmax.cmx Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx \
-    Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx csyntax.cmi 
-ctyping.cmo: Specif.cmi Maps.cmi Datatypes.cmi csyntax.cmi Coqlib.cmi \
-    CList.cmi AST.cmi ctyping.cmi 
-ctyping.cmx: Specif.cmx Maps.cmx Datatypes.cmx csyntax.cmx Coqlib.cmx \
-    CList.cmx AST.cmx ctyping.cmi 
+Cshmgen.cmo: Peano.cmi Integers.cmi Floats.cmi Datatypes.cmi Csyntax.cmi \
+    Csharpminor.cmi CList.cmi AST.cmi Cshmgen.cmi 
+Cshmgen.cmx: Peano.cmx Integers.cmx Floats.cmx Datatypes.cmx Csyntax.cmx \
+    Csharpminor.cmx CList.cmx AST.cmx Cshmgen.cmi 
+Csyntax.cmo: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \
+    Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Csyntax.cmi 
+Csyntax.cmx: Zmax.cmx Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx \
+    Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx Csyntax.cmi 
+Ctyping.cmo: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \
+    CList.cmi AST.cmi Ctyping.cmi 
+Ctyping.cmx: Specif.cmx Maps.cmx Datatypes.cmx Csyntax.cmx Coqlib.cmx \
+    CList.cmx AST.cmx Ctyping.cmi 
 Datatypes.cmo: Datatypes.cmi 
 Datatypes.cmx: Datatypes.cmi 
 Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \
@@ -312,11 +326,11 @@ Mach.cmx: Zmax.cmx Zdiv.cmx Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx \
     Locations.cmx Integers.cmx Globalenvs.cmx Datatypes.cmx Coqlib.cmx \
     CList.cmx BinPos.cmx BinInt.cmx AST.cmx Mach.cmi 
 Main.cmo: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \
-    Linearize.cmi Datatypes.cmi ctyping.cmi csyntax.cmi cshmgen.cmi \
+    Linearize.cmi Datatypes.cmi Ctyping.cmi Csyntax.cmi Cshmgen.cmi \
     Constprop.cmi Cminorgen.cmi Cminor.cmi CSE.cmi Allocation.cmi AST.cmi \
     Main.cmi 
 Main.cmx: Tunneling.cmx Stacking.cmx RTLgen.cmx PPCgen.cmx PPC.cmx \
-    Linearize.cmx Datatypes.cmx ctyping.cmx csyntax.cmx cshmgen.cmx \
+    Linearize.cmx Datatypes.cmx Ctyping.cmx Csyntax.cmx Cshmgen.cmx \
     Constprop.cmx Cminorgen.cmx Cminor.cmx CSE.cmx Allocation.cmx AST.cmx \
     Main.cmi 
 Maps.cmo: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \
diff --git a/extraction/Makefile b/extraction/Makefile
index 72bf244..e4dcdbe 100644
--- a/extraction/Makefile
+++ b/extraction/Makefile
@@ -6,10 +6,9 @@ FILES=\
   Coqlib.ml Maps.ml Sets.ml AST.ml Iteration.ml Integers.ml \
   ../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Parmov.ml Values.ml \
   Mem.ml Globalenvs.ml \
-  csyntax.ml ctyping.ml \
-  cshmgen.ml \
+  Csyntax.ml Ctyping.ml Csharpminor.ml Cshmgen.ml \
   Op.ml Cminor.ml Cmconstr.ml \
-  Csharpminor.ml Cminorgen.ml \
+  Cminorgen.ml \
   Registers.ml RTL.ml \
   ../caml/RTLgenaux.ml RTLgen.ml \
   Locations.ml Conventions.ml \
@@ -23,27 +22,30 @@ FILES=\
   Mach.ml Stacking.ml \
   PPC.ml PPCgen.ml \
   Main.ml \
+  ../caml/Cil2Csyntax.ml \
   ../caml/CMparser.ml ../caml/CMlexer.ml ../caml/CMtypecheck.ml \
-  ../caml/PrintPPC.ml ../caml/Main2.ml
+  ../caml/PrintCsyntax.ml ../caml/PrintPPC.ml \
+  ../caml/Main2.ml
 
 EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES))
 GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli)
 
-CAMLINCL=-I ../caml
+CAMLINCL=-I ../caml -I ../cil/obj/x86_LINUX
 OCAMLC=ocamlc -g $(CAMLINCL)
 OCAMLOPT=ocamlopt $(CAMLINCL)
 OCAMLDEP=ocamldep $(CAMLINCL)
+OCAMLLIBS=unix.cma str.cma cil.cma
 
 COQINCL=-I ../lib -I ../common -I ../backend -I ../cfrontend
 COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source
 
 ../ccomp: $(FILES:.ml=.cmo)
-	$(OCAMLC) -o ../ccomp $(FILES:.ml=.cmo)
+	$(OCAMLC) -o ../ccomp $(OCAMLLIBS) $(FILES:.ml=.cmo)
 clean::
 	rm -f ../ccomp
 
 ../ccomp.opt: $(FILES:.ml=.cmx)
-	$(OCAMLOPT) -o ../ccomp.opt $(FILES:.ml=.cmx)
+	$(OCAMLOPT) -o ../ccomp.opt $(OCAMLLIBS:.cma=.cmxa) $(FILES:.ml=.cmx)
 clean::
 	rm -f ../ccomp.opt