diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-19 18:17:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-29 23:02:38 +0200 |
| commit | f99f60902d7492902110fb091c52e58e1ed9cd32 (patch) | |
| tree | 44773647a104546828143de8636a5388b10b3260 /Makefile.build | |
| parent | e25d69f5d47f7ad6584bf54ea48e42fd482c95e0 (diff) | |
Use a homebrew parser to replace the GEXTEND extension points of Camlp5.
The parser is stupid and the syntax is almost the same as the previous one.
The only difference is that one needs to wrap OCaml code between { braces }
so that quoting works out of the box.
Files requiring such a syntax are handled specifically by the type system
and need to have a .mlg extension instead of a .ml4 one.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index b85418243..884b73347 100644 --- a/Makefile.build +++ b/Makefile.build @@ -342,6 +342,7 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h GRAMBASEDEPS := grammar/q_util.cmi GRAMCMO := grammar/q_util.cmo \ grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo +COQPPCMO := grammar/coqpp_parse.cmo grammar/coqpp_lex.cmo grammar/argextend.cmo : $(GRAMBASEDEPS) grammar/q_util.cmo : $(GRAMBASEDEPS) @@ -349,6 +350,10 @@ grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \ grammar/argextend.cmo +grammar/coqpp_parse.cmi: grammar/coqpp_ast.cmi +grammar/coqpp_parse.cmo: grammar/coqpp_ast.cmi grammar/coqpp_parse.cmi +grammar/coqpp_lex.cmo: grammar/coqpp_ast.cmi grammar/coqpp_parse.cmo + ## Ocaml compiler with the right options and -I for grammar GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \ @@ -359,11 +364,15 @@ GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \ grammar/grammar.cma : $(GRAMCMO) $(SHOW)'Testing $@' @touch grammar/test.mlp - $(HIDE)$(GRAMC) -pp '$(CAMLP5O) -I $(MYCAMLP5LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test + $(HIDE)$(GRAMC) -pp '$(CAMLP5O) $^ -impl' -impl grammar/test.mlp -o grammar/test @rm -f grammar/test.* grammar/test $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ +grammar/coqpp: $(COQPPCMO) grammar/coqpp_main.ml + $(SHOW)'OCAMLC -a $@' + $(HIDE)$(GRAMC) $^ -linkall -o $@ + ## Support of Camlp5 and Camlp5 COMPATCMO:= @@ -376,6 +385,10 @@ grammar/%.cmo: grammar/%.mlp | $(COMPATCMO) $(SHOW)'OCAMLC -c -pp $<' $(HIDE)$(GRAMC) -c -pp '$(GRAMPP)' -impl $< +grammar/%.cmo: grammar/%.ml | $(COMPATCMO) + $(SHOW)'OCAMLC -c -pp $<' + $(HIDE)$(GRAMC) -c $< + grammar/%.cmi: grammar/%.mli $(SHOW)'OCAMLC -c $<' $(HIDE)$(GRAMC) -c $< @@ -746,11 +759,18 @@ plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLLEX $<' $(HIDE)$(OCAMLLEX) -o $@ "$*.mll" -%.ml: %.ml4 $(CAMLP5DEPS) +%.ml %.mli: %.mly + $(SHOW)'OCAMLYACC $<' + $(HIDE)$(OCAMLYACC) --strict "$*.mly" + +%.ml: %.ml4 $(CAMLP5DEPS) grammar/coqpp $(SHOW)'CAMLP5O $<' $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \ $(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@ +%.ml: %.mlg grammar/coqpp + $(SHOW)'COQPP $<' + $(HIDE)grammar/coqpp $< ########################################################################### # Dependencies of ML code |