diff options
| author | Christopher Pulte | 2016-09-25 15:14:12 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-09-25 15:14:12 +0100 |
| commit | dd052bfc3e00a1ae988044ae81dd1624332dd899 (patch) | |
| tree | 357d6e14136545dce7d0d120b7c1e5bccf27970d /src/gen_lib/sail_values.lem | |
| parent | 6e7cee1575a7c49f4bdc30dfd6f25546c6c70995 (diff) | |
nicer lem output: no more unecessary 'unit' returns if if-expressions, for-loops or case-expressions also return updated variables
Diffstat (limited to 'src/gen_lib/sail_values.lem')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 27 |
1 files changed, 13 insertions, 14 deletions
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 + + + |