diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-04-29 13:58:18 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-04-29 13:58:18 +0000 |
| commit | f1d236b83003eda71e12840732d159fd23b1b771 (patch) | |
| tree | 0edad805ea24f7b626d2c6fee9fc50da23acfc47 /Makefile | |
| parent | 39df8fb19bacb38f317abf06de432b83296dfdd1 (diff) | |
Integration of Jacques-Henri Jourdan's verified parser.
(Merge of branch newparser.)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 21 |
1 files changed, 18 insertions, 3 deletions
@@ -16,9 +16,9 @@ include Makefile.config DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver \ - flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight + flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight cparser cparser/validator -RECDIRS=lib common backend cfrontend driver flocq exportclight +RECDIRS=lib common backend cfrontend driver flocq exportclight cparser COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) \ -I $(ARCH)/$(VARIANT) -as compcert.$(ARCH).$(VARIANT) \ @@ -26,6 +26,7 @@ COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) \ CAMLINCLUDES=$(patsubst %,-I %, $(DIRS)) -I extraction -I cparser +MENHIR=menhir COQC="$(COQBIN)coqc" -q $(COQINCLUDES) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" @@ -109,13 +110,24 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Cstrategy.v Cexec.v \ Cshmgen.v Cshmgenproof.v \ Csharpminor.v Cminorgen.v Cminorgenproof.v +# LR(1) parser validator + +PARSERVALIDATOR=Alphabet.v Interpreter_complete.v Interpreter.v \ + Validator_complete.v Automaton.v Interpreter_correct.v Main.v \ + Validator_safe.v Grammar.v Interpreter_safe.v Tuples.v + +# Parser + +PARSER=Cabs.v Parser.v + # Putting everything together (in driver/) DRIVER=Compopts.v Compiler.v Complements.v # All source files -FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) +FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ + $(PARSERVALIDATOR) $(PARSER) # Symbolic links vs. copy @@ -222,6 +234,9 @@ driver/Configuration.ml: Makefile.config VERSION echo let version = "\"$$version\"") \ > driver/Configuration.ml +cparser/Parser.v: cparser/Parser.vy + $(MENHIR) --coq cparser/Parser.vy + depend: $(FILES) exportclight/Clightdefs.v $(COQDEP) $^ \ | sed -e 's|$(ARCH)/$(VARIANT)/|$$(ARCH)/$$(VARIANT)/|g' \ |