diff options
Diffstat (limited to 'src/gen_lib/sail2_string.lem')
| -rw-r--r-- | src/gen_lib/sail2_string.lem | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/gen_lib/sail2_string.lem b/src/gen_lib/sail2_string.lem index a54ffa65..3374d800 100644 --- a/src/gen_lib/sail2_string.lem +++ b/src/gen_lib/sail2_string.lem @@ -30,10 +30,8 @@ let string_append = stringAppend ***********************************************) val maybeIntegerOfString : string -> maybe integer - +let maybeIntegerOfString _ = Nothing (* TODO FIXME *) declare ocaml target_rep function maybeIntegerOfString = `(fun s -> match int_of_string_opt s with None -> None | Some i -> Some (Nat_big_num.of_int i))` -declare isabelle target_rep function maybeIntegerOfString = `maybeIntegerOfString` (* TODO FIXME *) -declare hol target_rep function maybeIntegerOfString = `maybeIntegerOfString` (* TODO FIXME *) (*********************************************** * end stuff that should be in Lem Num_extra * @@ -65,10 +63,12 @@ let rec n_leading_spaces s = (* match len with * (\* | 0 -> 0 *\) * (\* | 1 -> *\) - * | len -> *) match nth s 0 with - | #' ' -> 1 + (n_leading_spaces (string_sub s 1 (len - 1))) - | _ -> 0 - end + * | len -> *) + (* Isabelle generation for pattern matching on characters + is currently broken, so use an if-expression *) + if nth s 0 = #' ' + then 1 + (n_leading_spaces (string_sub s 1 (len - 1))) + else 0 (* end *) let opt_spc_matches_prefix s = |