Merge pull request #31 from AeneasVerif/son_lean_backend

Improve the Lean backend

1 files changed, 11 insertions, 10 deletions

diff --git a/tests/hol4/misc-paper/paperScript.sml b/tests/hol4/misc-paper/paperScript.sml
index 4d6e99ba..3ac5b6ca 100644
--- a/tests/hol4/misc-paper/paperScript.sml
+++ b/tests/hol4/misc-paper/paperScript.sml
@@ -6,13 +6,14 @@ val _ = new_theory "paper"
 
 
 val ref_incr_fwd_back_def = Define ‘
-  (** [paper::ref_incr] *)
+  (** [paper::ref_incr]: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
   ref_incr_fwd_back (x : i32) : i32 result =
     i32_add x (int_to_i32 1)
 ’
 
 val test_incr_fwd_def = Define ‘
-  (** [paper::test_incr] *)
+  (** [paper::test_incr]: forward function *)
   test_incr_fwd : unit result =
     do
     x <- ref_incr_fwd_back (int_to_i32 0);
@@ -24,19 +25,19 @@ val test_incr_fwd_def = Define ‘
 val _ = assert_return (“test_incr_fwd”)
 
 val choose_fwd_def = Define ‘
-  (** [paper::choose] *)
+  (** [paper::choose]: forward function *)
   choose_fwd (b : bool) (x : 't) (y : 't) : 't result =
     if b then Return x else Return y
 ’
 
 val choose_back_def = Define ‘
-  (** [paper::choose] *)
+  (** [paper::choose]: backward function 0 *)
   choose_back (b : bool) (x : 't) (y : 't) (ret : 't) : ('t # 't) result =
     if b then Return (ret, y) else Return (x, ret)
 ’
 
 val test_choose_fwd_def = Define ‘
-  (** [paper::test_choose] *)
+  (** [paper::test_choose]: forward function *)
   test_choose_fwd : unit result =
     do
     z <- choose_fwd T (int_to_i32 0) (int_to_i32 0);
@@ -62,7 +63,7 @@ Datatype:
 End
 
 val [list_nth_mut_fwd_def] = DefineDiv ‘
-  (** [paper::list_nth_mut] *)
+  (** [paper::list_nth_mut]: forward function *)
   list_nth_mut_fwd (l : 't list_t) (i : u32) : 't result =
     (case l of
     | ListCons x tl =>
@@ -76,7 +77,7 @@ val [list_nth_mut_fwd_def] = DefineDiv ‘
 ’
 
 val [list_nth_mut_back_def] = DefineDiv ‘
-  (** [paper::list_nth_mut] *)
+  (** [paper::list_nth_mut]: backward function 0 *)
   list_nth_mut_back (l : 't list_t) (i : u32) (ret : 't) : 't list_t result =
     (case l of
     | ListCons x tl =>
@@ -92,7 +93,7 @@ val [list_nth_mut_back_def] = DefineDiv ‘
 ’
 
 val [sum_fwd_def] = DefineDiv ‘
-  (** [paper::sum] *)
+  (** [paper::sum]: forward function *)
   sum_fwd (l : i32 list_t) : i32 result =
     (case l of
     | ListCons x tl => do
@@ -103,7 +104,7 @@ val [sum_fwd_def] = DefineDiv ‘
 ’
 
 val test_nth_fwd_def = Define ‘
-  (** [paper::test_nth] *)
+  (** [paper::test_nth]: forward function *)
   test_nth_fwd : unit result =
     let l = ListNil in
     let l0 = ListCons (int_to_i32 3) l in
@@ -121,7 +122,7 @@ val test_nth_fwd_def = Define ‘
 val _ = assert_return (“test_nth_fwd”)
 
 val call_choose_fwd_def = Define ‘
-  (** [paper::call_choose] *)
+  (** [paper::call_choose]: forward function *)
   call_choose_fwd (p : (u32 # u32)) : u32 result =
     let (px, py) = p in
     do