Merge pull request #31 from AeneasVerif/son_lean_backend

Improve the Lean backend

2 files changed, 52 insertions, 43 deletions

diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
index 5a8f7ff8..6ec6223d 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
@@ -7,13 +7,13 @@ val _ = new_theory "hashmapMain_Funs"
 
 
 val hashmap_hash_key_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::hash_key] *)
+  (** [hashmap_main::hashmap::hash_key]: forward function *)
   hashmap_hash_key_fwd (k : usize) : usize result =
     Return k
 ’
 
 val [hashmap_hash_map_allocate_slots_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *)
   hashmap_hash_map_allocate_slots_loop_fwd
     (slots : 't hashmap_list_t vec) (n : usize) :
     't hashmap_list_t vec result
@@ -29,7 +29,7 @@ val [hashmap_hash_map_allocate_slots_loop_fwd_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_allocate_slots_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: forward function *)
   hashmap_hash_map_allocate_slots_fwd
     (slots : 't hashmap_list_t vec) (n : usize) :
     't hashmap_list_t vec result
@@ -38,7 +38,7 @@ val hashmap_hash_map_allocate_slots_fwd_def = Define ‘
 ’
 
 val hashmap_hash_map_new_with_capacity_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity]: forward function *)
   hashmap_hash_map_new_with_capacity_fwd
     (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) :
     't hashmap_hash_map_t result
