From 0797ca2d7b7f55b3387a4a2b8e69dd2c74d069ae Mon Sep 17 00:00:00 2001
From: Hrutvik Kanabar <hrutvikkanabar@yahoo.co.uk>
Date: Wed, 13 Mar 2024 14:33:12 +0000
Subject: [PATCH] Add a couple of tests

Co-authored-by: Magnus Myreen <myreen@chalmers.se>
---
 cv_translator/cv_demoScript.sml | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/cv_translator/cv_demoScript.sml b/cv_translator/cv_demoScript.sml
index cfa25edbb1..1d403b64bd 100644
--- a/cv_translator/cv_demoScript.sml
+++ b/cv_translator/cv_demoScript.sml
@@ -7,6 +7,11 @@ open arithmeticTheory wordsTheory cv_repTheory cv_primTheory cv_transLib wordsLi
 
 val _ = new_theory "cv_demo";
 
+fun test_for_failure f x =
+  case total f x of
+    NONE => ()
+  | SOME _ => failwith "unexpected success";
+
 Overload c2n[local] = “cv$c2n”
 Overload c2b[local] = “cv$c2b”
 Overload Num[local] = “cv$Num”
@@ -197,4 +202,24 @@ End
 
 val _ = cv_trans test_u2_def;
 
+Datatype:
+  foo = RoseTree (num -> num) (foo list)
+End
+
+val _ = test_for_failure (cv_rep_for []) “RoseTree (λi. i) []”;
+
+Definition missing_arg_def:
+  missing_arg = K
+End
+
+val _ = cv_trans combinTheory.K_THM
+val _ = cv_trans missing_arg_def
+
+Definition apply_list_def:
+  apply_list [] x = x ∧
+  apply_list (f::fs) x = apply_list fs (f x)
+End
+
+val _ = test_for_failure cv_trans apply_list_def;
+
 val _ = export_theory();