From 975ddb208f18cb4ba46293dd788c46eb1ce43938 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 11:58:44 +0200 Subject: Regenerate the test files --- tests/coq/demo/Demo.v | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'tests/coq/demo') diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v index d5a6e535..abec8e88 100644 --- a/tests/coq/demo/Demo.v +++ b/tests/coq/demo/Demo.v @@ -13,8 +13,8 @@ Module Demo. 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) + then let back := fun (ret : T) => Return (ret, y) in Return (x, back) + else let back := fun (ret : T) => Return (x, ret) in Return (y, back) . (** [demo::mul2_add1]: @@ -79,16 +79,16 @@ Fixpoint list_nth_mut | 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) + let back := fun (ret : T) => Return (CList_CCons ret tl) in + Return (x, back) 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 := + let back := fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (CList_CCons x tl1) in - Return (t, back_'a)) + Return (t, back)) | CList_CNil => Fail_ Failure end end @@ -107,15 +107,15 @@ Fixpoint list_nth_mut1_loop | 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) + let back := fun (ret : T) => Return (CList_CCons ret tl) in + Return (x, back) 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)) + let (t, back) := p in + let back1 := + fun (ret : T) => tl1 <- back ret; Return (CList_CCons x tl1) in + Return (t, back1)) | CList_CNil => Fail_ Failure end end @@ -155,10 +155,10 @@ Fixpoint list_tail | CList_CCons t tl => p <- list_tail T n1 tl; let (c, list_tail_back) := p in - let back_'a := + let back := fun (ret : CList_t T) => tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in - Return (c, back_'a) + Return (c, back) | CList_CNil => Return (CList_CNil, Return) end end -- cgit v1.2.3 From b455f94c841b2423898f39bc9b6a4c35a3db56e3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 16:20:20 +0200 Subject: Regenerate the test files --- tests/coq/demo/Demo.v | 40 +++++++++++++++++---------------------- tests/coq/demo/Primitives.v | 46 ++++++++++++++++++++++----------------------- 2 files changed, 40 insertions(+), 46 deletions(-) (limited to 'tests/coq/demo') diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v index abec8e88..00b9b889 100644 --- a/tests/coq/demo/Demo.v +++ b/tests/coq/demo/Demo.v @@ -13,8 +13,8 @@ Module Demo. Definition choose (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) := if b - then let back := fun (ret : T) => Return (ret, y) in Return (x, back) - else let back := fun (ret : T) => Return (x, ret) in Return (y, back) + then let back := fun (ret : T) => Ok (ret, y) in Ok (x, back) + else let back := fun (ret : T) => Ok (x, ret) in Ok (y, back) . (** [demo::mul2_add1]: @@ -37,7 +37,7 @@ Definition incr (x : u32) : result u32 := (** [demo::use_incr]: Source: 'src/demo.rs', lines 25:0-25:17 *) Definition use_incr : result unit := - x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Return tt + x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Ok tt . (** [demo::CList] @@ -58,9 +58,7 @@ Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T := | 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) + if i s= 0%u32 then Ok x else (i1 <- u32_sub i 1%u32; list_nth T n1 tl i1) | CList_CNil => Fail_ Failure end end @@ -78,17 +76,15 @@ Fixpoint list_nth_mut match l with | CList_CCons x tl => if i s= 0%u32 - then - let back := fun (ret : T) => Return (CList_CCons ret tl) in - Return (x, back) + then let back := fun (ret : T) => Ok (CList_CCons ret tl) in Ok (x, back) 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 := - fun (ret : T) => - tl1 <- list_nth_mut_back ret; Return (CList_CCons x tl1) in - Return (t, back)) + fun (ret : T) => tl1 <- list_nth_mut_back ret; Ok (CList_CCons x tl1) + in + Ok (t, back)) | CList_CNil => Fail_ Failure end end @@ -106,16 +102,14 @@ Fixpoint list_nth_mut1_loop match l with | CList_CCons x tl => if i s= 0%u32 - then - let back := fun (ret : T) => Return (CList_CCons ret tl) in - Return (x, back) + then let back := fun (ret : T) => Ok (CList_CCons ret tl) in Ok (x, back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut1_loop T n1 tl i1; let (t, back) := p in - let back1 := - fun (ret : T) => tl1 <- back ret; Return (CList_CCons x tl1) in - Return (t, back1)) + let back1 := fun (ret : T) => tl1 <- back ret; Ok (CList_CCons x tl1) + in + Ok (t, back1)) | CList_CNil => Fail_ Failure end end @@ -137,7 +131,7 @@ Fixpoint i32_id (n : nat) (i : i32) : result i32 := | O => Fail_ OutOfFuel | S n1 => if i s= 0%i32 - then Return 0%i32 + then Ok 0%i32 else (i1 <- i32_sub i 1%i32; i2 <- i32_id n1 i1; i32_add i2 1%i32) end . @@ -157,9 +151,9 @@ Fixpoint list_tail let (c, list_tail_back) := p in let back := fun (ret : CList_t T) => - tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in - Return (c, back) - | CList_CNil => Return (CList_CNil, Return) + tl1 <- list_tail_back ret; Ok (CList_CCons t tl1) in + Ok (c, back) + | CList_CNil => Ok (CList_CNil, Ok) end end . @@ -176,7 +170,7 @@ Arguments Counter_t_incr { _ }. (** [demo::{(demo::Counter for usize)}::incr]: 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) + self1 <- usize_add self 1%usize; Ok (self, self1) . (** Trait implementation: [demo::{(demo::Counter for usize)}] diff --git a/tests/coq/demo/Primitives.v b/tests/coq/demo/Primitives.v index 990e27e4..e84d65ce 100644 --- a/tests/coq/demo/Primitives.v +++ b/tests/coq/demo/Primitives.v @@ -19,19 +19,19 @@ Inductive error := | OutOfFuel. Inductive result A := - | Return : A -> result A + | Ok : A -> result A | Fail_ : error -> result A. -Arguments Return {_} a. +Arguments Ok {_} a. Arguments Fail_ {_}. Definition bind {A B} (m: result A) (f: A -> result B) : result B := match m with | Fail_ e => Fail_ e - | Return x => f x + | Ok x => f x end. -Definition return_ {A: Type} (x: A) : result A := Return x. +Definition return_ {A: Type} (x: A) : result A := Ok x. Definition fail_ {A: Type} (e: error) : result A := Fail_ e. Notation "x <- c1 ; c2" := (bind c1 (fun x => c2)) @@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2)) (** Monadic assert *) Definition massert (b: bool) : result unit := - if b then Return tt else Fail_ Failure. + if b then Ok tt else Fail_ Failure. (** Normalize and unwrap a successful result (used for globals) *) -Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A := - match a as r return (r = Return x -> A) with - | Return a' => fun _ => a' +Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A := + match a as r return (r = Ok x -> A) with + | Ok a' => fun _ => a' | Fail_ e => fun p' => False_rect _ (eq_ind (Fail_ e) (fun e : result A => match e with - | Return _ => False + | Ok _ => False | Fail_ e => True end) - I (Return x) p') + I (Ok x) p') end p. Notation "x %global" := (eval_result_refl x eq_refl) (at level 40). Notation "x %return" := (eval_result_refl x eq_refl) (at level 40). (* Sanity check *) -Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3. +Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3. (*** Misc *) @@ -236,7 +236,7 @@ Import Sumbool. Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) := match sumbool_of_bool (scalar_in_bounds ty x) with - | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H)) + | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H)) | right _ => Fail_ Failure end. @@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}. (*** [alloc] *) -Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x. +Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x. Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) := - Return (x, fun x => Return x). + Ok (x, fun x => Ok x). (* Trait instance *) Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {| @@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi result (T * (T -> result (array T n))) := match array_index_usize T n a i with | Fail_ e => Fail_ e - | Return x => Return (x, array_update_usize T n a i) + | Ok x => Ok (x, array_update_usize T n a i) end. (*** Slice *) @@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) : result (T * (T -> result (slice T))) := match slice_index_usize T s i with | Fail_ e => Fail_ e - | Return x => Return (x, slice_update_usize T s i) + | Ok x => Ok (x, slice_update_usize T s i) end. (*** Subslices *) @@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) : result (slice T * (slice T -> result (array T n))) := match array_to_slice T n a with | Fail_ e => Fail_ e - | Return x => Return (x, array_from_slice T n a) + | Ok x => Ok (x, array_from_slice T n a) end. Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T). @@ -657,17 +657,17 @@ end end. Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) := l <- f (alloc_vec_Vec_to_list v) ; match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with - | left H => Return (exist _ l (scalar_le_max_valid _ _ H)) + | left H => Ok (exist _ l (scalar_le_max_valid _ _ H)) | right _ => Fail_ Failure end. Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) := - alloc_vec_Vec_bind v (fun l => Return (l ++ [x])). + alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])). Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) := alloc_vec_Vec_bind v (fun l => if to_Z i result (alloc_vec_Vec T))) := match alloc_vec_Vec_index_usize v i with - | Return x => - Return (x, alloc_vec_Vec_update_usize v i) + | Ok x => + Ok (x, alloc_vec_Vec_update_usize v i) | Fail_ e => Fail_ e end. @@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index x <- inst.(core_slice_index_SliceIndex_get) i s; match x with | None => Fail_ Failure - | Some x => Return x + | Some x => Ok x end. (* [core::slice::index::Range:::get]: forward function *) -- cgit v1.2.3