From 89d7a7ee757faccd8d4c9c3c7c7baa0a8ef9d2bb Mon Sep 17 00:00:00 2001 From: Ryota Kobayashi Date: Tue, 10 Oct 2023 14:49:27 +0900 Subject: [PATCH] add tests --- src/test/list/append.imp | 8 ++++---- src/test/list/mochi/append.ml | 36 +++++++++++++++++++++++++++++++++ src/test/list/mochi/reverse2.ml | 34 +++++++++++++++++++++++++++++++ src/test/list/reverse2.imp | 7 +++---- 4 files changed, 77 insertions(+), 8 deletions(-) create mode 100644 src/test/list/mochi/append.ml create mode 100644 src/test/list/mochi/reverse2.ml diff --git a/src/test/list/append.imp b/src/test/list/append.imp index d300317c..e56145ac 100644 --- a/src/test/list/append.imp +++ b/src/test/list/append.imp @@ -54,9 +54,9 @@ append(l, r){ let n = ( _ : ~ >= 0) in let l1 = mklist(m) in let l2 = mklist(n) in - let l = append(l1, l2) in - let sum_length = len(l1) + len(l2) in { - alias(l = l1); - assert(len(l) = sum_length) + let sum_length = len(l1) + len(l2) in + let l = append(l1, l2) in { + alias(l = l1); + assert(len(l) = sum_length) } } \ No newline at end of file diff --git a/src/test/list/mochi/append.ml b/src/test/list/mochi/append.ml new file mode 100644 index 00000000..15c9e79d --- /dev/null +++ b/src/test/list/mochi/append.ml @@ -0,0 +1,36 @@ +let rec mklist n = + if n > 0 then + let h = Random.int 0 in + let t = mklist (n - 1) in + h :: t + else [] + +and len (l: int list) = + match l with + [] -> 0 + | _ :: t -> 1 + len t + +and append (l1: int list) (l2: int list) = + match l1 with + [] -> l2 + | h :: t -> h :: (append t l2) + +let main () = + let m = + let rec nd' () = + let _' = Random.int 0 in + if _' >= 0 then _' else nd' () + in nd' () + in + let n = + let rec nd' () = + let _' = Random.int 0 in + if _' >= 0 then _' else nd' () + in nd' () + in + let l1 = mklist m in + let l2 = mklist n in + let sum_length = len l1 + len l2 in + let l = append l1 l2 in + assert (len(l) = sum_length); + (()) diff --git a/src/test/list/mochi/reverse2.ml b/src/test/list/mochi/reverse2.ml new file mode 100644 index 00000000..d900d991 --- /dev/null +++ b/src/test/list/mochi/reverse2.ml @@ -0,0 +1,34 @@ +let rec mklist n = + if n > 0 then + let h = Random.int 0 in + let t = mklist (n - 1) in + h :: t + else [] + +and _reverse (l: int list) (acc: int list) = + match l with + [] -> acc + | h :: t -> _reverse t (h :: acc) + +and reverse (l: int list) = + _reverse l [] + +and len (l: int list) = + match l with + [] -> 0 + | _ :: t -> 1 + len t + +let main () = + let n = + let rec nd' () = + let _' = Random.int 0 in + if _' >= 0 then _' else nd' () + in nd' () + in + let l = mklist n in + let __t0 = len l in + let rev_l = reverse l in + let __t1 = len rev_l in + assert (__t0 = __t1); + let __t2 = 0 in + (()) diff --git a/src/test/list/reverse2.imp b/src/test/list/reverse2.imp index e48c4bb3..09d99c3b 100644 --- a/src/test/list/reverse2.imp +++ b/src/test/list/reverse2.imp @@ -48,8 +48,7 @@ len(l) { { let n = ( _ : ~ >= 0) in let l = mklist(n) in - let rev_l = reverse(l) in { - alias(l = rev_l); - assert(len(l) = len(rev_l)) - } + let len_l = len(l) in + let rev_l = reverse(l) in + assert(len_l = len(rev_l)) } \ No newline at end of file