summaryrefslogtreecommitdiff
path: root/tests/hol4/misc-external
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hol4/misc-external')
-rw-r--r--tests/hol4/misc-external/Holmakefile5
-rw-r--r--tests/hol4/misc-external/external_FunsScript.sml108
-rw-r--r--tests/hol4/misc-external/external_FunsTheory.sig105
-rw-r--r--tests/hol4/misc-external/external_OpaqueScript.sml25
-rw-r--r--tests/hol4/misc-external/external_OpaqueTheory.sig11
-rw-r--r--tests/hol4/misc-external/external_TypesScript.sml13
-rw-r--r--tests/hol4/misc-external/external_TypesTheory.sig11
7 files changed, 0 insertions, 278 deletions
diff --git a/tests/hol4/misc-external/Holmakefile b/tests/hol4/misc-external/Holmakefile
deleted file mode 100644
index 3c4b8973..00000000
--- a/tests/hol4/misc-external/Holmakefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# This file was automatically generated - modify ../Holmakefile.template instead
-INCLUDES = ../../../backends/hol4
-
-all: $(DEFAULT_TARGETS)
-.PHONY: all
diff --git a/tests/hol4/misc-external/external_FunsScript.sml b/tests/hol4/misc-external/external_FunsScript.sml
deleted file mode 100644
index f3692ee2..00000000
--- a/tests/hol4/misc-external/external_FunsScript.sml
+++ /dev/null
@@ -1,108 +0,0 @@
-(** 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/misc-external/external_FunsTheory.sig b/tests/hol4/misc-external/external_FunsTheory.sig
deleted file mode 100644
index 490f9d06..00000000
--- a/tests/hol4/misc-external/external_FunsTheory.sig
+++ /dev/null
@@ -1,105 +0,0 @@
-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/misc-external/external_OpaqueScript.sml b/tests/hol4/misc-external/external_OpaqueScript.sml
deleted file mode 100644
index b5a6d91d..00000000
--- a/tests/hol4/misc-external/external_OpaqueScript.sml
+++ /dev/null
@@ -1,25 +0,0 @@
-(** 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/misc-external/external_OpaqueTheory.sig b/tests/hol4/misc-external/external_OpaqueTheory.sig
deleted file mode 100644
index 7cd7a08c..00000000
--- a/tests/hol4/misc-external/external_OpaqueTheory.sig
+++ /dev/null
@@ -1,11 +0,0 @@
-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/misc-external/external_TypesScript.sml b/tests/hol4/misc-external/external_TypesScript.sml
deleted file mode 100644
index d290c3f6..00000000
--- a/tests/hol4/misc-external/external_TypesScript.sml
+++ /dev/null
@@ -1,13 +0,0 @@
-(** 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/misc-external/external_TypesTheory.sig b/tests/hol4/misc-external/external_TypesTheory.sig
deleted file mode 100644
index 17e2e8e3..00000000
--- a/tests/hol4/misc-external/external_TypesTheory.sig
+++ /dev/null
@@ -1,11 +0,0 @@
-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
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 21:44:50 +0000