nicer lem output: no more unecessary 'unit' returns if if-expressions, for-loops or case-expressions also return updated variables

4 files changed, 29 insertions, 29 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 4cd76156..a9aa3218 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -247,23 +247,23 @@ val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> M 'e
 let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit)
 
 val foreachM_inc : forall 'e 'vars. (nat * nat * nat) -> 'vars ->
-                  (nat -> 'vars -> M 'e (unit * 'vars)) -> M 'e (unit * 'vars)
+                  (nat -> 'vars -> M 'e 'vars) -> M 'e 'vars
 let rec foreachM_inc (i,stop,by) vars body = 
   if i <= stop
   then
-    body i vars >>= fun (_,vars) ->
+    body i vars >>= fun vars ->
     foreachM_inc (i + by,stop,by) vars body
-  else return ((),vars)
+  else return vars
 
 
 val foreachM_dec : forall 'e 'vars. (nat * nat * nat) -> 'vars ->
-                  (nat -> 'vars -> M 'e (unit * 'vars)) -> M 'e (unit * 'vars)
+                  (nat -> 'vars -> M 'e 'vars) -> M 'e 'vars
 let rec foreachM_dec (i,stop,by) vars body = 
   if i >= stop
   then
-    body i vars >>= fun (_,vars) ->
+    body i vars >>= fun vars ->
     foreachM_dec (i - by,stop,by) vars body
-  else return ((),vars)
+  else return vars
 
 
 let write_two_regs r1 r2 vec =
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index b9a4fbd1..454778c4 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -527,22 +527,21 @@ let toNaturalFiveTup (n1,n2,n3,n4,n5) =
    toNatural n5)
 
 
-
-
-val foreach_inc :  forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
-                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+val foreach_inc :  forall 'vars. (integer * integer * integer) -> 'vars ->
+                   (integer -> 'vars -> 'vars) -> 'vars
 let rec foreach_inc (i,stop,by) vars body = 
   if i <= stop
-  then
-    let (_,vars) = body i vars in
-    foreach_inc (i + by,stop,by) vars body
-  else ((),vars)
+  then let vars = body i vars in
+       foreach_inc (i + by,stop,by) vars body
+  else vars
 
-val foreach_dec : forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
-                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> 'vars) -> 'vars
 let rec foreach_dec (i,stop,by) vars body = 
   if i >= stop
-  then
-    let (_,vars) = body i vars in
-    foreach_dec (i - by,stop,by) vars body
-  else ((),vars)
+  then let vars = body i vars in
+       foreach_dec (i - by,stop,by) vars body
+  else vars
+
+
+         
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 51658d6e..5fc59207 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -158,20 +158,20 @@ let read_two_regs r1 r2 =
   return (v1 ^^ v2)
 
 val foreachM_inc : forall 'e 'vars. (i * i * i) -> 'vars ->
-                  (i -> 'vars -> M 'e (unit * 'vars)) -> M 'e (unit * 'vars)
+                  (i -> 'vars -> M 'e 'vars) -> M 'e 'vars
 let rec foreachM_inc (i,stop,by) vars body = 
   if i <= stop
   then
-    body i vars >>= fun (_,vars) ->
+    body i vars >>= fun vars ->
     foreachM_inc (i + by,stop,by) vars body
-  else return ((),vars)
+  else return vars
 
 
 val foreachM_dec : forall 'e 'vars. (i * i * i) -> 'vars ->
-                  (i -> 'vars -> M 'e (unit * 'vars)) -> M 'e (unit * 'vars)
+                  (i -> 'vars -> M 'e 'vars) -> M 'e 'vars
 let rec foreachM_dec (i,stop,by) vars body = 
   if i >= stop
   then
-    body i vars >>= fun (_,vars) ->
+    body i vars >>= fun vars ->
     foreachM_dec (i - by,stop,by) vars body
-  else return ((),vars)
+  else return vars
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index 7c22e3ba..b2d68132 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -34,7 +34,7 @@ let vector_concat (Vector bs start is_inc) (Vector bs' _ _) =
 
 let (^^) = vector_concat
 
-val slice : vector bit -> integer -> integer -> vector bit
+val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a
 let slice (Vector bs start is_inc) n m =
   let n = natFromInteger n in
   let m = natFromInteger m in
@@ -45,6 +45,7 @@ let slice (Vector bs start is_inc) n m =
   let n = integerFromNat n in
   Vector subvector n is_inc
 
+val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a
 let update (Vector bs start is_inc) n m (Vector bs' _ _) =
   let n = natFromInteger n in
   let m = natFromInteger m in
@@ -55,10 +56,10 @@ let update (Vector bs start is_inc) n m (Vector bs' _ _) =
   let start = integerFromNat start in
   Vector (prefix ++ (List.take length bs') ++ suffix) start is_inc
 
-val access : forall 'a. vector 'a -> (*nat*) integer -> 'a
+val access : forall 'a. vector 'a -> integer -> 'a
 let access (Vector bs start is_inc) n =
   if is_inc then nth bs (n - start) else nth bs (start - n)
 
-val update_pos : forall 'a. vector 'a -> (*nat*) integer -> 'a -> vector 'a
+val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
 let update_pos v n b =
   update v n n (Vector [b] 0 true)