summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2022-12-17 10:50:43 +0100
committerSon HO2023-02-03 11:21:46 +0100
commit304490110509324a20c7c2c3be9bf61931fa3a1c (patch)
tree47d47f70f70cc6cafa393ebe8cb7de68cf3b6739 /tests
parent464ecbb8d756de32f6d0c14dca4e90e90c76c5bc (diff)
Make minor modifications and generate code for loops
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/misc/Loops.v72
-rw-r--r--tests/coq/misc/_CoqProject1
-rw-r--r--tests/fstar/misc/Loops.Clauses.Template.fst13
-rw-r--r--tests/fstar/misc/Loops.Clauses.fst12
-rw-r--r--tests/fstar/misc/Loops.Funs.fst66
-rw-r--r--tests/fstar/misc/Loops.Types.fst12
6 files changed, 176 insertions, 0 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
new file mode 100644
index 00000000..48de76c2
--- /dev/null
+++ b/tests/coq/misc/Loops.v
@@ -0,0 +1,72 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module Loops.
+
+(** [loops::List] *)
+Inductive List_t (T : Type) :=
+| ListCons : T -> List_t T -> List_t T
+| ListNil : List_t T
+.
+
+Arguments ListCons {T} _ _.
+Arguments ListNil {T}.
+
+(** [loops::list_nth_mut_loop] *)
+Fixpoint list_nth_mut_loop_loop0_fwd
+ (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match ls with
+ | ListCons x tl =>
+ if i s= 0%u32
+ then Return x
+ else (
+ i0 <- u32_sub i 1%u32;
+ t <- list_nth_mut_loop_loop0_fwd T n0 tl i0;
+ Return t)
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_loop] *)
+Definition list_nth_mut_loop_fwd
+ (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+ t <- list_nth_mut_loop_loop0_fwd T n ls i; Return t
+.
+
+(** [loops::list_nth_mut_loop] *)
+Fixpoint list_nth_mut_loop_loop0_back
+ (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match ls with
+ | ListCons x tl =>
+ if i s= 0%u32
+ then Return (ListCons ret tl)
+ else (
+ i0 <- u32_sub i 1%u32;
+ l <- list_nth_mut_loop_loop0_back T n0 tl i0 ret;
+ Return (ListCons x l))
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_loop] *)
+Definition list_nth_mut_loop_back
+ (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ l <- list_nth_mut_loop_loop0_back T n ls i ret; Return l
+.
+
+End Loops .
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index c9ee0ff6..db6c2742 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -3,6 +3,7 @@
-arg -w
-arg all
+Loops.v
Primitives.v
External_Funs.v
Constants.v
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
+