diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail2_prompt.lem | 2 | ||||
| -rw-r--r-- | src/gen_lib/sail2_string.lem | 14 |
2 files changed, 8 insertions, 8 deletions
diff --git a/src/gen_lib/sail2_prompt.lem b/src/gen_lib/sail2_prompt.lem index 434df843..08a47052 100644 --- a/src/gen_lib/sail2_prompt.lem +++ b/src/gen_lib/sail2_prompt.lem @@ -2,7 +2,7 @@ open import Pervasives_extra (*open import Sail_impl_base*) open import Sail2_values open import Sail2_prompt_monad -open import {isabelle} `Prompt_monad_lemmas` +open import {isabelle} `Sail2_prompt_monad_lemmas` val (>>=) : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e declare isabelle target_rep function (>>=) = infix `\<bind>` 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 = |