@@ -60,14 +60,15 @@ val hashmap_hash_map_new_with_capacity_fwd_def = Define ‘
 ’
 
 val hashmap_hash_map_new_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::new] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::new]: forward function *)
   hashmap_hash_map_new_fwd : 't hashmap_hash_map_t result =
     hashmap_hash_map_new_with_capacity_fwd (int_to_usize 32) (int_to_usize 4)
       (int_to_usize 5)
 ’
 
 val [hashmap_hash_map_clear_loop_fwd_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
   hashmap_hash_map_clear_loop_fwd_back
     (slots : 't hashmap_list_t vec) (i : usize) :
     't hashmap_list_t vec result
@@ -84,7 +85,8 @@ val [hashmap_hash_map_clear_loop_fwd_back_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_clear_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::clear]: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
   hashmap_hash_map_clear_fwd_back
     (self : 't hashmap_hash_map_t) : 't hashmap_hash_map_t result =
     do
@@ -102,13 +104,13 @@ val hashmap_hash_map_clear_fwd_back_def = Define ‘
 ’
 
 val hashmap_hash_map_len_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::len] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::len]: forward function *)
   hashmap_hash_map_len_fwd (self : 't hashmap_hash_map_t) : usize result =
     Return self.hashmap_hash_map_num_entries
 ’
 
 val [hashmap_hash_map_insert_in_list_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *)
   hashmap_hash_map_insert_in_list_loop_fwd
     (key : usize) (value : 't) (ls : 't hashmap_list_t) : bool result =
     (case ls of
@@ -120,14 +122,14 @@ val [hashmap_hash_map_insert_in_list_loop_fwd_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_insert_in_list_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: forward function *)
   hashmap_hash_map_insert_in_list_fwd
     (key : usize) (value : 't) (ls : 't hashmap_list_t) : bool result =
     hashmap_hash_map_insert_in_list_loop_fwd key value ls
 ’
 
 val [hashmap_hash_map_insert_in_list_loop_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *)
   hashmap_hash_map_insert_in_list_loop_back
     (key : usize) (value : 't) (ls : 't hashmap_list_t) :
     't hashmap_list_t result
@@ -146,7 +148,7 @@ val [hashmap_hash_map_insert_in_list_loop_back_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_insert_in_list_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: backward function 0 *)
   hashmap_hash_map_insert_in_list_back
     (key : usize) (value : 't) (ls : 't hashmap_list_t) :
     't hashmap_list_t result
@@ -155,7 +157,8 @@ val hashmap_hash_map_insert_in_list_back_def = Define ‘
 ’
 
 val hashmap_hash_map_insert_no_resize_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
   hashmap_hash_map_insert_no_resize_fwd_back
     (self : 't hashmap_hash_map_t) (key : usize) (value : 't) :
     't hashmap_hash_map_t result
@@ -199,7 +202,8 @@ Definition core_num_u32_max_c_def:
 End
 
 val [hashmap_hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
   hashmap_hash_map_move_elements_from_list_loop_fwd_back
     (ntable : 't hashmap_hash_map_t) (ls : 't hashmap_list_t) :
     't hashmap_hash_map_t result
@@ -214,7 +218,8 @@ val [hashmap_hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_move_elements_from_list_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
   hashmap_hash_map_move_elements_from_list_fwd_back
     (ntable : 't hashmap_hash_map_t) (ls : 't hashmap_list_t) :
     't hashmap_hash_map_t result
@@ -223,7 +228,8 @@ val hashmap_hash_map_move_elements_from_list_fwd_back_def = Define ‘
 ’
 
 val [hashmap_hash_map_move_elements_loop_fwd_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
   hashmap_hash_map_move_elements_loop_fwd_back
     (ntable : 't hashmap_hash_map_t) (slots : 't hashmap_list_t vec)
     (i : usize) :
@@ -249,7 +255,8 @@ val [hashmap_hash_map_move_elements_loop_fwd_back_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_move_elements_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::move_elements]: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
   hashmap_hash_map_move_elements_fwd_back
     (ntable : 't hashmap_hash_map_t) (slots : 't hashmap_list_t vec)
     (i : usize) :
@@ -259,7 +266,8 @@ val hashmap_hash_map_move_elements_fwd_back_def = Define ‘
 ’
 
 val hashmap_hash_map_try_resize_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::try_resize]: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
   hashmap_hash_map_try_resize_fwd_back
     (self : 't hashmap_hash_map_t) : 't hashmap_hash_map_t result =
     do
@@ -293,7 +301,8 @@ val hashmap_hash_map_try_resize_fwd_back_def = Define ‘
 ’
 
 val hashmap_hash_map_insert_fwd_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::insert] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
   hashmap_hash_map_insert_fwd_back
     (self : 't hashmap_hash_map_t) (key : usize) (value : 't) :
     't hashmap_hash_map_t result
@@ -308,7 +317,7 @@ val hashmap_hash_map_insert_fwd_back_def = Define ‘
 ’
 
 val [hashmap_hash_map_contains_key_in_list_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *)
   hashmap_hash_map_contains_key_in_list_loop_fwd
     (key : usize) (ls : 't hashmap_list_t) : bool result =
     (case ls of
@@ -320,14 +329,14 @@ val [hashmap_hash_map_contains_key_in_list_loop_fwd_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_contains_key_in_list_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: forward function *)
   hashmap_hash_map_contains_key_in_list_fwd
     (key : usize) (ls : 't hashmap_list_t) : bool result =
     hashmap_hash_map_contains_key_in_list_loop_fwd key ls
 ’
 
 val hashmap_hash_map_contains_key_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::contains_key]: forward function *)
   hashmap_hash_map_contains_key_fwd
     (self : 't hashmap_hash_map_t) (key : usize) : bool result =
     do
@@ -342,7 +351,7 @@ val hashmap_hash_map_contains_key_fwd_def = Define ‘
 ’
 
 val [hashmap_hash_map_get_in_list_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *)
   hashmap_hash_map_get_in_list_loop_fwd
     (key : usize) (ls : 't hashmap_list_t) : 't result =
     (case ls of
@@ -354,14 +363,14 @@ val [hashmap_hash_map_get_in_list_loop_fwd_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_get_in_list_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: forward function *)
   hashmap_hash_map_get_in_list_fwd
     (key : usize) (ls : 't hashmap_list_t) : 't result =
     hashmap_hash_map_get_in_list_loop_fwd key ls
 ’
 
 val hashmap_hash_map_get_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::get]: forward function *)
   hashmap_hash_map_get_fwd
     (self : 't hashmap_hash_map_t) (key : usize) : 't result =
     do
@@ -376,7 +385,7 @@ val hashmap_hash_map_get_fwd_def = Define ‘
 ’
 
 val [hashmap_hash_map_get_mut_in_list_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *)
   hashmap_hash_map_get_mut_in_list_loop_fwd
     (ls : 't hashmap_list_t) (key : usize) : 't result =
     (case ls of
@@ -388,14 +397,14 @@ val [hashmap_hash_map_get_mut_in_list_loop_fwd_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_get_mut_in_list_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: forward function *)
   hashmap_hash_map_get_mut_in_list_fwd
     (ls : 't hashmap_list_t) (key : usize) : 't result =
     hashmap_hash_map_get_mut_in_list_loop_fwd ls key
 ’
 
 val [hashmap_hash_map_get_mut_in_list_loop_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *)
   hashmap_hash_map_get_mut_in_list_loop_back
     (ls : 't hashmap_list_t) (key : usize) (ret : 't) :
     't hashmap_list_t result
@@ -413,7 +422,7 @@ val [hashmap_hash_map_get_mut_in_list_loop_back_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_get_mut_in_list_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *)
   hashmap_hash_map_get_mut_in_list_back
     (ls : 't hashmap_list_t) (key : usize) (ret : 't) :
     't hashmap_list_t result
@@ -422,7 +431,7 @@ val hashmap_hash_map_get_mut_in_list_back_def = Define ‘
 ’
 
 val hashmap_hash_map_get_mut_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::get_mut]: forward function *)
   hashmap_hash_map_get_mut_fwd
     (self : 't hashmap_hash_map_t) (key : usize) : 't result =
     do
@@ -437,7 +446,7 @@ val hashmap_hash_map_get_mut_fwd_def = Define ‘
 ’
 
 val hashmap_hash_map_get_mut_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 *)
   hashmap_hash_map_get_mut_back
     (self : 't hashmap_hash_map_t) (key : usize) (ret : 't) :
     't hashmap_hash_map_t result
@@ -456,7 +465,7 @@ val hashmap_hash_map_get_mut_back_def = Define ‘
 ’
 
 val [hashmap_hash_map_remove_from_list_loop_fwd_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *)
   hashmap_hash_map_remove_from_list_loop_fwd
     (key : usize) (ls : 't hashmap_list_t) : 't option result =
     (case ls of
@@ -473,14 +482,14 @@ val [hashmap_hash_map_remove_from_list_loop_fwd_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_remove_from_list_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function *)
   hashmap_hash_map_remove_from_list_fwd
     (key : usize) (ls : 't hashmap_list_t) : 't option result =
     hashmap_hash_map_remove_from_list_loop_fwd key ls
 ’
 
 val [hashmap_hash_map_remove_from_list_loop_back_def] = DefineDiv ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *)
   hashmap_hash_map_remove_from_list_loop_back
     (key : usize) (ls : 't hashmap_list_t) : 't hashmap_list_t result =
     (case ls of
@@ -501,14 +510,14 @@ val [hashmap_hash_map_remove_from_list_loop_back_def] = DefineDiv ‘
 ’
 
 val hashmap_hash_map_remove_from_list_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: backward function 1 *)
   hashmap_hash_map_remove_from_list_back
     (key : usize) (ls : 't hashmap_list_t) : 't hashmap_list_t result =
     hashmap_hash_map_remove_from_list_loop_back key ls
 ’
 
 val hashmap_hash_map_remove_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::remove]: forward function *)
   hashmap_hash_map_remove_fwd
     (self : 't hashmap_hash_map_t) (key : usize) : 't option result =
     do
@@ -530,7 +539,7 @@ val hashmap_hash_map_remove_fwd_def = Define ‘
 ’
 
 val hashmap_hash_map_remove_back_def = Define ‘
-  (** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+  (** [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 *)
   hashmap_hash_map_remove_back
     (self : 't hashmap_hash_map_t) (key : usize) :
     't hashmap_hash_map_t result
@@ -566,7 +575,7 @@ val hashmap_hash_map_remove_back_def = Define ‘
 ’
 
 val hashmap_test1_fwd_def = Define ‘
-  (** [hashmap_main::hashmap::test1] *)
+  (** [hashmap_main::hashmap::test1]: forward function *)
   hashmap_test1_fwd : unit result =
     do
     hm <- hashmap_hash_map_new_fwd;
@@ -623,7 +632,7 @@ val hashmap_test1_fwd_def = Define ‘
 val _ = assert_return (“hashmap_test1_fwd”)
 
 val insert_on_disk_fwd_def = Define ‘
-  (** [hashmap_main::insert_on_disk] *)
+  (** [hashmap_main::insert_on_disk]: forward function *)
   insert_on_disk_fwd
     (key : usize) (value : u64) (st : state) : (state # unit) result =
     do
@@ -635,7 +644,7 @@ val insert_on_disk_fwd_def = Define ‘
 ’
 
 val main_fwd_def = Define ‘
-  (** [hashmap_main::main] *)
+  (** [hashmap_main::main]: forward function *)
   main_fwd : unit result =
     Return ()
 ’
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
index 5f6bcbb4..f7221d92 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
@@ -1,15 +1,15 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: opaque function definitions *)
+(** [hashmap_main]: external function declarations *)
 open primitivesLib divDefLib
 open hashmapMain_TypesTheory
 
 val _ = new_theory "hashmapMain_Opaque"
 
 
-val _ = new_constant ("hashmap_utils_deserialize_fwd",
+(** [hashmap_main::hashmap_utils::deserialize]: forward function *)val _ = new_constant ("hashmap_utils_deserialize_fwd",
   “:state -> (state # u64 hashmap_hash_map_t) result”)
 
-val _ = new_constant ("hashmap_utils_serialize_fwd",
+(** [hashmap_main::hashmap_utils::serialize]: forward function *)val _ = new_constant ("hashmap_utils_serialize_fwd",
   “:u64 hashmap_hash_map_t -> state -> (state # unit) result”)
 
 val _ = export_theory ()