From fa6dcd3ebbdc7a508157ff2a12f91e70d2012a86 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 15 Nov 2022 15:25:47 +0100 Subject: Change the name of the generated Coq modules --- tests/coq/misc/External_Funs.v | 114 ++++++++++++++++++++++++++++++++++++++ tests/coq/misc/External_Opaque.v | 36 ++++++++++++ tests/coq/misc/External_Types.v | 15 +++++ tests/coq/misc/External__Funs.v | 114 -------------------------------------- tests/coq/misc/External__Opaque.v | 36 ------------ tests/coq/misc/External__Types.v | 15 ----- 6 files changed, 165 insertions(+), 165 deletions(-) create mode 100644 tests/coq/misc/External_Funs.v create mode 100644 tests/coq/misc/External_Opaque.v create mode 100644 tests/coq/misc/External_Types.v delete mode 100644 tests/coq/misc/External__Funs.v delete mode 100644 tests/coq/misc/External__Opaque.v delete mode 100644 tests/coq/misc/External__Types.v (limited to 'tests/coq/misc') diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v new file mode 100644 index 00000000..3ddc1cf3 --- /dev/null +++ b/tests/coq/misc/External_Funs.v @@ -0,0 +1,114 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Require Export External_Types. +Import External_Types. +Require Export External_Opaque. +Import External_Opaque. +Module External_Funs. + +(** [external::swap] *) +Definition swap_fwd + (T : Type) (x : T) (y : T) (st : state) : result (state * unit) := + p <- core_mem_swap_fwd T x y st; + let (st0, _) := p in + p0 <- core_mem_swap_back0 T x y st st0; + let (st1, _) := p0 in + p1 <- core_mem_swap_back1 T x y st st1; + let (st2, _) := p1 in + Return (st2, tt) +. + +(** [external::swap] *) +Definition swap_back + (T : Type) (x : T) (y : T) (st : state) (st0 : state) : + result (state * (T * T)) + := + p <- core_mem_swap_fwd T x y st; + let (st1, _) := p in + p0 <- core_mem_swap_back0 T x y st st1; + let (st2, x0) := p0 in + p1 <- core_mem_swap_back1 T x y st st2; + let (_, y0) := p1 in + Return (st0, (x0, y0)) +. + +(** [external::test_new_non_zero_u32] *) +Definition test_new_non_zero_u32_fwd + (x : u32) (st : state) : result (state * Core_num_nonzero_non_zero_u32_t) := + p <- core_num_nonzero_non_zero_u32_new_fwd x st; + let (st0, opt) := p in + p0 <- core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0; + let (st1, nzu) := p0 in + Return (st1, nzu) +. + +(** [external::test_vec] *) +Definition test_vec_fwd : result unit := + let v := vec_new u32 in + v0 <- vec_push_back u32 v (0%u32); + let _ := v0 in + Return tt +. + +(** Unit test for [external::test_vec] *) +Check (test_vec_fwd )%return. + +(** [external::custom_swap] *) +Definition custom_swap_fwd + (T : Type) (x : T) (y : T) (st : state) : result (state * T) := + p <- core_mem_swap_fwd T x y st; + let (st0, _) := p in + p0 <- core_mem_swap_back0 T x y st st0; + let (st1, x0) := p0 in + p1 <- core_mem_swap_back1 T x y st st1; + let (st2, _) := p1 in + Return (st2, x0) +. + +(** [external::custom_swap] *) +Definition custom_swap_back + (T : Type) (x : T) (y : T) (st : state) (ret : T) (st0 : state) : + result (state * (T * T)) + := + p <- core_mem_swap_fwd T x y st; + let (st1, _) := p in + p0 <- core_mem_swap_back0 T x y st st1; + let (st2, _) := p0 in + p1 <- core_mem_swap_back1 T x y st st2; + let (_, y0) := p1 in + Return (st0, (ret, y0)) +. + +(** [external::test_custom_swap] *) +Definition test_custom_swap_fwd + (x : u32) (y : u32) (st : state) : result (state * unit) := + p <- custom_swap_fwd u32 x y st; let (st0, _) := p in Return (st0, tt) +. + +(** [external::test_custom_swap] *) +Definition test_custom_swap_back + (x : u32) (y : u32) (st : state) (st0 : state) : + result (state * (u32 * u32)) + := + p <- custom_swap_back u32 x y st (1%u32) st0; + let (st1, p0) := p in + let (x0, y0) := p0 in + Return (st1, (x0, y0)) +. + +(** [external::test_swap_non_zero] *) +Definition test_swap_non_zero_fwd + (x : u32) (st : state) : result (state * u32) := + p <- swap_fwd u32 x (0%u32) st; + let (st0, _) := p in + p0 <- swap_back u32 x (0%u32) st st0; + let (st1, p1) := p0 in + let (x0, _) := p1 in + if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0) +. + +End External_Funs . diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v new file mode 100644 index 00000000..d60251e0 --- /dev/null +++ b/tests/coq/misc/External_Opaque.v @@ -0,0 +1,36 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: opaque function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Require Export External_Types. +Import External_Types. +Module External_Opaque. + +(** [core::mem::swap] *) +Axiom core_mem_swap_fwd : + forall(T : Type), T -> T -> state -> result (state * unit) +. + +(** [core::mem::swap] *) +Axiom core_mem_swap_back0 : + forall(T : Type), T -> T -> state -> state -> result (state * T) +. + +(** [core::mem::swap] *) +Axiom core_mem_swap_back1 : + forall(T : Type), T -> T -> state -> state -> result (state * T) +. + +(** [core::num::nonzero::NonZeroU32::{14}::new] *) +Axiom core_num_nonzero_non_zero_u32_new_fwd + : u32 -> state -> result (state * (option Core_num_nonzero_non_zero_u32_t)) +. + +(** [core::option::Option::{0}::unwrap] *) +Axiom core_option_option_unwrap_fwd : + forall(T : Type), option T -> state -> result (state * T) +. + +End External_Opaque . diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v new file mode 100644 index 00000000..cec5b88e --- /dev/null +++ b/tests/coq/misc/External_Types.v @@ -0,0 +1,15 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: type definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Module External_Types. + +(** [core::num::nonzero::NonZeroU32] *) +Axiom Core_num_nonzero_non_zero_u32_t : Type. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End External_Types . diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v deleted file mode 100644 index e7020040..00000000 --- a/tests/coq/misc/External__Funs.v +++ /dev/null @@ -1,114 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [external]: function definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Local Open Scope Primitives_scope. -Require Export External__Types. -Import External__Types. -Require Export External__Opaque. -Import External__Opaque. -Module External__Funs. - -(** [external::swap] *) -Definition swap_fwd - (T : Type) (x : T) (y : T) (st : state) : result (state * unit) := - p <- core_mem_swap_fwd T x y st; - let (st0, _) := p in - p0 <- core_mem_swap_back0 T x y st st0; - let (st1, _) := p0 in - p1 <- core_mem_swap_back1 T x y st st1; - let (st2, _) := p1 in - Return (st2, tt) -. - -(** [external::swap] *) -Definition swap_back - (T : Type) (x : T) (y : T) (st : state) (st0 : state) : - result (state * (T * T)) - := - p <- core_mem_swap_fwd T x y st; - let (st1, _) := p in - p0 <- core_mem_swap_back0 T x y st st1; - let (st2, x0) := p0 in - p1 <- core_mem_swap_back1 T x y st st2; - let (_, y0) := p1 in - Return (st0, (x0, y0)) -. - -(** [external::test_new_non_zero_u32] *) -Definition test_new_non_zero_u32_fwd - (x : u32) (st : state) : result (state * Core_num_nonzero_non_zero_u32_t) := - p <- core_num_nonzero_non_zero_u32_new_fwd x st; - let (st0, opt) := p in - p0 <- core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0; - let (st1, nzu) := p0 in - Return (st1, nzu) -. - -(** [external::test_vec] *) -Definition test_vec_fwd : result unit := - let v := vec_new u32 in - v0 <- vec_push_back u32 v (0%u32); - let _ := v0 in - Return tt -. - -(** Unit test for [external::test_vec] *) -Check (test_vec_fwd )%return. - -(** [external::custom_swap] *) -Definition custom_swap_fwd - (T : Type) (x : T) (y : T) (st : state) : result (state * T) := - p <- core_mem_swap_fwd T x y st; - let (st0, _) := p in - p0 <- core_mem_swap_back0 T x y st st0; - let (st1, x0) := p0 in - p1 <- core_mem_swap_back1 T x y st st1; - let (st2, _) := p1 in - Return (st2, x0) -. - -(** [external::custom_swap] *) -Definition custom_swap_back - (T : Type) (x : T) (y : T) (st : state) (ret : T) (st0 : state) : - result (state * (T * T)) - := - p <- core_mem_swap_fwd T x y st; - let (st1, _) := p in - p0 <- core_mem_swap_back0 T x y st st1; - let (st2, _) := p0 in - p1 <- core_mem_swap_back1 T x y st st2; - let (_, y0) := p1 in - Return (st0, (ret, y0)) -. - -(** [external::test_custom_swap] *) -Definition test_custom_swap_fwd - (x : u32) (y : u32) (st : state) : result (state * unit) := - p <- custom_swap_fwd u32 x y st; let (st0, _) := p in Return (st0, tt) -. - -(** [external::test_custom_swap] *) -Definition test_custom_swap_back - (x : u32) (y : u32) (st : state) (st0 : state) : - result (state * (u32 * u32)) - := - p <- custom_swap_back u32 x y st (1%u32) st0; - let (st1, p0) := p in - let (x0, y0) := p0 in - Return (st1, (x0, y0)) -. - -(** [external::test_swap_non_zero] *) -Definition test_swap_non_zero_fwd - (x : u32) (st : state) : result (state * u32) := - p <- swap_fwd u32 x (0%u32) st; - let (st0, _) := p in - p0 <- swap_back u32 x (0%u32) st st0; - let (st1, p1) := p0 in - let (x0, _) := p1 in - if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0) -. - -End External__Funs . diff --git a/tests/coq/misc/External__Opaque.v b/tests/coq/misc/External__Opaque.v deleted file mode 100644 index 93652450..00000000 --- a/tests/coq/misc/External__Opaque.v +++ /dev/null @@ -1,36 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [external]: opaque function definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Local Open Scope Primitives_scope. -Require Export External__Types. -Import External__Types. -Module External__Opaque. - -(** [core::mem::swap] *) -Axiom core_mem_swap_fwd : - forall(T : Type), T -> T -> state -> result (state * unit) -. - -(** [core::mem::swap] *) -Axiom core_mem_swap_back0 : - forall(T : Type), T -> T -> state -> state -> result (state * T) -. - -(** [core::mem::swap] *) -Axiom core_mem_swap_back1 : - forall(T : Type), T -> T -> state -> state -> result (state * T) -. - -(** [core::num::nonzero::NonZeroU32::{14}::new] *) -Axiom core_num_nonzero_non_zero_u32_new_fwd - : u32 -> state -> result (state * (option Core_num_nonzero_non_zero_u32_t)) -. - -(** [core::option::Option::{0}::unwrap] *) -Axiom core_option_option_unwrap_fwd : - forall(T : Type), option T -> state -> result (state * T) -. - -End External__Opaque . diff --git a/tests/coq/misc/External__Types.v b/tests/coq/misc/External__Types.v deleted file mode 100644 index f4f74272..00000000 --- a/tests/coq/misc/External__Types.v +++ /dev/null @@ -1,15 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [external]: type definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Local Open Scope Primitives_scope. -Module External__Types. - -(** [core::num::nonzero::NonZeroU32] *) -Axiom Core_num_nonzero_non_zero_u32_t : Type. - -(** The state type used in the state-error monad *) -Axiom state : Type. - -End External__Types . -- cgit v1.2.3