Merge pull request #32 from AeneasVerif/son_arrays

Add support for arrays/slices and const generics

1 files changed, 26 insertions, 13 deletions

diff --git a/Makefile b/Makefile
index 1b11592f..a0111b37 100644
--- a/Makefile
+++ b/Makefile
@@ -90,7 +90,8 @@ tests: trans-no_nested_borrows trans-paper \
 	trans-external trans-constants \
 	transp-polonius_list transp-betree_main \
 	test-transp-betree_main \
-	trans-loops
+	trans-loops \
+	trans-array # TODO: generalize to all backends
 
 # Verify the F* files generated by the translation
 .PHONY: verify
@@ -122,6 +123,18 @@ tlean-paper: SUBDIR :=
 thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows
 thol4-paper: SUBDIR := misc-paper
 
+trans-array: OPTIONS += -no-state
+trans-array: SUBDIR := array
+tfstar-array: OPTIONS += -decreases-clauses -template-clauses
+tcoq-array: OPTIONS += -use-fuel
+tlean-array: SUBDIR :=
+tlean-array: OPTIONS +=
+thol4-array: OPTIONS +=
+
+# TODO: activate the arrays for all the backends
+thol4-array:
+	echo "Ignoring the array test for HOL4"
+
 trans-loops: OPTIONS += -no-state
 trans-loops: SUBDIR := misc
 tfstar-loops: OPTIONS += -decreases-clauses -template-clauses
@@ -129,15 +142,15 @@ tcoq-loops: OPTIONS += -use-fuel -no-split-files
 tlean-loops: SUBDIR :=
 thol4-loops: SUBDIR := misc-loops
 
-trans-hashmap: OPTIONS += -no-state
+trans-hashmap: OPTIONS += -no-state -test-trans-units
 trans-hashmap: SUBDIR := hashmap
 tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap: OPTIONS += -use-fuel
 tlean-hashmap: SUBDIR :=
-tlean-hashmap: OPTIONS +=
+tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hashmap.lean file: we do not want to overwrite it
 thol4-hashmap: OPTIONS +=
 
-trans-hashmap_main: OPTIONS +=
+trans-hashmap_main: OPTIONS += -test-trans-units
 trans-hashmap_main: SUBDIR := hashmap_on_disk
 tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap_main: OPTIONS += -use-fuel
@@ -162,7 +175,7 @@ tlean-constants: OPTIONS +=
 thol4-constants: SUBDIR := misc-constants
 thol4-constants: OPTIONS +=
 
-trans-external: OPTIONS +=
+trans-external: OPTIONS += -test-trans-units
 trans-external: SUBDIR := misc
 tfstar-external: OPTIONS +=
 tcoq-external: OPTIONS +=
@@ -172,7 +185,7 @@ thol4-external: SUBDIR := misc-external
 thol4-external: OPTIONS +=
 
 BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
-transp-betree_main: OPTIONS += -backward-no-state-update
+transp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units
 transp-betree_main: SUBDIR:=betree
 tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
 tcoqp-betree_main: OPTIONS += -use-fuel
@@ -224,20 +237,20 @@ transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
 	echo "# Test $* done"
 
 .PHONY: tfstar-%
-tfstar-%: OPTIONS += -backend fstar -test-trans-units
+tfstar-%: OPTIONS += -backend fstar
 tfstar-%: BACKEND_SUBDIR := fstar
 tfstar-%:
 	$(AENEAS_CMD)
 
 # "p" stands for "Polonius"
 .PHONY: tfstarp-%
-tfstarp-%: OPTIONS += -backend fstar -test-trans-units
+tfstarp-%: OPTIONS += -backend fstar
 tfstarp-%: BACKEND_SUBDIR := fstar
 tfstarp-%:
 	$(AENEAS_CMD)
 
 .PHONY: tcoq-%
-tcoq-%: OPTIONS += -backend coq -test-trans-units
+tcoq-%: OPTIONS += -backend coq
 tcoq-%: BACKEND_SUBDIR := coq
 tcoq-%:
 	$(AENEAS_CMD)
@@ -250,7 +263,7 @@ tcoqp-%:
 	$(AENEAS_CMD)
 
 .PHONY: tlean-%
-tlean-%: OPTIONS += -backend lean -test-trans-units
+tlean-%: OPTIONS += -backend lean
 tlean-%: BACKEND_SUBDIR := lean
 tlean-%:
 	$(AENEAS_CMD)
@@ -258,19 +271,19 @@ tlean-%:
 # "p" stands for "Polonius"
 .PHONY: tleanp-%
 
-tleanp-%: OPTIONS += -backend lean -test-trans-units
+tleanp-%: OPTIONS += -backend lean
 tleanp-%: BACKEND_SUBDIR := lean
 tleanp-%:
 	$(AENEAS_CMD)
 
 .PHONY: thol4-%
-thol4-%: OPTIONS += -backend hol4 -test-trans-units
+thol4-%: OPTIONS += -backend hol4
 thol4-%: BACKEND_SUBDIR := hol4
 thol4-%:
 	$(AENEAS_CMD)
 
 .PHONY: thol4p-%
-thol4p-%: OPTIONS += -backend hol4 -test-trans-units
+thol4p-%: OPTIONS += -backend hol4
 thol4p-%: BACKEND_SUBDIR := hol4
 thol4p-%:
 	$(AENEAS_CMD)