Merge pull request #73 from AeneasVerif/son/demo

Add some demo files

Makefile

@@ -93,7 +93,7 @@ tests: test-no_nested_borrows test-paper \
 	testp-polonius_list testp-betree_main \
 	ctest-testp-betree_main \
 	test-loops \
-	test-arrays test-traits test-bitwise
+	test-arrays test-traits test-bitwise test-demo
 
 # Verify the F* files generated by the translation
 .PHONY: verify
@@ -148,6 +148,13 @@ tcoq-loops: OPTIONS += -use-fuel
 tlean-loops: SUBDIR :=
 thol4-loops: SUBDIR := misc-loops
 
+test-demo: OPTIONS +=
+test-demo: SUBDIR := demo
+tfstar-demo: OPTIONS += -use-fuel
+tcoq-demo: OPTIONS += -use-fuel
+tlean-demo: SUBDIR := Demo
+thol4-demo: OPTIONS +=
+
 # TODO: reactivate -test-trans-units
 test-hashmap: OPTIONS += -split-files
 test-hashmap: SUBDIR := hashmap

tests/coq/demo/Demo.v

@@ -0,0 +1,167 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [demo] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module Demo.
+
+(** [demo::choose]:
+    Source: 'src/demo.rs', lines 5:0-5:70 *)
+Definition choose
+  (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
+  if b
+  then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a)
+  else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a)
+.
+
+(** [demo::mul2_add1]:
+    Source: 'src/demo.rs', lines 13:0-13:31 *)
+Definition mul2_add1 (x : u32) : result u32 :=
+  i <- u32_add x x; u32_add i 1%u32
+.
+
+(** [demo::use_mul2_add1]:
+    Source: 'src/demo.rs', lines 17:0-17:43 *)
+Definition use_mul2_add1 (x : u32) (y : u32) : result u32 :=
+  i <- mul2_add1 x; u32_add i y
+.
+
+(** [demo::incr]:
+    Source: 'src/demo.rs', lines 21:0-21:31 *)
+Definition incr (x : u32) : result u32 :=
+  u32_add x 1%u32.
+
+(** [demo::CList]
+    Source: 'src/demo.rs', lines 27:0-27:17 *)
+Inductive CList_t (T : Type) :=
+| CList_CCons : T -> CList_t T -> CList_t T
+| CList_CNil : CList_t T
+.
+
+Arguments CList_CCons { _ }.
+Arguments CList_CNil { _ }.
+
+(** [demo::list_nth]:
+    Source: 'src/demo.rs', lines 32:0-32:56 *)
+Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match l with
+    | CList_CCons x tl =>
+      if i s= 0%u32
+      then Return x
+      else (i1 <- u32_sub i 1%u32; list_nth T n1 tl i1)
+    | CList_CNil => Fail_ Failure
+    end
+  end
+.
+
+(** [demo::list_nth_mut]:
+    Source: 'src/demo.rs', lines 47:0-47:68 *)
+Fixpoint list_nth_mut
+  (T : Type) (n : nat) (l : CList_t T) (i : u32) :
+  result (T * (T -> result (CList_t T)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match l with
+    | CList_CCons x tl =>
+      if i s= 0%u32
+      then
+        let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in
+        Return (x, back_'a)
+      else (
+        i1 <- u32_sub i 1%u32;
+        p <- list_nth_mut T n1 tl i1;
+        let (t, list_nth_mut_back) := p in
+        let back_'a :=
+          fun (ret : T) =>
+            tl1 <- list_nth_mut_back ret; Return (CList_CCons x tl1) in
+        Return (t, back_'a))
+    | CList_CNil => Fail_ Failure
+    end
+  end
+.
+
+(** [demo::list_nth_mut1]: loop 0:
+    Source: 'src/demo.rs', lines 62:0-71:1 *)
+Fixpoint list_nth_mut1_loop
+  (T : Type) (n : nat) (l : CList_t T) (i : u32) :
+  result (T * (T -> result (CList_t T)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match l with
+    | CList_CCons x tl =>
+      if i s= 0%u32
+      then
+        let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in
+        Return (x, back_'a)
+      else (
+        i1 <- u32_sub i 1%u32;
+        p <- list_nth_mut1_loop T n1 tl i1;
+        let (t, back_'a) := p in
+        let back_'a1 :=
+          fun (ret : T) => tl1 <- back_'a ret; Return (CList_CCons x tl1) in
+        Return (t, back_'a1))
+    | CList_CNil => Fail_ Failure
+    end
+  end
+.
+
+(** [demo::list_nth_mut1]:
+    Source: 'src/demo.rs', lines 62:0-62:77 *)
+Definition list_nth_mut1
+  (T : Type) (n : nat) (l : CList_t T) (i : u32) :
+  result (T * (T -> result (CList_t T)))
+  :=
+  p <- list_nth_mut1_loop T n l i; let (t, back_'a) := p in Return (t, back_'a)
+.
+
+(** [demo::i32_id]:
+    Source: 'src/demo.rs', lines 73:0-73:28 *)
+Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    if i s= 0%i32
+    then Return 0%i32
+    else (i1 <- i32_sub i 1%i32; i2 <- i32_id n1 i1; i32_add i2 1%i32)
+  end
+.
+
+(** Trait declaration: [demo::Counter]
+    Source: 'src/demo.rs', lines 83:0-83:17 *)
+Record Counter_t (Self : Type) := mkCounter_t {
+  Counter_t_incr : Self -> result (usize * Self);
+}.
+
+Arguments mkCounter_t { _ }.
+Arguments Counter_t_incr { _ }.
+
+(** [demo::{usize}::incr]:
+    Source: 'src/demo.rs', lines 88:4-88:31 *)
+Definition usize_incr (self : usize) : result (usize * usize) :=
+  self1 <- usize_add self 1%usize; Return (self, self1)
+.
+
+(** Trait implementation: [demo::{usize}]
+    Source: 'src/demo.rs', lines 87:0-87:22 *)
+Definition demo_CounterUsizeInst : Counter_t usize := {|
+  Counter_t_incr := usize_incr;
+|}.
+
+(** [demo::use_counter]:
+    Source: 'src/demo.rs', lines 95:0-95:59 *)
+Definition use_counter
+  (T : Type) (counterTInst : Counter_t T) (cnt : T) : result (usize * T) :=
+  counterTInst.(Counter_t_incr) cnt
+.
+
+End Demo.

tests/coq/demo/Makefile

@@ -0,0 +1,23 @@
+# This file was automatically generated - modify ../Makefile.template instead
+# Makefile originally taken from coq-club
+
+%: Makefile.coq phony
+	+make -f Makefile.coq $@
+
+all: Makefile.coq
+	+make -f Makefile.coq all
+
+clean: Makefile.coq
+	+make -f Makefile.coq clean
+	rm -f Makefile.coq
+
+Makefile.coq: _CoqProject Makefile
+	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
+
+_CoqProject: ;
+
+Makefile: ;
+
+phony: ;
+
+.PHONY: all clean phony