From 304490110509324a20c7c2c3be9bf61931fa3a1c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 17 Dec 2022 10:50:43 +0100
Subject: Make minor modifications and generate code for loops

---
 tests/fstar/misc/Loops.Clauses.Template.fst | 13 ++++++
 tests/fstar/misc/Loops.Clauses.fst          | 12 ++++++
 tests/fstar/misc/Loops.Funs.fst             | 66 +++++++++++++++++++++++++++++
 tests/fstar/misc/Loops.Types.fst            | 12 ++++++
 4 files changed, 103 insertions(+)
 create mode 100644 tests/fstar/misc/Loops.Clauses.Template.fst
 create mode 100644 tests/fstar/misc/Loops.Clauses.fst
 create mode 100644 tests/fstar/misc/Loops.Funs.fst
 create mode 100644 tests/fstar/misc/Loops.Types.fst

(limited to 'tests/fstar')

diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
new file mode 100644
index 00000000..a898e9fb
--- /dev/null
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -0,0 +1,13 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops]: templates for the decreases clauses *)
+module Loops.Clauses.Template
+open Primitives
+open Loops.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [loops::list_nth_mut_loop]: decreases clause *)
+unfold
+let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
+  admit ()
+
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
new file mode 100644
index 00000000..e09eda9a
--- /dev/null
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -0,0 +1,12 @@
+(** [loops]: templates for the decreases clauses *)
+module Loops.Clauses
+open Primitives
+open Loops.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [loops::list_nth_mut_loop]: decreases clause *)
+unfold
+let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
+  i
+
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
new file mode 100644
index 00000000..f5339339
--- /dev/null
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -0,0 +1,66 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops]: function definitions *)
+module Loops.Funs
+open Primitives
+include Loops.Types
+include Loops.Clauses
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [loops::list_nth_mut_loop] *)
+let rec list_nth_mut_loop_loop0_fwd
+  (t : Type0) (ls : list_t t) (i : u32) :
+  Tot (result t) (decreases (list_nth_mut_loop_decreases t ls i))
+  =
+  begin match ls with
+  | ListCons x tl ->
+    if i = 0
+    then Return x
+    else
+      begin match u32_sub i 1 with
+      | Fail e -> Fail e
+      | Return i0 ->
+        begin match list_nth_mut_loop_loop0_fwd t tl i0 with
+        | Fail e -> Fail e
+        | Return x0 -> Return x0
+        end
+      end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop] *)
+let list_nth_mut_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
+  begin match list_nth_mut_loop_loop0_fwd t ls i with
+  | Fail e -> Fail e
+  | Return x -> Return x
+  end
+
+(** [loops::list_nth_mut_loop] *)
+let rec list_nth_mut_loop_loop0_back
+  (t : Type0) (ls : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t)) (decreases (list_nth_mut_loop_decreases t ls i))
+  =
+  begin match ls with
+  | ListCons x tl ->
+    if i = 0
+    then Return (ListCons ret tl)
+    else
+      begin match u32_sub i 1 with
+      | Fail e -> Fail e
+      | Return i0 ->
+        begin match list_nth_mut_loop_loop0_back t tl i0 ret with
+        | Fail e -> Fail e
+        | Return l -> Return (ListCons x l)
+        end
+      end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop] *)
+let list_nth_mut_loop_back
+  (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
+  begin match list_nth_mut_loop_loop0_back t ls i ret with
+  | Fail e -> Fail e
+  | Return l -> Return l
+  end
+
diff --git a/tests/fstar/misc/Loops.Types.fst b/tests/fstar/misc/Loops.Types.fst
new file mode 100644
index 00000000..2e032fe7
--- /dev/null
+++ b/tests/fstar/misc/Loops.Types.fst
@@ -0,0 +1,12 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops]: type definitions *)
+module Loops.Types
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [loops::List] *)
+type list_t (t : Type0) =
+| ListCons : t -> list_t t -> list_t t
+| ListNil : list_t t
+
-- 
cgit v1.2.3