summaryrefslogtreecommitdiff
path: root/tests/hol4/misc-loops
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hol4/misc-loops')
-rw-r--r--tests/hol4/misc-loops/Holmakefile5
-rw-r--r--tests/hol4/misc-loops/loops_FunsScript.sml755
-rw-r--r--tests/hol4/misc-loops/loops_FunsTheory.sig731
-rw-r--r--tests/hol4/misc-loops/loops_TypesScript.sml13
-rw-r--r--tests/hol4/misc-loops/loops_TypesTheory.sig94
5 files changed, 0 insertions, 1598 deletions
diff --git a/tests/hol4/misc-loops/Holmakefile b/tests/hol4/misc-loops/Holmakefile
deleted file mode 100644
index 3c4b8973..00000000
--- a/tests/hol4/misc-loops/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-loops/loops_FunsScript.sml b/tests/hol4/misc-loops/loops_FunsScript.sml
deleted file mode 100644
index 65cf77d4..00000000
--- a/tests/hol4/misc-loops/loops_FunsScript.sml
+++ /dev/null
@@ -1,755 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [loops]: function definitions *)
-open primitivesLib divDefLib
-open loops_TypesTheory
-
-val _ = new_theory "loops_Funs"
-
-
-val [sum_loop_fwd_def] = DefineDiv ‘
- (** [loops::sum]: loop 0: forward function *)
- sum_loop_fwd (max : u32) (i : u32) (s : u32) : u32 result =
- if u32_lt i max
- then (
- do
- s0 <- u32_add s i;
- i0 <- u32_add i (int_to_u32 1);
- sum_loop_fwd max i0 s0
- od)
- else u32_mul s (int_to_u32 2)
-’
-
-val sum_fwd_def = Define ‘
- (** [loops::sum]: forward function *)
- sum_fwd (max : u32) : u32 result =
- sum_loop_fwd max (int_to_u32 0) (int_to_u32 0)
-’
-
-val [sum_with_mut_borrows_loop_fwd_def] = DefineDiv ‘
- (** [loops::sum_with_mut_borrows]: loop 0: forward function *)
- sum_with_mut_borrows_loop_fwd
- (max : u32) (mi : u32) (ms : u32) : u32 result =
- if u32_lt mi max
- then (
- do
- ms0 <- u32_add ms mi;
- mi0 <- u32_add mi (int_to_u32 1);
- sum_with_mut_borrows_loop_fwd max mi0 ms0
- od)
- else u32_mul ms (int_to_u32 2)
-’
-
-val sum_with_mut_borrows_fwd_def = Define ‘
- (** [loops::sum_with_mut_borrows]: forward function *)
- sum_with_mut_borrows_fwd (max : u32) : u32 result =
- sum_with_mut_borrows_loop_fwd max (int_to_u32 0) (int_to_u32 0)
-’
-
-val [sum_with_shared_borrows_loop_fwd_def] = DefineDiv ‘
- (** [loops::sum_with_shared_borrows]: loop 0: forward function *)
- sum_with_shared_borrows_loop_fwd
- (max : u32) (i : u32) (s : u32) : u32 result =
- if u32_lt i max
- then (
- do
- i0 <- u32_add i (int_to_u32 1);
- s0 <- u32_add s i0;
- sum_with_shared_borrows_loop_fwd max i0 s0
- od)
- else u32_mul s (int_to_u32 2)
-’
-
-val sum_with_shared_borrows_fwd_def = Define ‘
- (** [loops::sum_with_shared_borrows]: forward function *)
- sum_with_shared_borrows_fwd (max : u32) : u32 result =
- sum_with_shared_borrows_loop_fwd max (int_to_u32 0) (int_to_u32 0)
-’
-
-val [clear_loop_fwd_back_def] = DefineDiv ‘
- (** [loops::clear]: loop 0: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) *)
- clear_loop_fwd_back (v : u32 vec) (i : usize) : u32 vec result =
- let i0 = vec_len v in
- if usize_lt i i0
- then (
- do
- i1 <- usize_add i (int_to_usize 1);
- v0 <- vec_index_mut_back v i (int_to_u32 0);
- clear_loop_fwd_back v0 i1
- od)
- else Return v
-’
-
-val clear_fwd_back_def = Define ‘
- (** [loops::clear]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) *)
- clear_fwd_back (v : u32 vec) : u32 vec result =
- clear_loop_fwd_back v (int_to_usize 0)
-’
-
-val [list_mem_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_mem]: loop 0: forward function *)
- list_mem_loop_fwd (x : u32) (ls : u32 list_t) : bool result =
- (case ls of
- | ListCons y tl => if y = x then Return T else list_mem_loop_fwd x tl
- | ListNil => Return F)
-’
-
-val list_mem_fwd_def = Define ‘
- (** [loops::list_mem]: forward function *)
- list_mem_fwd (x : u32) (ls : u32 list_t) : bool result =
- list_mem_loop_fwd x ls
-’
-
-val [list_nth_mut_loop_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_mut_loop]: loop 0: forward function *)
- list_nth_mut_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result =
- (case ls of
- | ListCons x tl =>
- if i = int_to_u32 0
- then Return x
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_loop_loop_fwd tl i0
- od)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_fwd_def = Define ‘
- (** [loops::list_nth_mut_loop]: forward function *)
- list_nth_mut_loop_fwd (ls : 't list_t) (i : u32) : 't result =
- list_nth_mut_loop_loop_fwd ls i
-’
-
-val [list_nth_mut_loop_loop_back_def] = DefineDiv ‘
- (** [loops::list_nth_mut_loop]: loop 0: backward function 0 *)
- list_nth_mut_loop_loop_back
- (ls : 't list_t) (i : u32) (ret : 't) : 't list_t result =
- (case ls of
- | ListCons x tl =>
- if i = int_to_u32 0
- then Return (ListCons ret tl)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl0 <- list_nth_mut_loop_loop_back tl i0 ret;
- Return (ListCons x tl0)
- od)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_back_def = Define ‘
- (** [loops::list_nth_mut_loop]: backward function 0 *)
- list_nth_mut_loop_back
- (ls : 't list_t) (i : u32) (ret : 't) : 't list_t result =
- list_nth_mut_loop_loop_back ls i ret
-’
-
-val [list_nth_shared_loop_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_shared_loop]: loop 0: forward function *)
- list_nth_shared_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result =
- (case ls of
- | ListCons x tl =>
- if i = int_to_u32 0
- then Return x
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_loop_loop_fwd tl i0
- od)
- | ListNil => Fail Failure)
-’
-
-val list_nth_shared_loop_fwd_def = Define ‘
- (** [loops::list_nth_shared_loop]: forward function *)
- list_nth_shared_loop_fwd (ls : 't list_t) (i : u32) : 't result =
- list_nth_shared_loop_loop_fwd ls i
-’
-
-val [get_elem_mut_loop_fwd_def] = DefineDiv ‘
- (** [loops::get_elem_mut]: loop 0: forward function *)
- get_elem_mut_loop_fwd (x : usize) (ls : usize list_t) : usize result =
- (case ls of
- | ListCons y tl => if y = x then Return y else get_elem_mut_loop_fwd x tl
- | ListNil => Fail Failure)
-’
-
-val get_elem_mut_fwd_def = Define ‘
- (** [loops::get_elem_mut]: forward function *)
- get_elem_mut_fwd (slots : usize list_t vec) (x : usize) : usize result =
- do
- l <- vec_index_mut_fwd slots (int_to_usize 0);
- get_elem_mut_loop_fwd x l
- od
-’
-
-val [get_elem_mut_loop_back_def] = DefineDiv ‘
- (** [loops::get_elem_mut]: loop 0: backward function 0 *)
- get_elem_mut_loop_back
- (x : usize) (ls : usize list_t) (ret : usize) : usize list_t result =
- (case ls of
- | ListCons y tl =>
- if y = x
- then Return (ListCons ret tl)
- else (
- do
- tl0 <- get_elem_mut_loop_back x tl ret;
- Return (ListCons y tl0)
- od)
- | ListNil => Fail Failure)
-’
-
-val get_elem_mut_back_def = Define ‘
- (** [loops::get_elem_mut]: backward function 0 *)
- get_elem_mut_back
- (slots : usize list_t vec) (x : usize) (ret : usize) :
- usize list_t vec result
- =
- do
- l <- vec_index_mut_fwd slots (int_to_usize 0);
- l0 <- get_elem_mut_loop_back x l ret;
- vec_index_mut_back slots (int_to_usize 0) l0
- od
-’
-
-val [get_elem_shared_loop_fwd_def] = DefineDiv ‘
- (** [loops::get_elem_shared]: loop 0: forward function *)
- get_elem_shared_loop_fwd (x : usize) (ls : usize list_t) : usize result =
- (case ls of
- | ListCons y tl =>
- if y = x then Return y else get_elem_shared_loop_fwd x tl
- | ListNil => Fail Failure)
-’
-
-val get_elem_shared_fwd_def = Define ‘
- (** [loops::get_elem_shared]: forward function *)
- get_elem_shared_fwd (slots : usize list_t vec) (x : usize) : usize result =
- do
- l <- vec_index_fwd slots (int_to_usize 0);
- get_elem_shared_loop_fwd x l
- od
-’
-
-val id_mut_fwd_def = Define ‘
- (** [loops::id_mut]: forward function *)
- id_mut_fwd (ls : 't list_t) : 't list_t result =
- Return ls
-’
-
-val id_mut_back_def = Define ‘
- (** [loops::id_mut]: backward function 0 *)
- id_mut_back (ls : 't list_t) (ret : 't list_t) : 't list_t result =
- Return ret
-’
-
-val id_shared_fwd_def = Define ‘
- (** [loops::id_shared]: forward function *)
- id_shared_fwd (ls : 't list_t) : 't list_t result =
- Return ls
-’
-
-val [list_nth_mut_loop_with_id_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *)
- list_nth_mut_loop_with_id_loop_fwd (i : u32) (ls : 't list_t) : 't result =
- (case ls of
- | ListCons x tl =>
- if i = int_to_u32 0
- then Return x
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_loop_with_id_loop_fwd i0 tl
- od)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_with_id_fwd_def = Define ‘
- (** [loops::list_nth_mut_loop_with_id]: forward function *)
- list_nth_mut_loop_with_id_fwd (ls : 't list_t) (i : u32) : 't result =
- do
- ls0 <- id_mut_fwd ls;
- list_nth_mut_loop_with_id_loop_fwd i ls0
- od
-’
-
-val [list_nth_mut_loop_with_id_loop_back_def] = DefineDiv ‘
- (** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *)
- list_nth_mut_loop_with_id_loop_back
- (i : u32) (ls : 't list_t) (ret : 't) : 't list_t result =
- (case ls of
- | ListCons x tl =>
- if i = int_to_u32 0
- then Return (ListCons ret tl)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl0 <- list_nth_mut_loop_with_id_loop_back i0 tl ret;
- Return (ListCons x tl0)
- od)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_with_id_back_def = Define ‘
- (** [loops::list_nth_mut_loop_with_id]: backward function 0 *)
- list_nth_mut_loop_with_id_back
- (ls : 't list_t) (i : u32) (ret : 't) : 't list_t result =
- do
- ls0 <- id_mut_fwd ls;
- l <- list_nth_mut_loop_with_id_loop_back i ls0 ret;
- id_mut_back ls l
- od
-’
-
-val [list_nth_shared_loop_with_id_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *)
- list_nth_shared_loop_with_id_loop_fwd
- (i : u32) (ls : 't list_t) : 't result =
- (case ls of
- | ListCons x tl =>
- if i = int_to_u32 0
- then Return x
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_loop_with_id_loop_fwd i0 tl
- od)
- | ListNil => Fail Failure)
-’
-
-val list_nth_shared_loop_with_id_fwd_def = Define ‘
- (** [loops::list_nth_shared_loop_with_id]: forward function *)
- list_nth_shared_loop_with_id_fwd (ls : 't list_t) (i : u32) : 't result =
- do
- ls0 <- id_shared_fwd ls;
- list_nth_shared_loop_with_id_loop_fwd i ls0
- od
-’
-
-val [list_nth_mut_loop_pair_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_mut_loop_pair]: loop 0: forward function *)
- list_nth_mut_loop_pair_loop_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (x0, x1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_loop_pair_loop_fwd tl0 tl1 i0
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_pair_fwd_def = Define ‘
- (** [loops::list_nth_mut_loop_pair]: forward function *)
- list_nth_mut_loop_pair_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- list_nth_mut_loop_pair_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_loop_pair_loop_back'a_def] = DefineDiv ‘
- (** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *)
- list_nth_mut_loop_pair_loop_back'a
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (ListCons ret tl0)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl00 <- list_nth_mut_loop_pair_loop_back'a tl0 tl1 i0 ret;
- Return (ListCons x0 tl00)
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_pair_back'a_def = Define ‘
- (** [loops::list_nth_mut_loop_pair]: backward function 0 *)
- list_nth_mut_loop_pair_back'a
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret
-’
-
-val [list_nth_mut_loop_pair_loop_back'b_def] = DefineDiv ‘
- (** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 *)
- list_nth_mut_loop_pair_loop_back'b
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (ListCons ret tl1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl10 <- list_nth_mut_loop_pair_loop_back'b tl0 tl1 i0 ret;
- Return (ListCons x1 tl10)
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_pair_back'b_def = Define ‘
- (** [loops::list_nth_mut_loop_pair]: backward function 1 *)
- list_nth_mut_loop_pair_back'b
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret
-’
-
-val [list_nth_shared_loop_pair_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_shared_loop_pair]: loop 0: forward function *)
- list_nth_shared_loop_pair_loop_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (x0, x1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_loop_pair_loop_fwd tl0 tl1 i0
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_shared_loop_pair_fwd_def = Define ‘
- (** [loops::list_nth_shared_loop_pair]: forward function *)
- list_nth_shared_loop_pair_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- list_nth_shared_loop_pair_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *)
- list_nth_mut_loop_pair_merge_loop_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (x0, x1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_loop_pair_merge_loop_fwd tl0 tl1 i0
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_pair_merge_fwd_def = Define ‘
- (** [loops::list_nth_mut_loop_pair_merge]: forward function *)
- list_nth_mut_loop_pair_merge_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_loop_pair_merge_loop_back_def] = DefineDiv ‘
- (** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *)
- list_nth_mut_loop_pair_merge_loop_back
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : ('t # 't)) :
- ('t list_t # 't list_t) result
- =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then let (t, t0) = ret in Return (ListCons t tl0, ListCons t0 tl1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- (tl00, tl10) <-
- list_nth_mut_loop_pair_merge_loop_back tl0 tl1 i0 ret;
- Return (ListCons x0 tl00, ListCons x1 tl10)
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_pair_merge_back_def = Define ‘
- (** [loops::list_nth_mut_loop_pair_merge]: backward function 0 *)
- list_nth_mut_loop_pair_merge_back
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : ('t # 't)) :
- ('t list_t # 't list_t) result
- =
- list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret
-’
-
-val [list_nth_shared_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *)
- list_nth_shared_loop_pair_merge_loop_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (x0, x1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_loop_pair_merge_loop_fwd tl0 tl1 i0
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_shared_loop_pair_merge_fwd_def = Define ‘
- (** [loops::list_nth_shared_loop_pair_merge]: forward function *)
- list_nth_shared_loop_pair_merge_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_shared_loop_pair_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *)
- list_nth_mut_shared_loop_pair_loop_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (x0, x1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_shared_loop_pair_loop_fwd tl0 tl1 i0
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_shared_loop_pair_fwd_def = Define ‘
- (** [loops::list_nth_mut_shared_loop_pair]: forward function *)
- list_nth_mut_shared_loop_pair_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_shared_loop_pair_loop_back_def] = DefineDiv ‘
- (** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *)
- list_nth_mut_shared_loop_pair_loop_back
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (ListCons ret tl0)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl00 <- list_nth_mut_shared_loop_pair_loop_back tl0 tl1 i0 ret;
- Return (ListCons x0 tl00)
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_shared_loop_pair_back_def = Define ‘
- (** [loops::list_nth_mut_shared_loop_pair]: backward function 0 *)
- list_nth_mut_shared_loop_pair_back
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret
-’
-
-val [list_nth_mut_shared_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *)
- list_nth_mut_shared_loop_pair_merge_loop_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (x0, x1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_shared_loop_pair_merge_loop_fwd tl0 tl1 i0
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_shared_loop_pair_merge_fwd_def = Define ‘
- (** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *)
- list_nth_mut_shared_loop_pair_merge_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_shared_loop_pair_merge_loop_back_def] = DefineDiv ‘
- (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *)
- list_nth_mut_shared_loop_pair_merge_loop_back
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (ListCons ret tl0)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl00 <- list_nth_mut_shared_loop_pair_merge_loop_back tl0 tl1 i0 ret;
- Return (ListCons x0 tl00)
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_mut_shared_loop_pair_merge_back_def = Define ‘
- (** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 *)
- list_nth_mut_shared_loop_pair_merge_back
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret
-’
-
-val [list_nth_shared_mut_loop_pair_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *)
- list_nth_shared_mut_loop_pair_loop_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (x0, x1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_mut_loop_pair_loop_fwd tl0 tl1 i0
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_shared_mut_loop_pair_fwd_def = Define ‘
- (** [loops::list_nth_shared_mut_loop_pair]: forward function *)
- list_nth_shared_mut_loop_pair_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_shared_mut_loop_pair_loop_back_def] = DefineDiv ‘
- (** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *)
- list_nth_shared_mut_loop_pair_loop_back
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (ListCons ret tl1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl10 <- list_nth_shared_mut_loop_pair_loop_back tl0 tl1 i0 ret;
- Return (ListCons x1 tl10)
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_shared_mut_loop_pair_back_def = Define ‘
- (** [loops::list_nth_shared_mut_loop_pair]: backward function 1 *)
- list_nth_shared_mut_loop_pair_back
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret
-’
-
-val [list_nth_shared_mut_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
- (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *)
- list_nth_shared_mut_loop_pair_merge_loop_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (x0, x1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_mut_loop_pair_merge_loop_fwd tl0 tl1 i0
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_shared_mut_loop_pair_merge_fwd_def = Define ‘
- (** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *)
- list_nth_shared_mut_loop_pair_merge_fwd
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
- list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_shared_mut_loop_pair_merge_loop_back_def] = DefineDiv ‘
- (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *)
- list_nth_shared_mut_loop_pair_merge_loop_back
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- (case ls0 of
- | ListCons x0 tl0 =>
- (case ls1 of
- | ListCons x1 tl1 =>
- if i = int_to_u32 0
- then Return (ListCons ret tl1)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl10 <- list_nth_shared_mut_loop_pair_merge_loop_back tl0 tl1 i0 ret;
- Return (ListCons x1 tl10)
- od)
- | ListNil => Fail Failure)
- | ListNil => Fail Failure)
-’
-
-val list_nth_shared_mut_loop_pair_merge_back_def = Define ‘
- (** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 *)
- list_nth_shared_mut_loop_pair_merge_back
- (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
- 't list_t result
- =
- list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret
-’
-
-val _ = export_theory ()
diff --git a/tests/hol4/misc-loops/loops_FunsTheory.sig b/tests/hol4/misc-loops/loops_FunsTheory.sig
deleted file mode 100644
index 63fe56c9..00000000
--- a/tests/hol4/misc-loops/loops_FunsTheory.sig
+++ /dev/null
@@ -1,731 +0,0 @@
-signature loops_FunsTheory =
-sig
- type thm = Thm.thm
-
- (* Definitions *)
- val clear_fwd_back_def : thm
- val clear_loop_fwd_back_def : thm
- val get_elem_mut_back_def : thm
- val get_elem_mut_fwd_def : thm
- val get_elem_mut_loop_back_def : thm
- val get_elem_mut_loop_fwd_def : thm
- val get_elem_shared_fwd_def : thm
- val get_elem_shared_loop_fwd_def : thm
- val id_mut_back_def : thm
- val id_mut_fwd_def : thm
- val id_shared_fwd_def : thm
- val list_mem_fwd_def : thm
- val list_mem_loop_fwd_def : thm
- val list_nth_mut_loop_back_def : thm
- val list_nth_mut_loop_fwd_def : thm
- val list_nth_mut_loop_loop_back_def : thm
- val list_nth_mut_loop_loop_fwd_def : thm
- val list_nth_mut_loop_pair_back'a_def : thm
- val list_nth_mut_loop_pair_back'b_def : thm
- val list_nth_mut_loop_pair_fwd_def : thm
- val list_nth_mut_loop_pair_loop_back'a_def : thm
- val list_nth_mut_loop_pair_loop_back'b_def : thm
- val list_nth_mut_loop_pair_loop_fwd_def : thm
- val list_nth_mut_loop_pair_merge_back_def : thm
- val list_nth_mut_loop_pair_merge_fwd_def : thm
- val list_nth_mut_loop_pair_merge_loop_back_def : thm
- val list_nth_mut_loop_pair_merge_loop_fwd_def : thm
- val list_nth_mut_loop_with_id_back_def : thm
- val list_nth_mut_loop_with_id_fwd_def : thm
- val list_nth_mut_loop_with_id_loop_back_def : thm
- val list_nth_mut_loop_with_id_loop_fwd_def : thm
- val list_nth_mut_shared_loop_pair_back_def : thm
- val list_nth_mut_shared_loop_pair_fwd_def : thm
- val list_nth_mut_shared_loop_pair_loop_back_def : thm
- val list_nth_mut_shared_loop_pair_loop_fwd_def : thm
- val list_nth_mut_shared_loop_pair_merge_back_def : thm
- val list_nth_mut_shared_loop_pair_merge_fwd_def : thm
- val list_nth_mut_shared_loop_pair_merge_loop_back_def : thm
- val list_nth_mut_shared_loop_pair_merge_loop_fwd_def : thm
- val list_nth_shared_loop_fwd_def : thm
- val list_nth_shared_loop_loop_fwd_def : thm
- val list_nth_shared_loop_pair_fwd_def : thm
- val list_nth_shared_loop_pair_loop_fwd_def : thm
- val list_nth_shared_loop_pair_merge_fwd_def : thm
- val list_nth_shared_loop_pair_merge_loop_fwd_def : thm
- val list_nth_shared_loop_with_id_fwd_def : thm
- val list_nth_shared_loop_with_id_loop_fwd_def : thm
- val list_nth_shared_mut_loop_pair_back_def : thm
- val list_nth_shared_mut_loop_pair_fwd_def : thm
- val list_nth_shared_mut_loop_pair_loop_back_def : thm
- val list_nth_shared_mut_loop_pair_loop_fwd_def : thm
- val list_nth_shared_mut_loop_pair_merge_back_def : thm
- val list_nth_shared_mut_loop_pair_merge_fwd_def : thm
- val list_nth_shared_mut_loop_pair_merge_loop_back_def : thm
- val list_nth_shared_mut_loop_pair_merge_loop_fwd_def : thm
- val sum_fwd_def : thm
- val sum_loop_fwd_def : thm
- val sum_with_mut_borrows_fwd_def : thm
- val sum_with_mut_borrows_loop_fwd_def : thm
- val sum_with_shared_borrows_fwd_def : thm
- val sum_with_shared_borrows_loop_fwd_def : thm
-
- val loops_Funs_grammars : type_grammar.grammar * term_grammar.grammar
-(*
- [loops_Types] Parent theory of "loops_Funs"
-
- [clear_fwd_back_def] Definition
-
- ⊢ ∀v. clear_fwd_back v = clear_loop_fwd_back v (int_to_usize 0)
-
- [clear_loop_fwd_back_def] Definition
-
- ⊢ ∀v i.
- clear_loop_fwd_back v i =
- (let
- i0 = vec_len v
- in
- if usize_lt i i0 then
- do
- i1 <- usize_add i (int_to_usize 1);
- v0 <- vec_index_mut_back v i (int_to_u32 0);
- clear_loop_fwd_back v0 i1
- od
- else Return v)
-
- [get_elem_mut_back_def] Definition
-
- ⊢ ∀slots x ret.
- get_elem_mut_back slots x ret =
- do
- l <- vec_index_mut_fwd slots (int_to_usize 0);
- l0 <- get_elem_mut_loop_back x l ret;
- vec_index_mut_back slots (int_to_usize 0) l0
- od
-
- [get_elem_mut_fwd_def] Definition
-
- ⊢ ∀slots x.
- get_elem_mut_fwd slots x =
- do
- l <- vec_index_mut_fwd slots (int_to_usize 0);
- get_elem_mut_loop_fwd x l
- od
-
- [get_elem_mut_loop_back_def] Definition
-
- ⊢ ∀x ls ret.
- get_elem_mut_loop_back x ls ret =
- case ls of
- ListCons y tl =>
- if y = x then Return (ListCons ret tl)
- else
- do
- tl0 <- get_elem_mut_loop_back x tl ret;
- Return (ListCons y tl0)
- od
- | ListNil => Fail Failure
-
- [get_elem_mut_loop_fwd_def] Definition
-
- ⊢ ∀x ls.
- get_elem_mut_loop_fwd x ls =
- case ls of
- ListCons y tl =>
- if y = x then Return y else get_elem_mut_loop_fwd x tl
- | ListNil => Fail Failure
-
- [get_elem_shared_fwd_def] Definition
-
- ⊢ ∀slots x.
- get_elem_shared_fwd slots x =
- do
- l <- vec_index_fwd slots (int_to_usize 0);
- get_elem_shared_loop_fwd x l
- od
-
- [get_elem_shared_loop_fwd_def] Definition
-
- ⊢ ∀x ls.
- get_elem_shared_loop_fwd x ls =
- case ls of
- ListCons y tl =>
- if y = x then Return y else get_elem_shared_loop_fwd x tl
- | ListNil => Fail Failure
-
- [id_mut_back_def] Definition
-
- ⊢ ∀ls ret. id_mut_back ls ret = Return ret
-
- [id_mut_fwd_def] Definition
-
- ⊢ ∀ls. id_mut_fwd ls = Return ls
-
- [id_shared_fwd_def] Definition
-
- ⊢ ∀ls. id_shared_fwd ls = Return ls
-
- [list_mem_fwd_def] Definition
-
- ⊢ ∀x ls. list_mem_fwd x ls = list_mem_loop_fwd x ls
-
- [list_mem_loop_fwd_def] Definition
-
- ⊢ ∀x ls.
- list_mem_loop_fwd x ls =
- case ls of
- ListCons y tl =>
- if y = x then Return T else list_mem_loop_fwd x tl
- | ListNil => Return F
-
- [list_nth_mut_loop_back_def] Definition
-
- ⊢ ∀ls i ret.
- list_nth_mut_loop_back ls i ret =
- list_nth_mut_loop_loop_back ls i ret
-
- [list_nth_mut_loop_fwd_def] Definition
-
- ⊢ ∀ls i. list_nth_mut_loop_fwd ls i = list_nth_mut_loop_loop_fwd ls i
-
- [list_nth_mut_loop_loop_back_def] Definition
-
- ⊢ ∀ls i ret.
- list_nth_mut_loop_loop_back ls i ret =
- case ls of
- ListCons x tl =>
- if i = int_to_u32 0 then Return (ListCons ret tl)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl0 <- list_nth_mut_loop_loop_back tl i0 ret;
- Return (ListCons x tl0)
- od
- | ListNil => Fail Failure
-
- [list_nth_mut_loop_loop_fwd_def] Definition
-
- ⊢ ∀ls i.
- list_nth_mut_loop_loop_fwd ls i =
- case ls of
- ListCons x tl =>
- if i = int_to_u32 0 then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_loop_loop_fwd tl i0
- od
- | ListNil => Fail Failure
-
- [list_nth_mut_loop_pair_back'a_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_mut_loop_pair_back'a ls0 ls1 i ret =
- list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret
-
- [list_nth_mut_loop_pair_back'b_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_mut_loop_pair_back'b ls0 ls1 i ret =
- list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret
-
- [list_nth_mut_loop_pair_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_mut_loop_pair_fwd ls0 ls1 i =
- list_nth_mut_loop_pair_loop_fwd ls0 ls1 i
-
- [list_nth_mut_loop_pair_loop_back'a_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (ListCons ret tl0)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl00 <-
- list_nth_mut_loop_pair_loop_back'a tl0 tl1 i0 ret;
- Return (ListCons x0 tl00)
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_mut_loop_pair_loop_back'b_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (ListCons ret tl1)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl10 <-
- list_nth_mut_loop_pair_loop_back'b tl0 tl1 i0 ret;
- Return (ListCons x1 tl10)
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_mut_loop_pair_loop_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_mut_loop_pair_loop_fwd ls0 ls1 i =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (x0,x1)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_loop_pair_loop_fwd tl0 tl1 i0
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_mut_loop_pair_merge_back_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_mut_loop_pair_merge_back ls0 ls1 i ret =
- list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret
-
- [list_nth_mut_loop_pair_merge_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_mut_loop_pair_merge_fwd ls0 ls1 i =
- list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i
-
- [list_nth_mut_loop_pair_merge_loop_back_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then
- (let
- (t,t0) = ret
- in
- Return (ListCons t tl0,ListCons t0 tl1))
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- (tl00,tl10) <-
- list_nth_mut_loop_pair_merge_loop_back tl0 tl1 i0
- ret;
- Return (ListCons x0 tl00,ListCons x1 tl10)
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_mut_loop_pair_merge_loop_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (x0,x1)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_loop_pair_merge_loop_fwd tl0 tl1 i0
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_mut_loop_with_id_back_def] Definition
-
- ⊢ ∀ls i ret.
- list_nth_mut_loop_with_id_back ls i ret =
- do
- ls0 <- id_mut_fwd ls;
- l <- list_nth_mut_loop_with_id_loop_back i ls0 ret;
- id_mut_back ls l
- od
-
- [list_nth_mut_loop_with_id_fwd_def] Definition
-
- ⊢ ∀ls i.
- list_nth_mut_loop_with_id_fwd ls i =
- do
- ls0 <- id_mut_fwd ls;
- list_nth_mut_loop_with_id_loop_fwd i ls0
- od
-
- [list_nth_mut_loop_with_id_loop_back_def] Definition
-
- ⊢ ∀i ls ret.
- list_nth_mut_loop_with_id_loop_back i ls ret =
- case ls of
- ListCons x tl =>
- if i = int_to_u32 0 then Return (ListCons ret tl)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl0 <- list_nth_mut_loop_with_id_loop_back i0 tl ret;
- Return (ListCons x tl0)
- od
- | ListNil => Fail Failure
-
- [list_nth_mut_loop_with_id_loop_fwd_def] Definition
-
- ⊢ ∀i ls.
- list_nth_mut_loop_with_id_loop_fwd i ls =
- case ls of
- ListCons x tl =>
- if i = int_to_u32 0 then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_loop_with_id_loop_fwd i0 tl
- od
- | ListNil => Fail Failure
-
- [list_nth_mut_shared_loop_pair_back_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_mut_shared_loop_pair_back ls0 ls1 i ret =
- list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret
-
- [list_nth_mut_shared_loop_pair_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_mut_shared_loop_pair_fwd ls0 ls1 i =
- list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i
-
- [list_nth_mut_shared_loop_pair_loop_back_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (ListCons ret tl0)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl00 <-
- list_nth_mut_shared_loop_pair_loop_back tl0 tl1 i0
- ret;
- Return (ListCons x0 tl00)
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_mut_shared_loop_pair_loop_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (x0,x1)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_shared_loop_pair_loop_fwd tl0 tl1 i0
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_mut_shared_loop_pair_merge_back_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_mut_shared_loop_pair_merge_back ls0 ls1 i ret =
- list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret
-
- [list_nth_mut_shared_loop_pair_merge_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_mut_shared_loop_pair_merge_fwd ls0 ls1 i =
- list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i
-
- [list_nth_mut_shared_loop_pair_merge_loop_back_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (ListCons ret tl0)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl00 <-
- list_nth_mut_shared_loop_pair_merge_loop_back tl0
- tl1 i0 ret;
- Return (ListCons x0 tl00)
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_mut_shared_loop_pair_merge_loop_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (x0,x1)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_shared_loop_pair_merge_loop_fwd tl0 tl1
- i0
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_shared_loop_fwd_def] Definition
-
- ⊢ ∀ls i.
- list_nth_shared_loop_fwd ls i =
- list_nth_shared_loop_loop_fwd ls i
-
- [list_nth_shared_loop_loop_fwd_def] Definition
-
- ⊢ ∀ls i.
- list_nth_shared_loop_loop_fwd ls i =
- case ls of
- ListCons x tl =>
- if i = int_to_u32 0 then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_loop_loop_fwd tl i0
- od
- | ListNil => Fail Failure
-
- [list_nth_shared_loop_pair_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_shared_loop_pair_fwd ls0 ls1 i =
- list_nth_shared_loop_pair_loop_fwd ls0 ls1 i
-
- [list_nth_shared_loop_pair_loop_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_shared_loop_pair_loop_fwd ls0 ls1 i =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (x0,x1)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_loop_pair_loop_fwd tl0 tl1 i0
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_shared_loop_pair_merge_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_shared_loop_pair_merge_fwd ls0 ls1 i =
- list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i
-
- [list_nth_shared_loop_pair_merge_loop_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (x0,x1)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_loop_pair_merge_loop_fwd tl0 tl1 i0
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_shared_loop_with_id_fwd_def] Definition
-
- ⊢ ∀ls i.
- list_nth_shared_loop_with_id_fwd ls i =
- do
- ls0 <- id_shared_fwd ls;
- list_nth_shared_loop_with_id_loop_fwd i ls0
- od
-
- [list_nth_shared_loop_with_id_loop_fwd_def] Definition
-
- ⊢ ∀i ls.
- list_nth_shared_loop_with_id_loop_fwd i ls =
- case ls of
- ListCons x tl =>
- if i = int_to_u32 0 then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_loop_with_id_loop_fwd i0 tl
- od
- | ListNil => Fail Failure
-
- [list_nth_shared_mut_loop_pair_back_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_shared_mut_loop_pair_back ls0 ls1 i ret =
- list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret
-
- [list_nth_shared_mut_loop_pair_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_shared_mut_loop_pair_fwd ls0 ls1 i =
- list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i
-
- [list_nth_shared_mut_loop_pair_loop_back_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (ListCons ret tl1)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl10 <-
- list_nth_shared_mut_loop_pair_loop_back tl0 tl1 i0
- ret;
- Return (ListCons x1 tl10)
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_shared_mut_loop_pair_loop_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (x0,x1)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_mut_loop_pair_loop_fwd tl0 tl1 i0
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_shared_mut_loop_pair_merge_back_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_shared_mut_loop_pair_merge_back ls0 ls1 i ret =
- list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret
-
- [list_nth_shared_mut_loop_pair_merge_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_shared_mut_loop_pair_merge_fwd ls0 ls1 i =
- list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i
-
- [list_nth_shared_mut_loop_pair_merge_loop_back_def] Definition
-
- ⊢ ∀ls0 ls1 i ret.
- list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (ListCons ret tl1)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl10 <-
- list_nth_shared_mut_loop_pair_merge_loop_back tl0
- tl1 i0 ret;
- Return (ListCons x1 tl10)
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [list_nth_shared_mut_loop_pair_merge_loop_fwd_def] Definition
-
- ⊢ ∀ls0 ls1 i.
- list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i =
- case ls0 of
- ListCons x0 tl0 =>
- (case ls1 of
- ListCons x1 tl1 =>
- if i = int_to_u32 0 then Return (x0,x1)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_shared_mut_loop_pair_merge_loop_fwd tl0 tl1
- i0
- od
- | ListNil => Fail Failure)
- | ListNil => Fail Failure
-
- [sum_fwd_def] Definition
-
- ⊢ ∀max. sum_fwd max = sum_loop_fwd max (int_to_u32 0) (int_to_u32 0)
-
- [sum_loop_fwd_def] Definition
-
- ⊢ ∀max i s.
- sum_loop_fwd max i s =
- if u32_lt i max then
- do
- s0 <- u32_add s i;
- i0 <- u32_add i (int_to_u32 1);
- sum_loop_fwd max i0 s0
- od
- else u32_mul s (int_to_u32 2)
-
- [sum_with_mut_borrows_fwd_def] Definition
-
- ⊢ ∀max.
- sum_with_mut_borrows_fwd max =
- sum_with_mut_borrows_loop_fwd max (int_to_u32 0) (int_to_u32 0)
-
- [sum_with_mut_borrows_loop_fwd_def] Definition
-
- ⊢ ∀max mi ms.
- sum_with_mut_borrows_loop_fwd max mi ms =
- if u32_lt mi max then
- do
- ms0 <- u32_add ms mi;
- mi0 <- u32_add mi (int_to_u32 1);
- sum_with_mut_borrows_loop_fwd max mi0 ms0
- od
- else u32_mul ms (int_to_u32 2)
-
- [sum_with_shared_borrows_fwd_def] Definition
-
- ⊢ ∀max.
- sum_with_shared_borrows_fwd max =
- sum_with_shared_borrows_loop_fwd max (int_to_u32 0)
- (int_to_u32 0)
-
- [sum_with_shared_borrows_loop_fwd_def] Definition
-
- ⊢ ∀max i s.
- sum_with_shared_borrows_loop_fwd max i s =
- if u32_lt i max then
- do
- i0 <- u32_add i (int_to_u32 1);
- s0 <- u32_add s i0;
- sum_with_shared_borrows_loop_fwd max i0 s0
- od
- else u32_mul s (int_to_u32 2)
-
-
-*)
-end
diff --git a/tests/hol4/misc-loops/loops_TypesScript.sml b/tests/hol4/misc-loops/loops_TypesScript.sml
deleted file mode 100644
index e3e5b8d1..00000000
--- a/tests/hol4/misc-loops/loops_TypesScript.sml
+++ /dev/null
@@ -1,13 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [loops]: type definitions *)
-open primitivesLib divDefLib
-
-val _ = new_theory "loops_Types"
-
-
-Datatype:
- (** [loops::List] *)
- list_t = | ListCons 't list_t | ListNil
-End
-
-val _ = export_theory ()
diff --git a/tests/hol4/misc-loops/loops_TypesTheory.sig b/tests/hol4/misc-loops/loops_TypesTheory.sig
deleted file mode 100644
index c3e638d8..00000000
--- a/tests/hol4/misc-loops/loops_TypesTheory.sig
+++ /dev/null
@@ -1,94 +0,0 @@
-signature loops_TypesTheory =
-sig
- type thm = Thm.thm
-
- (* Definitions *)
- val list_t_TY_DEF : thm
- val list_t_case_def : thm
- val list_t_size_def : thm
-
- (* Theorems *)
- val datatype_list_t : thm
- val list_t_11 : thm
- val list_t_Axiom : thm
- val list_t_case_cong : thm
- val list_t_case_eq : thm
- val list_t_distinct : thm
- val list_t_induction : thm
- val list_t_nchotomy : thm
-
- val loops_Types_grammars : type_grammar.grammar * term_grammar.grammar
-(*
- [divDef] Parent theory of "loops_Types"
-
- [list_t_TY_DEF] Definition
-
- ⊢ ∃rep.
- TYPE_DEFINITION
- (λa0'.
- ∀ $var$('list_t').
- (∀a0'.
- (∃a0 a1.
- a0' =
- (λa0 a1.
- ind_type$CONSTR 0 a0
- (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
- a0 a1 ∧ $var$('list_t') a1) ∨
- a0' =
- ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
- $var$('list_t') a0') ⇒
- $var$('list_t') a0') rep
-
- [list_t_case_def] Definition
-
- ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
- ∀f v. list_t_CASE ListNil f v = v
-
- [list_t_size_def] Definition
-
- ⊢ (∀f a0 a1.
- list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
- ∀f. list_t_size f ListNil = 0
-
- [datatype_list_t] Theorem
-
- ⊢ DATATYPE (list_t ListCons ListNil)
-
- [list_t_11] Theorem
-
- ⊢ ∀a0 a1 a0' a1'.
- ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
-
- [list_t_Axiom] Theorem
-
- ⊢ ∀f0 f1. ∃fn.
- (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
- fn ListNil = f1
-
- [list_t_case_cong] Theorem
-
- ⊢ ∀M M' f v.
- M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
- (M' = ListNil ⇒ v = v') ⇒
- list_t_CASE M f v = list_t_CASE M' f' v'
-
- [list_t_case_eq] Theorem
-
- ⊢ list_t_CASE x f v = v' ⇔
- (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
-
- [list_t_distinct] Theorem
-
- ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
-
- [list_t_induction] Theorem
-
- ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
-
- [list_t_nchotomy] Theorem
-
- ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
-
-
-*)
-end
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 16:47:44 +0000