Merge pull request #206 from AeneasVerif/subdir

1 files changed, 37 insertions, 0 deletions

diff --git a/tests/hol4/polonius_list/poloniusListScript.sml b/tests/hol4/polonius_list/poloniusListScript.sml
new file mode 100644
index 00000000..06876ed4
--- /dev/null
+++ b/tests/hol4/polonius_list/poloniusListScript.sml
@@ -0,0 +1,37 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [polonius_list] *)
+open primitivesLib divDefLib
+
+val _ = new_theory "poloniusList"
+
+
+Datatype:
+  (** [polonius_list::List] *)
+  list_t = | ListCons 't list_t | ListNil
+End
+
+val [get_list_at_x_fwd_def] = DefineDiv ‘
+  (** [polonius_list::get_list_at_x]: forward function *)
+  get_list_at_x_fwd (ls : u32 list_t) (x : u32) : u32 list_t result =
+    (case ls of
+    | ListCons hd tl =>
+      if hd = x then Return (ListCons hd tl) else get_list_at_x_fwd tl x
+    | ListNil => Return ListNil)
+’
+
+val [get_list_at_x_back_def] = DefineDiv ‘
+  (** [polonius_list::get_list_at_x]: backward function 0 *)
+  get_list_at_x_back
+    (ls : u32 list_t) (x : u32) (ret : u32 list_t) : u32 list_t result =
+    (case ls of
+    | ListCons hd tl =>
+      if hd = x
+      then Return ret
+      else (do
+            tl0 <- get_list_at_x_back tl x ret;
+            Return (ListCons hd tl0)
+            od)
+    | ListNil => Return ret)
+’
+
+val _ = export_theory ()