diff options
| author | Thomas Bauereiss | 2018-06-21 17:50:54 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-06-21 17:54:17 +0100 |
| commit | 2005eb7c190f8d28d6499df3dd77cf65a87e60cb (patch) | |
| tree | 73f7c9d58e77f8ff08832b211779ba2789c8f8f7 /src/gen_lib | |
| parent | 3f626070c3fcba7871f6364630b05fa62d36c5c8 (diff) | |
Follow Sail2 renaming in Isabelle library
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 = |