Add the generated HOL4 files

1 files changed, 25 insertions, 4 deletions

diff --git a/Makefile b/Makefile
index 9df5f264..606ed3eb 100644
--- a/Makefile
+++ b/Makefile
@@ -119,6 +119,8 @@ trans-no_nested_borrows trans-paper: SUBDIR := misc
 tfstar-no_nested_borrows tfstar-paper:
 tlean-no_nested_borrows: SUBDIR := misc-no_nested_borrows
 tlean-paper: SUBDIR := misc-paper
+thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows
+thol4-paper: SUBDIR := misc-paper
 
 trans-loops: OPTIONS += -no-state
 trans-loops: SUBDIR := misc
@@ -126,18 +128,21 @@ tfstar-loops: OPTIONS += -decreases-clauses -template-clauses
 tcoq-loops: OPTIONS += -use-fuel -no-split-files
 tlean-loops: SUBDIR := misc-loops
 tlean-loops: OPTIONS += -decreases-clauses -template-clauses
+thol4-loops: SUBDIR := misc-loops
 
 trans-hashmap: OPTIONS += -no-state
 trans-hashmap: SUBDIR := hashmap
 tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap: OPTIONS += -use-fuel
 tlean-hashmap: OPTIONS += -decreases-clauses -template-clauses
+thol4-hashmap: OPTIONS +=
 
 trans-hashmap_main: OPTIONS +=
 trans-hashmap_main: SUBDIR := hashmap_on_disk
 tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap_main: OPTIONS += -use-fuel
 tlean-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
+thol4-hashmap_main: OPTIONS +=
 
 transp-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state
 transp-polonius_list: SUBDIR := misc
@@ -145,6 +150,8 @@ tfstarp-polonius_list: OPTIONS +=
 tcoqp-polonius_list: OPTIONS +=
 tleanp-polonius_list: SUBDIR := misc-polonius_list
 tleanp-polonius_list: OPTIONS +=
+thol4p-polonius_list: SUBDIR := misc-polonius_list
+thol4p-polonius_list: OPTIONS +=
 
 trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state
 trans-constants: SUBDIR := misc
@@ -152,6 +159,8 @@ tfstar-constants: OPTIONS +=
 tcoq-constants: OPTIONS +=
 tlean-constants: SUBDIR := misc-constants
 tlean-constants: OPTIONS +=
+thol4-constants: SUBDIR := misc-constants
+thol4-constants: OPTIONS +=
 
 trans-external: OPTIONS +=
 trans-external: SUBDIR := misc
@@ -159,6 +168,8 @@ tfstar-external: OPTIONS +=
 tcoq-external: OPTIONS +=
 tlean-external: SUBDIR := misc-external
 tlean-external: OPTIONS +=
+thol4-external: SUBDIR := misc-external
+thol4-external: OPTIONS +=
 
 BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
 transp-betree_main: OPTIONS += -backward-no-state-update
@@ -166,6 +177,7 @@ transp-betree_main: SUBDIR:=betree
 tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
 tcoqp-betree_main: OPTIONS += -use-fuel
 tleanp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
+thol4-betree_main: 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.
@@ -200,14 +212,14 @@ gen-llbcp-%:
 .PHONY: trans-%
 trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
 trans-%: FILE = $*
-trans-%: gen-llbc-% tfstar-% tcoq-% tlean-%
+trans-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-%
 	echo "# Test $* done"
 
 # "p" stands for "Polonius"
 .PHONY: transp-%
 transp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
 transp-%: FILE = $*
-transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-%
+transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
 	echo "# Test $* done"
 
 .PHONY: tfstar-%
@@ -243,8 +255,6 @@ tlean-%: BACKEND_SUBDIR := lean
 tlean-%:
 	$(AENEAS_CMD)
 
-
-
 # "p" stands for "Polonius"
 .PHONY: tleanp-%
 
@@ -259,6 +269,17 @@ tleanp-%: BACKEND_SUBDIR := lean
 tleanp-%:
 	$(AENEAS_CMD)
 
+.PHONY: thol4-%
+thol4-%: OPTIONS += -backend hol4 -test-trans-units
+thol4-%: BACKEND_SUBDIR := hol4
+thol4-%:
+	$(AENEAS_CMD)
+
+.PHONY: thol4p-%
+thol4p-%: OPTIONS += -backend hol4 -test-trans-units
+thol4p-%: BACKEND_SUBDIR := hol4
+thol4p-%:
+	$(AENEAS_CMD)
 
 # Nix - TODO: add the lean tests
 .PHONY: nix