From f99f60902d7492902110fb091c52e58e1ed9cd32 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 19 Oct 2017 18:17:33 +0200
Subject: 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.
---
 Makefile.build | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

(limited to 'Makefile.build')

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
-- 
cgit v1.2.3