diff options
author | Son Ho | 2024-03-19 04:52:36 +0100 |
---|---|---|
committer | Son Ho | 2024-03-19 04:52:36 +0100 |
commit | d6efe5bd2878135bf1fc3fc31fec66322c5b8a86 (patch) | |
tree | d159905f81d12d64ccac0a0a33e2e5b531ca9125 | |
parent | a24f42ff7f0ae3c2aeb51decb0d0c90d6e50ffac (diff) |
Update the demo
Diffstat (limited to '')
-rw-r--r-- | tests/coq/demo/Demo.v | 48 | ||||
-rw-r--r-- | tests/fstar/demo/Demo.fst | 45 | ||||
-rw-r--r-- | tests/lean/Demo/Demo.lean | 47 | ||||
-rw-r--r-- | tests/lean/Demo/Properties.lean | 16 |
4 files changed, 126 insertions, 30 deletions
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v index ec7ca29d..48067c02 100644 --- a/tests/coq/demo/Demo.v +++ b/tests/coq/demo/Demo.v @@ -34,8 +34,14 @@ Definition use_mul2_add1 (x : u32) (y : u32) : result u32 := Definition incr (x : u32) : result u32 := u32_add x 1%u32. +(** [demo::use_incr]: + Source: 'src/demo.rs', lines 25:0-25:17 *) +Definition use_incr : result unit := + i <- incr 0%u32; i1 <- incr i; _ <- incr i1; Return tt +. + (** [demo::CList] - Source: 'src/demo.rs', lines 27:0-27:17 *) + Source: 'src/demo.rs', lines 34:0-34:17 *) Inductive CList_t (T : Type) := | CList_CCons : T -> CList_t T -> CList_t T | CList_CNil : CList_t T @@ -45,7 +51,7 @@ Arguments CList_CCons { _ }. Arguments CList_CNil { _ }. (** [demo::list_nth]: - Source: 'src/demo.rs', lines 32:0-32:56 *) + Source: 'src/demo.rs', lines 39:0-39:56 *) Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T := match n with | O => Fail_ OutOfFuel @@ -61,7 +67,7 @@ Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T := . (** [demo::list_nth_mut]: - Source: 'src/demo.rs', lines 47:0-47:68 *) + Source: 'src/demo.rs', lines 54:0-54:68 *) Fixpoint list_nth_mut (T : Type) (n : nat) (l : CList_t T) (i : u32) : result (T * (T -> result (CList_t T))) @@ -89,7 +95,7 @@ Fixpoint list_nth_mut . (** [demo::list_nth_mut1]: loop 0: - Source: 'src/demo.rs', lines 62:0-71:1 *) + Source: 'src/demo.rs', lines 69:0-78:1 *) Fixpoint list_nth_mut1_loop (T : Type) (n : nat) (l : CList_t T) (i : u32) : result (T * (T -> result (CList_t T))) @@ -116,7 +122,7 @@ Fixpoint list_nth_mut1_loop . (** [demo::list_nth_mut1]: - Source: 'src/demo.rs', lines 62:0-62:77 *) + Source: 'src/demo.rs', lines 69:0-69:77 *) Definition list_nth_mut1 (T : Type) (n : nat) (l : CList_t T) (i : u32) : result (T * (T -> result (CList_t T))) @@ -125,7 +131,7 @@ Definition list_nth_mut1 . (** [demo::i32_id]: - Source: 'src/demo.rs', lines 73:0-73:28 *) + Source: 'src/demo.rs', lines 80:0-80:28 *) Fixpoint i32_id (n : nat) (i : i32) : result i32 := match n with | O => Fail_ OutOfFuel @@ -136,8 +142,30 @@ Fixpoint i32_id (n : nat) (i : i32) : result i32 := end . +(** [demo::list_tail]: + Source: 'src/demo.rs', lines 88:0-88:64 *) +Fixpoint list_tail + (T : Type) (n : nat) (l : CList_t T) : + result ((CList_t T) * (CList_t T -> result (CList_t T))) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match l with + | CList_CCons t tl => + p <- list_tail T n1 tl; + let (c, list_tail_back) := p in + let back_'a := + fun (ret : CList_t T) => + tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in + Return (c, back_'a) + | CList_CNil => Return (CList_CNil, Return) + end + end +. + (** Trait declaration: [demo::Counter] - Source: 'src/demo.rs', lines 83:0-83:17 *) + Source: 'src/demo.rs', lines 97:0-97:17 *) Record Counter_t (Self : Type) := mkCounter_t { Counter_t_incr : Self -> result (usize * Self); }. @@ -146,19 +174,19 @@ Arguments mkCounter_t { _ }. Arguments Counter_t_incr { _ }. (** [demo::{(demo::Counter for usize)}::incr]: - Source: 'src/demo.rs', lines 88:4-88:31 *) + Source: 'src/demo.rs', lines 102:4-102:31 *) Definition counterUsize_incr (self : usize) : result (usize * usize) := self1 <- usize_add self 1%usize; Return (self, self1) . (** Trait implementation: [demo::{(demo::Counter for usize)}] - Source: 'src/demo.rs', lines 87:0-87:22 *) + Source: 'src/demo.rs', lines 101:0-101:22 *) Definition CounterUsize : Counter_t usize := {| Counter_t_incr := counterUsize_incr; |}. (** [demo::use_counter]: - Source: 'src/demo.rs', lines 95:0-95:59 *) + Source: 'src/demo.rs', lines 109:0-109:59 *) Definition use_counter (T : Type) (counterInst : Counter_t T) (cnt : T) : result (usize * T) := counterInst.(Counter_t_incr) cnt diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst index d13d2ba3..5651b80f 100644 --- a/tests/fstar/demo/Demo.fst +++ b/tests/fstar/demo/Demo.fst @@ -28,14 +28,19 @@ let use_mul2_add1 (x : u32) (y : u32) : result u32 = let incr (x : u32) : result u32 = u32_add x 1 +(** [demo::use_incr]: + Source: 'src/demo.rs', lines 25:0-25:17 *) +let use_incr : result unit = + let* i = incr 0 in let* i1 = incr i in let* _ = incr i1 in Return () + (** [demo::CList] - Source: 'src/demo.rs', lines 27:0-27:17 *) + Source: 'src/demo.rs', lines 34:0-34:17 *) type cList_t (t : Type0) = | CList_CCons : t -> cList_t t -> cList_t t | CList_CNil : cList_t t (** [demo::list_nth]: - Source: 'src/demo.rs', lines 32:0-32:56 *) + Source: 'src/demo.rs', lines 39:0-39:56 *) let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t = if is_zero n then Fail OutOfFuel @@ -48,7 +53,7 @@ let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t = end (** [demo::list_nth_mut]: - Source: 'src/demo.rs', lines 47:0-47:68 *) + Source: 'src/demo.rs', lines 54:0-54:68 *) let rec list_nth_mut (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result (t & (t -> result (cList_t t))) @@ -74,7 +79,7 @@ let rec list_nth_mut end (** [demo::list_nth_mut1]: loop 0: - Source: 'src/demo.rs', lines 62:0-71:1 *) + Source: 'src/demo.rs', lines 69:0-78:1 *) let rec list_nth_mut1_loop (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result (t & (t -> result (cList_t t))) @@ -99,7 +104,7 @@ let rec list_nth_mut1_loop end (** [demo::list_nth_mut1]: - Source: 'src/demo.rs', lines 62:0-62:77 *) + Source: 'src/demo.rs', lines 69:0-69:77 *) let list_nth_mut1 (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result (t & (t -> result (cList_t t))) @@ -107,7 +112,7 @@ let list_nth_mut1 let* (x, back_'a) = list_nth_mut1_loop t n l i in Return (x, back_'a) (** [demo::i32_id]: - Source: 'src/demo.rs', lines 73:0-73:28 *) + Source: 'src/demo.rs', lines 80:0-80:28 *) let rec i32_id (n : nat) (i : i32) : result i32 = if is_zero n then Fail OutOfFuel @@ -117,21 +122,41 @@ let rec i32_id (n : nat) (i : i32) : result i32 = then Return 0 else let* i1 = i32_sub i 1 in let* i2 = i32_id n1 i1 in i32_add i2 1 +(** [demo::list_tail]: + Source: 'src/demo.rs', lines 88:0-88:64 *) +let rec list_tail + (t : Type0) (n : nat) (l : cList_t t) : + result ((cList_t t) & (cList_t t -> result (cList_t t))) + = + if is_zero n + then Fail OutOfFuel + else + let n1 = decrease n in + begin match l with + | CList_CCons x tl -> + let* (c, list_tail_back) = list_tail t n1 tl in + let back_'a = + fun ret -> let* tl1 = list_tail_back ret in Return (CList_CCons x tl1) + in + Return (c, back_'a) + | CList_CNil -> Return (CList_CNil, Return) + end + (** Trait declaration: [demo::Counter] - Source: 'src/demo.rs', lines 83:0-83:17 *) + Source: 'src/demo.rs', lines 97:0-97:17 *) noeq type counter_t (self : Type0) = { incr : self -> result (usize & self); } (** [demo::{(demo::Counter for usize)}::incr]: - Source: 'src/demo.rs', lines 88:4-88:31 *) + Source: 'src/demo.rs', lines 102:4-102:31 *) let counterUsize_incr (self : usize) : result (usize & usize) = let* self1 = usize_add self 1 in Return (self, self1) (** Trait implementation: [demo::{(demo::Counter for usize)}] - Source: 'src/demo.rs', lines 87:0-87:22 *) + Source: 'src/demo.rs', lines 101:0-101:22 *) let counterUsize : counter_t usize = { incr = counterUsize_incr; } (** [demo::use_counter]: - Source: 'src/demo.rs', lines 95:0-95:59 *) + Source: 'src/demo.rs', lines 109:0-109:59 *) let use_counter (t : Type0) (counterInst : counter_t t) (cnt : t) : result (usize & t) = counterInst.incr cnt diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 854b4853..f38b5cd3 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -36,14 +36,23 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 := def incr (x : U32) : Result U32 := x + 1#u32 +/- [demo::use_incr]: + Source: 'src/demo.rs', lines 25:0-25:17 -/ +def use_incr : Result Unit := + do + let i ← incr 0#u32 + let i1 ← incr i + let _ ← incr i1 + Result.ret () + /- [demo::CList] - Source: 'src/demo.rs', lines 27:0-27:17 -/ + Source: 'src/demo.rs', lines 34:0-34:17 -/ inductive CList (T : Type) := | CCons : T → CList T → CList T | CNil : CList T /- [demo::list_nth]: - Source: 'src/demo.rs', lines 32:0-32:56 -/ + Source: 'src/demo.rs', lines 39:0-39:56 -/ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := match l with | CList.CCons x tl => @@ -55,7 +64,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := | CList.CNil => Result.fail .panic /- [demo::list_nth_mut]: - Source: 'src/demo.rs', lines 47:0-47:68 -/ + Source: 'src/demo.rs', lines 54:0-54:68 -/ divergent def list_nth_mut (T : Type) (l : CList T) (i : U32) : Result (T × (T → Result (CList T))) @@ -79,7 +88,7 @@ divergent def list_nth_mut | CList.CNil => Result.fail .panic /- [demo::list_nth_mut1]: loop 0: - Source: 'src/demo.rs', lines 62:0-71:1 -/ + Source: 'src/demo.rs', lines 69:0-78:1 -/ divergent def list_nth_mut1_loop (T : Type) (l : CList T) (i : U32) : Result (T × (T → Result (CList T))) @@ -102,7 +111,7 @@ divergent def list_nth_mut1_loop | CList.CNil => Result.fail .panic /- [demo::list_nth_mut1]: - Source: 'src/demo.rs', lines 62:0-62:77 -/ + Source: 'src/demo.rs', lines 69:0-69:77 -/ def list_nth_mut1 (T : Type) (l : CList T) (i : U32) : Result (T × (T → Result (CList T))) @@ -112,7 +121,7 @@ def list_nth_mut1 Result.ret (t, back_'a) /- [demo::i32_id]: - Source: 'src/demo.rs', lines 73:0-73:28 -/ + Source: 'src/demo.rs', lines 80:0-80:28 -/ divergent def i32_id (i : I32) : Result I32 := if i = 0#i32 then Result.ret 0#i32 @@ -121,26 +130,44 @@ divergent def i32_id (i : I32) : Result I32 := let i2 ← i32_id i1 i2 + 1#i32 +/- [demo::list_tail]: + Source: 'src/demo.rs', lines 88:0-88:64 -/ +divergent def list_tail + (T : Type) (l : CList T) : + Result ((CList T) × (CList T → Result (CList T))) + := + match l with + | CList.CCons t tl => + do + let (c, list_tail_back) ← list_tail T tl + let back_'a := + fun ret => + do + let tl1 ← list_tail_back ret + Result.ret (CList.CCons t tl1) + Result.ret (c, back_'a) + | CList.CNil => Result.ret (CList.CNil, Result.ret) + /- Trait declaration: [demo::Counter] - Source: 'src/demo.rs', lines 83:0-83:17 -/ + Source: 'src/demo.rs', lines 97:0-97:17 -/ structure Counter (Self : Type) where incr : Self → Result (Usize × Self) /- [demo::{(demo::Counter for usize)}::incr]: - Source: 'src/demo.rs', lines 88:4-88:31 -/ + Source: 'src/demo.rs', lines 102:4-102:31 -/ def CounterUsize.incr (self : Usize) : Result (Usize × Usize) := do let self1 ← self + 1#usize Result.ret (self, self1) /- Trait implementation: [demo::{(demo::Counter for usize)}] - Source: 'src/demo.rs', lines 87:0-87:22 -/ + Source: 'src/demo.rs', lines 101:0-101:22 -/ def CounterUsize : Counter Usize := { incr := CounterUsize.incr } /- [demo::use_counter]: - Source: 'src/demo.rs', lines 95:0-95:59 -/ + Source: 'src/demo.rs', lines 109:0-109:59 -/ def use_counter (T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) := CounterInst.incr cnt diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean index cdec7332..e514ac3e 100644 --- a/tests/lean/Demo/Properties.lean +++ b/tests/lean/Demo/Properties.lean @@ -65,4 +65,20 @@ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : termination_by x.val.toNat decreasing_by scalar_decr_tac +theorem list_tail_spec {T : Type} [Inhabited T] (l : CList T) : + ∃ back, list_tail T l = ret (CList.CNil, back) ∧ + ∀ tl', ∃ l', back tl' = ret l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by + rw [list_tail] + match l with + | CNil => + simp_all + | CCons hd tl => + simp_all + progress as ⟨ back ⟩ + simp + -- Proving the backward function + intro tl' + progress + simp_all + end demo |