From e7b4aba11391bede785799237a73ef7bd16d0372 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Oct 2022 18:04:31 +0200
Subject: Use "polonius" in the names instead of "nll"

---
 Makefile                      | 17 +++++++++--------
 tests/misc/BetreeNll.fst      | 41 -----------------------------------------
 tests/misc/BetreePolonius.fst | 41 +++++++++++++++++++++++++++++++++++++++++
 3 files changed, 50 insertions(+), 49 deletions(-)
 delete mode 100644 tests/misc/BetreeNll.fst
 create mode 100644 tests/misc/BetreePolonius.fst

diff --git a/Makefile b/Makefile
index f75d00be..93ff7431 100644
--- a/Makefile
+++ b/Makefile
@@ -37,7 +37,7 @@ build:
 tests: build trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-constants \
-	trans-nll-betree_nll trans-nll-betree_main
+	trans-polonius-betree_polonius trans-polonius-betree_main
 
 # Verify the F* files generated by the translation
 .PHONY: verify
@@ -60,8 +60,8 @@ trans-hashmap: SUBDIR:=hashmap
 trans-hashmap_main: TRANS_OPTIONS += -template-clauses
 trans-hashmap_main: SUBDIR:=hashmap_on_disk
 
-trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
-trans-nll-betree_nll: SUBDIR:=misc
+trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
+trans-polonius-betree_polonius: SUBDIR:=misc
 
 trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
 trans-constants: SUBDIR:=misc
@@ -69,8 +69,8 @@ trans-constants: SUBDIR:=misc
 trans-external: TRANS_OPTIONS +=
 trans-external: SUBDIR:=misc
 
-trans-nll-betree_main: TRANS_OPTIONS += -template-clauses
-trans-nll-betree_main: SUBDIR:=betree
+trans-polonius-betree_main: TRANS_OPTIONS += -template-clauses
+trans-polonius-betree_main: SUBDIR:=betree
 
 # 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
@@ -80,15 +80,16 @@ gen-llbc-%: build
 	cd $(CHARON_HOME) && $(MAKE) test-$*
 
 # Generic rule to test the translation of an LLBC file.
-# Note that the non-linear lifetime files are generated in the tests-nll subdirectory.
+# Note that the files requiring the Polonius borrow-checker are generated
+# in the tests-polonius subdirectory.
 .PHONY: trans-%
 trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc
-trans-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/llbc
+trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
 
 trans-%: gen-llbc-%
 	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
 
-trans-nll-%: gen-llbc-nll-%
+trans-polonius-%: gen-llbc-polonius-%
 	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
 
 .PHONY: doc
diff --git a/tests/misc/BetreeNll.fst b/tests/misc/BetreeNll.fst
deleted file mode 100644
index b548a18b..00000000
--- a/tests/misc/BetreeNll.fst
+++ /dev/null
@@ -1,41 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_nll] *)
-module BetreeNll
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_nll::List] *)
-type list_t (t : Type0) =
-| ListCons : t -> list_t t -> list_t t
-| ListNil : list_t t
-
-(** [betree_nll::get_list_at_x] *)
-let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
-  begin match ls with
-  | ListCons hd tl ->
-    if hd = x
-    then Return (ListCons hd tl)
-    else
-      begin match get_list_at_x_fwd tl x with
-      | Fail -> Fail
-      | Return l -> Return l
-      end
-  | ListNil -> Return ListNil
-  end
-
-(** [betree_nll::get_list_at_x] *)
-let rec get_list_at_x_back
-  (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) =
-  begin match ls with
-  | ListCons hd tl ->
-    if hd = x
-    then Return ret
-    else
-      begin match get_list_at_x_back tl x ret with
-      | Fail -> Fail
-      | Return tl0 -> Return (ListCons hd tl0)
-      end
-  | ListNil -> Return ret
-  end
-
diff --git a/tests/misc/BetreePolonius.fst b/tests/misc/BetreePolonius.fst
new file mode 100644
index 00000000..2bac07b6
--- /dev/null
+++ b/tests/misc/BetreePolonius.fst
@@ -0,0 +1,41 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_polonius] *)
+module BetreePolonius
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_polonius::List] *)
+type list_t (t : Type0) =
+| ListCons : t -> list_t t -> list_t t
+| ListNil : list_t t
+
+(** [betree_polonius::get_list_at_x] *)
+let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
+  begin match ls with
+  | ListCons hd tl ->
+    if hd = x
+    then Return (ListCons hd tl)
+    else
+      begin match get_list_at_x_fwd tl x with
+      | Fail -> Fail
+      | Return l -> Return l
+      end
+  | ListNil -> Return ListNil
+  end
+
+(** [betree_polonius::get_list_at_x] *)
+let rec get_list_at_x_back
+  (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) =
+  begin match ls with
+  | ListCons hd tl ->
+    if hd = x
+    then Return ret
+    else
+      begin match get_list_at_x_back tl x ret with
+      | Fail -> Fail
+      | Return tl0 -> Return (ListCons hd tl0)
+      end
+  | ListNil -> Return ret
+  end
+
-- 
cgit v1.2.3