Make good progress on the Coq backend

1 files changed, 65 insertions, 31 deletions

diff --git a/Makefile b/Makefile
index 6f35eaac..c4ec50ef 100644
--- a/Makefile
+++ b/Makefile
@@ -34,7 +34,7 @@ AENEAS_EXE ?= bin/aeneas.exe
 # - unfold all the monadic let bindings to matches (required by F*)
 # - insert calls to the normalizer in the translated code to test the
 #   generated unit functions
-OPTIONS += -unfold-monads -test-trans-units
+OPTIONS +=
 
 #
 # The rules use (and update) the following variables
@@ -43,6 +43,8 @@ OPTIONS += -unfold-monads -test-trans-units
 CHARON_TEST_DIR =
 # The options with which to call Charon
 CHARON_OPTIONS =
+# The backend sub-directory in which to generate the files
+BACKEND_SUBDIR :=
 # The directory in which to extract the result of the translation
 SUBDIR :=
 
@@ -86,8 +88,8 @@ clean:
 tests: trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-constants \
-	trans-polonius-polonius_list trans-polonius-betree_main \
-	test-trans-polonius-betree_main
+	transp-polonius_list transp-betree_main \
+	test-transp-betree_main
 
 # Verify the F* files generated by the translation
 .PHONY: verify
@@ -106,70 +108,102 @@ CHARON_CMD = cd $(CHARON_TEST_DIR) && NOT_ALL_TESTS=1 $(MAKE) test-$*
 endif
 
 # The command to run Aeneas on the proper llbc file
-AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/fstar/$(SUBDIR) $(OPTIONS)
+AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BACKEND_SUBDIR)/$(SUBDIR) $(OPTIONS)
 
 
 # Add specific options to some tests
 trans-no_nested_borrows trans-paper: \
-	OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
+	OPTIONS += -test-units -test-trans-units -no-split-files -no-state
 trans-no_nested_borrows trans-paper: SUBDIR:=misc
+tfstar-no_nested_borrows tfstar-paper:
 
-trans-hashmap: OPTIONS += -template-clauses -no-state
+trans-hashmap: OPTIONS += -no-state
 trans-hashmap: SUBDIR:=hashmap
+tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
 
-trans-hashmap_main: OPTIONS += -template-clauses
+trans-hashmap_main: OPTIONS +=
 trans-hashmap_main: SUBDIR:=hashmap_on_disk
+tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
 
-trans-polonius-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
-trans-polonius-polonius_list: SUBDIR:=misc
+transp-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state
+transp-polonius_list: SUBDIR:=misc
+tfstarp-polonius_list: OPTIONS +=
 
-trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
+trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state
 trans-constants: SUBDIR:=misc
+tfstar-constants: OPTIONS +=
 
 trans-external: OPTIONS +=
 trans-external: SUBDIR:=misc
+tfstar-external: OPTIONS +=
 
-BETREE_OPTIONS = -template-clauses
-trans-polonius-betree_main: OPTIONS += $(BETREE_OPTIONS) -backward-no-state-update
-trans-polonius-betree_main: SUBDIR:=betree
+BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
+transp-betree_main: OPTIONS += -backward-no-state-update
+transp-betree_main: SUBDIR:=betree
+tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
 
 # Additional test on the betree: translate it without `-backward-no-state-update`.
 # This generates very ugly code, but is good to test the translation.
-test-trans-polonius-betree_main: trans-polonius-betree_main
-test-trans-polonius-betree_main: OPTIONS += $(BETREE_OPTIONS)
-test-trans-polonius-betree_main: SUBDIR:=betree_back_stateful
-test-trans-polonius-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-test-trans-polonius-betree_main: FILE = betree_main
-test-trans-polonius-betree_main:
+.PHONY: test-transp-betree_main
+test-transp-betree_main: transp-betree_main
+test-transp-betree_main: OPTIONS += -backend fstar -unfold-monads -test-trans-units
+test-transp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
+test-transp-betree_main: BACKEND_SUBDIR := "fstar"
+test-transp-betree_main: SUBDIR:=betree_back_stateful
+test-transp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
+test-transp-betree_main: FILE = betree_main
+test-transp-betree_main:
 	$(AENEAS_CMD)
 
 # Generic rules to extract the LLBC from a rust file
 # We use the rules in Charon's Makefile to generate the .llbc files: the options
 # vary with the test files.
-.PHONY: gen-llbc-polonius-%
-gen-llbc-polonius-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-gen-llbc-polonius-%:
-	$(CHARON_CMD)
-
 .PHONY: gen-llbc-%
 gen-llbc-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
 gen-llbc-%:
 	$(CHARON_CMD)
 
-# Generic rule to test the translation of an LLBC file.
+# "p" stands for "Polonius"
+.PHONY: gen-llbcp-%
+gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
+gen-llbcp-%:
+	$(CHARON_CMD)
+
+# Generic rules to test the translation of an LLBC file.
 # Note that the files requiring the Polonius borrow-checker are generated
 # in the tests-polonius subdirectory.
 .PHONY: trans-%
-trans-%:
-trans-polonius-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
 trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
+trans-%: FILE = $*
+trans-%: gen-llbc-% tfstar-% tcoq-%
+	echo "# Test $* done"
+
+# "p" stands for "Polonius"
+.PHONY: transp-%
+transp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
+transp-%: FILE = $*
+transp-%: gen-llbcp-% tfstarp-%
+	echo "# Test $* done"
+
+.PHONY: tfstar-%
+tfstar-%: OPTIONS += -backend fstar -unfold-monads -test-trans-units
+tfstar-%: BACKEND_SUBDIR := fstar
+tfstar-%:
+	$(AENEAS_CMD)
 
-trans-polonius-%: FILE = $*
-trans-polonius-%: gen-llbc-polonius-%
+# "p" stands for "Polonius"
+.PHONY: tfstarp-%
+tfstarp-%: OPTIONS += -backend fstar -unfold-monads -test-trans-units
+tfstarp-%: BACKEND_SUBDIR := fstar
+tfstarp-%:
 	$(AENEAS_CMD)
 
-trans-%: FILE = $*
-trans-%: gen-llbc-%
+# TODO: -test-trans-units
+# It doesn't work on vec_push_fwd, I don't understand why.
+.PHONY: tcoq-%
+tcoq-%: OPTIONS += -backend coq -decompose-monads
+tcoq-%: BACKEND_SUBDIR := coq
+tcoq-%:
 	$(AENEAS_CMD)
 
 # Nix