summaryrefslogtreecommitdiff
path: root/tests/hol4/external
diff options
context:
space:
mode:
authorSon Ho2024-06-04 13:52:44 +0200
committerSon Ho2024-06-04 13:52:44 +0200
commit3ad6c4712fd41efec55f29af5ccc31f68a0e12cf (patch)
tree89f3b6999e1697595f1c3fbb2d9c4d8c60a69e49 /tests/hol4/external
parent2a7a18d6a07ea4967ba9ec0763e6b7d04849dc7e (diff)
parent4a31acdff7a5dfdc26bf25ad25bb8266b790f891 (diff)
Merge branch 'main' into son/loops2
Diffstat (limited to 'tests/hol4/external')
-rw-r--r--tests/hol4/external/Holmakefile5
-rw-r--r--tests/hol4/external/external_FunsScript.sml108
-rw-r--r--tests/hol4/external/external_FunsTheory.sig105
-rw-r--r--tests/hol4/external/external_OpaqueScript.sml25
-rw-r--r--tests/hol4/external/external_OpaqueTheory.sig11
-rw-r--r--tests/hol4/external/external_TypesScript.sml13
-rw-r--r--tests/hol4/external/external_TypesTheory.sig11
7 files changed, 278 insertions, 0 deletions
diff --git a/tests/hol4/external/Holmakefile b/tests/hol4/external/Holmakefile
new file mode 100644
index 00000000..3c4b8973
--- /dev/null
+++ b/tests/hol4/external/Holmakefile
@@ -0,0 +1,5 @@
+# This file was automatically generated - modify ../Holmakefile.template instead
+INCLUDES = ../../../backends/hol4
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/tests/hol4/external/external_FunsScript.sml b/tests/hol4/external/external_FunsScript.sml
new file mode 100644
index 00000000..f3692ee2
--- /dev/null
+++ b/tests/hol4/external/external_FunsScript.sml
@@ -0,0 +1,108 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: function definitions *)
+open primitivesLib divDefLib
+open external_TypesTheory external_OpaqueTheory
+
+val _ = new_theory "external_Funs"
+
+
+val swap_fwd_def = Define ‘
+ (** [external::swap]: forward function *)
+ swap_fwd (x : 't) (y : 't) (st : state) : (state # unit) result =
+ do
+ (st0, _) <- core_mem_swap_fwd x y st;
+ (st1, _) <- core_mem_swap_back0 x y st st0;
+ (st2, _) <- core_mem_swap_back1 x y st st1;
+ Return (st2, ())
+ od
+’
+
+val swap_back_def = Define ‘
+ (** [external::swap]: backward function 0 *)
+ swap_back
+ (x : 't) (y : 't) (st : state) (st0 : state) : (state # ('t # 't)) result =
+ do
+ (st1, _) <- core_mem_swap_fwd x y st;
+ (st2, x0) <- core_mem_swap_back0 x y st st1;
+ (_, y0) <- core_mem_swap_back1 x y st st2;
+ Return (st0, (x0, y0))
+ od
+’
+
+val test_new_non_zero_u32_fwd_def = Define ‘
+ (** [external::test_new_non_zero_u32]: forward function *)
+ test_new_non_zero_u32_fwd
+ (x : u32) (st : state) : (state # core_num_nonzero_non_zero_u32_t) result =
+ do
+ (st0, opt) <- core_num_nonzero_non_zero_u32_new_fwd x st;
+ core_option_option_unwrap_fwd opt st0
+ od
+’
+
+val test_vec_fwd_def = Define ‘
+ (** [external::test_vec]: forward function *)
+ test_vec_fwd : unit result =
+ let v = vec_new in do
+ _ <- vec_push_back v (int_to_u32 0);
+ Return ()
+ od
+’
+
+(** Unit test for [external::test_vec] *)
+val _ = assert_return (“test_vec_fwd”)
+
+val custom_swap_fwd_def = Define ‘
+ (** [external::custom_swap]: forward function *)
+ custom_swap_fwd (x : 't) (y : 't) (st : state) : (state # 't) result =
+ do
+ (st0, _) <- core_mem_swap_fwd x y st;
+ (st1, x0) <- core_mem_swap_back0 x y st st0;
+ (st2, _) <- core_mem_swap_back1 x y st st1;
+ Return (st2, x0)
+ od
+’
+
+val custom_swap_back_def = Define ‘
+ (** [external::custom_swap]: backward function 0 *)
+ custom_swap_back
+ (x : 't) (y : 't) (st : state) (ret : 't) (st0 : state) :
+ (state # ('t # 't)) result
+ =
+ do
+ (st1, _) <- core_mem_swap_fwd x y st;
+ (st2, _) <- core_mem_swap_back0 x y st st1;
+ (_, y0) <- core_mem_swap_back1 x y st st2;
+ Return (st0, (ret, y0))
+ od
+’
+
+val test_custom_swap_fwd_def = Define ‘
+ (** [external::test_custom_swap]: forward function *)
+ test_custom_swap_fwd
+ (x : u32) (y : u32) (st : state) : (state # unit) result =
+ do
+ (st0, _) <- custom_swap_fwd x y st;
+ Return (st0, ())
+ od
+’
+
+val test_custom_swap_back_def = Define ‘
+ (** [external::test_custom_swap]: backward function 0 *)
+ test_custom_swap_back
+ (x : u32) (y : u32) (st : state) (st0 : state) :
+ (state # (u32 # u32)) result
+ =
+ custom_swap_back x y st (int_to_u32 1) st0
+’
+
+val test_swap_non_zero_fwd_def = Define ‘
+ (** [external::test_swap_non_zero]: forward function *)
+ test_swap_non_zero_fwd (x : u32) (st : state) : (state # u32) result =
+ do
+ (st0, _) <- swap_fwd x (int_to_u32 0) st;
+ (st1, (x0, _)) <- swap_back x (int_to_u32 0) st st0;
+ if x0 = int_to_u32 0 then Fail Failure else Return (st1, x0)
+ od
+’
+
+val _ = export_theory ()
diff --git a/tests/hol4/external/external_FunsTheory.sig b/tests/hol4/external/external_FunsTheory.sig
new file mode 100644
index 00000000..490f9d06
--- /dev/null
+++ b/tests/hol4/external/external_FunsTheory.sig
@@ -0,0 +1,105 @@
+signature external_FunsTheory =
+sig
+ type thm = Thm.thm
+
+ (* Definitions *)
+ val custom_swap_back_def : thm
+ val custom_swap_fwd_def : thm
+ val swap_back_def : thm
+ val swap_fwd_def : thm
+ val test_custom_swap_back_def : thm
+ val test_custom_swap_fwd_def : thm
+ val test_new_non_zero_u32_fwd_def : thm
+ val test_swap_non_zero_fwd_def : thm
+ val test_vec_fwd_def : thm
+
+ val external_Funs_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+ [external_Opaque] Parent theory of "external_Funs"
+
+ [custom_swap_back_def] Definition
+
+ ⊢ ∀x y st ret st0.
+ custom_swap_back x y st ret st0 =
+ do
+ (st1,_) <- core_mem_swap_fwd x y st;
+ (st2,_) <- core_mem_swap_back0 x y st st1;
+ (_,y0) <- core_mem_swap_back1 x y st st2;
+ Return (st0,ret,y0)
+ od
+
+ [custom_swap_fwd_def] Definition
+
+ ⊢ ∀x y st.
+ custom_swap_fwd x y st =
+ do
+ (st0,_) <- core_mem_swap_fwd x y st;
+ (st1,x0) <- core_mem_swap_back0 x y st st0;
+ (st2,_) <- core_mem_swap_back1 x y st st1;
+ Return (st2,x0)
+ od
+
+ [swap_back_def] Definition
+
+ ⊢ ∀x y st st0.
+ swap_back x y st st0 =
+ do
+ (st1,_) <- core_mem_swap_fwd x y st;
+ (st2,x0) <- core_mem_swap_back0 x y st st1;
+ (_,y0) <- core_mem_swap_back1 x y st st2;
+ Return (st0,x0,y0)
+ od
+
+ [swap_fwd_def] Definition
+
+ ⊢ ∀x y st.
+ swap_fwd x y st =
+ do
+ (st0,_) <- core_mem_swap_fwd x y st;
+ (st1,_) <- core_mem_swap_back0 x y st st0;
+ (st2,_) <- core_mem_swap_back1 x y st st1;
+ Return (st2,())
+ od
+
+ [test_custom_swap_back_def] Definition
+
+ ⊢ ∀x y st st0.
+ test_custom_swap_back x y st st0 =
+ custom_swap_back x y st (int_to_u32 1) st0
+
+ [test_custom_swap_fwd_def] Definition
+
+ ⊢ ∀x y st.
+ test_custom_swap_fwd x y st =
+ do (st0,_) <- custom_swap_fwd x y st; Return (st0,()) od
+
+ [test_new_non_zero_u32_fwd_def] Definition
+
+ ⊢ ∀x st.
+ test_new_non_zero_u32_fwd x st =
+ do
+ (st0,opt) <- core_num_nonzero_non_zero_u32_new_fwd x st;
+ core_option_option_unwrap_fwd opt st0
+ od
+
+ [test_swap_non_zero_fwd_def] Definition
+
+ ⊢ ∀x st.
+ test_swap_non_zero_fwd x st =
+ do
+ (st0,_) <- swap_fwd x (int_to_u32 0) st;
+ (st1,x0,_) <- swap_back x (int_to_u32 0) st st0;
+ if x0 = int_to_u32 0 then Fail Failure else Return (st1,x0)
+ od
+
+ [test_vec_fwd_def] Definition
+
+ ⊢ test_vec_fwd =
+ (let
+ v = vec_new
+ in
+ monad_ignore_bind (vec_push_back v (int_to_u32 0)) (Return ()))
+
+
+*)
+end
diff --git a/tests/hol4/external/external_OpaqueScript.sml b/tests/hol4/external/external_OpaqueScript.sml
new file mode 100644
index 00000000..b5a6d91d
--- /dev/null
+++ b/tests/hol4/external/external_OpaqueScript.sml
@@ -0,0 +1,25 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external function declarations *)
+open primitivesLib divDefLib
+open external_TypesTheory
+
+val _ = new_theory "external_Opaque"
+
+
+(** [core::mem::swap]: forward function *)val _ = new_constant ("core_mem_swap_fwd",
+ “:'t -> 't -> state -> (state # unit) result”)
+
+(** [core::mem::swap]: backward function 0 *)val _ = new_constant ("core_mem_swap_back0",
+ “:'t -> 't -> state -> state -> (state # 't) result”)
+
+(** [core::mem::swap]: backward function 1 *)val _ = new_constant ("core_mem_swap_back1",
+ “:'t -> 't -> state -> state -> (state # 't) result”)
+
+(** [core::num::nonzero::NonZeroU32::{14}::new]: forward function *)val _ = new_constant ("core_num_nonzero_non_zero_u32_new_fwd",
+ “:u32 -> state -> (state # core_num_nonzero_non_zero_u32_t option)
+ result”)
+
+(** [core::option::Option::{0}::unwrap]: forward function *)val _ = new_constant ("core_option_option_unwrap_fwd",
+ “:'t option -> state -> (state # 't) result”)
+
+val _ = export_theory ()
diff --git a/tests/hol4/external/external_OpaqueTheory.sig b/tests/hol4/external/external_OpaqueTheory.sig
new file mode 100644
index 00000000..7cd7a08c
--- /dev/null
+++ b/tests/hol4/external/external_OpaqueTheory.sig
@@ -0,0 +1,11 @@
+signature external_OpaqueTheory =
+sig
+ type thm = Thm.thm
+
+ val external_Opaque_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+ [external_Types] Parent theory of "external_Opaque"
+
+
+*)
+end
diff --git a/tests/hol4/external/external_TypesScript.sml b/tests/hol4/external/external_TypesScript.sml
new file mode 100644
index 00000000..d290c3f6
--- /dev/null
+++ b/tests/hol4/external/external_TypesScript.sml
@@ -0,0 +1,13 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: type definitions *)
+open primitivesLib divDefLib
+
+val _ = new_theory "external_Types"
+
+
+val _ = new_type ("core_num_nonzero_non_zero_u32_t", 0)
+
+(** The state type used in the state-error monad *)
+val _ = new_type ("state", 0)
+
+val _ = export_theory ()
diff --git a/tests/hol4/external/external_TypesTheory.sig b/tests/hol4/external/external_TypesTheory.sig
new file mode 100644
index 00000000..17e2e8e3
--- /dev/null
+++ b/tests/hol4/external/external_TypesTheory.sig
@@ -0,0 +1,11 @@
+signature external_TypesTheory =
+sig
+ type thm = Thm.thm
+
+ val external_Types_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+ [divDef] Parent theory of "external_Types"
+
+
+*)
+end