Update makefile to make extraction cleaner (#41)

* Update makefile to make extraction cleaner

* Update makefile

.github/workflows/ci_build.yml

@@ -33,6 +33,7 @@ jobs:
         with:
           ocaml-compiler: ${{ env.OCAML_VER }}
           dune-cache: true
+          cache-prefix: "v2"
       - name: install Menhir and Coq
         run: |
           opam update

.gitignore

@@ -1,8 +1,8 @@
 _build
 
 # Ignore generated parser code
-driver/parser.ml
-driver/parser.mli
+**/parser.ml
+**/parser.mli
 theories/**/Parser.v
 
 # Remove Coq compiled code
@@ -14,5 +14,5 @@ theories/**/Parser.v
 *.vok
 *.vos
 .lia.cache
-makefile.coq*
+CoqMakefile.mk*
 *.~undo-tree~

driver/main.ml

@@ -5,7 +5,8 @@ let parse text =
      which we then feed into the parser. *)
   let rec loop lexbuf = lazy (Buf_cons (Lexer.read lexbuf, loop lexbuf)) in
   let token_stream = loop (Lexing.from_string text) in
-  match Parser.prog 50 token_stream with
+  let parse : int -> buffer -> Parser.Cst.obj parse_result = Parser.prog in
+  match parse 50 token_stream with
   | Parsed_pr (e, _) -> Some e
   | Fail_pr_full (_, _) -> None
   | _ -> None

theories/Frontend/ParserExtraction.v

@@ -8,5 +8,4 @@ Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlNatInt.
 Require Import ExtrOcamlNativeString.
 
-(* Meant to be run in this directory *)
-Extraction "../driver/parser.ml" Parser.prog.
+Extraction "parser.ml" Parser.prog.

theories/Makefile

@@ -0,0 +1,55 @@
+empty :=
+space := $(empty) $(empty)
+
+MENHIR := menhir
+
+COQMAKEFILE := CoqMakefile.mk
+COQPROJECTFILE := _CoqProject
+PARSERBASE := parser.ml
+PARSERFILE := ../driver/$(PARSERBASE)
+PARSEREXTRACTIONDIR := Frontend
+PARSEREXTRACTIONCOQFILE := $(PARSEREXTRACTIONDIR)/ParserExtraction.v
+PARSEREXTRACTIONRESULTFILE := $(PARSEREXTRACTIONDIR)/$(PARSERBASE)
+COQPARSERFILE := $(patsubst %.vy,%.v,$(shell find ./ -name '*.vy'))
+COQFILES := $(sort $(shell find ./ -name '*.v') $(COQPARSERFILE))
+
+.PHONY: all
+all: $(COQMAKEFILE) $(COQPARSERFILE)
+	@+$(MAKE) -f "$(COQMAKEFILE)" all
+	@+$(MAKE) "$(PARSERFILE)"
+
+.PHONY: clean
+clean: $(COQMAKEFILE)
+	@+$(MAKE) -f "$(COQMAKEFILE)" cleanall
+	@echo "CLEAN $(COQPARSERFILE) $(PARSERFILE) $(COQMAKEFILE) $(COQMAKEFILE).conf"
+	@rm -f "$(COQPARSERFILE)" "$(PARSERBASE)" "$(PARSERFILE)" "$(COQMAKEFILE)" "$(COQMAKEFILE).conf"
+
+.PHONY: update_CoqProject
+update_CoqProject: clean
+	(echo "-R . Mcltt"; \
+        echo ""; \
+        echo "-arg -w -arg -notation-overridden"; \
+        echo ""; \
+        echo -e "$(subst $(space),\n,$(COQFILES))") > "$(COQPROJECTFILE)"
+
+.PHONY: force
+force: ;
+
+$(COQMAKEFILE): $(COQPROJECTFILE)
+	$(COQBIN)coq_makefile -f "$(COQPROJECTFILE)" -o "$(COQMAKEFILE)"
+
+$(COQPARSERFILE): %.v : %.vy
+	$(MENHIR) --coq "$?"
+
+$(COQPROJECTFILE): ;
+
+$(PARSERBASE): $(PARSEREXTRACTIONCOQFILE)
+	@+$(MAKE) -f "$(COQMAKEFILE)" -B "$(patsubst %.v,%.vo,$?)"
+
+$(PARSERFILE): $(PARSEREXTRACTIONCOQFILE)
+	@+$(MAKE) "$(PARSERBASE)"
+	@echo "MOVE $(PARSERBASE) => $(PARSERFILE)"
+	@mv "$(PARSERBASE)" "$(PARSERFILE)"
+
+%: $(COQMAKEFILE) force
+	@+$(MAKE) -f "$(COQMAKEFILE)" "$@"