From 2005eb7c190f8d28d6499df3dd77cf65a87e60cb Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 21 Jun 2018 17:50:54 +0100
Subject: Follow Sail2 renaming in Isabelle library

---
 src/gen_lib/sail2_prompt.lem |  2 +-
 src/gen_lib/sail2_string.lem | 14 +++++++-------
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'src/gen_lib')

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 =
-- 
cgit v1.2.3